From: Andrew Reynolds Date: Thu, 5 May 2022 19:13:41 +0000 (-0500) Subject: Preparation for making equality strictly typed (#8728) X-Git-Tag: cvc5-1.0.1~164 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3266c58ad0ad1c1e3b04a69ceb1caf2a468597db;p=cvc5.git Preparation for making equality strictly typed (#8728) This changes several places in arithmetic so that it never generates equalities between and an Int and a Real. It also changes several uses of mkConstReal on integer values with mkConstInt whenever their type does not matter. Since we do not construct CONST_INTEGER yet, this PR has no behavior change yet. --- diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index c149ef6a5..202cb1292 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -1088,9 +1088,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, TNode scalar = args[i]; bool isPos = scalar.getConst() > 0; Node scalarCmp = - nm->mkNode(isPos ? GT : LT, - scalar, - nm->mkConstRealOrInt(scalar.getType(), Rational(0))); + nm->mkNode(isPos ? GT : LT, scalar, nm->mkConstInt(Rational(0))); // (= scalarCmp true) Node scalarCmpOrTrue = steps.tryStep(PfRule::EVALUATE, {}, {scalarCmp}); Assert(!scalarCmpOrTrue.isNull()); diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index f96374127..6d3499611 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -185,24 +185,24 @@ int ArithMSum::isolate( children.push_back(m); } } - val = - children.size() > 1 - ? nm->mkNode(ADD, children) - : (children.size() == 1 ? children[0] - : nm->mkConstRealOrInt(vtn, Rational(0))); + val = children.size() > 1 + ? nm->mkNode(ADD, children) + : (children.size() == 1 ? children[0] + : nm->mkConstInt(Rational(0))); if (!r.isOne() && !r.isNegativeOne()) { if (vtn.isInteger()) { - veq_c = nm->mkConstReal(r.abs()); + veq_c = nm->mkConstRealOrInt(r.abs()); } else { - val = nm->mkNode(MULT, val, nm->mkConstReal(Rational(1) / r.abs())); + val = nm->mkNode( + MULT, val, nm->mkConstReal(Rational(1) / r.abs())); } } val = r.sgn() == 1 - ? nm->mkNode(MULT, nm->mkConstRealOrInt(vtn, Rational(-1)), val) + ? nm->mkNode(MULT, nm->mkConstRealOrInt(Rational(-1)), val) : val; return (r.sgn() == 1 || k == EQUAL) ? 1 : -1; } diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index f20964a57..00cbae056 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -351,6 +351,21 @@ Node multConstants(const Node& c1, const Node& c2) tn, Rational(c1.getConst() * c2.getConst())); } +Node mkEquality(Node a, Node b) +{ + NodeManager* nm = NodeManager::currentNM(); + Assert(a.getType().isRealOrInt()); + Assert(b.getType().isRealOrInt()); + // if they have the same type, just make them equal + if (a.getType() == b.getType()) + { + return nm->mkNode(EQUAL, a, b); + } + // otherwise subtract and set equal to zero + Node diff = nm->mkNode(Kind::SUB, a, b); + return nm->mkNode(EQUAL, diff, mkZero(diff.getType())); +} + } // namespace arith } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 748703cf6..584e1125a 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -338,6 +338,13 @@ Node negateProofLiteral(TNode n); */ Node multConstants(const Node& c1, const Node& c2); +/** + * Make the equality (= a b) or (= (- a b) zero) if a and b have different + * types, where zero has the same type as (- a b). + * Use this utility to ensure an equality is properly typed. + */ +Node mkEquality(Node a, Node b); + } // namespace arith } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp index 3ec622dcf..238ed794f 100644 --- a/src/theory/arith/bound_inference.cpp +++ b/src/theory/arith/bound_inference.cpp @@ -16,6 +16,7 @@ #include "theory/arith/bound_inference.h" #include "smt/env.h" +#include "theory/arith/arith_utilities.h" #include "theory/arith/linear/normal_form.h" #include "theory/rewriter.h" @@ -161,6 +162,7 @@ void BoundInference::update_lower_bound(const Node& origin, const Node& value, bool strict) { + Assert(value.isConst()); // lhs > or >= value because of origin Trace("bound-inf") << "\tNew bound " << lhs << (strict ? ">" : ">=") << value << " due to " << origin << std::endl; @@ -176,8 +178,8 @@ void BoundInference::update_lower_bound(const Node& origin, if (!b.lower_strict && !b.upper_strict && b.lower_value == b.upper_value) { - b.lower_bound = b.upper_bound = - rewrite(nm->mkNode(Kind::EQUAL, lhs, value)); + Node eq = mkEquality(lhs, value); + b.lower_bound = b.upper_bound = rewrite(eq); } else { @@ -211,8 +213,8 @@ void BoundInference::update_upper_bound(const Node& origin, b.upper_origin = origin; if (!b.lower_strict && !b.upper_strict && b.lower_value == b.upper_value) { - b.lower_bound = b.upper_bound = - rewrite(nm->mkNode(Kind::EQUAL, lhs, value)); + Node eq = mkEquality(lhs, value); + b.lower_bound = b.upper_bound = rewrite(eq); } else { diff --git a/src/theory/arith/linear/normal_form.cpp b/src/theory/arith/linear/normal_form.cpp index f2c1b5736..100223596 100644 --- a/src/theory/arith/linear/normal_form.cpp +++ b/src/theory/arith/linear/normal_form.cpp @@ -32,7 +32,7 @@ namespace arith::linear { Constant Constant::mkConstant(const Rational& rat) { NodeManager* nm = NodeManager::currentNM(); - return Constant(nm->mkConstReal(rat)); + return Constant(nm->mkConstRealOrInt(rat)); } size_t Variable::getComplexity() const{ diff --git a/src/theory/arith/linear/normal_form.h b/src/theory/arith/linear/normal_form.h index c9f8eb72b..83a7fd536 100644 --- a/src/theory/arith/linear/normal_form.h +++ b/src/theory/arith/linear/normal_form.h @@ -911,7 +911,10 @@ public: } } - static Polynomial parsePolynomial(Node n) { + static Polynomial parsePolynomial(Node n) + { + // required to remove TO_REAL here since equalities may require casts + n = n.getKind() == kind::TO_REAL ? n[0] : n; return Polynomial(n); } diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index db92ce763..1ef35b66a 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -37,9 +37,9 @@ ExtState::ExtState(InferenceManager& im, NlModel& model, Env& env) { d_false = NodeManager::currentNM()->mkConst(false); d_true = NodeManager::currentNM()->mkConst(true); - d_zero = NodeManager::currentNM()->mkConstReal(Rational(0)); - d_one = NodeManager::currentNM()->mkConstReal(Rational(1)); - d_neg_one = NodeManager::currentNM()->mkConstReal(Rational(-1)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); + d_one = NodeManager::currentNM()->mkConstInt(Rational(1)); + d_neg_one = NodeManager::currentNM()->mkConstInt(Rational(-1)); if (d_env.isTheoryProofProducing()) { d_proof.reset(new CDProofSet( diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 5c93be8cb..a6ba87dd2 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -125,6 +125,8 @@ void FactoringCheck::check(const std::vector& asserts, } Node sum = nm->mkNode(Kind::ADD, itf->second); sum = rewrite(sum); + // remove TO_REAL if necessary here + sum = sum.getKind() == TO_REAL ? sum[0] : sum; Trace("nl-ext-factor") << "* Factored sum for " << x << " : " << sum << std::endl; diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index f2cdd5ca7..8f2b23f44 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -403,6 +403,7 @@ bool MonomialCheck::compareMonomial( << "compareMonomial " << oa << " and " << ob << ", indices = " << a_index << " " << b_index << std::endl; Assert(status == 0 || status == 2); + NodeManager* nm = NodeManager::currentNM(); const std::vector& vla = d_data->d_mdb.getVariableList(a); const std::vector& vlb = d_data->d_mdb.getVariableList(b); if (a_index == vla.size() && b_index == vlb.size()) @@ -425,7 +426,6 @@ bool MonomialCheck::compareMonomial( exp.push_back(v.eqNode(zero).negate()); } } - NodeManager* nm = NodeManager::currentNM(); Node clem = nm->mkNode( Kind::IMPLIES, nm->mkAnd(exp), mkLit(oa, ob, status, true)); Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl; @@ -504,7 +504,8 @@ bool MonomialCheck::compareMonomial( { Trace("nl-ext-comp-debug") << "...take leading " << bv << std::endl; // can multiply b by <=1 - exp.push_back(mkLit(d_data->d_one, bv, bvo == ovo ? 0 : 2, true)); + Node one = mkOne(bv.getType()); + exp.push_back(mkLit(one, bv, bvo == ovo ? 0 : 2, true)); return compareMonomial(oa, a, a_index, @@ -528,7 +529,8 @@ bool MonomialCheck::compareMonomial( { Trace("nl-ext-comp-debug") << "...take leading " << av << std::endl; // can multiply a by >=1 - exp.push_back(mkLit(av, d_data->d_one, avo == ovo ? 0 : 2, true)); + Node one = mkOne(av.getType()); + exp.push_back(mkLit(av, one, avo == ovo ? 0 : 2, true)); return compareMonomial(oa, a, a_index + 1, @@ -553,7 +555,8 @@ bool MonomialCheck::compareMonomial( { Trace("nl-ext-comp-debug") << "...take leading " << av << std::endl; // do avo>=1 instead - exp.push_back(mkLit(av, d_data->d_one, avo == ovo ? 0 : 2, true)); + Node one = mkOne(av.getType()); + exp.push_back(mkLit(av, one, avo == ovo ? 0 : 2, true)); return compareMonomial(oa, a, a_index + 1, @@ -717,23 +720,23 @@ 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())); if (status == 0) { - Node a_eq_b = a.eqNode(b); + Node a_eq_b = mkEquality(a, b); if (!isAbsolute) { return a_eq_b; } - Node negate_b = NodeManager::currentNM()->mkNode(Kind::NEG, b); - return a_eq_b.orNode(a.eqNode(negate_b)); + Node negate_b = nm->mkNode(Kind::NEG, b); + return a_eq_b.orNode(mkEquality(a, negate_b)); } else if (status < 0) { return mkLit(b, a, -status); } Assert(status == 1 || status == 2); - NodeManager* nm = NodeManager::currentNM(); Kind greater_op = status == 1 ? Kind::GEQ : Kind::GT; if (!isAbsolute) { diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index b8030ff84..7f822c043 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -71,9 +71,6 @@ NonlinearExtension::NonlinearExtension(Env& env, d_extTheory.addFunctionKind(kind::IAND); d_extTheory.addFunctionKind(kind::POW2); d_true = NodeManager::currentNM()->mkConst(true); - d_zero = NodeManager::currentNM()->mkConstReal(Rational(0)); - d_one = NodeManager::currentNM()->mkConstReal(Rational(1)); - d_neg_one = NodeManager::currentNM()->mkConstReal(Rational(-1)); if (d_env.isTheoryProofProducing()) { diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 75ed54a29..67877f6b3 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -190,9 +190,6 @@ class NonlinearExtension : EnvObj const std::vector& xts); /** commonly used terms */ - Node d_zero; - Node d_one; - Node d_neg_one; Node d_true; // The theory of arithmetic containing this extension. TheoryArith& d_containing; diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp index 1fc6df297..d5d3437e5 100644 --- a/src/theory/arith/nl/pow2_solver.cpp +++ b/src/theory/arith/nl/pow2_solver.cpp @@ -159,7 +159,7 @@ void Pow2Solver::checkFullRefine() if (x < 0 && pow2x != 0) { Node assumption = nm->mkNode(LT, n[0], d_zero); - Node conclusion = nm->mkNode(EQUAL, n, d_zero); + Node conclusion = nm->mkNode(EQUAL, n, mkZero(n.getType())); Node lem = nm->mkNode(IMPLIES, assumption, conclusion); d_im.addPendingLemma( lem, InferenceId::ARITH_NL_POW2_TRIVIAL_CASE_REFINE, nullptr, true); diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 27aaa7730..e80b12641 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -81,10 +81,12 @@ void ExponentialSolver::checkInitialRefine() // initial refinements if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end()) { + Node zero = nm->mkConstInt(Rational(0)); + Node one = nm->mkConstInt(Rational(1)); d_tf_initial_refine[t] = true; { // exp is always positive: exp(t) > 0 - Node lem = nm->mkNode(Kind::GT, t, d_data->d_zero); + Node lem = nm->mkNode(Kind::GT, t, zero); CDProof* proof = nullptr; if (d_data->isProofEnabled()) { @@ -95,10 +97,12 @@ void ExponentialSolver::checkInitialRefine() lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof); } { - // exp at zero: (t = 0) <=> (exp(t) = 1) - Node lem = nm->mkNode(Kind::EQUAL, - t[0].eqNode(d_data->d_zero), - t.eqNode(d_data->d_one)); + // must use real one/zero in equalities + Node rzero = nm->mkConstReal(Rational(0)); + Node rone = nm->mkConstReal(Rational(1)); + // exp at zero: (t = 0.0) <=> (exp(t) = 1.0) + Node lem = + nm->mkNode(Kind::EQUAL, t[0].eqNode(rzero), t.eqNode(rone)); CDProof* proof = nullptr; if (d_data->isProofEnabled()) { @@ -111,8 +115,8 @@ void ExponentialSolver::checkInitialRefine() { // exp on negative values: (t < 0) <=> (exp(t) < 1) Node lem = nm->mkNode(Kind::EQUAL, - nm->mkNode(Kind::LT, t[0], d_data->d_zero), - nm->mkNode(Kind::LT, t, d_data->d_one)); + nm->mkNode(Kind::LT, t[0], zero), + nm->mkNode(Kind::LT, t, one)); CDProof* proof = nullptr; if (d_data->isProofEnabled()) { @@ -126,9 +130,8 @@ void ExponentialSolver::checkInitialRefine() // exp on positive values: (t <= 0) or (exp(t) > t+1) Node lem = nm->mkNode( Kind::OR, - nm->mkNode(Kind::LEQ, t[0], d_data->d_zero), - nm->mkNode( - Kind::GT, t, nm->mkNode(Kind::ADD, t[0], d_data->d_one))); + nm->mkNode(Kind::LEQ, t[0], zero), + nm->mkNode(Kind::GT, t, nm->mkNode(Kind::ADD, t[0], one))); CDProof* proof = nullptr; if (d_data->isProofEnabled()) { @@ -277,15 +280,17 @@ std::pair ExponentialSolver::getSecantBounds(TNode e, // Check if we already have neighboring secant points if (bounds.first.isNull()) { + NodeManager* nm = NodeManager::currentNM(); + Node one = nm->mkConstInt(Rational(1)); // pick c-1 - bounds.first = rewrite( - NodeManager::currentNM()->mkNode(Kind::SUB, center, d_data->d_one)); + bounds.first = rewrite(nm->mkNode(Kind::SUB, center, one)); } if (bounds.second.isNull()) { + NodeManager* nm = NodeManager::currentNM(); + Node one = nm->mkConstInt(Rational(1)); // pick c+1 - bounds.second = rewrite( - NodeManager::currentNM()->mkNode(Kind::ADD, center, d_data->d_one)); + bounds.second = rewrite(nm->mkNode(Kind::ADD, center, one)); } return bounds; } diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index 488e58ce7..5f6c166b8 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -84,9 +84,9 @@ Node TranscendentalProofRuleChecker::checkInternal( PfRule id, const std::vector& children, const std::vector& args) { NodeManager* nm = NodeManager::currentNM(); - Node zero = nm->mkConstReal(Rational(0)); - Node one = nm->mkConstReal(Rational(1)); - Node mone = nm->mkConstReal(Rational(-1)); + Node zero = nm->mkConstInt(Rational(0)); + Node one = nm->mkConstInt(Rational(1)); + Node mone = nm->mkConstInt(Rational(-1)); Node pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); Node mpi = nm->mkNode(Kind::MULT, mone, pi); Trace("nl-trans-checker") << "Checking " << id << std::endl; @@ -136,7 +136,9 @@ Node TranscendentalProofRuleChecker::checkInternal( Assert(children.empty()); Assert(args.size() == 1); Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]); - return nm->mkNode(EQUAL, args[0].eqNode(zero), e.eqNode(one)); + Node rzero = nm->mkConstReal(Rational(0)); + Node rone = nm->mkConstReal(Rational(1)); + return nm->mkNode(EQUAL, args[0].eqNode(rzero), e.eqNode(rone)); } else if (id == PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS) { diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 470862311..dfb011c4b 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -43,9 +43,9 @@ TranscendentalState::TranscendentalState(Env& env, { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); - d_zero = NodeManager::currentNM()->mkConstReal(Rational(0)); - d_one = NodeManager::currentNM()->mkConstReal(Rational(1)); - d_neg_one = NodeManager::currentNM()->mkConstReal(Rational(-1)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); + d_one = NodeManager::currentNM()->mkConstInt(Rational(1)); + d_neg_one = NodeManager::currentNM()->mkConstInt(Rational(-1)); if (d_env.isTheoryProofProducing()) { d_proof.reset(new CDProofSet( diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 6e4480e0a..78a6a3899 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -105,7 +105,7 @@ Node OperatorElim::eliminateOperators(Node node, lems.push_back(mkSkolemLemma(lem, v)); if (k == IS_INTEGER) { - return nm->mkNode(EQUAL, node[0], v); + return mkEquality(node[0], v); } Assert(k == TO_INTEGER); return v; @@ -226,7 +226,7 @@ Node OperatorElim::eliminateOperators(Node node, Node v = sm->mkPurifySkolem( rw, "nonlinearDiv", "the result of a non-linear div term"); Node lem = nm->mkNode(IMPLIES, - den.eqNode(nm->mkConstReal(Rational(0))).negate(), + den.eqNode(mkZero(den.getType())).negate(), nm->mkNode(MULT, den, v).eqNode(num)); lems.push_back(mkSkolemLemma(lem, v)); return v; @@ -241,7 +241,7 @@ Node OperatorElim::eliminateOperators(Node node, { checkNonLinearLogic(node); Node divByZeroNum = getArithSkolemApp(num, SkolemFunId::DIV_BY_ZERO); - Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConstReal(Rational(0))); + Node denEq0 = nm->mkNode(EQUAL, den, mkZero(den.getType())); ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret); } return ret; diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index f05bd2185..81aefe6e8 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -74,7 +74,7 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, || rel == Kind::LEQ || rel == Kind::GT || rel == Kind::GEQ); Node lhs = args[1][0]; Node rhs = args[1][1]; - Node zero = nm->mkConstRealOrInt(mult.getType(), Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); return nm->mkNode(Kind::IMPLIES, nm->mkAnd(std::vector{ nm->mkNode(Kind::GT, mult, zero), args[1]}), @@ -93,7 +93,7 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, Kind rel_inv = (rel == Kind::DISTINCT ? rel : reverseRelationKind(rel)); Node lhs = args[1][0]; Node rhs = args[1][1]; - Node zero = nm->mkConstRealOrInt(mult.getType(), Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); return nm->mkNode(Kind::IMPLIES, nm->mkAnd(std::vector{ nm->mkNode(Kind::LT, mult, zero), args[1]}), diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 40e07fb55..36e4f5a7c 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -18,9 +18,10 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" +#include "theory/arith/arith_utilities.h" #include "theory/arith/linear/partial_model.h" -#include "theory/arith/theory_arith.h" #include "theory/arith/linear/theory_arith_private.h" +#include "theory/arith/theory_arith.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "util/random.h" @@ -93,7 +94,7 @@ bool ArithInstantiator::processEquality(CegInstantiator* ci, eq_rhs = nm->mkNode(MULT, lhs_coeff, eq_rhs); } } - Node eq = eq_lhs.eqNode(eq_rhs); + Node eq = arith::mkEquality(eq_lhs, eq_rhs); eq = rewrite(eq); Node val; TermProperties pv_prop; @@ -689,7 +690,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable( // solve updated rewritten equality for vars[index], if coefficient is one, // then we are successful Node eq_rhs = sf.d_subs[index]; - Node eq = eq_lhs.eqNode(eq_rhs); + Node eq = arith::mkEquality(eq_lhs, eq_rhs); eq = rewrite(eq); Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl; std::map msum;