From 8d7787f310e385056badf3580914195372ba87e4 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 31 Mar 2022 18:32:44 -0700 Subject: [PATCH] api: Swap arguments of declareSygusVar. (#8499) Make it consistent with other declare*/define* functions. --- examples/api/cpp/sygus-fun.cpp | 4 ++-- examples/api/cpp/sygus-grammar.cpp | 2 +- examples/api/java/SygusFun.java | 4 ++-- examples/api/java/SygusGrammar.java | 2 +- examples/api/python/sygus-fun.py | 4 ++-- examples/api/python/sygus-grammar.py | 2 +- src/api/cpp/cvc5.cpp | 2 +- src/api/cpp/cvc5.h | 3 +-- src/api/java/io/github/cvc5/Solver.java | 15 +++------------ src/api/java/jni/solver.cpp | 6 +++--- src/api/python/cvc5.pxd | 3 +-- src/api/python/cvc5.pxi | 4 ++-- src/parser/smt2/Smt2.g | 2 +- test/unit/api/cpp/solver_black.cpp | 13 ++++++------- test/unit/api/java/SolverTest.java | 14 +++++++------- test/unit/api/python/test_solver.py | 13 ++++++------- 16 files changed, 40 insertions(+), 53 deletions(-) diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp index 864ab6a11..15a53c36e 100644 --- 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 cca30d301..a69382e12 100644 --- 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 3ce5a5e45..4f0626748 100644 --- 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 127da1c5f..c97fb23e0 100644 --- 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 94cd26d6b..990307041 100644 --- 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 1613f6595..618bd2069 100644 --- 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 3cc67a0c7..7534eceaa 100644 --- 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 96fe3775f..2358ee879 100644 --- 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 885ccc359..384824e5d 100644 --- 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 b83560e9f..f21434dd2 100644 --- 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(pointer); Sort* sort = reinterpret_cast(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(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 05e06b695..929c03900 100644 --- 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 a5c3c3f7e..eb0e749bd 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1550,7 +1550,7 @@ cdef class Solver: grammar.cgrammar = self.csolver.mkSygusGrammar( bvc, 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 f561c1019..c0458c4f5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -516,7 +516,7 @@ sygusCommand returns [std::unique_ptr 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 c728c72e9..6b8d985c9 100644 --- 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 7942b75f4..41ebf499a 100644 --- 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 5960c6cfe..7478f244a 100644 --- 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): -- 2.30.2