api: Swap arguments of declareSygusVar. (#8499)

Make it consistent with other declare*/define* functions.

diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp
index 864ab6a111764f50aa49691a8ab9de6224903874..15a53c36e7f743c41cec54044c87869355928602 100644 (file)
--- a/examples/api/cpp/sygus-fun.cpp
+++ b/examples/api/cpp/sygus-fun.cpp
@@ -71,8 +71,8 @@ int main()
   Term min = slv.synthFun("min", {x, y}, integer);
 
   // declare universal variables.
-  Term varX = slv.declareSygusVar(integer, "x");
-  Term varY = slv.declareSygusVar(integer, "y");
+  Term varX = slv.declareSygusVar("x", integer);
+  Term varY = slv.declareSygusVar("y", integer);
 
   Term max_x_y = slv.mkTerm(APPLY_UF, {max, varX, varY});
   Term min_x_y = slv.mkTerm(APPLY_UF, {min, varX, varY});

diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp
index cca30d301b9baf86c9c5c79594877ac8214a9321..a69382e120ed21b4f6c12eb24f595097dca0e9c5 100644 (file)
--- a/examples/api/cpp/sygus-grammar.cpp
+++ b/examples/api/cpp/sygus-grammar.cpp
@@ -73,7 +73,7 @@ int main()
   Term id4 = slv.synthFun("id4", {x}, integer, g1);
 
   // declare universal variables.
-  Term varX = slv.declareSygusVar(integer, "x");
+  Term varX = slv.declareSygusVar("x", integer);
 
   Term id1_x = slv.mkTerm(APPLY_UF, {id1, varX});
   Term id2_x = slv.mkTerm(APPLY_UF, {id2, varX});

diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java
index 3ce5a5e45501ef7f082e32f25dddd99d74a483a1..4f06267489ae964adf869e3c6c2b7297790d6530 100644 (file)
--- a/examples/api/java/SygusFun.java
+++ b/examples/api/java/SygusFun.java
@@ -69,8 +69,8 @@ public class SygusFun
       Term min = slv.synthFun("min", new Term[] {x, y}, integer);
 
       // declare universal variables.
-      Term varX = slv.declareSygusVar(integer, "x");
-      Term varY = slv.declareSygusVar(integer, "y");
+      Term varX = slv.declareSygusVar("x", integer);
+      Term varY = slv.declareSygusVar("y", integer);
 
       Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY);
       Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY);

diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java
index 127da1c5f7efac370584919931fb0dc2670841bf..c97fb23e00f6de8ae43045ac4e4f12cc50287b1d 100644 (file)
--- a/examples/api/java/SygusGrammar.java
+++ b/examples/api/java/SygusGrammar.java
@@ -72,7 +72,7 @@ public class SygusGrammar
       Term id4 = slv.synthFun("id4", new Term[] {x}, integer, g1);
 
       // declare universal variables.
-      Term varX = slv.declareSygusVar(integer, "x");
+      Term varX = slv.declareSygusVar("x", integer);
 
       Term id1_x = slv.mkTerm(APPLY_UF, id1, varX);
       Term id2_x = slv.mkTerm(APPLY_UF, id2, varX);

diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index 94cd26d6be173ea9784d1316d9564e6fd5008caa..9903070419f1d147f2caea43ac94640469a8c660 100644 (file)
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -66,8 +66,8 @@ if __name__ == "__main__":
   min = slv.synthFun("min", [x, y], integer)
 
   # declare universal variables.
-  varX = slv.declareSygusVar(integer, "x")
-  varY = slv.declareSygusVar(integer, "y")
+  varX = slv.declareSygusVar("x", integer)
+  varY = slv.declareSygusVar("y", integer)
 
   max_x_y = slv.mkTerm(Kind.ApplyUf, max, varX, varY)
   min_x_y = slv.mkTerm(Kind.ApplyUf, min, varX, varY)

diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index 1613f659516c00a40d1bce9280f0635a104e9398..618bd206952ec272a6a09a62cffef8e49f0b6f11 100644 (file)
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -69,7 +69,7 @@ if __name__ == "__main__":
   id4 = slv.synthFun("id4", {x}, integer, g1)
 
   # declare universal variables.
-  varX = slv.declareSygusVar(integer, "x")
+  varX = slv.declareSygusVar("x", integer)
 
   id1_x = slv.mkTerm(Kind.ApplyUf, id1, varX)
   id2_x = slv.mkTerm(Kind.ApplyUf, id2, varX)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 3cc67a0c7ca891d5dc0a9b3cfe56abb0ca765665..7534eceaabe3b5a62ffa16fc07286bf36520a2e1 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7426,7 +7426,7 @@ void Solver::setOption(const std::string& option,
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::declareSygusVar(const Sort& sort, const std::string& symbol) const
+Term Solver::declareSygusVar(const std::string& symbol, const Sort& sort) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 96fe3775f6b9b268683d9efe92a5f0fe9b6e9cd6..2358ee879e82fc8423d427713149594ff1ae8cf7 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4636,8 +4636,7 @@ class CVC5_EXPORT Solver
    * @param symbol the name of the universal variable
    * @return the universal variable
    */
-  Term declareSygusVar(const Sort& sort,
-                       const std::string& symbol = std::string()) const;
+  Term declareSygusVar(const std::string& symbol, const Sort& sort) const;
 
   /**
    * Create a Sygus grammar. The first non-terminal is treated as the starting

diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java
index 885ccc359c5a52d31da84d58dc21072fc0ae09d5..384824e5d5a63a22c6933ca798ecc5299d842dff 100644 (file)
--- a/src/api/java/io/github/cvc5/Solver.java
+++ b/src/api/java/io/github/cvc5/Solver.java
@@ -2556,15 +2556,6 @@ public class Solver implements IPointer, AutoCloseable
 
   private native void setOption(long pointer, String option, String value);
 
-  /**
-   * Append \p symbol to the current list of universal variables.
-   * @param sort the sort of the universal variable
-   * @return the universal variable
-   */
-  public Term declareSygusVar(Sort sort)
-  {
-    return declareSygusVar(sort, "");
-  }
   /**
    * Append \p symbol to the current list of universal variables.
    * SyGuS v2:
@@ -2575,13 +2566,13 @@ public class Solver implements IPointer, AutoCloseable
    * @param symbol the name of the universal variable
    * @return the universal variable
    */
-  public Term declareSygusVar(Sort sort, String symbol)
+  public Term declareSygusVar(String symbol, Sort sort)
   {
-    long termPointer = declareSygusVar(pointer, sort.getPointer(), symbol);
+    long termPointer = declareSygusVar(pointer, symbol, sort.getPointer());
     return new Term(this, termPointer);
   }
 
-  private native long declareSygusVar(long pointer, long sortPointer, String symbol);
+  private native long declareSygusVar(long pointer, String symbol, long sortPointer);
 
   /**
    * Create a Sygus grammar. The first non-terminal is treated as the starting

diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index b83560e9f302a94297ef943c42f03bd4106fd388..f21434dd23b3248ce7fe03cdd1863b6573529ba6 100644 (file)
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -2446,17 +2446,17 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_setOption(
 /*
  * Class:     io_github_cvc5_Solver
  * Method:    declareSygusVar
- * Signature: (JJLjava/lang/String;)J
+ * Signature: (JJjava/lang/String;L)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_declareSygusVar(
-    JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol)
+    JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jlong sortPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
   std::string cSymbol(s);
-  Term* retPointer = new Term(solver->declareSygusVar(*sort, cSymbol));
+  Term* retPointer = new Term(solver->declareSygusVar(cSymbol, *sort));
   env->ReleaseStringUTFChars(jSymbol, s);
   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 05e06b6954f179693926d21bc278902481675d39..929c03900b72d74c9f069042b1730970fcbda63c 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -241,8 +241,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         Op mkOp(Kind kind, const vector[uint32_t]& args) except +
         # Sygus related functions
         Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except +
-        Term declareSygusVar(Sort sort, const string& symbol) except +
-        Term declareSygusVar(Sort sort) except +
+        Term declareSygusVar(const string& symbol, Sort sort) except +
         void addSygusConstraint(Term term) except +
         void addSygusAssume(Term term) except +
         void addSygusInvConstraint(Term inv_f, Term pre_f, Term trans_f, Term post_f) except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index a5c3c3f7edd4e62c127dcea40e5c570646fb63c2..eb0e749bd501b1fb973a826b864e4e4665d373bc 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1550,7 +1550,7 @@ cdef class Solver:
         grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
         return grammar
 
-    def declareSygusVar(self, Sort sort, str symbol=""):
+    def declareSygusVar(self, str symbol, Sort sort):
         """Append symbol to the current list of universal variables.
 
         SyGuS v2:
@@ -1564,7 +1564,7 @@ cdef class Solver:
         :return: the universal variable
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.declareSygusVar(sort.csort, symbol.encode())
+        term.cterm = self.csolver.declareSygusVar(symbol.encode(), sort.csort)
         return term
 
     def addSygusConstraint(self, Term t):

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f561c101962c0402b163528b7e8f3c0a47ec0871..c0458c4f506bebcd4a40a589fd2f41335e8ef655 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -516,7 +516,7 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
     { PARSER_STATE->checkUserSymbol(name); }
     sortSymbol[t,CHECK_DECLARED]
     {
-      cvc5::Term var = SOLVER->declareSygusVar(t, name);
+      cvc5::Term var = SOLVER->declareSygusVar(name, t);
       PARSER_STATE->defineVar(name, var);
       cmd.reset(new DeclareSygusVarCommand(name, var, t));
     }

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index c728c72e9ca783b1e9732fc329c285badf34766e..6b8d985c9f3f850c7643297f187a1fc071506f78 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -2540,15 +2540,14 @@ TEST_F(TestApiBlackSolver, declareSygusVar)
   Sort intSort = d_solver.getIntegerSort();
   Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
 
-  ASSERT_NO_THROW(d_solver.declareSygusVar(boolSort));
-  ASSERT_NO_THROW(d_solver.declareSygusVar(funSort));
-  ASSERT_NO_THROW(d_solver.declareSygusVar(boolSort, std::string("b")));
-  ASSERT_NO_THROW(d_solver.declareSygusVar(funSort, ""));
-  ASSERT_THROW(d_solver.declareSygusVar(Sort()), CVC5ApiException);
-  ASSERT_THROW(d_solver.declareSygusVar(d_solver.getNullSort(), "a"),
+  ASSERT_NO_THROW(d_solver.declareSygusVar("", boolSort));
+  ASSERT_NO_THROW(d_solver.declareSygusVar("", funSort));
+  ASSERT_NO_THROW(d_solver.declareSygusVar(std::string("b"), boolSort));
+  ASSERT_THROW(d_solver.declareSygusVar("", Sort()), CVC5ApiException);
+  ASSERT_THROW(d_solver.declareSygusVar("a", d_solver.getNullSort()),
                CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.declareSygusVar(boolSort), CVC5ApiException);
+  ASSERT_THROW(slv.declareSygusVar("", boolSort), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkSygusGrammar)

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 7942b75f406501c73c65e1d358bd16369b76066f..41ebf499ae1310f1d3984c413e0362120e3070cf 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -2607,18 +2607,18 @@ class SolverTest
     Sort intSort = d_solver.getIntegerSort();
     Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
 
-    assertDoesNotThrow(() -> d_solver.declareSygusVar(boolSort));
-    assertDoesNotThrow(() -> d_solver.declareSygusVar(funSort));
-    assertDoesNotThrow(() -> d_solver.declareSygusVar(boolSort, ("b")));
-    assertDoesNotThrow(() -> d_solver.declareSygusVar(funSort, ""));
+    assertDoesNotThrow(() -> d_solver.declareSygusVar("", boolSort));
+    assertDoesNotThrow(() -> d_solver.declareSygusVar("", funSort));
+    assertDoesNotThrow(() -> d_solver.declareSygusVar(("b"), boolSort));
 
-    assertThrows(CVC5ApiException.class, () -> d_solver.declareSygusVar(d_solver.getNullSort()));
     assertThrows(
-        CVC5ApiException.class, () -> d_solver.declareSygusVar(d_solver.getNullSort(), "a"));
+        CVC5ApiException.class, () -> d_solver.declareSygusVar("", d_solver.getNullSort()));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.declareSygusVar("a", d_solver.getNullSort()));
 
     Solver slv = new Solver();
     slv.setOption("sygus", "true");
-    assertThrows(CVC5ApiException.class, () -> slv.declareSygusVar(boolSort));
+    assertThrows(CVC5ApiException.class, () -> slv.declareSygusVar("", boolSort));
     slv.close();
   }
 

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 5960c6cfe65434fcbffe369dc1cd1b95a0acd44c..7478f244a210eda981b508f528a0b3c20f193239 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -2514,18 +2514,17 @@ def test_mk_sygus_var(solver):
     intSort = solver.getIntegerSort()
     funSort = solver.mkFunctionSort(intSort, boolSort)
 
-    solver.declareSygusVar(boolSort)
-    solver.declareSygusVar(funSort)
-    solver.declareSygusVar(boolSort, "b")
-    solver.declareSygusVar(funSort, "")
+    solver.declareSygusVar("", boolSort)
+    solver.declareSygusVar("", funSort)
+    solver.declareSygusVar("b", boolSort)
     with pytest.raises(RuntimeError):
-        solver.declareSygusVar(cvc5.Sort(solver))
+        solver.declareSygusVar("", cvc5.Sort(solver))
     with pytest.raises(RuntimeError):
-        solver.declareSygusVar(solver.getNullSort(), "a")
+        solver.declareSygusVar("a", solver.getNullSort())
     slv = cvc5.Solver()
     solver.setOption("sygus", "true")
     with pytest.raises(RuntimeError):
-        slv.declareSygusVar(boolSort)
+        slv.declareSygusVar("", boolSort)
 
 
 def test_synth_fun(solver):