From 9fe8509ed935c094469a7a108d59b854aaa71b35 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 16 May 2022 17:46:41 -0500 Subject: [PATCH] Last remaining fixes for eliminating subtyping (#8772) Also fixes a debug failure for the nightlies. This also changes mkTuple to not rely on subtyping (this method should regardless be deleted from our API, as it is not the recommended way of constructing tuples). --- NEWS.md | 2 + src/api/cpp/cvc5.cpp | 47 ++++--------------- src/api/cpp/cvc5.h | 15 +----- src/expr/array_store_all.cpp | 2 +- .../arith/linear/theory_arith_private.cpp | 9 ++-- src/theory/arith/nl/ext/monomial_check.cpp | 2 +- src/theory/sets/term_registry.cpp | 13 ----- src/theory/sets/term_registry.h | 14 ------ test/unit/api/cpp/solver_black.cpp | 5 +- test/unit/api/java/SolverTest.java | 7 +-- test/unit/api/python/test_solver.py | 3 +- test/unit/theory/theory_arith_white.cpp | 3 +- test/unit/util/array_store_all_white.cpp | 7 ++- 13 files changed, 36 insertions(+), 93 deletions(-) diff --git a/NEWS.md b/NEWS.md index b9b13ae83..f2910e9e1 100644 --- a/NEWS.md +++ b/NEWS.md @@ -13,6 +13,8 @@ cvc5 1.0.1 integers and reals. Type rules for other operators like `APPLY_UF` now require their arguments to match the type of the function being applied, and do not assume integer/real subtyping. +- The API method `mkTuple` no longer supports casting integers to reals when + constructing tuples. cvc5 1.0 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 05e247fd6..1bbc1bede 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5145,38 +5145,6 @@ Term Solver::synthFunHelper(const std::string& symbol, return Term(this, fun); } -Term Solver::ensureTermSort(const Term& term, const Sort& sort) const -{ - // Note: Term and sort are checked in the caller to avoid double checks - CVC5_API_CHECK(term.getSort() == sort - || (term.getSort().isInteger() && sort.isReal())) - << "Expected conversion from Int to Real"; - //////// all checks before this line - - Sort t = term.getSort(); - if (term.getSort() == sort) - { - return term; - } - - // Integers are reals, too - Assert(t.d_type->isReal()); - Term res = term; - if (t.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. - res = Term(this, - d_nodeMgr->mkNode(extToIntKind(DIVISION), - *res.d_node, - d_nodeMgr->mkConstInt(internal::Rational(1)))); - } - Assert(res.getSort() == sort); - return res; -} - bool Solver::isValidInteger(const std::string& s) const { //////// all checks before this line @@ -6023,11 +5991,16 @@ Term Solver::mkTuple(const std::vector& sorts, << "Expected the same number of sorts and elements"; CVC5_API_SOLVER_CHECK_SORTS(sorts); CVC5_API_SOLVER_CHECK_TERMS(terms); + for (size_t i = 0, size = sorts.size(); i < size; i++) + { + CVC5_API_CHECK(terms[i].getSort() == sorts[i]) + << "Type mismatch in mkTuple"; + } //////// all checks before this line std::vector args; for (size_t i = 0, size = sorts.size(); i < size; i++) { - args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node); + args.push_back(*terms[i].d_node); } Sort s = mkTupleSortHelper(sorts); @@ -6194,7 +6167,7 @@ Term Solver::simplify(const Term& term) CVC5_API_SOLVER_CHECK_TERM(term); //////// all checks before this line Term res = Term(this, d_slv->simplify(*term.d_node)); - Assert(res.getSort().d_type->isSubtypeOf(*term.getSort().d_type)); + Assert(*res.getSort().d_type == *term.getSort().d_type); return res; //////// CVC5_API_TRY_CATCH_END; @@ -6335,7 +6308,7 @@ Term Solver::defineFun(const std::string& symbol, // SMT-LIB inputs in the Reals theory, where NUMERAL can be used to specify // reals. Instead of making our parser for numerals dependent on the logic, // we instead allow integers here in this case. - CVC5_API_CHECK(term.d_node->getType().isSubtypeOf(*sort.d_type)) + CVC5_API_CHECK(term.d_node->getType() == *sort.d_type) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; @@ -6380,7 +6353,7 @@ Term Solver::defineFunRec(const std::string& symbol, CVC5_API_SOLVER_CHECK_TERM(term); CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort); // we are permissive with subtypes, similar to defineFun - CVC5_API_CHECK(term.d_node->getType().isSubtypeOf(*sort.d_type)) + CVC5_API_CHECK(term.d_node->getType() == *sort.d_type) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; @@ -6430,7 +6403,7 @@ Term Solver::defineFunRec(const Term& fun, CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts); Sort codomain = fun.getSort().getFunctionCodomainSort(); // we are permissive with subtypes, similar to defineFun - CVC5_API_CHECK(codomain.d_type->isSubtypeOf(term.d_node->getType())) + CVC5_API_CHECK(*codomain.d_type == term.d_node->getType()) << "Invalid sort of function body '" << term << "', expected '" << codomain << "'"; } diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 975093e8d..6ad7b6a39 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3444,8 +3444,7 @@ class CVC5_EXPORT Solver Term mkTerm(const Op& op, const std::vector& children = {}) const; /** - * Create a tuple term. Terms are automatically converted if sorts are - * compatible. + * Create a tuple term, where terms have the provided sorts. * @param sorts The sorts of the elements in the tuple. * @param terms The elements in the tuple. * @return The tuple Term. @@ -5056,18 +5055,6 @@ class CVC5_EXPORT Solver /** Check whether string s is a valid decimal integer. */ bool isValidInteger(const std::string& s) const; - /** - * If needed, convert this term to a given sort. - * - * The sort of the term must be convertible into the target sort. - * Currently only Int to Real conversions are supported. - * - * @param t The term. - * @param s The target sort. - * @return The term wrapped into a sort conversion if needed. - */ - Term ensureTermSort(const Term& t, const Sort& s) const; - /** * Check that the given term is a valid closed term, which can be used as an * argument to, e.g., assert, get-value, block-model-values, etc. diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index 1d8487be0..0d027de51 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -38,7 +38,7 @@ ArrayStoreAll::ArrayStoreAll(const TypeNode& type, const Node& value) type.toString().c_str()); PrettyCheckArgument( - value.getType().isComparableTo(type.getArrayConstituentType()), + value.getType() == type.getArrayConstituentType(), value, "expr type `%s' does not match constituent type of array type `%s'", value.getType().toString().c_str(), diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp index 29bec9c28..e97b32963 100644 --- a/src/theory/arith/linear/theory_arith_private.cpp +++ b/src/theory/arith/linear/theory_arith_private.cpp @@ -974,7 +974,10 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert( // x = (p - ax - c) * -1/a // Add the substitution if not recursive Assert(elim == rewrite(elim)); - + if (elim.getType().isInteger() && !minVar.getType().isInteger()) + { + elim = NodeManager::currentNM()->mkNode(kind::TO_REAL, elim); + } if (right.size() > options().arith.ppAssertMaxSubSize) { Trace("simplify") @@ -989,10 +992,6 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert( // substitution is integral Trace("simplify") << "TheoryArithPrivate::solve(): substitution " << minVar << " |-> " << elim << endl; - if (elim.getType().isInteger() && !minVar.getType().isInteger()) - { - elim = NodeManager::currentNM()->mkNode(kind::TO_REAL, elim); - } Assert(elim.getType() == minVar.getType()); outSubstitutions.addSubstitutionSolved(minVar, elim, tin); return Theory::PP_ASSERT_STATUS_SOLVED; diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index 479b77130..f2337a629 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -720,7 +720,7 @@ void MonomialCheck::assignOrderIds(std::vector& vars, Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const { NodeManager* nm = NodeManager::currentNM(); - Assert(a.getType().isComparableTo(b.getType())); + Assert(a.getType().isRealOrInt() && b.getType().isRealOrInt()); if (status == 0) { Node a_eq_b = mkEquality(a, b); diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp index e9f2bfa99..0ea0312c4 100644 --- a/src/theory/sets/term_registry.cpp +++ b/src/theory/sets/term_registry.cpp @@ -95,19 +95,6 @@ Node TermRegistry::getUnivSet(TypeNode tn) return n; } -Node TermRegistry::getTypeConstraintSkolem(Node n, TypeNode tn) -{ - std::map::iterator it = d_tc_skolem[n].find(tn); - if (it == d_tc_skolem[n].end()) - { - SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); - Node k = sm->mkDummySkolem("tc_k", tn); - d_tc_skolem[n][tn] = k; - return k; - } - return it->second; -} - void TermRegistry::debugPrintSet(Node s, const char* c) const { if (s.getNumChildren() == 0) diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h index 1b460dc3c..d15ae401d 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -46,18 +46,6 @@ class TermRegistry : protected EnvObj InferenceManager& im, SkolemCache& skc, ProofNodeManager* pnm); - /** Get type constraint skolem - * - * The sets theory solver outputs equality lemmas of the form: - * n = d_tc_skolem[n][tn] - * where the type of d_tc_skolem[n][tn] is tn, and the type - * of n is not a subtype of tn. This is required to handle benchmarks like - * test/regress/regress0/sets/sets-of-sets-subtypes.smt2 - * where for s : (Set Int) and t : (Set Real), we have that - * ( s = t ^ y in t ) implies ( exists k : Int. y = k ) - * The type constraint Skolem for (y, Int) is the skolemization of k above. - */ - Node getTypeConstraintSkolem(Node n, TypeNode tn); /** get the proxy variable for set n * * Proxy variables are used to communicate information that otherwise would @@ -88,8 +76,6 @@ class TermRegistry : protected EnvObj NodeMap d_proxy; /** Backwards map of above */ NodeMap d_proxy_to_term; - /** Cache of type constraint skolems (see getTypeConstraintSkolem) */ - std::map > d_tc_skolem; /** Map from types to empty set of that type */ std::map d_emptyset; /** Map from types to universe set of that type */ diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index da4bef952..7ad259fdb 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -949,8 +949,9 @@ TEST_F(TestApiBlackSolver, mkTuple) { ASSERT_NO_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(3)}, {d_solver.mkBitVector(3, "101", 2)})); - ASSERT_NO_THROW( - d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkInteger("5")})); + ASSERT_THROW( + d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkInteger("5")}), + CVC5ApiException); ASSERT_THROW(d_solver.mkTuple({}, {d_solver.mkBitVector(3, "101", 2)}), CVC5ApiException); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index e70e43d0c..f9384c288 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -913,9 +913,10 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkTuple(new Sort[] {d_solver.mkBitVectorSort(3)}, new Term[] {d_solver.mkBitVector(3, "101", 2)})); - assertDoesNotThrow(() - -> d_solver.mkTuple(new Sort[] {d_solver.getRealSort()}, - new Term[] {d_solver.mkInteger("5")})); + assertThrows(CVC5ApiException.class, + () + -> d_solver.mkTuple(new Sort[] {d_solver.getRealSort()}, + new Term[] {d_solver.mkInteger("5")})); assertThrows(CVC5ApiException.class, () -> d_solver.mkTuple(new Sort[] {}, new Term[] {d_solver.mkBitVector(3, "101", 2)})); diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index a8021ff47..4e0c4bbb0 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -908,7 +908,8 @@ def test_mk_true(solver): def test_mk_tuple(solver): solver.mkTuple([solver.mkBitVectorSort(3)], [solver.mkBitVector(3, "101", 2)]) - solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")]) + with pytest.raises(RuntimeError): + solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")]) with pytest.raises(RuntimeError): solver.mkTuple([], [solver.mkBitVector(3, "101", 2)]) diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 9c5775790..981b9d3f1 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -117,9 +117,10 @@ TEST_F(TestTheoryWhiteArith, int_normal_form) ASSERT_EQ(Rewriter::rewrite(absX), absX); // (exp (+ 2 + x)) --> (* (exp x) (exp 1) (exp 1)) + Node cr0 = d_nodeManager->mkConstReal(d_zero); Node t = d_nodeManager->mkNode(EXPONENTIAL, d_nodeManager->mkNode(ADD, c2, xr)) - .eqNode(c0); + .eqNode(cr0); ASSERT_EQ(Rewriter::rewrite(Rewriter::rewrite(t)), Rewriter::rewrite(t)); } } // namespace test diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 91e3e0d26..ba1054a85 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -37,7 +37,7 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) d_nodeManager->mkConst(UninterpretedSortValue(usort, 0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->realType()), - d_nodeManager->mkConstInt(Rational(0))); + d_nodeManager->mkConstReal(Rational(0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->integerType()), d_nodeManager->mkConstInt(Rational(0))); @@ -57,6 +57,11 @@ TEST_F(TestUtilWhiteArrayStoreAll, type_errors) d_nodeManager->mkSort("U")), d_nodeManager->mkConstReal(Rational(9, 2))), IllegalArgumentException); + ASSERT_THROW(ArrayStoreAll( + d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), + d_nodeManager->realType()), + d_nodeManager->mkConstInt(Rational(0))), + IllegalArgumentException); } TEST_F(TestUtilWhiteArrayStoreAll, const_error) -- 2.30.2