diff options
| -rw-r--r-- | examples/api/bitvectors-new.cpp | 4 | ||||
| -rw-r--r-- | examples/api/datatypes-new.cpp | 14 | ||||
| -rw-r--r-- | examples/api/extract-new.cpp | 16 | ||||
| -rw-r--r-- | src/api/cvc4cpp.cpp | 1015 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 404 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 371 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 51 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.h | 10 | ||||
| -rw-r--r-- | src/preprocessing/passes/ackermann.cpp | 4 | ||||
| -rw-r--r-- | src/preprocessing/passes/ackermann.h | 4 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 | ||||
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 40 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/printer/symbol_starting_w_digit.smt2 | 12 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue3481.smt2 | 495 | ||||
| -rw-r--r-- | test/unit/api/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/unit/api/op_black.h (renamed from test/unit/api/opterm_black.h) | 108 | ||||
| -rw-r--r-- | test/unit/api/solver_black.h | 234 | ||||
| -rw-r--r-- | test/unit/api/term_black.h | 6 |
21 files changed, 1760 insertions, 1049 deletions
diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp index 58912a1bb..4578da733 100644 --- a/examples/api/bitvectors-new.cpp +++ b/examples/api/bitvectors-new.cpp @@ -114,8 +114,8 @@ int main() cout << " CVC4: " << slv.checkValidAssuming(v) << endl; // Assert that a is odd - OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); - Term lsb_of_a = slv.mkTerm(BITVECTOR_EXTRACT, extract_op, a); + Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); + Term lsb_of_a = slv.mkTerm(extract_op, a); cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl; Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u)); cout << "Assert " << a_odd << endl; diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index efbd33645..9ff05ac0d 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -36,11 +36,9 @@ void test(Solver& slv, Sort& consListSort) // which is equivalent to consList["cons"].getConstructor(). Note that // "nil" is a constructor too, so it needs to be applied with // APPLY_CONSTRUCTOR, even though it has no arguments. - Term t = slv.mkTerm( - APPLY_CONSTRUCTOR, - consList.getConstructorTerm("cons"), - slv.mkReal(0), - slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + Term t = slv.mkTerm(consList.getConstructorTerm("cons"), + slv.mkReal(0), + slv.mkTerm(consList.getConstructorTerm("nil"))); std::cout << "t is " << t << std::endl << "sort of cons is " @@ -53,8 +51,7 @@ void test(Solver& slv, Sort& consListSort) // Here we first get the DatatypeConstructor for cons (with // consList["cons"]) in order to get the "head" selector symbol // to apply. - Term t2 = - slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); + Term t2 = slv.mkTerm(consList["cons"].getSelectorTerm("head"), t); std::cout << "t2 is " << t2 << std::endl << "simplify(t2) is " << slv.simplify(t2) << std::endl @@ -118,8 +115,7 @@ void test(Solver& slv, Sort& consListSort) Term a = slv.mkConst(paramConsIntListSort, "a"); std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; - Term head_a = slv.mkTerm( - APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a); + Term head_a = slv.mkTerm(paramConsList["cons"].getSelectorTerm("head"), a); std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl << "sort of cons is " diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp index 0cb885b2c..0f0f8243a 100644 --- a/examples/api/extract-new.cpp +++ b/examples/api/extract-new.cpp @@ -30,17 +30,17 @@ int main() 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); + Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, 31, 1); + Term x_31_1 = slv.mkTerm(ext_31_1, x); - OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0); - Term x_30_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_30_0, x); + Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, 30, 0); + Term x_30_0 = slv.mkTerm(ext_30_0, x); - OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31); - Term x_31_31 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_31, x); + Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, 31, 31); + Term x_31_31 = slv.mkTerm(ext_31_31, x); - OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); - Term x_0_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_0_0, x); + Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); + Term x_0_0 = slv.mkTerm(ext_0_0, x); Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0); cout << " Asserting: " << eq << endl; diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 4bb772e9d..651ed60e4 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -77,7 +77,6 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {LAMBDA, CVC4::Kind::LAMBDA}, {CHOICE, CVC4::Kind::CHOICE}, {CHAIN, CVC4::Kind::CHAIN}, - {CHAIN_OP, CVC4::Kind::CHAIN_OP}, /* Boolean ------------------------------------------------------------- */ {CONST_BOOLEAN, CVC4::Kind::CONST_BOOLEAN}, {NOT, CVC4::Kind::NOT}, @@ -118,7 +117,6 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {ARCSECANT, CVC4::Kind::ARCSECANT}, {ARCCOTANGENT, CVC4::Kind::ARCCOTANGENT}, {SQRT, CVC4::Kind::SQRT}, - {DIVISIBLE_OP, CVC4::Kind::DIVISIBLE_OP}, {CONST_RATIONAL, CVC4::Kind::CONST_RATIONAL}, {LT, CVC4::Kind::LT}, {LEQ, CVC4::Kind::LEQ}, @@ -166,19 +164,12 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {BITVECTOR_ITE, CVC4::Kind::BITVECTOR_ITE}, {BITVECTOR_REDOR, CVC4::Kind::BITVECTOR_REDOR}, {BITVECTOR_REDAND, CVC4::Kind::BITVECTOR_REDAND}, - {BITVECTOR_EXTRACT_OP, CVC4::Kind::BITVECTOR_EXTRACT_OP}, - {BITVECTOR_REPEAT_OP, CVC4::Kind::BITVECTOR_REPEAT_OP}, - {BITVECTOR_ZERO_EXTEND_OP, CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP}, - {BITVECTOR_SIGN_EXTEND_OP, CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP}, - {BITVECTOR_ROTATE_LEFT_OP, CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP}, - {BITVECTOR_ROTATE_RIGHT_OP, CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP}, {BITVECTOR_EXTRACT, CVC4::Kind::BITVECTOR_EXTRACT}, {BITVECTOR_REPEAT, CVC4::Kind::BITVECTOR_REPEAT}, {BITVECTOR_ZERO_EXTEND, CVC4::Kind::BITVECTOR_ZERO_EXTEND}, {BITVECTOR_SIGN_EXTEND, CVC4::Kind::BITVECTOR_SIGN_EXTEND}, {BITVECTOR_ROTATE_LEFT, CVC4::Kind::BITVECTOR_ROTATE_LEFT}, {BITVECTOR_ROTATE_RIGHT, CVC4::Kind::BITVECTOR_ROTATE_RIGHT}, - {INT_TO_BITVECTOR_OP, CVC4::Kind::INT_TO_BITVECTOR_OP}, {INT_TO_BITVECTOR, CVC4::Kind::INT_TO_BITVECTOR}, {BITVECTOR_TO_NAT, CVC4::Kind::BITVECTOR_TO_NAT}, /* FP ------------------------------------------------------------------ */ @@ -209,34 +200,17 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {FLOATINGPOINT_ISNAN, CVC4::Kind::FLOATINGPOINT_ISNAN}, {FLOATINGPOINT_ISNEG, CVC4::Kind::FLOATINGPOINT_ISNEG}, {FLOATINGPOINT_ISPOS, CVC4::Kind::FLOATINGPOINT_ISPOS}, - {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, - CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP}, - {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, - CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, - {FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, - CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP}, {FLOATINGPOINT_TO_FP_FLOATINGPOINT, CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT}, - {FLOATINGPOINT_TO_FP_REAL_OP, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP}, {FLOATINGPOINT_TO_FP_REAL, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL}, - {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, - CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP}, {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, - {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, - CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP}, {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR}, - {FLOATINGPOINT_TO_FP_GENERIC_OP, - CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP}, {FLOATINGPOINT_TO_FP_GENERIC, CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC}, - {FLOATINGPOINT_TO_UBV_OP, CVC4::Kind::FLOATINGPOINT_TO_UBV_OP}, {FLOATINGPOINT_TO_UBV, CVC4::Kind::FLOATINGPOINT_TO_UBV}, - {FLOATINGPOINT_TO_UBV_TOTAL_OP, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP}, {FLOATINGPOINT_TO_UBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL}, - {FLOATINGPOINT_TO_SBV_OP, CVC4::Kind::FLOATINGPOINT_TO_SBV_OP}, {FLOATINGPOINT_TO_SBV, CVC4::Kind::FLOATINGPOINT_TO_SBV}, - {FLOATINGPOINT_TO_SBV_TOTAL_OP, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP}, {FLOATINGPOINT_TO_SBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL}, {FLOATINGPOINT_TO_REAL, CVC4::Kind::FLOATINGPOINT_TO_REAL}, {FLOATINGPOINT_TO_REAL_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL}, @@ -249,9 +223,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR}, {APPLY_SELECTOR_TOTAL, CVC4::Kind::APPLY_SELECTOR_TOTAL}, {APPLY_TESTER, CVC4::Kind::APPLY_TESTER}, - {TUPLE_UPDATE_OP, CVC4::Kind::TUPLE_UPDATE_OP}, {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE}, - {RECORD_UPDATE_OP, CVC4::Kind::RECORD_UPDATE_OP}, {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE}, /* Separation Logic ---------------------------------------------------- */ {SEP_NIL, CVC4::Kind::SEP_NIL}, @@ -323,7 +295,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::LAMBDA, LAMBDA}, {CVC4::Kind::CHOICE, CHOICE}, {CVC4::Kind::CHAIN, CHAIN}, - {CVC4::Kind::CHAIN_OP, CHAIN_OP}, + {CVC4::Kind::CHAIN_OP, CHAIN}, /* Boolean --------------------------------------------------------- */ {CVC4::Kind::CONST_BOOLEAN, CONST_BOOLEAN}, {CVC4::Kind::NOT, NOT}, @@ -364,7 +336,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::ARCSECANT, ARCSECANT}, {CVC4::Kind::ARCCOTANGENT, ARCCOTANGENT}, {CVC4::Kind::SQRT, SQRT}, - {CVC4::Kind::DIVISIBLE_OP, DIVISIBLE_OP}, + {CVC4::Kind::DIVISIBLE_OP, DIVISIBLE}, {CVC4::Kind::CONST_RATIONAL, CONST_RATIONAL}, {CVC4::Kind::LT, LT}, {CVC4::Kind::LEQ, LEQ}, @@ -412,19 +384,19 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::BITVECTOR_ITE, BITVECTOR_ITE}, {CVC4::Kind::BITVECTOR_REDOR, BITVECTOR_REDOR}, {CVC4::Kind::BITVECTOR_REDAND, BITVECTOR_REDAND}, - {CVC4::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT_OP}, - {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT_OP}, - {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND_OP}, - {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND_OP}, - {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT_OP}, - {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT_OP}, + {CVC4::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT}, + {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT}, + {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND}, + {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND}, + {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT}, + {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT}, {CVC4::Kind::BITVECTOR_EXTRACT, BITVECTOR_EXTRACT}, {CVC4::Kind::BITVECTOR_REPEAT, BITVECTOR_REPEAT}, {CVC4::Kind::BITVECTOR_ZERO_EXTEND, BITVECTOR_ZERO_EXTEND}, {CVC4::Kind::BITVECTOR_SIGN_EXTEND, BITVECTOR_SIGN_EXTEND}, {CVC4::Kind::BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_LEFT}, {CVC4::Kind::BITVECTOR_ROTATE_RIGHT, BITVECTOR_ROTATE_RIGHT}, - {CVC4::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR_OP}, + {CVC4::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR}, {CVC4::Kind::INT_TO_BITVECTOR, INT_TO_BITVECTOR}, {CVC4::Kind::BITVECTOR_TO_NAT, BITVECTOR_TO_NAT}, /* FP -------------------------------------------------------------- */ @@ -456,35 +428,33 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG}, {CVC4::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS}, {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP}, + FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, - FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP}, + FLOATINGPOINT_TO_FP_FLOATINGPOINT}, {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT, FLOATINGPOINT_TO_FP_FLOATINGPOINT}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL_OP}, + {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL}, {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL}, {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP}, + FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP}, + FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR}, {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR}, {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP, - FLOATINGPOINT_TO_FP_GENERIC_OP}, + FLOATINGPOINT_TO_FP_GENERIC}, {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC}, - {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV_OP}, + {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV}, {CVC4::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV}, - {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, - FLOATINGPOINT_TO_UBV_TOTAL_OP}, + {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, FLOATINGPOINT_TO_UBV_TOTAL}, {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL, FLOATINGPOINT_TO_UBV_TOTAL}, - {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV_OP}, + {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV}, {CVC4::Kind::FLOATINGPOINT_TO_SBV, FLOATINGPOINT_TO_SBV}, - {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, - FLOATINGPOINT_TO_SBV_TOTAL_OP}, + {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, FLOATINGPOINT_TO_SBV_TOTAL}, {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL, FLOATINGPOINT_TO_SBV_TOTAL}, {CVC4::Kind::FLOATINGPOINT_TO_REAL, FLOATINGPOINT_TO_REAL}, {CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL, FLOATINGPOINT_TO_REAL_TOTAL}, @@ -497,9 +467,9 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR}, {CVC4::Kind::APPLY_SELECTOR_TOTAL, APPLY_SELECTOR_TOTAL}, {CVC4::Kind::APPLY_TESTER, APPLY_TESTER}, - {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE_OP}, + {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE}, {CVC4::Kind::TUPLE_UPDATE, TUPLE_UPDATE}, - {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE_OP}, + {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE}, {CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE}, /* Separation Logic ------------------------------------------------ */ {CVC4::Kind::SEP_NIL, SEP_NIL}, @@ -653,8 +623,8 @@ class CVC4ApiExceptionStream ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream() #define CVC4_API_CHECK_NOT_NULL \ - CVC4_API_CHECK(!isNull()) << "Invalid call to '" << __PRETTY_FUNCTION__ \ - << "', expected non-null object"; + CVC4_API_CHECK(!isNullHelper()) << "Invalid call to '" << __PRETTY_FUNCTION__ \ + << "', expected non-null object"; #define CVC4_API_ARG_CHECK_NOT_NULL(arg) \ CVC4_API_CHECK(!arg.isNull()) << "Invalid null argument for '" << #arg << "'"; @@ -787,11 +757,30 @@ Sort::Sort() : d_type(new CVC4::Type()) {} Sort::~Sort() {} +/* Helpers */ +/* -------------------------------------------------------------------------- */ + +/* Split out to avoid nested API calls (problematic with API tracing). */ +/* .......................................................................... */ + +bool Sort::isNullHelper() const { return d_type->isNull(); } + +std::vector<Sort> Sort::typeVectorToSorts( + const std::vector<CVC4::Type>& types) const +{ + std::vector<Sort> res; + for (const CVC4::Type& t : types) + { + res.push_back(Sort(t)); + } + return res; +} + bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; } bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; } -bool Sort::isNull() const { return d_type->isNull(); } +bool Sort::isNull() const { return isNullHelper(); } bool Sort::isBoolean() const { return d_type->isBoolean(); } @@ -998,28 +987,251 @@ std::vector<Sort> Sort::getTupleSorts() const /* --------------------------------------------------------------------- */ -std::vector<Sort> Sort::typeVectorToSorts( - const std::vector<CVC4::Type>& types) const +std::ostream& operator<<(std::ostream& out, const Sort& s) { - std::vector<Sort> res; - for (const CVC4::Type& t : types) + out << s.toString(); + return out; +} + +size_t SortHashFunction::operator()(const Sort& s) const +{ + return TypeHashFunction()(*s.d_type); +} + +/* -------------------------------------------------------------------------- */ +/* Op */ +/* -------------------------------------------------------------------------- */ + +Op::Op() : d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {} + +Op::Op(const Kind k) : d_kind(k), d_expr(new CVC4::Expr()) {} + +Op::Op(const Kind k, const CVC4::Expr& e) : d_kind(k), d_expr(new CVC4::Expr(e)) +{ +} + +Op::~Op() {} + +/* Helpers */ +/* -------------------------------------------------------------------------- */ + +/* Split out to avoid nested API calls (problematic with API tracing). */ +/* .......................................................................... */ + +bool Op::isNullHelper() const { return (d_expr->isNull() && (d_kind == NULL_EXPR)); } + +bool Op::isIndexedHelper() const { return !d_expr->isNull(); } + +/* Public methods */ +bool Op::operator==(const Op& t) const +{ + if (d_expr->isNull() || t.d_expr->isNull()) { - res.push_back(Sort(t)); + return false; } - return res; + return (d_kind == t.d_kind) && (*d_expr == *t.d_expr); } -/* --------------------------------------------------------------------- */ +bool Op::operator!=(const Op& t) const { return !(*this == t); } -std::ostream& operator<<(std::ostream& out, const Sort& s) +Kind Op::getKind() const { - out << s.toString(); + CVC4_API_CHECK(d_kind != NULL_EXPR) << "Expecting a non-null Kind"; + return d_kind; +} + +Sort Op::getSort() const +{ + CVC4_API_CHECK_NOT_NULL; + return Sort(d_expr->getType()); +} + +bool Op::isNull() const { return isNullHelper(); } + +bool Op::isIndexed() const { return isIndexedHelper(); } + +template <> +std::string Op::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(!d_expr->isNull()) + << "Expecting a non-null internal expression. This Op is not indexed."; + + std::string i; + Kind k = intToExtKind(d_expr->getKind()); + + if (k == DIVISIBLE) + { + // DIVISIBLE returns a string index to support + // arbitrary precision integers + CVC4::Integer _int = d_expr->getConst<Divisible>().k; + i = _int.toString(); + } + else if (k == RECORD_UPDATE) + { + i = d_expr->getConst<RecordUpdate>().getField(); + } + else + { + CVC4_API_CHECK(false) << "Can't get string index from" + << " kind " << kindToString(k); + } + + return i; +} + +template <> +Kind Op::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(!d_expr->isNull()) + << "Expecting a non-null internal expression. This Op is not indexed."; + Kind kind = intToExtKind(d_expr->getKind()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN"; + return intToExtKind(d_expr->getConst<Chain>().getOperator()); +} + +template <> +uint32_t Op::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(!d_expr->isNull()) + << "Expecting a non-null internal expression. This Op is not indexed."; + + uint32_t i = 0; + Kind k = intToExtKind(d_expr->getKind()); + switch (k) + { + case BITVECTOR_REPEAT: + i = d_expr->getConst<BitVectorRepeat>().repeatAmount; + break; + case BITVECTOR_ZERO_EXTEND: + i = d_expr->getConst<BitVectorZeroExtend>().zeroExtendAmount; + break; + case BITVECTOR_SIGN_EXTEND: + i = d_expr->getConst<BitVectorSignExtend>().signExtendAmount; + break; + case BITVECTOR_ROTATE_LEFT: + i = d_expr->getConst<BitVectorRotateLeft>().rotateLeftAmount; + break; + case BITVECTOR_ROTATE_RIGHT: + i = d_expr->getConst<BitVectorRotateRight>().rotateRightAmount; + break; + case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().size; break; + case FLOATINGPOINT_TO_UBV: + i = d_expr->getConst<FloatingPointToUBV>().bvs.size; + break; + case FLOATINGPOINT_TO_UBV_TOTAL: + i = d_expr->getConst<FloatingPointToUBVTotal>().bvs.size; + break; + case FLOATINGPOINT_TO_SBV: + i = d_expr->getConst<FloatingPointToSBV>().bvs.size; + break; + case FLOATINGPOINT_TO_SBV_TOTAL: + i = d_expr->getConst<FloatingPointToSBVTotal>().bvs.size; + break; + case TUPLE_UPDATE: i = d_expr->getConst<TupleUpdate>().getIndex(); break; + default: + CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" + << " kind " << kindToString(k); + } + return i; +} + +template <> +std::pair<uint32_t, uint32_t> Op::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(!d_expr->isNull()) + << "Expecting a non-null internal expression. This Op is not indexed."; + + std::pair<uint32_t, uint32_t> indices; + Kind k = intToExtKind(d_expr->getKind()); + + // using if/else instead of case statement because want local variables + if (k == BITVECTOR_EXTRACT) + { + CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>(); + indices = std::make_pair(ext.high, ext.low); + } + else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR) + { + CVC4::FloatingPointToFPIEEEBitVector ext = + d_expr->getConst<FloatingPointToFPIEEEBitVector>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) + { + CVC4::FloatingPointToFPFloatingPoint ext = + d_expr->getConst<FloatingPointToFPFloatingPoint>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_REAL) + { + CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) + { + CVC4::FloatingPointToFPSignedBitVector ext = + d_expr->getConst<FloatingPointToFPSignedBitVector>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) + { + CVC4::FloatingPointToFPUnsignedBitVector ext = + d_expr->getConst<FloatingPointToFPUnsignedBitVector>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_GENERIC) + { + CVC4::FloatingPointToFPGeneric ext = + d_expr->getConst<FloatingPointToFPGeneric>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else + { + CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from" + << " kind " << kindToString(k); + } + return indices; +} + +std::string Op::toString() const +{ + CVC4_API_CHECK_NOT_NULL; + if (d_expr->isNull()) + { + return kindToString(d_kind); + } + else + { + CVC4_API_CHECK(!d_expr->isNull()) + << "Expecting a non-null internal expression"; + return d_expr->toString(); + } +} + +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::Expr Op::getExpr(void) const { return *d_expr; } + +std::ostream& operator<<(std::ostream& out, const Op& t) +{ + out << t.toString(); return out; } -size_t SortHashFunction::operator()(const Sort& s) const +size_t OpHashFunction::operator()(const Op& t) const { - return TypeHashFunction()(*s.d_type); + if (t.isIndexedHelper()) + { + return ExprHashFunction()(*t.d_expr); + } + else + { + return KindHashFunction()(t.d_kind); + } } /* -------------------------------------------------------------------------- */ @@ -1032,6 +1244,14 @@ Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {} Term::~Term() {} +/* Helpers */ +/* -------------------------------------------------------------------------- */ + +/* Split out to avoid nested API calls (problematic with API tracing). */ +/* .......................................................................... */ + +bool Term::isNullHelper() const { return d_expr->isNull(); } + bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; } bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; } @@ -1054,7 +1274,40 @@ Sort Term::getSort() const return Sort(d_expr->getType()); } -bool Term::isNull() const { return d_expr->isNull(); } +bool Term::hasOp() const +{ + CVC4_API_CHECK_NOT_NULL; + return d_expr->hasOperator(); +} + +Op Term::getOp() const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(d_expr->hasOperator()) + << "Expecting Term to have an Op when calling getOp()"; + CVC4::Expr op = d_expr->getOperator(); + CVC4::Type t = op.getType(); + + // special cases for Datatype operators + if (t.isSelector()) + { + return Op(APPLY_SELECTOR, op); + } + else if (t.isConstructor()) + { + return Op(APPLY_CONSTRUCTOR, op); + } + else if (t.isTester()) + { + return Op(APPLY_TESTER, op); + } + else + { + return Op(intToExtKind(op.getKind()), op); + } +} + +bool Term::isNull() const { return isNullHelper(); } bool Term::isParameterized() const { @@ -1176,41 +1429,38 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const std::string Term::toString() const { return d_expr->toString(); } -Term::const_iterator::const_iterator() : d_iterator(nullptr) {} +Term::const_iterator::const_iterator() : d_orig_expr(nullptr), d_pos(0) {} -Term::const_iterator::const_iterator(void* it) : d_iterator(it) {} +Term::const_iterator::const_iterator(const std::shared_ptr<CVC4::Expr>& e, + uint32_t p) + : d_orig_expr(e), d_pos(p) +{ +} Term::const_iterator::const_iterator(const const_iterator& it) - : d_iterator(nullptr) + : d_orig_expr(nullptr) { - if (it.d_iterator != nullptr) + if (it.d_orig_expr != nullptr) { - d_iterator = new CVC4::Expr::const_iterator( - *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator)); + d_orig_expr = it.d_orig_expr; + d_pos = it.d_pos; } } Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it) { - delete static_cast<CVC4::Expr::const_iterator*>(d_iterator); - d_iterator = new CVC4::Expr::const_iterator( - *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator)); + d_orig_expr = it.d_orig_expr; + d_pos = it.d_pos; return *this; } -Term::const_iterator::~const_iterator() -{ - delete static_cast<CVC4::Expr::const_iterator*>(d_iterator); -} - bool Term::const_iterator::operator==(const const_iterator& it) const { - if (d_iterator == nullptr || it.d_iterator == nullptr) + if (d_orig_expr == nullptr || it.d_orig_expr == nullptr) { return false; } - return *static_cast<CVC4::Expr::const_iterator*>(d_iterator) - == *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator); + return (*d_orig_expr == *it.d_orig_expr) && (d_pos == it.d_pos); } bool Term::const_iterator::operator!=(const const_iterator& it) const @@ -1220,33 +1470,53 @@ bool Term::const_iterator::operator!=(const const_iterator& it) const Term::const_iterator& Term::const_iterator::operator++() { - Assert(d_iterator != nullptr); - ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator); + Assert(d_orig_expr != nullptr); + ++d_pos; return *this; } Term::const_iterator Term::const_iterator::operator++(int) { - Assert(d_iterator != nullptr); + Assert(d_orig_expr != nullptr); const_iterator it = *this; - ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator); + ++d_pos; return it; } Term Term::const_iterator::operator*() const { - Assert(d_iterator != nullptr); - return Term(**static_cast<CVC4::Expr::const_iterator*>(d_iterator)); + Assert(d_orig_expr != nullptr); + if (!d_pos && (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF)) + { + return Term(d_orig_expr->getOperator()); + } + else + { + uint32_t idx = d_pos; + if (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF) + { + Assert(idx > 0); + --idx; + } + Assert(idx >= 0); + return Term((*d_orig_expr)[idx]); + } } Term::const_iterator Term::begin() const { - return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->begin())); + return Term::const_iterator(d_expr, 0); } Term::const_iterator Term::end() const { - return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end())); + int endpos = d_expr->getNumChildren(); + if (d_expr->getKind() == CVC4::Kind::APPLY_UF) + { + // one more child if this is a UF application (count the UF as a child) + ++endpos; + } + return Term::const_iterator(d_expr, endpos); } // !!! This is only temporarily available until the parser is fully migrated @@ -1300,188 +1570,6 @@ size_t TermHashFunction::operator()(const Term& t) const return ExprHashFunction()(*t.d_expr); } -/* -------------------------------------------------------------------------- */ -/* OpTerm */ -/* -------------------------------------------------------------------------- */ - -OpTerm::OpTerm() : d_expr(new CVC4::Expr()) {} - -OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {} - -OpTerm::~OpTerm() {} - -bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; } - -bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; } - -Kind OpTerm::getKind() const -{ - CVC4_API_CHECK_NOT_NULL; - return intToExtKind(d_expr->getKind()); -} - -Sort OpTerm::getSort() const -{ - CVC4_API_CHECK_NOT_NULL; - return Sort(d_expr->getType()); -} - -bool OpTerm::isNull() const { return d_expr->isNull(); } - -template <> -std::string OpTerm::getIndices() const -{ - CVC4_API_CHECK_NOT_NULL; - std::string i; - Kind k = intToExtKind(d_expr->getKind()); - - if (k == DIVISIBLE_OP) - { - // DIVISIBLE_OP returns a string index to support - // arbitrary precision integers - CVC4::Integer _int = d_expr->getConst<Divisible>().k; - i = _int.toString(); - } - else if (k == RECORD_UPDATE_OP) - { - i = d_expr->getConst<RecordUpdate>().getField(); - } - else - { - CVC4_API_CHECK(false) << "Can't get string index from" - << " kind " << kindToString(k); - } - - return i; -} - -template <> -Kind OpTerm::getIndices() const -{ - CVC4_API_CHECK_NOT_NULL; - Kind kind = intToExtKind(d_expr->getKind()); - CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP"; - return intToExtKind(d_expr->getConst<Chain>().getOperator()); -} - -template <> -uint32_t OpTerm::getIndices() const -{ - CVC4_API_CHECK_NOT_NULL; - uint32_t i = 0; - Kind k = intToExtKind(d_expr->getKind()); - switch (k) - { - case BITVECTOR_REPEAT_OP: - i = d_expr->getConst<BitVectorRepeat>().repeatAmount; - break; - case BITVECTOR_ZERO_EXTEND_OP: - i = d_expr->getConst<BitVectorZeroExtend>().zeroExtendAmount; - break; - case BITVECTOR_SIGN_EXTEND_OP: - i = d_expr->getConst<BitVectorSignExtend>().signExtendAmount; - break; - case BITVECTOR_ROTATE_LEFT_OP: - i = d_expr->getConst<BitVectorRotateLeft>().rotateLeftAmount; - break; - case BITVECTOR_ROTATE_RIGHT_OP: - i = d_expr->getConst<BitVectorRotateRight>().rotateRightAmount; - break; - case INT_TO_BITVECTOR_OP: - i = d_expr->getConst<IntToBitVector>().size; - break; - case FLOATINGPOINT_TO_UBV_OP: - i = d_expr->getConst<FloatingPointToUBV>().bvs.size; - break; - case FLOATINGPOINT_TO_UBV_TOTAL_OP: - i = d_expr->getConst<FloatingPointToUBVTotal>().bvs.size; - break; - case FLOATINGPOINT_TO_SBV_OP: - i = d_expr->getConst<FloatingPointToSBV>().bvs.size; - break; - case FLOATINGPOINT_TO_SBV_TOTAL_OP: - i = d_expr->getConst<FloatingPointToSBVTotal>().bvs.size; - break; - case TUPLE_UPDATE_OP: i = d_expr->getConst<TupleUpdate>().getIndex(); break; - default: - CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" - << " kind " << kindToString(k); - } - return i; -} - -template <> -std::pair<uint32_t, uint32_t> OpTerm::getIndices() const -{ - CVC4_API_CHECK_NOT_NULL; - std::pair<uint32_t, uint32_t> indices; - Kind k = intToExtKind(d_expr->getKind()); - - // using if/else instead of case statement because want local variables - if (k == BITVECTOR_EXTRACT_OP) - { - CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>(); - indices = std::make_pair(ext.high, ext.low); - } - else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP) - { - CVC4::FloatingPointToFPIEEEBitVector ext = - d_expr->getConst<FloatingPointToFPIEEEBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP) - { - CVC4::FloatingPointToFPFloatingPoint ext = - d_expr->getConst<FloatingPointToFPFloatingPoint>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_REAL_OP) - { - CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP) - { - CVC4::FloatingPointToFPSignedBitVector ext = - d_expr->getConst<FloatingPointToFPSignedBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP) - { - CVC4::FloatingPointToFPUnsignedBitVector ext = - d_expr->getConst<FloatingPointToFPUnsignedBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_GENERIC_OP) - { - CVC4::FloatingPointToFPGeneric ext = - d_expr->getConst<FloatingPointToFPGeneric>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else - { - CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from" - << " kind " << kindToString(k); - } - return indices; -} - -std::string OpTerm::toString() const { return d_expr->toString(); } - -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! -CVC4::Expr OpTerm::getExpr(void) const { return *d_expr; } - -std::ostream& operator<<(std::ostream& out, const OpTerm& t) -{ - out << t.toString(); - return out; -} - -size_t OpTermHashFunction::operator()(const OpTerm& t) const -{ - return ExprHashFunction()(*t.d_expr); -} /* -------------------------------------------------------------------------- */ /* Datatypes */ @@ -1635,10 +1723,11 @@ DatatypeSelector::~DatatypeSelector() {} bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); } -OpTerm DatatypeSelector::getSelectorTerm() const +Op DatatypeSelector::getSelectorTerm() const { CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector."; - return d_stor->getSelector(); + CVC4::Expr sel = d_stor->getSelector(); + return Op(APPLY_SELECTOR, sel); } std::string DatatypeSelector::toString() const @@ -1675,10 +1764,11 @@ DatatypeConstructor::~DatatypeConstructor() {} bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); } -OpTerm DatatypeConstructor::getConstructorTerm() const +Op DatatypeConstructor::getConstructorTerm() const { CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor."; - return OpTerm(d_ctor->getConstructor()); + CVC4::Expr ctor = d_ctor->getConstructor(); + return Op(APPLY_CONSTRUCTOR, ctor); } DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const @@ -1695,11 +1785,12 @@ DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const return (*d_ctor)[name]; } -OpTerm DatatypeConstructor::getSelectorTerm(const std::string& name) const +Op DatatypeConstructor::getSelectorTerm(const std::string& name) const { // CHECK: cons with name exists? // CHECK: is resolved? - return d_ctor->getSelector(name); + CVC4::Expr sel = d_ctor->getSelector(name); + return Op(APPLY_SELECTOR, sel); } DatatypeConstructor::const_iterator DatatypeConstructor::begin() const @@ -1824,11 +1915,12 @@ DatatypeConstructor Datatype::getConstructor(const std::string& name) const return (*d_dtype)[name]; } -OpTerm Datatype::getConstructorTerm(const std::string& name) const +Op Datatype::getConstructorTerm(const std::string& name) const { // CHECK: cons with name exists? // CHECK: is resolved? - return d_dtype->getConstructor(name); + CVC4::Expr ctor = d_dtype->getConstructor(name); + return Op(APPLY_CONSTRUCTOR, ctor); } size_t Datatype::getNumConstructors() const @@ -2032,6 +2124,31 @@ Term Solver::mkBVFromStrHelper(uint32_t size, return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); } +Term Solver::mkTermFromKind(Kind kind) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK_EXPECTED( + kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind) + << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; + + Term res; + if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) + { + CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); + res = d_exprMgr->mkExpr(k, std::vector<Expr>()); + } + else + { + Assert(kind == PI); + res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); + } + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + + CVC4_API_SOLVER_TRY_CATCH_END; +} + /* Helpers for converting vectors. */ /* .......................................................................... */ @@ -2079,36 +2196,6 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const << " children (the one under construction has " << nchildren << ")"; } -void Solver::checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const -{ - Assert(isDefinedIntKind(extToIntKind(kind))); - const CVC4::Kind int_kind = extToIntKind(kind); - const CVC4::Kind int_op_kind = opTerm.d_expr->getKind(); - const CVC4::Kind int_op_to_kind = - NodeManager::operatorToKind(opTerm.d_expr->getNode()); - CVC4_API_ARG_CHECK_EXPECTED( - int_kind == int_op_to_kind - || (kind == APPLY_CONSTRUCTOR - && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND) - || (kind == APPLY_SELECTOR - && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND) - || (kind == APPLY_UF && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND), - kind) - << "kind that matches kind associated with given operator term"; - CVC4_API_ARG_CHECK_EXPECTED( - int_op_kind == CVC4::kind::BUILTIN - || CVC4::kind::metaKindOf(int_kind) == kind::metakind::PARAMETERIZED, - opTerm) - << "This term constructor is for parameterized kinds only"; - uint32_t min_arity = ExprManager::minArity(int_kind); - uint32_t max_arity = ExprManager::maxArity(int_kind); - CVC4_API_KIND_CHECK_EXPECTED(nchildren >= min_arity && nchildren <= max_arity, - kind) - << "Terms with kind " << kindToString(kind) << " must have at least " - << min_arity << " children and at most " << max_arity - << " children (the one under construction has " << nchildren << ")"; -} - /* Sorts Handling */ /* -------------------------------------------------------------------------- */ @@ -2758,25 +2845,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const Term Solver::mkTerm(Kind kind) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_KIND_CHECK_EXPECTED( - kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind) - << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; - - Term res; - if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) - { - CVC4::Kind k = extToIntKind(kind); - Assert(isDefinedIntKind(k)); - res = d_exprMgr->mkExpr(k, std::vector<Expr>()); - } - else - { - Assert(kind == PI); - res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); - } - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - + return mkTermFromKind(kind); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -2849,69 +2918,99 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkTerm(Kind kind, OpTerm opTerm) const +Term Solver::mkTerm(Op op) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - checkMkOpTerm(kind, opTerm, 0); - const CVC4::Kind int_kind = extToIntKind(kind); - Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr); + Term res; + if (op.isIndexedHelper()) + { + const CVC4::Kind int_kind = extToIntKind(op.d_kind); + res = d_exprMgr->mkExpr(int_kind, *op.d_expr); + } + else + { + res = mkTermFromKind(op.d_kind); + } + (void)res.d_expr->getType(true); /* kick off type checking */ return res; CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child) const +Term Solver::mkTerm(Op op, Term child) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; - checkMkOpTerm(kind, opTerm, 1); - const CVC4::Kind int_kind = extToIntKind(kind); - Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, *child.d_expr); + const CVC4::Kind int_kind = extToIntKind(op.d_kind); + Term res; + if (op.isIndexedHelper()) + { + res = d_exprMgr->mkExpr(int_kind, *op.d_expr, *child.d_expr); + } + else + { + res = d_exprMgr->mkExpr(int_kind, *child.d_expr); + } + (void)res.d_expr->getType(true); /* kick off type checking */ return res; CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const +Term Solver::mkTerm(Op op, Term child1, Term child2) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; - checkMkOpTerm(kind, opTerm, 2); - const CVC4::Kind int_kind = extToIntKind(kind); - Term res = d_exprMgr->mkExpr( - int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr); + const CVC4::Kind int_kind = extToIntKind(op.d_kind); + Term res; + if (op.isIndexedHelper()) + { + res = + d_exprMgr->mkExpr(int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr); + } + else + { + res = d_exprMgr->mkExpr(int_kind, *child1.d_expr, *child2.d_expr); + } + (void)res.d_expr->getType(true); /* kick off type checking */ return res; CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkTerm( - Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const +Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term"; - checkMkOpTerm(kind, opTerm, 3); - const CVC4::Kind int_kind = extToIntKind(kind); - Term res = d_exprMgr->mkExpr( - int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr); + const CVC4::Kind int_kind = extToIntKind(op.d_kind); + Term res; + if (op.isIndexedHelper()) + { + res = d_exprMgr->mkExpr( + int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr); + } + else + { + res = d_exprMgr->mkExpr( + int_kind, *child1.d_expr, *child2.d_expr, *child3.d_expr); + } + (void)res.d_expr->getType(true); /* kick off type checking */ return res; CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkTerm(Kind kind, - OpTerm opTerm, - const std::vector<Term>& children) const +Term Solver::mkTerm(Op op, const std::vector<Term>& children) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = children.size(); i < size; ++i) @@ -2920,11 +3019,19 @@ Term Solver::mkTerm(Kind kind, !children[i].isNull(), "parameter term", children[i], i) << "non-null term"; } - checkMkOpTerm(kind, opTerm, children.size()); - const CVC4::Kind int_kind = extToIntKind(kind); + const CVC4::Kind int_kind = extToIntKind(op.d_kind); std::vector<Expr> echildren = termVectorToExprs(children); - Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren); + Term res; + if (op.isIndexedHelper()) + { + res = d_exprMgr->mkExpr(int_kind, *op.d_expr, echildren); + } + else + { + res = d_exprMgr->mkExpr(int_kind, echildren); + } + (void)res.d_expr->getType(true); /* kick off type checking */ return res; @@ -2954,30 +3061,33 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts, CVC4_API_SOLVER_TRY_CATCH_END; } -/* Create operator terms */ +/* Create operators */ /* -------------------------------------------------------------------------- */ -OpTerm Solver::mkOpTerm(Kind kind, Kind k) const +Op Solver::mkOp(Kind kind, Kind k) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP"; + CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN"; - return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get(); + return Op( + kind, + *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get()); CVC4_API_SOLVER_TRY_CATCH_END; } -OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const +Op Solver::mkOp(Kind kind, const std::string& arg) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_KIND_CHECK_EXPECTED( - (kind == RECORD_UPDATE_OP) || (kind == DIVISIBLE_OP), kind) - << "RECORD_UPDATE_OP or DIVISIBLE_OP"; - OpTerm res; - if (kind == RECORD_UPDATE_OP) + CVC4_API_KIND_CHECK_EXPECTED((kind == RECORD_UPDATE) || (kind == DIVISIBLE), + kind) + << "RECORD_UPDATE or DIVISIBLE"; + Op res; + if (kind == RECORD_UPDATE) { - res = - *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get(); + res = Op( + kind, + *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get()); } else { @@ -2986,76 +3096,90 @@ OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const * as invalid. */ CVC4_API_ARG_CHECK_EXPECTED(arg != ".", arg) << "a string representing an integer, real or rational value."; - res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg))) - .d_expr.get(); + res = Op(kind, + *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg))) + .d_expr.get()); } return res; CVC4_API_SOLVER_TRY_CATCH_END; } -OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const +Op Solver::mkOp(Kind kind, uint32_t arg) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK(kind); - OpTerm res; + Op res; switch (kind) { - case DIVISIBLE_OP: - res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get(); + case DIVISIBLE: + res = + Op(kind, + *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get()); break; - case BITVECTOR_REPEAT_OP: - res = *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg)) - .d_expr.get(); + case BITVECTOR_REPEAT: + res = Op(kind, + *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg)) + .d_expr.get()); break; - case BITVECTOR_ZERO_EXTEND_OP: - res = *mkValHelper<CVC4::BitVectorZeroExtend>( - CVC4::BitVectorZeroExtend(arg)) - .d_expr.get(); + case BITVECTOR_ZERO_EXTEND: + res = Op(kind, + *mkValHelper<CVC4::BitVectorZeroExtend>( + CVC4::BitVectorZeroExtend(arg)) + .d_expr.get()); break; - case BITVECTOR_SIGN_EXTEND_OP: - res = *mkValHelper<CVC4::BitVectorSignExtend>( - CVC4::BitVectorSignExtend(arg)) - .d_expr.get(); + case BITVECTOR_SIGN_EXTEND: + res = Op(kind, + *mkValHelper<CVC4::BitVectorSignExtend>( + CVC4::BitVectorSignExtend(arg)) + .d_expr.get()); break; - case BITVECTOR_ROTATE_LEFT_OP: - res = *mkValHelper<CVC4::BitVectorRotateLeft>( - CVC4::BitVectorRotateLeft(arg)) - .d_expr.get(); + case BITVECTOR_ROTATE_LEFT: + res = Op(kind, + *mkValHelper<CVC4::BitVectorRotateLeft>( + CVC4::BitVectorRotateLeft(arg)) + .d_expr.get()); break; - case BITVECTOR_ROTATE_RIGHT_OP: - res = *mkValHelper<CVC4::BitVectorRotateRight>( - CVC4::BitVectorRotateRight(arg)) - .d_expr.get(); + case BITVECTOR_ROTATE_RIGHT: + res = Op(kind, + *mkValHelper<CVC4::BitVectorRotateRight>( + CVC4::BitVectorRotateRight(arg)) + .d_expr.get()); break; - case INT_TO_BITVECTOR_OP: - res = *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)) - .d_expr.get(); + case INT_TO_BITVECTOR: + res = Op(kind, + *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_UBV_OP: - res = + case FLOATINGPOINT_TO_UBV: + res = Op( + kind, *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg)) - .d_expr.get(); + .d_expr.get()); break; - case FLOATINGPOINT_TO_UBV_TOTAL_OP: - res = *mkValHelper<CVC4::FloatingPointToUBVTotal>( - CVC4::FloatingPointToUBVTotal(arg)) - .d_expr.get(); + case FLOATINGPOINT_TO_UBV_TOTAL: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToUBVTotal>( + CVC4::FloatingPointToUBVTotal(arg)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_SBV_OP: - res = + case FLOATINGPOINT_TO_SBV: + res = Op( + kind, *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg)) - .d_expr.get(); + .d_expr.get()); break; - case FLOATINGPOINT_TO_SBV_TOTAL_OP: - res = *mkValHelper<CVC4::FloatingPointToSBVTotal>( - CVC4::FloatingPointToSBVTotal(arg)) - .d_expr.get(); + case FLOATINGPOINT_TO_SBV_TOTAL: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToSBVTotal>( + CVC4::FloatingPointToSBVTotal(arg)) + .d_expr.get()); break; - case TUPLE_UPDATE_OP: - res = - *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get(); + case TUPLE_UPDATE: + res = Op( + kind, + *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get()); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -3067,48 +3191,55 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const CVC4_API_SOLVER_TRY_CATCH_END; } -OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const +Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK(kind); - OpTerm res; + Op res; switch (kind) { - case BITVECTOR_EXTRACT_OP: - res = *mkValHelper<CVC4::BitVectorExtract>( - CVC4::BitVectorExtract(arg1, arg2)) - .d_expr.get(); + case BITVECTOR_EXTRACT: + res = Op(kind, + *mkValHelper<CVC4::BitVectorExtract>( + CVC4::BitVectorExtract(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: - res = *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>( - CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>( + CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: - res = *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>( - CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_FLOATINGPOINT: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>( + CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_REAL_OP: - res = *mkValHelper<CVC4::FloatingPointToFPReal>( - CVC4::FloatingPointToFPReal(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_REAL: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPReal>( + CVC4::FloatingPointToFPReal(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: - res = *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>( - CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>( + CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: - res = *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>( - CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>( + CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_GENERIC_OP: - res = *mkValHelper<CVC4::FloatingPointToFPGeneric>( - CVC4::FloatingPointToFPGeneric(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_GENERIC: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPGeneric>( + CVC4::FloatingPointToFPGeneric(arg1, arg2)) + .d_expr.get()); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index ad923f866..326a8fb70 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -177,7 +177,7 @@ class CVC4_PUBLIC Sort friend class DatatypeConstructorDecl; friend class DatatypeDecl; friend class DatatypeSelectorDecl; - friend class OpTerm; + friend class Op; friend class Solver; friend struct SortHashFunction; friend class Term; @@ -495,6 +495,12 @@ class CVC4_PUBLIC Sort std::vector<Sort> getTupleSorts() const; private: + /** + * Helper for isNull checks. This prevents calling an API function with + * CVC4_API_CHECK_NOT_NULL + */ + bool isNullHelper() const; + /* Helper to convert a vector of sorts into a vector of internal types. */ std::vector<Sort> typeVectorToSorts( const std::vector<CVC4::Type>& vector) const; @@ -524,6 +530,136 @@ struct CVC4_PUBLIC SortHashFunction }; /* -------------------------------------------------------------------------- */ +/* Op */ +/* -------------------------------------------------------------------------- */ + +/** + * A CVC4 operator. + * An operator is a term that represents certain operators, instantiated + * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT. + */ +class CVC4_PUBLIC Op +{ + friend class Solver; + friend struct OpHashFunction; + + public: + /** + * Constructor. + */ + Op(); + + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor for a single kind (non-indexed operator). + * @param k the kind of this Op + */ + Op(const Kind k); + + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor. + * @param k the kind of this Op + * @param e the internal expression that is to be wrapped by this term + * @return the Term + */ + Op(const Kind k, const CVC4::Expr& e); + + /** + * Destructor. + */ + ~Op(); + + /** + * Syntactic equality operator. + * Return true if both operators are syntactically identical. + * Both operators must belong to the same solver object. + * @param t the operator to compare to for equality + * @return true if the operators are equal + */ + bool operator==(const Op& t) const; + + /** + * Syntactic disequality operator. + * Return true if both operators differ syntactically. + * Both terms must belong to the same solver object. + * @param t the operator to compare to for disequality + * @return true if operators are disequal + */ + bool operator!=(const Op& t) const; + + /** + * @return the kind of this operator + */ + Kind getKind() const; + + /** + * @return the sort of this operator + */ + Sort getSort() const; + + /** + * @return true if this operator is a null term + */ + bool isNull() const; + + /** + * @return true iff this operator is indexed + */ + bool isIndexed() const; + + /** + * Get the indices used to create this Op. + * Supports the following template arguments: + * - string + * - Kind + * - uint32_t + * - pair<uint32_t, uint32_t> + * Check the Op Kind with getKind() to determine which argument to use. + * @return the indices used to create this Op + */ + template <typename T> + T getIndices() const; + + /** + * @return a string representation of this operator + */ + std::string toString() const; + + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::Expr getExpr(void) const; + + private: + /** + * Helper for isNull checks. This prevents calling an API function with + * CVC4_API_CHECK_NOT_NULL + */ + bool isNullHelper() const; + + /** + * Note: An indexed operator has a non-null internal expr, d_expr + * Note 2: We use a helper method to avoid having API functions call + * other API functions (we need to call this internally) + * @return true iff this Op is indexed + */ + bool isIndexedHelper() const; + + /* The kind of this operator. */ + Kind d_kind; + + /** + * The internal expression wrapped by this operator. + * This is a shared_ptr rather than a unique_ptr to avoid overhead due to + * memory allocation (CVC4::Expr is already ref counted, so this could be + * a unique_ptr instead). + */ + std::shared_ptr<CVC4::Expr> d_expr; +}; + +/* -------------------------------------------------------------------------- */ /* Term */ /* -------------------------------------------------------------------------- */ @@ -591,6 +727,17 @@ class CVC4_PUBLIC Term Sort getSort() const; /** + * @return true iff this term has an operator + */ + bool hasOp() const; + + /** + * @return the Op used to create this term + * Note: This is safe to call when hasOp() returns true. + */ + Op getOp() const; + + /** * @return true if this Term is a null term */ bool isNull() const; @@ -668,6 +815,9 @@ class CVC4_PUBLIC Term /** * Iterator for the children of a Term. + * Note: This treats uninterpreted functions as Term just like any other term + * for example, the term f(x, y) will have Kind APPLY_UF and three + * children: f, x, and y */ class const_iterator : public std::iterator<std::input_iterator_tag, Term> { @@ -675,19 +825,21 @@ class CVC4_PUBLIC Term public: /** - * Constructor. + * Null Constructor. */ const_iterator(); /** - * Copy constructor. + * Constructor + * @param e a shared pointer to the expression that we're iterating over + * @param p the position of the iterator (e.g. which child it's on) */ - const_iterator(const const_iterator& it); + const_iterator(const std::shared_ptr<CVC4::Expr>& e, uint32_t p); /** - * Destructor. + * Copy constructor. */ - ~const_iterator(); + const_iterator(const const_iterator& it); /** * Assignment operator. @@ -729,10 +881,10 @@ class CVC4_PUBLIC Term Term operator*() const; private: - /* The internal expression iterator wrapped by this iterator. */ - void* d_iterator; - /* Constructor. */ - explicit const_iterator(void*); + /* The original expression to be iterated over */ + std::shared_ptr<CVC4::Expr> d_orig_expr; + /* Keeps track of the iteration position */ + uint32_t d_pos; }; /** @@ -751,6 +903,12 @@ class CVC4_PUBLIC Term private: /** + * Helper for isNull checks. This prevents calling an API function with + * CVC4_API_CHECK_NOT_NULL + */ + bool isNullHelper() const; + + /** * The internal expression wrapped by this term. * This is a shared_ptr rather than a unique_ptr to avoid overhead due to * memory allocation (CVC4::Expr is already ref counted, so this could be @@ -827,119 +985,20 @@ std::ostream& operator<<(std::ostream& out, const std::unordered_map<Term, V, TermHashFunction>& unordered_map) CVC4_PUBLIC; -/* -------------------------------------------------------------------------- */ -/* OpTerm */ -/* -------------------------------------------------------------------------- */ - -/** - * A CVC4 operator term. - * An operator term is a term that represents certain operators, instantiated - * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT. - */ -class CVC4_PUBLIC OpTerm -{ - friend class Solver; - friend struct OpTermHashFunction; - - public: - /** - * Constructor. - */ - OpTerm(); - - // !!! This constructor is only temporarily public until the parser is fully - // migrated to the new API. !!! - /** - * Constructor. - * @param e the internal expression that is to be wrapped by this term - * @return the Term - */ - OpTerm(const CVC4::Expr& e); - - /** - * Destructor. - */ - ~OpTerm(); - - /** - * Syntactic equality operator. - * Return true if both operator terms are syntactically identical. - * Both operator terms must belong to the same solver object. - * @param t the operator term to compare to for equality - * @return true if the operator terms are equal - */ - bool operator==(const OpTerm& t) const; - - /** - * Syntactic disequality operator. - * Return true if both operator terms differ syntactically. - * Both terms must belong to the same solver object. - * @param t the operator term to compare to for disequality - * @return true if operator terms are disequal - */ - bool operator!=(const OpTerm& t) const; - - /** - * @return the kind of this operator term - */ - Kind getKind() const; - - /** - * @return the sort of this operator term - */ - Sort getSort() const; - - /** - * @return true if this operator term is a null term - */ - bool isNull() const; - - /** - * Get the indices used to create this OpTerm. - * Supports the following template arguments: - * - string - * - Kind - * - uint32_t - * - pair<uint32_t, uint32_t> - * Check the OpTerm Kind with getKind() to determine which argument to use. - * @return the indices used to create this OpTerm - */ - template <typename T> - T getIndices() const; - - /** - * @return a string representation of this operator term - */ - std::string toString() const; - - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - CVC4::Expr getExpr(void) const; - - private: - /** - * The internal expression wrapped by this operator term. - * This is a shared_ptr rather than a unique_ptr to avoid overhead due to - * memory allocation (CVC4::Expr is already ref counted, so this could be - * a unique_ptr instead). - */ - std::shared_ptr<CVC4::Expr> d_expr; -}; - /** - * Serialize an operator term to given stream. + * Serialize an operator to given stream. * @param out the output stream - * @param t the operator term to be serialized to the given output stream + * @param t the operator to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const OpTerm& t) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const Op& t) CVC4_PUBLIC; /** - * Hash function for OpTerms. + * Hash function for Ops. */ -struct CVC4_PUBLIC OpTermHashFunction +struct CVC4_PUBLIC OpHashFunction { - size_t operator()(const OpTerm& t) const; + size_t operator()(const Op& t) const; }; /* -------------------------------------------------------------------------- */ @@ -1143,7 +1202,7 @@ class CVC4_PUBLIC DatatypeSelector * Get the selector operator of this datatype selector. * @return the selector operator */ - OpTerm getSelectorTerm() const; + Op getSelectorTerm() const; /** * @return a string representation of this datatype selector @@ -1200,7 +1259,7 @@ class CVC4_PUBLIC DatatypeConstructor * Get the constructor operator of this datatype constructor. * @return the constructor operator */ - OpTerm getConstructorTerm() const; + Op getConstructorTerm() const; /** * Get the datatype selector with the given name. @@ -1219,7 +1278,7 @@ class CVC4_PUBLIC DatatypeConstructor * @param name the name of the datatype selector * @return a term representing the datatype selector with the given name */ - OpTerm getSelectorTerm(const std::string& name) const; + Op getSelectorTerm(const std::string& name) const; /** * @return a string representation of this datatype constructor @@ -1366,7 +1425,7 @@ class CVC4_PUBLIC Datatype * similarly-named constructors, the * first is returned. */ - OpTerm getConstructorTerm(const std::string& name) const; + Op getConstructorTerm(const std::string& name) const; /** Get the number of constructors for this Datatype. */ size_t getNumConstructors() const; @@ -1773,59 +1832,52 @@ class CVC4_PUBLIC Solver Term mkTerm(Kind kind, const std::vector<Term>& children) const; /** - * Create nullary term of given kind from a given operator term. - * Create operator terms with mkOpTerm(). - * @param kind the kind of the term - * @param the operator term + * Create nullary term of given kind from a given operator. + * Create operators with mkOp(). + * @param the operator * @return the Term */ - Term mkTerm(Kind kind, OpTerm opTerm) const; + Term mkTerm(Op op) const; /** - * Create unary term of given kind from a given operator term. - * Create operator terms with mkOpTerm(). - * @param kind the kind of the term - * @param the operator term + * Create unary term of given kind from a given operator. + * Create operators with mkOp(). + * @param the operator * @child the child of the term * @return the Term */ - Term mkTerm(Kind kind, OpTerm opTerm, Term child) const; + Term mkTerm(Op op, Term child) const; /** - * Create binary term of given kind from a given operator term. - * @param kind the kind of the term - * Create operator terms with mkOpTerm(). - * @param the operator term + * Create binary term of given kind from a given operator. + * Create operators with mkOp(). + * @param the operator * @child1 the first child of the term * @child2 the second child of the term * @return the Term */ - Term mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const; + Term mkTerm(Op op, Term child1, Term child2) const; /** - * Create ternary term of given kind from a given operator term. - * Create operator terms with mkOpTerm(). - * @param kind the kind of the term - * @param the operator term + * Create ternary term of given kind from a given operator. + * Create operators with mkOp(). + * @param the operator * @child1 the first child of the term * @child2 the second child of the term * @child3 the third child of the term * @return the Term */ - Term mkTerm( - Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const; + Term mkTerm(Op op, Term child1, Term child2, Term child3) const; /** - * Create n-ary term of given kind from a given operator term. - * Create operator terms with mkOpTerm(). + * Create n-ary term of given kind from a given operator. + * Create operators with mkOp(). * @param kind the kind of the term - * @param the operator term + * @param the operator * @children the children of the term * @return the Term */ - Term mkTerm(Kind kind, - OpTerm opTerm, - const std::vector<Term>& children) const; + Term mkTerm(Op op, const std::vector<Term>& children) const; /** * Create a tuple term. Terms are automatically converted if sorts are @@ -1842,59 +1894,59 @@ class CVC4_PUBLIC Solver /* .................................................................... */ /** - * Create operator term of kind: - * - CHAIN_OP + * Create operator of kind: + * - CHAIN * See enum Kind for a description of the parameters. * @param kind the kind of the operator * @param k the kind argument to this operator */ - OpTerm mkOpTerm(Kind kind, Kind k) const; + Op mkOp(Kind kind, Kind k) const; /** * Create operator of kind: - * - RECORD_UPDATE_OP - * - DIVISIBLE_OP (to support arbitrary precision integers) + * - RECORD_UPDATE + * - DIVISIBLE (to support arbitrary precision integers) * See enum Kind for a description of the parameters. * @param kind the kind of the operator * @param arg the string argument to this operator */ - OpTerm mkOpTerm(Kind kind, const std::string& arg) const; + Op mkOp(Kind kind, const std::string& arg) const; /** * Create operator of kind: - * - DIVISIBLE_OP - * - BITVECTOR_REPEAT_OP - * - BITVECTOR_ZERO_EXTEND_OP - * - BITVECTOR_SIGN_EXTEND_OP - * - BITVECTOR_ROTATE_LEFT_OP - * - BITVECTOR_ROTATE_RIGHT_OP - * - INT_TO_BITVECTOR_OP - * - FLOATINGPOINT_TO_UBV_OP - * - FLOATINGPOINT_TO_UBV_TOTAL_OP - * - FLOATINGPOINT_TO_SBV_OP - * - FLOATINGPOINT_TO_SBV_TOTAL_OP - * - TUPLE_UPDATE_OP + * - DIVISIBLE + * - BITVECTOR_REPEAT + * - BITVECTOR_ZERO_EXTEND + * - BITVECTOR_SIGN_EXTEND + * - BITVECTOR_ROTATE_LEFT + * - BITVECTOR_ROTATE_RIGHT + * - INT_TO_BITVECTOR + * - FLOATINGPOINT_TO_UBV + * - FLOATINGPOINT_TO_UBV_TOTAL + * - FLOATINGPOINT_TO_SBV + * - FLOATINGPOINT_TO_SBV_TOTAL + * - TUPLE_UPDATE * See enum Kind for a description of the parameters. * @param kind the kind of the operator * @param arg the uint32_t argument to this operator */ - OpTerm mkOpTerm(Kind kind, uint32_t arg) const; + Op mkOp(Kind kind, uint32_t arg) const; /** * Create operator of Kind: - * - BITVECTOR_EXTRACT_OP - * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP - * - FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP - * - FLOATINGPOINT_TO_FP_REAL_OP - * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP - * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP - * - FLOATINGPOINT_TO_FP_GENERIC_OP + * - BITVECTOR_EXTRACT + * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR + * - FLOATINGPOINT_TO_FP_FLOATINGPOINT + * - FLOATINGPOINT_TO_FP_REAL + * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR + * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR + * - FLOATINGPOINT_TO_FP_GENERIC * See enum Kind for a description of the parameters. * @param kind the kind of the operator * @param arg1 the first uint32_t argument to this operator * @param arg2 the second uint32_t argument to this operator */ - OpTerm mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const; + Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const; /* .................................................................... */ /* Create Constants */ @@ -2537,9 +2589,7 @@ class CVC4_PUBLIC Solver std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const; /* Helper to convert a vector of sorts to internal types. */ std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const; - /* Helper to check for API misuse in mkTerm functions. */ - void checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const; - /* Helper to check for API misuse in mkOpTerm functions. */ + /* Helper to check for API misuse in mkOp functions. */ void checkMkTerm(Kind kind, uint32_t nchildren) const; /* Helper for mk-functions that call d_exprMgr->mkConst(). */ template <typename T> @@ -2555,6 +2605,8 @@ class CVC4_PUBLIC Solver Term mkBVFromIntHelper(uint32_t size, uint64_t val) const; /* Helper for setLogic. */ void setLogicHelper(const std::string& logic) const; + /* Helper for mkTerm functions that create Term from a Kind */ + Term mkTermFromKind(Kind kind) const; /** * Helper function that ensures that a given term is of sort real (as opposed diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 1f2a36676..bb2700706 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -143,26 +143,24 @@ enum CVC4_PUBLIC Kind : int32_t */ CHOICE, /** - * Chained operation. + * Chained operator. + * Parameters: 1 + * -[1]: Kind of the binary operation + * Create with: + * mkOp(Kind opkind, Kind kind) + + * Apply chained operation. * Parameters: n > 1 - * -[1]: Term of kind CHAIN_OP (represents a binary op) + * -[1]: Op of kind CHAIN (represents a binary op) * -[2]..[n]: Arguments to that operator * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, Term child1, Term child2, Term child3) + * mkTerm(Op op, const std::vector<Term>& children) * Turned into a conjunction of binary applications of the operator on * adjoining parameters. */ CHAIN, - /** - * Chained operator. - * Parameters: 1 - * -[1]: Kind of the binary operation - * Create with: - * mkOpTerm(Kind opkind, Kind kind) - */ - CHAIN_OP, /* Boolean --------------------------------------------------------------- */ @@ -382,16 +380,6 @@ enum CVC4_PUBLIC Kind : int32_t */ ABS, /** - * Divisibility-by-k predicate. - * Parameters: 2 - * -[1]: DIVISIBLE_OP Term - * -[2]: Integer Term - * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) - */ - DIVISIBLE, - /** * Arithmetic power. * Parameters: 2 * -[1]..[2]: Terms of sort Integer, Real @@ -517,9 +505,17 @@ enum CVC4_PUBLIC Kind : int32_t * Parameter: 1 * -[1]: The k to divide by (sort Integer) * Create with: - * mkOpTerm(Kind kind, uint32_t param) + * mkOp(Kind kind, uint32_t param) + * + * Apply divisibility-by-k predicate. + * Parameters: 2 + * -[1]: Op of kind DIVISIBLE + * -[2]: Integer Term + * Create with: + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) */ - DIVISIBLE_OP, + DIVISIBLE, /** * Multiple-precision rational constant. * Parameters: @@ -973,9 +969,6 @@ enum CVC4_PUBLIC Kind : int32_t /* term to be treated as a variable. used for eager bit-blasting Ackermann * expansion of bvurem (internal-only symbol) */ BITVECTOR_ACKERMANIZE_UREM, - /* operator for the bit-vector boolean bit extract. - * One parameter, parameter is the index of the bit to extract */ - BITVECTOR_BITOF_OP, #endif /** * Operator for bit-vector extract (from index 'high' to 'low'). @@ -983,125 +976,115 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: The 'high' index * -[2]: The 'low' index * Create with: - * mkOpTerm(Kind kind, uint32_t param, uint32_t param) + * mkOp(Kind kind, uint32_t param, uint32_t param) + * + * Apply bit-vector extract. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_EXTRACT + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_EXTRACT_OP, + BITVECTOR_EXTRACT, /** * Operator for bit-vector repeat. * Parameter 1: * -[1]: Number of times to repeat a given bit-vector * Create with: - * mkOpTerm(Kind kind, uint32_t param). + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector repeat. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_REPEAT + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_REPEAT_OP, + BITVECTOR_REPEAT, /** * Operator for bit-vector zero-extend. * Parameter 1: * -[1]: Number of bits by which a given bit-vector is to be extended * Create with: - * mkOpTerm(Kind kind, uint32_t param). + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector zero-extend. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_ZERO_EXTEND + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_ZERO_EXTEND_OP, + BITVECTOR_ZERO_EXTEND, /** * Operator for bit-vector sign-extend. * Parameter 1: * -[1]: Number of bits by which a given bit-vector is to be extended * Create with: - * mkOpTerm(Kind kind, uint32_t param). - */ - BITVECTOR_SIGN_EXTEND_OP, - /** - * Operator for bit-vector rotate left. - * Parameter 1: - * -[1]: Number of bits by which a given bit-vector is to be rotated + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector sign-extend. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_SIGN_EXTEND + * -[2]: Term of bit-vector sort * Create with: - * mkOpTerm(Kind kind, uint32_t param). + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_ROTATE_LEFT_OP, + BITVECTOR_SIGN_EXTEND, /** - * Operator for bit-vector rotate right. + * Operator for bit-vector rotate left. * Parameter 1: * -[1]: Number of bits by which a given bit-vector is to be rotated * Create with: - * mkOpTerm(Kind kind, uint32_t param). - */ - BITVECTOR_ROTATE_RIGHT_OP, -#if 0 - /* bit-vector boolean bit extract. - * first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term */ - BITVECTOR_BITOF, -#endif - /* Bit-vector extract. - * Parameters: 2 - * -[1]: BITVECTOR_EXTRACT_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_EXTRACT, - /* Bit-vector repeat. - * Parameters: 2 - * -[1]: BITVECTOR_REPEAT_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_REPEAT, - /* Bit-vector zero-extend. - * Parameters: 2 - * -[1]: BITVECTOR_ZERO_EXTEND_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_ZERO_EXTEND, - /* Bit-vector sign-extend. - * Parameters: 2 - * -[1]: BITVECTOR_SIGN_EXTEND_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_SIGN_EXTEND, - /* Bit-vector rotate left. + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector rotate left. * Parameters: 2 - * -[1]: BITVECTOR_ROTATE_LEFT_OP Term + * -[1]: Op of kind BITVECTOR_ROTATE_LEFT * -[2]: Term of bit-vector sort * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ BITVECTOR_ROTATE_LEFT, /** - * Bit-vector rotate right. + * Operator for bit-vector rotate right. + * Parameter 1: + * -[1]: Number of bits by which a given bit-vector is to be rotated + * Create with: + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector rotate right. * Parameters: 2 - * -[1]: BITVECTOR_ROTATE_RIGHT_OP Term + * -[1]: Op of kind BITVECTOR_ROTATE_RIGHT * -[2]: Term of bit-vector sort * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ BITVECTOR_ROTATE_RIGHT, +#if 0 + /* bit-vector boolean bit extract. */ + BITVECTOR_BITOF, +#endif /** * Operator for the conversion from Integer to bit-vector. * Parameter: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param). - */ - INT_TO_BITVECTOR_OP, - /** - * Integer conversion to bit-vector. + * mkOp(Kind kind, uint32_t param). + * + * Apply integer conversion to bit-vector. * Parameters: 2 - * -[1]: INT_TO_BITVECTOR_OP Term + * -[1]: Op of kind INT_TO_BITVECTOR * -[2]: Integer term * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ INT_TO_BITVECTOR, /** @@ -1371,17 +1354,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, - /** + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * * Conversion from an IEEE-754 bit vector to floating-point. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_IEEE_BITVECTOR * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, /** @@ -1390,17 +1371,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, - /** + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * * Conversion between floating-point sorts. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_FLOATINGPOINT * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_FLOATINGPOINT, /** @@ -1409,17 +1388,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_REAL_OP, - /** + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * * Conversion from a real to floating-point. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_REAL_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_REAL * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_REAL, /* @@ -1428,17 +1405,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, - /** + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * * Conversion from a signed bit vector to floating-point. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, /** @@ -1447,17 +1422,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, - /** - * Operator for converting an unsigned bit vector to floating-point. + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * + * Converting an unsigned bit vector to floating-point. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, /** @@ -1466,17 +1439,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_GENERIC_OP, - /** + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * * Generic conversion to floating-point, used in parsing only. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_GENERIC_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_GENERIC * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_GENERIC, /** @@ -1484,17 +1455,15 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param) - */ - FLOATINGPOINT_TO_UBV_OP, - /** + * mkOp(Kind kind, uint32_t param) + * * Conversion from a floating-point value to an unsigned bit vector. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_TO_UBV_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_UBV * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_UBV, /** @@ -1502,18 +1471,16 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param) - */ - FLOATINGPOINT_TO_UBV_TOTAL_OP, - /** + * mkOp(Kind kind, uint32_t param) + * * Conversion from a floating-point value to an unsigned bit vector * (defined for all inputs). * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_TO_UBV_TOTAL_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_UBV_TOTAL * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_UBV_TOTAL, /** @@ -1521,17 +1488,15 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param) - */ - FLOATINGPOINT_TO_SBV_OP, - /** + * mkOp(Kind kind, uint32_t param) + * * Conversion from a floating-point value to a signed bit vector. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_TO_SBV_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_SBV * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_SBV, /** @@ -1539,18 +1504,16 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param) - */ - FLOATINGPOINT_TO_SBV_TOTAL_OP, - /** + * mkOp(Kind kind, uint32_t param) + * * Conversion from a floating-point value to a signed bit vector * (defined for all inputs). * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_TO_SBV_TOTAL_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_SBV_TOTAL * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_SBV_TOTAL, /** @@ -1578,8 +1541,8 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Term of array sort * -[2]: Selection index * Create with: - * mkTerm(Term opTerm, Term child1, Term child2) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) */ SELECT, /** @@ -1589,8 +1552,8 @@ enum CVC4_PUBLIC Kind : int32_t * -[2]: Store index * -[3]: Term to store at the index * Create with: - * mkTerm(Term opTerm, Term child1, Term child2, Term child3) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2, Term child3) + * mkTerm(Op op, const std::vector<Term>& children) */ STORE, /** @@ -1599,8 +1562,8 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Array sort * -[2]: Term representing a constant * Create with: - * mkTerm(Term opTerm, Term child1, Term child2) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) * * Note: We currently support the creation of constant arrays, but under some * conditions when there is a chain of equalities connecting two constant @@ -1623,32 +1586,32 @@ enum CVC4_PUBLIC Kind : int32_t /** * Constructor application. * Paramters: n > 0 - * -[1]: Constructor (operator term) + * -[1]: Constructor (operator) * -[2]..[n]: Parameters to the constructor * Create with: - * mkTerm(Kind kind, OpTerm opTerm) - * mkTerm(Kind kind, OpTerm opTerm, Term child) - * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) - * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, OpTerm opTerm, const std::vector<Term>& children) + * mkTerm(Kind kind, Op op) + * mkTerm(Kind kind, Op op, Term child) + * mkTerm(Kind kind, Op op, Term child1, Term child2) + * mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, Op op, const std::vector<Term>& children) */ APPLY_CONSTRUCTOR, /** * Datatype selector application. * Parameters: 1 - * -[1]: Selector (operator term) + * -[1]: Selector (operator) * -[2]: Datatype term (undefined if mis-applied) * Create with: - * mkTerm(Kind kind, OpTerm opTerm, Term child) + * mkTerm(Kind kind, Op op, Term child) */ APPLY_SELECTOR, /** * Datatype selector application. * Parameters: 1 - * -[1]: Selector (operator term) + * -[1]: Selector (operator) * -[2]: Datatype term (defined rigidly if mis-applied) * Create with: - * mkTerm(Kind kind, OpTerm opTerm, Term child) + * mkTerm(Kind kind, Op op, Term child) */ APPLY_SELECTOR_TOTAL, /** @@ -1674,18 +1637,16 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Index of the tuple to be updated * Create with: - * mkOpTerm(Kind kind, uint32_t param) - */ - TUPLE_UPDATE_OP, - /** - * Tuple update. + * mkOp(Kind kind, uint32_t param) + * + * Apply tuple update. * Parameters: 3 - * -[1]: TUPLE_UPDATE_OP (which references an index) + * -[1]: Op of kind TUPLE_UPDATE (which references an index) * -[2]: Tuple * -[3]: Element to store in the tuple at the given index * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) */ TUPLE_UPDATE, /** @@ -1693,18 +1654,16 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Name of the field to be updated * Create with: - * mkOpTerm(Kind kind, const std::string& param) - */ - RECORD_UPDATE_OP, - /** + * mkOp(Kind kind, const std::string& param) + * * Record update. * Parameters: 3 - * -[1]: RECORD_UPDATE_OP Term (which references a field) + * -[1]: Op of kind RECORD_UPDATE (which references a field) * -[2]: Record term to update * -[3]: Element to store in the record in the given field * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op,, const std::vector<Term>& children) */ RECORD_UPDATE, #if 0 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 6dc29b8fe..c7e70495e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -123,23 +123,18 @@ void Smt2::addBitvectorOperators() { addOperator(kind::BITVECTOR_TO_NAT, "bv2nat"); addIndexedOperator( - kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT_OP, "extract"); + kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract"); + addIndexedOperator(kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat"); addIndexedOperator( - kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT_OP, "repeat"); - addIndexedOperator(kind::BITVECTOR_ZERO_EXTEND, - api::BITVECTOR_ZERO_EXTEND_OP, - "zero_extend"); - addIndexedOperator(kind::BITVECTOR_SIGN_EXTEND, - api::BITVECTOR_SIGN_EXTEND_OP, - "sign_extend"); - addIndexedOperator(kind::BITVECTOR_ROTATE_LEFT, - api::BITVECTOR_ROTATE_LEFT_OP, - "rotate_left"); + kind::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend"); + addIndexedOperator( + kind::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend"); + addIndexedOperator( + kind::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left"); addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT, - api::BITVECTOR_ROTATE_RIGHT_OP, + api::BITVECTOR_ROTATE_RIGHT, "rotate_right"); - addIndexedOperator( - kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR_OP, "int2bv"); + addIndexedOperator(kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv"); } void Smt2::addDatatypesOperators() @@ -234,29 +229,29 @@ void Smt2::addFloatingPointOperators() { addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real"); addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC, - api::FLOATINGPOINT_TO_FP_GENERIC_OP, + api::FLOATINGPOINT_TO_FP_GENERIC, "to_fp"); addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, - api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, + api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, "to_fp_unsigned"); addIndexedOperator( - kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV_OP, "fp.to_ubv"); + kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); addIndexedOperator( - kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV_OP, "fp.to_sbv"); + kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv"); if (!strictModeEnabled()) { addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, - api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, + api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, "to_fp_bv"); addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT, - api::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, + api::FLOATINGPOINT_TO_FP_FLOATINGPOINT, "to_fp_fp"); addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL, - api::FLOATINGPOINT_TO_FP_REAL_OP, + api::FLOATINGPOINT_TO_FP_REAL, "to_fp_real"); addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, - api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, + api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, "to_fp_signed"); } } @@ -311,7 +306,7 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::INTS_DIVISION, "div"); addOperator(kind::INTS_MODULUS, "mod"); addOperator(kind::ABS, "abs"); - addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE_OP, "divisible"); + addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE, "divisible"); break; case THEORY_REALS: @@ -549,8 +544,8 @@ api::Term Smt2::mkIndexedConstant(const std::string& name, return api::Term(); } -api::OpTerm Smt2::mkIndexedOp(const std::string& name, - const std::vector<uint64_t>& numerals) +api::Op Smt2::mkIndexedOp(const std::string& name, + const std::vector<uint64_t>& numerals) { const auto& kIt = d_indexedOpKindMap.find(name); if (kIt != d_indexedOpKindMap.end()) @@ -558,16 +553,16 @@ api::OpTerm Smt2::mkIndexedOp(const std::string& name, api::Kind k = (*kIt).second; if (numerals.size() == 1) { - return d_solver->mkOpTerm(k, numerals[0]); + return d_solver->mkOp(k, numerals[0]); } else if (numerals.size() == 2) { - return d_solver->mkOpTerm(k, numerals[0], numerals[1]); + return d_solver->mkOp(k, numerals[0], numerals[1]); } } parseError(std::string("Unknown indexed function `") + name + "'"); - return api::OpTerm(); + return api::Op(); } Expr Smt2::mkDefineFunRec( diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ec7e2071a..215f565cd 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -75,7 +75,7 @@ class Smt2 : public Parser std::unordered_map<std::string, Kind> operatorKindMap; /** * Maps indexed symbols to the kind of the operator (e.g. "extract" to - * BITVECTOR_EXTRACT_OP). + * BITVECTOR_EXTRACT). */ std::unordered_map<std::string, api::Kind> d_indexedOpKindMap; std::pair<Expr, std::string> d_lastNamedTerm; @@ -106,7 +106,7 @@ class Smt2 : public Parser * BITVECTOR_EXTRACT). NOTE: this is an internal kind for now * because that is what we use to create expressions. Eventually * it will be an api::Kind. - * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT_OP) + * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT) * @param name The name of the symbol (e.g. "extract") */ void addIndexedOperator(Kind tKind, @@ -141,8 +141,8 @@ class Smt2 : public Parser * @return The operator term corresponding to the indexed operator or a parse * error if the name is not valid. */ - api::OpTerm mkIndexedOp(const std::string& name, - const std::vector<uint64_t>& numerals); + api::Op mkIndexedOp(const std::string& name, + const std::vector<uint64_t>& numerals); /** * Returns the expression that name should be interpreted as. @@ -214,7 +214,7 @@ class Smt2 : public Parser const std::vector<Expr>& guards, const std::vector<Expr>& heads, Expr body); - + /** * Class for creating instances of `SynthFunCommand`s. Creating an instance * of this class pushes the scope, destroying it pops the scope. diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 4b5873e80..87c7fa2ce 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -35,8 +35,7 @@ namespace passes { /* -------------------------------------------------------------------------- */ -namespace -{ +namespace { void addLemmaForPair(TNode args1, TNode args2, @@ -219,7 +218,6 @@ PreprocessingPassResult Ackermann::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } - /* -------------------------------------------------------------------------- */ } // namespace passes diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index 8f27cab25..410dde8b9 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -55,8 +55,8 @@ class Ackermann : public PreprocessingPass * occurring in the input formula, add the following lemma: * (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y */ - PreprocessingPassResult applyInternal( - AssertionPipeline* assertionsToPreprocess) override; + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; private: /* Map each function to a set of terms associated with it */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 1f45d8536..555908ea2 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -95,7 +95,7 @@ static std::string maybeQuoteSymbol(const std::string& s) { if (s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz" "0123456789~!@$%^&*_-+=<>.?/") != string::npos - || s.empty()) + || s.empty() || (s[0] >= '0' && s[0] <= '9')) { // need to quote it stringstream ss; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index eb10f580a..c47506510 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2283,9 +2283,10 @@ void SmtEngine::setDefaults() { << endl; setOption("incremental", SExpr("false")); } - if (d_logic > LogicInfo("QF_AUFBVLRA")) { - throw OptionException( - "Proofs are only supported for sub-logics of QF_AUFBVLIA."); + if (d_logic > LogicInfo("QF_AUFBVLRA")) + { + throw OptionException( + "Proofs are only supported for sub-logics of QF_AUFBVLIA."); } if (options::bitvectorAlgebraicSolver()) { diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 13ab03b45..a1264c612 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -746,7 +746,9 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){ ? nm->mkNode(kind::UMINUS, nn) : nn; return RewriteResponse(REWRITE_AGAIN, ret); - }else if(dIsConstant && n.getKind() == kind::CONST_RATIONAL){ + } + else if (dIsConstant && n.getKind() == kind::CONST_RATIONAL) + { Assert(d.getConst<Rational>().isIntegral()); Assert(n.getConst<Rational>().isIntegral()); Assert(!d.getConst<Rational>().isZero()); @@ -759,7 +761,9 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){ Node resultNode = mkRationalNode(Rational(result)); return RewriteResponse(REWRITE_DONE, resultNode); - }else{ + } + else + { return RewriteResponse(REWRITE_DONE, t); } } diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 54708f6cb..e425cd345 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -41,8 +41,8 @@ void QuantDSplit::checkOwnership(Node q) { return; } - int max_index = -1; - int max_score = -1; + bool takeOwnership = false; + bool doSplit = false; Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ TypeNode tn = q[0][i].getType(); @@ -51,9 +51,9 @@ void QuantDSplit::checkOwnership(Node q) if( dt.isRecursiveSingleton( tn.toType() ) ){ Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl; }else{ - int score = -1; if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ - score = dt.isInterpretedFinite( tn.toType() ) ? 1 : 0; + // split if it is a finite datatype + doSplit = dt.isInterpretedFinite(tn.toType()); }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){ if (dt.isInterpretedFinite(tn.toType())) @@ -61,29 +61,43 @@ void QuantDSplit::checkOwnership(Node q) // split if goes from being unhandled -> handled by finite // instantiation. An example is datatypes with uninterpreted sort // fields which are "interpreted finite" but not "finite". - score = 1; + doSplit = true; + // we additionally take ownership of this formula, in other words, + // we mark it reduced. + takeOwnership = true; } else if (dt.getNumConstructors() == 1 && !dt.isCodatatype()) { // split if only one constructor - score = 1; + doSplit = true; } } } - Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl; - if( score>max_score ){ - max_index = i; - max_score = score; + if (doSplit) + { + // store the index to split + d_quant_to_reduce[q] = i; + Trace("quant-dsplit-debug") + << "Split at index " << i << " based on datatype " << dt.getName() + << std::endl; + break; } + Trace("quant-dsplit-debug") + << "Do not split based on datatype " << dt.getName() << std::endl; } } } - if( max_index!=-1 ){ - Trace("quant-dsplit-debug") << "Will split at index " << max_index << "." << std::endl; - d_quant_to_reduce[q] = max_index; + if (takeOwnership) + { + Trace("quant-dsplit-debug") << "Will take ownership." << std::endl; d_quantEngine->setOwner( q, this ); } + // Notice we may not take ownership in some cases, meaning that both the + // original quantified formula and the split one are generated. This may + // increase our ability to answer "unsat", since quantifier instantiation + // heuristics may be more effective for one or the other (see issues #993 + // and 3481). } /* whether this module needs to check this round */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 946f54650..510316ae3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -612,6 +612,7 @@ set(regress_0_tests regress0/printer/bv_consts_dec.smt2 regress0/printer/empty_symbol_name.smt2 regress0/printer/let_shadowing.smt2 + regress0/printer/symbol_starting_w_digit.smt2 regress0/printer/tuples_and_records.cvc regress0/proof_no_support.smt2 regress0/push-pop/boolean/fuzz_12.smt2 @@ -1404,6 +1405,7 @@ set(regress_1_tests regress1/quantifiers/issue3250-syg-inf-q.smt2 regress1/quantifiers/issue3316.smt2 regress1/quantifiers/issue3317.smt2 + regress1/quantifiers/issue3481.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lra-vts-inf.smt2 diff --git a/test/regress/regress0/printer/symbol_starting_w_digit.smt2 b/test/regress/regress0/printer/symbol_starting_w_digit.smt2 new file mode 100644 index 000000000..6a688a16f --- /dev/null +++ b/test/regress/regress0/printer/symbol_starting_w_digit.smt2 @@ -0,0 +1,12 @@ +; EXPECT: sat +; EXPECT: ((|0_0| (_ bv1 4))) +; EXPECT: ((x (_ bv3 4))) +(set-option :produce-models true) +(set-logic QF_BV) +(declare-const |0_0| (_ BitVec 4)) +(declare-const x (_ BitVec 4)) +(assert (= |0_0| #b0001)) +(assert (= x #b0011)) +(check-sat) +(get-value (|0_0|)) +(get-value (x)) diff --git a/test/regress/regress1/quantifiers/issue3481.smt2 b/test/regress/regress1/quantifiers/issue3481.smt2 new file mode 100644 index 000000000..47d2bcbe4 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue3481.smt2 @@ -0,0 +1,495 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat + +;; produced by cvc4_16.drv ;; +(set-info :smt-lib-version 2.6) +(set-logic AUFBVFPDTNIRA) +;;; generated by SMT-LIB2 driver +;;; SMT-LIB2 driver: bit-vectors, common part +;;; SMT-LIB2: integer arithmetic +(declare-datatypes ((tuple0 0)) +(((Tuple0)))) +(declare-sort us_private 0) + +(declare-fun private__bool_eq (us_private us_private) Bool) + +(declare-const us_null_ext__ us_private) + +(declare-sort us_type_of_heap 0) + +(declare-datatypes ((us_type_of_heap__ref 0)) +(((us_type_of_heap__refqtmk (us_type_of_heap__content us_type_of_heap))))) +(declare-sort us_image 0) + +(declare-datatypes ((int__ref 0)) +(((int__refqtmk (int__content Int))))) +(declare-datatypes ((bool__ref 0)) +(((bool__refqtmk (bool__content Bool))))) +(declare-datatypes ((us_fixed__ref 0)) +(((us_fixed__refqtmk (us_fixed__content Int))))) +(declare-datatypes ((real__ref 0)) +(((real__refqtmk (real__content Real))))) +(declare-datatypes ((us_private__ref 0)) +(((us_private__refqtmk (us_private__content us_private))))) +(define-fun int__ref___projection ((a int__ref)) Int (int__content a)) + +(define-fun us_fixed__ref___projection ((a us_fixed__ref)) Int (us_fixed__content + a)) + +(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a)) + +(define-fun real__ref___projection ((a real__ref)) Real (real__content a)) + +(define-fun us_private__ref___projection ((a us_private__ref)) us_private + (us_private__content a)) + +(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1))) + +(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool) + +(declare-sort integer 0) + +(declare-fun integerqtint (integer) Int) + + +(declare-fun attr__ATTRIBUTE_IMAGE1 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Int) + +(declare-fun user_eq (integer integer) Bool) + +(declare-const dummy integer) + +(declare-datatypes ((integer__ref 0)) +(((integer__refqtmk (integer__content integer))))) +(define-fun integer__ref_integer__content__projection ((a integer__ref)) integer + (integer__content a)) + +(define-fun to_rep ((x integer)) Int (integerqtint x)) + +(declare-fun of_rep (Int) integer) + + +(declare-sort positive 0) + +(declare-fun positiveqtint (positive) Int) + +(declare-datatypes ((positive__ref 0)) +(((positive__refqtmk (positive__content positive))))) +(define-fun positive__ref_positive__content__projection ((a positive__ref)) positive + (positive__content a)) + +(declare-datatypes ((us_split_fields 0)) +(((us_split_fieldsqtmk + (rec__test_route__point__x integer)(rec__test_route__point__y integer))))) +(define-fun us_split_fields_rec__test_route__point__x__projection ((a us_split_fields)) integer + (rec__test_route__point__x a)) + +(define-fun us_split_fields_rec__test_route__point__y__projection ((a us_split_fields)) integer + (rec__test_route__point__y a)) + +(declare-datatypes ((us_split_fields__ref 0)) +(((us_split_fields__refqtmk (us_split_fields__content us_split_fields))))) +(define-fun us_split_fields__ref___split_fields__content__projection ((a us_split_fields__ref)) us_split_fields + (us_split_fields__content a)) + +(declare-datatypes ((us_rep 0)) +(((us_repqtmk (us_split_fields1 us_split_fields))))) +(define-fun us_rep___split_fields__projection ((a us_rep)) us_split_fields + (us_split_fields1 a)) + + +(declare-const value__size Int) + +(declare-const object__size Int) + +(declare-const alignment Int) + +(declare-const test_route__point__x__first__bit Int) + +(declare-const test_route__point__x__last__bit Int) + +(declare-const test_route__point__x__position Int) + +(declare-const test_route__point__y__first__bit Int) + +(declare-const test_route__point__y__last__bit Int) + +(declare-const test_route__point__y__position Int) + +(declare-fun user_eq2 (us_rep us_rep) Bool) + +(declare-const dummy2 us_rep) + +(declare-datatypes ((point__ref 0)) +(((point__refqtmk (point__content us_rep))))) +(define-fun point__ref_point__content__projection ((a point__ref)) us_rep + (point__content a)) + +(declare-datatypes ((us_rep1 0)) +(((us_repqtmk1 + (rec__test_route__point_acc__is_null_pointer Bool)(rec__test_route__point_acc__pointer_address Int)(rec__test_route__point_acc__pointer_value us_rep))))) +(define-fun us_rep_rec__test_route__point_acc__is_null_pointer__projection ((a us_rep1)) Bool + (rec__test_route__point_acc__is_null_pointer a)) + +(define-fun us_rep_rec__test_route__point_acc__pointer_address__projection ((a us_rep1)) Int + (rec__test_route__point_acc__pointer_address a)) + +(define-fun us_rep_rec__test_route__point_acc__pointer_value__projection ((a us_rep1)) us_rep + (rec__test_route__point_acc__pointer_value a)) + +(declare-datatypes ((us_rep__ref 0)) +(((us_rep__refqtmk (us_rep__content us_rep1))))) +(define-fun us_rep__ref___rep__content__projection ((a us_rep__ref)) us_rep1 + (us_rep__content a)) + +(define-fun rec__test_route__point_acc__pointer_value__pred ((a us_rep1)) Bool + (not (= (rec__test_route__point_acc__is_null_pointer a) true))) + +(declare-const us_null_pointer us_rep1) + +;; __null_pointer__def_axiom + (assert + (= (rec__test_route__point_acc__is_null_pointer us_null_pointer) true)) + +(declare-const dummy3 us_rep1) + +(declare-datatypes ((t1b__ref 0)) +(((t1b__refqtmk (t1b__content us_rep1))))) +(define-fun t1b__ref_t1b__content__projection ((a t1b__ref)) us_rep1 + (t1b__content a)) + +(declare-sort us_main_type 0) + +(declare-datatypes ((us_rep2 0)) +(((us_repqtmk2 + (rec__test_route__route_acc__is_null_pointer Bool)(rec__test_route__route_acc__pointer_address Int)(rec__test_route__route_acc__pointer_value_abstr us_main_type))))) +(define-fun us_rep_rec__test_route__route_acc__is_null_pointer__projection ((a us_rep2)) Bool + (rec__test_route__route_acc__is_null_pointer a)) + +(define-fun us_rep_rec__test_route__route_acc__pointer_address__projection ((a us_rep2)) Int + (rec__test_route__route_acc__pointer_address a)) + +(define-fun us_rep_rec__test_route__route_acc__pointer_value_abstr__projection ((a us_rep2)) us_main_type + (rec__test_route__route_acc__pointer_value_abstr a)) + +(declare-datatypes ((us_rep__ref1 0)) +(((us_rep__refqtmk1 (us_rep__content1 us_rep2))))) +(define-fun us_rep__ref___rep__content__2__projection ((a us_rep__ref1)) us_rep2 + (us_rep__content1 a)) + + +(declare-const dummy4 us_rep2) + +(declare-datatypes ((t4b__ref 0)) +(((t4b__refqtmk (t4b__content us_rep2))))) +(define-fun t4b__ref_t4b__content__projection ((a t4b__ref)) us_rep2 + (t4b__content a)) + +(declare-fun length (us_rep2) Int) + +(declare-fun length__function_guard (Int us_rep2) Bool) + +(define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) + +(define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) + +(declare-sort natural 0) + +(declare-fun naturalqtint (natural) Int) + +(define-fun in_range3 ((x Int)) Bool (and (<= 0 x) (<= x 2147483647))) + +(declare-fun attr__ATTRIBUTE_IMAGE3 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE3 (us_image) Int) + +(declare-fun user_eq3 (natural natural) Bool) + +(declare-const dummy5 natural) + +(declare-datatypes ((natural__ref 0)) +(((natural__refqtmk (natural__content natural))))) +(define-fun natural__ref_natural__content__projection ((a natural__ref)) natural + (natural__content a)) + +(declare-const dummy6 us_rep1) + +(declare-datatypes ((point_acc__ref 0)) +(((point_acc__refqtmk (point_acc__content us_rep1))))) +(define-fun point_acc__ref_point_acc__content__projection ((a point_acc__ref)) us_rep1 + (point_acc__content a)) + +(declare-const dummy7 us_rep2) + +(declare-datatypes ((route_acc__ref 0)) +(((route_acc__refqtmk (route_acc__content us_rep2))))) +(define-fun route_acc__ref_route_acc__content__projection ((a route_acc__ref)) us_rep2 + (route_acc__content a)) + +(declare-datatypes ((us_split_fields2 0)) +(((us_split_fieldsqtmk1 + (rec__test_route__route__current us_rep1)(rec__test_route__route__rest us_rep2))))) +(define-fun us_split_fields_rec__test_route__route__current__projection ((a us_split_fields2)) us_rep1 + (rec__test_route__route__current a)) + +(define-fun us_split_fields_rec__test_route__route__rest__projection ((a us_split_fields2)) us_rep2 + (rec__test_route__route__rest a)) + +(declare-datatypes ((us_split_fields__ref1 0)) +(((us_split_fields__refqtmk1 (us_split_fields__content1 us_split_fields2))))) +(define-fun us_split_fields__ref___split_fields__content__2__projection ((a us_split_fields__ref1)) us_split_fields2 + (us_split_fields__content1 a)) + +(declare-datatypes ((us_rep3 0)) +(((us_repqtmk3 (us_split_fields3 us_split_fields2))))) +(define-fun us_rep___split_fields__2__projection ((a us_rep3)) us_split_fields2 + (us_split_fields3 a)) + +(declare-const value__size1 Int) + +(declare-const object__size1 Int) + +(declare-const alignment1 Int) + +(declare-const test_route__route__current__first__bit Int) + +(declare-const test_route__route__current__last__bit Int) + +(declare-const test_route__route__current__position Int) + + +(declare-const test_route__route__rest__first__bit Int) + +(declare-const test_route__route__rest__last__bit Int) + +(declare-const test_route__route__rest__position Int) + + +(declare-fun user_eq4 (us_rep3 us_rep3) Bool) + +(declare-const dummy8 us_rep3) + +(declare-datatypes ((route__ref 0)) +(((route__refqtmk (route__content us_rep3))))) +(define-fun route__ref_route__content__projection ((a route__ref)) us_rep3 + (route__content a)) + +(declare-fun us_open (us_main_type) us_rep3) + +(declare-fun us_close (us_rep3) us_main_type) + +(define-fun rec__test_route__route_acc__pointer_value ((a us_rep2)) us_rep3 + (us_open (rec__test_route__route_acc__pointer_value_abstr a))) + +(define-fun rec__test_route__route_acc__pointer_value__pred ((a us_rep2)) Bool + (not (= (rec__test_route__route_acc__is_null_pointer a) true))) + +(declare-const us_null_pointer1 us_rep2) + + +(declare-fun temp___dynamic_invariant_202 (us_rep2 Bool Bool Bool Bool) Bool) + + + +(declare-const dummy9 us_rep2) + +(declare-datatypes ((t5b__ref 0)) +(((t5b__refqtmk (t5b__content us_rep2))))) +(define-fun t5b__ref_t5b__content__projection ((a t5b__ref)) us_rep2 + (t5b__content a)) + +(declare-fun nth_x (us_rep2 Int) Int) + +(declare-fun nth_x__function_guard (Int us_rep2 Int) Bool) + +(declare-datatypes ((map__ref 0)) +(((map__refqtmk (map__content (Array Int integer)))))) +(declare-fun slide ((Array Int integer) Int Int) (Array Int integer)) + + +(declare-sort t 0) + +(declare-fun first (t) integer) + +(declare-fun last (t) integer) + +(declare-fun mk (Int Int) t) + +(declare-datatypes ((us_t 0)) +(((us_tqtmk (elts (Array Int integer))(rt t))))) + +(declare-const value__size2 Int) + +(declare-const object__size2 Int) + +(declare-const component__size Int) + +(declare-const alignment2 Int) + + +(declare-fun user_eq5 (us_t us_t) Bool) + +(declare-const dummy10 us_t) + +(declare-datatypes ((int_array__ref 0)) +(((int_array__refqtmk (int_array__content us_t))))) +(define-fun int_array__ref_int_array__content__projection ((a int_array__ref)) us_t + (int_array__content a)) + +(declare-const dummy11 us_rep2) + +(declare-datatypes ((t9b__ref 0)) +(((t9b__refqtmk (t9b__content us_rep2))))) +(define-fun t9b__ref_t9b__content__projection ((a t9b__ref)) us_rep2 + (t9b__content a)) + + +(declare-const dummy12 us_rep2) + +(declare-datatypes ((t21b__ref 0)) +(((t21b__refqtmk (t21b__content us_rep2))))) +(define-fun t21b__ref_t21b__content__projection ((a t21b__ref)) us_rep2 + (t21b__content a)) + +(declare-const dummy13 us_rep1) + +(declare-datatypes ((t22b__ref 0)) +(((t22b__refqtmk (t22b__content us_rep1))))) +(define-fun t22b__ref_t22b__content__projection ((a t22b__ref)) us_rep1 + (t22b__content a)) + +(declare-fun nth_point (us_rep2 Int) us_rep1) + +(declare-fun nth_point__function_guard (us_rep1 us_rep2 Int) Bool) + +(declare-sort us_pledge_ty 0) + +(declare-datatypes ((us_pledge_ty__ref 0)) +(((us_pledge_ty__refqtmk (us_pledge_ty__content us_pledge_ty))))) +(declare-fun us_pledge_get (us_pledge_ty us_rep2 us_rep1) Bool) + +(declare-fun test_route__nth_point__pledge (us_rep2 Int) us_pledge_ty) + +(declare-const r__pointer_address Int) + +(declare-const r__is_null_pointer Bool) + +(declare-const attr__ATTRIBUTE_ADDRESS Int) + +(declare-const n Int) + +(declare-const attr__ATTRIBUTE_ADDRESS1 Int) + +(declare-const s Int) + +(declare-const attr__ATTRIBUTE_ADDRESS2 Int) + +(declare-const l Int) + +(declare-const attr__ATTRIBUTE_ADDRESS3 Int) + +(declare-const dummy14 us_rep2) + +(declare-datatypes ((t29b__ref 0)) +(((t29b__refqtmk (t29b__content us_rep2))))) +(define-fun t29b__ref_t29b__content__projection ((a t29b__ref)) us_rep2 + (t29b__content a)) + +(declare-const dummy15 us_rep1) + +(declare-datatypes ((t34b__ref 0)) +(((t34b__refqtmk (t34b__content us_rep1))))) +(define-fun t34b__ref_t34b__content__projection ((a t34b__ref)) us_rep1 + (t34b__content a)) + +(declare-const attr__ATTRIBUTE_ADDRESS4 Int) + +(declare-sort us_pledge_ty1 0) + +(declare-datatypes ((us_pledge_ty__ref1 0)) +(((us_pledge_ty__refqtmk1 (us_pledge_ty__content1 us_pledge_ty1))))) +(declare-fun us_pledge_get1 (us_pledge_ty1 us_rep2 us_rep1) Bool) + + +(declare-const r__pointer_value us_split_fields2) + + +(define-fun o () us_rep2 (us_repqtmk2 r__is_null_pointer r__pointer_address + (us_close (us_repqtmk3 r__pointer_value)))) + +(define-fun test_route__shift_nth_x__l__assume () Int (length o)) + + +(define-fun o1 () Int n) + +(define-fun o2 () us_rep2 (us_repqtmk2 r__is_null_pointer r__pointer_address + (us_close (us_repqtmk3 r__pointer_value)))) + +(define-fun test_route__shift_nth_x__p__assume () us_rep1 (nth_point o2 o1)) + + + +(declare-const usf us_pledge_ty1) + + +(declare-const test_route__shift_nth_x__p__pledge us_pledge_ty1) + + +(declare-const p__pointer_value us_split_fields) + + +(declare-const p__pointer_address Int) + + +(declare-const p__is_null_pointer Bool) + + +(declare-const temp___borrowed_250 us_rep2) + +(declare-const temp___brower_249 us_rep1) + +;; H + (assert + + (forall ((temp___borrowed_236 us_rep2)) + (forall ((temp___brower_235 us_rep1)) + (=> + (and + (and + (= (us_pledge_get (test_route__nth_point__pledge o2 n) temp___borrowed_236 + temp___brower_235) true) + (not + (= (rec__test_route__point_acc__is_null_pointer temp___brower_235) true))) + (and + (= r__is_null_pointer (rec__test_route__route_acc__is_null_pointer + temp___borrowed_236)) + (= (rec__test_route__point_acc__is_null_pointer + test_route__shift_nth_x__p__assume) (rec__test_route__point_acc__is_null_pointer + temp___brower_235)))) + (= (length temp___borrowed_236) (length o2)))))) + +(assert (not (=> + (and + (and + (= (us_pledge_get (test_route__nth_point__pledge o2 n) temp___borrowed_250 + temp___brower_249) true) + (not + (= (rec__test_route__point_acc__is_null_pointer temp___brower_249) true))) + (and + (= r__is_null_pointer (rec__test_route__route_acc__is_null_pointer + temp___borrowed_250)) + (= (rec__test_route__point_acc__is_null_pointer + test_route__shift_nth_x__p__assume) (rec__test_route__point_acc__is_null_pointer + temp___brower_249)))) + (= (length temp___borrowed_250) (length o2))))) + +(check-sat) diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index ca3c59750..7566c432d 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -2,7 +2,7 @@ # Add unit tests cvc4_add_unit_test_black(datatype_api_black api) -cvc4_add_unit_test_black(opterm_black api) +cvc4_add_unit_test_black(op_black api) cvc4_add_unit_test_black(solver_black api) cvc4_add_unit_test_black(sort_black api) cvc4_add_unit_test_black(term_black api) diff --git a/test/unit/api/opterm_black.h b/test/unit/api/op_black.h index 150cebcbf..3bf9b93c3 100644 --- a/test/unit/api/opterm_black.h +++ b/test/unit/api/op_black.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file opterm_black.h +/*! \file op_black.h ** \verbatim ** Top contributors (to current version): ** Aina Niemetz @@ -18,7 +18,7 @@ using namespace CVC4::api; -class OpTermBlack : public CxxTest::TestSuite +class OpBlack : public CxxTest::TestSuite { public: void setUp() override {} @@ -27,6 +27,7 @@ class OpTermBlack : public CxxTest::TestSuite void testGetKind(); void testGetSort(); void testIsNull(); + void testOpFromKind(); void testGetIndicesString(); void testGetIndicesKind(); void testGetIndicesUint(); @@ -36,168 +37,173 @@ class OpTermBlack : public CxxTest::TestSuite Solver d_solver; }; -void OpTermBlack::testGetKind() +void OpBlack::testGetKind() { - OpTerm x; + Op x; TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&); - x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); TS_ASSERT_THROWS_NOTHING(x.getKind()); } -void OpTermBlack::testGetSort() +void OpBlack::testGetSort() { - OpTerm x; + Op x; TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&); - x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); TS_ASSERT_THROWS_NOTHING(x.getSort()); } -void OpTermBlack::testIsNull() +void OpBlack::testIsNull() { - OpTerm x; + Op x; TS_ASSERT(x.isNull()); - x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); TS_ASSERT(!x.isNull()); } -void OpTermBlack::testGetIndicesString() +void OpBlack::testOpFromKind() { - OpTerm x; + Op plus(PLUS); + TS_ASSERT(!plus.isIndexed()); + TS_ASSERT_THROWS(plus.getIndices<uint32_t>(), CVC4ApiException&); +} + +void OpBlack::testGetIndicesString() +{ + Op x; TS_ASSERT_THROWS(x.getIndices<std::string>(), CVC4ApiException&); - OpTerm divisible_ot = d_solver.mkOpTerm(DIVISIBLE_OP, 4); + Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4); + TS_ASSERT(divisible_ot.isIndexed()); std::string divisible_idx = divisible_ot.getIndices<std::string>(); TS_ASSERT(divisible_idx == "4"); - OpTerm record_update_ot = d_solver.mkOpTerm(RECORD_UPDATE_OP, "test"); + Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test"); std::string record_update_idx = record_update_ot.getIndices<std::string>(); TS_ASSERT(record_update_idx == "test"); TS_ASSERT_THROWS(record_update_ot.getIndices<uint32_t>(), CVC4ApiException&); } -void OpTermBlack::testGetIndicesKind() +void OpBlack::testGetIndicesKind() { - OpTerm chain_ot = d_solver.mkOpTerm(CHAIN_OP, AND); + Op chain_ot = d_solver.mkOp(CHAIN, AND); + TS_ASSERT(chain_ot.isIndexed()); Kind chain_idx = chain_ot.getIndices<Kind>(); TS_ASSERT(chain_idx == AND); } -void OpTermBlack::testGetIndicesUint() +void OpBlack::testGetIndicesUint() { - OpTerm bitvector_repeat_ot = d_solver.mkOpTerm(BITVECTOR_REPEAT_OP, 5); + Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); + TS_ASSERT(bitvector_repeat_ot.isIndexed()); uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices<uint32_t>(); TS_ASSERT(bitvector_repeat_idx == 5); TS_ASSERT_THROWS( (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()), CVC4ApiException&); - OpTerm bitvector_zero_extend_ot = - d_solver.mkOpTerm(BITVECTOR_ZERO_EXTEND_OP, 6); + Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); uint32_t bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIndices<uint32_t>(); TS_ASSERT(bitvector_zero_extend_idx == 6); - OpTerm bitvector_sign_extend_ot = - d_solver.mkOpTerm(BITVECTOR_SIGN_EXTEND_OP, 7); + Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7); uint32_t bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIndices<uint32_t>(); TS_ASSERT(bitvector_sign_extend_idx == 7); - OpTerm bitvector_rotate_left_ot = - d_solver.mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 8); + Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8); uint32_t bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIndices<uint32_t>(); TS_ASSERT(bitvector_rotate_left_idx == 8); - OpTerm bitvector_rotate_right_ot = - d_solver.mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 9); + Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9); uint32_t bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIndices<uint32_t>(); TS_ASSERT(bitvector_rotate_right_idx == 9); - OpTerm int_to_bitvector_ot = d_solver.mkOpTerm(INT_TO_BITVECTOR_OP, 10); + Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10); uint32_t int_to_bitvector_idx = int_to_bitvector_ot.getIndices<uint32_t>(); TS_ASSERT(int_to_bitvector_idx == 10); - OpTerm floatingpoint_to_ubv_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_OP, 11); + Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11); uint32_t floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIndices<uint32_t>(); TS_ASSERT(floatingpoint_to_ubv_idx == 11); - OpTerm floatingpoint_to_ubv_total_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_TOTAL_OP, 12); + Op floatingpoint_to_ubv_total_ot = + d_solver.mkOp(FLOATINGPOINT_TO_UBV_TOTAL, 12); uint32_t floatingpoint_to_ubv_total_idx = floatingpoint_to_ubv_total_ot.getIndices<uint32_t>(); TS_ASSERT(floatingpoint_to_ubv_total_idx == 12); - OpTerm floatingpoint_to_sbv_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_OP, 13); + Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); uint32_t floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices<uint32_t>(); TS_ASSERT(floatingpoint_to_sbv_idx == 13); - OpTerm floatingpoint_to_sbv_total_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_TOTAL_OP, 14); + Op floatingpoint_to_sbv_total_ot = + d_solver.mkOp(FLOATINGPOINT_TO_SBV_TOTAL, 14); uint32_t floatingpoint_to_sbv_total_idx = floatingpoint_to_sbv_total_ot.getIndices<uint32_t>(); TS_ASSERT(floatingpoint_to_sbv_total_idx == 14); - OpTerm tuple_update_ot = d_solver.mkOpTerm(TUPLE_UPDATE_OP, 5); + Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5); uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>(); TS_ASSERT(tuple_update_idx == 5); TS_ASSERT_THROWS(tuple_update_ot.getIndices<std::string>(), CVC4ApiException&); } -void OpTermBlack::testGetIndicesPairUint() +void OpBlack::testGetIndicesPairUint() { - OpTerm bitvector_extract_ot = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 4, 0); + Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); + TS_ASSERT(bitvector_extract_ot.isIndexed()); std::pair<uint32_t, uint32_t> bitvector_extract_indices = bitvector_extract_ot.getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0})); - OpTerm floatingpoint_to_fp_ieee_bitvector_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, 4, 25); + Op floatingpoint_to_fp_ieee_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot .getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((floatingpoint_to_fp_ieee_bitvector_indices == std::pair<uint32_t, uint32_t>{4, 25})); - OpTerm floatingpoint_to_fp_floatingpoint_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, 4, 25); + Op floatingpoint_to_fp_floatingpoint_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot .getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((floatingpoint_to_fp_floatingpoint_indices == std::pair<uint32_t, uint32_t>{4, 25})); - OpTerm floatingpoint_to_fp_real_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_REAL_OP, 4, 25); + Op floatingpoint_to_fp_real_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((floatingpoint_to_fp_real_indices == std::pair<uint32_t, uint32_t>{4, 25})); - OpTerm floatingpoint_to_fp_signed_bitvector_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, 4, 25); + Op floatingpoint_to_fp_signed_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot .getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((floatingpoint_to_fp_signed_bitvector_indices == std::pair<uint32_t, uint32_t>{4, 25})); - OpTerm floatingpoint_to_fp_unsigned_bitvector_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, 4, 25); + Op floatingpoint_to_fp_unsigned_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot .getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((floatingpoint_to_fp_unsigned_bitvector_indices == std::pair<uint32_t, uint32_t>{4, 25})); - OpTerm floatingpoint_to_fp_generic_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_GENERIC_OP, 4, 25); + Op floatingpoint_to_fp_generic_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot .getIndices<std::pair<uint32_t, uint32_t>>(); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 374a3ff2a..92313ac3c 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -40,7 +40,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkFloatingPointSort(); void testMkDatatypeSort(); void testMkFunctionSort(); - void testMkOpTerm(); + void testMkOp(); void testMkParamSort(); void testMkPredicateSort(); void testMkRecordSort(); @@ -70,7 +70,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkSepNil(); void testMkString(); void testMkTerm(); - void testMkTermFromOpTerm(); + void testMkTermFromOp(); void testMkTrue(); void testMkTuple(); void testMkUninterpretedConst(); @@ -85,6 +85,9 @@ class SolverBlack : public CxxTest::TestSuite void testDefineFunRec(); void testDefineFunsRec(); + void testUFIteration(); + void testGetOp(); + void testPush1(); void testPush2(); void testPop1(); @@ -453,29 +456,27 @@ void SolverBlack::testMkPosZero() } } -void SolverBlack::testMkOpTerm() +void SolverBlack::testMkOp() { - // mkOpTerm(Kind kind, Kind k) - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(CHAIN_OP, EQUAL)); - TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, EQUAL), - CVC4ApiException&); + // mkOp(Kind kind, Kind k) + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(CHAIN, EQUAL)); + TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException&); - // mkOpTerm(Kind kind, const std::string& arg) - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(RECORD_UPDATE_OP, "asdf")); - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, "2147483648")); - TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, "asdf"), + // mkOp(Kind kind, const std::string& arg) + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(RECORD_UPDATE, "asdf")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(DIVISIBLE, "2147483648")); + TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, "asdf"), CVC4ApiException&); - // mkOpTerm(Kind kind, uint32_t arg) - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, 1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 1)); - TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1), - CVC4ApiException&); + // mkOp(Kind kind, uint32_t arg) + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(DIVISIBLE, 1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_ROTATE_LEFT, 1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_ROTATE_RIGHT, 1)); + TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, 1), CVC4ApiException&); - // mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1, 1)); - TS_ASSERT_THROWS(d_solver->mkOpTerm(DIVISIBLE_OP, 1, 2), CVC4ApiException&); + // mkOp(Kind kind, uint32_t arg1, uint32_t arg2) + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_EXTRACT, 1, 1)); + TS_ASSERT_THROWS(d_solver->mkOp(DIVISIBLE, 1, 2), CVC4ApiException&); } void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); } @@ -611,7 +612,7 @@ void SolverBlack::testMkTerm() TS_ASSERT_THROWS(d_solver->mkTerm(DISTINCT, v6), CVC4ApiException&); } -void SolverBlack::testMkTermFromOpTerm() +void SolverBlack::testMkTermFromOp() { Sort bv32 = d_solver->mkBitVectorSort(32); Term a = d_solver->mkConst(bv32, "a"); @@ -620,9 +621,9 @@ void SolverBlack::testMkTermFromOpTerm() std::vector<Term> v2 = {d_solver->mkReal(1), Term()}; std::vector<Term> v3 = {}; // simple operator terms - OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1); - OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1); - OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL); + Op opterm1 = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1); + Op opterm2 = d_solver->mkOp(DIVISIBLE, 1); + Op opterm3 = d_solver->mkOp(CHAIN, EQUAL); // list datatype Sort sort = d_solver->mkParamSort("T"); @@ -641,80 +642,60 @@ void SolverBlack::testMkTermFromOpTerm() Term c = d_solver->mkConst(intListSort, "c"); Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - OpTerm consTerm1 = list.getConstructorTerm("cons"); - OpTerm consTerm2 = list.getConstructor("cons").getConstructorTerm(); - OpTerm nilTerm1 = list.getConstructorTerm("nil"); - OpTerm nilTerm2 = list.getConstructor("nil").getConstructorTerm(); - OpTerm headTerm1 = list["cons"].getSelectorTerm("head"); - OpTerm headTerm2 = list["cons"].getSelector("head").getSelectorTerm(); - OpTerm tailTerm1 = list["cons"].getSelectorTerm("tail"); - OpTerm tailTerm2 = list["cons"]["tail"].getSelectorTerm(); - - // mkTerm(Kind kind, OpTerm opTerm) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2)); - TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, opterm1), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1), + Op consTerm1 = list.getConstructorTerm("cons"); + Op consTerm2 = list.getConstructor("cons").getConstructorTerm(); + Op nilTerm1 = list.getConstructorTerm("nil"); + Op nilTerm2 = list.getConstructor("nil").getConstructorTerm(); + Op headTerm1 = list["cons"].getSelectorTerm("head"); + Op headTerm2 = list["cons"].getSelector("head").getSelectorTerm(); + Op tailTerm1 = list["cons"].getSelectorTerm("tail"); + Op tailTerm2 = list["cons"]["tail"].getSelectorTerm(); + + // mkTerm(Kind kind, Op op) const + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm2)); + TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(consTerm2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(headTerm1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(tailTerm2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&); + + // mkTerm(Kind kind, Op op, Term child) const + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(headTerm1, c)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(tailTerm2, c)); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1, d_solver->mkReal(0)), CVC4ApiException&); - // mkTerm(Kind kind, OpTerm opTerm, Term child) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a)); + // mkTerm(Kind kind, Op op, Term child1, Term child2) const TS_ASSERT_THROWS_NOTHING( - d_solver->mkTerm(DIVISIBLE, opterm2, d_solver->mkReal(1))); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c)); - TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm1, a), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm2, a), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, Term()), - CVC4ApiException&); - TS_ASSERT_THROWS( - d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)), - CVC4ApiException&); - - // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const + d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2))); TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( - CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(2))); - TS_ASSERT_THROWS_NOTHING( - d_solver->mkTerm(APPLY_CONSTRUCTOR, - consTerm1, - d_solver->mkReal(0), - d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); - TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b), + consTerm1, d_solver->mkReal(0), d_solver->mkTerm(nilTerm1))); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)), CVC4ApiException&); - TS_ASSERT_THROWS( - d_solver->mkTerm(CHAIN, opterm3, d_solver->mkReal(1), Term()), - CVC4ApiException&); - TS_ASSERT_THROWS( - d_solver->mkTerm(CHAIN, opterm3, Term(), d_solver->mkReal(1)), - CVC4ApiException&); - // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) + // mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3) // const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN, - opterm3, - d_solver->mkReal(1), - d_solver->mkReal(1), - d_solver->mkReal(2))); - TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b, a), - CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( + opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2))); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&); TS_ASSERT_THROWS( d_solver->mkTerm( - CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()), + opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()), CVC4ApiException&); - // mkTerm(OpTerm opTerm, const std::vector<Term>& children) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN, opterm3, v1)); - TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v3), CVC4ApiException&); + // mkTerm(Op op, const std::vector<Term>& children) const + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm3, v1)); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v3), CVC4ApiException&); } void SolverBlack::testMkTrue() @@ -916,6 +897,73 @@ void SolverBlack::testDefineFunsRec() CVC4ApiException&); } +void SolverBlack::testUFIteration() +{ + Sort intSort = d_solver->getIntegerSort(); + Sort funSort = d_solver->mkFunctionSort({intSort, intSort}, intSort); + Term x = d_solver->mkConst(intSort, "x"); + Term y = d_solver->mkConst(intSort, "y"); + Term f = d_solver->mkConst(funSort, "f"); + Term fxy = d_solver->mkTerm(APPLY_UF, f, x, y); + + // Expecting the uninterpreted function to be one of the children + Term expected_children[3] = {f, x, y}; + uint32_t idx = 0; + for (auto c : fxy) + { + TS_ASSERT(idx < 3); + TS_ASSERT(c == expected_children[idx]); + idx++; + } +} + +void SolverBlack::testGetOp() +{ + Sort bv32 = d_solver->mkBitVectorSort(32); + Term a = d_solver->mkConst(bv32, "a"); + Op ext = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1); + Term exta = d_solver->mkTerm(ext, a); + + TS_ASSERT(!a.hasOp()); + TS_ASSERT_THROWS(a.getOp(), CVC4ApiException&); + TS_ASSERT(exta.hasOp()); + TS_ASSERT_EQUALS(exta.getOp(), ext); + + // Test Datatypes -- more complicated + DatatypeDecl consListSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(head); + cons.addSelector(tail); + consListSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + consListSpec.addConstructor(nil); + Sort consListSort = d_solver->mkDatatypeSort(consListSpec); + Datatype consList = consListSort.getDatatype(); + + Op consTerm = consList.getConstructorTerm("cons"); + Op nilTerm = consList.getConstructorTerm("nil"); + Op headTerm = consList["cons"].getSelectorTerm("head"); + + TS_ASSERT(consTerm.getKind() == APPLY_CONSTRUCTOR); + TS_ASSERT(nilTerm.getKind() == APPLY_CONSTRUCTOR); + TS_ASSERT(headTerm.getKind() == APPLY_SELECTOR); + + Term listnil = d_solver->mkTerm(nilTerm); + Term listcons1 = d_solver->mkTerm(consTerm, d_solver->mkReal(1), listnil); + Term listhead = d_solver->mkTerm(headTerm, listcons1); + + TS_ASSERT(listnil.hasOp()); + TS_ASSERT_EQUALS(listnil.getOp(), nilTerm); + + TS_ASSERT(listcons1.hasOp()); + TS_ASSERT_EQUALS(listcons1.getOp(), consTerm); + + TS_ASSERT(listhead.hasOp()); + TS_ASSERT_EQUALS(listhead.getOp(), headTerm); +} + void SolverBlack::testPush1() { d_solver->setOption("incremental", "true"); @@ -1026,14 +1074,12 @@ void SolverBlack::testSimplify() TS_ASSERT(i1 == d_solver->simplify(i3)); Datatype consList = consListSort.getDatatype(); - Term dt1 = d_solver->mkTerm( - APPLY_CONSTRUCTOR, - consList.getConstructorTerm("cons"), - d_solver->mkReal(0), - d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + Term dt1 = + d_solver->mkTerm(consList.getConstructorTerm("cons"), + d_solver->mkReal(0), + d_solver->mkTerm(consList.getConstructorTerm("nil"))); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1)); - Term dt2 = d_solver->mkTerm( - APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1); + Term dt2 = d_solver->mkTerm(consList["cons"].getSelectorTerm("head"), dt1); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2)); Term b1 = d_solver->mkVar(bvSort, "b1"); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index c5300dbfe..0d5400f5f 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -207,7 +207,7 @@ void TermBlack::testAndTerm() Term b = d_solver.mkTrue(); TS_ASSERT_THROWS(Term().andTerm(b), CVC4ApiException&); - TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&); + TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.andTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&); @@ -471,7 +471,7 @@ void TermBlack::testImpTerm() Term b = d_solver.mkTrue(); TS_ASSERT_THROWS(Term().impTerm(b), CVC4ApiException&); - TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&); + TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.impTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&); @@ -538,7 +538,7 @@ void TermBlack::testIteTerm() Term b = d_solver.mkTrue(); TS_ASSERT_THROWS(Term().iteTerm(b, b), CVC4ApiException&); TS_ASSERT_THROWS(b.iteTerm(Term(), b), CVC4ApiException&); - TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&); + TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x)); |