From e61a7cb2c0304c28b56c569f774e3e3fedf0ce03 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 12 Apr 2022 08:58:18 -0500 Subject: [PATCH] Fix more misuses of arithmetic subtypes (#8601) --- src/theory/arith/arith_utilities.cpp | 5 +++ src/theory/arith/arith_utilities.h | 3 ++ src/theory/arith/nl/ext/proof_checker.cpp | 6 +--- src/theory/arith/nl/ext/split_zero_check.cpp | 6 ++-- .../arith/nl/ext/tangent_plane_check.cpp | 4 ++- src/theory/arith/nl/nl_model.cpp | 8 ++--- .../cegqi/ceg_arith_instantiator.cpp | 17 +++++---- .../quantifiers/cegqi/ceg_instantiator.cpp | 35 ++++++++++--------- 8 files changed, 48 insertions(+), 36 deletions(-) diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index d6bec5b9a..f20964a57 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -110,6 +110,11 @@ bool isZero(const Node& n) return n.isConst() && n.getConst().sgn() == 0; } +Node mkOne(const TypeNode& tn, bool isNeg) +{ + return NodeManager::currentNM()->mkConstRealOrInt(tn, isNeg ? -1 : 1); +} + bool isTranscendentalKind(Kind k) { // many operators are eliminated during rewriting diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index c1412257c..0f85468a2 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -228,6 +228,9 @@ Node mkZero(const TypeNode& tn); /** Is n (integer or real) zero? */ bool isZero(const Node& n); +/** Make one of the given type, maybe negated */ +Node mkOne(const TypeNode& tn, bool isNeg = false); + // Returns an node that is the identity of a select few kinds. inline Node getIdentityType(const TypeNode& tn, Kind k) { diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index 51ccd5576..cae590492 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -37,11 +37,6 @@ Node ExtProofRuleChecker::checkInternal(PfRule id, const std::vector& args) { NodeManager* nm = NodeManager::currentNM(); - auto zero = nm->mkConst(CONST_RATIONAL, 0); - auto one = nm->mkConst(CONST_RATIONAL, 1); - auto mone = nm->mkConst(CONST_RATIONAL, -1); - auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); - auto mpi = nm->mkNode(Kind::MULT, mone, pi); Trace("nl-ext-checker") << "Checking " << id << std::endl; for (const auto& c : children) { @@ -103,6 +98,7 @@ Node ExtProofRuleChecker::checkInternal(PfRule id, } } } + Node zero = nm->mkConstRealOrInt(mon.getType(), Rational(0)); switch (sign) { case -1: diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 5c97e1a18..869b0e0d6 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -17,7 +17,7 @@ #include "expr/node.h" #include "proof/proof.h" -#include "theory/arith/arith_msum.h" +#include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_model.h" @@ -29,7 +29,7 @@ namespace arith { namespace nl { SplitZeroCheck::SplitZeroCheck(Env& env, ExtState* data) - : EnvObj(env), d_data(data), d_zero_split(d_data->d_env.getUserContext()) + : EnvObj(env), d_data(data), d_zero_split(userContext()) { } @@ -40,7 +40,7 @@ void SplitZeroCheck::check() Node v = d_data->d_ms_vars[i]; if (d_zero_split.insert(v)) { - Node eq = rewrite(v.eqNode(d_data->d_zero)); + Node eq = rewrite(v.eqNode(mkZero(v.getType()))); Node lem = eq.orNode(eq.negate()); CDProof* proof = nullptr; if (d_data->isProofEnabled()) diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 8f23cb957..add09b67d 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -18,6 +18,7 @@ #include "expr/node.h" #include "proof/proof.h" #include "theory/arith/arith_msum.h" +#include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_model.h" @@ -63,7 +64,8 @@ void TangentPlaneCheck::check(bool asWaitingLemmas) for (unsigned j = 0; j < it->second.size(); j++) { Node tc = it->second[j]; - if (tc != d_data->d_one) + Node one = mkOne(tc.getType()); + if (tc != one) { Node tc_diff = d_data->d_mdb.getContainsDiffNl(tc, t); Assert(!tc_diff.isNull()); diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index e13294f10..4c97801f0 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -519,8 +519,7 @@ bool NlModel::solveEqualitySimple(Node eq, Assert(false); return false; } - Node val = nm->mkConst(CONST_RATIONAL, - -c.getConst() / b.getConst()); + Node val = nm->mkConstReal(-c.getConst() / b.getConst()); if (TraceIsOn("nl-ext-cm")) { Trace("nl-ext-cm") << "check-model-bound : exact : " << var << " = "; @@ -1086,8 +1085,9 @@ Node NlModel::getValueInternal(TNode n) // to mapping from the linear solver. This ensures that if the nonlinear // solver assumes that n = 0, then this assumption is recorded in the overall // model. - d_arithVal[n] = d_zero; - return d_zero; + Node zero = mkZero(n.getType()); + d_arithVal[n] = zero; + return zero; } bool NlModel::hasAssignment(Node v) const diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index d881fda5d..33b5f08f2 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -421,7 +421,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, MULT, nm->mkConstReal(Rational(1) / d_mbp_coeff[rr][j].getConst()), - value[t]); + nm->mkNode(TO_REAL, value[t])); value[t] = rewrite(value[t]); } // check if new best, if we have not already set it. @@ -430,15 +430,20 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, Assert(!value[t].isNull() && !best_bound_value[t].isNull()); if (value[t] != best_bound_value[t]) { - Kind k = rr == 0 ? GEQ : LEQ; - Node cmp_bound = nm->mkNode(k, value[t], best_bound_value[t]); - cmp_bound = rewrite(cmp_bound); // Should be comparing two constant values which should rewrite // to a constant. If a step failed, we assume that this is not // the new best bound. We might not be comparing constant // values (for instance if transcendental functions are - // involved), in which case we do update the best bound value. - if (!cmp_bound.isConst() || !cmp_bound.getConst()) + // involved), in which case we do not update the best bound value. + if (!value[t].isConst() || !best_bound_value[t].isConst()) + { + new_best = false; + break; + } + Rational rt = value[t].getConst(); + Rational brt = best_bound_value[t].getConst(); + bool cmp = rr == 0 ? rt >= brt : rt <= brt; + if (!cmp) { new_best = false; break; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index ac0aca893..f09faf22f 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1146,6 +1146,7 @@ bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& no Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) { + NodeManager* nm = NodeManager::currentNM(); n = rewrite(n); computeProgVars( n ); bool is_basic = canApplyBasicSubstitution( n, non_basic ); @@ -1216,31 +1217,31 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node pv_prop.d_coeff = rewrite(pv_prop.d_coeff); Trace("sygus-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl; std::vector< Node > children; + TypeNode type = n.getType(); for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - Node c_coeff; - if( !msum_coeff[it->first].isNull() ){ - c_coeff = rewrite(NodeManager::currentNM()->mkConstReal( - pv_prop.d_coeff.getConst() - / msum_coeff[it->first].getConst())); - }else{ - c_coeff = pv_prop.d_coeff; + Rational c_coeff = pv_prop.d_coeff.getConst(); + Node mc = msum_coeff[it->first]; + if (!mc.isNull()) + { + Assert(mc.isConst()); + c_coeff = c_coeff / mc.getConst(); } if( !it->second.isNull() ){ - c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); + Assert(it->second.isConst()); + c_coeff = c_coeff * it->second.getConst(); } - Assert(!c_coeff.isNull()); - Node c; - if( msum_term[it->first].isNull() ){ - c = c_coeff; - }else{ - c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); + Node c = nm->mkConstRealOrInt(type, c_coeff); + Node v = msum_term[it->first]; + if (!v.isNull()) + { + Assert(v.getType() == type); + c = nm->mkNode(MULT, c, v); } children.push_back( c ); Trace("sygus-si-apply-subs-debug") << "Add child : " << c << std::endl; } - Node nretc = children.size() == 1 - ? children[0] - : NodeManager::currentNM()->mkNode(ADD, children); + Node nretc = + children.size() == 1 ? children[0] : nm->mkNode(ADD, children); nretc = rewrite(nretc); //ensure that nret does not contain vars if (!expr::hasSubterm(nretc, vars)) -- 2.30.2