diff options
-rw-r--r-- | src/theory/arith/Makefile.am | 11 | ||||
-rw-r--r-- | src/theory/arith/arith_constants.h | 38 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 468 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 92 | ||||
-rw-r--r-- | src/theory/arith/arith_utilities.h | 128 | ||||
-rw-r--r-- | src/theory/arith/basic.h | 33 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.h | 82 | ||||
-rw-r--r-- | src/theory/arith/normal.h | 29 | ||||
-rw-r--r-- | src/theory/arith/normal_form_notes.txt | 455 | ||||
-rw-r--r-- | src/theory/arith/partial_model.h | 342 | ||||
-rw-r--r-- | src/theory/arith/slack.h | 14 | ||||
-rw-r--r-- | src/theory/arith/tableau.h | 243 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 384 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 40 | ||||
-rw-r--r-- | src/util/rational.h | 21 |
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; |