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 c149ef6a5273bea108e4c5fbd1535c2763fea901..202cb129213acf9a2b8e19c53b2921286c134a79 100644 (file)
--- 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<Rational>() > 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 f963741277ef32720da6f0ffcc77f6a7b9bd30fc..6d34996112e5817eaf85728e4ecea70fdab38f72 100644 (file)
--- 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 f20964a57eb6fbbd7bf5dc43823c09b9a102e23d..00cbae056cca87c3bd6a1a0c7e4ae74e10b19f42 100644 (file)
--- 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<Rational>() * c2.getConst<Rational>()));
 }
 
+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 748703cf695d8856ed7bedd0c7ac1dd5537151cd..584e1125ad5303e3ddc78a9b8bb2043fa522e603 100644 (file)
--- 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 3ec622dcf363136e53f32934df631de5a5c2c72d..238ed794f6aa8bc2ea83907ce64238391b3f787e 100644 (file)
--- 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 f2c1b573600eada76b412bac52bab369796d7acd..1002235966f1134815b9d6ac0e4a1ea156a5ee20 100644 (file)
--- 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 c9f8eb72b5ea0ae5f05e4cd8c87fdc79d84ee20a..83a7fd5364e51873f2406caaec5d00b688a16846 100644 (file)
--- 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 db92ce76329d81c126e7f12d474023b369d59243..1ef35b66a5177da0f30e6c19d0c8ef01ad66db5e 100644 (file)
--- 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<CDProof>(

diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index 5c93be8cb24c5e9423f830e6445f1188b87d5e33..a6ba87dd2018dc107a79ba7565b5650fb9d2a3f7 100644 (file)
--- 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<Node>& 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 f2cdd5ca7db0e73786e9f471fd0a52325a11d99f..8f2b23f44ea5f802ed278ee730d8985230c46e2c 100644 (file)
--- 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<Node>& vla = d_data->d_mdb.getVariableList(a);
   const std::vector<Node>& 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<Node>& 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 b8030ff843df54cf78bb2139dd775d21fec3b303..7f822c043991f8ebb92872e7b8e8eb94d71ec128 100644 (file)
--- 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 75ed54a29b3164c29b30a6c8022c6d2febd52f1b..67877f6b32b6532ffd21043b078f25a63368101d 100644 (file)
--- 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<Node>& 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 1fc6df2971e27f1d1e6f552a7032cdb4590a3743..d5d3437e5548d6edd8bf5c1f3f0661dc8ac698bb 100644 (file)
--- 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 27aaa7730c3546de0d3df5d121eae42db7769576..e80b12641ff0c9efad2faf651da172b37e6100f6 100644 (file)
--- 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<Node, Node> 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 488e58ce7a30cc777e24fbefd415bc4d0050a61d..5f6c166b8474f3cbd934531d1771caafda8413b3 100644 (file)
--- 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<Node>& children, const std::vector<Node>& 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 470862311ea4f7b27eaf136a17dd15127788c6f3..dfb011c4b66721fef08b3f4f54e69ae1eaabd5a6 100644 (file)
--- 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<CDProof>(

diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 6e4480e0add10c119183eb887532645efbb2057c..78a6a3899005ff04c3e7470d1a91f1d4485a2512 100644 (file)
--- 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 f05bd218546efab6e27996b1b86c3ce40b47b432..81aefe6e8e68dc91edbeeb62a07c8034306d02fa 100644 (file)
--- 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<Node>{
                             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<Node>{
                             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 40e07fb55590dd9550a6ec1dd2976b925b0254e1..36e4f5a7cd32af824a78a19434ebd6b6a864a817 100644 (file)
--- 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<Node, Node> msum;