summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arith/arith_utilities.h6
-rw-r--r--src/theory/arith/normal_form.cpp11
-rw-r--r--src/theory/arith/normal_form.h15
-rw-r--r--src/theory/arith/theory_arith.cpp176
-rw-r--r--src/theory/arith/theory_arith.h7
5 files changed, 200 insertions, 15 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 6ac2338f3..427ebbbd3 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -45,7 +45,13 @@ inline Node mkBoolNode(bool b){
return NodeManager::currentNM()->mkConst<bool>(b);
}
+inline Node mkIntSkolem(const std::string& name){
+ return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->integerType());
+}
+inline Node mkRealSkolem(const std::string& name){
+ return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->realType());
+}
/** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
inline bool isRelationOperator(Kind k){
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index c90be63b9..39618d498 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -27,6 +27,17 @@ namespace CVC4 {
namespace theory{
namespace arith {
+bool Variable::isDivMember(Node n){
+ switch(n.getKind()){
+ case kind::DIVISION:
+ case kind::INTS_DIVISION:
+ case kind::INTS_MODULUS:
+ return Polynomial::isMember(n[0]) && Polynomial::isMember(n[1]);
+ default:
+ return false;
+ }
+}
+
bool VarList::isSorted(iterator start, iterator end) {
return __gnu_cxx::is_sorted(start, end);
}
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 33fc42cea..3184deec5 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -211,7 +211,6 @@ namespace arith {
* | (+ [monomial]) -> [monomial]
*/
-
/**
* A NodeWrapper is a class that is a thinly veiled container of a Node object.
*/
@@ -232,9 +231,17 @@ public:
// TODO: check if it's a theory leaf also
static bool isMember(Node n) {
- if (n.getKind() == kind::CONST_RATIONAL) return false;
- if (isRelationOperator(n.getKind())) return false;
- return Theory::isLeafOf(n, theory::THEORY_ARITH);
+ Kind k = n.getKind();
+ if (k == kind::CONST_RATIONAL) return false;
+ if (isRelationOperator(k)) return false;
+ if (Theory::isLeafOf(n, theory::THEORY_ARITH)) return true;
+ if (k == kind::INTS_DIVISION || k == kind::INTS_MODULUS || k == kind::DIVISION) return isDivMember(n);
+ return false;
+ }
+
+ static bool isDivMember(Node n);
+ bool isDivLike() const{
+ return isDivMember(getNode());
}
bool isNormalForm() { return isMember(getNode()); }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e159c0e42..e552ae5a0 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -58,6 +58,7 @@ const uint32_t RESET_START = 2;
TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe),
+ d_nlIncomplete(u, false),
d_qflraStatus(Result::SAT_UNKNOWN),
d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
@@ -653,6 +654,7 @@ Node TheoryArith::ppRewrite(TNode atom) {
<< a << endl;
}
+
if (a.getKind() == kind::EQUAL && options::arithRewriteEq()) {
Node leq = NodeBuilder<2>(kind::LEQ) << a[0] << a[1];
Node geq = NodeBuilder<2>(kind::GEQ) << a[0] << a[1];
@@ -792,6 +794,12 @@ void TheoryArith::setupVariable(const Variable& x){
setupInitialValue(varN);
markSetup(n);
+
+
+ if(x.isDivLike()){
+ interpretDivLike(x);
+ }
+
}
void TheoryArith::setupVariableList(const VarList& vl){
@@ -813,6 +821,7 @@ void TheoryArith::setupVariableList(const VarList& vl){
// vl is the product of at least 2 variables
// vl : (* v1 v2 ...)
d_out->setIncomplete();
+ d_nlIncomplete = true;
++(d_statistics.d_statUserVariables);
ArithVar av = requestArithVar(vlNode, false);
@@ -826,6 +835,68 @@ void TheoryArith::setupVariableList(const VarList& vl){
* See the comment in setupPolynomail for more.
*/
}
+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);
+ }
+
+ 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);
+
+ 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) {
Assert(!poly.containsConstant());
@@ -923,7 +994,9 @@ void TheoryArith::preRegisterTerm(TNode n) {
ArithVar TheoryArith::requestArithVar(TNode x, bool slack){
- Assert(isLeaf(x) || x.getKind() == PLUS);
+ //TODO : The VarList trick is good enough?
+ Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS);
+ Assert(!Variable::isDivMember(x) || !getLogicInfo().isLinear());
Assert(!d_arithvarNodeMap.hasArithVar(x));
Assert(x.getType().isReal());// real or integer
@@ -966,20 +1039,23 @@ void TheoryArith::asVectors(const Polynomial& p, std::vector<Rational>& coeffs,
Debug("rewriter") << "should be var: " << n << endl;
- Assert(isLeaf(n));
+ // TODO: This VarList::isMember(n) can be stronger
+ Assert(isLeaf(n) || VarList::isMember(n));
Assert(theoryOf(n) != THEORY_ARITH || d_arithvarNodeMap.hasArithVar(n));
Assert(d_arithvarNodeMap.hasArithVar(n));
ArithVar av;
- if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) {
- // The only way not to get it through pre-register is if it's a foreign term
- ++(d_statistics.d_statUserVariables);
- av = requestArithVar(n,false);
- setupInitialValue(av);
- } else {
- // Otherwise, we already have it's variable
- av = d_arithvarNodeMap.asArithVar(n);
- }
+ // The first if is likely dead is likely dead code:
+ // if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) {
+ // // The only way not to get it through pre-register is if it's a foreign term
+ // ++(d_statistics.d_statUserVariables);
+ // av = requestArithVar(n,false);
+ // setupInitialValue(av);
+ // } else {
+ // // Otherwise, we already have it's variable
+ // av = d_arithvarNodeMap.asArithVar(n);
+ // }
+ av = d_arithvarNodeMap.asArithVar(n);
coeffs.push_back(constant.getValue());
variables.push_back(av);
@@ -1870,6 +1946,7 @@ bool TheoryArith::getDeltaAtomValue(TNode n) {
DeltaRational TheoryArith::getDeltaValue(TNode n) {
Assert(d_qflraStatus != Result::SAT_UNKNOWN);
+ Assert(!d_nlIncomplete);
Debug("arith::value") << n << std::endl;
switch(n.getKind()) {
@@ -1925,8 +2002,76 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
}
}
+DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) {
+ Assert(d_qflraStatus != Result::SAT_UNKNOWN);
+ Assert(d_nlIncomplete);
+
+ Debug("arith::value") << n << std::endl;
+
+ switch(n.getKind()) {
+
+ case kind::CONST_RATIONAL:
+ return n.getConst<Rational>();
+
+ case kind::PLUS: { // 2+ args
+ DeltaRational value(0);
+ for(TNode::iterator i = n.begin(),
+ iend = n.end();
+ i != iend && !failed;
+ ++i) {
+ value = value + getDeltaValueWithNonlinear(*i, failed);
+ }
+ return value;
+ }
+
+ case kind::MULT: { // 2+ args
+ DeltaRational value(1);
+ if (n[0].getKind() == kind::CONST_RATIONAL) {
+ return getDeltaValueWithNonlinear(n[1], failed) * n[0].getConst<Rational>();
+ }else{
+ failed = true;
+ return value;
+ }
+ }
+
+ case kind::MINUS: // 2 args
+ // should have been rewritten
+ Unreachable();
+
+ case kind::UMINUS: // 1 arg
+ // should have been rewritten
+ Unreachable();
+
+ case kind::DIVISION: // 2 args
+ Assert(n[1].isConst());
+ if (n[1].getKind() == kind::CONST_RATIONAL) {
+ return getDeltaValueWithNonlinear(n[0], failed) / n[0].getConst<Rational>();
+ }else{
+ failed = true;
+ return DeltaRational();
+ }
+ //fall through
+ case kind::INTS_DIVISION:
+ case kind::INTS_MODULUS:
+ //a bit strict
+ failed = true;
+ return DeltaRational();
+
+ default:
+ {
+ if(isSetup(n)){
+ ArithVar var = d_arithvarNodeMap.asArithVar(n);
+ return d_partialModel.getAssignment(var);
+ }else{
+ Unreachable();
+ }
+ }
+ }
+}
+
void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
Assert(d_qflraStatus == Result::SAT);
+ Assert(!d_nlIncomplete);
Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
@@ -2110,6 +2255,15 @@ void TheoryArith::presolve(){
EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
if(d_qflraStatus == Result::SAT_UNKNOWN){
return EQUALITY_UNKNOWN;
+ }else if(d_nlIncomplete){
+ bool failed = false;
+ DeltaRational amod = getDeltaValueWithNonlinear(a, failed);
+ DeltaRational bmod = getDeltaValueWithNonlinear(b, failed);
+ if(failed){
+ return EQUALITY_UNKNOWN;
+ }else{
+ return amod == bmod ? EQUALITY_TRUE_IN_MODEL : EQUALITY_FALSE_IN_MODEL;
+ }
}else if (getDeltaValue(a) == getDeltaValue(b)) {
return EQUALITY_TRUE_IN_MODEL;
} else {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index c98c759f7..1c2c942fd 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -64,6 +64,8 @@ class InstantiatorTheoryArith;
class TheoryArith : public Theory {
friend class InstantiatorTheoryArith;
private:
+ context::CDO<bool> d_nlIncomplete;
+
enum Result::Sat d_qflraStatus;
// check()
// !done() -> d_qflraStatus = Unknown
@@ -105,6 +107,8 @@ private:
d_setupNodes.insert(n);
}
+ void interpretDivLike(const Variable& x);
+
void setupVariable(const Variable& x);
void setupVariableList(const VarList& vl);
void setupPolynomial(const Polynomial& poly);
@@ -310,6 +314,9 @@ private:
/** Internal model value for the node */
DeltaRational getDeltaValue(TNode n);
+ /** TODO : get rid of this. */
+ DeltaRational getDeltaValueWithNonlinear(TNode n, bool& failed);
+
public:
TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
virtual ~TheoryArith();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback