From cd396280ff2b1a81c7c812c0b08893e72fba8b1e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 30 Mar 2022 13:06:34 -0500 Subject: [PATCH] Fix subtype issue in cegqi arithmetic (#8440) Fixes #8410. Was not properly checking for cases where an Integer variable had a Real term as its solution. --- .../cegqi/ceg_arith_instantiator.cpp | 24 +++++++++++++------ .../cegqi/ceg_arith_instantiator.h | 6 +++++ .../quantifiers/cegqi/ceg_instantiator.cpp | 2 ++ test/regress/cli/CMakeLists.txt | 1 + .../quantifiers/issue8410-vts-subtypes.smt2 | 6 +++++ 5 files changed, 32 insertions(+), 7 deletions(-) create mode 100644 test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2 diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 8c10d49aa..0b94bdc37 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -144,6 +144,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, Node alit, CegInstEffort effort) { + Trace("cegqi-arith-debug") << "Process assertion " << lit << std::endl; NodeManager* nm = NodeManager::currentNM(); Node atom = lit.getKind() == NOT ? lit[0] : lit; bool pol = lit.getKind() != NOT; @@ -828,9 +829,10 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, return CEG_TT_INVALID; } // if its type is integer but the substitution is not integer + Node vval = mkVtsSum(val, vts_coeff[0], vts_coeff[1]); if (pvtn.isInteger() && ((!veq_c.isNull() && !veq_c.getType().isInteger()) - || !val.getType().isInteger())) + || !vval.getType().isInteger())) { // redo, split integer/non-integer parts bool useCoeff = false; @@ -985,20 +987,28 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, val = rewrite(val); Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl; } + return mkVtsSum(val, inf_coeff, delta_coeff); +} + +Node ArithInstantiator::mkVtsSum(const Node& val, + const Node& inf_coeff, + const Node& delta_coeff) +{ + NodeManager* nm = NodeManager::currentNM(); + Node vval = val; if (!inf_coeff.isNull()) { Assert(!d_vts_sym[0].isNull()); - val = nm->mkNode(ADD, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0])); - val = rewrite(val); + vval = nm->mkNode(ADD, vval, nm->mkNode(MULT, inf_coeff, d_vts_sym[0])); } if (!delta_coeff.isNull()) { // create delta here if necessary - val = nm->mkNode( - ADD, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta())); - val = rewrite(val); + vval = nm->mkNode( + ADD, vval, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta())); } - return val; + vval = rewrite(vval); + return vval; } Node ArithInstantiator::negate(const Node& t) const diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index fecb85722..cf75a3e45 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -208,6 +208,12 @@ class ArithInstantiator : public Instantiator Node delta_coeff); /** Return the rewritten form of the negation of t */ Node negate(const Node& t) const; + /** + * Make the node from base value, with infinity and delta coefficients. + */ + Node mkVtsSum(const Node& val, + const Node& inf_coeff, + const Node& delta_coeff); }; } // namespace quantifiers diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 0be469ac7..f10e59540 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -146,6 +146,7 @@ void TermProperties::composeProperty(TermProperties& p) // push the substitution pv_prop.getModifiedTerm(pv) -> n void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop) { + Assert(n.getType().isSubtypeOf(pv.getType())); d_vars.push_back(pv); d_subs.push_back(n); d_props.push_back(pv_prop); @@ -938,6 +939,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv, SolvedForm& sf, bool revertOnSuccess) { + Assert(n.getType().isSubtypeOf(pv.getType())); Node cnode = pv_prop.getCacheNode(); if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){ d_curr_subs_proc[pv][n][cnode] = true; diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index ac0ec5f05..4f37e2e2e 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2213,6 +2213,7 @@ set(regress_1_tests regress1/quantifiers/issue7537-cegqi-comp-types.smt2 regress1/quantifiers/issue8157-duplicate-conflicts.smt2 regress1/quantifiers/issue8344-cegqi-string-witness.smt2 + regress1/quantifiers/issue8410-vts-subtypes.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 diff --git a/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2 b/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2 new file mode 100644 index 000000000..3a2905fd4 --- /dev/null +++ b/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: -i +; EXPECT: unsat +(set-logic ALL) +(push) +(assert (or (forall ((v Real)) (or (exists ((V Real)) (or (exists ((V Real)) (= 0 (mod (to_int v) (to_int (- v))))))))))) +(check-sat) -- 2.30.2