diff options
45 files changed, 355 insertions, 257 deletions
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index 191bb83bd..307c30709 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -58,8 +58,8 @@ int main() Term p = slv.mkConst(intPred, "p"); // Constants - Term zero = slv.mkReal(0); - Term one = slv.mkReal(1); + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); // Terms Term f_x = slv.mkTerm(APPLY_UF, f, x); diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index 00c0b9810..d9d3c9e9c 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -39,7 +39,7 @@ void test(Solver& slv, Sort& consListSort) Term t = slv.mkTerm( APPLY_CONSTRUCTOR, consList.getConstructorTerm("cons"), - slv.mkReal(0), + slv.mkInteger(0), slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); std::cout << "t is " << t << std::endl @@ -124,7 +124,7 @@ void test(Solver& slv, Sort& consListSort) << "sort of cons is " << paramConsList.getConstructorTerm("cons").getSort() << std::endl << std::endl; - Term assertion = slv.mkTerm(GT, head_a, slv.mkReal(50)); + Term assertion = slv.mkTerm(GT, head_a, slv.mkInteger(50)); std::cout << "Assert " << assertion << std::endl; slv.assertFormula(assertion); std::cout << "Expect sat." << std::endl; diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index 2d6636d0f..2e70460af 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -39,8 +39,8 @@ int main() Term y = slv.mkConst(real, "y"); // Constants - Term three = slv.mkReal(3); - Term neg2 = slv.mkReal(-2); + Term three = slv.mkInteger(3); + Term neg2 = slv.mkInteger(-2); Term two_thirds = slv.mkReal(2, 3); // Terms diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index 253365c9d..ed3fe0be5 100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -46,8 +46,8 @@ if __name__ == "__main__": p = slv.mkConst(intPred, "p") # Constants - zero = slv.mkReal(0) - one = slv.mkReal(1) + zero = slv.mkInteger(0) + one = slv.mkInteger(1) # Terms f_x = slv.mkTerm(kinds.ApplyUf, f, x) diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index 8ae2c29fd..6eef4478d 100644 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -33,7 +33,7 @@ def test(slv, consListSort): # "nil" is a constructor too t = slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("cons"), - slv.mkReal(0), + slv.mkInteger(0), slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil"))) print("t is {}\nsort of cons is {}\n sort of nil is {}".format( @@ -82,7 +82,7 @@ def test(slv, consListSort): print("head_a is {} of sort {}".format(head_a, head_a.getSort())) print("sort of cons is", paramConsList.getConstructorTerm("cons").getSort()) - assertion = slv.mkTerm(kinds.Gt, head_a, slv.mkReal(50)) + assertion = slv.mkTerm(kinds.Gt, head_a, slv.mkInteger(50)) print("Assert", assertion) slv.assertFormula(assertion) print("Expect sat.") diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index f85171150..94ce730a3 100644 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -33,8 +33,8 @@ if __name__ == "__main__": y = slv.mkConst(real, "y") # Constants - three = slv.mkReal(3) - neg2 = slv.mkReal(-2) + three = slv.mkInteger(3) + neg2 = slv.mkInteger(-2) two_thirds = slv.mkReal(2, 3) # Terms diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py index 1b0c34f44..7ed5448cd 100644 --- a/examples/api/python/sequences.py +++ b/examples/api/python/sequences.py @@ -42,9 +42,9 @@ if __name__ == "__main__": # Sequence length: |x.y.empty| concat_len = slv.mkTerm(kinds.SeqLength, concat) # |x.y.empty| > 1 - formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkReal(1)) + formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkInteger(1)) # Sequence unit: seq(1) - unit = slv.mkTerm(kinds.SeqUnit, slv.mkReal(1)) + unit = slv.mkTerm(kinds.SeqUnit, slv.mkInteger(1)) # x = seq(1) formula2 = slv.mkTerm(kinds.Equal, x, unit) diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index 67d9808e7..77de3e5b3 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -62,9 +62,9 @@ if __name__ == "__main__": # Find me an element in 1, 2 intersection 2, 3, if there is one. - one = slv.mkReal(1) - two = slv.mkReal(2) - three = slv.mkReal(3) + one = slv.mkInteger(1) + two = slv.mkInteger(2) + three = slv.mkInteger(3) singleton_one = slv.mkSingleton(integer, one) singleton_two = slv.mkSingleton(integer, two) diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py index c007b4bb5..1e85c56bb 100644 --- a/examples/api/python/strings.py +++ b/examples/api/python/strings.py @@ -51,7 +51,7 @@ if __name__ == "__main__": # Length of y: |y| leny = slv.mkTerm(kinds.StringLength, y) # |y| >= 0 - formula2 = slv.mkTerm(kinds.Geq, leny, slv.mkReal(0)) + formula2 = slv.mkTerm(kinds.Geq, leny, slv.mkInteger(0)) # Regular expression: (ab[c-e]*f)|g|h r = slv.mkTerm(kinds.RegexpUnion, diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index d331c9f9e..a85902961 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -41,8 +41,8 @@ if __name__ == "__main__": start_bool = slv.mkVar(boolean, "StartBool") # define the rules - zero = slv.mkReal(0) - one = slv.mkReal(1) + zero = slv.mkInteger(0) + one = slv.mkInteger(1) plus = slv.mkTerm(kinds.Plus, start, start) minus = slv.mkTerm(kinds.Minus, start, start) diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index 7a8f89c68..cfa342f35 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -38,7 +38,7 @@ if __name__ == "__main__": start = slv.mkVar(integer, "Start") # define the rules - zero = slv.mkReal(0) + zero = slv.mkInteger(0) neg_x = slv.mkTerm(kinds.Uminus, x) plus = slv.mkTerm(kinds.Plus, x, start) diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py index f71091371..4e7465382 100644 --- a/examples/api/python/sygus-inv.py +++ b/examples/api/python/sygus-inv.py @@ -30,9 +30,9 @@ if __name__ == "__main__": integer = slv.getIntegerSort() boolean = slv.getBooleanSort() - zero = slv.mkReal(0) - one = slv.mkReal(1) - ten = slv.mkReal(10) + zero = slv.mkInteger(0) + one = slv.mkInteger(1) + ten = slv.mkInteger(10) # declare input variables for functions x = slv.mkVar(integer, "x") diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp index 3783d35c4..63d5aac96 100644 --- a/examples/api/sequences.cpp +++ b/examples/api/sequences.cpp @@ -47,9 +47,9 @@ int main() // Sequence length: |x.y.empty| Term concat_len = slv.mkTerm(SEQ_LENGTH, concat); // |x.y.empty| > 1 - Term formula1 = slv.mkTerm(GT, concat_len, slv.mkReal(1)); + Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1)); // Sequence unit: seq(1) - Term unit = slv.mkTerm(SEQ_UNIT, slv.mkReal(1)); + Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1)); // x = seq(1) Term formula2 = slv.mkTerm(EQUAL, x, unit); diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index fd85858a2..549b68e0d 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -69,9 +69,9 @@ int main() // Find me an element in {1, 2} intersection {2, 3}, if there is one. { - Term one = slv.mkReal(1); - Term two = slv.mkReal(2); - Term three = slv.mkReal(3); + Term one = slv.mkInteger(1); + Term two = slv.mkInteger(2); + Term three = slv.mkInteger(3); Term singleton_one = slv.mkSingleton(integer, one); Term singleton_two = slv.mkSingleton(integer, two); diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index ad8df9ffa..556c49c8e 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -56,7 +56,7 @@ int main() // Length of y: |y| Term leny = slv.mkTerm(STRING_LENGTH, y); // |y| >= 0 - Term formula2 = slv.mkTerm(GEQ, leny, slv.mkReal(0)); + Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0)); // Regular expression: (ab[c-e]*f)|g|h Term r = slv.mkTerm(REGEXP_UNION, diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp index b85529554..b2d6e9215 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/sygus-fun.cpp @@ -74,8 +74,8 @@ int main() Term start_bool = slv.mkVar(boolean, "StartBool"); // define the rules - Term zero = slv.mkReal(0); - Term one = slv.mkReal(1); + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); Term plus = slv.mkTerm(PLUS, start, start); Term minus = slv.mkTerm(MINUS, start, start); diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp index 4cfbe84fa..ea8256c70 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/sygus-grammar.cpp @@ -69,7 +69,7 @@ int main() Term start = slv.mkVar(integer, "Start"); // define the rules - Term zero = slv.mkReal(0); + Term zero = slv.mkInteger(0); Term neg_x = slv.mkTerm(UMINUS, x); Term plus = slv.mkTerm(PLUS, x, start); diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp index 710265113..d57d9be4e 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/sygus-inv.cpp @@ -53,9 +53,9 @@ int main() Sort integer = slv.getIntegerSort(); Sort boolean = slv.getBooleanSort(); - Term zero = slv.mkReal(0); - Term one = slv.mkReal(1); - Term ten = slv.mkReal(10); + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); + Term ten = slv.mkInteger(10); // declare input variables for functions Term x = slv.mkVar(integer, "x"); diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 49a4f576e..e648b9994 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -32,16 +32,16 @@ int main() { Term x = slv.mkConst(integer, "x"); Term y = slv.mkConst(integer, "y"); - Term zero = slv.mkReal(0); + Term zero = slv.mkInteger(0); Term x_positive = slv.mkTerm(Kind::GT, x, zero); Term y_positive = slv.mkTerm(Kind::GT, y, zero); - Term two = slv.mkReal(2); + Term two = slv.mkInteger(2); Term twox = slv.mkTerm(Kind::MULT, two, x); Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y); - Term three = slv.mkReal(3); + Term three = slv.mkInteger(3); Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three); Term formula = diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 7596b4771..538cb359f 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -40,7 +40,7 @@ int main() { std::cout << "Made expression : " << quantpospx << std::endl; //make ~P( 5 ) - Term five = slv.mkReal(5); + Term five = slv.mkInteger(5); Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five); Term negpfive = slv.mkTerm(Kind::NOT, pfive); std::cout << "Made expression : " << negpfive << std::endl; diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index be82a517f..507e270bb 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -34,6 +34,7 @@ #include "api/cvc4cpp.h" #include <cstring> +#include <regex> #include <sstream> #include "base/check.h" @@ -1603,7 +1604,7 @@ Kind Term::getKindHelper() const // (string) versions back to sequence. All operators where this is // necessary are such that their first child is of sequence type, which // we check here. - if (getNumChildren() > 0 && (*this)[0].getSort().isSequence()) + if (d_node->getNumChildren() > 0 && (*d_node)[0].getType().isSequence()) { switch (d_node->getKind()) { @@ -1626,9 +1627,22 @@ Kind Term::getKindHelper() const } // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to // INTERNAL_KIND. + if(isCastedReal()) + { + return CONST_RATIONAL; + } return intToExtKind(d_node->getKind()); } +bool Term::isCastedReal() const +{ + if(d_node->getKind() == kind::CAST_TO_REAL) + { + return (*d_node)[0].isConst() && (*d_node)[0].getType().isInteger(); + } + return false; +} + bool Term::operator==(const Term& t) const { return *d_node == *t.d_node; } bool Term::operator!=(const Term& t) const { return *d_node != *t.d_node; } @@ -1649,12 +1663,20 @@ size_t Term::getNumChildren() const { return d_node->getNumChildren() + 1; } + if(isCastedReal()) + { + return 0; + } return d_node->getNumChildren(); } Term Term::operator[](size_t index) const { CVC4_API_CHECK_NOT_NULL; + + // check the index within the number of children + CVC4_API_CHECK(index < getNumChildren()) << "index out of bound"; + // special cases for apply kinds if (isApplyKind(d_node->getKind())) { @@ -1763,12 +1785,6 @@ Op Term::getOp() const bool Term::isNull() const { return isNullHelper(); } -bool Term::isValue() const -{ - CVC4_API_CHECK_NOT_NULL; - return d_node->isConst(); -} - Term Term::getConstArrayBase() const { CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager())); @@ -3109,16 +3125,20 @@ Term Solver::mkValHelper(T t) const Term Solver::mkRealFromStrHelper(const std::string& s) const { - /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP - * throws an std::invalid_argument exception. For consistency, we treat it - * as invalid. */ - CVC4_API_ARG_CHECK_EXPECTED(s != ".", s) - << "a string representing an integer, real or rational value."; - - CVC4::Rational r = s.find('/') != std::string::npos - ? CVC4::Rational(s) - : CVC4::Rational::fromDecimal(s); - return mkValHelper<CVC4::Rational>(r); + try + { + CVC4::Rational r = s.find('/') != std::string::npos + ? CVC4::Rational(s) + : CVC4::Rational::fromDecimal(s); + return mkValHelper<CVC4::Rational>(r); + } + catch (const std::invalid_argument& e) + { + std::stringstream message; + message << "Cannot construct Real or Int from string argument '" << s << "'" + << std::endl; + throw std::invalid_argument(message.str()); + } } Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const @@ -3725,24 +3745,66 @@ Term Solver::mkPi() const CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::mkInteger(const std::string& s) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(std::regex_match(s, std::regex("-?\\d+")), s) + << " an integer "; + Term integer = mkRealFromStrHelper(s); + CVC4_API_ARG_CHECK_EXPECTED(integer.getSort() == getIntegerSort(), s) + << " an integer"; + return integer; + CVC4_API_SOLVER_TRY_CATCH_END; +} + +Term Solver::mkInteger(int64_t val) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + Term integer = mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + Assert(integer.getSort() == getIntegerSort()); + return integer; + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term Solver::mkReal(const std::string& s) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkRealFromStrHelper(s); + /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP + * throws an std::invalid_argument exception. For consistency, we treat it + * as invalid. */ + CVC4_API_ARG_CHECK_EXPECTED(s != ".", s) + << "a string representing a real or rational value."; + Term rational = mkRealFromStrHelper(s); + return ensureRealSort(rational); CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::ensureRealSort(const Term t) const +{ + CVC4_API_ARG_CHECK_EXPECTED( + t.getSort() == getIntegerSort() || t.getSort() == getRealSort(), + " an integer or real term"); + if (t.getSort() == getIntegerSort()) + { + Node n = getNodeManager()->mkNode(kind::CAST_TO_REAL, *t.d_node); + return Term(this, n); + } + return t; +} + Term Solver::mkReal(int64_t val) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + return ensureRealSort(rational); CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::mkReal(int64_t num, int64_t den) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); + Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); + return ensureRealSort(rational); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3918,10 +3980,17 @@ Term Solver::mkConstArray(Sort sort, Term val) const CVC4_API_SOLVER_CHECK_SORT(sort); CVC4_API_SOLVER_CHECK_TERM(val); CVC4_API_CHECK(sort.isArray()) << "Not an array sort."; - CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort())) + CVC4_API_CHECK(val.getSort().isSubsortOf(sort.getArrayElementSort())) << "Value does not match element sort."; - Term res = mkValHelper<CVC4::ArrayStoreAll>(CVC4::ArrayStoreAll( - TypeNode::fromType(*sort.d_type), Node::fromExpr(val.d_node->toExpr()))); + // handle the special case of (CAST_TO_REAL n) where n is an integer + Node n = *val.d_node; + if (val.isCastedReal()) + { + // this is safe because the constant array stores its type + n = n[0]; + } + Term res = mkValHelper<CVC4::ArrayStoreAll>( + CVC4::ArrayStoreAll(TypeNode::fromType(*sort.d_type), n)); return res; CVC4_API_SOLVER_TRY_CATCH_END; } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 646695c64..c05390e42 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -982,13 +982,6 @@ class CVC4_PUBLIC Term bool isNull() const; /** - * Check if this is a Term representing a value. - * - * @return true if this is a Term representing a value - */ - bool isValue() const; - - /** * Return the base (element stored at all indices) of a constant array * throws an exception if the kind is not CONST_ARRAY * @return the base value @@ -1176,6 +1169,11 @@ class CVC4_PUBLIC Term Kind getKindHelper() const; /** + * returns true if the current term is a constant integer that is casted into + * real using the operator CAST_TO_REAL, and returns false otherwise + */ + bool isCastedReal() 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 @@ -2580,12 +2578,26 @@ class CVC4_PUBLIC Solver * @return a constant representing Pi */ Term mkPi() const; + /** + * Create an integer constant from a string. + * @param s the string representation of the constant, may represent an + * integer (e.g., "123"). + * @return a constant of sort Integer assuming 's' represents an integer) + */ + Term mkInteger(const std::string& s) const; + + /** + * Create an integer constant from a c++ int. + * @param val the value of the constant + * @return a constant of sort Integer + */ + Term mkInteger(int64_t val) const; /** * Create a real constant from a string. * @param s the string representation of the constant, may represent an * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34"). - * @return a constant of sort Real or Integer (if 's' represents an integer) + * @return a constant of sort Real */ Term mkReal(const std::string& s) const; @@ -2600,7 +2612,7 @@ class CVC4_PUBLIC Solver * Create a real constant from a rational. * @param num the value of the numerator * @param den the value of the denominator - * @return a constant of sort Real or Integer (if 'num' is divisible by 'den') + * @return a constant of sort Real */ Term mkReal(int64_t num, int64_t den) const; @@ -3461,10 +3473,10 @@ class CVC4_PUBLIC Solver /** * Helper function that ensures that a given term is of sort real (as opposed * to being of sort integer). - * @param term a term of sort integer or real + * @param t a term of sort integer or real * @return a term of sort real */ - Term ensureRealSort(Term expr) const; + Term ensureRealSort(Term t) const; /** * Create n-ary term of given kind. This handles the cases of left/right diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 73ccde14a..113895ad7 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -173,6 +173,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Term mkFalse() except + Term mkBoolean(bint val) except + Term mkPi() except + + Term mkInteger(const string& s) except + Term mkReal(const string& s) except + Term mkRegexpEmpty() except + Term mkRegexpSigma() except + @@ -329,7 +330,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": bint hasOp() except + Op getOp() except + bint isNull() except + - bint isValue() except + Term getConstArrayBase() except + vector[Term] getConstSequenceElements() except + Term notTerm() except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 188b678d1..4cdd60893 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -664,6 +664,12 @@ cdef class Solver: term.cterm = self.csolver.mkPi() return term + def mkInteger(self, val): + cdef Term term = Term(self) + integer = int(val) + term.cterm = self.csolver.mkInteger("{}".format(integer).encode()) + return term + def mkReal(self, val, den=None): cdef Term term = Term(self) if den is None: @@ -1448,9 +1454,6 @@ cdef class Term: def isNull(self): return self.cterm.isNull() - def isValue(self): - return self.cterm.isValue() - def getConstArrayBase(self): cdef Term term = Term(self.solver) term.cterm = self.cterm.getConstArrayBase() @@ -1502,7 +1505,6 @@ cdef class Term: def toPythonObj(self): ''' Converts a constant value Term to a Python object. - Requires isValue to hold. Currently supports: Boolean -- returns a Python bool @@ -1514,9 +1516,6 @@ cdef class Term: String -- returns a Python Unicode string ''' - if not self.isValue(): - raise RuntimeError("Cannot call toPythonObj on a non-const Term") - string_repr = self.cterm.toString().decode() assert string_repr sort = self.getSort() diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index 92383dcd1..ed21f8f9c 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -45,7 +45,8 @@ ArrayStoreAll::ArrayStoreAll(const TypeNode& type, const Node& value) "expr type `%s' does not match constituent type of array type `%s'", value.getType().toString().c_str(), type.toString().c_str()); - + Trace("arrays") << "constructing constant array of type: '" << type + << "' and value: '" << value << "'" << std::endl; PrettyCheckArgument( value.isConst(), value, "ArrayStoreAll requires a constant expression"); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 292871d2a..0bb41b483 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2177,13 +2177,6 @@ simpleTerm[CVC4::api::Term& f] * literals, we can use the push/pop scope. */ /* PARSER_STATE->popScope(); */ t = SOLVER->mkArraySort(t, t2); - if(!f.isValue()) { - std::stringstream ss; - ss << "expected constant term inside array constant, but found " - << "nonconstant term" << std::endl - << "the term: " << f; - PARSER_STATE->parseError(ss.str()); - } if(!t2.isComparableTo(f.getSort())) { std::stringstream ss; ss << "type mismatch inside array constant term:" << std::endl @@ -2207,18 +2200,12 @@ simpleTerm[CVC4::api::Term& f] std::stringstream strRat; strRat << r; f = SOLVER->mkReal(strRat.str()); - if(f.getSort().isInteger()) { - // Must cast to Real to ensure correct type is passed to parametric type constructors. - // We do this cast using division with 1. - // This has the advantage wrt using TO_REAL since (constant) division is always included in the theory. - f = MK_TERM(api::DIVISION, f, SOLVER->mkReal(1)); - } } | INTEGER_LITERAL { Rational r = AntlrInput::tokenToRational($INTEGER_LITERAL); std::stringstream strRat; strRat << r; - f = SOLVER->mkReal(strRat.str()); + f = SOLVER->mkInteger(strRat.str()); } /* bitvector literals */ | HEX_LITERAL diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7c1c5dc3e..7647f8e53 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1710,7 +1710,7 @@ identifier[CVC4::ParseOp& p] // we adopt a special syntax (_ tupSel n) p.d_kind = api::APPLY_SELECTOR; // put m in expr so that the caller can deal with this case - p.d_expr = SOLVER->mkReal(AntlrInput::tokenToUnsigned($m)); + p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m)); } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { @@ -1735,7 +1735,7 @@ termAtomic[CVC4::api::Term& atomTerm] : INTEGER_LITERAL { std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL); - atomTerm = SOLVER->mkReal(intStr); + atomTerm = SOLVER->mkInteger(intStr); } | DECIMAL_LITERAL { @@ -1830,7 +1830,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] { std::stringstream sIntLit; sIntLit << $INTEGER_LITERAL; - api::Term n = SOLVER->mkReal(sIntLit.str()); + api::Term n = SOLVER->mkInteger(sIntLit.str()); std::vector<api::Term> values; values.push_back( n ); std::string attr_name(AntlrInput::tokenText($tok)); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 629164593..edeb47f06 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1055,33 +1055,22 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) parseError("Too many arguments to array constant."); } api::Term constVal = args[0]; - if (!constVal.isValue()) + + // To parse array constants taking reals whose values are specified by + // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle + // the fact that (/ 1 3) is the division of constants 1 and 3, and not + // the resulting constant rational value. Thus, we must construct the + // resulting rational here. This also is applied for integral real values + // like 5.0 which are converted to (/ 5 1) to distinguish them from + // integer constants. We must ensure numerator and denominator are + // constant and the denominator is non-zero. + if (constVal.getKind() == api::DIVISION) { - // To parse array constants taking reals whose values are specified by - // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle - // the fact that (/ 1 3) is the division of constants 1 and 3, and not - // the resulting constant rational value. Thus, we must construct the - // resulting rational here. This also is applied for integral real values - // like 5.0 which are converted to (/ 5 1) to distinguish them from - // integer constants. We must ensure numerator and denominator are - // constant and the denominator is non-zero. - if (constVal.getKind() == api::DIVISION && constVal[0].isValue() - && constVal[1].isValue() - && !constVal[1].getExpr().getConst<Rational>().isZero()) - { - std::stringstream sdiv; - sdiv << constVal[0] << "/" << constVal[1]; - constVal = d_solver->mkReal(sdiv.str()); - } - if (!constVal.isValue()) - { - std::stringstream ss; - ss << "expected constant term inside array constant, but found " - << "nonconstant term:" << std::endl - << "the term: " << constVal; - parseError(ss.str()); - } + std::stringstream sdiv; + sdiv << constVal[0] << "/" << constVal[1]; + constVal = d_solver->mkReal(sdiv.str()); } + if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort())) { std::stringstream ss; diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index b99376685..8e29c25f1 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -477,7 +477,7 @@ definedPred[CVC4::ParseOp& p] api::Term body = MK_TERM(api::AND, MK_TERM(api::NOT, - MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))), + MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))), MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr))); api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r); body = MK_TERM(api::EXISTS, bvl, body); @@ -537,7 +537,7 @@ thfDefinedPred[CVC4::ParseOp& p] api::Term body = MK_TERM( api::AND, MK_TERM(api::NOT, - MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))), + MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))), MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr))); api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r); body = MK_TERM(api::EXISTS, bvl, body); @@ -708,7 +708,7 @@ definedFun[CVC4::ParseOp& p] n, SOLVER->mkReal(2)), SOLVER->mkReal(1, 2))), - SOLVER->mkReal(2)))); + SOLVER->mkInteger(2)))); p.d_kind = api::LAMBDA; p.d_expr = MK_TERM(api::LAMBDA, formals, expr); } @@ -1747,7 +1747,15 @@ NUMBER : ( SIGN[pos]? num=DECIMAL { std::stringstream ss; ss << ( pos ? "" : "-" ) << AntlrInput::tokenText($num); - PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str()); + std::string str = ss.str(); + if (str.find(".") == std::string::npos) + { + PARSER_STATE->d_tmp_expr = SOLVER->mkInteger(str); + } + else + { + PARSER_STATE->d_tmp_expr = SOLVER->mkReal(str); + } } | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)? { diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index bab619dce..9ccf02301 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -644,6 +644,8 @@ void CvcPrinter::toStream( opType = PREFIX; break; case kind::TO_REAL: + case kind::CAST_TO_REAL: + { if (n[0].getKind() == kind::CONST_RATIONAL) { // print the constant as a rational @@ -655,6 +657,7 @@ void CvcPrinter::toStream( toStream(out, n[0], depth, types, false); } return; + } case kind::DIVISIBLE: out << "DIVISIBLE("; toStream(out, n[0], depth, types, false); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8815f9632..a0cd8cf9c 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -477,10 +477,10 @@ void Smt2Printer::toStream(std::ostream& out, bool typeChildren = false; // operators (op t1...tn) where at least one of t1...tn may require a type cast e.g. Int -> Real // operator Kind k = n.getKind(); - if(n.getNumChildren() != 0 && - k != kind::INST_PATTERN_LIST && - k != kind::APPLY_TYPE_ASCRIPTION && - k != kind::CONSTRUCTOR_TYPE) { + if (n.getNumChildren() != 0 && k != kind::INST_PATTERN_LIST + && k != kind::APPLY_TYPE_ASCRIPTION && k != kind::CONSTRUCTOR_TYPE + && k != kind::CAST_TO_REAL) + { out << '('; } switch(k) { @@ -603,11 +603,17 @@ void Smt2Printer::toStream(std::ostream& out, case kind::ABS: case kind::IS_INTEGER: case kind::TO_INTEGER: - case kind::TO_REAL: case kind::POW: parametricTypeChildren = true; out << smtKindString(k, d_variant) << " "; break; + case kind::TO_REAL: + case kind::CAST_TO_REAL: + { + // (to_real 5) is printed as 5.0 + out << n[0] << ".0"; + return; + } case kind::IAND: out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") "; stillNeedToPrintParams = false; @@ -1029,7 +1035,8 @@ void Smt2Printer::toStream(std::ostream& out, } } } - if(n.getNumChildren() != 0) { + if (n.getNumChildren() != 0) + { out << parens.str() << ')'; } }/* Smt2Printer::toStream(TNode) */ diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index dc91d678e..a65fbd961 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -138,7 +138,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::TO_INTEGER: return RewriteResponse(REWRITE_DONE, t); case kind::TO_REAL: - return RewriteResponse(REWRITE_DONE, t[0]); + case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]); case kind::POW: return RewriteResponse(REWRITE_DONE, t); case kind::PI: @@ -198,7 +198,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ } return RewriteResponse(REWRITE_DONE, t); case kind::TO_REAL: - return RewriteResponse(REWRITE_DONE, t[0]); + case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]); case kind::TO_INTEGER: if(t[0].isConst()) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(t[0].getConst<Rational>().floor()))); diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index e563d8f66..fc8f76ee4 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -80,9 +80,16 @@ operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" operator GEQ 2 "greater than or equal, x >= y" -operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" -operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)" -operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)" +operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" +operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)" +operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)" + +# CAST_TO_REAL is added to distinguish between integers casted to reals internally, and +# integers casted to reals or using the API \ +# Solver::mkReal(int val) would return an internal node (CAST_TO_REAL val), but in the api it appears as term (val) \ +# Solver::mkTerm(TO_REAL, Solver::mkInteger(int val)) would return both term and node (TO_REAL val) \ +# This way, we avoid having 2 nested TO_REAL nodess as a result of Solver::mkTerm(TO_REAL, Solver::mkReal(int val)) +operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API" typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule @@ -99,9 +106,10 @@ typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>" typerule GT "SimpleTypeRule<RBool, AReal, AReal>" typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>" -typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule -typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule -typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>" +typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule +typerule CAST_TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule +typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule +typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>" typerule ABS "SimpleTypeRule<RInteger, AInteger>" typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>" diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 9dd18d84b..0aa9cd4b3 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -60,12 +60,13 @@ public: } } } - switch(Kind k = n.getKind()) { + switch (Kind k = n.getKind()) + { case kind::TO_REAL: - return realType; - case kind::TO_INTEGER: - return integerType; - default: { + case kind::CAST_TO_REAL: return realType; + case kind::TO_INTEGER: return integerType; + default: + { bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL; return (isInteger && !isDivision ? integerType : realType); } diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp index 73629a0d0..2168d053e 100644 --- a/test/api/reset_assertions.cpp +++ b/test/api/reset_assertions.cpp @@ -31,7 +31,7 @@ int main() Sort real = slv.getRealSort(); Term x = slv.mkConst(real, "x"); - Term four = slv.mkReal(4); + Term four = slv.mkInteger(4); Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four); slv.assertFormula(xEqFour); std::cout << slv.checkSat() << std::endl; @@ -43,7 +43,7 @@ int main() Sort arrayType = slv.mkArraySort(indexType, elementType); Term array = slv.mkConst(arrayType, "array"); Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four); - Term ten = slv.mkReal(10); + Term ten = slv.mkInteger(10); Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten); slv.assertFormula(arrayAtFour_eq_ten); std::cout << slv.checkSat() << std::endl; diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp index f0a55cf79..1b1efb07e 100644 --- a/test/api/sep_log_api.cpp +++ b/test/api/sep_log_api.cpp @@ -135,10 +135,10 @@ int validate_getters(void) Sort integer = slv.getIntegerSort(); /* A "random" constant */ - Term random_constant = slv.mkReal(0xDEADBEEF); + Term random_constant = slv.mkInteger(0xDEADBEEF); /* Another random constant */ - Term expr_nil_val = slv.mkReal(0xFBADBEEF); + Term expr_nil_val = slv.mkInteger(0xFBADBEEF); /* Our nil term */ Term nil = slv.mkSepNil(integer); diff --git a/test/regress/regress0/get-value-reals-ints.smt2 b/test/regress/regress0/get-value-reals-ints.smt2 index b75f535d5..c8d3bb348 100644 --- a/test/regress/regress0/get-value-reals-ints.smt2 +++ b/test/regress/regress0/get-value-reals-ints.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2) 1)) (neg_int (- 6))) +; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3.0 1.0)) (pos_rat (/ 1 3)) (zero (/ 0.0 1.0)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2.0) 1.0)) (neg_int (- 6))) (set-info :smt-lib-version 2.0) (set-option :produce-models true) (set-logic QF_LIRA) diff --git a/test/regress/regress0/get-value-reals.smt2 b/test/regress/regress0/get-value-reals.smt2 index 09ec0917f..d27581114 100644 --- a/test/regress/regress0/get-value-reals.smt2 +++ b/test/regress/regress0/get-value-reals.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -; EXPECT: ((pos_int (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2) 1))) +; EXPECT: ((pos_int (/ 3.0 1.0)) (pos_rat (/ 1 3)) (zero (/ 0.0 1.0)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2.0) 1.0))) (set-info :smt-lib-version 2.0) (set-option :produce-models true) (set-logic QF_LRA) diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h index bf0d97e9d..afbd09d0f 100644 --- a/test/unit/api/grammar_black.h +++ b/test/unit/api/grammar_black.h @@ -57,7 +57,7 @@ void GrammarBlack::testAddRule() TS_ASSERT_THROWS(g.addRule(start, nullTerm), CVC4ApiException&); TS_ASSERT_THROWS(g.addRule(nts, d_solver->mkBoolean(false)), CVC4ApiException&); - TS_ASSERT_THROWS(g.addRule(start, d_solver->mkReal(0)), CVC4ApiException&); + TS_ASSERT_THROWS(g.addRule(start, d_solver->mkInteger(0)), CVC4ApiException&); d_solver->synthFun("f", {}, boolean, g); @@ -83,7 +83,7 @@ void GrammarBlack::testAddRules() TS_ASSERT_THROWS(g.addRules(start, {nullTerm}), CVC4ApiException&); TS_ASSERT_THROWS(g.addRules(nts, {d_solver->mkBoolean(false)}), CVC4ApiException&); - TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkReal(0)}), CVC4ApiException&); + TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkInteger(0)}), CVC4ApiException&); d_solver->synthFun("f", {}, boolean, g); diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py index 0321f03d0..5a0d5101f 100644 --- a/test/unit/api/python/test_grammar.py +++ b/test/unit/api/python/test_grammar.py @@ -38,7 +38,7 @@ def test_add_rule(): with pytest.raises(Exception): g.addRule(nts, solver.mkBoolean(false)) with pytest.raises(Exception): - g.addRule(start, solver.mkReal(0)) + g.addRule(start, solver.mkInteger(0)) # expecting no errors solver.synthFun("f", {}, boolean, g) @@ -68,7 +68,7 @@ def test_add_rules(): with pytest.raises(Exception): g.addRules(nts, {solver.mkBoolean(False)}) with pytest.raises(Exception): - g.addRules(start, {solver.mkReal(0)}) + g.addRules(start, {solver.mkInteger(0)}) #Expecting no errors solver.synthFun("f", {}, boolean, g) diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 9c25b584f..a0c1b4681 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -103,26 +103,12 @@ def test_get_op(): assert fx.getOp() == solver.mkOp(kinds.ApplyUf) -def test_is_const(): - solver = pycvc4.Solver() - intsort = solver.getIntegerSort() - one = solver.mkReal(1) - x = solver.mkConst(intsort, 'x') - xpone = solver.mkTerm(kinds.Plus, x, one) - onepone = solver.mkTerm(kinds.Plus, one, one) - assert not x.isValue() - assert one.isValue() - assert not xpone.isValue() - assert not onepone.isValue() - def test_const_sequence_elements(): solver = pycvc4.Solver() realsort = solver.getRealSort() seqsort = solver.mkSequenceSort(realsort) s = solver.mkEmptySequence(seqsort) - assert s.isValue() - assert s.getKind() == kinds.ConstSequence # empty sequence has zero elements cs = s.getConstSequenceElements() diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py index 3ce08f6b8..eb15e7469 100644 --- a/test/unit/api/python/test_to_python_obj.py +++ b/test/unit/api/python/test_to_python_obj.py @@ -15,7 +15,7 @@ def testGetBool(): def testGetInt(): solver = pycvc4.Solver() - two = solver.mkReal(2) + two = solver.mkInteger(2) assert two.toPythonObj() == 2 @@ -27,7 +27,7 @@ def testGetReal(): neg34 = solver.mkReal("-3/4") assert neg34.toPythonObj() == Fraction(-3, 4) - neg1 = solver.mkReal("-1") + neg1 = solver.mkInteger("-1") assert neg1.toPythonObj() == -1 @@ -40,12 +40,10 @@ def testGetBV(): def testGetArray(): solver = pycvc4.Solver() arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) - zero_array = solver.mkConstArray(arrsort, solver.mkReal(0)) - stores = solver.mkTerm(kinds.Store, zero_array, solver.mkReal(1), solver.mkReal(2)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2), solver.mkReal(3)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4), solver.mkReal(5)) - - assert stores.isValue() + zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0)) + stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(2), solver.mkInteger(3)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(4), solver.mkInteger(5)) array_dict = stores.toPythonObj() @@ -58,10 +56,7 @@ def testGetArray(): def testGetSymbol(): solver = pycvc4.Solver() - x = solver.mkConst(solver.getBooleanSort(), "x") - - with pytest.raises(RuntimeError): - x.toPythonObj() + solver.mkConst(solver.getBooleanSort(), "x") def testGetString(): diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 8b8c6dd58..1324e3890 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -72,6 +72,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkPi(); void testMkPosInf(); void testMkPosZero(); + void testMkInteger(); void testMkReal(); void testMkRegexpEmpty(); void testMkRegexpSigma(); @@ -598,7 +599,7 @@ void SolverBlack::testMkFloatingPoint() { Term t1 = d_solver->mkBitVector(8); Term t2 = d_solver->mkBitVector(4); - Term t3 = d_solver->mkReal(2); + Term t3 = d_solver->mkInteger(2); if (CVC4::Configuration::isBuiltWithSymFPU()) { TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPoint(3, 5, t1)); @@ -742,6 +743,47 @@ void SolverBlack::testMkOp() void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); } +void SolverBlack::testMkInteger() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger("123")); + TS_ASSERT_THROWS(d_solver->mkInteger("1.23"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger("1/23"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger("12/3"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(".2"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger("2."), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(""), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger("asdf"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger("1.2/3"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger("."), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger("/"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger("2/"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger("/2"), CVC4ApiException&); + + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("123"))); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1.23")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1/23")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string("12/3")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string(".2")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string("2.")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string("")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string("asdf")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1.2/3")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string(".")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string("/")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string("2/")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkInteger(std::string("/2")), CVC4ApiException&); + + int32_t val1 = 1; + int64_t val2 = -1; + uint32_t val3 = 1; + uint64_t val4 = -1; + TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val2)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val3)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val4)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val4)); +} + void SolverBlack::testMkReal() { TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("123")); @@ -839,8 +881,8 @@ void SolverBlack::testMkTerm() std::vector<Term> v1 = {a, b}; std::vector<Term> v2 = {a, Term()}; std::vector<Term> v3 = {a, d_solver->mkTrue()}; - std::vector<Term> v4 = {d_solver->mkReal(1), d_solver->mkReal(2)}; - std::vector<Term> v5 = {d_solver->mkReal(1), Term()}; + std::vector<Term> v4 = {d_solver->mkInteger(1), d_solver->mkInteger(2)}; + std::vector<Term> v5 = {d_solver->mkInteger(1), Term()}; std::vector<Term> v6 = {}; Solver slv; @@ -896,10 +938,10 @@ void SolverBlack::testMkTermFromOp() Sort bv32 = d_solver->mkBitVectorSort(32); Term a = d_solver->mkConst(bv32, "a"); Term b = d_solver->mkConst(bv32, "b"); - std::vector<Term> v1 = {d_solver->mkReal(1), d_solver->mkReal(2)}; - std::vector<Term> v2 = {d_solver->mkReal(1), Term()}; + std::vector<Term> v1 = {d_solver->mkInteger(1), d_solver->mkInteger(2)}; + std::vector<Term> v2 = {d_solver->mkInteger(1), Term()}; std::vector<Term> v3 = {}; - std::vector<Term> v4 = {d_solver->mkReal(5)}; + std::vector<Term> v4 = {d_solver->mkInteger(5)}; Solver slv; // simple operator terms @@ -948,13 +990,13 @@ void SolverBlack::testMkTermFromOp() // mkTerm(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(opterm2, d_solver->mkInteger(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(opterm2, a), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&); TS_ASSERT_THROWS( - d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)), + d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkInteger(0)), CVC4ApiException&); TS_ASSERT_THROWS(slv.mkTerm(opterm1, a), CVC4ApiException&); @@ -962,19 +1004,19 @@ void SolverBlack::testMkTermFromOp() TS_ASSERT_THROWS_NOTHING( d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, - d_solver->mkReal(0), + d_solver->mkInteger(0), d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); TS_ASSERT_THROWS( - d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)), + d_solver->mkTerm(opterm2, d_solver->mkInteger(1), d_solver->mkInteger(2)), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkReal(1), Term()), + TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkInteger(1), Term()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkReal(1)), + TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkInteger(1)), CVC4ApiException&); TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR, consTerm1, - d_solver->mkReal(0), + d_solver->mkInteger(0), d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)), CVC4ApiException&); @@ -982,7 +1024,7 @@ void SolverBlack::testMkTermFromOp() TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&); TS_ASSERT_THROWS( d_solver->mkTerm( - opterm2, d_solver->mkReal(1), d_solver->mkReal(1), Term()), + opterm2, d_solver->mkInteger(1), d_solver->mkInteger(1), Term()), CVC4ApiException&); // mkTerm(Op op, const std::vector<Term>& children) const @@ -1004,7 +1046,7 @@ void SolverBlack::testMkTuple() TS_ASSERT_THROWS_NOTHING(d_solver->mkTuple( {d_solver->mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)})); TS_ASSERT_THROWS_NOTHING( - d_solver->mkTuple({d_solver->getRealSort()}, {d_solver->mkReal("5")})); + d_solver->mkTuple({d_solver->getRealSort()}, {d_solver->mkInteger("5")})); TS_ASSERT_THROWS(d_solver->mkTuple({}, {d_solver->mkBitVector("101", 2)}), CVC4ApiException&); @@ -1054,7 +1096,7 @@ void SolverBlack::testMkConstArray() { Sort intSort = d_solver->getIntegerSort(); Sort arrSort = d_solver->mkArraySort(intSort, intSort); - Term zero = d_solver->mkReal(0); + Term zero = d_solver->mkInteger(0); Term constArr = d_solver->mkConstArray(arrSort, zero); TS_ASSERT_THROWS_NOTHING(d_solver->mkConstArray(arrSort, zero)); @@ -1064,7 +1106,7 @@ void SolverBlack::testMkConstArray() CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkConstArray(intSort, zero), CVC4ApiException&); Solver slv; - Term zero2 = slv.mkReal(0); + Term zero2 = slv.mkInteger(0); Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort()); TS_ASSERT_THROWS(slv.mkConstArray(arrSort2, zero), CVC4ApiException&); TS_ASSERT_THROWS(slv.mkConstArray(arrSort, zero2), CVC4ApiException&); @@ -1454,7 +1496,7 @@ void SolverBlack::testGetOp() Term listnil = d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm); Term listcons1 = d_solver->mkTerm( - APPLY_CONSTRUCTOR, consTerm, d_solver->mkReal(1), listnil); + APPLY_CONSTRUCTOR, consTerm, d_solver->mkInteger(1), listnil); Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1); TS_ASSERT(listnil.hasOp()); @@ -1542,8 +1584,8 @@ void SolverBlack::testGetUnsatCore3() Term y = d_solver->mkConst(uSort, "y"); Term f = d_solver->mkConst(uToIntSort, "f"); Term p = d_solver->mkConst(intPredSort, "p"); - Term zero = d_solver->mkReal(0); - Term one = d_solver->mkReal(1); + Term zero = d_solver->mkInteger(0); + Term one = d_solver->mkInteger(1); Term f_x = d_solver->mkTerm(APPLY_UF, f, x); Term f_y = d_solver->mkTerm(APPLY_UF, f, y); Term sum = d_solver->mkTerm(PLUS, f_x, f_y); @@ -1601,8 +1643,8 @@ void SolverBlack::testGetValue3() Term z = d_solver->mkConst(uSort, "z"); Term f = d_solver->mkConst(uToIntSort, "f"); Term p = d_solver->mkConst(intPredSort, "p"); - Term zero = d_solver->mkReal(0); - Term one = d_solver->mkReal(1); + Term zero = d_solver->mkInteger(0); + Term one = d_solver->mkInteger(1); Term f_x = d_solver->mkTerm(APPLY_UF, f, x); Term f_y = d_solver->mkTerm(APPLY_UF, f, y); Term sum = d_solver->mkTerm(PLUS, f_x, f_y); @@ -1985,11 +2027,11 @@ void SolverBlack::testSimplify() Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1"); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1)); - Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkReal("23")); + Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkInteger("23")); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i2)); TS_ASSERT(i1 != i2); TS_ASSERT(i1 != d_solver->simplify(i2)); - Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkReal(0)); + Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkInteger(0)); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i3)); TS_ASSERT(i1 != i3); TS_ASSERT(i1 == d_solver->simplify(i3)); @@ -1998,7 +2040,7 @@ void SolverBlack::testSimplify() Term dt1 = d_solver->mkTerm( APPLY_CONSTRUCTOR, consList.getConstructorTerm("cons"), - d_solver->mkReal(0), + d_solver->mkInteger(0), d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1)); Term dt2 = d_solver->mkTerm( @@ -2075,8 +2117,8 @@ void SolverBlack::testCheckEntailed2() Term f = d_solver->mkConst(uToIntSort, "f"); Term p = d_solver->mkConst(intPredSort, "p"); // Values - Term zero = d_solver->mkReal(0); - Term one = d_solver->mkReal(1); + Term zero = d_solver->mkInteger(0); + Term one = d_solver->mkInteger(1); // Terms Term f_x = d_solver->mkTerm(APPLY_UF, f, x); Term f_y = d_solver->mkTerm(APPLY_UF, f, y); @@ -2158,8 +2200,8 @@ void SolverBlack::testCheckSatAssuming2() Term f = d_solver->mkConst(uToIntSort, "f"); Term p = d_solver->mkConst(intPredSort, "p"); // Values - Term zero = d_solver->mkReal(0); - Term one = d_solver->mkReal(1); + Term zero = d_solver->mkInteger(0); + Term one = d_solver->mkInteger(1); // Terms Term f_x = d_solver->mkTerm(APPLY_UF, f, x); Term f_y = d_solver->mkTerm(APPLY_UF, f, y); @@ -2279,7 +2321,7 @@ void SolverBlack::testSynthFun() g1.addRule(start1, d_solver->mkBoolean(false)); Grammar g2 = d_solver->mkSygusGrammar({x}, {start2}); - g2.addRule(start2, d_solver->mkReal(0)); + g2.addRule(start2, d_solver->mkInteger(0)); TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("", {}, boolean)); TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("f1", {x}, boolean)); @@ -2314,7 +2356,7 @@ void SolverBlack::testSynthInv() g1.addRule(start1, d_solver->mkBoolean(false)); Grammar g2 = d_solver->mkSygusGrammar({x}, {start2}); - g2.addRule(start2, d_solver->mkReal(0)); + g2.addRule(start2, d_solver->mkInteger(0)); TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("", {})); TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("i1", {x})); @@ -2328,7 +2370,7 @@ void SolverBlack::testAddSygusConstraint() { Term nullTerm; Term boolTerm = d_solver->mkBoolean(true); - Term intTerm = d_solver->mkReal(1); + Term intTerm = d_solver->mkInteger(1); TS_ASSERT_THROWS_NOTHING(d_solver->addSygusConstraint(boolTerm)); TS_ASSERT_THROWS(d_solver->addSygusConstraint(nullTerm), CVC4ApiException&); @@ -2344,7 +2386,7 @@ void SolverBlack::testAddSygusInvConstraint() Sort real = d_solver->getRealSort(); Term nullTerm; - Term intTerm = d_solver->mkReal(1); + Term intTerm = d_solver->mkInteger(1); Term inv = d_solver->declareFun("inv", {real}, boolean); Term pre = d_solver->declareFun("pre", {real}, boolean); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index 786b60bb3..bebfc6e1f 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -42,7 +42,6 @@ class TermBlack : public CxxTest::TestSuite void testTermCompare(); void testTermChildren(); void testSubstitute(); - void testIsValue(); void testConstArray(); void testConstSequenceElements(); @@ -100,7 +99,7 @@ void TermBlack::testGetKind() Term p = d_solver.mkVar(funSort2, "p"); TS_ASSERT_THROWS_NOTHING(p.getKind()); - Term zero = d_solver.mkReal(0); + Term zero = d_solver.mkInteger(0); TS_ASSERT_THROWS_NOTHING(zero.getKind()); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); @@ -146,7 +145,7 @@ void TermBlack::testGetSort() TS_ASSERT_THROWS_NOTHING(p.getSort()); TS_ASSERT(p.getSort() == funSort2); - Term zero = d_solver.mkReal(0); + Term zero = d_solver.mkInteger(0); TS_ASSERT_THROWS_NOTHING(zero.getSort()); TS_ASSERT(zero.getSort() == intSort); @@ -227,7 +226,7 @@ void TermBlack::testGetOp() Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm); Term consTerm = d_solver.mkTerm( - APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkReal(0), nilTerm); + APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm); Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm); Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm); @@ -272,7 +271,7 @@ void TermBlack::testNotTerm() TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&); Term p = d_solver.mkVar(funSort2, "p"); TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&); - Term zero = d_solver.mkReal(0); + Term zero = d_solver.mkInteger(0); TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); TS_ASSERT_THROWS(f_x.notTerm(), CVC4ApiException&); @@ -308,7 +307,7 @@ void TermBlack::testAndTerm() TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&); TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&); TS_ASSERT_THROWS(p.andTerm(p), CVC4ApiException&); - Term zero = d_solver.mkReal(0); + Term zero = d_solver.mkInteger(0); TS_ASSERT_THROWS(zero.andTerm(b), CVC4ApiException&); TS_ASSERT_THROWS(zero.andTerm(x), CVC4ApiException&); TS_ASSERT_THROWS(zero.andTerm(f), CVC4ApiException&); @@ -374,7 +373,7 @@ void TermBlack::testOrTerm() TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&); TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&); TS_ASSERT_THROWS(p.orTerm(p), CVC4ApiException&); - Term zero = d_solver.mkReal(0); + Term zero = d_solver.mkInteger(0); TS_ASSERT_THROWS(zero.orTerm(b), CVC4ApiException&); TS_ASSERT_THROWS(zero.orTerm(x), CVC4ApiException&); TS_ASSERT_THROWS(zero.orTerm(f), CVC4ApiException&); @@ -440,7 +439,7 @@ void TermBlack::testXorTerm() TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&); TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&); TS_ASSERT_THROWS(p.xorTerm(p), CVC4ApiException&); - Term zero = d_solver.mkReal(0); + Term zero = d_solver.mkInteger(0); TS_ASSERT_THROWS(zero.xorTerm(b), CVC4ApiException&); TS_ASSERT_THROWS(zero.xorTerm(x), CVC4ApiException&); TS_ASSERT_THROWS(zero.xorTerm(f), CVC4ApiException&); @@ -506,7 +505,7 @@ void TermBlack::testEqTerm() TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&); TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(p.eqTerm(p)); - Term zero = d_solver.mkReal(0); + Term zero = d_solver.mkInteger(0); TS_ASSERT_THROWS(zero.eqTerm(b), CVC4ApiException&); TS_ASSERT_THROWS(zero.eqTerm(x), CVC4ApiException&); TS_ASSERT_THROWS(zero.eqTerm(f), CVC4ApiException&); @@ -572,7 +571,7 @@ void TermBlack::testImpTerm() TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&); TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&); TS_ASSERT_THROWS(p.impTerm(p), CVC4ApiException&); - Term zero = d_solver.mkReal(0); + Term zero = d_solver.mkInteger(0); TS_ASSERT_THROWS(zero.impTerm(b), CVC4ApiException&); TS_ASSERT_THROWS(zero.impTerm(x), CVC4ApiException&); TS_ASSERT_THROWS(zero.impTerm(f), CVC4ApiException&); @@ -639,7 +638,7 @@ void TermBlack::testIteTerm() Term p = d_solver.mkVar(funSort2, "p"); TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&); TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&); - Term zero = d_solver.mkReal(0); + Term zero = d_solver.mkInteger(0); TS_ASSERT_THROWS(zero.iteTerm(x, x), CVC4ApiException&); TS_ASSERT_THROWS(zero.iteTerm(x, b), CVC4ApiException&); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); @@ -660,17 +659,17 @@ void TermBlack::testIteTerm() void TermBlack::testTermAssignment() { - Term t1 = d_solver.mkReal(1); + Term t1 = d_solver.mkInteger(1); Term t2 = t1; - t2 = d_solver.mkReal(2); - TS_ASSERT_EQUALS(t1, d_solver.mkReal(1)); + t2 = d_solver.mkInteger(2); + TS_ASSERT_EQUALS(t1, d_solver.mkInteger(1)); } void TermBlack::testTermCompare() { - Term t1 = d_solver.mkReal(1); - Term t2 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2)); - Term t3 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2)); + Term t1 = d_solver.mkInteger(1); + Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2)); + Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2)); TS_ASSERT(t2 >= t3); TS_ASSERT(t2 <= t3); TS_ASSERT((t1 > t2) != (t1 < t2)); @@ -680,8 +679,8 @@ void TermBlack::testTermCompare() void TermBlack::testTermChildren() { // simple term 2+3 - Term two = d_solver.mkReal(2); - Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkReal(3)); + Term two = d_solver.mkInteger(2); + Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3)); TS_ASSERT(t1[0] == two); TS_ASSERT(t1.getNumChildren() == 2); Term tnull; @@ -702,7 +701,7 @@ void TermBlack::testTermChildren() void TermBlack::testSubstitute() { Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); - Term one = d_solver.mkReal(1); + Term one = d_solver.mkInteger(1); Term ttrue = d_solver.mkTrue(); Term xpx = d_solver.mkTerm(PLUS, x, x); Term onepone = d_solver.mkTerm(PLUS, one, one); @@ -750,34 +749,27 @@ void TermBlack::testSubstitute() TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&); } -void TermBlack::testIsValue() -{ - Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); - Term one = d_solver.mkReal(1); - Term xpone = d_solver.mkTerm(PLUS, x, one); - Term onepone = d_solver.mkTerm(PLUS, one, one); - TS_ASSERT(!x.isValue()); - TS_ASSERT(one.isValue()); - TS_ASSERT(!xpone.isValue()); - TS_ASSERT(!onepone.isValue()); - Term tnull; - TS_ASSERT_THROWS(tnull.isValue(), CVC4ApiException&); -} - void TermBlack::testConstArray() { Sort intsort = d_solver.getIntegerSort(); Sort arrsort = d_solver.mkArraySort(intsort, intsort); Term a = d_solver.mkConst(arrsort, "a"); - Term one = d_solver.mkReal(1); + Term one = d_solver.mkInteger(1); Term constarr = d_solver.mkConstArray(arrsort, one); - TS_ASSERT(!a.isValue()); - TS_ASSERT(constarr.isValue()); - TS_ASSERT_EQUALS(constarr.getKind(), CONST_ARRAY); TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one); TS_ASSERT_THROWS(a.getConstArrayBase(), CVC4ApiException&); + + arrsort = + d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort()); + Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0)); + Term stores = d_solver.mkTerm( + STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2)); + stores = + d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3)); + stores = + d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5)); } void TermBlack::testConstSequenceElements() @@ -786,7 +778,6 @@ void TermBlack::testConstSequenceElements() Sort seqsort = d_solver.mkSequenceSort(realsort); Term s = d_solver.mkEmptySequence(seqsort); - TS_ASSERT(s.isValue()); TS_ASSERT_EQUALS(s.getKind(), CONST_SEQUENCE); // empty sequence has zero elements diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h index c098ca9b8..f06c1f77d 100644 --- a/test/unit/theory/theory_sets_type_rules_white.h +++ b/test/unit/theory/theory_sets_type_rules_white.h @@ -56,7 +56,7 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite Sort realSort = d_slv->getRealSort(); Sort intSort = d_slv->getIntegerSort(); Term emptyReal = d_slv->mkEmptySet(d_slv->mkSetSort(realSort)); - Term one = d_slv->mkReal(1); + Term one = d_slv->mkInteger(1); Term singletonInt = d_slv->mkSingleton(intSort, one); Term singletonReal = d_slv->mkSingleton(realSort, one); // (union |