Node PropEngine::getValue(TNode node) const {
Assert(node.getType().isBoolean());
+ Assert(d_cnfStream->hasLiteral(node));
+
SatLiteral lit = d_cnfStream->getLiteral(node);
SatLiteralValue v = d_satSolver->value(lit);
bool PropEngine::hasValue(TNode node, bool& value) const {
Assert(node.getType().isBoolean());
+ Assert(d_cnfStream->hasLiteral(node));
+
SatLiteral lit = d_cnfStream->getLiteral(node);
SatLiteralValue v = d_satSolver->value(lit);
arithvar_node_map.h \
atom_database.h \
atom_database.cpp \
+ difference_manager.h \
+ difference_manager.cpp \
normal_form.h\
normal_form.cpp \
arith_utilities.h \
bool asserted = isAsserted(bestImplied);
if( !asserted && !isPropagated(bestImplied)){
- propagate(bestImplied, reason);
+ propagate(bestImplied, reason, false);
++d_statistics.d_addedPropagation;
success = true;
}else if(!asserted){
namespace arith {
class PropManager {
+public:
+ struct PropUnit {
+ // consequent <= antecedent
+ Node consequent;
+ Node antecedent;
+ bool flag;
+ PropUnit(Node c, Node a, bool f) :
+ consequent(c), antecedent(a), flag(f)
+ {}
+ };
+
private:
- context::CDList<TNode> d_propagated;
+ context::CDList<PropUnit> d_propagated;
+
context::CDO<uint32_t> d_propagatedPos;
- typedef context::CDMap<TNode, TNode, TNodeHashFunction> ExplainMap;
+ typedef context::CDMap<Node, size_t, NodeHashFunction> ExplainMap;
ExplainMap d_explanationMap;
- context::CDList<Node> d_reasons;
+ size_t getIndex(TNode n) const {
+ Assert(isPropagated(n));
+ return (*(d_explanationMap.find(n))).second;
+ }
public:
PropManager(context::Context* c):
d_propagated(c),
d_propagatedPos(c, 0),
- d_explanationMap(c),
- d_reasons(c)
+ d_explanationMap(c)
{ }
+ const PropUnit& getUnit(TNode n) const {
+ return d_propagated[getIndex(n)];
+ }
+
bool isPropagated(TNode n) const {
return d_explanationMap.find(n) != d_explanationMap.end();
}
- void propagate(TNode n, Node reason) {
- Assert(!isPropagated(n));
- Assert(reason.getKind() == kind::AND);
+ bool isFlagged(TNode n) const {
+ return getUnit(n).flag;
+ }
- d_explanationMap.insert(n, reason);
+ void propagate(TNode n, Node reason, bool flag) {
+ Assert(!isPropagated(n));
- d_reasons.push_back(reason);
- d_propagated.push_back(n);
+ d_explanationMap.insert(n, d_propagated.size());
+ d_propagated.push_back(PropUnit(n, reason, flag));
Debug("ArithPropManager") << n << std::endl << "<="<< reason<< std::endl;
}
return d_propagatedPos < d_propagated.size();
}
- TNode getPropagation() {
+ const PropUnit& getNextPropagation() {
Assert(hasMorePropagations());
- TNode prop = d_propagated[d_propagatedPos];
+ const PropUnit& prop = d_propagated[d_propagatedPos];
d_propagatedPos = d_propagatedPos + 1;
return prop;
}
TNode explain(TNode n) const {
- Assert(isPropagated(n));
- ExplainMap::iterator p = d_explanationMap.find(n);
- return (*p).second;
+ return getUnit(n).antecedent;
}
};/* class PropManager */
return c;
}
+ int sgn() const {
+ int x = getNoninfinitesimalPart().sgn();
+ if(x == 0){
+ return getInfinitesimalPart().sgn();
+ }else{
+ return x;
+ }
+ }
+
DeltaRational operator+(const DeltaRational& other) const{
CVC4::Rational tmpC = c+other.c;
CVC4::Rational tmpK = k+other.k;
--- /dev/null
+#include "theory/arith/difference_manager.h"
+#include "theory/uf/equality_engine_impl.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+DifferenceManager::DifferenceManager(context::Context* c, PropManager& pm)
+ : d_reasons(c),
+ d_queue(pm),
+ d_notify(*this),
+ d_ee(d_notify, c, "theory::arith::DifferenceManager"),
+ d_false(NodeManager::currentNM()->mkConst<bool>(false))
+{}
+
+void DifferenceManager::propagate(TNode x){
+ Debug("arith::differenceManager")<< "DifferenceManager::propagate("<<x<<")"<<std::endl;
+
+ d_queue.propagate(x, Node::null(), true);
+}
+
+void DifferenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
+ TNode lhs, rhs;
+ switch (literal.getKind()) {
+ case kind::EQUAL:
+ lhs = literal[0];
+ rhs = literal[1];
+ break;
+ case kind::NOT:
+ lhs = literal[0];
+ rhs = d_false;
+ break;
+ default:
+ Unreachable();
+ }
+ d_ee.getExplanation(lhs, rhs, assumptions);
+}
+
+#warning "Stolen from theory_uf.h verbatim. Generalize me!"
+Node mkAnd(const std::vector<TNode>& conjunctions) {
+ Assert(conjunctions.size() > 0);
+
+ std::set<TNode> all;
+ all.insert(conjunctions.begin(), conjunctions.end());
+
+ if (all.size() == 1) {
+ // All the same, or just one
+ return conjunctions[0];
+ }
+
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::const_iterator it_end = all.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+
+ return conjunction;
+}
+
+
+Node DifferenceManager::explain(TNode lit){
+ std::vector<TNode> assumptions;
+ explain(lit, assumptions);
+ return mkAnd(assumptions);
+}
+
+void DifferenceManager::addDifference(ArithVar s, Node x, Node y){
+ Assert(s >= d_differences.size() || !isDifferenceSlack(s));
+
+ Debug("arith::differenceManager") << s << x << y << std::endl;
+
+ d_differences.resize(s+1);
+ d_differences[s] = Difference(x,y);
+}
+
+void DifferenceManager::differenceIsZero(ArithVar s, TNode reason){
+ Assert(isDifferenceSlack(s));
+ TNode x = d_differences[s].x;
+ TNode y = d_differences[s].y;
+
+ d_reasons.push_back(reason);
+ d_ee.addEquality(x, y, reason);
+}
+
+void DifferenceManager::differenceCannotBeZero(ArithVar s, TNode reason){
+ Assert(isDifferenceSlack(s));
+ TNode x = d_differences[s].x;
+ TNode y = d_differences[s].y;
+
+ d_reasons.push_back(reason);
+ d_ee.addDisequality(x, y, reason);
+}
+
+void DifferenceManager::addSharedTerm(Node x){
+ d_ee.addTriggerTerm(x);
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
+#define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
+
+#include "theory/arith/arith_utilities.h"
+#include "theory/uf/equality_engine.h"
+#include "context/cdo.h"
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "util/stats.h"
+#include "theory/arith/arith_prop_manager.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class DifferenceManager {
+private:
+ struct Difference {
+ bool isSlack;
+ TNode x;
+ TNode y;
+ Difference() : isSlack(false), x(TNode::null()), y(TNode::null()){}
+ Difference(TNode a, TNode b) : isSlack(true), x(a), y(b) {
+ Assert(x < y);
+ }
+ };
+
+
+ class DifferenceNotifyClass {
+ private:
+ DifferenceManager& d_dm;
+ public:
+ DifferenceNotifyClass(DifferenceManager& dm): d_dm(dm) {}
+
+ bool notify(TNode propagation) {
+ Debug("arith::differences") << "DifferenceNotifyClass::notify(" << propagation << ")" << std::endl;
+ // Just forward to dm
+ d_dm.propagate(propagation);
+ return true;
+ }
+
+ void notify(TNode t1, TNode t2) {
+ Debug("arith::differences") << "DifferenceNotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+ Node equality = t1.eqNode(t2);
+ d_dm.propagate(equality);
+ }
+ };
+
+ std::vector< Difference > d_differences;
+
+ context::CDList<Node> d_reasons;
+ PropManager& d_queue;
+
+
+ DifferenceNotifyClass d_notify;
+ theory::uf::EqualityEngine<DifferenceNotifyClass> d_ee;
+
+ void propagate(TNode x);
+ void explain(TNode literal, std::vector<TNode>& assumptions);
+
+ Node d_false;
+
+public:
+
+ DifferenceManager(context::Context*, PropManager&);
+
+ Node explain(TNode literal);
+
+ void addDifference(ArithVar s, Node x, Node y);
+
+ inline bool isDifferenceSlack(ArithVar s) const{
+ if(s < d_differences.size()){
+ return d_differences[s].isSlack;
+ }else{
+ return false;
+ }
+ }
+
+ void differenceIsZero(ArithVar s, TNode reason);
+
+ void differenceCannotBeZero(ArithVar s, TNode reason);
+
+ void addSharedTerm(Node x);
+};/* class DifferenceManager */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H */
+
using namespace CVC4::theory;
using namespace CVC4::theory::arith;
+
+
+void ArithPartialModel::zeroDifferenceDetected(ArithVar x){
+ Assert(d_dm.isDifferenceSlack(x));
+ Assert(upperBoundIsZero(x));
+ Assert(lowerBoundIsZero(x));
+
+ Node lb = getLowerConstraint(x);
+ Node ub = getUpperConstraint(x);
+ Node reason = lb != ub ? lb.andNode(ub) : lb;
+ d_dm.differenceIsZero(x, reason);
+}
+
void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){
d_deltaIsSafe = false;
Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl;
d_hasHadABound[x] = true;
d_upperBound.set(x,r);
+
+ if(d_dm.isDifferenceSlack(x)){
+ int sgn = r.sgn();
+ if(sgn < 0){
+ d_dm.differenceCannotBeZero(x, getUpperConstraint(x));
+ }else if(sgn == 0 && lowerBoundIsZero(x)){
+ zeroDifferenceDetected(x);
+ }
+ }
}
void ArithPartialModel::setLowerBound(ArithVar x, const DeltaRational& r){
d_deltaIsSafe = false;
+ Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
d_hasHadABound[x] = true;
d_lowerBound.set(x,r);
+
+
+ if(d_dm.isDifferenceSlack(x)){
+ int sgn = r.sgn();
+ if(sgn > 0){
+ d_dm.differenceCannotBeZero(x, getLowerConstraint(x));
+ }else if(sgn == 0 && upperBoundIsZero(x)){
+ zeroDifferenceDetected(x);
+ }
+ }
}
void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){
#include "expr/attribute.h"
#include "expr/node.h"
+#include "theory/arith/difference_manager.h"
+
#include <deque>
#ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
context::CDVector<Node> d_upperConstraint;
context::CDVector<Node> d_lowerConstraint;
+
bool d_deltaIsSafe;
Rational d_delta;
typedef std::vector<ArithVar> HistoryList;
HistoryList d_history;
+ DifferenceManager& d_dm;
+
public:
- ArithPartialModel(context::Context* c):
+ ArithPartialModel(context::Context* c, DifferenceManager& dm):
d_mapSize(0),
d_hasHadABound(),
d_hasSafeAssignment(),
d_lowerConstraint(c,true),
d_deltaIsSafe(false),
d_delta(-1,1),
- d_history()
+ d_history(),
+ d_dm(dm)
{ }
void setLowerConstraint(ArithVar x, TNode constraint);
void commitAssignmentChanges();
+ inline bool lowerBoundIsZero(ArithVar x){
+ return hasLowerBound(x) && getLowerBound(x).sgn() == 0;
+ }
+
+ inline bool upperBoundIsZero(ArithVar x){
+ return hasUpperBound(x) && getUpperBound(x).sgn() == 0;
+ }
+
+private:
+ void zeroDifferenceDetected(ArithVar x);
+
+public:
void setUpperBound(ArithVar x, const DeltaRational& r);
const DeltaRational& getAssignment(ArithVar x) const;
+
/**
* x >= l
* ? c < l
explainNonbasicsLowerBound(basic, nb);
}
Node explanation = nb;
- d_propManager.propagate(bestImplied, explanation);
+ d_propManager.propagate(bestImplied, explanation, false);
return true;
}else{
Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl;
d_atomsInContext(c),
d_learner(d_pbSubstitutions),
d_nextIntegerCheckVar(0),
- d_partialModel(c),
+ d_partialModel(c, d_differenceManager),
d_userVariables(),
d_diseq(c),
d_tableau(),
d_tableauResetPeriod(10),
d_atomDatabase(c, out),
d_propManager(c, d_arithvarNodeMap, d_atomDatabase, valuation),
+ d_differenceManager(c, d_propManager),
d_simplex(d_propManager, d_partialModel, d_tableau),
d_DELTA_ZERO(0),
d_statistics()
d_staticLearningTimer("theory::arith::staticLearningTimer"),
d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
d_presolveTime("theory::arith::presolveTime"),
+ d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0),
d_initialTableauSize("theory::arith::initialTableauSize", 0),
d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
StatisticsRegistry::registerStat(&d_presolveTime);
+ StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
StatisticsRegistry::registerStat(&d_initialTableauSize);
StatisticsRegistry::registerStat(&d_currSetToSmaller);
StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
StatisticsRegistry::unregisterStat(&d_presolveTime);
+ StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
StatisticsRegistry::unregisterStat(&d_initialTableauSize);
StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
StatisticsRegistry::unregisterStat(&d_restartTimer);
}
+
+void TheoryArith::addSharedTerm(TNode n){
+ d_differenceManager.addSharedTerm(n);
+}
+
Node TheoryArith::preprocess(TNode atom) {
Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
d_tableau.addRow(varSlack, coefficients, variables);
setupInitialValue(varSlack);
+ //Add differences to the difference manager
+ Polynomial::iterator i = poly.begin(), end = poly.end();
+ if(i != end){
+ Monomial first = *i;
+ ++i;
+ if(i != end){
+ Monomial second = *i;
+ ++i;
+ if(i == end){
+ if(first.getConstant().isOne() && second.getConstant().getValue() == -1){
+ VarList vl0 = first.getVarList();
+ VarList vl1 = second.getVarList();
+ if(vl0.singleton() && vl1.singleton()){
+ d_differenceManager.addDifference(varSlack, vl0.getNode(), vl1.getNode());
+ }
+ }
+ }
+ }
+ }
+
++(d_statistics.d_statSlackVariables);
markSetup(polyNode);
}
} else {
Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl;
}
+ ++(d_statistics.d_externalBranchAndBounds);
d_out->lemma(lem);
// split only on one var
} else {
Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl;
}
+ ++(d_statistics.d_externalBranchAndBounds);
d_out->lemma(lem);
// split only on one var
} else {
Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl;
}
+ ++(d_statistics.d_externalBranchAndBounds);
d_out->lemma(lem);
// split only on one var
Node TheoryArith::explain(TNode n) {
Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
Assert(d_propManager.isPropagated(n));
- return d_propManager.explain(n);
+
+ if(d_propManager.isFlagged(n)){
+ return d_differenceManager.explain(n);
+ }else{
+ return d_propManager.explain(n);
+ }
}
void TheoryArith::propagate(Effort e) {
}
while(d_propManager.hasMorePropagations()){
- TNode toProp = d_propManager.getPropagation();
+ const PropManager::PropUnit next = d_propManager.getNextPropagation();
+ bool flag = next.flag;
+ TNode toProp = next.consequent;
+
TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
- if(inContextAtom(atom)){
+
+ Debug("arith::propagate") << "propagate " << flag << " " << toProp << endl;
+
+ if(flag) {
+ //Currently if the flag is set this came from an equality detected by the
+ //equality engine in the the difference manager.
+ d_out->propagate(toProp);
+ propagated = true;
+ }else if(inContextAtom(atom)){
Node satValue = d_valuation.getSatValue(toProp);
AlwaysAssert(satValue.isNull());
propagated = true;
}else{
//Not clear if this is a good time to do this or not...
Debug("arith::propagate") << "Atom is not in context" << toProp << endl;
- #warning "enable remove atom in database"
+#warning "enable remove atom in database"
//d_atomDatabase.removeAtom(atom);
}
}
#include "theory/arith/arith_prop_manager.h"
#include "theory/arith/arithvar_node_map.h"
#include "theory/arith/dio_solver.h"
+#include "theory/arith/difference_manager.h"
#include "util/stats.h"
/** This manager keeps track of information needed to propagate. */
ArithPropManager d_propManager;
+ /** This keeps track of difference equalities. Mostly for sharing. */
+ DifferenceManager d_differenceManager;
+
/** This implements the Simplex decision procedure. */
SimplexDecisionProcedure d_simplex;
-
public:
TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
virtual ~TheoryArith();
EqualityStatus getEqualityStatus(TNode a, TNode b);
+ void addSharedTerm(TNode n);
+
private:
/** The constant zero. */
DeltaRational d_DELTA_ZERO;
IntStat d_permanentlyRemovedVariables;
TimerStat d_presolveTime;
+ IntStat d_externalBranchAndBounds;
+
IntStat d_initialTableauSize;
IntStat d_currSetToSmaller;
IntStat d_smallerSetToCurr;
TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
if (atom.getKind() == kind::EQUAL) {
explainEquality(theoryId, literal, builder);
+ } else if(literal.getKind() == kind::AND){
+ explainEqualities(theoryId, literal, builder);
} else {
builder << literal;
}
projects / cvc5.git / commitdiff