*/
template <class T>
inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
+ bool anyRequireClearing = false;
+ typedef AttributeTraits<T, false> traits_t;
+ typedef AttrHash<T> hash_t;
for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
- typedef AttributeTraits<T, false> traits_t;
- typedef AttrHash<T> 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();
}
}
};
+// for hash_maps, hash_sets..
+struct TNodeHashFunction {
+ size_t operator()(CVC4::TNode node) const {
+ return (size_t) node.getId();
+ }
+};
+
template <bool ref_count>
inline size_t NodeTemplate<ref_count>::getNumChildren() const {
return d_nv->getNumChildren();
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
#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
Rational d_ONE;
Rational d_NEGATIVE_ONE;
+ DeltaRational d_ZERO_DELTA;
+
Node d_ZERO_NODE;
Node d_ONE_NODE;
Node d_NEGATIVE_ONE_NODE;
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))
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
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));
return nf;
}
+
//Transform this to: (left- right) |><| 0
Node diff = makeSubtractionNode(left, right);
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);
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'):
if(rewrittenChild.getMetaKind() == kind::metakind::CONSTANT){//c
Rational c = rewrittenChild.getConst<Rational>();
accumulator = accumulator * c;
- if(accumulator == 0){
+ if(accumulator == d_constants->d_ZERO){
return d_constants->d_ZERO_NODE;
}
}else if(rewrittenChild.getMetaKind() == kind::metakind::VARIABLE){ //v
* 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;
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];
}
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;
Node res;
- if(n.isAtomic()){
+ if(isRelationOperator(n.getKind())){
res = rewriteAtom(n);
}else{
res = rewriteTerm(n);
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);
Node var2pnf(TNode variable);
+ Node multPnfByNonZero(TNode pnf, Rational& q);
+
public:
ArithRewriter(ArithConstants* ac) :
d_constants(ac)
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();
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 */
-
+#include "expr/node.h"
#include "expr/attribute.h"
+
#ifndef __CVC4__THEORY__ARITH__BASIC_H
#define __CVC4__THEORY__ARITH__BASIC_H
inline bool isBasic(TNode x){
- return x.hasAttribute(IsBasic());
+ return x.getAttribute(IsBasic());
}
inline void makeBasic(TNode x){
--- /dev/null
+
+#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() << ")";
+}
#include "util/integer.h"
#include "util/rational.h"
+#include <ostream>
+
#ifndef __CVC4__THEORY__ARITH__DELTA_RATIONAL_H
#define __CVC4__THEORY__ARITH__DELTA_RATIONAL_H
+namespace CVC4 {
+
/**
* A DeltaRational is a pair of rationals (c,k) that represent the number
* c + kd
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;
return !(*this <= other);
}
- DeltaRational& operator=(DeltaRational& other){
+ DeltaRational& operator=(const DeltaRational& other){
c = other.c;
k = other.k;
return *(this);
}
};
+std::ostream& operator<<(std::ostream& os, const DeltaRational& n);
+
+}/* CVC4 namespace */
+
#endif /* __CVC4__THEORY__ARITH__DELTA_RATIONAL_H */
inline bool isNormalized(TNode x){
- return x.hasAttribute(IsNormal());
+ return x.getAttribute(IsNormal());
}
struct NormalFormAttrID;
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)
+
--- /dev/null
+
+#include "theory/arith/partial_model.h"
+#include "util/output.h"
+
+using namespace std;
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+using namespace CVC4::theory::arith::partial_model;
+
+void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ d_UpperBoundMap[x] = r;
+}
+
+void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ d_LowerBoundMap[x] = r;
+}
+
+void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ if(d_savingAssignments){
+ d_history.push_back(make_pair(x,r));
+ }
+
+ DeltaRational* c;
+ if(x.getAttribute(partial_model::Assignment(), c)){
+ *c = r;
+ Debug("partial_model") << "pm: updating the assignment to" << x
+ << " now " << r <<endl;
+ }else{
+ Debug("partial_model") << "pm: constructing an assignment for " << x
+ << " initially " << r <<endl;
+
+ c = new DeltaRational(r);
+ x.setAttribute(partial_model::Assignment(), c);
+ }
+}
+
+/** Must know that the bound exists both calling this! */
+DeltaRational ArithPartialModel::getUpperBound(TNode x) const {
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+ Assert(i != d_UpperBoundMap.end());
+
+ return DeltaRational((*i).second);
+}
+
+DeltaRational ArithPartialModel::getLowerBound(TNode x) const{
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+ Assert(i != d_LowerBoundMap.end());
+
+ return DeltaRational((*i).second);
+}
+
+
+DeltaRational ArithPartialModel::getAssignment(TNode x) const{
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ DeltaRational* assign;
+ AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+ return *assign;
+}
+
+
+void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ Debug("partial_model") << "setLowerConstraint("
+ << x << ":" << constraint << ")" << endl;
+
+ x.setAttribute(partial_model::LowerConstraint(),constraint);
+}
+
+void ArithPartialModel::setUpperConstraint(TNode x, TNode constraint){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ Debug("partial_model") << "setUpperConstraint("
+ << x << ":" << constraint << ")" << endl;
+
+ x.setAttribute(partial_model::UpperConstraint(),constraint);
+}
+
+TNode ArithPartialModel::getLowerConstraint(TNode x){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ TNode ret;
+ AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
+ return ret;
+}
+
+TNode ArithPartialModel::getUpperConstraint(TNode x){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+ TNode ret;
+ AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
+ return ret;
+}
+
+// TNode CVC4::theory::arith::getLowerConstraint(TNode x){
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+// TNode ret;
+// AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
+// return ret;
+// }
+
+// TNode CVC4::theory::arith::getUpperConstraint(TNode x){
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+// TNode ret;
+// AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
+// return ret;
+// }
+
+
+bool ArithPartialModel::belowLowerBound(TNode x, DeltaRational& c, bool strict){
+ CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+ if(i == d_LowerBoundMap.end()){
+ // l = -\intfy
+ // ? c < -\infty |- _|_
+ return false;
+ }
+
+ DeltaRational l = (*i).second;
+
+ if(strict){
+ return c < l;
+ }else{
+ return c <= l;
+ }
+}
+
+bool ArithPartialModel::aboveUpperBound(TNode x, DeltaRational& c, bool strict){
+ CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+ if(i == d_UpperBoundMap.end()){
+ // u = -\intfy
+ // ? u < -\infty |- _|_
+ return false;
+ }
+ DeltaRational u = (*i).second;
+
+ if(strict){
+ return c > u;
+ }else{
+ return c >= u;
+ }
+}
+
+bool ArithPartialModel::strictlyBelowUpperBound(TNode x){
+ DeltaRational* assign;
+ AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+
+ CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+ if(i == d_UpperBoundMap.end()){// u = \infty
+ return true;
+ }
+ DeltaRational u = (*i).second;
+
+ return *assign < u;
+}
+
+bool ArithPartialModel::strictlyAboveLowerBound(TNode x){
+ DeltaRational* assign;
+ AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+
+ CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+ if(i == d_LowerBoundMap.end()){// l = \infty
+ return true;
+ }
+ DeltaRational l = (*i).second;
+ return l < *assign;
+}
+
+bool ArithPartialModel::assignmentIsConsistent(TNode x){
+ DeltaRational beta = getAssignment(x);
+
+ bool above_li = !belowLowerBound(x,beta,true);
+ bool below_ui = !aboveUpperBound(x,beta,true);
+
+ //l_i <= beta(x_i) <= u_i
+ return above_li && below_ui;
+}
+
+void ArithPartialModel::beginRecordingAssignments(){
+ Assert(!d_savingAssignments);
+ Assert(d_history.empty());
+
+ d_savingAssignments = true;
+}
+
+
+void ArithPartialModel::stopRecordingAssignments(bool revert){
+ Assert(d_savingAssignments);
+
+ d_savingAssignments = false;
+
+ if(revert){
+ while(!d_history.empty()){
+ pair<TNode, DeltaRational>& curr = d_history.back();
+ d_history.pop_back();
+
+ TNode x = curr.first;
+
+ DeltaRational* c;
+ bool hasAssignment = x.getAttribute(partial_model::Assignment(), c);
+ Assert(hasAssignment);
+
+ *c = curr.second;
+ }
+ }else{
+ d_history.clear();
+ }
+
+}
-#include "context/cdlist.h"
#include "context/context.h"
+#include "context/cdmap.h"
#include "theory/arith/delta_rational.h"
+#include "expr/attribute.h"
#include "expr/node.h"
+#include <deque>
#ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
#define __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
namespace theory {
namespace arith {
-typedef CVC4::context::CDList<TNode> BoundsList;
-
namespace partial_model {
struct DeltaRationalCleanupStrategy{
static void cleanup(DeltaRational* 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;
+struct AssignmentAttrID {};
+typedef expr::Attribute<AssignmentAttrID,
+ DeltaRational*,
+ DeltaRationalCleanupStrategy> Assignment;
/**
- * BoundsListAttr is the attribute that maps a node to atoms .
+ * This defines a context dependent delta rational map.
+ * This is used to keep track of the current lower and upper bounds on
+ * each variable. This information is conext dependent.
+ */
+typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
+/* Side disucssion for why new tables are introduced instead of using the attribute
+ * framework.
+ * It comes down to that the obvious ways to use the current attribute framework do
+ * do not provide a terribly satisfying answer.
+ * - Suppose the type of the attribute is CD and maps to type DeltaRational.
+ * Well it can't map to a DeltaRational, and it thus it will be a DeltaRational*
+ * However being context dependent means givening up cleanup functions.
+ * So this leaks memory.
+ * - Suppose the type of the attribute is CD and the type mapped to
+ * was a Node wrapping a CONST_DELTA_RATIONAL.
+ * This was rejected for inefficiency, and uglyness.
+ * Inefficiency: Every lookup and comparison will require going through the
+ * massaging in between a node and the constant being wrapped. Every update
+ * requires going through the additional expense of creating at least 1 node.
+ * The Uglyness: If this was chosen it would also suggest using comparisons against
+ * DeltaRationals for the tracking the constraints for conflict analysis.
+ * This seems to invite misuse and introducing Nodes that should probably not escape
+ * arith.
+ * - Suppose that the of the attribute was not CD and mapped to a CDO<DeltaRational*>
+ * or similarly a ContextObj that wraps a DeltaRational*.
+ * This is currently rejected just because this is difficult to get right,
+ * and maintain. However with enough effort this the best solution is probably of
+ * this form.
*/
-typedef expr::Attribute<BoundsListID,
- BoundsList*,
- BoundsListCleanupStrategy> BoundsListAttr;
-
-}; /*namespace partial_model*/
-struct TheoryArithPropagatedID;
-typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
/**
- * Validates that a node constraint has the following form:
- * constraint: x |><| c
- * where |><| is either <, <=, ==, >=, LT and c is a constant rational.
+ * This is the literal that was asserted in the current context to the theory
+ * that asserted the tightest lower bound on a variable.
+ * For example: for a variable x this could be the constraint (>= x 4) or (not (<= x 50))
+ * Note the strong correspondence between this and LowerBoundMap.
+ * This is used during conflict analysis.
*/
-bool validateConstraint(TNode constraint){
- using namespace CVC4::kind;
- switch(constraint.getKind()){
- case LT:case LEQ: case EQUAL: case GEQ: case GT: break;
- default: return false;
- }
-
- if(constraint[0].getMetaKind() != metakind::VARIABLE) return false;
- return constraint[1].getKind() == CONST_RATIONAL;
-}
-
-void addBound(TNode constraint){
- Assert(validateConstraint(constraint));
- TNode x = constraint[0];
-
- BoundsList* bl;
- if(!x.getAttribute(partial_model::BoundsListAttr(), bl)){
- //TODO
- context::Context* context = NULL;
- bl = new (true) BoundsList(context);
- x.setAttribute(partial_model::BoundsListAttr(), bl);
- }
- bl->push_back(constraint);
-}
-
-inline int deltaCoeff(Kind k){
- switch(k){
- case kind::LT:
- return -1;
- case kind::GT:
- return 1;
- default:
- return 0;
- }
-}
-
+struct LowerConstraintAttrID {};
+typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint;
-inline bool negateBoundPropogation(CVC4::Kind k, bool isLowerBound){
- /* !isLowerBound
- * [x <= u && u < c] \=> x < c
- * [x <= u && u < c] \=> x <= c
- * [x <= u && u < c] \=> !(x == c)
- * [x <= u && u < c] \=> !(x >= c)
- * [x <= u && u < c] \=> !(x > c)
- */
- /* isLowerBound
- * [x >= l && l > c] \=> x > c
- * [x >= l && l > c] \=> x >= c
- * [x >= l && l > c] \=> !(x == c)
- * [x >= l && l > c] \=> !(x <= c)
- * [x >= l && l > c] \=> !(x < c)
- */
- using namespace CVC4::kind;
- switch(k){
- case LT:
- case LEQ:
- return isLowerBound;
- case EQUAL:
- return true;
- case GEQ:
- case GT:
- return !isLowerBound;
- default:
- Unreachable();
- return false;
- }
-}
+/**
+ * See the documentation for LowerConstraint.
+ */
+struct UpperConstraintAttrID {};
+typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint;
-void propogateBound(TNode constraint, OutputChannel& oc, bool isLower){
- constraint.setAttribute(TheoryArithPropagated(),true);
- bool neg = negateBoundPropogation(constraint.getKind(), isLower);
- if(neg){
- oc.propagate(constraint.notNode(),false);
- }else{
- oc.propagate(constraint,false);
- }
-}
-
-void propagateBoundConstraints(TNode x, OutputChannel& oc){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
- DeltaRational* l;
- DeltaRational* u;
- bool hasLowerBound = x.getAttribute(partial_model::LowerBound(), l);
- bool hasUpperBound = x.getAttribute(partial_model::UpperBound(), u);
-
- if(!(hasLowerBound || hasUpperBound)) return;
- BoundsList* bl;
-
- if(!x.getAttribute(partial_model::BoundsListAttr(), bl)) return;
-
- for(BoundsList::const_iterator iter = bl->begin(); iter != bl->end(); ++iter){
- TNode constraint = *iter;
- if(constraint.hasAttribute(TheoryArithPropagated())){
- continue;
- }
- //TODO improve efficiency Rational&
- Rational c = constraint[1].getConst<Rational>();
- Rational k(Integer(deltaCoeff(constraint.getKind())));
- DeltaRational ec(c, k);
- if(hasUpperBound && (*u) < ec ){
- propogateBound(constraint, oc, false);
- }
- if(hasLowerBound && (*l) > ec ){
- propogateBound(constraint, oc, true);
- }
- }
-}
-
-void setUpperBound(TNode x, DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* c;
- if(x.getAttribute(partial_model::UpperBound(), c)){
- *c = r;
- }else{
- c = new DeltaRational(r);
- x.setAttribute(partial_model::UpperBound(), c);
- }
-}
-
-void setLowerBound(TNode x, DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* c;
- if(x.getAttribute(partial_model::LowerBound(), c)){
- *c = r;
- }else{
- c = new DeltaRational(r);
- x.setAttribute(partial_model::LowerBound(), c);
- }
-}
-void setAssignment(TNode x, DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* c;
- if(x.getAttribute(partial_model::Assignment(), c)){
- *c = r;
- }else{
- c = new DeltaRational(r);
- x.setAttribute(partial_model::Assignment(), c);
- }
-}
+}; /*namespace partial_model*/
-/** Must know that the bound exists both calling this! */
-DeltaRational getUpperBound(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::UpperBound(),assign));
- return *assign;
-}
+struct TheoryArithPropagatedID {};
+typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
-DeltaRational getLowerBound(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::LowerBound(),assign));
- return *assign;
-}
+class ArithPartialModel {
+private:
+ partial_model::CDDRationalMap d_LowerBoundMap;
+ partial_model::CDDRationalMap d_UpperBoundMap;
-DeltaRational getAssignment(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ typedef std::pair<TNode, DeltaRational> HistoryPair;
+ typedef std::deque< HistoryPair > HistoryStack;
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
- return *assign;
-}
+ HistoryStack d_history;
-void setLowerConstraint(TNode constraint){
- TNode x = constraint[0];
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ bool d_savingAssignments;
- x.setAttribute(partial_model::LowerConstraint(),constraint);
-}
+public:
-void setUpperConstraint(TNode constraint){
- TNode x = constraint[0];
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ ArithPartialModel(context::Context* c):
+ d_LowerBoundMap(c),
+ d_UpperBoundMap(c),
+ d_history(),
+ d_savingAssignments(false)
+ { }
- x.setAttribute(partial_model::UpperConstraint(),constraint);
-}
-TNode getLowerConstraint(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ void setLowerConstraint(TNode x, TNode constraint);
+ void setUpperConstraint(TNode x, TNode constraint);
+ TNode getLowerConstraint(TNode x);
+ TNode getUpperConstraint(TNode x);
- TNode ret;
- AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
- return ret;
-}
-TNode getUpperConstraint(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ void beginRecordingAssignments();
- TNode ret;
- AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
- return ret;
-}
+ /* */
+ void stopRecordingAssignments(bool revert);
-/**
- * x <= l
- * ? c < l
- */
-bool belowLowerBound(TNode x, DeltaRational& c, bool strict){
- DeltaRational* l;
- if(!x.getAttribute(partial_model::LowerBound(), l)){
- // l = -\intfy
- // ? c < -\infty |- _|_
- return false;
- }
- if(strict){
- return c < *l;
- }else{
- return c <= *l;
- }
-}
+ void setUpperBound(TNode x, const DeltaRational& r);
+ void setLowerBound(TNode x, const DeltaRational& r);
+ void setAssignment(TNode x, const DeltaRational& r);
-/**
- * x <= u
- * ? c < u
- */
-bool aboveUpperBound(TNode x, DeltaRational& c, bool strict){
- DeltaRational* u;
- if(!x.getAttribute(partial_model::UpperBound(), u)){
- // c = \intfy
- // ? c > \infty |- _|_
- return false;
- }
+ /** Must know that the bound exists before calling this! */
+ DeltaRational getUpperBound(TNode x) const;
+ DeltaRational getLowerBound(TNode x) const;
+ DeltaRational getAssignment(TNode x) const;
- if(strict){
- return c > *u;
- }else{
- return c >= *u;
- }
-}
-bool strictlyBelowUpperBound(TNode x){
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+ /**
+ * x <= l
+ * ? c < l
+ */
+ bool belowLowerBound(TNode x, DeltaRational& c, bool strict);
- DeltaRational* u;
- if(!x.getAttribute(partial_model::UpperBound(), u)){ // u = \infty
- return true;
- }
- return *assign < *u;
-}
+ /**
+ * x <= u
+ * ? c < u
+ */
+ bool aboveUpperBound(TNode x, DeltaRational& c, bool strict);
-bool strictlyAboveLowerBound(TNode x){
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+ bool strictlyBelowUpperBound(TNode x);
+ bool strictlyAboveLowerBound(TNode x);
+ bool assignmentIsConsistent(TNode x);
+};
- DeltaRational* l;
- if(!x.getAttribute(partial_model::LowerBound(), l)){ // l = -\infty
- return true;
- }
- return *l < *assign;
-}
-bool assignmentIsConsistent(TNode x){
- DeltaRational beta = getAssignment(x);
- //l_i <= beta(x_i) <= u_i
- return !aboveUpperBound(x,beta, true) && !belowLowerBound(x,beta,true);
-}
}; /* namesapce arith */
}; /* namespace theory */
//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);
}
#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"
#include "theory/arith/tableau.h"
#include "theory/arith/normal.h"
#include "theory/arith/slack.h"
+#include "theory/arith/basic.h"
#include "theory/arith/arith_rewriter.h"
#include "theory/arith/theory_arith.h"
#include <map>
+#include <stdint.h>
using namespace std;
using namespace CVC4::theory;
using namespace CVC4::theory::arith;
+TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
+ Theory(c, out),
+ d_constants(NodeManager::currentNM()),
+ d_partialModel(c),
+ d_diseq(c),
+ d_preprocessed(c),
+ d_rewriter(&d_constants)
+{
+ uint64_t ass_id = partial_model::Assignment::getId();
+ Debug("arithsetup") << "Assignment: " << ass_id
+ << std::endl;
+}
+
bool isBasicSum(TNode n){
- Unimplemented();
- return false;
+ if(n.getKind() != kind::PLUS) return false;
+
+ for(TNode::const_iterator i=n.begin(); i!=n.end(); ++i){
+ TNode child = *i;
+ if(child.getKind() != MULT) return false;
+ if(child[0].getKind() != CONST_RATIONAL) return false;
+ for(unsigned j=1; j<child.getNumChildren(); ++j){
+ TNode var = child[j];
+ if(var.getMetaKind() != metakind::VARIABLE) return false;
+ }
+ }
+ return true;
}
Kind multKind(Kind k){
void registerAtom(TNode rel){
- addBound(rel);
+ //addBound(rel);
//Anything else?
}
Node TheoryArith::rewrite(TNode n){
- return d_rewriter.rewrite(n);
+ Debug("arith") << "rewrite(" << n << ")" << endl;
+
+ Node result = d_rewriter.rewrite(n);
+ Debug("arith-rewrite") << "rewrite("
+ << n << " -> " << result
+ << ")" << endl;
+ return result;
}
void TheoryArith::registerTerm(TNode tn){
- if(tn.isAtomic()){
+ Debug("arith") << "registerTerm(" << tn << ")" << endl;
+
+ if(tn.getKind() == kind::BUILTIN) return;
+
+ if(tn.getMetaKind() == metakind::VARIABLE){
+ d_partialModel.setAssignment(tn,d_constants.d_ZERO_DELTA);
+ }
+
+ //TODO is an atom
+ if(isRelationOperator(tn.getKind())){
Node normalForm = (isNormalized(tn)) ? Node(tn) : rewrite(tn);
+ normalForm = (normalForm.getKind() == NOT) ? pushInNegation(normalForm):normalForm;
Kind k = normalForm.getKind();
if(k != kind::CONST_BOOLEAN){
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);
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);
}
/* procedure AssertUpper( x_i <= c_i) */
-void TheoryArith::AssertUpper(TNode n){
+void TheoryArith::AssertUpper(TNode n, TNode original){
TNode x_i = n[0];
Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
DeltaRational c_i(n[1].getConst<Rational>(), dcoeff);
- if(aboveUpperBound(x_i, c_i, false) ){
+
+ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
+
+
+ if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){
return; //sat
}
- if(belowLowerBound(x_i, c_i, true)){
- d_out->conflict(n);
+ if(d_partialModel.belowLowerBound(x_i, c_i, true)){
+ Node conflict = NodeManager::currentNM()->mkNode(AND, d_partialModel.getLowerConstraint(x_i), original);
+ d_out->conflict(conflict);
return;
}
- setUpperConstraint(n);
- setUpperBound(x_i, c_i);
+ d_partialModel.setUpperConstraint(x_i,original);
+ d_partialModel.setUpperBound(x_i, c_i);
if(!isBasic(x_i)){
- if(getAssignment(x_i) > c_i){
+ if(d_partialModel.getAssignment(x_i) > c_i){
update(x_i, c_i);
}
}
}
/* procedure AssertLower( x_i >= c_i ) */
-void TheoryArith::AssertLower(TNode n){
+void TheoryArith::AssertLower(TNode n, TNode orig){
TNode x_i = n[0];
Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
DeltaRational c_i(n[1].getConst<Rational>(),dcoeff);
- if(belowLowerBound(x_i, c_i, false)){
+ Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
+
+ if(d_partialModel.belowLowerBound(x_i, c_i, false)){
return; //sat
}
- if(aboveUpperBound(x_i, c_i, true)){
- d_out->conflict(n);
+ if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
+ Node conflict = NodeManager::currentNM()->mkNode(AND, d_partialModel.getUpperConstraint(x_i), orig);
+ d_out->conflict(conflict);
return;
}
- setLowerConstraint(n);
- setLowerBound(x_i, c_i);
+ d_partialModel.setLowerConstraint(x_i,orig);
+ d_partialModel.setLowerBound(x_i, c_i);
if(!isBasic(x_i)){
- if(getAssignment(x_i) > c_i){
+ if(d_partialModel.getAssignment(x_i) < c_i){
update(x_i, c_i);
}
}
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();
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();
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);
}
}
++basicIter){
TNode basic = *basicIter;
- if(!assignmentIsConsistent(basic)){
+ if(!d_partialModel.assignmentIsConsistent(basic)){
return basic;
}
}
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 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);
}
Row* row_i = d_tableau.lookup(conflictVar);
NodeBuilder<> nb(kind::AND);
- nb << getUpperConstraint(conflictVar);
+ TNode bound = d_partialModel.getUpperConstraint(conflictVar);
+
+ Debug("arith") << "generateConflictAbove "
+ << "conflictVar " << conflictVar
+ << " " << bound << endl;
+
+ nb << bound;
typedef std::set<TNode>::iterator NonBasicIter;
Assert(a_ij != d_constants.d_ZERO);
if(a_ij < d_constants.d_ZERO){
- nb << getUpperConstraint(nonbasic);
+ bound = d_partialModel.getUpperConstraint(nonbasic);
+ Debug("arith") << "below 0 "<< nonbasic << " " << bound << endl;
+ nb << bound;
}else{
- nb << getLowerConstraint(nonbasic);
+ bound = d_partialModel.getLowerConstraint(nonbasic);
+ Debug("arith") << " above 0 "<< nonbasic << " " << bound << endl;
+ nb << bound;
}
}
Node conflict = nb;
return conflict;
}
+
Node TheoryArith::generateConflictBelow(TNode conflictVar){
Row* row_i = d_tableau.lookup(conflictVar);
NodeBuilder<> nb(kind::AND);
- nb << getLowerConstraint(conflictVar);
+ TNode bound = d_partialModel.getLowerConstraint(conflictVar);
+
+ Debug("arith") << "generateConflictBelow "
+ << "conflictVar " << conflictVar
+ << " " << bound << endl;
+ nb << bound;
typedef std::set<TNode>::iterator NonBasicIter;
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();
}
if(fullEffort(level)){
Node possibleConflict = updateInconsistentVars();
if(possibleConflict != Node::null()){
+ Debug("arith") << "Found a conflict " << possibleConflict << endl;
d_out->conflict(possibleConflict);
}
}
if(fullEffort(level)){
- NodeBuilder<> lemmas(AND);
+ bool enqueuedCaseSplit = false;
typedef context::CDList<Node>::const_iterator diseq_iterator;
for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){
Node assertion = *i;
TNode x_i = eq[0];
TNode c_i = eq[1];
DeltaRational constant = c_i.getConst<Rational>();
- if(getAssignment(x_i) == constant){
+ if(d_partialModel.getAssignment(x_i) == constant){
+ enqueuedCaseSplit = true;
Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
- Node disjunct = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
- lemmas<< disjunct;
+ Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
+ //d_out->enqueueCaseSplits(caseSplit);
}
}
- Node caseSplits = lemmas;
- //TODO
- //DemandCaseSplits(caseSplits);
+ if(enqueuedCaseSplit){
+ //d_out->caseSplit();
+ }
}
}
#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 {
class TheoryArith : public Theory {
private:
ArithConstants d_constants;
+ ArithPartialModel d_partialModel;
context::CDList<Node> d_diseq;
+ context::CDList<Node> d_preprocessed;
+ //TODO This is currently needed to save preprocessed nodes that may not
+ //currently have an outisde reference. Get rid of when preprocessing is occuring
+ //correctly.
+
Tableau d_tableau;
ArithRewriter d_rewriter;
public:
- TheoryArith(context::Context* c, OutputChannel& out) :
- Theory(c, out),
- d_constants(NodeManager::currentNM()), d_diseq(c), d_rewriter(&d_constants)
- {}
+ TheoryArith(context::Context* c, OutputChannel& out);
Node rewrite(TNode n);
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);
Node generateConflictAbove(TNode conflictVar);
Node generateConflictBelow(TNode conflictVar);
+ //TODO get rid of this!
+ Node simulatePreprocessing(TNode n);
+
};
}/* CVC4::theory::arith namespace */
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&) {
logops.04.cvc \
logops.05.cvc \
simple.cvc \
+ ineq_basic.smt \
+ ineq_slack.smt \
smallcnf.cvc \
test11.cvc \
test9.cvc \
--- /dev/null
+(benchmark ineq_basic
+:status unsat
+:logic QF_LRA
+:extrafuns ((x Real))
+:formula
+ (and (<= 0 x)
+ (< x 0)
+ )
+)
--- /dev/null
+(benchmark ineq_basic
+:status unsat
+:logic QF_LRA
+:extrafuns ((x Real))
+:extrafuns ((y Real))
+:formula
+ (and (<= (+ x y) 0)
+ (< 1 x)
+ (<= 0 y)
+ )
+)
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;
+// }
};
projects / cvc5.git / commitdiff