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