From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 23 Mar 2021 22:44:28 +0000 (-0500)
Subject: Remove unused code for axioms (#6197)
X-Git-Tag: cvc5-1.0.0~2036
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=34798fb86eabe7b9aaff86be23a7a3428ebfc957;p=cvc5.git

Remove unused code for axioms (#6197)

This is leftover from a previous way of eliminating extended operators
---

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 74b13aed1..f6278d3a1 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1299,65 +1299,6 @@ void TheoryArithPrivate::cautiousSetupPolynomial(const Polynomial& p){
   }
 }
 
-Node TheoryArithPrivate::axiomIteForTotalDivision(Node div_tot){
-  Assert(div_tot.getKind() == DIVISION_TOTAL);
-
-  // Inverse of multiplication axiom:
-  //   (for all ((n Real) (d Real))
-  //    (ite (= d 0)
-  //     (= (DIVISION_TOTAL n d) 0)
-  //     (= (* d (DIVISION_TOTAL n d)) n)))
-
-
-  Polynomial n = Polynomial::parsePolynomial(div_tot[0]);
-  Polynomial d = Polynomial::parsePolynomial(div_tot[1]);
-  Polynomial div_tot_p = Polynomial::parsePolynomial(div_tot);
-
-  Comparison invEq = Comparison::mkComparison(EQUAL, n, d * div_tot_p);
-  Comparison zeroEq = Comparison::mkComparison(EQUAL, div_tot_p, Polynomial::mkZero());
-  Node dEq0 = (d.getNode()).eqNode(mkRationalNode(0));
-  Node ite = dEq0.iteNode(zeroEq.getNode(), invEq.getNode());
-
-  return ite;
-}
-
-Node TheoryArithPrivate::axiomIteForTotalIntDivision(Node int_div_like){
-  Kind k = int_div_like.getKind();
-  Assert(k == INTS_DIVISION_TOTAL || k == INTS_MODULUS_TOTAL);
-
-  // See the discussion of integer division axioms above.
-
-  Polynomial n = Polynomial::parsePolynomial(int_div_like[0]);
-  Polynomial d = Polynomial::parsePolynomial(int_div_like[1]);
-
-  NodeManager* currNM = NodeManager::currentNM();
-  Node zero = mkRationalNode(0);
-
-  Node q = (k == INTS_DIVISION_TOTAL) ? int_div_like : currNM->mkNode(INTS_DIVISION_TOTAL, n.getNode(), d.getNode());
-  Node r = (k == INTS_MODULUS_TOTAL) ? int_div_like : currNM->mkNode(INTS_MODULUS_TOTAL, n.getNode(), d.getNode());
-
-  Node dEq0 = (d.getNode()).eqNode(zero);
-  Node qEq0 = q.eqNode(zero);
-  Node rEq0 = r.eqNode(zero);
-
-  Polynomial rp = Polynomial::parsePolynomial(r);
-  Polynomial qp = Polynomial::parsePolynomial(q);
-
-  Node abs_d = (d.isConstant()) ?
-    d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs");
-
-  Node eq = Comparison::mkComparison(EQUAL, n, d * qp + rp).getNode();
-  Node leq0 = currNM->mkNode(LEQ, zero, r);
-  Node leq1 = currNM->mkNode(LT, r, abs_d);
-
-  Node andE = currNM->mkNode(AND, eq, leq0, leq1);
-  Node defDivMode = dEq0.iteNode(qEq0.andNode(rEq0), andE);
-  Node lem = abs_d.getMetaKind () == metakind::VARIABLE ?
-    defDivMode.andNode(d.makeAbsCondition(Variable(abs_d))) : defDivMode;
-
-  return lem;
-}
-
 
 void TheoryArithPrivate::setupPolynomial(const Polynomial& poly) {
   Assert(!poly.containsConstant());
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 4f261bc00..181861b00 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -417,9 +417,6 @@ private:
    */
   DeltaRational getDeltaValue(TNode term) const
       /* throw(DeltaRationalException, ModelException) */;
-
-  Node axiomIteForTotalDivision(Node div_tot);
-  Node axiomIteForTotalIntDivision(Node int_div_like);
  public:
   TheoryArithPrivate(TheoryArith& containing,
                      context::Context* c,