summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/normal_form.cpp13
-rw-r--r--src/theory/arith/normal_form.h12
-rw-r--r--src/theory/arith/theory_arith.cpp107
3 files changed, 76 insertions, 56 deletions
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 2e1d7fd5c..de5f801f0 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -1047,6 +1047,19 @@ Kind Comparison::comparisonKind(TNode literal){
}
}
+
+Node Polynomial::makeAbsCondition(Variable v, Polynomial p){
+ Polynomial zerop = Polynomial::mkZero();
+
+ Polynomial varp = Polynomial::mkPolynomial(v);
+ Comparison pLeq0 = Comparison::mkComparison(kind::LEQ, p, zerop);
+ Comparison negP = Comparison::mkComparison(kind::EQUAL, varp, -p);
+ Comparison posP = Comparison::mkComparison(kind::EQUAL, varp, p);
+
+ Node absCnd = (pLeq0.getNode()).iteNode(negP.getNode(), posP.getNode());
+ return absCnd;
+}
+
} //namespace arith
} //namespace theory
} //namespace CVC4
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index bdaaf1918..31f8e138e 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -992,7 +992,7 @@ public:
}else{
uint32_t max = (*i).coefficientLength();
++i;
- for(; i!=e; ++i){
+ for(; i!=e; ++i){
uint32_t curr = (*i).coefficientLength();
if(curr > max){
max = curr;
@@ -1032,7 +1032,15 @@ public:
}
friend class SumPair;
- friend class Comparison;;
+ friend class Comparison;
+
+ /** Returns a node that if asserted ensures v is the abs of this polynomial.*/
+ Node makeAbsCondition(Variable v){
+ return makeAbsCondition(v, *this);
+ }
+
+ /** Returns a node that if asserted ensures v is the abs of p.*/
+ static Node makeAbsCondition(Variable v, Polynomial p);
};/* class Polynomial */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 65d9551ac..5bd4c166d 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -819,63 +819,62 @@ void TheoryArith::interpretDivLike(const Variable& v){
Assert(v.isDivLike());
Node vnode = v.getNode();
Assert(isSetup(vnode)); // Otherwise there is some invariant breaking recursion
- Polynomial m = Polynomial::parsePolynomial(vnode[0]);
- Polynomial n = Polynomial::parsePolynomial(vnode[1]);
-
- NodeManager* currNM = NodeManager::currentNM();
-
- Node nNeq0 = currNM->mkNode(EQUAL, n.getNode(), mkRationalNode(0)).notNode();
- if(vnode.getKind() == INTS_DIVISION || vnode.getKind() == INTS_MODULUS){
- // (for all ((m Int) (n Int))
- // (=> (distinct n 0)
- // (let ((q (div m n)) (r (mod m n)))
- // (and (= m (+ (* n q) r))
- // (<= 0 r (- (abs n) 1))))))
-
- Node q = (vnode.getKind() == INTS_DIVISION) ? vnode : currNM->mkNode(INTS_DIVISION, m.getNode(), n.getNode());
- Node r = (vnode.getKind() == INTS_MODULUS) ? vnode : currNM->mkNode(INTS_MODULUS, m.getNode(), n.getNode());
-
-
- Polynomial rp = Polynomial::parsePolynomial(r);
- Polynomial qp = Polynomial::parsePolynomial(q);
-
- Node abs_n;
- Node zero = mkRationalNode(0);
-
- if(n.isConstant()){
- abs_n = n.getHead().getConstant().abs().getNode();
- }else{
- abs_n = mkIntSkolem("abs_$$");
- Polynomial abs_np = Polynomial::parsePolynomial(abs_n);
- Node absCnd = currNM->mkNode(ITE,
- currNM->mkNode(LEQ, n.getNode(), zero),
- Comparison::mkComparison(EQUAL, abs_np, -rp).getNode(),
- Comparison::mkComparison(EQUAL, abs_np, rp).getNode());
-
- d_out->lemma(absCnd);
- }
+ Polynomial m = Polynomial::parsePolynomial(vnode[0]);
+ Polynomial n = Polynomial::parsePolynomial(vnode[1]);
+
+ NodeManager* currNM = NodeManager::currentNM();
+ Node nNeq0 = currNM->mkNode(EQUAL, n.getNode(), mkRationalNode(0)).notNode();
+ if(vnode.getKind() == INTS_DIVISION || vnode.getKind() == INTS_MODULUS){
+ // (for all ((m Int) (n Int))
+ // (=> (distinct n 0)
+ // (let ((q (div m n)) (r (mod m n)))
+ // (and (= m (+ (* n q) r))
+ // (<= 0 r (- (abs n) 1))))))
+
+ // Updated for div 0 functions
+ // (for all ((m Int) (n Int))
+ // (let ((q (div m n)) (r (mod m n)))
+ // (ite (= n 0)
+ // (and (= q (div_0_func m)) (= r (mod_0_func m)))
+ // (and (= m (+ (* n q) r))
+ // (<= 0 r (- (abs n) 1)))))))
+
+ Node q = (vnode.getKind() == INTS_DIVISION) ? vnode : currNM->mkNode(INTS_DIVISION, m.getNode(), n.getNode());
+ Node r = (vnode.getKind() == INTS_MODULUS) ? vnode : currNM->mkNode(INTS_MODULUS, m.getNode(), n.getNode());
+
+
+ Polynomial rp = Polynomial::parsePolynomial(r);
+ Polynomial qp = Polynomial::parsePolynomial(q);
+
+ Node abs_n;
+ Node zero = mkRationalNode(0);
+
+ if(n.isConstant()){
+ abs_n = n.getHead().getConstant().abs().getNode();
+ }else{
+ abs_n = mkIntSkolem("abs_$$");
+ Node absCnd = n.makeAbsCondition(Variable(abs_n));
+ d_out->lemma(absCnd);
+ }
- Node eq = Comparison::mkComparison(EQUAL, m, n * qp + rp).getNode();
- Node leq0 = currNM->mkNode(LEQ, zero, r);
- Node leq1 = currNM->mkNode(LT, r, abs_n);
+ Node eq = Comparison::mkComparison(EQUAL, m, n * qp + rp).getNode();
+ Node leq0 = currNM->mkNode(LEQ, zero, r);
+ Node leq1 = currNM->mkNode(LT, r, abs_n);
- Node andE = currNM->mkNode(AND, eq, leq0, leq1);
- Node nNeq0ImpliesandE = currNM->mkNode(IMPLIES, nNeq0, andE);
+ Node andE = currNM->mkNode(AND, eq, leq0, leq1);
+ Node nNeq0ImpliesandE = currNM->mkNode(IMPLIES, nNeq0, andE);
+
+ d_out->lemma(nNeq0ImpliesandE);
+ }else{
+ // DIVISION (/ q r)
+ // (=> (distinct 0 n) (= m (* d n)))
+ Assert(vnode.getKind() == DIVISION);
+ Node d = mkRealSkolem("division_$$");
+ Node eq = Comparison::mkComparison(EQUAL, m, n * Polynomial::parsePolynomial(d)).getNode();
+ Node nNeq0ImpliesEq = currNM->mkNode(IMPLIES, nNeq0, eq);
+ d_out->lemma(nNeq0ImpliesEq);
+ }
- d_out->lemma(nNeq0ImpliesandE);
- }else{
- // DIVISION (/ q r)
- // (=> (distinct 0 n) (= m (* d n)))
-
- Assert(vnode.getKind() == DIVISION);
- Node d = mkRealSkolem("division_$$");
-
- Node eq = Comparison::mkComparison(EQUAL, m, n * Polynomial::parsePolynomial(d)).getNode();
- Node nNeq0ImpliesEq = currNM->mkNode(IMPLIES, nNeq0, eq);
-
- d_out->lemma(nNeq0ImpliesEq);
- }
-
}
void TheoryArith::setupPolynomial(const Polynomial& poly) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback