summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arith/Makefile.am11
-rw-r--r--src/theory/arith/arith_constants.h38
-rw-r--r--src/theory/arith/arith_rewriter.cpp468
-rw-r--r--src/theory/arith/arith_rewriter.h92
-rw-r--r--src/theory/arith/arith_utilities.h128
-rw-r--r--src/theory/arith/basic.h33
-rw-r--r--src/theory/arith/delta_rational.h82
-rw-r--r--src/theory/arith/normal.h29
-rw-r--r--src/theory/arith/normal_form_notes.txt455
-rw-r--r--src/theory/arith/partial_model.h342
-rw-r--r--src/theory/arith/slack.h14
-rw-r--r--src/theory/arith/tableau.h243
-rw-r--r--src/theory/arith/theory_arith.cpp384
-rw-r--r--src/theory/arith/theory_arith.h40
-rw-r--r--src/util/rational.h21
15 files changed, 2373 insertions, 7 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index cb838f497..7c3e76d0a 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -6,6 +6,15 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libarith.la
libarith_la_SOURCES = \
- theory_arith.h
+ theory_arith.h \
+ theory_arith.cpp \
+ arith_rewriter.h \
+ arith_rewriter.cpp \
+ arith_utilities.h \
+ arith_constants.h \
+ basic.h \
+ normal.h \
+ slack.h \
+ tableau.h
EXTRA_DIST = kinds
diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h
new file mode 100644
index 000000000..d9419cd6b
--- /dev/null
+++ b/src/theory/arith/arith_constants.h
@@ -0,0 +1,38 @@
+
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "util/rational.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
+#define __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class ArithConstants{
+public:
+ Rational d_ZERO;
+ Rational d_ONE;
+ Rational d_NEGATIVE_ONE;
+
+ Node d_ZERO_NODE;
+ Node d_ONE_NODE;
+ Node d_NEGATIVE_ONE_NODE;
+
+ ArithConstants(NodeManager* nm) :
+ d_ZERO(0,1),
+ d_ONE(1,1),
+ d_NEGATIVE_ONE(-1,1),
+ d_ZERO_NODE(nm->mkConst(d_ZERO)),
+ d_ONE_NODE(nm->mkConst(d_ONE)),
+ d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE))
+ {}
+};
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
new file mode 100644
index 000000000..f3d3061d7
--- /dev/null
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -0,0 +1,468 @@
+
+#include "theory/arith/arith_rewriter.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/normal.h"
+
+#include <vector>
+#include <set>
+#include <stack>
+
+
+using namespace CVC4;
+using namespace CVC4::theory;
+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
+ * v |><| b
+ * Also writes relations with constants on both sides to TRUE or FALSE.
+ * If it can, it returns true and sets res to this value.
+ *
+ * This is for optimizing rewriteAtom() to avoid the more compuationally
+ * expensive general rewriting procedure.
+ *
+ * If simplification is not done, it returns Node::null()
+ */
+Node almostVarOrConstEqn(TNode atom, Kind k, TNode left, TNode right){
+ Assert(atom.getKind() == k);
+ Assert(isRelationOperator(k));
+ Assert(atom[0] == left);
+ Assert(atom[1] == right);
+ bool leftIsConst = left.getMetaKind() == kind::metakind::CONSTANT;
+ bool rightIsConst = right.getMetaKind() == kind::metakind::CONSTANT;
+
+ bool leftIsVar = left.getMetaKind() == kind::metakind::VARIABLE;
+ bool rightIsVar = right.getMetaKind() == kind::metakind::VARIABLE;
+
+ if(leftIsConst && rightIsConst){
+ Rational lc = coerceToRational(left);
+ Rational rc = coerceToRational(right);
+ bool res = evaluateConstantPredicate(k,lc, rc);
+ return mkBoolNode(res);
+ }else if(leftIsVar && rightIsConst){
+ return atom;
+ }else if(leftIsConst && rightIsVar){
+ return NodeManager::currentNM()->mkNode(multKind(k,-1),right,left);
+ }
+
+ return Node::null();
+}
+
+Node ArithRewriter::rewriteAtom(TNode atom){
+
+ Kind k = atom.getKind();
+ Assert(isRelationOperator(k));
+
+ // left |><| right
+ TNode left = atom[0];
+ TNode right = atom[1];
+
+ Node nf = almostVarOrConstEqn(atom, k,left,right);
+ if(nf != Node::null() ){
+ return nf;
+ }
+
+ //Transform this to: (left- right) |><| 0
+ Node diff = makeSubtractionNode(left, right);
+
+ Node rewritten = rewrite(diff);
+ // rewritten =_{Reals} left - right => rewritten |><| 0
+
+ if(rewritten.getMetaKind() == kind::metakind::CONSTANT){
+ // Case 1 rewritten : c
+ Rational c = rewritten.getConst<Rational>();
+ bool res = evaluateConstantPredicate(k, c, d_constants->d_ZERO);
+ nf = mkBoolNode(res);
+ }else if(rewritten.getMetaKind() == kind::metakind::VARIABLE){
+ // Case 2 rewritten : v
+ nf = NodeManager::currentNM()->mkNode(k, rewritten, d_constants->d_ZERO_NODE);
+ }else{
+ // Case 3 rewritten : (+ c p_1 p_2 ... p_N) | not(N=1 and c=0 and p_1.d=1)
+ Rational c = rewritten[0].getConst<Rational>();
+ c = -c;
+ TNode p_1 = rewritten[1];
+ Rational d = p_1[0].getConst<Rational>();
+ d = d.inverse();
+ c = c * d;
+ Node newRight = mkRationalNode(c);
+ Kind newKind = multKind(k, d.sgn());
+ int N = rewritten.getNumChildren() - 1;
+
+ if(N==1){
+ int M = p_1.getNumChildren()-1;
+ if(M == 1){ // v |><| b
+ TNode v = p_1[1];
+ nf = NodeManager::currentNM()->mkNode(newKind, v, newRight);
+ }else{ // p |><| b
+ Node newLeft = multPnfByNonZero(p_1, d);
+ nf = NodeManager::currentNM()->mkNode(newKind, newLeft, newRight);
+ }
+ }else{ //(+ p_1 .. p_N) |><| b
+ NodeBuilder<> plus;
+ for(int i=1; i<=N; ++i){
+ TNode p_i = rewritten[i];
+ plus << multPnfByNonZero(p_i, d);
+ }
+ Node newLeft = plus;
+ nf = NodeManager::currentNM()->mkNode(newKind, newLeft, newRight);
+ }
+ }
+
+ return nf;
+}
+
+
+/* cmp( (* d v_1 v_2 ... v_M), (* d' v'_1 v'_2 ... v'_M'):
+ * if(M == M'):
+ * then tupleCompare(v_i, v'_i)
+ * else M -M'
+ */
+struct pnfLessThan {
+ bool operator()(Node p0, Node p1) {
+ int p0_M = p0.getNumChildren() -1;
+ int p1_M = p1.getNumChildren() -1;
+ if(p0_M == p1_M){
+ for(int i=1; i<= p0_M; ++i){
+ if(p0[i] != p1[i]){
+ return p0[i] < p1[i];
+ }
+ }
+ return false; //p0 == p1 in this order
+ }else{
+ return p0_M < p1_M;
+ }
+ }
+};
+
+Node addPnfs(TNode p0, TNode p1){
+ //TODO asserts
+ Rational c0 = p0[0].getConst<Rational>();
+ Rational c1 = p1[0].getConst<Rational>();
+
+ int M = p0.getNumChildren();
+
+ Rational addedC = c0 + c1;
+ Node newC = mkRationalNode(addedC);
+ NodeBuilder<> nb(kind::PLUS);
+ nb << newC;
+ for(int i=1; i <= M; ++i){
+ nb << p0[i];
+ }
+ Node newPnf = nb;
+ return newPnf;
+}
+
+void sortAndCombineCoefficients(std::vector<Node>& pnfs){
+ using namespace std;
+
+ /* combined contains exactly 1 representative per for each pnf.
+ * This is maintained by combining the coefficients for pnfs.
+ * that is equal according to pnfLessThan.
+ */
+ typedef set<Node, pnfLessThan> PnfSet;
+ PnfSet combined;
+
+ for(vector<Node>::iterator i=pnfs.begin(); i != pnfs.end(); ++i){
+ Node pnf = *i;
+ PnfSet::iterator pos = combined.find(pnf);
+
+ if(pos == combined.end()){
+ combined.insert(pnf);
+ }else{
+ Node current = *pos;
+ Node sum = addPnfs(pnf, current);
+ combined.erase(pos);
+ combined.insert(sum);
+ }
+ }
+ pnfs.clear();
+ for(PnfSet::iterator i=combined.begin(); i != combined.end(); ++i){
+ Node pnf = *i;
+ pnfs.push_back(pnf);
+ }
+}
+
+Node ArithRewriter::var2pnf(TNode variable){
+ return NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_ONE_NODE,variable);
+}
+
+Node ArithRewriter::rewritePlus(TNode t){
+ using namespace std;
+
+ Rational accumulator;
+ vector<Node> pnfs;
+
+ for(TNode::iterator i = t.begin(); i!= t.end(); ++i){
+ TNode child = *i;
+ Node rewrittenChild = rewrite(child);
+
+ if(rewrittenChild.getMetaKind() == kind::metakind::CONSTANT){//c
+ Rational c = rewrittenChild.getConst<Rational>();
+ accumulator = accumulator + c;
+ }else if(rewrittenChild.getMetaKind() == kind::metakind::VARIABLE){ //v
+ Node pnf = var2pnf(rewrittenChild);
+ pnfs.push_back(pnf);
+ }else{ //(+ c p_1 p_2 ... p_N)
+ Rational c = rewrittenChild[0].getConst<Rational>();
+ accumulator = accumulator + c;
+ int N = rewrittenChild.getNumChildren() - 1;
+ for(int i=1; i<=N; ++i){
+ TNode pnf = rewrittenChild[i];
+ pnfs.push_back(pnf);
+ }
+ }
+ }
+ sortAndCombineCoefficients(pnfs);
+ if(pnfs.size() == 0){
+ return mkRationalNode(accumulator);
+ }
+
+ // pnfs.size() >= 1
+
+ //Enforce not(N=1 and c=0 and p_1.d=1)
+ if(pnfs.size() == 1){
+ Node p_1 = *(pnfs.begin());
+ if(p_1[0].getConst<Rational>() == d_constants->d_ONE){
+ if(accumulator == 0){ // 0 + (* 1 var) |-> var
+ Node var = p_1[1];
+ return var;
+ }
+ }
+ }
+
+ //We must be in this case
+ //(+ c p_1 p_2 ... p_N) | not(N=1 and c=0 and p_1.d=1)
+
+ NodeBuilder<> nb(kind::PLUS);
+ nb << mkRationalNode(accumulator);
+ for(vector<Node>::iterator i = pnfs.begin(); i != pnfs.end(); ++i){
+ nb << *i;
+ }
+
+ Node normalForm = nb;
+ return normalForm;
+}
+
+//Does not enforce
+//5) v_i are of metakind VARIABLE,
+//6) v_i are in increasing (not strict) nodeOrder,
+Node toPnf(Rational& c, std::set<Node>& variables){
+ NodeBuilder<> nb(kind::MULT);
+ nb << mkRationalNode(c);
+ for(std::set<Node>::iterator i = variables.begin(); i != variables.end(); ++i){
+ nb << *i;
+ }
+ Node pnf = nb;
+ return pnf;
+}
+
+Node distribute(TNode n, TNode sum){
+ NodeBuilder<> nb(kind::PLUS);
+ for(TNode::iterator i=sum.begin(); i!=sum.end(); ++i){
+ Node prod = NodeManager::currentNM()->mkNode(kind::MULT, n, *i);
+ nb << prod;
+ }
+ return nb;
+}
+Node distributeSum(TNode sum, TNode distribSum){
+ NodeBuilder<> nb(kind::PLUS);
+ for(TNode::iterator i=sum.begin(); i!=sum.end(); ++i){
+ Node dist = distribute(*i, distribSum);
+ for(Node::iterator j=dist.begin(); j!=dist.end(); ++j){
+ nb << *j;
+ }
+ }
+ return nb;
+}
+
+Node ArithRewriter::rewriteMult(TNode t){
+
+ using namespace std;
+
+ Rational accumulator(1,1);
+ set<Node> variables;
+ vector<Node> sums;
+ stack<pair<TNode, TNode::iterator> > mult_iterators;
+
+ mult_iterators.push(make_pair(t, t.begin()));
+ while(!mult_iterators.empty()){
+ pair<TNode, TNode::iterator> p = mult_iterators.top();
+ mult_iterators.pop();
+
+ TNode mult = p.first;
+ TNode::iterator i = p.second;
+
+ for(; i!= mult.end(); ++i){
+ TNode child = *i;
+ if(child.getKind() == kind::MULT){ //TODO add not rewritten already checks
+ ++i;
+ mult_iterators.push(make_pair(mult,i));
+ mult_iterators.push(make_pair(child,child.begin()));
+ break;
+ }
+ Node rewrittenChild = rewrite(child);
+
+ if(rewrittenChild.getMetaKind() == kind::metakind::CONSTANT){//c
+ Rational c = rewrittenChild.getConst<Rational>();
+ accumulator = accumulator * c;
+ if(accumulator == 0){
+ return d_constants->d_ZERO_NODE;
+ }
+ }else if(rewrittenChild.getMetaKind() == kind::metakind::VARIABLE){ //v
+ variables.insert(rewrittenChild);
+ }else{ //(+ c p_1 p_2 ... p_N)
+ sums.push_back(rewrittenChild);
+ }
+ }
+ }
+ // accumulator * (\prod var_i) *(\prod sum_j)
+
+ if(sums.size() == 0){ //accumulator * (\prod var_i)
+ if(variables.size() == 0){ //accumulator
+ return mkRationalNode(accumulator);
+ }else if(variables.size() == 1 && accumulator == d_constants->d_ONE){ // var_1
+ Node var = *(variables.begin());
+ return var;
+ }else{
+ //We need to return (+ c p_1 p_2 ... p_N)
+ //To accomplish this:
+ // let pnf = pnf(accumulator * (\prod var_i)) in (+ 0 pnf)
+ Node pnf = toPnf(accumulator, variables);
+ Node normalForm = NodeManager::currentNM()->mkNode(kind::PLUS, d_constants->d_ZERO_NODE, pnf);
+ return normalForm;
+ }
+ }else{
+ vector<Node>::iterator sum_iter = sums.begin();
+ // \sum t
+ // t \in Q \cup A
+ // where A = lfp {\prod s | s \in Q \cup Variables \cup A}
+ Node distributed = *sum_iter;
+ ++sum_iter;
+ while(sum_iter != sums.end()){
+ Node curr = *sum_iter;
+ distributed = distributeSum(curr, distributed);
+ ++sum_iter;
+ }
+ if(variables.size() >= 1){
+ Node pnf = toPnf(accumulator, variables);
+ distributed = distribute(pnf, distributed);
+ }else{
+ Node constant = mkRationalNode(accumulator);
+ distributed = distribute(constant, distributed);
+ }
+
+ Node nf_distributed = rewrite(distributed);
+ return nf_distributed;
+ }
+}
+
+Node ArithRewriter::rewriteTerm(TNode t){
+ if(t.getMetaKind() == kind::metakind::CONSTANT){
+ return coerceToRationalNode(t);
+ }else if(t.getMetaKind() == kind::metakind::VARIABLE){
+ return t;
+ }else if(t.getKind() == kind::MULT){
+ return rewriteMult(t);
+ }else if(t.getKind() == kind::PLUS){
+ return rewritePlus(t);
+ }else{
+ Unreachable();
+ return Node::null();
+ }
+}
+
+
+/**
+ * Given a node in PNF pnf = (* d p_1 p_2 .. p_M) and a rational q != 0
+ * constuct a node equal to q * pnf that is in pnf.
+ *
+ * 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);
+ //TODO Assert(isPNF(pnf) );
+
+ int M = pnf.getNumChildren()-1;
+ Rational d = pnf[0].getConst<Rational>();
+ Rational new_d = d*q;
+
+
+ NodeBuilder<> mult;
+ mult << mkRationalNode(new_d);
+ for(int i=1; i<=M; ++i){
+ mult << pnf[i];
+ }
+
+ Node result = mult;
+ return result;
+}
+
+
+
+Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){
+ using namespace CVC4::kind;
+ NodeManager* currentNM = NodeManager::currentNM();
+ Node negR = currentNM->mkNode(MULT, d_constants->d_NEGATIVE_ONE_NODE, r);
+ Node diff = currentNM->mkNode(PLUS, l, negR);
+
+ return diff;
+}
+
+
+Kind multKind(Kind k, int sgn){
+ using namespace kind;
+
+ if(sgn < 0){
+
+ switch(k){
+ case LT: return GT;
+ case LEQ: return GEQ;
+ case EQUAL: return EQUAL;
+ case GEQ: return LEQ;
+ case GT: return LT;
+ default:
+ Unhandled();
+ }
+ return NULL_EXPR;
+ }else{
+ return k;
+ }
+}
+
+Node ArithRewriter::rewrite(TNode n){
+ using namespace std;
+ cout << "Trace rewrite:" << n << endl;
+
+ if(n.getAttribute(IsNormal())){
+ return n;
+ }
+
+ Node res;
+
+ if(n.isAtomic()){
+ res = rewriteAtom(n);
+ }else{
+ res = rewriteTerm(n);
+ }
+
+ if(n == res){
+ n.setAttribute(NormalForm(), Node::null());
+ }else{
+ n.setAttribute(NormalForm(), res);
+ }
+
+ return res;
+}
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
new file mode 100644
index 000000000..844663ce8
--- /dev/null
+++ b/src/theory/arith/arith_rewriter.h
@@ -0,0 +1,92 @@
+
+#include "expr/node.h"
+#include "util/rational.h"
+#include "theory/arith/arith_constants.h"
+
+#ifndef __CVC4__THEORY__ARITH__REWRITER_H
+#define __CVC4__THEORY__ARITH__REWRITER_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+
+/***********************************************/
+/***************** Normal Form *****************/
+/***********************************************/
+/***********************************************/
+
+/**
+ * Normal form for predicates:
+ * TRUE
+ * FALSE
+ * v |><| b
+ * p |><| b
+ * (+ p_1 .. p_N) |><| b
+ * where
+ * 1) b is of type CONST_RATIONAL
+ * 2) |><| is of kind <, <=, =, >= or >
+ * 3) p, p_i is in PNF,
+ * 4) p.M >= 2
+ * 5) p_i's are in strictly ascending <p,
+ * 6) N >= 2,
+ * 7) the kind of (+ p_1 .. p_N) is an N arity PLUS,
+ * 8) p.d, p_1.d are 1,
+ * 9) v has metakind variable, and
+ *
+ * PNF(t):
+ * (* d v_1 v_2 ... v_M)
+ * where
+ * 1) d is of type CONST_RATIONAL,
+ * 2) d != 0,
+ * 4) M>=1,
+ * 5) v_i are of metakind VARIABLE,
+ * 6) v_i are in increasing (not strict) nodeOrder, and
+ * 7) the kind of t is an M+1 arity MULT.
+ *
+ * <p is defined over PNF as follows (skipping some symmetry):
+ * cmp( (* d v_1 v_2 ... v_M), (* d' v'_1 v'_2 ... v'_M'):
+ * if(M == M'):
+ * then tupleCompare(v_i, v'_i)
+ * else M -M'
+ *
+ * Rewrite Normal Form for Terms:
+ * b
+ * v
+ * (+ c p_1 p_2 ... p_N) | not(N=1 and c=0 and p_1.d=1)
+ * where
+ * 1) b,c is of type CONST_RATIONAL,
+ * 3) p_i is in PNF,
+ * 4) N >= 1
+ * 5) the kind of (+ c p_1 p_2 ... p_N) is an N+1 arity PLUS,
+ * 6) and p_i's are in strictly <p.
+ *
+ */
+
+class ArithRewriter{
+private:
+ ArithConstants* d_constants;
+
+ Node rewriteAtom(TNode atom);
+ Node rewriteTerm(TNode t);
+ Node rewriteMult(TNode t);
+ Node rewritePlus(TNode t);
+ Node makeSubtractionNode(TNode l, TNode r);
+
+
+ Node var2pnf(TNode variable);
+
+public:
+ ArithRewriter(ArithConstants* ac) :
+ d_constants(ac)
+ {}
+ Node rewrite(TNode t);
+
+};
+
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH__REWRITER_H */
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
new file mode 100644
index 000000000..7b578c934
--- /dev/null
+++ b/src/theory/arith/arith_utilities.h
@@ -0,0 +1,128 @@
+
+
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
+#define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
+
+
+#include "util/rational.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+inline Node mkRationalNode(Rational& q){
+ return NodeManager::currentNM()->mkConst<Rational>(q);
+}
+
+inline Node mkBoolNode(bool b){
+ return NodeManager::currentNM()->mkConst<bool>(b);
+}
+
+
+
+inline Rational coerceToRational(TNode constant){
+ switch(constant.getKind()){
+ case kind::CONST_INTEGER:
+ {
+ Rational q(constant.getConst<Integer>());
+ return q;
+ }
+ case kind::CONST_RATIONAL:
+ return constant.getConst<Rational>();
+ default:
+ Unreachable();
+ }
+ Rational unreachable(0,0);
+ return unreachable;
+}
+
+inline Node coerceToRationalNode(TNode constant){
+ switch(constant.getKind()){
+ case kind::CONST_INTEGER:
+ {
+ Rational q(constant.getConst<Integer>());
+ Node n = mkRationalNode(q);
+ return n;
+ }
+ case kind::CONST_RATIONAL:
+ return constant;
+ default:
+ Unreachable();
+ }
+ return Node::null();
+}
+
+
+
+/** is k \in {LT, LEQ, EQ, GEQ, GT} */
+inline bool isRelationOperator(Kind k){
+ using namespace kind;
+
+ switch(k){
+ case LT:
+ case LEQ:
+ case EQUAL:
+ case GEQ:
+ case GT:
+ return true;
+ default:
+ return false;
+ }
+}
+
+inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Rational& right){
+ using namespace kind;
+
+ switch(k){
+ case LT: return left < right;
+ case LEQ: return left <= right;
+ case EQUAL: return left == right;
+ case GEQ: return left >= right;
+ case GT: return left > right;
+ default:
+ Unreachable();
+ return true;
+ }
+}
+
+
+
+inline Node pushInNegation(Node assertion){
+ using namespace CVC4::kind;
+ Assert(assertion.getKind() == NOT);
+
+ Node p = assertion[0];
+
+ Kind k;
+
+ switch(p.getKind()){
+ case EQUAL:
+ return assertion;
+ case GT:
+ k = LT;
+ break;
+ case GEQ:
+ k = LEQ;
+ break;
+ case LEQ:
+ k = GEQ;
+ break;
+ case LT:
+ k = GT;
+ break;
+ default:
+ Unreachable();
+ }
+
+ return NodeManager::currentNM()->mkNode(k, p[0],p[1]);
+}
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_UTILITIES_H */
diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h
new file mode 100644
index 000000000..999b54b70
--- /dev/null
+++ b/src/theory/arith/basic.h
@@ -0,0 +1,33 @@
+
+
+#include "expr/attribute.h"
+
+#ifndef __CVC4__THEORY__ARITH__BASIC_H
+#define __CVC4__THEORY__ARITH__BASIC_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+struct IsBasicAttrID;
+
+typedef expr::Attribute<IsBasicAttrID, bool> IsBasic;
+
+
+inline bool isBasic(TNode x){
+ return x.hasAttribute(IsBasic());
+}
+
+inline void makeBasic(TNode x){
+ return x.setAttribute(IsBasic(), true);
+}
+
+inline void makeNonbasic(TNode x){
+ return x.setAttribute(IsBasic(), false);
+}
+
+}; /* namespace arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH__BASIC_H */
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
new file mode 100644
index 000000000..5fd4d4e07
--- /dev/null
+++ b/src/theory/arith/delta_rational.h
@@ -0,0 +1,82 @@
+#include "cvc4_private.h"
+
+#include "util/integer.h"
+#include "util/rational.h"
+
+
+#ifndef __CVC4__THEORY__ARITH__DELTA_RATIONAL_H
+#define __CVC4__THEORY__ARITH__DELTA_RATIONAL_H
+
+/**
+ * A DeltaRational is a pair of rationals (c,k) that represent the number
+ * c + kd
+ * where d is an implicit system wide symbolic infinitesimal.
+ */
+class DeltaRational {
+private:
+ CVC4::Rational c;
+ CVC4::Rational k;
+
+public:
+ DeltaRational() : c(0), k(0) {}
+ DeltaRational(const CVC4::Rational& base) : c(base), k(0) {}
+ DeltaRational(const CVC4::Rational& base, const CVC4::Rational& coeff) :
+ c(base), k(coeff) {}
+
+ DeltaRational operator+(const DeltaRational& other) const{
+ CVC4::Rational tmpC = c+other.c;
+ CVC4::Rational tmpK = k+other.k;
+ return DeltaRational(tmpC, tmpK);
+ }
+
+ DeltaRational operator*(CVC4::Rational& a) const{
+ CVC4::Rational tmpC = a*c;
+ CVC4::Rational tmpK = a*k;
+ return DeltaRational(tmpC, tmpK);
+ }
+
+ DeltaRational operator-(const DeltaRational& a) const{
+ CVC4::Rational negOne(CVC4::Integer(-1));
+ return *(this) + (a * negOne);
+ }
+
+ bool operator==(DeltaRational& other){
+ return (k == other.k) && (c == other.c);
+ }
+
+ bool operator<=(DeltaRational& other){
+ int cmp = c.cmp(other.c);
+ return (cmp < 0) || ((cmp==0)&&(k <= other.k));
+ }
+ bool operator<(DeltaRational& other){
+ return (other > *this);
+ }
+ bool operator>=(DeltaRational& other){
+ return (other <= *this);
+ }
+ bool operator>(DeltaRational& other){
+ return !(*this <= other);
+ }
+
+ DeltaRational& operator=(DeltaRational& other){
+ c = other.c;
+ k = other.k;
+ return *(this);
+ }
+
+ DeltaRational& operator*=(CVC4::Rational& a){
+ c = c * a;
+ k = k * a;
+
+ return *(this);
+ }
+
+ DeltaRational& operator+=(DeltaRational& other){
+ c =c + other.c;
+ k =k + other.k;
+
+ return *(this);
+ }
+};
+
+#endif /* __CVC4__THEORY__ARITH__DELTA_RATIONAL_H */
diff --git a/src/theory/arith/normal.h b/src/theory/arith/normal.h
new file mode 100644
index 000000000..7f8192a7d
--- /dev/null
+++ b/src/theory/arith/normal.h
@@ -0,0 +1,29 @@
+
+#ifndef __CVC4__THEORY__ARITH__NORMAL_H
+#define __CVC4__THEORY__ARITH__NORMAL_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+struct IsNormalAttrID;
+
+typedef expr::Attribute<IsNormalAttrID, bool> IsNormal;
+
+
+inline bool isNormalized(TNode x){
+ return x.hasAttribute(IsNormal());
+}
+
+struct NormalFormAttrID;
+
+typedef expr::Attribute<IsNormalAttrID, Node> NormalForm;
+
+
+
+}; /* namespace arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+
+#endif /* __CVC4__THEORY__ARITH__NORMAL_H */
diff --git a/src/theory/arith/normal_form_notes.txt b/src/theory/arith/normal_form_notes.txt
new file mode 100644
index 000000000..30786e980
--- /dev/null
+++ b/src/theory/arith/normal_form_notes.txt
@@ -0,0 +1,455 @@
+
+/** DRAFT 1
+ * Normal form for predicates:
+ * TRUE
+ * FALSE
+ * var_i |><| b
+ * \sum_i product_i |><| b
+ * where
+ * 1) b is of type CONST_RATIONAL
+ * 2) |><| is of type <=, >, =, < or >=
+ * 3) product_i is in product normal form,
+ * 4) product_i is not 0,
+ * 5) product_i's are in strictly ascending productOrder,
+ * 6) product_i has at least 2 members,
+ * 7) product_1 has a positive coefficient, and
+ * 8) var_i has metakind variable.
+ *
+ * Normal form for terms:
+ * c
+ * c + \sum_i product_i
+ * where
+ * 1) c is of type CONST_RATIONAL,
+ * 2) product_i is in product normal form,
+ * 3) product_i is not a constant,
+ * 4) and product_i's are in strictly ascending productOrder.
+ *
+ * Normal form for products:
+ * d
+ * var_i
+ * e * \prod var_i
+ * where
+ * 1) d,e is of type CONST_RATIONAL,
+ * 2) e != 0,
+ * 3) e != 1 or there are at least 2 variables,
+ * 2) var_i is of metakind VARIABLE,
+ * 3) and var_i are in increasing (not strict) nodeOrder.
+ *
+ * productOrder is well defined over normal form products as follows:
+ * cmp(d,d') = rational order.
+ * cmp(d,var_i)= -1
+ * cmp(var_i,var_j) is the node order
+ * cmp(var_i,d * \prod var_i) = -1
+ * cmp(p = d * \prod var_i, p' = d' * \prod var_i')=
+ * if(len(p) == len(p'))
+ * then tupleCompare(var_i, var_i')
+ * else len(p) - len(p')
+ */
+
+
+
+/** DRAFT 2
+ * Normal form for predicates:
+ * TRUE
+ * FALSE
+ * var |><| b
+ * (\sum_{i=1 to N} p_i) |><| b
+ * where
+ * 1) b is of type CONST_RATIONAL
+ * 2) |><| is of kind <, <=, =, >= or >
+ * 3) p_i is in PNF,
+ * 5) p_i's are in strictly ascending <p,
+ * 6) N >= 2,
+ * 7) the kind of (\sum_{i=1 to N} p_i) is an N arity PLUS,
+ * 8) p_1 has coefficient 1, and
+ * 9) var has metakind variable.
+ *
+ * PNF:
+ * v
+ * d * v
+ * (\prod_{i=1 to M} v_i)
+ * d * (\prod_{i=1 to M} v_i)
+ * where
+ * 1) d is of type CONST_RATIONAL,
+ * 2) d != 0,
+ * 3) d != 1,
+ * 4) M>=2,
+ * 5) v, v_i are of metakind VARIABLE,
+ * 6) v_i are in increasing (not strict) nodeOrder, and
+ * 7) the kind of (\prod_{i=1 to M} v_i) is an M arity MULT.
+ *
+ * <p is defined over PNF as follows (skipping some symmetry):
+ * cmp( v, v') is the node order over v and v'
+ * cmp( v,d'*v') is the node order over v and v'
+ * cmp(d*v,d'*v') is the node order over v and v'
+ * cmp( v, (\prod v'_i)) = -1
+ * cmp(d*v, (\prod v_i)) = -1
+ * cmp( v, d*(\prod v'_i)) = -1
+ * cmp(d*v, d*(\prod v_i)) = -1
+ * cmp((\prod_{i=1 to M} v_i),(\prod_{i=1 to M'} v'_i))=
+ * if(M == M')
+ * then tupleCompare(v_i, v'_i)
+ * else M - M'
+ * cmp((\prod_{i=1 to M} v_i), d*(\prod_{i=1 to M'} v'_i))=
+ * if(M == M')
+ * then tupleCompare(v_i, v'_i)
+ * else M - M'
+ * cmp(d * (\prod_{i=1 to M} v_i), d' * (\prod_{i=1 to M'} v'_i))=
+ * if(M == M')
+ * then tupleCompare(v_i, v'_i)
+ * else M - M'
+ *
+ * Rewrite Normal Form for Terms:
+ * b
+ * p
+ * c + p
+ * (\sum_{i=1 to N} p_i)
+ * c + (\sum_{i=1 to N} p_i)
+ * where
+ * 1) b,c is of type CONST_RATIONAL,
+ * 2) c != 0,
+ * 3) p, p_i is in PNF,
+ * 4) N >= 2
+ * 5) the kind of (\sum_{i=1 to N} p_i) is an N arity PLUS,
+ * 6) and p_i's are in strictly <p.
+ *
+ */
+
+
+bool isVarMultList(TNode v){
+ for(v = 1 to l.getLength()){
+ if(!isVar(v[i])){
+ return false;
+ }
+ }
+
+ for(v = 2 to l.getLength()){
+ if(!(v[i-1] <= v[i])){
+ return false;
+ }
+ }
+ return true;
+}
+
+bool isPNF(TNode p){
+ if(p.getKind() == MULT){
+ if(p[0].getKind() == CONST_RATIONAL){
+ if(p[0].getConst<CONST_RATIONAL>() != 0 &&
+ p[0].getConst<CONST_RATIONAL> != 1){
+ if(p[1].getKind() != MULT){
+ if(p[1].getMetaKind() == VARIABLE){
+ return true; // d * v
+ }else{
+ return false;
+ }
+ }else{
+ if(isVarMultList(p[1])){
+ return true; // d * (\prod_{i=1 to M} v_i)
+ }else{
+ return false;
+ }
+ }
+ }else{
+ return false;
+ }
+ }else{
+ if(isVarMultList(p)){
+ return true; //(\prod_{i=1 to M} v_i)
+ }else{
+ return false;
+ }
+ }
+ }else{
+ if(p.getMetaKind() == VARIABLE){
+ return true; // v
+ }else{
+ return false;
+ }
+ }
+}
+
+
+bool <p(TNode p0, TNode p1){
+ PNFType t0 = same as the comments in isPNF(p0);
+ PNFType t1 = same as the comments in isPNF(p1);
+
+ bool t0IsVar = (t0 == "v") ||(t0 == "d*v");
+ bool t1IsVar = (t1 == "v") ||(t1 == "d*v");
+
+ if(t0IsVar && t1IsVar){
+ TNode v0 = (t0 == "d*v") ? p0[1] : p0;
+ TNode v1 = (t1 == "d*v") ? p1[1] : p1;
+ return v0 < v1;
+ }else if(!t0IsVar && t1IsVar){
+ return false;
+ }else if(t0IsVar && !t1IsVar){
+ return true;
+ }else{
+ TNode prod0 = (t0 == "d * (\prod_{i=1 to M} v_i)") ? p0[1] : p0;
+ TNode prod1 = (t1 == "d * (\prod_{i=1 to M} v_i)") ? p1[1] : p1;
+
+ int M0 = prod0.getNumChildren();
+ int M1 = prod1.getNumChildren();
+
+ if(M0 == M1){
+ for(i in 1 to M0){
+ if(prod0[i] < prod[i]){
+ return true;
+ }
+ }
+ return false;
+ }else{
+ return M0 < M1;
+ }
+ }
+}
+
+bool isPNFSum(TNode p){
+
+ for(i = 1 to p.getNumChildren()){
+ if(!isPNF(p[i])){
+ return false;
+ }
+ }
+ for(i = 2 to p.getNumChildren()){
+ if(!(p[i-1] <p p[i])){
+ return false;
+ }
+ }
+ return true;
+}
+
+string isNormalFormTerm(TNode t){
+ Kind k = t.getKind();
+ if(k != PLUS){
+ if(k == CONST_RATIONAL){
+ return true; // b
+ }else if(isPNF(p)){
+ return true; // p
+ }else{
+ return false;
+ }
+ }else{
+ if(t[0].getKind() == CONST_RATIONAL){
+ if(t[0].getConst<CONST_RATIONAL>() != 0){
+ if(t[1].getKind() == PLUS){
+ if(isPNFSum(t[1])){
+ return true; // c + (\sum_{i=1 to N} p_i)
+ }else{
+ return false;
+ }
+ }else{
+ if(isPNF(t[1])){
+ return true; // c + p
+ }else{
+ return false;
+ }
+ }
+ }else{
+ return false;
+ }
+ }else{
+ if(isPNFSum(t)){
+ return true; // (\sum_{i=1 to N} p_i)
+ }else{
+ return false;
+ }
+ }
+ }
+}
+
+/***********************************************/
+/***********************************************/
+/******************* DRAFT 3 *******************/
+/***********************************************/
+/***********************************************/
+
+/** DRAFT 3
+ * Normal form for predicates:
+ * TRUE
+ * FALSE
+ * v |><| b
+ * p |><| b
+ * (+ p_1 .. p_N) |><| b
+ * where
+ * 1) b is of type CONST_RATIONAL
+ * 2) |><| is of kind <, <=, =, >= or >
+ * 3) p, p_i is in PNF,
+ * 5) p_i's are in strictly ascending <p,
+ * 6) N >= 2,
+ * 7) the kind of (+ p_1 .. p_N) is an N arity PLUS,
+ * 8) p.d, p_1.d are 1, and
+ * 9) v has metakind variable.
+ *
+ * PNF(t):
+ * (* d v_1 v_2 ... v_M)
+ * where
+ * 1) d is of type CONST_RATIONAL,
+ * 2) d != 0,
+ * 4) M>=1,
+ * 5) v_i are of metakind VARIABLE,
+ * 6) v_i are in increasing (not strict) nodeOrder, and
+ * 7) the kind of t is an M+1 arity MULT.
+ *
+ * <p is defined over PNF as follows (skipping some symmetry):
+ * cmp( (* d v_1 v_2 ... v_M), (* d' v'_1 v'_2 ... v'_M'):
+ * if(M == M'):
+ * then tupleCompare(v_i, v'_i)
+ * else M -M'
+ *
+ * Rewrite Normal Form for Terms:
+ * b
+ * v
+ * (+ c p_1 p_2 ... p_N) | not(N=1 and c=0 and p_1.d=1)
+ * where
+ * 1) b,c is of type CONST_RATIONAL,
+ * 2) c != 0,
+ * 3) p_i is in PNF,
+ * 4) N >= 1
+ * 5) the kind of (+ c p_1 p_2 ... p_N) is an N+1 arity PLUS,
+ * 6) and p_i's are in strictly <p.
+ *
+ */
+
+
+/* Assuming that the terms have been normalized, how much work is the case splitting.
+ * The following should provide a good insight into how difficult it is to use
+ * these normal forms when writing code.
+ */
+
+enum PredicateNFKind{TRUE, FALSE, v |><| b, p |><| b, (+ p_1 .. p_N) |><| b};
+
+PredicateNFKind kindOfNormalFormPredicate(TNode n){
+ if(n.getKind() == CONST_BOOLEAN){
+ if(n.getConst<bool>()){
+ return TRUE;
+ }else{
+ return FALSE;
+ }
+ }else{
+ TNode left = n[0];
+ if(left.getMetaKind() == metakind::VARIABLE){
+ return v |><| b;
+ }else if(left.getKind() == MULT){
+ return p |><| b;
+ }else{
+ return (+ p_1 .. p_N) |><| b;
+ }
+ }
+}
+
+enum TermNFKind{c, v, (+ c p_1 p_2 ... p_N)};
+
+TermNFKind kindOfTermNFKind(TNode n){
+ if(n.getMetaKind() == metakind::CONSTANT){
+ return c;
+ }else if(n.getMetaKind() == metakind::VARIABLE){
+ return v;
+ }else{
+ return (+ c p_1 p_2 ... p_N)
+ }
+}
+
+
+/* Verify that the term meets all of the criteria for a normal form.
+ * This should provide good insight into how difficult it is to write/debug
+ * the rewriters themselves, and other parts of the code that are
+ * "highly knowledgable" about the normal form (such as helper functions).
+ */
+
+
+bool rangeIsSorted(bool strict, TNode::iterator start, TNode::iterator stop, NodeComparitor cmp){
+ if(start == stop) return true;
+ TNode prev = *start;
+ ++start;
+ while(start != stop){
+ TNode curr = *start;
+ int tmp = cmp(prev, curr);
+ if(strict && tmp >= 0
+ !strict && tmp > 0
+ ){
+ return false;
+ }
+ prev = curr;
+ ++start;
+ }
+ return true;
+}
+
+bool rangeAll(TNode::iterator start, TNode::iterator stop, NodePredicate rho){
+ for(;start != stop; ++start){
+ if(! rho(*start)) return false;
+ }
+ return true;
+}
+bool isPNF(TNode p){
+ return
+ p.getKind() == MULT &&
+ p[0].getKind() == CONST_RATIONAL&&
+ p[0].getConst<CONST_RATIONAL>() != 0 &&
+ rangeIsSorted(false, p.begin()+1, p.end(), nodeOrder) &&
+ rangeAll(p.begin()+1, p.end(), \t -> t.getMetaKind() == metakind::VARIABLE);
+}
+
+
+bool cmpPNF(TNode p0, TNode p1){
+ int M0 = p0.getNumChildren();
+ int M1 = p1.getNumChildren();
+
+ if(M0 == M1){
+ for(int i=1; i< M0; ++i){
+ int cmp = nodeOrder(p0[i],p1[i]);
+ if(cmp != 0){
+ return cmp;
+ }
+ }
+ return 0;
+ }else{
+ return M0 - M1;
+ }
+}
+
+bool isNormalFormTerm(TNode t){
+ if(t.getKind() == CONST_RATIONAL){
+ return true;
+ }else if(t.getMetaKind() == VARIABLE){
+ return true;
+ }else if(t.getKind() == PLUS){ //may be (+ c p_1 p_2 ... p_N)
+ int N = t.getNumChildren()-1;
+ TNode c = t[0];
+ return c.getKind() == CONST_RATIONAL &&
+ c.getConst<Rational>() !- 0 &&
+ N >= 1 && //This check is redundent because of an invariant in NodeBuilder<>
+ rangeAll(p.begin()+1, p.end(), isPNF) &&
+ rangeIsSorted(true, p.begin()+1, p.end(), cmpPNF);
+ }else{
+ return false;
+ }
+}
+
+bool isNormalFormAtom(TNode n){
+ if(n.getKind() == CONST_BOOLEAN){
+ return true;
+ }else if(n.getKind() \in {<, <=, ==, >=, >}){
+ TNode left = n[0];
+ TNode right = n[1];
+ if(right.getKind() == CONST_RATIONAL){
+ if(left.getMetaKind() == VARIABLE){
+ return true;
+ }else if(left.getKind() == MULT){
+ return isPNF(left) && left[0] == 1;
+ }else if(left.getKind() == PLUS){
+ return left.getNumChildren() >= 2 &&
+ rangeAll(left.begin(), left.end(), isPNF) &&
+ left[0][0] == 1 &&
+ rangeIsSorted(true, left.begin(), left.end(), cmpPNF);
+ }else{
+ return false;
+ }
+ }else{
+ return false;
+ }
+ }else{
+ return false;
+ }
+}
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
new file mode 100644
index 000000000..a0f35f9db
--- /dev/null
+++ b/src/theory/arith/partial_model.h
@@ -0,0 +1,342 @@
+
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "theory/arith/delta_rational.h"
+#include "expr/node.h"
+
+
+#ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
+#define __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+typedef CVC4::context::CDList<TNode> BoundsList;
+
+namespace partial_model {
+struct DeltaRationalCleanupStrategy{
+ static void cleanup(DeltaRational* dq){
+ Debug("arithgc") << "cleaning up " << dq << "\n";
+ delete dq;
+ }
+};
+
+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;
+
+/**
+ * BoundsListAttr is the attribute that maps a node to atoms .
+ */
+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.
+ */
+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;
+ }
+}
+
+
+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;
+ }
+}
+
+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);
+ }
+}
+
+/** 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;
+}
+
+
+DeltaRational getLowerBound(TNode x){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ DeltaRational* assign;
+ AlwaysAssert(x.getAttribute(partial_model::LowerBound(),assign));
+ return *assign;
+}
+
+DeltaRational getAssignment(TNode x){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ DeltaRational* assign;
+ AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+ return *assign;
+}
+
+void setLowerConstraint(TNode constraint){
+ TNode x = constraint[0];
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ x.setAttribute(partial_model::LowerConstraint(),constraint);
+}
+
+void setUpperConstraint(TNode constraint){
+ TNode x = constraint[0];
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ x.setAttribute(partial_model::UpperConstraint(),constraint);
+}
+TNode getLowerConstraint(TNode x){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ TNode ret;
+ AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
+ return ret;
+}
+
+TNode getUpperConstraint(TNode x){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ TNode ret;
+ AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
+ return ret;
+}
+
+/**
+ * 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;
+ }
+}
+
+/**
+ * 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;
+ }
+
+ if(strict){
+ return c > *u;
+ }else{
+ return c >= *u;
+ }
+}
+
+bool strictlyBelowUpperBound(TNode x){
+ DeltaRational* assign;
+ AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+
+ DeltaRational* u;
+ if(!x.getAttribute(partial_model::UpperBound(), u)){ // u = \infty
+ return true;
+ }
+ return *assign < *u;
+}
+
+bool strictlyAboveLowerBound(TNode x){
+ DeltaRational* assign;
+ AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+
+ 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 */
+}; /* namespace CVC4 */
+
+
+
+#endif /* __CVC4__THEORY__ARITH__PARTIAL_MODEL_H */
diff --git a/src/theory/arith/slack.h b/src/theory/arith/slack.h
new file mode 100644
index 000000000..37595fda5
--- /dev/null
+++ b/src/theory/arith/slack.h
@@ -0,0 +1,14 @@
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+struct SlackAttrID;
+
+typedef expr::Attribute<SlackAttrID, Node> Slack;
+
+
+}; /* namespace arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
new file mode 100644
index 000000000..10daa0c13
--- /dev/null
+++ b/src/theory/arith/tableau.h
@@ -0,0 +1,243 @@
+
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+#include "theory/arith/basic.h"
+
+#include <ext/hash_map>
+#include <set>
+
+#ifndef __CVC4__THEORY__ARITH__TABLEAU_H
+#define __CVC4__THEORY__ARITH__TABLEAU_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+
+class Row {
+ TNode d_x_i;
+
+ typedef __gnu_cxx::hash_map<TNode, Rational, NodeHashFunction> CoefficientTable;
+
+ std::set<TNode> d_nonbasic;
+ CoefficientTable d_coeffs;
+
+public:
+
+ /**
+ * Construct a row equal to:
+ * basic = \sum_{x_i} c_i * x_i
+ */
+ Row(TNode basic, TNode sum): d_x_i(basic),d_nonbasic(), d_coeffs(){
+ using namespace CVC4::kind;
+
+ Assert(d_x_i.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ //TODO Assert(d_x_i.getType() == REAL);
+ Assert(sum.getKind() == PLUS);
+
+ for(TNode::iterator iter=sum.begin(); iter != sum.end(); ++iter){
+ TNode pair = *iter;
+ Assert(pair.getKind() == MULT);
+ Assert(pair.getNumChildren() == 2);
+ TNode coeff = pair[0];
+ TNode var_i = pair[1];
+ Assert(coeff.getKind() == CONST_RATIONAL);
+ Assert(var_i.getKind() == VARIABLE);
+ //TODO Assert(var_i.getKind() == REAL);
+ Assert(!has(var_i));
+ d_nonbasic.insert(var_i);
+ d_coeffs[var_i] = coeff.getConst<Rational>();
+ }
+ }
+
+ std::set<TNode>::iterator begin(){
+ return d_nonbasic.begin();
+ }
+
+ std::set<TNode>::iterator end(){
+ return d_nonbasic.end();
+ }
+
+ TNode basicVar(){
+ return d_x_i;
+ }
+
+ bool has(TNode x_j){
+ CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
+
+ return x_jPos != d_coeffs.end();
+ }
+
+ Rational& lookup(TNode x_j){
+ return d_coeffs[x_j];
+ }
+
+ void pivot(TNode x_j){
+ Rational negInverseA_rs = -(lookup(x_j).inverse());
+ d_coeffs[d_x_i] = Rational(Integer(-1));
+ d_coeffs.erase(x_j);
+
+ d_nonbasic.erase(x_j);
+ d_nonbasic.insert(d_x_i);
+ d_x_i = x_j;
+
+ for(std::set<TNode>::iterator nonbasicIter = d_nonbasic.begin();
+ nonbasicIter != d_nonbasic.end();
+ ++nonbasicIter){
+ TNode nb = *nonbasicIter;
+ d_coeffs[nb] = d_coeffs[nb] * negInverseA_rs;
+ }
+ }
+
+ void subsitute(Row& row_s){
+ TNode x_s = row_s.basicVar();
+
+ Assert(!has(x_s));
+ Assert(x_s != d_x_i);
+
+
+ Rational a_rs = lookup(x_s);
+ d_coeffs.erase(x_s);
+
+ for(std::set<TNode>::iterator iter = row_s.d_nonbasic.begin();
+ iter != row_s.d_nonbasic.end();
+ ++iter){
+ TNode x_j = *iter;
+ Rational a_sj = a_rs * row_s.lookup(x_j);
+ if(has(x_j)){
+ d_coeffs[x_j] = d_coeffs[x_j] + a_sj;
+ }else{
+ d_nonbasic.insert(x_j);
+ d_coeffs[x_j] = a_sj;
+ }
+ }
+ }
+};
+
+class Tableau {
+public:
+ typedef std::set<TNode> VarSet;
+
+private:
+ typedef __gnu_cxx::hash_map<TNode, Row*, NodeHashFunction> RowsTable;
+
+ VarSet d_basicVars;
+ RowsTable d_rows;
+
+ inline bool contains(TNode var){
+ return d_basicVars.find(var) != d_basicVars.end();
+ }
+
+public:
+ /**
+ * Constructs an empty tableau.
+ */
+ Tableau() : d_basicVars(), d_rows() {}
+
+ VarSet::iterator begin(){
+ return d_basicVars.begin();
+ }
+
+ VarSet::iterator end(){
+ return d_basicVars.end();
+ }
+
+ Row* lookup(TNode var){
+ Assert(contains(var));
+ return d_rows[var];
+ }
+
+ /**
+ * Iterator for the tableau. Iterates over rows.
+ */
+ /* TODO add back in =(
+ class iterator {
+ private:
+ const Tableau* table_ref;
+ VarSet::iterator variableIter;
+
+ iterator(const Tableau* tr, VarSet::iterator& i) :
+ table_ref(tr), variableIter(i){}
+
+ public:
+ void operator++(){
+ ++variableIter;
+ }
+
+ bool operator==(iterator& other){
+ return variableIter == other.variableIter;
+ }
+ bool operator!=(iterator& other){
+ return variableIter != other.variableIter;
+ }
+
+ Row& operator*() const{
+ TNode var = *variableIter;
+ RowsTable::iterator iter = table_ref->d_rows.find(var);
+ return *iter;
+ }
+ };
+ iterator begin(){
+ return iterator(this, d_basicVars.begin());
+ }
+ iterator end(){
+ return iterator(this, d_basicVars.end());
+ }*/
+
+ void addRow(TNode eq){
+ Assert(eq.getKind() == kind::EQUAL);
+ Assert(eq.getNumChildren() == 2);
+
+ TNode var = eq[0];
+ TNode sum = eq[1];
+
+ //Assert(isAdmissableVariable(var));
+ Assert(var.getAttribute(IsBasic()));
+
+ Assert(d_basicVars.find(var) != d_basicVars.end());
+ d_basicVars.insert(var);
+ d_rows[var] = new Row(var,sum);
+ }
+
+ /**
+ * preconditions:
+ * x_r is basic,
+ * x_s is non-basic, and
+ * a_rs != 0.
+ */
+ void pivot(TNode x_r, TNode x_s){
+ RowsTable::iterator ptrRow_r = d_rows.find(x_r);
+ Assert(ptrRow_r != d_rows.end());
+
+ Row* row_s = (*ptrRow_r).second;
+
+ Assert(row_s->has(x_s));
+ row_s->pivot(x_s);
+
+ d_rows.erase(ptrRow_r);
+ d_basicVars.erase(x_r);
+ makeNonbasic(x_r);
+
+ d_rows.insert(std::make_pair(x_s,row_s));
+ d_basicVars.insert(x_s);
+ makeBasic(x_s);
+
+ for(VarSet::iterator basicIter = begin(); basicIter != end(); ++basicIter){
+ TNode basic = *basicIter;
+ Row* row_k = lookup(basic);
+ if(row_k->basicVar() != x_s){
+ if(row_k->has(x_s)){
+ row_k->subsitute(*row_s);
+ }
+ }
+ }
+ }
+};
+
+}; /* namespace arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH__TABLEAU_H */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
new file mode 100644
index 000000000..50d4fb633
--- /dev/null
+++ b/src/theory/arith/theory_arith.cpp
@@ -0,0 +1,384 @@
+#include "expr/node.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+
+#include "util/rational.h"
+#include "util/integer.h"
+
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/arith/delta_rational.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/tableau.h"
+#include "theory/arith/normal.h"
+#include "theory/arith/slack.h"
+
+#include "theory/arith/arith_rewriter.h"
+
+#include "theory/arith/theory_arith.h"
+#include <map>
+
+using namespace std;
+
+using namespace CVC4;
+using namespace CVC4::kind;
+
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+
+bool isBasicSum(TNode n){
+ Unimplemented();
+ return false;
+}
+
+Kind multKind(Kind k){
+ switch(k){
+ case LT: return GT;
+ case LEQ: return GEQ;
+ case EQUAL: return EQUAL;
+ case GEQ: return LEQ;
+ case GT: return LT;
+ default:
+ Unhandled();
+ }
+ return NULL_EXPR;
+}
+
+
+void registerAtom(TNode rel){
+ addBound(rel);
+ //Anything else?
+}
+
+Node TheoryArith::rewrite(TNode n){
+ return d_rewriter.rewrite(n);
+}
+
+void TheoryArith::registerTerm(TNode tn){
+ if(tn.isAtomic()){
+ Node normalForm = (isNormalized(tn)) ? Node(tn) : rewrite(tn);
+ Kind k = normalForm.getKind();
+
+ if(k != kind::CONST_BOOLEAN){
+ Assert(isRelationOperator(k));
+ TNode left = normalForm[0];
+ TNode right = normalForm[1];
+ if(left.getKind() == PLUS){
+ //We may need to introduce a slack variable.
+ Assert(left.getNumChildren() >= 2);
+ Assert(isBasicSum(left));
+ Node slack;
+ if(!left.getAttribute(Slack(), slack)){
+ //TODO
+ //slack = NodeManager::currentNM()->mkVar(RealType());
+ left.setAttribute(Slack(), slack);
+ makeBasic(slack);
+
+ Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left);
+ slackEqLeft.setAttribute(TheoryArithPropagated(), true);
+ //TODO this has to be wrong no?
+ d_out->lemma(slackEqLeft);
+
+ d_tableau.addRow(slackEqLeft);
+ }
+
+ Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
+ registerAtom(rewritten);
+ }else{
+ Assert(left.getMetaKind() == metakind::VARIABLE);
+ Assert(right.getKind() == CONST_RATIONAL);
+ registerAtom(normalForm);
+ }
+ }
+ }
+}
+
+/* procedure AssertUpper( x_i <= c_i) */
+void TheoryArith::AssertUpper(TNode n){
+ 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) ){
+ return; //sat
+ }
+ if(belowLowerBound(x_i, c_i, true)){
+ d_out->conflict(n);
+ return;
+ }
+
+ setUpperConstraint(n);
+ setUpperBound(x_i, c_i);
+
+ if(!isBasic(x_i)){
+ if(getAssignment(x_i) > c_i){
+ update(x_i, c_i);
+ }
+ }
+}
+
+/* procedure AssertLower( x_i >= c_i ) */
+void TheoryArith::AssertLower(TNode n){
+ 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)){
+ return; //sat
+ }
+ if(aboveUpperBound(x_i, c_i, true)){
+ d_out->conflict(n);
+ return;
+ }
+
+ setLowerConstraint(n);
+ setLowerBound(x_i, c_i);
+
+ if(!isBasic(x_i)){
+ if(getAssignment(x_i) > c_i){
+ update(x_i, c_i);
+ }
+ }
+}
+
+void TheoryArith::update(TNode x_i, DeltaRational& v){
+
+ DeltaRational assignment_x_i = getAssignment(x_i);
+ DeltaRational diff = v - assignment_x_i;
+
+ for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+ basicIter != d_tableau.end();
+ ++basicIter){
+ TNode x_j = *basicIter;
+ Row* row_j = d_tableau.lookup(x_j);
+
+ Rational& a_ji = row_j->lookup(x_i);
+
+ DeltaRational assignment = getAssignment(x_j);
+ DeltaRational nAssignment = assignment+(diff * a_ji);
+ setAssignment(x_j, nAssignment);
+ }
+
+ 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);
+
+
+ DeltaRational betaX_i = getAssignment(x_i);
+
+ Rational inv_aij = a_ij.inverse();
+ DeltaRational theta = (v - betaX_i)*inv_aij;
+
+ setAssignment(x_i, v);
+
+
+ DeltaRational tmp = getAssignment(x_j) + theta;
+ setAssignment(x_j, tmp);
+
+ for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+ basicIter != d_tableau.end();
+ ++basicIter){
+ TNode x_k = *basicIter;
+ Row* row_k = d_tableau.lookup(x_k);
+
+ if(x_k != x_i){
+ DeltaRational a_kj = row_k->lookup(x_j);
+ DeltaRational nextAssignment = getAssignment(x_k) + theta;
+ setAssignment(x_k, nextAssignment);
+ }
+ }
+
+ d_tableau.pivot(x_i, x_j);
+}
+
+TNode TheoryArith::selectSmallestInconsistentVar(){
+
+ for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+ basicIter != d_tableau.end();
+ ++basicIter){
+
+ TNode basic = *basicIter;
+ if(!assignmentIsConsistent(basic)){
+ return basic;
+ }
+ }
+
+ return TNode::null();
+}
+
+TNode TheoryArith::selectSlackBelow(TNode x_i){ //beta(x_i) < l_i
+ Row* row_i = d_tableau.lookup(x_i);
+
+ typedef std::set<TNode>::iterator NonBasicIter;
+
+ for(NonBasicIter nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
+ TNode nonbasic = *nbi;
+
+ Rational a_ij = row_i->lookup(nonbasic);
+ if(a_ij > d_constants.d_ZERO && strictlyBelowUpperBound(nonbasic)){
+ return nonbasic;
+ }else if(a_ij < d_constants.d_ZERO && strictlyAboveLowerBound(nonbasic)){
+ return nonbasic;
+ }else{
+ Unreachable();
+ }
+ }
+ return TNode::null();
+}
+
+TNode TheoryArith::selectSlackAbove(TNode x_i){ // beta(x_i) > u_i
+ Row* row_i = d_tableau.lookup(x_i);
+
+ typedef std::set<TNode>::iterator NonBasicIter;
+
+ for(NonBasicIter nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
+ TNode nonbasic = *nbi;
+
+ Rational a_ij = row_i->lookup(nonbasic);
+ if(a_ij < d_constants.d_ZERO && strictlyBelowUpperBound(nonbasic)){
+ return nonbasic;
+ }else if(a_ij > d_constants.d_ZERO && strictlyAboveLowerBound(nonbasic)){
+ return nonbasic;
+ }else{
+ Unreachable();
+ }
+ }
+ return TNode::null();
+}
+
+
+TNode TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
+
+ while(true){
+ TNode x_i = selectSmallestInconsistentVar();
+ if(x_i == Node::null()){
+ 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)){
+ TNode x_j = selectSlackBelow(x_i);
+ if(x_j == TNode::null() ){
+ return generateConflictBelow(x_i); //unsat
+ }
+ pivotAndUpdate(x_i, x_j, l_i);
+ }else if(aboveUpperBound(x_i, beta_i, true)){
+ TNode x_j = selectSlackAbove(x_i);
+ if(x_j == TNode::null() ){
+ return generateConflictAbove(x_j); //unsat
+ }
+ pivotAndUpdate(x_i, x_j, u_i);
+ }
+ }
+}
+
+Node TheoryArith::generateConflictAbove(TNode conflictVar){
+ Row* row_i = d_tableau.lookup(conflictVar);
+
+ NodeBuilder<> nb(kind::AND);
+ nb << getUpperConstraint(conflictVar);
+
+ typedef std::set<TNode>::iterator NonBasicIter;
+
+ for(NonBasicIter nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
+ TNode nonbasic = *nbi;
+ Rational& a_ij = row_i->lookup(nonbasic);
+
+ Assert(a_ij != d_constants.d_ZERO);
+
+ if(a_ij < d_constants.d_ZERO){
+ nb << getUpperConstraint(nonbasic);
+ }else{
+ nb << getLowerConstraint(nonbasic);
+ }
+ }
+ Node conflict = nb;
+ return conflict;
+}
+Node TheoryArith::generateConflictBelow(TNode conflictVar){
+ Row* row_i = d_tableau.lookup(conflictVar);
+
+ NodeBuilder<> nb(kind::AND);
+ nb << getLowerConstraint(conflictVar);
+
+ typedef std::set<TNode>::iterator NonBasicIter;
+
+ for(NonBasicIter nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
+ TNode nonbasic = *nbi;
+ Rational& a_ij = row_i->lookup(nonbasic);
+
+ Assert(a_ij != d_constants.d_ZERO);
+
+ if(a_ij < d_constants.d_ZERO){
+ nb << getLowerConstraint(nonbasic);
+ }else{
+ nb << getUpperConstraint(nonbasic);
+ }
+ }
+ Node conflict = nb;
+ return conflict;
+}
+
+void TheoryArith::check(Effort level){
+ while(!done()){
+ Node assertion = get();
+
+ if(assertion.getKind() == NOT){
+ assertion = pushInNegation(assertion);
+ }
+
+ switch(assertion.getKind()){
+ case LT:
+ case LEQ:
+ AssertUpper(assertion);
+ break;
+ case GEQ:
+ case GT:
+ AssertLower(assertion);
+ break;
+ case EQUAL:
+ AssertUpper(assertion);
+ AssertLower(assertion);
+ break;
+ case NOT:
+ Assert(assertion[0].getKind() == EQUAL);
+ d_diseq.push_back(assertion);
+ break;
+ default:
+ Unhandled();
+ }
+ }
+
+ if(fullEffort(level)){
+ Node possibleConflict = updateInconsistentVars();
+ if(possibleConflict != Node::null()){
+ d_out->conflict(possibleConflict);
+ }
+ }
+
+ if(fullEffort(level)){
+ NodeBuilder<> lemmas(AND);
+ typedef context::CDList<Node>::const_iterator diseq_iterator;
+ for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){
+ Node assertion = *i;
+ TNode eq = assertion[0];
+ TNode x_i = eq[0];
+ TNode c_i = eq[1];
+ DeltaRational constant = c_i.getConst<Rational>();
+ if(getAssignment(x_i) == constant){
+ 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 caseSplits = lemmas;
+ //TODO
+ //DemandCaseSplits(caseSplits);
+ }
+}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index d211cd37d..82bb47eb4 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -1,7 +1,7 @@
/********************* */
/** theory_arith.h
** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: taking
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
@@ -20,22 +20,52 @@
#include "theory/theory.h"
#include "context/context.h"
+#include "context/cdlist.h"
+
+#include "theory/arith/delta_rational.h"
+#include "theory/arith/tableau.h"
+#include "theory/arith/arith_rewriter.h"
namespace CVC4 {
namespace theory {
namespace arith {
class TheoryArith : public Theory {
+private:
+ ArithConstants d_constants;
+
+ context::CDList<Node> d_diseq;
+ Tableau d_tableau;
+ ArithRewriter d_rewriter;
+
public:
TheoryArith(context::Context* c, OutputChannel& out) :
- Theory(c, out) {
- }
+ Theory(c, out),
+ d_constants(NodeManager::currentNM()), d_diseq(c), d_rewriter(&d_constants)
+ {}
+
+ Node rewrite(TNode n);
void preRegisterTerm(TNode n) { Unimplemented(); }
- void registerTerm(TNode n) { Unimplemented(); }
- void check(Effort e) { Unimplemented(); }
+ void registerTerm(TNode n);
+ void check(Effort e);
void propagate(Effort e) { Unimplemented(); }
void explain(TNode n, Effort e) { Unimplemented(); }
+
+private:
+ void AssertLower(TNode n);
+ void AssertUpper(TNode n);
+ void update(TNode x_i, DeltaRational& v);
+ void pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v);
+ TNode updateInconsistentVars();
+
+ TNode selectSlackBelow(TNode x_i);
+ TNode selectSlackAbove(TNode x_i);
+ TNode selectSmallestInconsistentVar();
+
+ Node generateConflictAbove(TNode conflictVar);
+ Node generateConflictBelow(TNode conflictVar);
+
};
}/* CVC4::theory::arith namespace */
diff --git a/src/util/rational.h b/src/util/rational.h
index e4f0e2bb7..90ac388b2 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -24,6 +24,7 @@
#ifndef __CVC4__RATIONAL_H
#define __CVC4__RATIONAL_H
+#include <gmp.h>
#include <string>
#include "util/integer.h"
@@ -93,7 +94,11 @@ public:
{
d_value.canonicalize();
}
-
+ Rational(const Integer& n) :
+ d_value(n.get_mpz())
+ {
+ d_value.canonicalize();
+ }
~Rational() {}
@@ -113,6 +118,20 @@ public:
return Integer(d_value.get_den());
}
+ Rational inverse() const {
+ return Rational(getDenominator(), getNumerator());
+ }
+
+ int cmp(const Rational& x) const {
+ //Don't use mpq_class's cmp() function.
+ //The name ends up conflicting with this function.
+ return mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t());
+ }
+
+
+ int sgn() {
+ return mpq_sgn(d_value.get_mpq_t());
+ }
Rational& operator=(const Rational& x){
if(this == &x) return *this;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback