diff options
| -rw-r--r-- | examples/api/bitvectors-new.cpp | 10 | ||||
| -rw-r--r-- | examples/api/bitvectors_and_arrays-new.cpp | 2 | ||||
| -rw-r--r-- | examples/api/combination-new.cpp | 8 | ||||
| -rw-r--r-- | examples/api/datatypes-new.cpp | 2 | ||||
| -rw-r--r-- | examples/api/extract-new.cpp | 2 | ||||
| -rw-r--r-- | examples/api/linear_arith-new.cpp | 4 | ||||
| -rw-r--r-- | examples/api/sets-new.cpp | 10 | ||||
| -rw-r--r-- | examples/api/strings-new.cpp | 10 | ||||
| -rw-r--r-- | src/api/cvc4cpp.cpp | 145 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 36 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 20 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
| -rw-r--r-- | test/unit/api/solver_black.h | 117 |
13 files changed, 168 insertions, 202 deletions
diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp index 6aea56163..d0c26f134 100644 --- a/examples/api/bitvectors-new.cpp +++ b/examples/api/bitvectors-new.cpp @@ -50,9 +50,9 @@ int main() Sort bitvector32 = slv.mkBitVectorSort(32); // Variables - Term x = slv.mkVar(bitvector32, "x"); - Term a = slv.mkVar(bitvector32, "a"); - Term b = slv.mkVar(bitvector32, "b"); + Term x = slv.mkConst(bitvector32, "x"); + Term a = slv.mkConst(bitvector32, "a"); + Term b = slv.mkConst(bitvector32, "b"); // First encode the assumption that x must be equal to a or b Term x_eq_a = slv.mkTerm(EQUAL, x, a); @@ -63,9 +63,9 @@ int main() slv.assertFormula(assumption); // Introduce a new variable for the new value of x after assignment. - Term new_x = slv.mkVar(bitvector32, "new_x"); // x after executing code (0) + Term new_x = slv.mkConst(bitvector32, "new_x"); // x after executing code (0) Term new_x_ = - slv.mkVar(bitvector32, "new_x_"); // x after executing code (1) or (2) + slv.mkConst(bitvector32, "new_x_"); // x after executing code (1) or (2) // Encoding code (0) // new_x = x == a ? b : a; diff --git a/examples/api/bitvectors_and_arrays-new.cpp b/examples/api/bitvectors_and_arrays-new.cpp index f0883d634..955a83cff 100644 --- a/examples/api/bitvectors_and_arrays-new.cpp +++ b/examples/api/bitvectors_and_arrays-new.cpp @@ -53,7 +53,7 @@ int main() Sort arraySort = slv.mkArraySort(indexSort, elementSort); // Variables - Term current_array = slv.mkVar(arraySort, "current_array"); + Term current_array = slv.mkConst(arraySort, "current_array"); // Making a bit-vector constant Term zero = slv.mkBitVector(index_size, 0u); diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp index a3ff4421f..e78e8919f 100644 --- a/examples/api/combination-new.cpp +++ b/examples/api/combination-new.cpp @@ -51,12 +51,12 @@ int main() Sort intPred = slv.mkFunctionSort(integer, boolean); // Variables - Term x = slv.mkVar(u, "x"); - Term y = slv.mkVar(u, "y"); + Term x = slv.mkConst(u, "x"); + Term y = slv.mkConst(u, "y"); // Functions - Term f = slv.mkVar(uToInt, "f"); - Term p = slv.mkVar(intPred, "p"); + Term f = slv.mkConst(uToInt, "f"); + Term p = slv.mkConst(intPred, "p"); // Constants Term zero = slv.mkReal(0); diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index c499fa111..08918fc87 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -116,7 +116,7 @@ void test(Solver& slv, Sort& consListSort) } } - Term a = slv.declareConst("a", paramConsIntListSort); + Term a = slv.mkConst(paramConsIntListSort, "a"); std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; Term head_a = slv.mkTerm( diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp index aad9e0fb5..cb7d96fa5 100644 --- a/examples/api/extract-new.cpp +++ b/examples/api/extract-new.cpp @@ -29,7 +29,7 @@ int main() Sort bitvector32 = slv.mkBitVectorSort(32); - Term x = slv.mkVar(bitvector32, "a"); + Term x = slv.mkConst(bitvector32, "a"); OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x); diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp index aae2fa67e..2edcaf71e 100644 --- a/examples/api/linear_arith-new.cpp +++ b/examples/api/linear_arith-new.cpp @@ -36,8 +36,8 @@ int main() Sort integer = slv.getIntegerSort(); // Variables - Term x = slv.mkVar(integer, "x"); - Term y = slv.mkVar(real, "y"); + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(real, "y"); // Constants Term three = slv.mkReal(3); diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp index 6c0352302..60df7a82f 100644 --- a/examples/api/sets-new.cpp +++ b/examples/api/sets-new.cpp @@ -40,9 +40,9 @@ int main() // Verify union distributions over intersection // (A union B) intersection C = (A intersection C) union (B intersection C) { - Term A = slv.mkVar(set, "A"); - Term B = slv.mkVar(set, "B"); - Term C = slv.mkVar(set, "C"); + Term A = slv.mkConst(set, "A"); + Term B = slv.mkConst(set, "B"); + Term C = slv.mkConst(set, "C"); Term unionAB = slv.mkTerm(UNION, A, B); Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); @@ -59,7 +59,7 @@ int main() // Verify emptset is a subset of any set { - Term A = slv.mkVar(set, "A"); + Term A = slv.mkConst(set, "A"); Term emptyset = slv.mkEmptySet(set); Term theorem = slv.mkTerm(SUBSET, emptyset, A); @@ -81,7 +81,7 @@ int main() Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); - Term x = slv.mkVar(integer, "x"); + Term x = slv.mkConst(integer, "x"); Term e = slv.mkTerm(MEMBER, x, intersection); diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp index a9c6dd491..42630dc0e 100644 --- a/examples/api/strings-new.cpp +++ b/examples/api/strings-new.cpp @@ -43,9 +43,9 @@ int main() Term ab = slv.mkString(str_ab); Term abc = slv.mkString("abc"); // String variables - Term x = slv.mkVar(string, "x"); - Term y = slv.mkVar(string, "y"); - Term z = slv.mkVar(string, "z"); + Term x = slv.mkConst(string, "x"); + Term y = slv.mkConst(string, "y"); + Term z = slv.mkConst(string, "z"); // String concatenation: x.ab.y Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y); @@ -70,8 +70,8 @@ int main() slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h"))); // String variables - Term s1 = slv.mkVar(string, "s1"); - Term s2 = slv.mkVar(string, "s2"); + Term s1 = slv.mkConst(string, "s1"); + Term s2 = slv.mkConst(string, "s2"); // String concatenation: s1.s2 Term s = slv.mkTerm(STRING_CONCAT, s1, s2); diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 86072d601..4cd9f4923 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -56,8 +56,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {APPLY, CVC4::Kind::APPLY}, {EQUAL, CVC4::Kind::EQUAL}, {DISTINCT, CVC4::Kind::DISTINCT}, - {VARIABLE, CVC4::Kind::VARIABLE}, - {BOUND_VARIABLE, CVC4::Kind::BOUND_VARIABLE}, + {CONSTANT, CVC4::Kind::VARIABLE}, + {VARIABLE, CVC4::Kind::BOUND_VARIABLE}, {LAMBDA, CVC4::Kind::LAMBDA}, {CHOICE, CVC4::Kind::CHOICE}, {CHAIN, CVC4::Kind::CHAIN}, @@ -304,8 +304,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::APPLY, APPLY}, {CVC4::Kind::EQUAL, EQUAL}, {CVC4::Kind::DISTINCT, DISTINCT}, - {CVC4::Kind::VARIABLE, VARIABLE}, - {CVC4::Kind::BOUND_VARIABLE, BOUND_VARIABLE}, + {CVC4::Kind::VARIABLE, CONSTANT}, + {CVC4::Kind::BOUND_VARIABLE, VARIABLE}, {CVC4::Kind::LAMBDA, LAMBDA}, {CVC4::Kind::CHOICE, CHOICE}, {CVC4::Kind::CHAIN, CHAIN}, @@ -1970,7 +1970,7 @@ Term Solver::mkPi() const } template <typename T> -Term Solver::mkConstHelper(T t) const +Term Solver::mkValHelper(T t) const { try { @@ -1997,7 +1997,7 @@ Term Solver::mkRealFromStrHelper(std::string s) const CVC4::Rational r = s.find('/') != std::string::npos ? CVC4::Rational(s) : CVC4::Rational::fromDecimal(s); - return mkConstHelper<CVC4::Rational>(r); + return mkValHelper<CVC4::Rational>(r); } catch (const std::invalid_argument& e) { @@ -2020,7 +2020,7 @@ Term Solver::mkReal(int32_t val) const { try { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(val)); + return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); } catch (const std::invalid_argument& e) { @@ -2032,7 +2032,7 @@ Term Solver::mkReal(int64_t val) const { try { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(val)); + return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); } catch (const std::invalid_argument& e) { @@ -2044,7 +2044,7 @@ Term Solver::mkReal(uint32_t val) const { try { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(val)); + return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); } catch (const std::invalid_argument& e) { @@ -2056,7 +2056,7 @@ Term Solver::mkReal(uint64_t val) const { try { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(val)); + return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); } catch (const std::invalid_argument& e) { @@ -2068,7 +2068,7 @@ Term Solver::mkReal(int32_t num, int32_t den) const { try { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den)); + return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); } catch (const std::invalid_argument& e) { @@ -2080,7 +2080,7 @@ Term Solver::mkReal(int64_t num, int64_t den) const { try { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den)); + return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); } catch (const std::invalid_argument& e) { @@ -2092,7 +2092,7 @@ Term Solver::mkReal(uint32_t num, uint32_t den) const { try { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den)); + return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); } catch (const std::invalid_argument& e) { @@ -2104,7 +2104,7 @@ Term Solver::mkReal(uint64_t num, uint64_t den) const { try { - return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den)); + return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); } catch (const std::invalid_argument& e) { @@ -2146,7 +2146,7 @@ Term Solver::mkEmptySet(Sort s) const { CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s) << "null sort or set sort"; - return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type)); + return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type)); } Term Solver::mkSepNil(Sort sort) const @@ -2166,22 +2166,22 @@ Term Solver::mkSepNil(Sort sort) const Term Solver::mkString(const char* s, bool useEscSequences) const { - return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences)); + return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences)); } Term Solver::mkString(const std::string& s, bool useEscSequences) const { - return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences)); + return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences)); } Term Solver::mkString(const unsigned char c) const { - return mkConstHelper<CVC4::String>(CVC4::String(std::string(1, c))); + return mkValHelper<CVC4::String>(CVC4::String(std::string(1, c))); } Term Solver::mkString(const std::vector<unsigned>& s) const { - return mkConstHelper<CVC4::String>(CVC4::String(s)); + return mkValHelper<CVC4::String>(CVC4::String(s)); } Term Solver::mkUniverseSet(Sort sort) const @@ -2207,7 +2207,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0"; try { - return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); + return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); } catch (const std::invalid_argument& e) { @@ -2228,7 +2228,7 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const << "base 2, 10, or 16"; try { - return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base)); + return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base)); } catch (const std::invalid_argument& e) { @@ -2249,7 +2249,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size, CVC4_API_CHECK(val.modByPow2(size) == val) << "Overflow in bitvector construction (specified bitvector size " << size << " too small to hold value " << s << ")"; - return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); + return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); } catch (const std::invalid_argument& e) { @@ -2283,7 +2283,7 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const { CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - return mkConstHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC4::FloatingPoint>( FloatingPoint::makeInf(FloatingPointSize(exp, sig), false)); } @@ -2291,7 +2291,7 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const { CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - return mkConstHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC4::FloatingPoint>( FloatingPoint::makeInf(FloatingPointSize(exp, sig), true)); } @@ -2299,7 +2299,7 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const { CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - return mkConstHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC4::FloatingPoint>( FloatingPoint::makeNaN(FloatingPointSize(exp, sig))); } @@ -2307,7 +2307,7 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const { CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - return mkConstHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC4::FloatingPoint>( FloatingPoint::makeZero(FloatingPointSize(exp, sig), false)); } @@ -2315,19 +2315,19 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const { CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - return mkConstHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC4::FloatingPoint>( FloatingPoint::makeZero(FloatingPointSize(exp, sig), true)); } Term Solver::mkRoundingMode(RoundingMode rm) const { - return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm)); + return mkValHelper<CVC4::RoundingMode>(s_rmodes.at(rm)); } Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const { CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; - return mkConstHelper<CVC4::UninterpretedConstant>( + return mkValHelper<CVC4::UninterpretedConstant>( CVC4::UninterpretedConstant(*sort.d_type, index)); } @@ -2385,14 +2385,14 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const CVC4_API_ARG_CHECK_EXPECTED( val.getSort().isBitVector() && val.d_expr->isConst(), val) << "bit-vector constant"; - return mkConstHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC4::FloatingPoint>( CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>())); } -/* Create variables */ +/* Create constants */ /* -------------------------------------------------------------------------- */ -Term Solver::mkVar(Sort sort, const std::string& symbol) const +Term Solver::mkConst(Sort sort, const std::string& symbol) const { try { @@ -2408,7 +2408,10 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const } } -Term Solver::mkBoundVar(Sort sort, const std::string& symbol) const +/* Create variables */ +/* -------------------------------------------------------------------------- */ + +Term Solver::mkVar(Sort sort, const std::string& symbol) const { try { @@ -2436,8 +2439,9 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR, kind) << "Only operator-style terms are created with mkTerm(), " - "to create variables and constants see mkVar(), mkBoundVar(), " - "and mkConst()."; + "to create variables, constants and values see mkVar(), mkConst() " + "and the respective theory-specific functions to create values, " + "e.g., mkBitVector()."; CVC4_API_KIND_CHECK_EXPECTED( nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind) << "Terms with kind " << kindToString(kind) << " must have at least " @@ -2729,15 +2733,14 @@ std::vector<Expr> Solver::termVectorToExprs( OpTerm Solver::mkOpTerm(Kind kind, Kind k) { CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP"; - return *mkConstHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get(); + return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get(); } OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) { CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind) << "RECORD_UPDATE_OP"; - return *mkConstHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)) - .d_expr.get(); + return *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get(); } OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) @@ -2747,59 +2750,59 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) switch (kind) { case DIVISIBLE_OP: - res = *mkConstHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get(); + res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get(); break; case BITVECTOR_REPEAT_OP: - res = *mkConstHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg)) + res = *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg)) .d_expr.get(); break; case BITVECTOR_ZERO_EXTEND_OP: - res = *mkConstHelper<CVC4::BitVectorZeroExtend>( + res = *mkValHelper<CVC4::BitVectorZeroExtend>( CVC4::BitVectorZeroExtend(arg)) .d_expr.get(); break; case BITVECTOR_SIGN_EXTEND_OP: - res = *mkConstHelper<CVC4::BitVectorSignExtend>( + res = *mkValHelper<CVC4::BitVectorSignExtend>( CVC4::BitVectorSignExtend(arg)) .d_expr.get(); break; case BITVECTOR_ROTATE_LEFT_OP: - res = *mkConstHelper<CVC4::BitVectorRotateLeft>( + res = *mkValHelper<CVC4::BitVectorRotateLeft>( CVC4::BitVectorRotateLeft(arg)) .d_expr.get(); break; case BITVECTOR_ROTATE_RIGHT_OP: - res = *mkConstHelper<CVC4::BitVectorRotateRight>( + res = *mkValHelper<CVC4::BitVectorRotateRight>( CVC4::BitVectorRotateRight(arg)) .d_expr.get(); break; case INT_TO_BITVECTOR_OP: - res = *mkConstHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)) + res = *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)) .d_expr.get(); break; case FLOATINGPOINT_TO_UBV_OP: - res = *mkConstHelper<CVC4::FloatingPointToUBV>( - CVC4::FloatingPointToUBV(arg)) - .d_expr.get(); + res = + *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg)) + .d_expr.get(); break; case FLOATINGPOINT_TO_UBV_TOTAL_OP: - res = *mkConstHelper<CVC4::FloatingPointToUBVTotal>( + res = *mkValHelper<CVC4::FloatingPointToUBVTotal>( CVC4::FloatingPointToUBVTotal(arg)) .d_expr.get(); break; case FLOATINGPOINT_TO_SBV_OP: - res = *mkConstHelper<CVC4::FloatingPointToSBV>( - CVC4::FloatingPointToSBV(arg)) - .d_expr.get(); + res = + *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg)) + .d_expr.get(); break; case FLOATINGPOINT_TO_SBV_TOTAL_OP: - res = *mkConstHelper<CVC4::FloatingPointToSBVTotal>( + res = *mkValHelper<CVC4::FloatingPointToSBVTotal>( CVC4::FloatingPointToSBVTotal(arg)) .d_expr.get(); break; case TUPLE_UPDATE_OP: - res = *mkConstHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)) - .d_expr.get(); + res = + *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get(); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -2816,37 +2819,37 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) switch (kind) { case BITVECTOR_EXTRACT_OP: - res = *mkConstHelper<CVC4::BitVectorExtract>( + res = *mkValHelper<CVC4::BitVectorExtract>( CVC4::BitVectorExtract(arg1, arg2)) .d_expr.get(); break; case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: - res = *mkConstHelper<CVC4::FloatingPointToFPIEEEBitVector>( + res = *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>( CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) .d_expr.get(); break; case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: - res = *mkConstHelper<CVC4::FloatingPointToFPFloatingPoint>( + res = *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>( CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) .d_expr.get(); break; case FLOATINGPOINT_TO_FP_REAL_OP: - res = *mkConstHelper<CVC4::FloatingPointToFPReal>( + res = *mkValHelper<CVC4::FloatingPointToFPReal>( CVC4::FloatingPointToFPReal(arg1, arg2)) .d_expr.get(); break; case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: - res = *mkConstHelper<CVC4::FloatingPointToFPSignedBitVector>( + res = *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>( CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) .d_expr.get(); break; case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: - res = *mkConstHelper<CVC4::FloatingPointToFPUnsignedBitVector>( + res = *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>( CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) .d_expr.get(); break; case FLOATINGPOINT_TO_FP_GENERIC_OP: - res = *mkConstHelper<CVC4::FloatingPointToFPGeneric>( + res = *mkValHelper<CVC4::FloatingPointToFPGeneric>( CVC4::FloatingPointToFPGeneric(arg1, arg2)) .d_expr.get(); break; @@ -2940,24 +2943,6 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const } /** - * ( declare-const <symbol> <sort> ) - */ -Term Solver::declareConst(const std::string& symbol, Sort sort) const -{ - try - { - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; - Term res = d_exprMgr->mkVar(symbol, *sort.d_type); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } -} - -/** * ( declare-datatype <symbol> <datatype_decl> ) */ Sort Solver::declareDatatype( diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 203586066..c13c7919e 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2166,20 +2166,23 @@ class CVC4_PUBLIC Solver /* .................................................................... */ /** - * Create variable. - * @param sort the sort of the variable - * @param symbol the name of the variable - * @return the variable + * Create (first-order) constant (0-arity function symbol). + * SMT-LIB: ( declare-const <symbol> <sort> ) + * SMT-LIB: ( declare-fun <symbol> ( ) <sort> ) + * + * @param sort the sort of the constant + * @param symbol the name of the constant + * @return the first-order constant */ - Term mkVar(Sort sort, const std::string& symbol = std::string()) const; + Term mkConst(Sort sort, const std::string& symbol = std::string()) const; /** - * Create bound variable. + * Create (bound) variable. * @param sort the sort of the variable * @param symbol the name of the variable * @return the variable */ - Term mkBoundVar(Sort sort, const std::string& symbol = std::string()) const; + Term mkVar(Sort sort, const std::string& symbol = std::string()) const; /* .................................................................... */ /* Formula Handling */ @@ -2246,17 +2249,6 @@ class CVC4_PUBLIC Solver Result checkValidAssuming(const std::vector<Term>& assumptions) const; /** - * Declare first-order constant (0-arity function symbol). - * SMT-LIB: ( declare-const <symbol> <sort> ) - * SMT-LIB: ( declare-fun <symbol> ( ) <sort> ) - * This command corresponds to mkVar(). - * @param symbol the name of the first-order constant - * @param sort the sort of the first-order constant - * @return the first-order constant - */ - Term declareConst(const std::string& symbol, Sort sort) const; - - /** * Create datatype sort. * SMT-LIB: ( declare-datatype <symbol> <datatype_decl> ) * @param symbol the name of the datatype sort @@ -2303,7 +2295,7 @@ class CVC4_PUBLIC Solver /** * Define n-ary function. * SMT-LIB: ( define-fun <function_def> ) - * Create parameter 'fun' with mkVar(). + * Create parameter 'fun' with mkConst(). * @param fun the sorted function * @param bound_vars the parameters to this function * @param term the function body @@ -2330,7 +2322,7 @@ class CVC4_PUBLIC Solver /** * Define recursive function. * SMT-LIB: ( define-fun-rec <function_def> ) - * Create parameter 'fun' with mkVar(). + * Create parameter 'fun' with mkConst(). * @param fun the sorted function * @param bound_vars the parameters to this function * @param term the function body @@ -2343,7 +2335,7 @@ class CVC4_PUBLIC Solver /** * Define recursive functions. * SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) - * Create elements of parameter 'funs' with mkVar(). + * Create elements of parameter 'funs' with mkConst(). * @param funs the sorted functions * @param bound_vars the list of parameters to the functions * @param term the list of function bodies of the functions @@ -2506,7 +2498,7 @@ class CVC4_PUBLIC Solver void checkMkTerm(Kind kind, uint32_t nchildren) const; /* Helper for mk-functions that call d_exprMgr->mkConst(). */ template <typename T> - Term mkConstHelper(T t) const; + Term mkValHelper(T t) const; /* Helper for mkReal functions that take a string as argument. */ Term mkRealFromStrHelper(std::string s) const; /* Helper for mkBitVector functions that take a string as argument. */ diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 3aba6cebb..d4f6880f9 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -123,25 +123,25 @@ enum CVC4_PUBLIC Kind : int32_t */ DISTINCT, /** - * Variable. + * First-order constant. * Not permitted in bindings (forall, exists, ...). * Parameters: - * See mkVar(). + * See mkConst(). * Create with: - * mkVar(const std::string& symbol, Sort sort) - * mkVar(Sort sort) + * mkConst(const std::string& symbol, Sort sort) + * mkConst(Sort sort) */ - VARIABLE, + CONSTANT, /** - * Bound variable. + * (Bound) variable. * Permitted in bindings and in the lambda and quantifier bodies only. * Parameters: - * See mkBoundVar(). + * See mkVar(). * Create with: - * mkBoundVar(const std::string& symbol, Sort sort) - * mkBoundVar(Sort sort) + * mkVar(const std::string& symbol, Sort sort) + * mkVar(Sort sort) */ - BOUND_VARIABLE, + VARIABLE, #if 0 /* Skolem variable (internal only) */ SKOLEM, diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 00f2e944d..75df38637 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2307,8 +2307,8 @@ termAtomic[CVC4::api::Term& atomTerm] sortSymbol[type,CHECK_DECLARED] sortSymbol[type2,CHECK_DECLARED] { - api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1"); - api::Term v2 = SOLVER->mkVar(api::Sort(type2), "_emp2"); + api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1"); + api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2"); atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2); } diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index a5d927812..289fc26f0 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -76,7 +76,6 @@ class SolverBlack : public CxxTest::TestSuite void testMkUniverseSet(); void testMkVar(); - void testDeclareConst(); void testDeclareDatatype(); void testDeclareFun(); void testDeclareSort(); @@ -295,12 +294,12 @@ void SolverBlack::testMkBoundVar() Sort boolSort = d_solver->getBooleanSort(); Sort intSort = d_solver->getIntegerSort(); Sort funSort = d_solver->mkFunctionSort(intSort, boolSort); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(boolSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(funSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(boolSort, std::string("b"))); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(funSort, "")); - TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort(), "a"), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort, std::string("b"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort, "")); + TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkVar(Sort(), "a"), CVC4ApiException&); } void SolverBlack::testMkBoolean() @@ -512,7 +511,7 @@ void SolverBlack::testMkReal() void SolverBlack::testMkRegexpEmpty() { Sort strSort = d_solver->getStringSort(); - Term s = d_solver->mkVar(strSort, "s"); + Term s = d_solver->mkConst(strSort, "s"); TS_ASSERT_THROWS_NOTHING( d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpEmpty())); } @@ -520,7 +519,7 @@ void SolverBlack::testMkRegexpEmpty() void SolverBlack::testMkRegexpSigma() { Sort strSort = d_solver->getStringSort(); - Term s = d_solver->mkVar(strSort, "s"); + Term s = d_solver->mkConst(strSort, "s"); TS_ASSERT_THROWS_NOTHING( d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpSigma())); } @@ -544,8 +543,8 @@ void SolverBlack::testMkString() void SolverBlack::testMkTerm() { Sort bv32 = d_solver->mkBitVectorSort(32); - Term a = d_solver->mkVar(bv32, "a"); - Term b = d_solver->mkVar(bv32, "b"); + Term a = d_solver->mkConst(bv32, "a"); + Term b = d_solver->mkConst(bv32, "b"); std::vector<Term> v1 = {a, b}; std::vector<Term> v2 = {a, Term()}; std::vector<Term> v3 = {a, d_solver->mkTrue()}; @@ -597,8 +596,8 @@ void SolverBlack::testMkTerm() void SolverBlack::testMkTermFromOpTerm() { Sort bv32 = d_solver->mkBitVectorSort(32); - Term a = d_solver->mkVar(bv32, "a"); - Term b = d_solver->mkVar(bv32, "b"); + Term a = d_solver->mkConst(bv32, "a"); + Term b = d_solver->mkConst(bv32, "b"); std::vector<Term> v1 = {d_solver->mkReal(1), d_solver->mkReal(2)}; std::vector<Term> v2 = {d_solver->mkReal(1), Term()}; std::vector<Term> v3 = {}; @@ -620,7 +619,7 @@ void SolverBlack::testMkTermFromOpTerm() Sort listSort = d_solver->mkDatatypeSort(listDecl); Sort intListSort = listSort.instantiate(std::vector<Sort>{d_solver->getIntegerSort()}); - Term c = d_solver->declareConst("c", intListSort); + Term c = d_solver->mkConst(intListSort, "c"); Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms OpTerm consTerm1 = list.getConstructorTerm("cons"); @@ -733,24 +732,14 @@ void SolverBlack::testMkVar() Sort boolSort = d_solver->getBooleanSort(); Sort intSort = d_solver->getIntegerSort(); Sort funSort = d_solver->mkFunctionSort(intSort, boolSort); - TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort, std::string("b"))); - TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort, "")); - TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkVar(Sort(), "a"), CVC4ApiException&); -} - -void SolverBlack::testDeclareConst() -{ - Sort boolSort = d_solver->getBooleanSort(); - Sort intSort = d_solver->getIntegerSort(); - Sort funSort = d_solver->mkFunctionSort(intSort, boolSort); - TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("b"), boolSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("i"), intSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("f", funSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("", funSort)); - TS_ASSERT_THROWS(d_solver->declareConst("a", Sort()), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(boolSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(boolSort, std::string("b"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(intSort, std::string("i"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, "f")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, "")); + TS_ASSERT_THROWS(d_solver->mkConst(Sort()), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkConst(Sort(), "a"), CVC4ApiException&); } void SolverBlack::testDeclareDatatype() @@ -797,16 +786,16 @@ void SolverBlack::testDefineFun() Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"), d_solver->getIntegerSort()); - Term b1 = d_solver->mkBoundVar(bvSort, "b1"); - Term b11 = d_solver->mkBoundVar(bvSort, "b1"); - Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2"); - Term b3 = d_solver->mkBoundVar(funSort2, "b3"); - Term v1 = d_solver->mkBoundVar(bvSort, "v1"); - Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2"); - Term v3 = d_solver->mkVar(funSort2, "v3"); - Term f1 = d_solver->declareConst("f1", funSort1); - Term f2 = d_solver->declareConst("f2", funSort2); - Term f3 = d_solver->declareConst("f3", bvSort); + Term b1 = d_solver->mkVar(bvSort, "b1"); + Term b11 = d_solver->mkVar(bvSort, "b1"); + Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2"); + Term b3 = d_solver->mkVar(funSort2, "b3"); + Term v1 = d_solver->mkVar(bvSort, "v1"); + Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2"); + Term v3 = d_solver->mkConst(funSort2, "v3"); + Term f1 = d_solver->mkConst(funSort1, "f1"); + Term f2 = d_solver->mkConst(funSort2, "f2"); + Term f3 = d_solver->mkConst(bvSort, "f3"); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("f", {}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("ff", {b1, b2}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun(f1, {b1, b11}, v1)); @@ -829,16 +818,16 @@ void SolverBlack::testDefineFunRec() Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"), d_solver->getIntegerSort()); - Term b1 = d_solver->mkBoundVar(bvSort, "b1"); - Term b11 = d_solver->mkBoundVar(bvSort, "b1"); - Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2"); - Term b3 = d_solver->mkBoundVar(funSort2, "b3"); - Term v1 = d_solver->mkBoundVar(bvSort, "v1"); - Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2"); - Term v3 = d_solver->mkVar(funSort2, "v3"); - Term f1 = d_solver->declareConst("f1", funSort1); - Term f2 = d_solver->declareConst("f2", funSort2); - Term f3 = d_solver->declareConst("f3", bvSort); + Term b1 = d_solver->mkVar(bvSort, "b1"); + Term b11 = d_solver->mkVar(bvSort, "b1"); + Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2"); + Term b3 = d_solver->mkVar(funSort2, "b3"); + Term v1 = d_solver->mkVar(bvSort, "v1"); + Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2"); + Term v3 = d_solver->mkConst(funSort2, "v3"); + Term f1 = d_solver->mkConst(funSort1, "f1"); + Term f2 = d_solver->mkConst(funSort2, "f2"); + Term f3 = d_solver->mkConst(bvSort, "f3"); TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("f", {}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("ff", {b1, b2}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec(f1, {b1, b11}, v1)); @@ -863,18 +852,18 @@ void SolverBlack::testDefineFunsRec() Sort bvSort = d_solver->mkBitVectorSort(32); Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort()); - Term b1 = d_solver->mkBoundVar(bvSort, "b1"); - Term b11 = d_solver->mkBoundVar(bvSort, "b1"); - Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2"); - Term b3 = d_solver->mkBoundVar(funSort2, "b3"); - Term b4 = d_solver->mkBoundVar(uSort, "b4"); - Term v1 = d_solver->mkBoundVar(bvSort, "v1"); - Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2"); - Term v3 = d_solver->mkVar(funSort2, "v3"); - Term v4 = d_solver->mkVar(uSort, "v4"); - Term f1 = d_solver->declareConst("f1", funSort1); - Term f2 = d_solver->declareConst("f2", funSort2); - Term f3 = d_solver->declareConst("f3", bvSort); + Term b1 = d_solver->mkVar(bvSort, "b1"); + Term b11 = d_solver->mkVar(bvSort, "b1"); + Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2"); + Term b3 = d_solver->mkVar(funSort2, "b3"); + Term b4 = d_solver->mkVar(uSort, "b4"); + Term v1 = d_solver->mkVar(bvSort, "v1"); + Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2"); + Term v3 = d_solver->mkConst(funSort2, "v3"); + Term v4 = d_solver->mkConst(uSort, "v4"); + Term f1 = d_solver->mkConst(funSort1, "f1"); + Term f2 = d_solver->mkConst(funSort2, "f2"); + Term f3 = d_solver->mkConst(bvSort, "f3"); TS_ASSERT_THROWS_NOTHING( d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); TS_ASSERT_THROWS( |