summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/Makefile.am10
-rw-r--r--src/theory/arith/arith_constants.h4
-rw-r--r--src/theory/arith/arith_rewriter.cpp49
-rw-r--r--src/theory/arith/arith_rewriter.h6
-rw-r--r--src/theory/arith/arith_utilities.h37
-rw-r--r--src/theory/arith/basic.h5
-rw-r--r--src/theory/arith/delta_rational.cpp10
-rw-r--r--src/theory/arith/delta_rational.h22
-rw-r--r--src/theory/arith/normal.h2
-rw-r--r--src/theory/arith/normal_form_notes.txt111
-rw-r--r--src/theory/arith/partial_model.cpp223
-rw-r--r--src/theory/arith/partial_model.h372
-rw-r--r--src/theory/arith/tableau.h3
-rw-r--r--src/theory/arith/theory_arith.cpp285
-rw-r--r--src/theory/arith/theory_arith.h23
-rw-r--r--src/theory/theory_engine.h2
16 files changed, 770 insertions, 394 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 0428bf84e..ae9d3aab7 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -6,16 +6,20 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libarith.la
libarith_la_SOURCES = \
- theory_arith.h \
- theory_arith.cpp \
theory_arith_type_rules.h \
arith_rewriter.h \
arith_rewriter.cpp \
arith_utilities.h \
arith_constants.h \
+ delta_rational.h \
+ delta_rational.cpp \
+ partial_model.h \
+ partial_model.cpp \
basic.h \
normal.h \
slack.h \
- tableau.h
+ tableau.h \
+ theory_arith.h \
+ theory_arith.cpp
EXTRA_DIST = kinds
diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h
index d9419cd6b..775db3ae0 100644
--- a/src/theory/arith/arith_constants.h
+++ b/src/theory/arith/arith_constants.h
@@ -3,6 +3,7 @@
#include "expr/node.h"
#include "expr/node_manager.h"
#include "util/rational.h"
+#include "theory/arith/delta_rational.h"
#ifndef __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
#define __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
@@ -17,6 +18,8 @@ public:
Rational d_ONE;
Rational d_NEGATIVE_ONE;
+ DeltaRational d_ZERO_DELTA;
+
Node d_ZERO_NODE;
Node d_ONE_NODE;
Node d_NEGATIVE_ONE_NODE;
@@ -25,6 +28,7 @@ public:
d_ZERO(0,1),
d_ONE(1,1),
d_NEGATIVE_ONE(-1,1),
+ d_ZERO_DELTA(d_ZERO),
d_ZERO_NODE(nm->mkConst(d_ZERO)),
d_ONE_NODE(nm->mkConst(d_ONE)),
d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE))
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index f3d3061d7..a20d187bd 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -18,11 +18,6 @@ using namespace CVC4::theory::arith;
Kind multKind(Kind k, int sgn);
-Node coerceToRationalNode(TNode constant);
-
-Node multPnfByNonZero(TNode pnf, Rational& q);
-
-
/**
* Performs a quick check to see if it is easy to rewrite to
* this normal form
@@ -52,15 +47,24 @@ Node almostVarOrConstEqn(TNode atom, Kind k, TNode left, TNode right){
bool res = evaluateConstantPredicate(k,lc, rc);
return mkBoolNode(res);
}else if(leftIsVar && rightIsConst){
- return atom;
+ if(right.getKind() == kind::CONST_RATIONAL){
+ return atom;
+ }else{
+ return NodeManager::currentNM()->mkNode(k,left,coerceToRationalNode(right));
+ }
}else if(leftIsConst && rightIsVar){
- return NodeManager::currentNM()->mkNode(multKind(k,-1),right,left);
+ if(left.getKind() == kind::CONST_RATIONAL){
+ return NodeManager::currentNM()->mkNode(multKind(k,-1),right,left);
+ }else{
+ Node q_left = coerceToRationalNode(left);
+ return NodeManager::currentNM()->mkNode(multKind(k,-1),right,q_left);
+ }
}
return Node::null();
}
-Node ArithRewriter::rewriteAtom(TNode atom){
+Node ArithRewriter::rewriteAtomCore(TNode atom){
Kind k = atom.getKind();
Assert(isRelationOperator(k));
@@ -74,6 +78,7 @@ Node ArithRewriter::rewriteAtom(TNode atom){
return nf;
}
+
//Transform this to: (left- right) |><| 0
Node diff = makeSubtractionNode(left, right);
@@ -110,7 +115,7 @@ Node ArithRewriter::rewriteAtom(TNode atom){
nf = NodeManager::currentNM()->mkNode(newKind, newLeft, newRight);
}
}else{ //(+ p_1 .. p_N) |><| b
- NodeBuilder<> plus;
+ NodeBuilder<> plus(kind::PLUS);
for(int i=1; i<=N; ++i){
TNode p_i = rewritten[i];
plus << multPnfByNonZero(p_i, d);
@@ -123,6 +128,19 @@ Node ArithRewriter::rewriteAtom(TNode atom){
return nf;
}
+Node ArithRewriter::rewriteAtom(TNode atom){
+ Node rewritten = rewriteAtomCore(atom);
+ if(rewritten.getKind() == kind::LT){
+ Node geq = NodeManager::currentNM()->mkNode(kind::GEQ, rewritten[0], rewritten[1]);
+ return NodeManager::currentNM()->mkNode(kind::NOT, geq);
+ }else if(rewritten.getKind() == kind::GT){
+ Node leq = NodeManager::currentNM()->mkNode(kind::LEQ, rewritten[0], rewritten[1]);
+ return NodeManager::currentNM()->mkNode(kind::NOT, leq);
+ }else{
+ return rewritten;
+ }
+}
+
/* cmp( (* d v_1 v_2 ... v_M), (* d' v'_1 v'_2 ... v'_M'):
* if(M == M'):
@@ -317,7 +335,7 @@ Node ArithRewriter::rewriteMult(TNode t){
if(rewrittenChild.getMetaKind() == kind::metakind::CONSTANT){//c
Rational c = rewrittenChild.getConst<Rational>();
accumulator = accumulator * c;
- if(accumulator == 0){
+ if(accumulator == d_constants->d_ZERO){
return d_constants->d_ZERO_NODE;
}
}else if(rewrittenChild.getMetaKind() == kind::metakind::VARIABLE){ //v
@@ -391,8 +409,8 @@ Node ArithRewriter::rewriteTerm(TNode t){
* The claim is that this is always okay:
* If d' = q*d, p' = (* d' p_1 p_2 .. p_M) =_{Reals} q * pnf.
*/
-Node multPnfByNonZero(TNode pnf, Rational& q){
- Assert(q != 0);
+Node ArithRewriter::multPnfByNonZero(TNode pnf, Rational& q){
+ Assert(q != d_constants->d_ZERO);
//TODO Assert(isPNF(pnf) );
int M = pnf.getNumChildren()-1;
@@ -400,7 +418,7 @@ Node multPnfByNonZero(TNode pnf, Rational& q){
Rational new_d = d*q;
- NodeBuilder<> mult;
+ NodeBuilder<> mult(kind::MULT);
mult << mkRationalNode(new_d);
for(int i=1; i<=M; ++i){
mult << pnf[i];
@@ -443,8 +461,7 @@ Kind multKind(Kind k, int sgn){
}
Node ArithRewriter::rewrite(TNode n){
- using namespace std;
- cout << "Trace rewrite:" << n << endl;
+ Debug("arithrewriter") << "Trace rewrite:" << n << std::endl;
if(n.getAttribute(IsNormal())){
return n;
@@ -452,7 +469,7 @@ Node ArithRewriter::rewrite(TNode n){
Node res;
- if(n.isAtomic()){
+ if(isRelationOperator(n.getKind())){
res = rewriteAtom(n);
}else{
res = rewriteTerm(n);
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 844663ce8..a2a8b1b4b 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -67,7 +67,11 @@ class ArithRewriter{
private:
ArithConstants* d_constants;
+ //This is where the core of the work is done for rewriteAtom
+ //With a few additional checks done by rewriteAtom
+ Node rewriteAtomCore(TNode atom);
Node rewriteAtom(TNode atom);
+
Node rewriteTerm(TNode t);
Node rewriteMult(TNode t);
Node rewritePlus(TNode t);
@@ -76,6 +80,8 @@ private:
Node var2pnf(TNode variable);
+ Node multPnfByNonZero(TNode pnf, Rational& q);
+
public:
ArithRewriter(ArithConstants* ac) :
d_constants(ac)
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 7b578c934..297def3c7 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -101,16 +101,16 @@ inline Node pushInNegation(Node assertion){
case EQUAL:
return assertion;
case GT:
- k = LT;
+ k = LEQ;
break;
case GEQ:
- k = LEQ;
+ k = LT;
break;
case LEQ:
- k = GEQ;
+ k = GT;
break;
case LT:
- k = GT;
+ k = GEQ;
break;
default:
Unreachable();
@@ -119,6 +119,35 @@ inline Node pushInNegation(Node assertion){
return NodeManager::currentNM()->mkNode(k, p[0],p[1]);
}
+/**
+ * Validates that a node constraint has the following form:
+ * constraint: x |><| c
+ * where |><| is either <, <=, ==, >=, LT,
+ * x is of metakind a variabale,
+ * and c is a constant rational.
+ */
+inline bool validateConstraint(TNode constraint){
+ using namespace CVC4::kind;
+ switch(constraint.getKind()){
+ case LT:case LEQ: case EQUAL: case GEQ: case GT: break;
+ default: return false;
+ }
+
+ if(constraint[0].getMetaKind() != metakind::VARIABLE) return false;
+ return constraint[1].getKind() == CONST_RATIONAL;
+}
+
+inline int deltaCoeff(Kind k){
+ switch(k){
+ case kind::LT:
+ return -1;
+ case kind::GT:
+ return 1;
+ default:
+ return 0;
+ }
+}
+
}; /* namesapce arith */
}; /* namespace theory */
}; /* namespace CVC4 */
diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h
index 999b54b70..0f1cb07dc 100644
--- a/src/theory/arith/basic.h
+++ b/src/theory/arith/basic.h
@@ -1,7 +1,8 @@
-
+#include "expr/node.h"
#include "expr/attribute.h"
+
#ifndef __CVC4__THEORY__ARITH__BASIC_H
#define __CVC4__THEORY__ARITH__BASIC_H
@@ -15,7 +16,7 @@ typedef expr::Attribute<IsBasicAttrID, bool> IsBasic;
inline bool isBasic(TNode x){
- return x.hasAttribute(IsBasic());
+ return x.getAttribute(IsBasic());
}
inline void makeBasic(TNode x){
diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
new file mode 100644
index 000000000..90529529a
--- /dev/null
+++ b/src/theory/arith/delta_rational.cpp
@@ -0,0 +1,10 @@
+
+#include "theory/arith/delta_rational.h"
+
+using namespace std;
+using namespace CVC4;
+
+std::ostream& CVC4::operator<<(std::ostream& os, const DeltaRational& dq){
+ return os << "(" << dq.getNoninfintestimalPart()
+ << "," << dq.getInfintestimalPart() << ")";
+}
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 5fd4d4e07..c84a28e3d 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -3,10 +3,14 @@
#include "util/integer.h"
#include "util/rational.h"
+#include <ostream>
+
#ifndef __CVC4__THEORY__ARITH__DELTA_RATIONAL_H
#define __CVC4__THEORY__ARITH__DELTA_RATIONAL_H
+namespace CVC4 {
+
/**
* A DeltaRational is a pair of rationals (c,k) that represent the number
* c + kd
@@ -18,11 +22,19 @@ private:
CVC4::Rational k;
public:
- DeltaRational() : c(0), k(0) {}
- DeltaRational(const CVC4::Rational& base) : c(base), k(0) {}
+ DeltaRational() : c(0,1), k(0,1) {}
+ DeltaRational(const CVC4::Rational& base) : c(base), k(0,1) {}
DeltaRational(const CVC4::Rational& base, const CVC4::Rational& coeff) :
c(base), k(coeff) {}
+ const CVC4::Rational& getInfintestimalPart() const {
+ return k;
+ }
+
+ const CVC4::Rational& getNoninfintestimalPart() const {
+ return c;
+ }
+
DeltaRational operator+(const DeltaRational& other) const{
CVC4::Rational tmpC = c+other.c;
CVC4::Rational tmpK = k+other.k;
@@ -58,7 +70,7 @@ public:
return !(*this <= other);
}
- DeltaRational& operator=(DeltaRational& other){
+ DeltaRational& operator=(const DeltaRational& other){
c = other.c;
k = other.k;
return *(this);
@@ -79,4 +91,8 @@ public:
}
};
+std::ostream& operator<<(std::ostream& os, const DeltaRational& n);
+
+}/* CVC4 namespace */
+
#endif /* __CVC4__THEORY__ARITH__DELTA_RATIONAL_H */
diff --git a/src/theory/arith/normal.h b/src/theory/arith/normal.h
index 7f8192a7d..0dbd7355a 100644
--- a/src/theory/arith/normal.h
+++ b/src/theory/arith/normal.h
@@ -12,7 +12,7 @@ typedef expr::Attribute<IsNormalAttrID, bool> IsNormal;
inline bool isNormalized(TNode x){
- return x.hasAttribute(IsNormal());
+ return x.getAttribute(IsNormal());
}
struct NormalFormAttrID;
diff --git a/src/theory/arith/normal_form_notes.txt b/src/theory/arith/normal_form_notes.txt
index 30786e980..a692ef471 100644
--- a/src/theory/arith/normal_form_notes.txt
+++ b/src/theory/arith/normal_form_notes.txt
@@ -453,3 +453,114 @@ bool isNormalFormAtom(TNode n){
return false;
}
}
+
+/***********************************************/
+/***********************************************/
+/******************* DRAFT 4 *******************/
+/***********************************************/
+/***********************************************/
+
+/** DRAFT 4
+ * variable := n
+ * guards
+ * n getMetaKind() == metakind::VARIABLE
+
+ * constant := n
+ * guards
+ n.getKind() == kind::CONST_RATIONAL
+
+ * monomial := variable | (* [variable])
+ * guards
+ * len [variable] >= 2
+ * isSorted nodeOrder (getMList monomial)
+
+
+ * coeff_mono := monomial | (* coeff monomial)
+ * guards
+ * coeff is renaming for constant
+ coeff \not\in {0,1}
+
+ * sum := coeff_mono | (+ [coeff_mono])
+ * guards
+ * len [coeff_mono] >= 2
+ * isStronglySorted cmono_cmp [coeff_mono]
+
+ * cons_sum := sum | (+ constant_1 sum) | constant_0
+ * guards
+ * constant_1, constant_0 are accepted by constant
+ * constant_1 != 1
+
+ * comparison := leads_with_one |><| constant
+ * guards
+ * |><| is GEQ, EQ, LEQ
+ * isStronglySorted cmono_cmp (monomial::[coeff_monomial])
+ * leads with_one is a subexpression of sum s.t. it is also accepted by
+ * leads_with_one := monomial | (+ monomial [coeff_monomial])
+
+ * Normal Form for terms := cons_sum
+ * Normal Form for atoms := TRUE | FALSE | comparison | (not comparison)
+ *
+ * Important Notes:
+ *
+ * The languages for each are stratified. i.e. it is either the case that
+ * they or all of their children belong to a language that is strictly
+ * smaller according to the following partial order.
+ * constant -> monomial -> coeff_mono -> sum -> cons_sum
+ * variable comparison
+ * This partial order is not unique, but it is simple.
+ *
+ * This gives rise to the notion of the tightest language that accepts a node,
+ * which is simply the least according to the stratification order above.
+ *
+ * Each subexpression of a normal form is also a normal form.
+ *
+ * The tightest language that accepts a node does not always indicate the
+ * tighest language of the children:
+ * (+ v1 (* v1 v2) (* 2 (* v1 v2 v2)))
+
+ * TAGGING:
+ * A node in normal form is tagged with the tightest binding above that
+ * accepts/generates it.
+ * All subexpressions are also in normal form and are also tagged.
+ * The tags for terms are as follows:
+ * enum { CONSTANT, VARIABLE, MONOMIAL, COEFF_MONOMIAL, SUM, CONS_SUM};
+ */
+
+ Auxillary
+ let rec tuple_cmp elem_cmp pairs_list =
+ match pair_list with
+ [] -> 0
+ |(x,y)::ps -> let cmp_res = elem_cmp x y in
+ if cmp_res <> 0
+ then cmp_res
+ else tuple_cmp elem_cmp ps
+
+ let lex_cmp elem_cmp l0 l1 =
+ if len l0 == len l1
+ then tuple_cmp elem_cmp (zip l0 l1)
+ else (len l0) - (len l1)
+
+ let rec adjacent l =
+ mathc l with
+ a::b::xs -> (a,b)::(adjacent b::xs)
+ | _ -> []
+
+ let isWeaklySorted cmp l =
+ forall (fun (x,y) -> cmp x y <= 0) (adjacent l)
+
+ let isStronglySorted cmp l =
+ forall (fun (x,y) -> cmp x y < 0) (adjacent l)
+
+ let getMList monomial =
+ match monomial with
+ variable -> [variable]
+ |(* [variable]) -> [variable]
+
+ let drop_coeff coeff_mono =
+ match coeff_mono in
+ monomial -> monomial
+ |(* coeff monomial) -> monomial
+
+let mono_cmp m0 m1 = lex_cmp nodeOrder (getMList m0) (getMList m1)
+let cmono_cmp cm0 cm1 = mono_cmp (drop_coeff cm0) (drop_coeff cm1)
+
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
new file mode 100644
index 000000000..e3347df64
--- /dev/null
+++ b/src/theory/arith/partial_model.cpp
@@ -0,0 +1,223 @@
+
+#include "theory/arith/partial_model.h"
+#include "util/output.h"
+
+using namespace std;
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+using namespace CVC4::theory::arith::partial_model;
+
+void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ d_UpperBoundMap[x] = r;
+}
+
+void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ d_LowerBoundMap[x] = r;
+}
+
+void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ if(d_savingAssignments){
+ d_history.push_back(make_pair(x,r));
+ }
+
+ DeltaRational* c;
+ if(x.getAttribute(partial_model::Assignment(), c)){
+ *c = r;
+ Debug("partial_model") << "pm: updating the assignment to" << x
+ << " now " << r <<endl;
+ }else{
+ Debug("partial_model") << "pm: constructing an assignment for " << x
+ << " initially " << r <<endl;
+
+ c = new DeltaRational(r);
+ x.setAttribute(partial_model::Assignment(), c);
+ }
+}
+
+/** Must know that the bound exists both calling this! */
+DeltaRational ArithPartialModel::getUpperBound(TNode x) const {
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+ Assert(i != d_UpperBoundMap.end());
+
+ return DeltaRational((*i).second);
+}
+
+DeltaRational ArithPartialModel::getLowerBound(TNode x) const{
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+ Assert(i != d_LowerBoundMap.end());
+
+ return DeltaRational((*i).second);
+}
+
+
+DeltaRational ArithPartialModel::getAssignment(TNode x) const{
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ DeltaRational* assign;
+ AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+ return *assign;
+}
+
+
+void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ Debug("partial_model") << "setLowerConstraint("
+ << x << ":" << constraint << ")" << endl;
+
+ x.setAttribute(partial_model::LowerConstraint(),constraint);
+}
+
+void ArithPartialModel::setUpperConstraint(TNode x, TNode constraint){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ Debug("partial_model") << "setUpperConstraint("
+ << x << ":" << constraint << ")" << endl;
+
+ x.setAttribute(partial_model::UpperConstraint(),constraint);
+}
+
+TNode ArithPartialModel::getLowerConstraint(TNode x){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ TNode ret;
+ AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
+ return ret;
+}
+
+TNode ArithPartialModel::getUpperConstraint(TNode x){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ TNode ret;
+ AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
+ return ret;
+}
+
+// TNode CVC4::theory::arith::getLowerConstraint(TNode x){
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+// TNode ret;
+// AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
+// return ret;
+// }
+
+// TNode CVC4::theory::arith::getUpperConstraint(TNode x){
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+// TNode ret;
+// AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
+// return ret;
+// }
+
+
+bool ArithPartialModel::belowLowerBound(TNode x, DeltaRational& c, bool strict){
+ CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+ if(i == d_LowerBoundMap.end()){
+ // l = -\intfy
+ // ? c < -\infty |- _|_
+ return false;
+ }
+
+ DeltaRational l = (*i).second;
+
+ if(strict){
+ return c < l;
+ }else{
+ return c <= l;
+ }
+}
+
+bool ArithPartialModel::aboveUpperBound(TNode x, DeltaRational& c, bool strict){
+ CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+ if(i == d_UpperBoundMap.end()){
+ // u = -\intfy
+ // ? u < -\infty |- _|_
+ return false;
+ }
+ DeltaRational u = (*i).second;
+
+ if(strict){
+ return c > u;
+ }else{
+ return c >= u;
+ }
+}
+
+bool ArithPartialModel::strictlyBelowUpperBound(TNode x){
+ DeltaRational* assign;
+ AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+
+ CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+ if(i == d_UpperBoundMap.end()){// u = \infty
+ return true;
+ }
+ DeltaRational u = (*i).second;
+
+ return *assign < u;
+}
+
+bool ArithPartialModel::strictlyAboveLowerBound(TNode x){
+ DeltaRational* assign;
+ AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+
+ CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+ if(i == d_LowerBoundMap.end()){// l = \infty
+ return true;
+ }
+ DeltaRational l = (*i).second;
+ return l < *assign;
+}
+
+bool ArithPartialModel::assignmentIsConsistent(TNode x){
+ DeltaRational beta = getAssignment(x);
+
+ bool above_li = !belowLowerBound(x,beta,true);
+ bool below_ui = !aboveUpperBound(x,beta,true);
+
+ //l_i <= beta(x_i) <= u_i
+ return above_li && below_ui;
+}
+
+void ArithPartialModel::beginRecordingAssignments(){
+ Assert(!d_savingAssignments);
+ Assert(d_history.empty());
+
+ d_savingAssignments = true;
+}
+
+
+void ArithPartialModel::stopRecordingAssignments(bool revert){
+ Assert(d_savingAssignments);
+
+ d_savingAssignments = false;
+
+ if(revert){
+ while(!d_history.empty()){
+ pair<TNode, DeltaRational>& curr = d_history.back();
+ d_history.pop_back();
+
+ TNode x = curr.first;
+
+ DeltaRational* c;
+ bool hasAssignment = x.getAttribute(partial_model::Assignment(), c);
+ Assert(hasAssignment);
+
+ *c = curr.second;
+ }
+ }else{
+ d_history.clear();
+ }
+
+}
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index a0f35f9db..5a0b662f8 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -1,9 +1,11 @@
-#include "context/cdlist.h"
#include "context/context.h"
+#include "context/cdmap.h"
#include "theory/arith/delta_rational.h"
+#include "expr/attribute.h"
#include "expr/node.h"
+#include <deque>
#ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
#define __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
@@ -12,8 +14,6 @@ namespace CVC4 {
namespace theory {
namespace arith {
-typedef CVC4::context::CDList<TNode> BoundsList;
-
namespace partial_model {
struct DeltaRationalCleanupStrategy{
static void cleanup(DeltaRational* dq){
@@ -22,316 +22,130 @@ struct DeltaRationalCleanupStrategy{
}
};
-struct AssignmentAttrID;
-typedef expr::Attribute<AssignmentAttrID,DeltaRational*,DeltaRationalCleanupStrategy> Assignment;
-
-// TODO should have a cleanup see bug #110
-struct LowerBoundAttrID;
-typedef expr::CDAttribute<LowerBoundAttrID,DeltaRational*> LowerBound;
-
-// TODO should have a cleanup see bug #110
-struct UpperBoundAttrID;
-typedef expr::CDAttribute<UpperBoundAttrID,DeltaRational*> UpperBound;
-
-struct LowerConstraintAttrID;
-typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint;
-
-struct UpperConstraintAttrID;
-typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint;
-
-typedef CVC4::context::CDList<TNode> BoundsList;
-
-struct BoundsListCleanupStrategy{
- static void cleanup(BoundsList* bl){
- Debug("arithgc") << "cleaning up " << bl << "\n";
- bl->deleteSelf();
- }
-};
-
-
-/** Unique name to use for constructing ECAttr. */
-struct BoundsListID;
+struct AssignmentAttrID {};
+typedef expr::Attribute<AssignmentAttrID,
+ DeltaRational*,
+ DeltaRationalCleanupStrategy> Assignment;
/**
- * BoundsListAttr is the attribute that maps a node to atoms .
+ * This defines a context dependent delta rational map.
+ * This is used to keep track of the current lower and upper bounds on
+ * each variable. This information is conext dependent.
+ */
+typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
+/* Side disucssion for why new tables are introduced instead of using the attribute
+ * framework.
+ * It comes down to that the obvious ways to use the current attribute framework do
+ * do not provide a terribly satisfying answer.
+ * - Suppose the type of the attribute is CD and maps to type DeltaRational.
+ * Well it can't map to a DeltaRational, and it thus it will be a DeltaRational*
+ * However being context dependent means givening up cleanup functions.
+ * So this leaks memory.
+ * - Suppose the type of the attribute is CD and the type mapped to
+ * was a Node wrapping a CONST_DELTA_RATIONAL.
+ * This was rejected for inefficiency, and uglyness.
+ * Inefficiency: Every lookup and comparison will require going through the
+ * massaging in between a node and the constant being wrapped. Every update
+ * requires going through the additional expense of creating at least 1 node.
+ * The Uglyness: If this was chosen it would also suggest using comparisons against
+ * DeltaRationals for the tracking the constraints for conflict analysis.
+ * This seems to invite misuse and introducing Nodes that should probably not escape
+ * arith.
+ * - Suppose that the of the attribute was not CD and mapped to a CDO<DeltaRational*>
+ * or similarly a ContextObj that wraps a DeltaRational*.
+ * This is currently rejected just because this is difficult to get right,
+ * and maintain. However with enough effort this the best solution is probably of
+ * this form.
*/
-typedef expr::Attribute<BoundsListID,
- BoundsList*,
- BoundsListCleanupStrategy> BoundsListAttr;
-
-}; /*namespace partial_model*/
-struct TheoryArithPropagatedID;
-typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
/**
- * Validates that a node constraint has the following form:
- * constraint: x |><| c
- * where |><| is either <, <=, ==, >=, LT and c is a constant rational.
+ * This is the literal that was asserted in the current context to the theory
+ * that asserted the tightest lower bound on a variable.
+ * For example: for a variable x this could be the constraint (>= x 4) or (not (<= x 50))
+ * Note the strong correspondence between this and LowerBoundMap.
+ * This is used during conflict analysis.
*/
-bool validateConstraint(TNode constraint){
- using namespace CVC4::kind;
- switch(constraint.getKind()){
- case LT:case LEQ: case EQUAL: case GEQ: case GT: break;
- default: return false;
- }
-
- if(constraint[0].getMetaKind() != metakind::VARIABLE) return false;
- return constraint[1].getKind() == CONST_RATIONAL;
-}
-
-void addBound(TNode constraint){
- Assert(validateConstraint(constraint));
- TNode x = constraint[0];
-
- BoundsList* bl;
- if(!x.getAttribute(partial_model::BoundsListAttr(), bl)){
- //TODO
- context::Context* context = NULL;
- bl = new (true) BoundsList(context);
- x.setAttribute(partial_model::BoundsListAttr(), bl);
- }
- bl->push_back(constraint);
-}
-
-inline int deltaCoeff(Kind k){
- switch(k){
- case kind::LT:
- return -1;
- case kind::GT:
- return 1;
- default:
- return 0;
- }
-}
-
+struct LowerConstraintAttrID {};
+typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint;
-inline bool negateBoundPropogation(CVC4::Kind k, bool isLowerBound){
- /* !isLowerBound
- * [x <= u && u < c] \=> x < c
- * [x <= u && u < c] \=> x <= c
- * [x <= u && u < c] \=> !(x == c)
- * [x <= u && u < c] \=> !(x >= c)
- * [x <= u && u < c] \=> !(x > c)
- */
- /* isLowerBound
- * [x >= l && l > c] \=> x > c
- * [x >= l && l > c] \=> x >= c
- * [x >= l && l > c] \=> !(x == c)
- * [x >= l && l > c] \=> !(x <= c)
- * [x >= l && l > c] \=> !(x < c)
- */
- using namespace CVC4::kind;
- switch(k){
- case LT:
- case LEQ:
- return isLowerBound;
- case EQUAL:
- return true;
- case GEQ:
- case GT:
- return !isLowerBound;
- default:
- Unreachable();
- return false;
- }
-}
+/**
+ * See the documentation for LowerConstraint.
+ */
+struct UpperConstraintAttrID {};
+typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint;
-void propogateBound(TNode constraint, OutputChannel& oc, bool isLower){
- constraint.setAttribute(TheoryArithPropagated(),true);
- bool neg = negateBoundPropogation(constraint.getKind(), isLower);
- if(neg){
- oc.propagate(constraint.notNode(),false);
- }else{
- oc.propagate(constraint,false);
- }
-}
-
-void propagateBoundConstraints(TNode x, OutputChannel& oc){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
- DeltaRational* l;
- DeltaRational* u;
- bool hasLowerBound = x.getAttribute(partial_model::LowerBound(), l);
- bool hasUpperBound = x.getAttribute(partial_model::UpperBound(), u);
-
- if(!(hasLowerBound || hasUpperBound)) return;
- BoundsList* bl;
-
- if(!x.getAttribute(partial_model::BoundsListAttr(), bl)) return;
-
- for(BoundsList::const_iterator iter = bl->begin(); iter != bl->end(); ++iter){
- TNode constraint = *iter;
- if(constraint.hasAttribute(TheoryArithPropagated())){
- continue;
- }
- //TODO improve efficiency Rational&
- Rational c = constraint[1].getConst<Rational>();
- Rational k(Integer(deltaCoeff(constraint.getKind())));
- DeltaRational ec(c, k);
- if(hasUpperBound && (*u) < ec ){
- propogateBound(constraint, oc, false);
- }
- if(hasLowerBound && (*l) > ec ){
- propogateBound(constraint, oc, true);
- }
- }
-}
-
-void setUpperBound(TNode x, DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* c;
- if(x.getAttribute(partial_model::UpperBound(), c)){
- *c = r;
- }else{
- c = new DeltaRational(r);
- x.setAttribute(partial_model::UpperBound(), c);
- }
-}
-
-void setLowerBound(TNode x, DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* c;
- if(x.getAttribute(partial_model::LowerBound(), c)){
- *c = r;
- }else{
- c = new DeltaRational(r);
- x.setAttribute(partial_model::LowerBound(), c);
- }
-}
-void setAssignment(TNode x, DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* c;
- if(x.getAttribute(partial_model::Assignment(), c)){
- *c = r;
- }else{
- c = new DeltaRational(r);
- x.setAttribute(partial_model::Assignment(), c);
- }
-}
+}; /*namespace partial_model*/
-/** Must know that the bound exists both calling this! */
-DeltaRational getUpperBound(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::UpperBound(),assign));
- return *assign;
-}
+struct TheoryArithPropagatedID {};
+typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
-DeltaRational getLowerBound(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::LowerBound(),assign));
- return *assign;
-}
+class ArithPartialModel {
+private:
+ partial_model::CDDRationalMap d_LowerBoundMap;
+ partial_model::CDDRationalMap d_UpperBoundMap;
-DeltaRational getAssignment(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ typedef std::pair<TNode, DeltaRational> HistoryPair;
+ typedef std::deque< HistoryPair > HistoryStack;
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
- return *assign;
-}
+ HistoryStack d_history;
-void setLowerConstraint(TNode constraint){
- TNode x = constraint[0];
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ bool d_savingAssignments;
- x.setAttribute(partial_model::LowerConstraint(),constraint);
-}
+public:
-void setUpperConstraint(TNode constraint){
- TNode x = constraint[0];
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ ArithPartialModel(context::Context* c):
+ d_LowerBoundMap(c),
+ d_UpperBoundMap(c),
+ d_history(),
+ d_savingAssignments(false)
+ { }
- x.setAttribute(partial_model::UpperConstraint(),constraint);
-}
-TNode getLowerConstraint(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ void setLowerConstraint(TNode x, TNode constraint);
+ void setUpperConstraint(TNode x, TNode constraint);
+ TNode getLowerConstraint(TNode x);
+ TNode getUpperConstraint(TNode x);
- TNode ret;
- AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
- return ret;
-}
-TNode getUpperConstraint(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ void beginRecordingAssignments();
- TNode ret;
- AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
- return ret;
-}
+ /* */
+ void stopRecordingAssignments(bool revert);
-/**
- * x <= l
- * ? c < l
- */
-bool belowLowerBound(TNode x, DeltaRational& c, bool strict){
- DeltaRational* l;
- if(!x.getAttribute(partial_model::LowerBound(), l)){
- // l = -\intfy
- // ? c < -\infty |- _|_
- return false;
- }
- if(strict){
- return c < *l;
- }else{
- return c <= *l;
- }
-}
+ void setUpperBound(TNode x, const DeltaRational& r);
+ void setLowerBound(TNode x, const DeltaRational& r);
+ void setAssignment(TNode x, const DeltaRational& r);
-/**
- * x <= u
- * ? c < u
- */
-bool aboveUpperBound(TNode x, DeltaRational& c, bool strict){
- DeltaRational* u;
- if(!x.getAttribute(partial_model::UpperBound(), u)){
- // c = \intfy
- // ? c > \infty |- _|_
- return false;
- }
+ /** Must know that the bound exists before calling this! */
+ DeltaRational getUpperBound(TNode x) const;
+ DeltaRational getLowerBound(TNode x) const;
+ DeltaRational getAssignment(TNode x) const;
- if(strict){
- return c > *u;
- }else{
- return c >= *u;
- }
-}
-bool strictlyBelowUpperBound(TNode x){
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+ /**
+ * x <= l
+ * ? c < l
+ */
+ bool belowLowerBound(TNode x, DeltaRational& c, bool strict);
- DeltaRational* u;
- if(!x.getAttribute(partial_model::UpperBound(), u)){ // u = \infty
- return true;
- }
- return *assign < *u;
-}
+ /**
+ * x <= u
+ * ? c < u
+ */
+ bool aboveUpperBound(TNode x, DeltaRational& c, bool strict);
-bool strictlyAboveLowerBound(TNode x){
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+ bool strictlyBelowUpperBound(TNode x);
+ bool strictlyAboveLowerBound(TNode x);
+ bool assignmentIsConsistent(TNode x);
+};
- DeltaRational* l;
- if(!x.getAttribute(partial_model::LowerBound(), l)){ // l = -\infty
- return true;
- }
- return *l < *assign;
-}
-bool assignmentIsConsistent(TNode x){
- DeltaRational beta = getAssignment(x);
- //l_i <= beta(x_i) <= u_i
- return !aboveUpperBound(x,beta, true) && !belowLowerBound(x,beta,true);
-}
}; /* namesapce arith */
}; /* namespace theory */
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 10daa0c13..2ab94c195 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -196,7 +196,8 @@ public:
//Assert(isAdmissableVariable(var));
Assert(var.getAttribute(IsBasic()));
- Assert(d_basicVars.find(var) != d_basicVars.end());
+ //The new basic variable cannot already be a basic variable
+ Assert(d_basicVars.find(var) == d_basicVars.end());
d_basicVars.insert(var);
d_rows[var] = new Row(var,sum);
}
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 50d4fb633..390cb60aa 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1,6 +1,7 @@
#include "expr/node.h"
#include "expr/kind.h"
#include "expr/metakind.h"
+#include "expr/node_builder.h"
#include "util/rational.h"
#include "util/integer.h"
@@ -12,11 +13,13 @@
#include "theory/arith/tableau.h"
#include "theory/arith/normal.h"
#include "theory/arith/slack.h"
+#include "theory/arith/basic.h"
#include "theory/arith/arith_rewriter.h"
#include "theory/arith/theory_arith.h"
#include <map>
+#include <stdint.h>
using namespace std;
@@ -26,10 +29,33 @@ using namespace CVC4::kind;
using namespace CVC4::theory;
using namespace CVC4::theory::arith;
+TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
+ Theory(c, out),
+ d_constants(NodeManager::currentNM()),
+ d_partialModel(c),
+ d_diseq(c),
+ d_preprocessed(c),
+ d_rewriter(&d_constants)
+{
+ uint64_t ass_id = partial_model::Assignment::getId();
+ Debug("arithsetup") << "Assignment: " << ass_id
+ << std::endl;
+}
+
bool isBasicSum(TNode n){
- Unimplemented();
- return false;
+ if(n.getKind() != kind::PLUS) return false;
+
+ for(TNode::const_iterator i=n.begin(); i!=n.end(); ++i){
+ TNode child = *i;
+ if(child.getKind() != MULT) return false;
+ if(child[0].getKind() != CONST_RATIONAL) return false;
+ for(unsigned j=1; j<child.getNumChildren(); ++j){
+ TNode var = child[j];
+ if(var.getMetaKind() != metakind::VARIABLE) return false;
+ }
+ }
+ return true;
}
Kind multKind(Kind k){
@@ -47,17 +73,33 @@ Kind multKind(Kind k){
void registerAtom(TNode rel){
- addBound(rel);
+ //addBound(rel);
//Anything else?
}
Node TheoryArith::rewrite(TNode n){
- return d_rewriter.rewrite(n);
+ Debug("arith") << "rewrite(" << n << ")" << endl;
+
+ Node result = d_rewriter.rewrite(n);
+ Debug("arith-rewrite") << "rewrite("
+ << n << " -> " << result
+ << ")" << endl;
+ return result;
}
void TheoryArith::registerTerm(TNode tn){
- if(tn.isAtomic()){
+ Debug("arith") << "registerTerm(" << tn << ")" << endl;
+
+ if(tn.getKind() == kind::BUILTIN) return;
+
+ if(tn.getMetaKind() == metakind::VARIABLE){
+ d_partialModel.setAssignment(tn,d_constants.d_ZERO_DELTA);
+ }
+
+ //TODO is an atom
+ if(isRelationOperator(tn.getKind())){
Node normalForm = (isNormalized(tn)) ? Node(tn) : rewrite(tn);
+ normalForm = (normalForm.getKind() == NOT) ? pushInNegation(normalForm):normalForm;
Kind k = normalForm.getKind();
if(k != kind::CONST_BOOLEAN){
@@ -71,7 +113,9 @@ void TheoryArith::registerTerm(TNode tn){
Node slack;
if(!left.getAttribute(Slack(), slack)){
//TODO
- //slack = NodeManager::currentNM()->mkVar(RealType());
+ TypeNode real_type = NodeManager::currentNM()->realType();
+ slack = NodeManager::currentNM()->mkVar(real_type);
+ d_partialModel.setAssignment(slack,d_constants.d_ZERO_DELTA);
left.setAttribute(Slack(), slack);
makeBasic(slack);
@@ -81,10 +125,13 @@ void TheoryArith::registerTerm(TNode tn){
d_out->lemma(slackEqLeft);
d_tableau.addRow(slackEqLeft);
- }
- Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
- registerAtom(rewritten);
+ Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
+ registerAtom(rewritten);
+ }else{
+ Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
+ registerAtom(rewritten);
+ }
}else{
Assert(left.getMetaKind() == metakind::VARIABLE);
Assert(right.getKind() == CONST_RATIONAL);
@@ -95,48 +142,56 @@ void TheoryArith::registerTerm(TNode tn){
}
/* procedure AssertUpper( x_i <= c_i) */
-void TheoryArith::AssertUpper(TNode n){
+void TheoryArith::AssertUpper(TNode n, TNode original){
TNode x_i = n[0];
Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
DeltaRational c_i(n[1].getConst<Rational>(), dcoeff);
- if(aboveUpperBound(x_i, c_i, false) ){
+
+ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
+
+
+ if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){
return; //sat
}
- if(belowLowerBound(x_i, c_i, true)){
- d_out->conflict(n);
+ if(d_partialModel.belowLowerBound(x_i, c_i, true)){
+ Node conflict = NodeManager::currentNM()->mkNode(AND, d_partialModel.getLowerConstraint(x_i), original);
+ d_out->conflict(conflict);
return;
}
- setUpperConstraint(n);
- setUpperBound(x_i, c_i);
+ d_partialModel.setUpperConstraint(x_i,original);
+ d_partialModel.setUpperBound(x_i, c_i);
if(!isBasic(x_i)){
- if(getAssignment(x_i) > c_i){
+ if(d_partialModel.getAssignment(x_i) > c_i){
update(x_i, c_i);
}
}
}
/* procedure AssertLower( x_i >= c_i ) */
-void TheoryArith::AssertLower(TNode n){
+void TheoryArith::AssertLower(TNode n, TNode orig){
TNode x_i = n[0];
Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
DeltaRational c_i(n[1].getConst<Rational>(),dcoeff);
- if(belowLowerBound(x_i, c_i, false)){
+ Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
+
+ if(d_partialModel.belowLowerBound(x_i, c_i, false)){
return; //sat
}
- if(aboveUpperBound(x_i, c_i, true)){
- d_out->conflict(n);
+ if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
+ Node conflict = NodeManager::currentNM()->mkNode(AND, d_partialModel.getUpperConstraint(x_i), orig);
+ d_out->conflict(conflict);
return;
}
- setLowerConstraint(n);
- setLowerBound(x_i, c_i);
+ d_partialModel.setLowerConstraint(x_i,orig);
+ d_partialModel.setLowerBound(x_i, c_i);
if(!isBasic(x_i)){
- if(getAssignment(x_i) > c_i){
+ if(d_partialModel.getAssignment(x_i) < c_i){
update(x_i, c_i);
}
}
@@ -144,7 +199,10 @@ void TheoryArith::AssertLower(TNode n){
void TheoryArith::update(TNode x_i, DeltaRational& v){
- DeltaRational assignment_x_i = getAssignment(x_i);
+ DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
+
+ Debug("arith") <<"update " << x_i << ": "
+ << assignment_x_i << "|-> " << v << endl;
DeltaRational diff = v - assignment_x_i;
for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
@@ -155,29 +213,29 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
Rational& a_ji = row_j->lookup(x_i);
- DeltaRational assignment = getAssignment(x_j);
+ DeltaRational assignment = d_partialModel.getAssignment(x_j);
DeltaRational nAssignment = assignment+(diff * a_ji);
- setAssignment(x_j, nAssignment);
+ d_partialModel.setAssignment(x_j, nAssignment);
}
- setAssignment(x_i, v);
+ d_partialModel.setAssignment(x_i, v);
}
void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
Row* row_i = d_tableau.lookup(x_i);
- Rational& a_ij = row_i->lookup(x_i);
+ Rational& a_ij = row_i->lookup(x_j);
- DeltaRational betaX_i = getAssignment(x_i);
+ DeltaRational betaX_i = d_partialModel.getAssignment(x_i);
Rational inv_aij = a_ij.inverse();
DeltaRational theta = (v - betaX_i)*inv_aij;
- setAssignment(x_i, v);
+ d_partialModel.setAssignment(x_i, v);
- DeltaRational tmp = getAssignment(x_j) + theta;
- setAssignment(x_j, tmp);
+ DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta;
+ d_partialModel.setAssignment(x_j, tmp);
for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
basicIter != d_tableau.end();
@@ -187,8 +245,8 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
if(x_k != x_i){
DeltaRational a_kj = row_k->lookup(x_j);
- DeltaRational nextAssignment = getAssignment(x_k) + theta;
- setAssignment(x_k, nextAssignment);
+ DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + theta;
+ d_partialModel.setAssignment(x_k, nextAssignment);
}
}
@@ -202,7 +260,7 @@ TNode TheoryArith::selectSmallestInconsistentVar(){
++basicIter){
TNode basic = *basicIter;
- if(!assignmentIsConsistent(basic)){
+ if(!d_partialModel.assignmentIsConsistent(basic)){
return basic;
}
}
@@ -219,12 +277,10 @@ TNode TheoryArith::selectSlackBelow(TNode x_i){ //beta(x_i) < l_i
TNode nonbasic = *nbi;
Rational a_ij = row_i->lookup(nonbasic);
- if(a_ij > d_constants.d_ZERO && strictlyBelowUpperBound(nonbasic)){
+ if(a_ij > d_constants.d_ZERO && d_partialModel.strictlyBelowUpperBound(nonbasic)){
return nonbasic;
- }else if(a_ij < d_constants.d_ZERO && strictlyAboveLowerBound(nonbasic)){
+ }else if(a_ij < d_constants.d_ZERO && d_partialModel.strictlyAboveLowerBound(nonbasic)){
return nonbasic;
- }else{
- Unreachable();
}
}
return TNode::null();
@@ -239,38 +295,43 @@ TNode TheoryArith::selectSlackAbove(TNode x_i){ // beta(x_i) > u_i
TNode nonbasic = *nbi;
Rational a_ij = row_i->lookup(nonbasic);
- if(a_ij < d_constants.d_ZERO && strictlyBelowUpperBound(nonbasic)){
+ if(a_ij < d_constants.d_ZERO && d_partialModel.strictlyBelowUpperBound(nonbasic)){
return nonbasic;
- }else if(a_ij > d_constants.d_ZERO && strictlyAboveLowerBound(nonbasic)){
+ }else if(a_ij > d_constants.d_ZERO && d_partialModel.strictlyAboveLowerBound(nonbasic)){
return nonbasic;
- }else{
- Unreachable();
}
}
+
return TNode::null();
}
-TNode TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
+Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
+ Debug("arith") << "updateInconsistentVars" << endl;
+ d_partialModel.beginRecordingAssignments();
while(true){
TNode x_i = selectSmallestInconsistentVar();
if(x_i == Node::null()){
+ d_partialModel.stopRecordingAssignments(false);
return Node::null(); //sat
}
- DeltaRational beta_i = getAssignment(x_i);
- DeltaRational l_i = getLowerBound(x_i);
- DeltaRational u_i = getUpperBound(x_i);
- if(belowLowerBound(x_i, beta_i, true)){
+ DeltaRational beta_i = d_partialModel.getAssignment(x_i);
+
+ if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
+ DeltaRational l_i = d_partialModel.getLowerBound(x_i);
TNode x_j = selectSlackBelow(x_i);
if(x_j == TNode::null() ){
+ d_partialModel.stopRecordingAssignments(true);
return generateConflictBelow(x_i); //unsat
}
pivotAndUpdate(x_i, x_j, l_i);
- }else if(aboveUpperBound(x_i, beta_i, true)){
+ }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
+ DeltaRational u_i = d_partialModel.getUpperBound(x_i);
TNode x_j = selectSlackAbove(x_i);
if(x_j == TNode::null() ){
- return generateConflictAbove(x_j); //unsat
+ d_partialModel.stopRecordingAssignments(true);
+ return generateConflictAbove(x_i); //unsat
}
pivotAndUpdate(x_i, x_j, u_i);
}
@@ -281,7 +342,13 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){
Row* row_i = d_tableau.lookup(conflictVar);
NodeBuilder<> nb(kind::AND);
- nb << getUpperConstraint(conflictVar);
+ TNode bound = d_partialModel.getUpperConstraint(conflictVar);
+
+ Debug("arith") << "generateConflictAbove "
+ << "conflictVar " << conflictVar
+ << " " << bound << endl;
+
+ nb << bound;
typedef std::set<TNode>::iterator NonBasicIter;
@@ -292,19 +359,29 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){
Assert(a_ij != d_constants.d_ZERO);
if(a_ij < d_constants.d_ZERO){
- nb << getUpperConstraint(nonbasic);
+ bound = d_partialModel.getUpperConstraint(nonbasic);
+ Debug("arith") << "below 0 "<< nonbasic << " " << bound << endl;
+ nb << bound;
}else{
- nb << getLowerConstraint(nonbasic);
+ bound = d_partialModel.getLowerConstraint(nonbasic);
+ Debug("arith") << " above 0 "<< nonbasic << " " << bound << endl;
+ nb << bound;
}
}
Node conflict = nb;
return conflict;
}
+
Node TheoryArith::generateConflictBelow(TNode conflictVar){
Row* row_i = d_tableau.lookup(conflictVar);
NodeBuilder<> nb(kind::AND);
- nb << getLowerConstraint(conflictVar);
+ TNode bound = d_partialModel.getLowerConstraint(conflictVar);
+
+ Debug("arith") << "generateConflictBelow "
+ << "conflictVar " << conflictVar
+ << " " << bound << endl;
+ nb << bound;
typedef std::set<TNode>::iterator NonBasicIter;
@@ -315,40 +392,92 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){
Assert(a_ij != d_constants.d_ZERO);
if(a_ij < d_constants.d_ZERO){
- nb << getLowerConstraint(nonbasic);
+ TNode bound = d_partialModel.getLowerConstraint(nonbasic);
+ Debug("arith") << "Lower "<< nonbasic << " " << bound << endl;
+
+ nb << bound;
}else{
- nb << getUpperConstraint(nonbasic);
+ TNode bound = d_partialModel.getUpperConstraint(nonbasic);
+ Debug("arith") << "Upper "<< nonbasic << " " << bound << endl;
+
+ nb << bound;
}
}
- Node conflict = nb;
+ Node conflict (nb.constructNode());
return conflict;
}
+//TODO get rid of this!
+Node TheoryArith::simulatePreprocessing(TNode n){
+ if(n.getKind() == NOT){
+ Node sub = simulatePreprocessing(n[0]);
+ return NodeManager::currentNM()->mkNode(NOT,sub);
+ }else{
+ Node rewritten = rewrite(n);
+ Kind k = rewritten.getKind();
+ if(!isRelationOperator(k)){
+ return rewritten;
+ }else if(rewritten[0].getMetaKind() == metakind::VARIABLE){
+ return rewritten;
+ }else {
+ TNode left = rewritten[0];
+ TNode right = rewritten[1];
+ Node slack;
+ if(!left.getAttribute(Slack(), slack)){
+ Unreachable("Slack must be have been created!");
+ }else{
+ return NodeManager::currentNM()->mkNode(k,slack,right);
+ }
+ }
+ }
+}
+
void TheoryArith::check(Effort level){
+ Debug("arith") << "TheoryArith::check begun" << std::endl;
+
while(!done()){
- Node assertion = get();
+ Node original = get();
+ Node assertion = simulatePreprocessing(original);
+ Debug("arith") << "arith assertion(" << original
+ << " \\-> " << assertion << ")" << std::endl;
- if(assertion.getKind() == NOT){
- assertion = pushInNegation(assertion);
- }
+ d_preprocessed.push_back(assertion);
switch(assertion.getKind()){
- case LT:
case LEQ:
- AssertUpper(assertion);
+ AssertUpper(assertion, original);
break;
case GEQ:
- case GT:
- AssertLower(assertion);
+ AssertLower(assertion, original);
break;
case EQUAL:
- AssertUpper(assertion);
- AssertLower(assertion);
+ AssertUpper(assertion, original);
+ AssertLower(assertion, original);
break;
case NOT:
- Assert(assertion[0].getKind() == EQUAL);
- d_diseq.push_back(assertion);
- break;
+ {
+ TNode atom = assertion[0];
+ switch(atom.getKind()){
+ case LEQ: //(not (LEQ x c)) <=> (GT x c)
+ {
+ Node pushedin = pushInNegation(assertion);
+ AssertLower(pushedin,original);
+ break;
+ }
+ case GEQ: //(not (GEQ x c) <=> (LT x c)
+ {
+ Node pushedin = pushInNegation(assertion);
+ AssertUpper(pushedin,original);
+ break;
+ }
+ case EQUAL:
+ d_diseq.push_back(assertion);
+ break;
+ default:
+ Unhandled();
+ }
+ break;
+ }
default:
Unhandled();
}
@@ -357,12 +486,13 @@ void TheoryArith::check(Effort level){
if(fullEffort(level)){
Node possibleConflict = updateInconsistentVars();
if(possibleConflict != Node::null()){
+ Debug("arith") << "Found a conflict " << possibleConflict << endl;
d_out->conflict(possibleConflict);
}
}
if(fullEffort(level)){
- NodeBuilder<> lemmas(AND);
+ bool enqueuedCaseSplit = false;
typedef context::CDList<Node>::const_iterator diseq_iterator;
for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){
Node assertion = *i;
@@ -370,15 +500,16 @@ void TheoryArith::check(Effort level){
TNode x_i = eq[0];
TNode c_i = eq[1];
DeltaRational constant = c_i.getConst<Rational>();
- if(getAssignment(x_i) == constant){
+ if(d_partialModel.getAssignment(x_i) == constant){
+ enqueuedCaseSplit = true;
Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
- Node disjunct = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
- lemmas<< disjunct;
+ Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
+ //d_out->enqueueCaseSplits(caseSplit);
}
}
- Node caseSplits = lemmas;
- //TODO
- //DemandCaseSplits(caseSplits);
+ if(enqueuedCaseSplit){
+ //d_out->caseSplit();
+ }
}
}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 82bb47eb4..ecdebd720 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -21,10 +21,12 @@
#include "theory/theory.h"
#include "context/context.h"
#include "context/cdlist.h"
+#include "expr/node.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/tableau.h"
#include "theory/arith/arith_rewriter.h"
+#include "theory/arith/partial_model.h"
namespace CVC4 {
namespace theory {
@@ -33,16 +35,19 @@ namespace arith {
class TheoryArith : public Theory {
private:
ArithConstants d_constants;
+ ArithPartialModel d_partialModel;
context::CDList<Node> d_diseq;
+ context::CDList<Node> d_preprocessed;
+ //TODO This is currently needed to save preprocessed nodes that may not
+ //currently have an outisde reference. Get rid of when preprocessing is occuring
+ //correctly.
+
Tableau d_tableau;
ArithRewriter d_rewriter;
public:
- TheoryArith(context::Context* c, OutputChannel& out) :
- Theory(c, out),
- d_constants(NodeManager::currentNM()), d_diseq(c), d_rewriter(&d_constants)
- {}
+ TheoryArith(context::Context* c, OutputChannel& out);
Node rewrite(TNode n);
@@ -53,11 +58,12 @@ public:
void explain(TNode n, Effort e) { Unimplemented(); }
private:
- void AssertLower(TNode n);
- void AssertUpper(TNode n);
+ void AssertLower(TNode n, TNode orig);
+ void AssertUpper(TNode n, TNode orig);
void update(TNode x_i, DeltaRational& v);
void pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v);
- TNode updateInconsistentVars();
+
+ Node updateInconsistentVars();
TNode selectSlackBelow(TNode x_i);
TNode selectSlackAbove(TNode x_i);
@@ -66,6 +72,9 @@ private:
Node generateConflictAbove(TNode conflictVar);
Node generateConflictBelow(TNode conflictVar);
+ //TODO get rid of this!
+ Node simulatePreprocessing(TNode n);
+
};
}/* CVC4::theory::arith namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index d9b7a4fa6..b559da562 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -261,7 +261,7 @@ public:
try {
//d_bool.check(effort);
d_uf.check(effort);
- //d_arith.check(effort);
+ d_arith.check(effort);
//d_arrays.check(effort);
//d_bv.check(effort);
} catch(const theory::Interrupted&) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback