From: Tim King Date: Wed, 28 Apr 2010 20:14:17 +0000 (+0000) Subject: Merging the arithmetic theory draft (lra-init) back into the main trunk. This should... X-Git-Tag: cvc5-1.0.0~9101 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c59fe5b21c218d3d6048cc5c34a7e27b3643ae78;p=cvc5.git Merging the arithmetic theory draft (lra-init) back into the main trunk. This should not affect other parts of the system. This code is untested, and is volatile. It is going to be improved in the future so don't pick on it too much. I am merging this code in its current state back into the main trunk because it was getting unruly to keep merging the updated trunk back into the branch. --- 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 +#include +#include + + +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(); + 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(); + c = -c; + TNode p_1 = rewritten[1]; + Rational d = p_1[0].getConst(); + 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 c1 = p1[0].getConst(); + + 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& 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 PnfSet; + PnfSet combined; + + for(vector::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 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(); + 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(); + 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() == 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::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& variables){ + NodeBuilder<> nb(kind::MULT); + nb << mkRationalNode(c); + for(std::set::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 variables; + vector sums; + stack > mult_iterators; + + mult_iterators.push(make_pair(t, t.begin())); + while(!mult_iterators.empty()){ + pair 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(); + 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::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 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 = 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. + * + *

= 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 mkConst(q); +} + +inline Node mkBoolNode(bool b){ + return NodeManager::currentNM()->mkConst(b); +} + + + +inline Rational coerceToRational(TNode constant){ + switch(constant.getKind()){ + case kind::CONST_INTEGER: + { + Rational q(constant.getConst()); + return q; + } + case kind::CONST_RATIONAL: + return constant.getConst(); + default: + Unreachable(); + } + Rational unreachable(0,0); + return unreachable; +} + +inline Node coerceToRationalNode(TNode constant){ + switch(constant.getKind()){ + case kind::CONST_INTEGER: + { + Rational q(constant.getConst()); + 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 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 IsNormal; + + +inline bool isNormalized(TNode x){ + return x.hasAttribute(IsNormal()); +} + +struct NormalFormAttrID; + +typedef expr::Attribute 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 = 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. + * + *

= 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 () != 0 && + p[0].getConst != 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 () != 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 = 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. + * + *

= 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 <| b, p |><| b, (+ p_1 .. p_N) |><| b}; + +PredicateNFKind kindOfNormalFormPredicate(TNode n){ + if(n.getKind() == CONST_BOOLEAN){ + if(n.getConst()){ + 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() != 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() !- 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 BoundsList; + +namespace partial_model { +struct DeltaRationalCleanupStrategy{ + static void cleanup(DeltaRational* dq){ + Debug("arithgc") << "cleaning up " << dq << "\n"; + delete dq; + } +}; + +struct AssignmentAttrID; +typedef expr::Attribute Assignment; + +// TODO should have a cleanup see bug #110 +struct LowerBoundAttrID; +typedef expr::CDAttribute LowerBound; + +// TODO should have a cleanup see bug #110 +struct UpperBoundAttrID; +typedef expr::CDAttribute UpperBound; + +struct LowerConstraintAttrID; +typedef expr::CDAttribute LowerConstraint; + +struct UpperConstraintAttrID; +typedef expr::CDAttribute UpperConstraint; + +typedef CVC4::context::CDList 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 BoundsListAttr; + +}; /*namespace partial_model*/ + +struct TheoryArithPropagatedID; +typedef expr::CDAttribute 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 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 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 +#include + +#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 CoefficientTable; + + std::set 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(); + } + } + + std::set::iterator begin(){ + return d_nonbasic.begin(); + } + + std::set::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::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::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 VarSet; + +private: + typedef __gnu_cxx::hash_map 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 + +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(), 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(),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::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::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::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::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::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(); + 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 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 #include #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;