Rename mkSygusGrammar to mkGrammar (#8544)

diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp
index 15a53c36e7f743c41cec54044c87869355928602..b9e939f38722315a0f8eb2254d21d630b8c74351 100644 (file)
--- a/examples/api/cpp/sygus-fun.cpp
+++ b/examples/api/cpp/sygus-fun.cpp
@@ -59,7 +59,7 @@ int main()
   Term leq = slv.mkTerm(LEQ, {start, start});
 
   // create the grammar object
-  Grammar g = slv.mkSygusGrammar({x, y}, {start, start_bool});
+  Grammar g = slv.mkGrammar({x, y}, {start, start_bool});
 
   // bind each non-terminal to its rules
   g.addRules(start, {zero, one, x, y, plus, minus, ite});

diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp
index a69382e120ed21b4f6c12eb24f595097dca0e9c5..a5f051c6c23dc5e8560994b500d2c3651026c82b 100644 (file)
--- a/examples/api/cpp/sygus-grammar.cpp
+++ b/examples/api/cpp/sygus-grammar.cpp
@@ -49,7 +49,7 @@ int main()
   Term plus = slv.mkTerm(ADD, {x, start});
 
   // create the grammar object
-  Grammar g1 = slv.mkSygusGrammar({x}, {start});
+  Grammar g1 = slv.mkGrammar({x}, {start});
 
   // bind each non-terminal to its rules
   g1.addRules(start, {neg_x, plus});

diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java
index 4f06267489ae964adf869e3c6c2b7297790d6530..aa52fd008c520f4eb6bb6d9c47e36ced75c990e6 100644 (file)
--- a/examples/api/java/SygusFun.java
+++ b/examples/api/java/SygusFun.java
@@ -57,7 +57,8 @@ public class SygusFun
       Term leq = slv.mkTerm(LEQ, start, start);
 
       // create the grammar object
-      Grammar g = slv.mkSygusGrammar(new Term[] {x, y}, new Term[] {start, start_bool});
+      Grammar g =
+          slv.mkGrammar(new Term[] {x, y}, new Term[] {start, start_bool});
 
       // bind each non-terminal to its rules
       g.addRules(start, new Term[] {zero, one, x, y, plus, minus, ite});

diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java
index c97fb23e00f6de8ae43045ac4e4f12cc50287b1d..35c4b984639fbaf7c2165272382b3c85f6c4a8a3 100644 (file)
--- a/examples/api/java/SygusGrammar.java
+++ b/examples/api/java/SygusGrammar.java
@@ -48,7 +48,7 @@ public class SygusGrammar
       Term plus = slv.mkTerm(ADD, x, start);
 
       // create the grammar object
-      Grammar g1 = slv.mkSygusGrammar(new Term[] {x}, new Term[] {start});
+      Grammar g1 = slv.mkGrammar(new Term[] {x}, new Term[] {start});
 
       // bind each non-terminal to its rules
       g1.addRules(start, new Term[] {neg_x, plus});

diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index 9781ddb672126515cf72de7770ed30030bceb237..f81fd7fd4554b41ce01141fbecc6cb5e6dad04f9 100644 (file)
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -54,7 +54,7 @@ if __name__ == "__main__":
   leq = slv.mkTerm(Kind.LEQ, start, start)
 
   # create the grammar object
-  g = slv.mkSygusGrammar([x, y], [start, start_bool])
+  g = slv.mkGrammar([x, y], [start, start_bool])
 
   # bind each non-terminal to its rules
   g.addRules(start, {zero, one, x, y, plus, minus, ite})

diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index c70b0d9c88e615b73ffdf0bc2a994da455ea2152..20eb0ddf8a21b2909924153f1063b731a90db392 100644 (file)
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -45,9 +45,9 @@ if __name__ == "__main__":
   plus = slv.mkTerm(Kind.ADD, x, start)
 
   # create the grammar object
-  g1 = slv.mkSygusGrammar({x}, {start})
-  g2 = slv.mkSygusGrammar({x}, {start})
-  g3 = slv.mkSygusGrammar({x}, {start})
+  g1 = slv.mkGrammar({x}, {start})
+  g2 = slv.mkGrammar({x}, {start})
+  g3 = slv.mkGrammar({x}, {start})
 
   # bind each non-terminal to its rules
   g1.addRules(start, {neg_x, plus})

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 1c9d85240bd6354c3f8017a6459e92d4b34e77f2..768ec181b18e5ed5767881e3b6c8b34fb36d6acd 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7378,8 +7378,8 @@ Term Solver::declareSygusVar(const std::string& symbol, const Sort& sort) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
-                               const std::vector<Term>& ntSymbols) const
+Grammar Solver::mkGrammar(const std::vector<Term>& boundVars,
+                          const std::vector<Term>& ntSymbols) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index eba7dbdb9d6ea85b95166a168c0f24e067be430c..ef366cfe5becc2d27dc8e51a942df02d17d3abe4 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4681,8 +4681,8 @@ class CVC5_EXPORT Solver
    * @param ntSymbols the pre-declaration of the non-terminal symbols
    * @return the grammar
    */
-  Grammar mkSygusGrammar(const std::vector<Term>& boundVars,
-                         const std::vector<Term>& ntSymbols) const;
+  Grammar mkGrammar(const std::vector<Term>& boundVars,
+                    const std::vector<Term>& ntSymbols) const;
 
   /**
    * Synthesize n-ary function.

diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java
index feaed83e5571e436af711054bd935abf209b5b07..87ca11cc0a5ff6f3c341055e19a62c2586b835ff 100644 (file)
--- a/src/api/java/io/github/cvc5/Solver.java
+++ b/src/api/java/io/github/cvc5/Solver.java
@@ -2457,15 +2457,15 @@ public class Solver implements IPointer, AutoCloseable
    * @param ntSymbols the pre-declaration of the non-terminal symbols
    * @return the grammar
    */
-  public Grammar mkSygusGrammar(Term[] boundVars, Term[] ntSymbols)
-  {
+  public Grammar mkGrammar(Term[] boundVars, Term[] ntSymbols) {
     long[] boundVarPointers = Utils.getPointers(boundVars);
     long[] ntSymbolPointers = Utils.getPointers(ntSymbols);
-    long grammarPointer = mkSygusGrammar(pointer, boundVarPointers, ntSymbolPointers);
+    long grammarPointer =
+        mkGrammar(pointer, boundVarPointers, ntSymbolPointers);
     return new Grammar(this, grammarPointer);
   }
 
-  private native long mkSygusGrammar(
+  private native long mkGrammar(
       long pointer, long[] boundVarPointers, long[] ntSymbolPointers);
 
   /**

diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index 75db6960a5e13f2cbcd5e3574e4e78795f15b08c..a5a93a61aee2cba5a726e74addf21ef62f574813 100644 (file)
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -2395,22 +2395,21 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_declareSygusVar(
 
 /*
  * Class:     io_github_cvc5_Solver
- * Method:    mkSygusGrammar
+ * Method:    mkGrammar
  * Signature: (J[J[J)J
  */
 JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_mkSygusGrammar(JNIEnv* env,
-                                              jobject,
-                                              jlong pointer,
-                                              jlongArray jBoundVars,
-                                              jlongArray jNtSymbols)
+Java_io_github_cvc5_Solver_mkGrammar(JNIEnv* env,
+                                     jobject,
+                                     jlong pointer,
+                                     jlongArray jBoundVars,
+                                     jlongArray jNtSymbols)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   std::vector<Term> boundVars = getObjectsFromPointers<Term>(env, jBoundVars);
   std::vector<Term> ntSymbols = getObjectsFromPointers<Term>(env, jNtSymbols);
-  Grammar* retPointer =
-      new Grammar(solver->mkSygusGrammar(boundVars, ntSymbols));
+  Grammar* retPointer = new Grammar(solver->mkGrammar(boundVars, ntSymbols));
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index c6209434100735122b503f97feb39d12ff0deecc..52d6974922d202e25981e77864fcf0587c0d74b3 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -237,7 +237,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         Op mkOp(Kind kind, const string& arg) except +
         Op mkOp(Kind kind, const vector[uint32_t]& args) except +
         # Sygus related functions
-        Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except +
+        Grammar mkGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except +
         Term declareSygusVar(const string& symbol, Sort sort) except +
         void addSygusConstraint(Term term) except +
         void addSygusAssume(Term term) except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 441648f671d236dcc84e12338870f43a5261025e..90aa5deccf03ed61233497de8d0fb5f94546cca5 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1656,7 +1656,7 @@ cdef class Solver:
         r.cr = self.csolver.checkSat()
         return r
 
-    def mkSygusGrammar(self, boundVars, ntSymbols):
+    def mkGrammar(self, boundVars, ntSymbols):
         """
             Create a SyGuS grammar. The first non-terminal is treated as the
             starting non-terminal, so the order of non-terminals matters.
@@ -1673,7 +1673,7 @@ cdef class Solver:
             bvc.push_back((<Term?> bv).cterm)
         for nt in ntSymbols:
             ntc.push_back((<Term?> nt).cterm)
-        grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
+        grammar.cgrammar = self.csolver.mkGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
         return grammar
 
     def declareSygusVar(self, str symbol, Sort sort):

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 63cc3af4e24a206ed63ad654777ce4e0613e7dc8..3bdf8a08c7cfd124dc1620f4049c4e2f0eb31d8d 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -711,7 +711,7 @@ cvc5::Grammar* Smt2::mkGrammar(const std::vector<cvc5::Term>& boundVars,
                                const std::vector<cvc5::Term>& ntSymbols)
 {
   d_allocGrammars.emplace_back(
-      new cvc5::Grammar(d_solver->mkSygusGrammar(boundVars, ntSymbols)));
+      new cvc5::Grammar(d_solver->mkGrammar(boundVars, ntSymbols)));
   return d_allocGrammars.back().get();
 }
 

diff --git a/test/unit/api/cpp/grammar_black.cpp b/test/unit/api/cpp/grammar_black.cpp
index 0b5899f88ff75e7e1efb4da5aaa8668ab5d35324..be05d39c82a8c398204d7f08728ff97b550772fe 100644 (file)
--- a/test/unit/api/cpp/grammar_black.cpp
+++ b/test/unit/api/cpp/grammar_black.cpp
@@ -33,7 +33,7 @@ TEST_F(TestApiBlackGrammar, addRule)
   Term start = d_solver.mkVar(boolean);
   Term nts = d_solver.mkVar(boolean);
 
-  Grammar g = d_solver.mkSygusGrammar({}, {start});
+  Grammar g = d_solver.mkGrammar({}, {start});
 
   ASSERT_NO_THROW(g.addRule(start, d_solver.mkBoolean(false)));
 
@@ -59,7 +59,7 @@ TEST_F(TestApiBlackGrammar, addRules)
   Term start = d_solver.mkVar(boolean);
   Term nts = d_solver.mkVar(boolean);
 
-  Grammar g = d_solver.mkSygusGrammar({}, {start});
+  Grammar g = d_solver.mkGrammar({}, {start});
 
   ASSERT_NO_THROW(g.addRules(start, {d_solver.mkBoolean(false)}));
 
@@ -85,7 +85,7 @@ TEST_F(TestApiBlackGrammar, addAnyConstant)
   Term start = d_solver.mkVar(boolean);
   Term nts = d_solver.mkVar(boolean);
 
-  Grammar g = d_solver.mkSygusGrammar({}, {start});
+  Grammar g = d_solver.mkGrammar({}, {start});
 
   ASSERT_NO_THROW(g.addAnyConstant(start));
   ASSERT_NO_THROW(g.addAnyConstant(start));
@@ -108,8 +108,8 @@ TEST_F(TestApiBlackGrammar, addAnyVariable)
   Term start = d_solver.mkVar(boolean);
   Term nts = d_solver.mkVar(boolean);
 
-  Grammar g1 = d_solver.mkSygusGrammar({x}, {start});
-  Grammar g2 = d_solver.mkSygusGrammar({}, {start});
+  Grammar g1 = d_solver.mkGrammar({x}, {start});
+  Grammar g2 = d_solver.mkGrammar({}, {start});
 
   ASSERT_NO_THROW(g1.addAnyVariable(start));
   ASSERT_NO_THROW(g1.addAnyVariable(start));

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 7183d1d0c1f0672b0bbe917aa2a3121933b5961d..1e0ff5a66d149cb40dc70cfd5ad0359f512f7057 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1357,7 +1357,7 @@ TEST_F(TestApiBlackSolver, getAbduct)
   Term truen = d_solver.mkBoolean(true);
   Term start = d_solver.mkVar(boolean);
   Term output2;
-  Grammar g = d_solver.mkSygusGrammar({}, {start});
+  Grammar g = d_solver.mkGrammar({}, {start});
   Term conj2 = d_solver.mkTerm(GT, {x, zero});
   ASSERT_NO_THROW(g.addRule(start, truen));
   // Call the abduction api, while the resulting abduct is the output
@@ -2530,25 +2530,25 @@ TEST_F(TestApiBlackSolver, declareSygusVar)
   ASSERT_THROW(slv.declareSygusVar("", boolSort), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, mkSygusGrammar)
+TEST_F(TestApiBlackSolver, mkGrammar)
 {
   Term nullTerm;
   Term boolTerm = d_solver.mkBoolean(true);
   Term boolVar = d_solver.mkVar(d_solver.getBooleanSort());
   Term intVar = d_solver.mkVar(d_solver.getIntegerSort());
 
-  ASSERT_NO_THROW(d_solver.mkSygusGrammar({}, {intVar}));
-  ASSERT_NO_THROW(d_solver.mkSygusGrammar({boolVar}, {intVar}));
-  ASSERT_THROW(d_solver.mkSygusGrammar({}, {}), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkSygusGrammar({}, {nullTerm}), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkSygusGrammar({}, {boolTerm}), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkSygusGrammar({boolTerm}, {intVar}), CVC5ApiException);
+  ASSERT_NO_THROW(d_solver.mkGrammar({}, {intVar}));
+  ASSERT_NO_THROW(d_solver.mkGrammar({boolVar}, {intVar}));
+  ASSERT_THROW(d_solver.mkGrammar({}, {}), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkGrammar({}, {nullTerm}), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkGrammar({}, {boolTerm}), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkGrammar({boolTerm}, {intVar}), CVC5ApiException);
   Solver slv;
   Term boolVar2 = slv.mkVar(slv.getBooleanSort());
   Term intVar2 = slv.mkVar(slv.getIntegerSort());
-  ASSERT_NO_THROW(slv.mkSygusGrammar({boolVar2}, {intVar2}));
-  ASSERT_THROW(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC5ApiException);
-  ASSERT_THROW(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC5ApiException);
+  ASSERT_NO_THROW(slv.mkGrammar({boolVar2}, {intVar2}));
+  ASSERT_THROW(slv.mkGrammar({boolVar}, {intVar2}), CVC5ApiException);
+  ASSERT_THROW(slv.mkGrammar({boolVar2}, {intVar}), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, synthFun)
@@ -2564,10 +2564,10 @@ TEST_F(TestApiBlackSolver, synthFun)
   Term start1 = d_solver.mkVar(boolean);
   Term start2 = d_solver.mkVar(integer);
 
-  Grammar g1 = d_solver.mkSygusGrammar({x}, {start1});
+  Grammar g1 = d_solver.mkGrammar({x}, {start1});
   g1.addRule(start1, d_solver.mkBoolean(false));
 
-  Grammar g2 = d_solver.mkSygusGrammar({x}, {start2});
+  Grammar g2 = d_solver.mkGrammar({x}, {start2});
   g2.addRule(start2, d_solver.mkInteger(0));
 
   ASSERT_NO_THROW(d_solver.synthFun("", {}, boolean));
@@ -2599,10 +2599,10 @@ TEST_F(TestApiBlackSolver, synthInv)
   Term start1 = d_solver.mkVar(boolean);
   Term start2 = d_solver.mkVar(integer);
 
-  Grammar g1 = d_solver.mkSygusGrammar({x}, {start1});
+  Grammar g1 = d_solver.mkGrammar({x}, {start1});
   g1.addRule(start1, d_solver.mkBoolean(false));
 
-  Grammar g2 = d_solver.mkSygusGrammar({x}, {start2});
+  Grammar g2 = d_solver.mkGrammar({x}, {start2});
   g2.addRule(start2, d_solver.mkInteger(0));
 
   ASSERT_NO_THROW(d_solver.synthInv("", {}));

diff --git a/test/unit/api/java/GrammarTest.java b/test/unit/api/java/GrammarTest.java
index 0e71ddd5302fe2ad28f4fed9665545deab486774..f72190a096ddd7e37fb694775b0034525d208ce3 100644 (file)
--- a/test/unit/api/java/GrammarTest.java
+++ b/test/unit/api/java/GrammarTest.java
@@ -50,7 +50,7 @@ class GrammarTest
     Term start = d_solver.mkVar(bool);
     Term nts = d_solver.mkVar(bool);
 
-    Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+    Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start});
 
     assertDoesNotThrow(() -> g.addRule(start, d_solver.mkBoolean(false)));
 
@@ -76,7 +76,7 @@ class GrammarTest
     Term start = d_solver.mkVar(bool);
     Term nts = d_solver.mkVar(bool);
 
-    Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+    Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start});
 
     assertDoesNotThrow(() -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)}));
 
@@ -105,7 +105,7 @@ class GrammarTest
     Term start = d_solver.mkVar(bool);
     Term nts = d_solver.mkVar(bool);
 
-    Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+    Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start});
 
     assertDoesNotThrow(() -> g.addAnyConstant(start));
     assertDoesNotThrow(() -> g.addAnyConstant(start));
@@ -129,8 +129,8 @@ class GrammarTest
     Term start = d_solver.mkVar(bool);
     Term nts = d_solver.mkVar(bool);
 
-    Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start});
-    Grammar g2 = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+    Grammar g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start});
+    Grammar g2 = d_solver.mkGrammar(new Term[] {}, new Term[] {start});
 
     assertDoesNotThrow(() -> g1.addAnyVariable(start));
     assertDoesNotThrow(() -> g1.addAnyVariable(start));

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 6327bb553b8f7ab2e0e88e57ad7a21f1af254957..4cfbfcb88b681af6b086773df587b3faedf924cc 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1418,7 +1418,7 @@ class SolverTest
     Term truen = d_solver.mkBoolean(true);
     Term start = d_solver.mkVar(bsort);
     Term output2 = d_solver.getNullTerm();
-    Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
+    Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start});
     Term conj2 = d_solver.mkTerm(GT, x, zero);
     assertDoesNotThrow(() -> g.addRule(start, truen));
     // Call the abduction api, while the resulting abduct is the output
@@ -2599,35 +2599,37 @@ class SolverTest
   }
 
   @Test
-  void mkSygusGrammar() throws CVC5ApiException
-  {
+  void mkGrammar() throws CVC5ApiException {
     Term nullTerm = d_solver.getNullTerm();
     Term boolTerm = d_solver.mkBoolean(true);
     Term boolVar = d_solver.mkVar(d_solver.getBooleanSort());
     Term intVar = d_solver.mkVar(d_solver.getIntegerSort());
 
-    assertDoesNotThrow(() -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {intVar}));
-    assertDoesNotThrow(() -> d_solver.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar}));
+    assertDoesNotThrow(
+        () -> d_solver.mkGrammar(new Term[] {}, new Term[] {intVar}));
+    assertDoesNotThrow(
+        () -> d_solver.mkGrammar(new Term[] {boolVar}, new Term[] {intVar}));
 
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {}));
     assertThrows(CVC5ApiException.class,
-        () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {nullTerm}));
+        () -> d_solver.mkGrammar(new Term[] {}, new Term[] {}));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkGrammar(new Term[] {}, new Term[] {nullTerm}));
     assertThrows(CVC5ApiException.class,
-        () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {boolTerm}));
+        () -> d_solver.mkGrammar(new Term[] {}, new Term[] {boolTerm}));
     assertThrows(CVC5ApiException.class,
-        () -> d_solver.mkSygusGrammar(new Term[] {boolTerm}, new Term[] {intVar}));
+        () -> d_solver.mkGrammar(new Term[] {boolTerm}, new Term[] {intVar}));
 
     Solver slv = new Solver();
     slv.setOption("sygus", "true");
     Term boolVar2 = slv.mkVar(slv.getBooleanSort());
     Term intVar2 = slv.mkVar(slv.getIntegerSort());
-    assertDoesNotThrow(() -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar2}));
+    assertDoesNotThrow(
+        () -> slv.mkGrammar(new Term[] {boolVar2}, new Term[] {intVar2}));
 
     assertThrows(CVC5ApiException.class,
-        () -> slv.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar2}));
+        () -> slv.mkGrammar(new Term[] {boolVar}, new Term[] {intVar2}));
     assertThrows(CVC5ApiException.class,
-        () -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar}));
+        () -> slv.mkGrammar(new Term[] {boolVar2}, new Term[] {intVar}));
     slv.close();
   }
 
@@ -2645,10 +2647,10 @@ class SolverTest
     Term start1 = d_solver.mkVar(bool);
     Term start2 = d_solver.mkVar(integer);
 
-    Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start1});
+    Grammar g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
     g1.addRule(start1, d_solver.mkBoolean(false));
 
-    Grammar g2 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start2});
+    Grammar g2 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start2});
     g2.addRule(start2, d_solver.mkInteger(0));
 
     assertDoesNotThrow(() -> d_solver.synthFun("", new Term[] {}, bool));
@@ -2685,10 +2687,10 @@ class SolverTest
     Term start1 = d_solver.mkVar(bool);
     Term start2 = d_solver.mkVar(integer);
 
-    Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start1});
+    Grammar g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
     g1.addRule(start1, d_solver.mkBoolean(false));
 
-    Grammar g2 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start2});
+    Grammar g2 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start2});
     g2.addRule(start2, d_solver.mkInteger(0));
 
     assertDoesNotThrow(() -> d_solver.synthInv("", new Term[] {}));

diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py
index 6bdd504f237865c0732487579ec8d5d9193f9768..1c00da13c706f85d2252d573867e6d8b93910a5c 100644 (file)
--- a/test/unit/api/python/test_grammar.py
+++ b/test/unit/api/python/test_grammar.py
@@ -34,7 +34,7 @@ def test_add_rule(solver):
     nts = solver.mkVar(boolean)
 
     # expecting no error
-    g = solver.mkSygusGrammar([], [start])
+    g = solver.mkGrammar([], [start])
 
     g.addRule(start, solver.mkBoolean(False))
 
@@ -67,7 +67,7 @@ def test_add_rules(solver):
     start = solver.mkVar(boolean)
     nts = solver.mkVar(boolean)
 
-    g = solver.mkSygusGrammar([], [start])
+    g = solver.mkGrammar([], [start])
 
     g.addRules(start, {solver.mkBoolean(False)})
 
@@ -98,7 +98,7 @@ def test_add_any_constant(solver):
     start = solver.mkVar(boolean)
     nts = solver.mkVar(boolean)
 
-    g = solver.mkSygusGrammar({}, {start})
+    g = solver.mkGrammar({}, {start})
 
     g.addAnyConstant(start)
     g.addAnyConstant(start)
@@ -123,8 +123,8 @@ def test_add_any_variable(solver):
     start = solver.mkVar(boolean)
     nts = solver.mkVar(boolean)
 
-    g1 = solver.mkSygusGrammar({x}, {start})
-    g2 = solver.mkSygusGrammar({}, {start})
+    g1 = solver.mkGrammar({x}, {start})
+    g2 = solver.mkGrammar({}, {start})
 
     g1.addAnyVariable(start)
     g1.addAnyVariable(start)

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 657df330659433e9d728c646c018f649457c26ef..019edc251928a75b19a4286e69dd08236ad6f689 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -1885,24 +1885,24 @@ def test_mk_sygus_grammar(solver):
     boolVar = solver.mkVar(solver.getBooleanSort())
     intVar = solver.mkVar(solver.getIntegerSort())
 
-    solver.mkSygusGrammar([], [intVar])
-    solver.mkSygusGrammar([boolVar], [intVar])
+    solver.mkGrammar([], [intVar])
+    solver.mkGrammar([boolVar], [intVar])
     with pytest.raises(RuntimeError):
-        solver.mkSygusGrammar([], [])
+        solver.mkGrammar([], [])
     with pytest.raises(RuntimeError):
-        solver.mkSygusGrammar([], [nullTerm])
+        solver.mkGrammar([], [nullTerm])
     with pytest.raises(RuntimeError):
-        solver.mkSygusGrammar([], [boolTerm])
+        solver.mkGrammar([], [boolTerm])
     with pytest.raises(RuntimeError):
-        solver.mkSygusGrammar([boolTerm], [intVar])
+        solver.mkGrammar([boolTerm], [intVar])
     slv = cvc5.Solver()
     boolVar2 = slv.mkVar(slv.getBooleanSort())
     intVar2 = slv.mkVar(slv.getIntegerSort())
-    slv.mkSygusGrammar([boolVar2], [intVar2])
+    slv.mkGrammar([boolVar2], [intVar2])
     with pytest.raises(RuntimeError):
-        slv.mkSygusGrammar([boolVar], [intVar2])
+        slv.mkGrammar([boolVar], [intVar2])
     with pytest.raises(RuntimeError):
-        slv.mkSygusGrammar([boolVar2], [intVar])
+        slv.mkGrammar([boolVar2], [intVar])
 
 
 def test_synth_inv(solver):
@@ -1916,10 +1916,10 @@ def test_synth_inv(solver):
     start1 = solver.mkVar(boolean)
     start2 = solver.mkVar(integer)
 
-    g1 = solver.mkSygusGrammar([x], [start1])
+    g1 = solver.mkGrammar([x], [start1])
     g1.addRule(start1, solver.mkBoolean(False))
 
-    g2 = solver.mkSygusGrammar([x], [start2])
+    g2 = solver.mkGrammar([x], [start2])
     g2.addRule(start2, solver.mkInteger(0))
 
     solver.synthInv("", [])
@@ -2114,7 +2114,7 @@ def test_get_abduct(solver):
     truen = solver.mkBoolean(True)
     start = solver.mkVar(boolean)
     output2 = cvc5.Term(solver)
-    g = solver.mkSygusGrammar([], [start])
+    g = solver.mkGrammar([], [start])
     conj2 = solver.mkTerm(Kind.GT, x, zero)
     g.addRule(start, truen)
     output2 = solver.getAbduct(conj2, g)
@@ -2520,10 +2520,10 @@ def test_synth_fun(solver):
     start1 = solver.mkVar(boolean)
     start2 = solver.mkVar(integer)
 
-    g1 = solver.mkSygusGrammar(x, [start1])
+    g1 = solver.mkGrammar(x, [start1])
     g1.addRule(start1, solver.mkBoolean(False))
 
-    g2 = solver.mkSygusGrammar(x, [start2])
+    g2 = solver.mkGrammar(x, [start2])
     g2.addRule(start2, solver.mkInteger(0))
 
     solver.synthFun("", [], boolean)