summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/arithvar.cpp6
-rw-r--r--src/theory/arith/arithvar.h3
-rw-r--r--src/theory/arith/callbacks.cpp114
-rw-r--r--src/theory/arith/callbacks.h77
-rw-r--r--src/theory/arith/congruence_manager.cpp8
-rw-r--r--src/theory/arith/congruence_manager.h4
-rw-r--r--src/theory/arith/constraint.cpp889
-rw-r--r--src/theory/arith/constraint.h523
-rw-r--r--src/theory/arith/constraint_forward.h14
-rw-r--r--src/theory/arith/dio_solver.cpp7
-rw-r--r--src/theory/arith/linear_equality.cpp187
-rw-r--r--src/theory/arith/linear_equality.h31
-rw-r--r--src/theory/arith/normal_form.cpp31
-rw-r--r--src/theory/arith/normal_form.h31
-rw-r--r--src/theory/arith/simplex.cpp46
-rw-r--r--src/theory/arith/simplex.h12
-rw-r--r--src/theory/arith/soi_simplex.cpp129
-rw-r--r--src/theory/arith/soi_simplex.h2
-rw-r--r--src/theory/arith/tableau.cpp4
-rw-r--r--src/theory/arith/theory_arith_private.cpp661
-rw-r--r--src/theory/arith/theory_arith_private.h38
21 files changed, 1907 insertions, 910 deletions
diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp
index 9a7878750..acae61db0 100644
--- a/src/theory/arith/arithvar.cpp
+++ b/src/theory/arith/arithvar.cpp
@@ -18,6 +18,7 @@
#include "theory/arith/arithvar.h"
#include <limits>
+#include <set>
namespace CVC4 {
namespace theory {
@@ -25,6 +26,11 @@ namespace arith {
const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
+bool debugIsASet(const std::vector<ArithVar>& variables){
+ std::set<ArithVar> asSet(variables.begin(), variables.end());
+ return asSet.size() == variables.size();
+}
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index 00545fb48..dd049e94f 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -37,6 +37,9 @@ typedef std::vector<ArithVar> ArithVarVec;
typedef std::pair<ArithVar, Rational> ArithRatPair;
typedef std::vector< ArithRatPair > ArithRatPairVec;
+extern bool debugIsASet(const ArithVarVec& variables);
+
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 68bf3bbae..b6e579465 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -57,29 +57,117 @@ void BasicVarModelUpdateCallBack::operator()(ArithVar x){
d_ta.signal(x);
}
-RaiseConflict::RaiseConflict(TheoryArithPrivate& ta, ConstraintCPVec& buf )
+RaiseConflict::RaiseConflict(TheoryArithPrivate& ta)
: d_ta(ta)
- , d_construction(buf)
{}
+void RaiseConflict::raiseConflict(ConstraintCP c) const{
+ Assert(c->inConflict());
+ d_ta.raiseConflict(c);
+}
+
+FarkasConflictBuilder::FarkasConflictBuilder()
+ : d_farkas()
+ , d_constraints()
+ , d_consequent(NullConstraint)
+ , d_consequentSet(false)
+{
+ reset();
+}
+
+bool FarkasConflictBuilder::underConstruction() const{
+ return d_consequent != NullConstraint;
+}
+
+bool FarkasConflictBuilder::consequentIsSet() const{
+ return d_consequentSet;
+}
+
+void FarkasConflictBuilder::reset(){
+ d_consequent = NullConstraint;
+ d_constraints.clear();
+ d_consequentSet = false;
+ PROOF(d_farkas.clear());
+ Assert(!underConstruction());
+}
+
/* Adds a constraint to the constraint under construction. */
-void RaiseConflict::addConstraint(ConstraintCP c){
- d_construction.push_back(c);
+void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
+ Assert(!PROOF_ON() ||
+ (!underConstruction() && d_constraints.empty() && d_farkas.empty()) ||
+ (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
+ Assert(PROOF_ON() || d_farkas.empty());
+ Assert(c->isTrue());
+
+
+ if(d_consequent == NullConstraint){
+ d_consequent = c;
+ } else {
+ d_constraints.push_back(c);
+ }
+ PROOF(d_farkas.push_back(fc););
+ Assert(!PROOF_ON() || d_constraints.size() + 1 == d_farkas.size());
+ Assert(PROOF_ON() || d_farkas.empty());
}
-/* Turns the vector under construction into a conflict */
-void RaiseConflict::commitConflict(){
- Assert(!d_construction.empty());
- sendConflict(d_construction);
- d_construction.clear();
+
+void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){
+ Assert(!mult.isZero());
+ if(PROOF_ON() && !mult.isOne()){
+ Rational prod = fc * mult;
+ addConstraint(c, prod);
+ }else{
+ addConstraint(c, fc);
+ }
}
-void RaiseConflict::sendConflict(const ConstraintCPVec& vec){
- d_ta.raiseConflict(vec);
+void FarkasConflictBuilder::makeLastConsequent(){
+ Assert(!d_consequentSet);
+ Assert(underConstruction());
+
+ if(d_constraints.empty()){
+ // no-op
+ d_consequentSet = true;
+ } else {
+ Assert(d_consequent != NullConstraint);
+ ConstraintCP last = d_constraints.back();
+ d_constraints.back() = d_consequent;
+ d_consequent = last;
+ PROOF( std::swap( d_farkas.front(), d_farkas.back() ) );
+ d_consequentSet = true;
+ }
+
+ Assert(! d_consequent->negationHasProof() );
+ Assert(d_consequentSet);
}
+/* Turns the vector under construction into a conflict */
+ConstraintCP FarkasConflictBuilder::commitConflict(){
+ Assert(underConstruction());
+ Assert(!d_constraints.empty());
+ Assert(!PROOF_ON() ||
+ (!underConstruction() && d_constraints.empty() && d_farkas.empty()) ||
+ (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
+ Assert(PROOF_ON() || d_farkas.empty());
+ Assert(d_consequentSet);
+
+ ConstraintP not_c = d_consequent->getNegation();
+ RationalVectorCP coeffs = NULLPROOF(&d_farkas);
+ not_c->impliedByFarkas(d_constraints, coeffs, true );
+
+ reset();
+ Assert(!underConstruction());
+ Assert( not_c->inConflict() );
+ Assert(!d_consequentSet);
+ return not_c;
+}
+
+RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
+ : d_ta(ta)
+{}
+
/* If you are not an equality engine, don't use this! */
-void RaiseConflict::blackBoxConflict(Node n){
- d_ta.blackBoxConflict(n);
+void RaiseEqualityEngineConflict::raiseEEConflict(Node n) const{
+ d_ta.raiseBlackBoxConflict(n);
}
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index f0e314bfb..ad88aea86 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -100,19 +100,80 @@ public:
class RaiseConflict {
private:
TheoryArithPrivate& d_ta;
- ConstraintCPVec& d_construction;
public:
- RaiseConflict(TheoryArithPrivate& ta, ConstraintCPVec& d_construction);
+ RaiseConflict(TheoryArithPrivate& ta);
+
+ /** Calls d_ta.raiseConflict(c) */
+ void raiseConflict(ConstraintCP c) const;
+};
+
+class FarkasConflictBuilder {
+private:
+ RationalVector d_farkas;
+ ConstraintCPVec d_constraints;
+ ConstraintCP d_consequent;
+ bool d_consequentSet;
+public:
+
+ /**
+ * Constructs a new FarkasConflictBuilder.
+ */
+ FarkasConflictBuilder();
+
+ /**
+ * Adds an antecedent constraint to the conflict under construction
+ * with the farkas coefficient fc * mult.
+ *
+ * The value mult is either 1 or -1.
+ */
+ void addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult);
+
+ /**
+ * Adds an antecedent constraint to the conflict under construction
+ * with the farkas coefficient fc.
+ */
+ void addConstraint(ConstraintCP c, const Rational& fc);
+
+ /**
+ * Makes the last constraint added the consequent.
+ * Can be done exactly once per reset().
+ */
+ void makeLastConsequent();
+
+ /**
+ * Turns the antecendents into a proof of the negation of one of the
+ * antecedents.
+ *
+ * The buffer is no longer underConstruction afterwards.
+ *
+ * precondition:
+ * - At least two constraints have been asserted.
+ * - makeLastConsequent() has been called.
+ *
+ * postcondition: The returned constraint is in conflict.
+ */
+ ConstraintCP commitConflict();
+
+ /** Returns true if a conflict has been pushed back since the last reset. */
+ bool underConstruction() const;
+
+ /** Returns true if the consequent has been set since the last reset. */
+ bool consequentIsSet() const;
+
+ /** Resets the state of the buffer. */
+ void reset();
+};
- /* Adds a constraint to the constraint under construction. */
- void addConstraint(ConstraintCP c);
- /* Turns the vector under construction into a conflict */
- void commitConflict();
- void sendConflict(const ConstraintCPVec& vec);
+class RaiseEqualityEngineConflict {
+private:
+ TheoryArithPrivate& d_ta;
+
+public:
+ RaiseEqualityEngineConflict(TheoryArithPrivate& ta);
/* If you are not an equality engine, don't use this! */
- void blackBoxConflict(Node n);
+ void raiseEEConflict(Node n) const;
};
class BoundCountingLookup {
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 99f6e0836..8a145ffc2 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -23,7 +23,7 @@ namespace CVC4 {
namespace theory {
namespace arith {
-ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, RaiseConflict raiseConflict)
+ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, RaiseEqualityEngineConflict raiseConflict)
: d_inConflict(c),
d_raiseConflict(raiseConflict),
d_notify(*this),
@@ -109,7 +109,7 @@ void ArithCongruenceManager::raiseConflict(Node conflict){
Assert(!inConflict());
Debug("arith::conflict") << "difference manager conflict " << conflict << std::endl;
d_inConflict.raise();
- d_raiseConflict.blackBoxConflict(conflict);
+ d_raiseConflict.raiseEEConflict(conflict);
}
bool ArithCongruenceManager::inConflict() const{
return d_inConflict.isRaised();
@@ -172,7 +172,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP
++(d_statistics.d_watchedVariableIsZero);
ArithVar s = lb->getVariable();
- Node reason = Constraint_::externalExplainByAssertions(lb,ub);
+ Node reason = Constraint::externalExplainByAssertions(lb,ub);
d_keepAlive.push_back(reason);
assertionToEqualityEngine(true, s, reason);
@@ -413,7 +413,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
<< ub << std::endl;
ArithVar x = lb->getVariable();
- Node reason = Constraint_::externalExplainByAssertions(lb,ub);
+ Node reason = Constraint::externalExplainByAssertions(lb,ub);
Node xAsNode = d_avariables.asNode(x);
Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart());
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index b0fa8f6f4..7ecfd21cf 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -41,7 +41,7 @@ namespace arith {
class ArithCongruenceManager {
private:
context::CDRaised d_inConflict;
- RaiseConflict d_raiseConflict;
+ RaiseEqualityEngineConflict d_raiseConflict;
/**
* The set of ArithVars equivalent to a pair of terms.
@@ -132,7 +132,7 @@ private:
public:
- ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseConflict raiseConflict);
+ ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict);
Node explain(TNode literal);
void explain(TNode lit, NodeBuilder<>& out);
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 5e3808fc7..94632e50e 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -20,6 +20,8 @@
#include "theory/arith/arith_utilities.h"
#include "theory/arith/normal_form.h"
+#include "proof/proof.h"
+
#include <ostream>
#include <algorithm>
@@ -64,7 +66,7 @@ ConstraintType constraintTypeOfComparison(const Comparison& cmp){
}
}
-Constraint_::Constraint_(ArithVar x, ConstraintType t, const DeltaRational& v)
+Constraint::Constraint(ArithVar x, ConstraintType t, const DeltaRational& v)
: d_variable(x),
d_type(t),
d_value(v),
@@ -74,7 +76,7 @@ Constraint_::Constraint_(ArithVar x, ConstraintType t, const DeltaRational& v)
d_canBePropagated(false),
d_assertionOrder(AssertionOrderSentinel),
d_witness(TNode::null()),
- d_proof(ProofIdSentinel),
+ d_crid(ConstraintRuleIdSentinel),
d_split(false),
d_variablePosition()
{
@@ -82,6 +84,28 @@ Constraint_::Constraint_(ArithVar x, ConstraintType t, const DeltaRational& v)
}
+std::ostream& operator<<(std::ostream& o, const ArithProofType apt){
+ switch(apt){
+ case NoAP: o << "NoAP"; break;
+ case AssumeAP: o << "AssumeAP"; break;
+ case InternalAssumeAP: o << "InternalAssumeAP"; break;
+ case FarkasAP: o << "FarkasAP"; break;
+ case TrichotomyAP: o << "TrichotomyAP"; break;
+ case EqualityEngineAP: o << "EqualityEngineAP"; break;
+ case IntHoleAP: o << "IntHoleAP"; break;
+ default: break;
+ }
+ return o;
+}
+
+std::ostream& operator<<(std::ostream& o, const ConstraintCP c){
+ if(c == NullConstraint){
+ return o << "NullConstraint";
+ }else{
+ return o << *c;
+ }
+}
+
std::ostream& operator<<(std::ostream& o, const ConstraintP c){
if(c == NullConstraint){
return o << "NullConstraint";
@@ -105,7 +129,7 @@ std::ostream& operator<<(std::ostream& o, const ConstraintType t){
}
}
-std::ostream& operator<<(std::ostream& o, const Constraint_& c){
+std::ostream& operator<<(std::ostream& o, const Constraint& c){
o << c.getVariable() << ' ' << c.getType() << ' ' << c.getValue();
if(c.hasLiteral()){
o << "(node " << c.getLiteral() << ')';
@@ -154,7 +178,7 @@ std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){
return o;
}
-void Constraint_::debugPrint() const {
+void Constraint::debugPrint() const {
Message() << *this << endl;
}
@@ -360,19 +384,25 @@ ConstraintP ValueCollection::nonNull() const{
}
}
-bool Constraint_::initialized() const {
+bool Constraint::initialized() const {
return d_database != NULL;
}
-void Constraint_::initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation){
+const ConstraintDatabase& Constraint::getDatabase() const{
+ Assert(initialized());
+ return *d_database;
+}
+
+void Constraint::initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation){
Assert(!initialized());
d_database = db;
d_variablePosition = v;
d_negation = negation;
}
-Constraint_::~Constraint_() {
- Assert(safeToGarbageCollect());
+Constraint::~Constraint() {
+ // Call this instead of safeToGarbageCollect()
+ Assert(!contextDependentDataIsSet());
if(initialized()){
ValueCollection& vc = d_variablePosition->second;
@@ -392,11 +422,17 @@ Constraint_::~Constraint_() {
}
}
-const ValueCollection& Constraint_::getValueCollection() const{
+const ConstraintRule& Constraint::getConstraintRule() const {
+ Assert(hasProof());
+ return d_database->d_watches->d_constraintProofs[d_crid];
+}
+
+const ValueCollection& Constraint::getValueCollection() const{
return d_variablePosition->second;
}
-ConstraintP Constraint_::getCeiling() {
+
+ConstraintP Constraint::getCeiling() {
Debug("getCeiling") << "Constraint_::getCeiling on " << *this << endl;
Assert(getValue().getInfinitesimalPart().sgn() > 0);
@@ -406,7 +442,7 @@ ConstraintP Constraint_::getCeiling() {
return d_database->getConstraint(getVariable(), getType(), ceiling);
}
-ConstraintP Constraint_::getFloor() {
+ConstraintP Constraint::getFloor() {
Assert(getValue().getInfinitesimalPart().sgn() < 0);
DeltaRational floor(Rational(getValue().floor()));
@@ -415,26 +451,27 @@ ConstraintP Constraint_::getFloor() {
return d_database->getConstraint(getVariable(), getType(), floor);
}
-void Constraint_::setCanBePropagated() {
+void Constraint::setCanBePropagated() {
Assert(!canBePropagated());
d_database->pushCanBePropagatedWatch(this);
}
-void Constraint_::setAssertedToTheTheoryWithNegationTrue(TNode witness) {
+void Constraint::setAssertedToTheTheory(TNode witness, bool nowInConflict) {
Assert(hasLiteral());
Assert(!assertedToTheTheory());
- Assert(d_negation->hasProof());
+ Assert(negationHasProof() == nowInConflict);
d_database->pushAssertionOrderWatch(this, witness);
-}
-void Constraint_::setAssertedToTheTheory(TNode witness) {
- Assert(hasLiteral());
- Assert(!assertedToTheTheory());
- Assert(!d_negation->assertedToTheTheory());
- d_database->pushAssertionOrderWatch(this, witness);
+ if(Debug.isOn("constraint::conflictCommit") && nowInConflict ){
+ Debug("constraint::conflictCommit") << "inConflict@setAssertedToTheTheory";
+ Debug("constraint::conflictCommit") << "\t" << this << std::endl;
+ Debug("constraint::conflictCommit") << "\t" << getNegation() << std::endl;
+ Debug("constraint::conflictCommit") << "\t" << getNegation()->externalExplainByAssertions() << std::endl;
+
+ }
}
-bool Constraint_::satisfiedBy(const DeltaRational& dr) const {
+bool Constraint::satisfiedBy(const DeltaRational& dr) const {
switch(getType()){
case LowerBound:
return getValue() <= dr;
@@ -448,19 +485,31 @@ bool Constraint_::satisfiedBy(const DeltaRational& dr) const {
Unreachable();
}
-bool Constraint_::isInternalDecision() const {
- return d_proof == d_database->d_internalDecisionProof;
+bool Constraint::isInternalAssumption() const {
+ return getProofType() == InternalAssumeAP;
+}
+
+bool Constraint::isAssumption() const {
+ return getProofType() == AssumeAP;
+}
+
+bool Constraint::hasEqualityEngineProof() const {
+ return getProofType() == EqualityEngineAP;
}
-bool Constraint_::isSelfExplaining() const {
- return d_proof == d_database->d_selfExplainingProof;
+bool Constraint::hasFarkasProof() const {
+ return getProofType() == FarkasAP;
}
-bool Constraint_::hasEqualityEngineProof() const {
- return d_proof == d_database->d_equalityEngineProof;
+bool Constraint::hasIntHoleProof() const {
+ return getProofType() == IntHoleAP;
}
-bool Constraint_::sanityChecking(Node n) const {
+bool Constraint::hasTrichotomyProof() const {
+ return getProofType() == TrichotomyAP;
+}
+
+bool Constraint::sanityChecking(Node n) const {
Comparison cmp = Comparison::parseNormalForm(n);
Kind k = cmp.comparisonKind();
Polynomial pleft = cmp.normalizedVariablePart();
@@ -473,15 +522,15 @@ bool Constraint_::sanityChecking(Node n) const {
const ArithVariables& avariables = d_database->getArithVariables();
- Debug("nf::tmp") << cmp.getNode() << endl;
- Debug("nf::tmp") << k << endl;
- Debug("nf::tmp") << pleft.getNode() << endl;
- Debug("nf::tmp") << left << endl;
- Debug("nf::tmp") << right << endl;
- Debug("nf::tmp") << getValue() << endl;
- Debug("nf::tmp") << avariables.hasArithVar(left) << endl;
- Debug("nf::tmp") << avariables.asArithVar(left) << endl;
- Debug("nf::tmp") << getVariable() << endl;
+ Debug("Constraint::sanityChecking") << cmp.getNode() << endl;
+ Debug("Constraint::sanityChecking") << k << endl;
+ Debug("Constraint::sanityChecking") << pleft.getNode() << endl;
+ Debug("Constraint::sanityChecking") << left << endl;
+ Debug("Constraint::sanityChecking") << right << endl;
+ Debug("Constraint::sanityChecking") << getValue() << endl;
+ Debug("Constraint::sanityChecking") << avariables.hasArithVar(left) << endl;
+ Debug("Constraint::sanityChecking") << avariables.asArithVar(left) << endl;
+ Debug("Constraint::sanityChecking") << getVariable() << endl;
if(avariables.hasArithVar(left) &&
@@ -504,7 +553,176 @@ bool Constraint_::sanityChecking(Node n) const {
}
}
-ConstraintP Constraint_::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){
+void ConstraintRule::debugPrint() const {
+ print(std::cerr);
+}
+
+ConstraintCP ConstraintDatabase::getAntecedent (AntecedentId p) const {
+ Assert(p < d_antecedents.size());
+ return d_antecedents[p];
+}
+
+
+void ConstraintRule::print(std::ostream& out) const {
+
+ RationalVectorCP coeffs = NULLPROOF(d_farkasCoefficients);
+ out << "{ConstraintRule, ";
+ out << d_constraint << std::endl;
+ out << "d_proofType= " << d_proofType << ", " << std::endl;
+ out << "d_antecedentEnd= "<< d_antecedentEnd << std::endl;
+
+ if(d_constraint != NullConstraint){
+ const ConstraintDatabase& database = d_constraint->getDatabase();
+
+ size_t coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffs->size()-1 : 0;
+ AntecedentId p = d_antecedentEnd;
+ // must have at least one antecedent
+ ConstraintCP antecedent = database.getAntecedent(p);
+ while(antecedent != NullConstraint){
+ if(coeffs != RationalVectorCPSentinel){
+ out << coeffs->at(coeffIterator);
+ } else {
+ out << "_";
+ }
+ out << " * (" << *antecedent << ")" << std::endl;
+
+ Assert((coeffs == RationalVectorCPSentinel) || coeffIterator > 0);
+ --p;
+ coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffIterator-1 : 0;
+ antecedent = database.getAntecedent(p);
+ }
+ if(coeffs != RationalVectorCPSentinel){
+ out << coeffs->front();
+ } else {
+ out << "_";
+ }
+ out << " * (" << *(d_constraint->getNegation()) << ")";
+ out << " [not d_constraint] " << endl;
+ }
+ out << "}";
+}
+
+bool Constraint::wellFormedFarkasProof() const {
+ Assert(hasProof());
+
+ const ConstraintRule& cr = getConstraintRule();
+ if(cr.d_constraint != this){ return false; }
+ if(cr.d_proofType != FarkasAP){ return false; }
+
+ AntecedentId p = cr.d_antecedentEnd;
+
+ // must have at least one antecedent
+ ConstraintCP antecedent = d_database->d_antecedents[p];
+ if(antecedent == NullConstraint) { return false; }
+
+#ifdef CVC4_PROOF
+ if(!PROOF_ON()){ return cr.d_farkasCoefficients == RationalVectorCPSentinel; }
+ Assert(PROOF_ON());
+
+ if(cr.d_farkasCoefficients == RationalVectorCPSentinel){ return false; }
+ if(cr.d_farkasCoefficients->size() < 2){ return false; }
+
+ const ArithVariables& vars = d_database->getArithVariables();
+
+ DeltaRational rhs(0);
+ Node lhs = Polynomial::mkZero().getNode();
+
+ RationalVector::const_iterator coeffIterator = cr.d_farkasCoefficients->end()-1;
+ RationalVector::const_iterator coeffBegin = cr.d_farkasCoefficients->begin();
+
+ while(antecedent != NullConstraint){
+ Assert(lhs.isNull() || Polynomial::isMember(lhs));
+
+ const Rational& coeff = *coeffIterator;
+ int coeffSgn = coeff.sgn();
+
+ rhs += antecedent->getValue() * coeff;
+
+ ArithVar antVar = antecedent->getVariable();
+ if(!lhs.isNull() && vars.hasNode(antVar)){
+ Node antAsNode = vars.asNode(antVar);
+ if(Polynomial::isMember(antAsNode)){
+ Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
+ Polynomial antPoly = Polynomial::parsePolynomial(antAsNode);
+ Polynomial sum = lhsPoly + (antPoly * coeff);
+ lhs = sum.getNode();
+ }else{
+ lhs = Node::null();
+ }
+ } else {
+ lhs = Node::null();
+ }
+ Debug("constraints::wffp") << "running sum: " << lhs << " <= " << rhs << endl;
+
+ switch( antecedent->getType() ){
+ case LowerBound:
+ // fc[l] < 0, therefore return false if coeffSgn >= 0
+ if(coeffSgn >= 0){ return false; }
+ break;
+ case UpperBound:
+ // fc[u] > 0, therefore return false if coeffSgn <= 0
+ if(coeffSgn <= 0){ return false; }
+ break;
+ case Equality:
+ if(coeffSgn == 0) { return false; }
+ break;
+ case Disequality:
+ default:
+ return false;
+ }
+
+ if(coeffIterator == coeffBegin){ return false; }
+ --coeffIterator;
+ --p;
+ antecedent = d_database->d_antecedents[p];
+ }
+ if(coeffIterator != coeffBegin){ return false; }
+
+ const Rational& firstCoeff = (*coeffBegin);
+ int firstCoeffSgn = firstCoeff.sgn();
+ rhs += (getNegation()->getValue()) * firstCoeff;
+ if(!lhs.isNull() && vars.hasNode(getVariable())){
+ Node firstAsNode = vars.asNode(getVariable());
+ if(Polynomial::isMember(firstAsNode)){
+ Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
+ Polynomial firstPoly = Polynomial::parsePolynomial(firstAsNode);
+ Polynomial sum = lhsPoly + (firstPoly * firstCoeff);
+ lhs = sum.getNode();
+ }else{
+ lhs = Node::null();
+ }
+ }else{
+ lhs = Node::null();
+ }
+
+ switch( getNegation()->getType() ){
+ case LowerBound:
+ // fc[l] < 0, therefore return false if coeffSgn >= 0
+ if(firstCoeffSgn >= 0){ return false; }
+ break;
+ case UpperBound:
+ // fc[u] > 0, therefore return false if coeffSgn <= 0
+ if(firstCoeffSgn <= 0){ return false; }
+ break;
+ case Equality:
+ if(firstCoeffSgn == 0) { return false; }
+ break;
+ case Disequality:
+ default:
+ return false;
+ }
+ Debug("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl;
+ // 0 = lhs <= rhs < 0
+ return
+ (lhs.isNull() || Constant::isMember(lhs) && Constant(lhs).isZero() ) &&
+ rhs.sgn() < 0;
+
+#else
+ return true;
+#endif
+}
+
+ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){
switch(t){
case LowerBound:
{
@@ -513,12 +731,12 @@ ConstraintP Constraint_::makeNegation(ArithVar v, ConstraintType t, const DeltaR
Assert(r.getInfinitesimalPart() == 1);
// make (not (v > r)), which is (v <= r)
DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
- return new Constraint_(v, UpperBound, dropInf);
+ return new Constraint(v, UpperBound, dropInf);
}else{
Assert(r.infinitesimalSgn() == 0);
// make (not (v >= r)), which is (v < r)
DeltaRational addInf(r.getNoninfinitesimalPart(), -1);
- return new Constraint_(v, UpperBound, addInf);
+ return new Constraint(v, UpperBound, addInf);
}
}
case UpperBound:
@@ -528,18 +746,18 @@ ConstraintP Constraint_::makeNegation(ArithVar v, ConstraintType t, const DeltaR
Assert(r.getInfinitesimalPart() == -1);
// make (not (v < r)), which is (v >= r)
DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
- return new Constraint_(v, LowerBound, dropInf);
+ return new Constraint(v, LowerBound, dropInf);
}else{
Assert(r.infinitesimalSgn() == 0);
// make (not (v <= r)), which is (v > r)
DeltaRational addInf(r.getNoninfinitesimalPart(), 1);
- return new Constraint_(v, LowerBound, addInf);
+ return new Constraint(v, LowerBound, addInf);
}
}
case Equality:
- return new Constraint_(v, Disequality, r);
+ return new Constraint(v, Disequality, r);
case Disequality:
- return new Constraint_(v, Equality, r);
+ return new Constraint(v, Equality, r);
default:
Unreachable();
return NullConstraint;
@@ -547,24 +765,18 @@ ConstraintP Constraint_::makeNegation(ArithVar v, ConstraintType t, const DeltaR
}
ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVariables& avars, ArithCongruenceManager& cm, RaiseConflict raiseConflict)
- : d_varDatabases(),
- d_toPropagate(satContext),
- d_proofs(satContext, false),
- d_watches(new Watches(satContext, userContext)),
- d_avariables(avars),
- d_congruenceManager(cm),
- d_satContext(satContext),
- d_satAllocationLevel(d_satContext->getLevel()),
- d_raiseConflict(raiseConflict)
+ : d_varDatabases()
+ , d_toPropagate(satContext)
+ , d_antecedents(satContext, false)
+ , d_watches(new Watches(satContext, userContext))
+ , d_avariables(avars)
+ , d_congruenceManager(cm)
+ , d_satContext(satContext)
+ , d_raiseConflict(raiseConflict)
+ , d_one(1)
+ , d_negOne(-1)
{
- d_selfExplainingProof = d_proofs.size();
- d_proofs.push_back(NullConstraint);
-
- d_equalityEngineProof = d_proofs.size();
- d_proofs.push_back(NullConstraint);
-
- d_internalDecisionProof = d_proofs.size();
- d_proofs.push_back(NullConstraint);
+
}
SortedConstraintMap& ConstraintDatabase::getVariableSCM(ArithVar v) const{
@@ -592,10 +804,13 @@ void ConstraintDatabase::pushAssertionOrderWatch(ConstraintP c, TNode witness){
d_watches->d_assertionOrderWatches.push_back(c);
}
-void ConstraintDatabase::pushProofWatch(ConstraintP c, ProofId pid){
- Assert(c->d_proof == ProofIdSentinel);
- c->d_proof = pid;
- d_watches->d_proofWatches.push_back(c);
+
+void ConstraintDatabase::pushConstraintRule(const ConstraintRule& crp){
+ ConstraintP c = crp.d_constraint;
+ Assert(c->d_crid == ConstraintRuleIdSentinel);
+ Assert(!c->hasProof());
+ c->d_crid = d_watches->d_constraintProofs.size();
+ d_watches->d_constraintProofs.push_back(crp);
}
ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){
@@ -610,8 +825,8 @@ ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, cons
if(vc.hasConstraintOfType(t)){
return vc.getConstraintOfType(t);
}else{
- ConstraintP c = new Constraint_(v, t, r);
- ConstraintP negC = Constraint_::makeNegation(v, t, r);
+ ConstraintP c = new Constraint(v, t, r);
+ ConstraintP negC = Constraint::makeNegation(v, t, r);
SortedConstraintMapIterator negPos;
if(t == Equality || t == Disequality){
@@ -649,8 +864,6 @@ bool ConstraintDatabase::emptyDatabase(const std::vector<PerVariableDatabase>& v
}
ConstraintDatabase::~ConstraintDatabase(){
- Assert(d_satAllocationLevel <= d_satContext->getLevel());
-
delete d_watches;
std::vector<ConstraintP> constraintList;
@@ -727,14 +940,17 @@ void ConstraintDatabase::removeVariable(ArithVar v){
d_reclaimable.add(v);
}
-bool Constraint_::safeToGarbageCollect() const{
- return !isSplit()
- && !canBePropagated()
- && !hasProof()
- && !assertedToTheTheory();
+bool Constraint::safeToGarbageCollect() const{
+ // Do not call during destructor as getNegation() may be Null by this point
+ Assert(getNegation() != NullConstraint);
+ return !contextDependentDataIsSet() && ! getNegation()->contextDependentDataIsSet();
}
-Node Constraint_::split(){
+bool Constraint::contextDependentDataIsSet() const{
+ return hasProof() || isSplit() || canBePropagated() || assertedToTheTheory();
+}
+
+Node Constraint::split(){
Assert(isEquality() || isDisequality());
bool isEq = isEquality();
@@ -763,25 +979,6 @@ bool ConstraintDatabase::hasLiteral(TNode literal) const {
return lookup(literal) != NullConstraint;
}
-// ConstraintP ConstraintDatabase::addLiteral(TNode literal){
-// Assert(!hasLiteral(literal));
-// bool isNot = (literal.getKind() == NOT);
-// TNode atom = isNot ? literal[0] : literal;
-
-// ConstraintP atomC = addAtom(atom);
-
-// return isNot ? atomC->d_negation : atomC;
-// }
-
-// ConstraintP ConstraintDatabase::allocateConstraintForComparison(ArithVar v, const Comparison cmp){
-// Debug("arith::constraint") << "allocateConstraintForLiteral(" << v << ", "<< cmp <<")" << endl;
-// Kind kind = cmp.comparisonKind();
-// ConstraintType type = constraintTypeOfLiteral(kind);
-
-// DeltaRational dr = cmp.getDeltaRational();
-// return new Constraint_(v, type, dr);
-// }
-
ConstraintP ConstraintDatabase::addLiteral(TNode literal){
Assert(!hasLiteral(literal));
bool isNot = (literal.getKind() == NOT);
@@ -795,12 +992,11 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
ConstraintType posType = constraintTypeOfComparison(posCmp);
Polynomial nvp = posCmp.normalizedVariablePart();
- Debug("nf::tmp") << "here " << nvp.getNode() << " " << endl;
ArithVar v = d_avariables.asArithVar(nvp.getNode());
DeltaRational posDR = posCmp.normalizedDeltaRational();
- ConstraintP posC = new Constraint_(v, posType, posDR);
+ ConstraintP posC = new Constraint(v, posType, posDR);
Debug("arith::constraint") << "addliteral( literal ->" << literal << ")" << endl;
Debug("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl;
@@ -831,7 +1027,7 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
ConstraintType negType = constraintTypeOfComparison(negCmp);
DeltaRational negDR = negCmp.normalizedDeltaRational();
- ConstraintP negC = new Constraint_(v, negType, negDR);
+ ConstraintP negC = new Constraint(v, negType, negDR);
SortedConstraintMapIterator negI;
@@ -866,22 +1062,6 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
}
}
-// ConstraintType constraintTypeOfLiteral(Kind k){
-// switch(k){
-// case LT:
-// case LEQ:
-// return UpperBound;
-// case GT:
-// case GEQ:
-// return LowerBound;
-// case EQUAL:
-// return Equality;
-// case DISTINCT:
-// return Disequality;
-// default:
-// Unreachable();
-// }
-// }
ConstraintP ConstraintDatabase::lookup(TNode literal) const{
NodetoConstraintMap::const_iterator iter = d_nodetoConstraintMap.find(literal);
@@ -892,151 +1072,236 @@ ConstraintP ConstraintDatabase::lookup(TNode literal) const{
}
}
-void Constraint_::selfExplainingWithNegationTrue(){
+void Constraint::setAssumption(bool nowInConflict){
Assert(!hasProof());
- Assert(getNegation()->hasProof());
+ Assert(negationHasProof() == nowInConflict);
Assert(hasLiteral());
Assert(assertedToTheTheory());
- d_database->pushProofWatch(this, d_database->d_selfExplainingProof);
+
+ d_database->pushConstraintRule(ConstraintRule(this, AssumeAP));
+
+ Assert(inConflict() == nowInConflict);
+ if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+ Debug("constraint::conflictCommit") << "inConflict@setAssumption " << this << std::endl;
+ }
}
-void Constraint_::selfExplaining(){
- markAsTrue();
+void Constraint::tryToPropagate(){
+ Assert(hasProof());
+ Assert(!isAssumption());
+ Assert(!isInternalAssumption());
+
+ if(canBePropagated() && !assertedToTheTheory() && !isAssumption() && !isInternalAssumption()){
+ propagate();
+ }
}
-void Constraint_::propagate(){
+void Constraint::propagate(){
Assert(hasProof());
Assert(canBePropagated());
Assert(!assertedToTheTheory());
- Assert(!isSelfExplaining());
+ Assert(!isAssumption());
+ Assert(!isInternalAssumption());
d_database->d_toPropagate.push(this);
}
-void Constraint_::propagate(ConstraintCP a){
- Assert(!hasProof());
- Assert(canBePropagated());
-
- markAsTrue(a);
- propagate();
-}
-void Constraint_::propagate(ConstraintCP a, ConstraintCP b){
+/*
+ * Example:
+ * x <= a and a < b
+ * |= x <= b
+ * ---
+ * 1*(x <= a) + (-1)*(x > b) => (0 <= a-b)
+ */
+void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
Assert(!hasProof());
- Assert(canBePropagated());
+ Assert(imp->hasProof());
+ Assert(negationHasProof() == nowInConflict);
- markAsTrue(a, b);
- propagate();
-}
-void Constraint_::propagate(const ConstraintCPVec& b){
- Assert(!hasProof());
- Assert(canBePropagated());
+ d_database->d_antecedents.push_back(NullConstraint);
+ d_database->d_antecedents.push_back(imp);
- markAsTrue(b);
- propagate();
-}
+ AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
-void Constraint_::impliedBy(ConstraintCP a){
- Assert(truthIsUnknown());
+ RationalVectorP coeffs;
+ if(PROOF_ON()){
+ std::pair<int, int> sgns = unateFarkasSigns(getNegation(), imp);
- markAsTrue(a);
- if(canBePropagated()){
- propagate();
+ Rational first(sgns.first);
+ Rational second(sgns.second);
+
+ coeffs = new RationalVector();
+ coeffs->push_back(first);
+ coeffs->push_back(second);
+ } else {
+ coeffs = RationalVectorPSentinel;
}
-}
-void Constraint_::impliedBy(ConstraintCP a, ConstraintCP b){
- Assert(truthIsUnknown());
+ // no need to delete coeffs the memory is owned by ConstraintRule
+ d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffs));
- markAsTrue(a, b);
- if(canBePropagated()){
- propagate();
+ Assert(inConflict() == nowInConflict);
+ if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+ Debug("constraint::conflictCommit") << "inConflict@impliedByUnate " << this << std::endl;
+ }
+
+ if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
+ getConstraintRule().print(Debug("constraints::wffp"));
}
+ Assert(wellFormedFarkasProof());
}
-void Constraint_::impliedBy(const ConstraintCPVec& b){
- Assert(truthIsUnknown());
+void Constraint::impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool nowInConflict){
+ Assert(!hasProof());
+ Assert(negationHasProof() == nowInConflict);
+ Assert(a->hasProof());
+ Assert(b->hasProof());
- markAsTrue(b);
- if(canBePropagated()){
- propagate();
- }
-}
+ d_database->d_antecedents.push_back(NullConstraint);
+ d_database->d_antecedents.push_back(a);
+ d_database->d_antecedents.push_back(b);
-void Constraint_::setInternalDecision(){
- Assert(truthIsUnknown());
- Assert(!assertedToTheTheory());
+ AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
+ d_database->pushConstraintRule(ConstraintRule(this, TrichotomyAP, antecedentEnd));
- d_database->pushProofWatch(this, d_database->d_internalDecisionProof);
+ Assert(inConflict() == nowInConflict);
+ if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+ Debug("constraint::conflictCommit") << "inConflict@impliedByTrichotomy " << this << std::endl;
+ }
}
-void Constraint_::setEqualityEngineProof(){
- Assert(truthIsUnknown());
- Assert(hasLiteral());
- d_database->pushProofWatch(this, d_database->d_equalityEngineProof);
-}
-void Constraint_::markAsTrue(){
- Assert(truthIsUnknown());
- Assert(hasLiteral());
- Assert(assertedToTheTheory());
- d_database->pushProofWatch(this, d_database->d_selfExplainingProof);
+bool Constraint::allHaveProof(const ConstraintCPVec& b){
+ for(ConstraintCPVec::const_iterator i=b.begin(), i_end=b.end(); i != i_end; ++i){
+ ConstraintCP cp = *i;
+ if(! (cp->hasProof())){ return false; }
+ }
+ return true;
}
-void Constraint_::markAsTrue(ConstraintCP imp){
- Assert(truthIsUnknown());
- Assert(imp->hasProof());
+void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){
+ Assert(!hasProof());
+ Assert(negationHasProof() == nowInConflict);
+ Assert(a->hasProof());
+
+ d_database->d_antecedents.push_back(NullConstraint);
+ d_database->d_antecedents.push_back(a);
+ AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
+ d_database->pushConstraintRule(ConstraintRule(this, IntHoleAP, antecedentEnd));
- d_database->d_proofs.push_back(NullConstraint);
- d_database->d_proofs.push_back(imp);
- ProofId proof = d_database->d_proofs.size() - 1;
- d_database->pushProofWatch(this, proof);
+ Assert(inConflict() == nowInConflict);
+ if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+ Debug("constraint::conflictCommit") << "inConflict impliedByIntHole" << this << std::endl;
+ }
}
-void Constraint_::markAsTrue(ConstraintCP impA, ConstraintCP impB){
- Assert(truthIsUnknown());
- Assert(impA->hasProof());
- Assert(impB->hasProof());
+void Constraint::impliedByIntHole(const ConstraintCPVec& b, bool nowInConflict){
+ Assert(!hasProof());
+ Assert(negationHasProof() == nowInConflict);
+ Assert(allHaveProof(b));
+
+ CDConstraintList& antecedents = d_database->d_antecedents;
+ antecedents.push_back(NullConstraint);
+ for(ConstraintCPVec::const_iterator i=b.begin(), i_end=b.end(); i != i_end; ++i){
+ antecedents.push_back(*i);
+ }
+ AntecedentId antecedentEnd = antecedents.size() - 1;
- d_database->d_proofs.push_back(NullConstraint);
- d_database->d_proofs.push_back(impA);
- d_database->d_proofs.push_back(impB);
- ProofId proof = d_database->d_proofs.size() - 1;
+ d_database->pushConstraintRule(ConstraintRule(this, IntHoleAP, antecedentEnd));
- d_database->pushProofWatch(this, proof);
+ Assert(inConflict() == nowInConflict);
+ if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+ Debug("constraint::conflictCommit") << "inConflict@impliedByIntHole[vec] " << this << std::endl;
+ }
}
-void Constraint_::markAsTrue(const ConstraintCPVec& a){
- Assert(truthIsUnknown());
+/*
+ * If proofs are off, coeffs == RationalVectorSentinal.
+ * If proofs are on,
+ * coeffs != RationalVectorSentinal,
+ * coeffs->size() = a.size() + 1,
+ * for i in [0,a.size) : coeff[i] corresponds to a[i], and
+ * coeff.back() corresponds to the current constraint.
+ */
+void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coeffs, bool nowInConflict){
+ Assert(!hasProof());
+ Assert(negationHasProof() == nowInConflict);
+ Assert(allHaveProof(a));
+
+ Assert( PROOF_ON() == (coeffs != RationalVectorCPSentinel) );
+ // !PROOF_ON() => coeffs == RationalVectorCPSentinel
+ // PROOF_ON() => coeffs->size() == a.size() + 1
+ Assert(!PROOF_ON() || coeffs->size() == a.size() + 1);
Assert(a.size() >= 1);
- d_database->d_proofs.push_back(NullConstraint);
+
+ d_database->d_antecedents.push_back(NullConstraint);
for(ConstraintCPVec::const_iterator i = a.begin(), end = a.end(); i != end; ++i){
ConstraintCP c_i = *i;
Assert(c_i->hasProof());
- //Assert(!c_i->isPseudoConstraint());
- d_database->d_proofs.push_back(c_i);
+ d_database->d_antecedents.push_back(c_i);
+ }
+ AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
+
+ RationalVectorCP coeffsCopy;
+ if(PROOF_ON()){
+ Assert(coeffs != RationalVectorCPSentinel);
+ coeffsCopy = new RationalVector(*coeffs);
+ } else {
+ coeffsCopy = RationalVectorCPSentinel;
+ }
+ d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffsCopy));
+
+ Assert(inConflict() == nowInConflict);
+ if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+ Debug("constraint::conflictCommit") << "inConflict@impliedByFarkas " << this << std::endl;
+ }
+ if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
+ getConstraintRule().print(Debug("constraints::wffp"));
+ }
+ Assert(wellFormedFarkasProof());
+}
+
+
+void Constraint::setInternalAssumption(bool nowInConflict){
+ Assert(!hasProof());
+ Assert(negationHasProof() == nowInConflict);
+ Assert(!assertedToTheTheory());
+
+ d_database->pushConstraintRule(ConstraintRule(this, InternalAssumeAP));
+
+ Assert(inConflict() == nowInConflict);
+ if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+ Debug("constraint::conflictCommit") << "inConflict@setInternalAssumption " << this << std::endl;
}
+}
- ProofId proof = d_database->d_proofs.size() - 1;
- d_database->pushProofWatch(this, proof);
+void Constraint::setEqualityEngineProof(){
+ Assert(truthIsUnknown());
+ Assert(hasLiteral());
+ d_database->pushConstraintRule(ConstraintRule(this, EqualityEngineAP));
}
-SortedConstraintMap& Constraint_::constraintSet() const{
+
+SortedConstraintMap& Constraint::constraintSet() const{
Assert(d_database->variableDatabaseIsSetup(d_variable));
return (d_database->d_varDatabases[d_variable])->d_constraints;
}
-bool Constraint_::proofIsEmpty() const{
+bool Constraint::antecentListIsEmpty() const{
Assert(hasProof());
- bool result = d_database->d_proofs[d_proof] == NullConstraint;
- //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPseudoConstraint());
- Assert((!result) || isSelfExplaining() || hasEqualityEngineProof());
- return result;
+ return d_database->d_antecedents[getEndAntecedent()] == NullConstraint;
}
-Node Constraint_::externalImplication(const ConstraintCPVec& b) const{
+bool Constraint::antecedentListLengthIsOne() const {
+ Assert(hasProof());
+ return !antecentListIsEmpty() &&
+ d_database->d_antecedents[getEndAntecedent()-1] == NullConstraint;
+}
+
+Node Constraint::externalImplication(const ConstraintCPVec& b) const{
Assert(hasLiteral());
Node antecedent = externalExplainByAssertions(b);
Node implied = getLiteral();
@@ -1044,10 +1309,19 @@ Node Constraint_::externalImplication(const ConstraintCPVec& b) const{
}
-Node Constraint_::externalExplainByAssertions(const ConstraintCPVec& b){
+Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){
return externalExplain(b, AssertionOrderSentinel);
}
+Node Constraint::externalExplainConflict() const{
+ Assert(inConflict());
+ NodeBuilder<> nb(kind::AND);
+ externalExplainByAssertions(nb);
+ getNegation()->externalExplainByAssertions(nb);
+
+ return safeConstructNary(nb);
+}
+
struct ConstraintCPHash {
/* Todo replace with an id */
size_t operator()(ConstraintCP c) const{
@@ -1056,13 +1330,13 @@ struct ConstraintCPHash {
}
};
-void Constraint_::assertionFringe(ConstraintCPVec& v){
+void Constraint::assertionFringe(ConstraintCPVec& v){
hash_set<ConstraintCP, ConstraintCPHash> visited;
size_t writePos = 0;
if(!v.empty()){
const ConstraintDatabase* db = v.back()->d_database;
- const CDConstraintList& proofs = db->d_proofs;
+ const CDConstraintList& antecedents = db->d_antecedents;
for(size_t i = 0; i < v.size(); ++i){
ConstraintCP vi = v[i];
if(visited.find(vi) == visited.end()){
@@ -1072,13 +1346,14 @@ void Constraint_::assertionFringe(ConstraintCPVec& v){
v[writePos] = vi;
writePos++;
}else{
- Assert(!vi->isSelfExplaining());
- ProofId p = vi->d_proof;
- ConstraintCP antecedent = proofs[p];
+ Assert(vi->hasFarkasProof() || vi->hasIntHoleProof() );
+ AntecedentId p = vi->getEndAntecedent();
+
+ ConstraintCP antecedent = antecedents[p];
while(antecedent != NullConstraint){
v.push_back(antecedent);
--p;
- antecedent = proofs[p];
+ antecedent = antecedents[p];
}
}
}
@@ -1087,12 +1362,12 @@ void Constraint_::assertionFringe(ConstraintCPVec& v){
}
}
-void Constraint_::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){
+void Constraint::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){
o.insert(o.end(), i.begin(), i.end());
assertionFringe(o);
}
-Node Constraint_::externalExplain(const ConstraintCPVec& v, AssertionOrder order){
+Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order){
NodeBuilder<> nb(kind::AND);
ConstraintCPVec::const_iterator i, end;
for(i = v.begin(), end = v.end(); i != end; ++i){
@@ -1102,65 +1377,70 @@ Node Constraint_::externalExplain(const ConstraintCPVec& v, AssertionOrder order
return safeConstructNary(nb);
}
-void Constraint_::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{
+void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{
Assert(hasProof());
- Assert(!isSelfExplaining() || assertedToTheTheory());
- Assert(!isInternalDecision());
+ Assert(!isAssumption() || assertedToTheTheory());
+ Assert(!isInternalAssumption());
if(assertedBefore(order)){
nb << getWitness();
}else if(hasEqualityEngineProof()){
d_database->eeExplain(this, nb);
}else{
- Assert(!isSelfExplaining());
- ProofId p = d_proof;
- ConstraintCP antecedent = d_database->d_proofs[p];
+ Assert(!isAssumption());
+ AntecedentId p = getEndAntecedent();
+ ConstraintCP antecedent = d_database->d_antecedents[p];
- for(; antecedent != NullConstraint; antecedent = d_database->d_proofs[--p] ){
+ while(antecedent != NullConstraint){
antecedent->externalExplain(nb, order);
+ --p;
+ antecedent = d_database->d_antecedents[p];
}
}
}
-Node Constraint_::externalExplain(AssertionOrder order) const{
+Node Constraint::externalExplain(AssertionOrder order) const{
Assert(hasProof());
- Assert(!isSelfExplaining() || assertedBefore(order));
- Assert(!isInternalDecision());
+ Assert(!isAssumption() || assertedBefore(order));
+ Assert(!isInternalAssumption());
if(assertedBefore(order)){
return getWitness();
}else if(hasEqualityEngineProof()){
return d_database->eeExplain(this);
}else{
- Assert(!proofIsEmpty());
+ Assert(hasFarkasProof() || hasIntHoleProof() || hasTrichotomyProof());
+ Assert(!antecentListIsEmpty());
//Force the selection of the layer above if the node is
// assertedToTheTheory()!
- if(d_database->d_proofs[d_proof-1] == NullConstraint){
- ConstraintCP antecedent = d_database->d_proofs[d_proof];
+
+ AntecedentId listEnd = getEndAntecedent();
+ if(antecedentListLengthIsOne()){
+ ConstraintCP antecedent = d_database->d_antecedents[listEnd];
return antecedent->externalExplain(order);
}else{
NodeBuilder<> nb(kind::AND);
- Assert(!isSelfExplaining());
+ Assert(!isAssumption());
- ProofId p = d_proof;
- ConstraintCP antecedent = d_database->d_proofs[p];
+ AntecedentId p = listEnd;
+ ConstraintCP antecedent = d_database->d_antecedents[p];
while(antecedent != NullConstraint){
antecedent->externalExplain(nb, order);
--p;
- antecedent = d_database->d_proofs[p];
+ antecedent = d_database->d_antecedents[p];
}
return nb;
}
}
}
-Node Constraint_::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){
+Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){
NodeBuilder<> nb(kind::AND);
a->externalExplainByAssertions(nb);
b->externalExplainByAssertions(nb);
return nb;
}
-Node Constraint_::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c){
+Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c){
NodeBuilder<> nb(kind::AND);
a->externalExplainByAssertions(nb);
b->externalExplainByAssertions(nb);
@@ -1168,7 +1448,7 @@ Node Constraint_::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, Co
return nb;
}
-ConstraintP Constraint_::getStrictlyWeakerLowerBound(bool hasLiteral, bool asserted) const {
+ConstraintP Constraint::getStrictlyWeakerLowerBound(bool hasLiteral, bool asserted) const {
Assert(initialized());
Assert(!asserted || hasLiteral);
@@ -1193,7 +1473,7 @@ ConstraintP Constraint_::getStrictlyWeakerLowerBound(bool hasLiteral, bool asser
return NullConstraint;
}
-ConstraintP Constraint_::getStrictlyWeakerUpperBound(bool hasLiteral, bool asserted) const {
+ConstraintP Constraint::getStrictlyWeakerUpperBound(bool hasLiteral, bool asserted) const {
SortedConstraintMapConstIterator i = d_variablePosition;
const SortedConstraintMap& scm = constraintSet();
SortedConstraintMapConstIterator i_end = scm.end();
@@ -1273,12 +1553,12 @@ ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t
}
}
}
-Node ConstraintDatabase::eeExplain(const Constraint_* const c) const{
+Node ConstraintDatabase::eeExplain(const Constraint* const c) const{
Assert(c->hasLiteral());
return d_congruenceManager.explain(c->getLiteral());
}
-void ConstraintDatabase::eeExplain(const Constraint_* const c, NodeBuilder<>& nb) const{
+void ConstraintDatabase::eeExplain(const Constraint* const c, NodeBuilder<>& nb) const{
Assert(c->hasLiteral());
d_congruenceManager.explain(c->getLiteral(), nb);
}
@@ -1289,14 +1569,14 @@ bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const {
ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Context* userContext):
- d_proofWatches(satContext),
+ d_constraintProofs(satContext),
d_canBePropagatedWatches(satContext),
d_assertionOrderWatches(satContext),
d_splitWatches(userContext)
{}
-void Constraint_::setLiteral(Node n) {
+void Constraint::setLiteral(Node n) {
Assert(!hasLiteral());
Assert(sanityChecking(n));
d_literal = n;
@@ -1414,17 +1694,21 @@ void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& lemmas)
}
}
-void ConstraintDatabase::raiseUnateConflict(ConstraintP ant, ConstraintP cons){
- Assert(ant->hasProof());
- ConstraintP negCons = cons->getNegation();
- Assert(negCons->hasProof());
-
- Debug("arith::unate::conf") << ant << "implies " << cons << endl;
- Debug("arith::unate::conf") << negCons << " is true." << endl;
-
- d_raiseConflict.addConstraint(ant);
- d_raiseConflict.addConstraint(negCons);
- d_raiseConflict.commitConflict();
+bool ConstraintDatabase::handleUnateProp(ConstraintP ant, ConstraintP cons){
+ if(cons->negationHasProof()){
+ Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
+ cons->impliedByUnate(ant, true);
+ d_raiseConflict.raiseConflict(cons);
+ return true;
+ }else if(!cons->isTrue()){
+ ++d_statistics.d_unatePropagateImplications;
+ Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
+ cons->impliedByUnate(ant, false);
+ cons->tryToPropagate();
+ return false;
+ } else {
+ return false;
+ }
}
void ConstraintDatabase::unatePropLowerBound(ConstraintP curr, ConstraintP prev){
@@ -1460,27 +1744,11 @@ void ConstraintDatabase::unatePropLowerBound(ConstraintP curr, ConstraintP prev)
//These should all be handled by propagating the LowerBounds!
if(vc.hasLowerBound()){
ConstraintP lb = vc.getLowerBound();
- if(lb->negationHasProof()){
- raiseUnateConflict(curr, lb);
- return;
- }else if(!lb->isTrue()){
- ++d_statistics.d_unatePropagateImplications;
- Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << lb << endl;
-
- lb->impliedBy(curr);
- }
+ if(handleUnateProp(curr, lb)){ return; }
}
if(vc.hasDisequality()){
ConstraintP dis = vc.getDisequality();
- if(dis->negationHasProof()){
- raiseUnateConflict(curr, dis);
- return;
- }else if(!dis->isTrue()){
- ++d_statistics.d_unatePropagateImplications;
- Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << dis << endl;
-
- dis->impliedBy(curr);
- }
+ if(handleUnateProp(curr, dis)){ return; }
}
}
}
@@ -1511,26 +1779,11 @@ void ConstraintDatabase::unatePropUpperBound(ConstraintP curr, ConstraintP prev)
//These should all be handled by propagating the UpperBounds!
if(vc.hasUpperBound()){
ConstraintP ub = vc.getUpperBound();
- if(ub->negationHasProof()){
- raiseUnateConflict(curr, ub);
- return;
- }else if(!ub->isTrue()){
- ++d_statistics.d_unatePropagateImplications;
- Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << ub << endl;
- ub->impliedBy(curr);
- }
+ if(handleUnateProp(curr, ub)){ return; }
}
if(vc.hasDisequality()){
ConstraintP dis = vc.getDisequality();
- if(dis->negationHasProof()){
- raiseUnateConflict(curr, dis);
- return;
- }else if(!dis->isTrue()){
- Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl;
- ++d_statistics.d_unatePropagateImplications;
-
- dis->impliedBy(curr);
- }
+ if(handleUnateProp(curr, dis)){ return; }
}
}
}
@@ -1568,26 +1821,11 @@ void ConstraintDatabase::unatePropEquality(ConstraintP curr, ConstraintP prevLB,
//These should all be handled by propagating the LowerBounds!
if(vc.hasLowerBound()){
ConstraintP lb = vc.getLowerBound();
- if(lb->negationHasProof()){
- raiseUnateConflict(curr, lb);
- return;
- }else if(!lb->isTrue()){
- ++d_statistics.d_unatePropagateImplications;
- Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << lb << endl;
- lb->impliedBy(curr);
- }
+ if(handleUnateProp(curr, lb)){ return; }
}
if(vc.hasDisequality()){
ConstraintP dis = vc.getDisequality();
- if(dis->negationHasProof()){
- raiseUnateConflict(curr, dis);
- return;
- }else if(!dis->isTrue()){
- ++d_statistics.d_unatePropagateImplications;
- Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl;
-
- dis->impliedBy(curr);
- }
+ if(handleUnateProp(curr, dis)){ return; }
}
}
Assert(scm_i == scm_curr);
@@ -1603,28 +1841,51 @@ void ConstraintDatabase::unatePropEquality(ConstraintP curr, ConstraintP prevLB,
//These should all be handled by propagating the UpperBounds!
if(vc.hasUpperBound()){
ConstraintP ub = vc.getUpperBound();
- if(ub->negationHasProof()){
- raiseUnateConflict(curr, ub);
- return;
- }else if(!ub->isTrue()){
- ++d_statistics.d_unatePropagateImplications;
- Debug("arith::unate") << "unateProp " << curr << " implies " << ub << endl;
-
- ub->impliedBy(curr);
- }
+ if(handleUnateProp(curr, ub)){ return; }
}
if(vc.hasDisequality()){
ConstraintP dis = vc.getDisequality();
- if(dis->negationHasProof()){
- raiseUnateConflict(curr, dis);
- return;
- }else if(!dis->isTrue()){
- ++d_statistics.d_unatePropagateImplications;
- Debug("arith::unate") << "unateProp " << curr << " implies " << dis << endl;
- dis->impliedBy(curr);
- }
+ if(handleUnateProp(curr, dis)){ return; }
+ }
+ }
+}
+
+std::pair<int, int> Constraint::unateFarkasSigns(ConstraintCP ca, ConstraintCP cb){
+ ConstraintType a = ca->getType();
+ ConstraintType b = cb->getType();
+
+ Assert(a != Disequality);
+ Assert(b != Disequality);
+
+ int a_sgn = (a == LowerBound) ? -1 : ((a == UpperBound) ? 1 : 0);
+ int b_sgn = (b == LowerBound) ? -1 : ((b == UpperBound) ? 1 : 0);
+
+ if(a_sgn == 0 && b_sgn == 0){
+ Assert(a == Equality);
+ Assert(b == Equality);
+ Assert(ca->getValue() != cb->getValue());
+ if(ca->getValue() < cb->getValue()){
+ a_sgn = 1;
+ b_sgn = -1;
+ }else{
+ a_sgn = -1;
+ b_sgn = 1;
}
+ }else if(a_sgn == 0){
+ Assert(b_sgn != 0);
+ Assert(a == Equality);
+ a_sgn = -b_sgn;
+ }else if(b_sgn == 0){
+ Assert(a_sgn != 0);
+ Assert(b == Equality);
+ b_sgn = -a_sgn;
}
+ Assert(a_sgn != 0);
+ Assert(b_sgn != 0);
+
+ Debug("arith::unateFarkasSigns") << "Constraint::unateFarkasSigns("<<a <<", " << b << ") -> "
+ << "("<<a_sgn<<", "<< b_sgn <<")"<< endl;
+ return make_pair(a_sgn, b_sgn);
}
}/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index badb97bdd..795798450 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -26,7 +26,7 @@
** the TheoryEngine.
**
** In addition, Constraints keep track of the following:
- ** - A Constrain that is the negation of the Constraint.
+ ** - A Constraint that is the negation of the Constraint.
** - An iterator into a set of Constraints for the ArithVar sorted by
** DeltaRational value.
** - A context dependent internal proof of the node that can be used for
@@ -58,6 +58,16 @@
** Internals:
** - Constraints are pointers to ConstraintValues.
** - Undefined Constraints are NullConstraint.
+
+ **
+ ** Assumption vs. Assertion:
+ ** - An assertion is anything on the theory d_fact queue.
+ ** This includes any thing propagated and returned to the fact queue.
+ ** These can be used in external conflicts and propagations of earlier proofs.
+ ** - An assumption is anything on the theory d_fact queue that has no further
+ ** explanation i.e. this theory did not propagate it.
+ ** - To set something an assumption, first set it as being as assertion.
+ ** - Internal assumptions have no explanations and must be regressed out of the proof.
**/
#include "cvc4_private.h"
@@ -66,6 +76,7 @@
#define __CVC4__THEORY__ARITH__CONSTRAINT_H
#include "expr/node.h"
+#include "proof/proof.h"
#include "context/context.h"
#include "context/cdlist.h"
@@ -87,6 +98,38 @@ namespace theory {
namespace arith {
/**
+ * Logs the types of different proofs.
+ * Current, proof types:
+ * - NoAP : This constraint is not known to be true.
+ * - AssumeAP : This is an input assertion. There is no proof.
+ * : Something can be both asserted and have a proof.
+ * - InternalAssumeAP : An internal assumption. This has no guarantee of having an external proof.
+ * : This must be removed by regression.
+ * - FarkasAP : A proof with Farka's coefficients, i.e.
+ * : \sum lambda_i ( asNode(x_i) <= c_i ) |= 0 < 0
+ * : If proofs are on, coefficients will be logged.
+ * : If proofs are off, coefficients will not be logged.
+ * : A unate implication is a FarkasAP.
+ * - TrichotomyAP : This is any entailment using (x<= a and x >=a) => x = a
+ * : Equivalently, (x > a or x < a or x = a)
+ * : There are 3 candidate ways this can propagate:
+ * : !(x > a) and !(x = a) => x < a
+ * : !(x < a) and !(x = a) => x > a
+ * : !(x > a) and !(x < a) => x = a
+ * - EqualityEngineAP : This is propagated by the equality engine.
+ * : Consult this for the proof.
+ * - IntHoleAP : This is currently a catch-all for all integer specific reason.
+ */
+enum ArithProofType
+ { NoAP,
+ AssumeAP,
+ InternalAssumeAP,
+ FarkasAP,
+ TrichotomyAP,
+ EqualityEngineAP,
+ IntHoleAP};
+
+/**
* The types of constraints.
* The convex constraints are the constraints are LowerBound, Equality,
* and UpperBound.
@@ -98,11 +141,16 @@ typedef context::CDList<ConstraintCP> CDConstraintList;
typedef __gnu_cxx::hash_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap;
-typedef size_t ProofId;
-static ProofId ProofIdSentinel = std::numeric_limits<ProofId>::max();
+typedef size_t ConstraintRuleID;
+static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max();
+
+typedef size_t AntecedentId;
+static const AntecedentId AntecedentIdSentinel = std::numeric_limits<AntecedentId>::max();
+
typedef size_t AssertionOrder;
-static AssertionOrder AssertionOrderSentinel = std::numeric_limits<AssertionOrder>::max();
+static const AssertionOrder AssertionOrderSentinel = std::numeric_limits<AssertionOrder>::max();
+
/**
* A ValueCollection binds together convex constraints that have the same
@@ -195,7 +243,103 @@ struct PerVariableDatabase{
}
};
-class Constraint_ {
+
+/**
+ * If proofs are on, there is a vector of rationals for farkas coefficients.
+ * This is the owner of the memory for the vector, and calls delete upon cleanup.
+ *
+ */
+struct ConstraintRule {
+ ConstraintP d_constraint;
+ ArithProofType d_proofType;
+ AntecedentId d_antecedentEnd;
+
+ /**
+ * In this comment, we abbreviate ConstraintDatabase::d_antecedents
+ * and d_farkasCoefficients as ans and fc.
+ *
+ * This list is always empty if proofs are not enabled.
+ *
+ * If proofs are enabled, the proof of constraint c at p in ans[p] of length n is
+ * (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])
+ *
+ * Farkas' proofs show a contradiction with the negation of c, c_not = c->getNegation().
+ *
+ * We treat the position for NullConstraint (p-n) as the position for the farkas
+ * coefficient for so we pretend c_not is ans[p-n].
+ * So this correlation for the constraints we are going to use:
+ * (c_not, ans[p-(n-1)], ... , ans[p-1], ans[p])
+ * With the coefficients at positions:
+ * (fc[0], fc[1)], ... fc[n])
+ *
+ * The index of the constraints in the proof are {i | i <= 0 <= n] } (with c_not being p-n).
+ * Partition the indices into L, U, and E, the lower bounds, the upper bounds and equalities.
+ *
+ * We standardize the proofs to be upper bound oriented following the convention:
+ * A x <= b
+ * with the proof witness of the form
+ * (lambda) Ax <= (lambda) b and lambda >= 0.
+ *
+ * To accomplish this cleanly, the fc coefficients must be negative for lower bounds.
+ * The signs of equalities can be either positive or negative.
+ *
+ * Thus the proof corresponds to (with multiplication over inequalities):
+ * \sum_{u in U} fc[u] ans[p-n+u] + \sum_{e in E} fc[e] ans[p-n+e]
+ * + \sum_{l in L} fc[l] ans[p-n+l]
+ * |= 0 < 0
+ * where fc[u] > 0, fc[l] < 0, and fc[e] != 0 (i.e. it can be either +/-).
+ *
+ * There is no requirement that the proof is minimal.
+ * We do however use all of the constraints by requiring non-zero coefficients.
+ */
+#ifdef CVC4_PROOF
+ RationalVectorCP d_farkasCoefficients;
+#endif
+ ConstraintRule()
+ : d_constraint(NullConstraint)
+ , d_proofType(NoAP)
+ , d_antecedentEnd(AntecedentIdSentinel)
+ {
+#ifdef CVC4_PROOF
+ d_farkasCoefficients = RationalVectorCPSentinel;
+#endif
+ }
+
+ ConstraintRule(ConstraintP con, ArithProofType pt)
+ : d_constraint(con)
+ , d_proofType(pt)
+ , d_antecedentEnd(AntecedentIdSentinel)
+ {
+#ifdef CVC4_PROOF
+ d_farkasCoefficients = RationalVectorCPSentinel;
+#endif
+ }
+ ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd)
+ : d_constraint(con)
+ , d_proofType(pt)
+ , d_antecedentEnd(antecedentEnd)
+ {
+#ifdef CVC4_PROOF
+ d_farkasCoefficients = RationalVectorCPSentinel;
+#endif
+ }
+
+ ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd, RationalVectorCP coeffs)
+ : d_constraint(con)
+ , d_proofType(pt)
+ , d_antecedentEnd(antecedentEnd)
+ {
+ Assert(PROOF_ON() || coeffs == RationalVectorCPSentinel);
+#ifdef CVC4_PROOF
+ d_farkasCoefficients = coeffs;
+#endif
+ }
+
+ void print(std::ostream& out) const;
+ void debugPrint() const;
+}; /* class ConstraintRule */
+
+class Constraint {
private:
/** The ArithVar associated with the constraint. */
const ArithVar d_variable;
@@ -207,7 +351,7 @@ private:
const DeltaRational d_value;
/** A pointer to the associated database for the Constraint. */
- ConstraintDatabase * d_database;
+ ConstraintDatabase* d_database;
/**
* The node to be communicated with the TheoryEngine.
@@ -253,12 +397,13 @@ private:
TNode d_witness;
/**
- * This points at the proof for the constraint in the current context.
+ * The position of the constraint in the constraint rule id.
*
* Sat Context Dependent.
- * This is initially ProofIdSentinel.
+ * This is initially
*/
- ProofId d_proof;
+ ConstraintRuleID d_crid;
+
/**
* True if the equality has been split.
@@ -285,14 +430,15 @@ private:
* Because of circular dependencies a Constraint is not fully valid until
* initialize has been called on it.
*/
- Constraint_(ArithVar x, ConstraintType t, const DeltaRational& v);
+ Constraint(ArithVar x, ConstraintType t, const DeltaRational& v);
/**
* Destructor for a constraint.
* This should only be called if safeToGarbageCollect() is true.
*/
- ~Constraint_();
+ ~Constraint();
+ /** Returns true if the constraint has been initialized. */
bool initialized() const;
/**
@@ -301,12 +447,18 @@ private:
*/
void initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation);
- class ProofCleanup {
+
+ class ConstraintRuleCleanup {
public:
- inline void operator()(ConstraintP* p){
- ConstraintP constraint = *p;
- Assert(constraint->d_proof != ProofIdSentinel);
- constraint->d_proof = ProofIdSentinel;
+ inline void operator()(ConstraintRule* crp){
+ Assert(crp != NULL);
+ ConstraintP constraint = crp->d_constraint;
+ Assert(constraint->d_crid != ConstraintRuleIdSentinel);
+ constraint->d_crid = ConstraintRuleIdSentinel;
+
+ PROOF(if(crp->d_farkasCoefficients != RationalVectorCPSentinel){
+ delete crp->d_farkasCoefficients;
+ });
}
};
@@ -339,10 +491,18 @@ private:
}
};
- /** Returns true if the node is safe to garbage collect. */
+ /**
+ * Returns true if the node is safe to garbage collect.
+ * Both it and its negation must have no context dependent data set.
+ */
bool safeToGarbageCollect() const;
/**
+ * Returns true if the constraint has no context dependent data set.
+ */
+ bool contextDependentDataIsSet() const;
+
+ /**
* Returns true if the node correctly corresponds to the constraint that is
* being set.
*/
@@ -351,13 +511,17 @@ private:
/** Returns a reference to the map for d_variable. */
SortedConstraintMap& constraintSet() const;
+ /** Returns coefficients for the proofs for farkas cancellation. */
+ static std::pair<int, int> unateFarkasSigns(ConstraintCP a, ConstraintCP b);
+
+
public:
- ConstraintType getType() const {
+ inline ConstraintType getType() const {
return d_type;
}
- ArithVar getVariable() const {
+ inline ArithVar getVariable() const {
return d_variable;
}
@@ -365,7 +529,7 @@ public:
return d_value;
}
- ConstraintP getNegation() const {
+ inline ConstraintP getNegation() const {
return d_negation;
}
@@ -429,14 +593,18 @@ public:
return d_assertionOrder < time;
}
- /** Sets the witness literal for a node being on the assertion stack.
- * The negation of the node cannot be true. */
- void setAssertedToTheTheory(TNode witness);
-
- /** Sets the witness literal for a node being on the assertion stack.
- * The negation of the node must be true!
- * This is for conflict generation specificially! */
- void setAssertedToTheTheoryWithNegationTrue(TNode witness);
+ /**
+ * Sets the witness literal for a node being on the assertion stack.
+ *
+ * If the negation of the node is true, inConflict must be true.
+ * If the negation of the node is false, inConflict must be false.
+ * Hence, negationHasProof() == inConflict.
+ *
+ * This replaces:
+ * void setAssertedToTheTheory(TNode witness);
+ * void setAssertedToTheTheoryWithNegationTrue(TNode witness);
+ */
+ void setAssertedToTheTheory(TNode witness, bool inConflict);
bool hasLiteral() const {
return !d_literal.isNull();
@@ -450,25 +618,35 @@ public:
}
/**
- * Set the node as selfExplaining().
+ * Set the node as having a proof and being an assumption.
* The node must be assertedToTheTheory().
+ *
+ * Precondition: negationHasProof() == inConflict.
+ *
+ * Replaces:
+ * selfExplaining().
+ * selfExplainingWithNegationTrue().
*/
- void selfExplaining();
-
- void selfExplainingWithNegationTrue();
+ void setAssumption(bool inConflict);
- /** Returns true if the node is selfExplaining.*/
- bool isSelfExplaining() const;
+ /** Returns true if the node is an assumption.*/
+ bool isAssumption() const;
- /**
- * Set the constraint to be a EqualityEngine proof.
- */
+ /** Set the constraint to have an EqualityEngine proof. */
void setEqualityEngineProof();
bool hasEqualityEngineProof() const;
+ /** Returns true if the node has a Farkas' proof. */
+ bool hasFarkasProof() const;
+
+ /** Returns true if the node has a int hole proof. */
+ bool hasIntHoleProof() const;
+
+ /** Returns true if the node has a trichotomy proof. */
+ bool hasTrichotomyProof() const;
/**
- * A sets the constraint to be an internal decision.
+ * A sets the constraint to be an internal assumption.
*
* This does not need to have a witness or an associated literal.
* This is always itself in the explanation fringe for both conflicts
@@ -476,9 +654,10 @@ public:
* This cannot be converted back into a Node conflict or explanation.
*
* This cannot have a proof or be asserted to the theory!
+ *
*/
- void setInternalDecision();
- bool isInternalDecision() const;
+ void setInternalAssumption(bool inConflict);
+ bool isInternalAssumption() const;
/**
* Returns a explanation of the constraint that is appropriate for conflicts.
@@ -509,10 +688,8 @@ public:
/* Equivalent to calling externalExplainByAssertions on all constraints in b */
static Node externalExplainByAssertions(const ConstraintCPVec& b);
- /* utilities for calling externalExplainByAssertions on 2 constraints */
static Node externalExplainByAssertions(ConstraintCP a, ConstraintCP b);
static Node externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c);
- //static Node externalExplainByAssertions(ConstraintCP a);
/**
* This is the minimum fringe of the implication tree s.t. every constraint is
@@ -523,38 +700,31 @@ public:
static void assertionFringe(ConstraintCPVec& v);
static void assertionFringe(ConstraintCPVec& out, const ConstraintCPVec& in);
- /** Utility function built from explainForConflict. */
- //static Node explainConflict(ConstraintP a, ConstraintP b);
- //static Node explainConflict(ConstraintP a, ConstraintP b, Constraint c);
-
- //static Node explainConflictForEE(ConstraintCP a, ConstraintCP b);
- //static Node explainConflictForEE(ConstraintCP a);
- //static Node explainConflictForDio(ConstraintCP a);
- //static Node explainConflictForDio(ConstraintCP a, ConstraintCP b);
-
+ /** The fringe of a farkas' proof. */
bool onFringe() const {
- return assertedToTheTheory() || isInternalDecision() || hasEqualityEngineProof();
+ return assertedToTheTheory() || isInternalAssumption() || hasEqualityEngineProof();
}
/**
* Returns an explanation of a propagation by the ConstraintDatabase.
* The constraint must have a proof.
- * The constraint cannot be selfExplaining().
+ * The constraint cannot be an assumption.
*
* This is the minimum fringe of the implication tree (excluding the constraint itself)
* s.t. every constraint is assertedToTheTheory() or hasEqualityEngineProof().
*/
Node externalExplainForPropagation() const {
Assert(hasProof());
- Assert(!isSelfExplaining());
+ Assert(!isAssumption());
+ Assert(!isInternalAssumption());
return externalExplain(d_assertionOrder);
}
- // void externalExplainForPropagation(NodeBuilder<>& nb) const{
- // Assert(hasProof());
- // Assert(!isSelfExplaining());
- // externalExplain(nb, d_assertionOrder);
- // }
+ /**
+ * Explain the constraint and its negation in terms of assertions.
+ * The constraint must be in conflict.
+ */
+ Node externalExplainConflict() const;
private:
Node externalExplain(AssertionOrder order) const;
@@ -572,23 +742,32 @@ private:
static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);
public:
- bool hasProof() const {
- return d_proof != ProofIdSentinel;
+
+ /** The constraint is known to be true. */
+ inline bool hasProof() const {
+ return d_crid != ConstraintRuleIdSentinel;
}
- bool negationHasProof() const {
+
+ /** The negation of the constraint is known to hold. */
+ inline bool negationHasProof() const {
return d_negation->hasProof();
}
- /* Neither the contraint has a proof nor the negation has a proof.*/
+ /** Neither the contraint has a proof nor the negation has a proof.*/
bool truthIsUnknown() const {
return !hasProof() && !negationHasProof();
}
- /* This is a synonym for hasProof(). */
- bool isTrue() const {
+ /** This is a synonym for hasProof(). */
+ inline bool isTrue() const {
return hasProof();
}
+ /** Both the constraint and its negation are true. */
+ inline bool inConflict() const {
+ return hasProof() && negationHasProof();
+ }
+
/**
* Returns the constraint that corresponds to taking
* x r ceiling(getValue()) where r is the node's getType().
@@ -613,53 +792,118 @@ public:
ConstraintP getStrictlyWeakerLowerBound(bool hasLiteral, bool mustBeAsserted) const;
/**
- * Marks the node as having a proof a.
- * Adds the node the database's propagation queue.
+ * Marks a the constraint c as being entailed by a.
+ * The Farkas proof 1*(a) + -1 (c) |= 0<0
+ *
+ * After calling impliedByUnate(), the caller should either raise a conflict
+ * or try call tryToPropagate().
+ */
+ void impliedByUnate(ConstraintCP a, bool inConflict);
+
+ /**
+ * Marks a the constraint c as being entailed by a.
+ * The reason has to do with integer rounding.
+ *
+ * After calling impliedByIntHole(), the caller should either raise a conflict
+ * or try call tryToPropagate().
+ */
+ void impliedByIntHole(ConstraintCP a, bool inConflict);
+
+ /**
+ * Marks a the constraint c as being entailed by a.
+ * The reason has to do with integer rounding.
+ *
+ * After calling impliedByIntHole(), the caller should either raise a conflict
+ * or try call tryToPropagate().
+ */
+ void impliedByIntHole(const ConstraintCPVec& b, bool inConflict);
+
+ /**
+ * This is a lemma of the form:
+ * x < d or x = d or x > d
+ * The current constraint c is one of the above constraints and {a,b}
+ * are the negation of the other two constraints.
*
* Preconditions:
- * canBePropagated()
- * !assertedToTheTheory()
+ * - negationHasProof() == inConflict.
+ *
+ * After calling impliedByTrichotomy(), the caller should either raise a conflict
+ * or try call tryToPropagate().
*/
- void propagate(ConstraintCP a);
- void propagate(ConstraintCP a, ConstraintCP b);
- //void propagate(const std::vector<Constraint>& b);
- void propagate(const ConstraintCPVec& b);
+ void impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool inConflict);
/**
- * The only restriction is that this is not known be true.
- * This propagates if there is a node.
+ * Marks the node as having a Farkas proof.
+ *
+ * Preconditions:
+ * - coeffs == NULL if proofs are off.
+ * - See the comments for ConstraintRule for the form of coeffs when
+ * proofs are on.
+ * - negationHasProof() == inConflict.
+ *
+ * After calling impliedByFarkas(), the caller should either raise a conflict
+ * or try call tryToPropagate().
*/
- void impliedBy(ConstraintCP a);
- void impliedBy(ConstraintCP a, ConstraintCP b);
- //void impliedBy(const std::vector<Constraint>& b);
- void impliedBy(const ConstraintCPVec& b);
+ void impliedByFarkas(const ConstraintCPVec& b, RationalVectorCP coeffs, bool inConflict);
+ /**
+ * Generates an implication node, B => getLiteral(),
+ * where B is the result of externalExplainByAssertions(b).
+ * Does not guarantee b is the explanation of the constraint.
+ */
Node externalImplication(const ConstraintCPVec& b) const;
- static Node externalConjunction(const ConstraintCPVec& b);
- //static Node makeConflictNode(const ConstraintCPVec& b);
-
- /** The node must have a proof already and be eligible for propagation! */
- void propagate();
+ /**
+ * Returns true if the variable is assigned the value dr,
+ * the constraint would be satisfied.
+ */
bool satisfiedBy(const DeltaRational& dr) const;
-private:
/**
- * Marks the node as having a proof and being selfExplaining.
- * Neither the node nor its negation can have a proof.
- * This is internal!
+ * The node must have a proof already and be eligible for propagation!
+ * You probably want to call tryToPropagate() instead.
+ *
+ * Preconditions:
+ * - hasProof()
+ * - canBePropagated()
+ * - !assertedToTheTheory()
*/
- void markAsTrue();
+ void propagate();
+
/**
- * Marks the node as having a proof a.
- * This is safe if the node does not have
+ * If the constraint
+ * canBePropagated() and
+ * !assertedToTheTheory(),
+ * the constraint is added to the database's propagation queue.
+ *
+ * Precondition:
+ * - hasProof()
*/
- void markAsTrue(ConstraintCP a);
+ void tryToPropagate();
+
+ /**
+ * Returns a reference to the containing database.
+ * Precondition: the constraint must be initialized.
+ */
+ const ConstraintDatabase& getDatabase() const;
+
+private:
+
+ /** Returns the constraint rule at the position. */
+ const ConstraintRule& getConstraintRule() const;
+
+ inline ArithProofType getProofType() const {
+ return getConstraintRule().d_proofType;
+ }
- void markAsTrue(ConstraintCP a, ConstraintCP b);
- //void markAsTrue(const std::vector<Constraint>& b);
- void markAsTrue(const ConstraintCPVec& b);
+ inline AntecedentId getEndAntecedent() const {
+ return getConstraintRule().d_antecedentEnd;
+ }
+ inline RationalVectorCP getFarkasCoefficients() const {
+ return NULLPROOF(getConstraintRule().d_farkasCoefficients);
+ }
+
void debugPrint() const;
/**
@@ -668,15 +912,25 @@ private:
* isSelfExplaining() or
* hasEqualityEngineProof()
*/
- bool proofIsEmpty() const;
+ bool antecentListIsEmpty() const;
+
+ bool antecedentListLengthIsOne() const;
+
+ /** Return true if every element in b has a proof. */
+ static bool allHaveProof(const ConstraintCPVec& b);
+ /** Precondition: hasFarkasProof() */
+ bool wellFormedFarkasProof() const;
+
}; /* class ConstraintValue */
-std::ostream& operator<<(std::ostream& o, const Constraint_& c);
+std::ostream& operator<<(std::ostream& o, const Constraint& c);
std::ostream& operator<<(std::ostream& o, const ConstraintP c);
+std::ostream& operator<<(std::ostream& o, const ConstraintCP c);
std::ostream& operator<<(std::ostream& o, const ConstraintType t);
std::ostream& operator<<(std::ostream& o, const ValueCollection& c);
std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v);
+std::ostream& operator<<(std::ostream& o, const ArithProofType);
class ConstraintDatabase {
@@ -701,62 +955,46 @@ private:
context::CDQueue<ConstraintCP> d_toPropagate;
/**
- * Proof Lists.
- * Proofs are lists of valid constraints terminated by the first smaller
+ * Proofs are lists of valid constraints terminated by the first null
* sentinel value in the proof list.
- * The proof at p in d_proofs[p] of length n is
- * (NullConstraint, d_proofs[p-(n-1)], ... , d_proofs[p-1], d_proofs[p])
+ * We abbreviate d_antecedents as ans in the comment.
+ *
+ * The proof at p in ans[p] of length n is
+ * (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])
+ *
* The proof at p corresponds to the conjunction:
* (and x_i)
*
* So the proof of a Constraint c corresponds to the horn clause:
* (implies (and x_i) c)
- * where (and x_i) is the proof at c.d_proofs.
+ * where (and x_i) is the proof at c.d_crid d_antecedentEnd.
*
- * Constraints are pointers so this list is designed not to require any
- * destruction.
+ * Constraints are pointers so this list is designed not to require any destruction.
*/
- CDConstraintList d_proofs;
+ CDConstraintList d_antecedents;
- /**
- * This is a special proof for marking that nodes are their own explanation
- * from the perspective of the theory.
- * These must always be asserted to the theory.
- *
- * This proof is always a member of the list.
- */
- ProofId d_selfExplainingProof;
-
- /**
- * Marks a node as being proved by the equality engine.
- * The equality engine will be asked for the explanation of such nodes.
- *
- * This is a special proof that is always a member of the list.
- */
- ProofId d_equalityEngineProof;
+ typedef context::CDList<ConstraintRule, Constraint::ConstraintRuleCleanup> ConstraintRuleList;
+ typedef context::CDList<ConstraintP, Constraint::CanBePropagatedCleanup> CBPList;
+ typedef context::CDList<ConstraintP, Constraint::AssertionOrderCleanup> AOList;
+ typedef context::CDList<ConstraintP, Constraint::SplitCleanup> SplitList;
- /**
- * Marks a constraint as being proved by making an internal
- * decision. Such nodes cannot be used in external explanations
- * but can be used internally.
- */
- ProofId d_internalDecisionProof;
- typedef context::CDList<ConstraintP, Constraint_::ProofCleanup> ProofCleanupList;
- typedef context::CDList<ConstraintP, Constraint_::CanBePropagatedCleanup> CBPList;
- typedef context::CDList<ConstraintP, Constraint_::AssertionOrderCleanup> AOList;
- typedef context::CDList<ConstraintP, Constraint_::SplitCleanup> SplitList;
/**
* The watch lists are collected together as they need to be garbage collected
* carefully.
*/
struct Watches{
+
/**
- * Contains the exact list of atoms that have a proof.
+ * Contains the exact list of constraints that have a proof.
+ * Upon pop, this unsets d_crid to NoAP.
+ *
+ * The index in this list is the proper ordering of the proofs.
*/
- ProofCleanupList d_proofWatches;
-
+ ConstraintRuleList d_constraintProofs;
+
+
/**
* Contains the exact list of constraints that can be used for propagation.
*/
@@ -781,7 +1019,9 @@ private:
void pushSplitWatch(ConstraintP c);
void pushCanBePropagatedWatch(ConstraintP c);
void pushAssertionOrderWatch(ConstraintP c, TNode witness);
- void pushProofWatch(ConstraintP c, ProofId pid);
+
+ /** Assumes that antecedents have already been pushed. */
+ void pushConstraintRule(const ConstraintRule& crp);
/** Returns true if all of the entries of the vector are empty. */
static bool emptyDatabase(const std::vector<PerVariableDatabase>& vec);
@@ -796,12 +1036,15 @@ private:
ArithCongruenceManager& d_congruenceManager;
const context::Context * const d_satContext;
- const int d_satAllocationLevel;
RaiseConflict d_raiseConflict;
- friend class Constraint_;
+ const Rational d_one;
+ const Rational d_negOne;
+
+ friend class Constraint;
+
public:
ConstraintDatabase( context::Context* satContext,
@@ -906,8 +1149,12 @@ public:
void unatePropUpperBound(ConstraintP curr, ConstraintP prev);
void unatePropEquality(ConstraintP curr, ConstraintP prevLB, ConstraintP prevUB);
+ /** AntecendentID must be in range. */
+ ConstraintCP getAntecedent(AntecedentId p) const;
+
private:
- void raiseUnateConflict(ConstraintP ant, ConstraintP cons);
+ /** returns true if cons is now in conflict. */
+ bool handleUnateProp(ConstraintP ant, ConstraintP cons);
DenseSet d_reclaimable;
diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h
index c9a630984..bfa42af46 100644
--- a/src/theory/arith/constraint_forward.h
+++ b/src/theory/arith/constraint_forward.h
@@ -26,16 +26,22 @@ namespace CVC4 {
namespace theory {
namespace arith {
-class Constraint_;
-typedef Constraint_* ConstraintP;
-typedef const Constraint_* ConstraintCP;
+class Constraint;
+typedef Constraint* ConstraintP;
+typedef const Constraint* ConstraintCP;
-const ConstraintP NullConstraint = NULL;
+static const ConstraintP NullConstraint = NULL;
class ConstraintDatabase;
typedef std::vector<ConstraintCP> ConstraintCPVec;
+typedef std::vector<Rational> RationalVector;
+typedef RationalVector* RationalVectorP;
+typedef const RationalVector* RationalVectorCP;
+static const RationalVectorCP RationalVectorCPSentinel = NULL;
+static const RationalVectorP RationalVectorPSentinel = NULL;
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 36208ff8d..7e50dad87 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -145,6 +145,8 @@ void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){
return;
}
+
+
uint32_t length = sp.maxLength();
if(length > d_maxInputCoefficientLength){
d_maxInputCoefficientLength = length;
@@ -155,7 +157,10 @@ void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){
//Variable proofVariable(makeIntegerVariable());
TrailIndex posInTrail = d_trail.size();
- d_trail.push_back(Constraint(sp,Polynomial(Monomial(VarList(proofVariable)))));
+ Debug("dio::pushInputConstraint") << "pushInputConstraint @ " << posInTrail
+ << " " << eq.getNode()
+ << " " << reason << endl;
+ d_trail.push_back(Constraint(sp,Polynomial::mkPolynomial(proofVariable)));
size_t posInConstraintList = d_inputConstraints.size();
d_inputConstraints.push_back(InputConstraint(reason, posInTrail));
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 2aeee696e..bd252bf49 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -55,6 +55,10 @@ LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, Bou
d_basicVariableUpdates(f),
d_increasing(1),
d_decreasing(-1),
+ d_upperBoundDifference(),
+ d_lowerBoundDifference(),
+ d_one(1),
+ d_negOne(-1),
d_btracking(boundsTracking),
d_areTracking(false),
d_trackCallback(this)
@@ -505,40 +509,117 @@ void LinearEqualityModule::propagateBasicFromRow(ConstraintP c){
RowIndex ridx = d_tableau.basicToRowIndex(basic);
ConstraintCPVec bounds;
- propagateRow(bounds, ridx, upperBound, c);
- c->impliedBy(bounds);
+ RationalVectorP coeffs = NULLPROOF(new RationalVector());
+ propagateRow(bounds, ridx, upperBound, c, coeffs);
+ c->impliedByFarkas(bounds, coeffs, false);
+ c->tryToPropagate();
+
+ if(coeffs != RationalVectorPSentinel) { delete coeffs; }
}
-void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bool rowUp, ConstraintP c){
+/* An explanation of the farkas coefficients.
+ *
+ * We are proving c using the other variables on the row.
+ * The proof is in terms of the other constraints and the negation of c, ~c.
+ *
+ * A row has the form:
+ * sum a_i * x_i = 0
+ * or
+ * sx + sum r y + sum q z = 0
+ * where r > 0 and q < 0.
+ *
+ * If rowUp, we are proving c
+ * g = sum r u_y + sum q l_z
+ * and c is entailed by -sx <= g
+ * If !rowUp, we are proving c
+ * g = sum r l_y + sum q u_z
+ * and c is entailed by -sx >= g
+ *
+ * | s | c | ~c | u_i | l_i
+ * if rowUp | s > 0 | x >= -g/s | x < -g/s | a_i > 0 | a_i < 0
+ * if rowUp | s < 0 | x <= -g/s | x > -g/s | a_i > 0 | a_i < 0
+ * if !rowUp | s > 0 | x <= -g/s | x > -g/s | a_i < 0 | a_i > 0
+ * if !rowUp | s < 0 | x >= -g/s | x < -g/s | a_i < 0 | a_i > 0
+ *
+ *
+ * Thus we treat !rowUp as multiplying the row by -1 and rowUp as 1
+ * for the entire row.
+ */
+void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bool rowUp, ConstraintP c, RationalVectorP farkas){
Assert(!c->assertedToTheTheory());
Assert(c->canBePropagated());
Assert(!c->hasProof());
+ if(farkas != RationalVectorPSentinel){
+ Assert(farkas->empty());
+ farkas->push_back(Rational(0));
+ }
+
ArithVar v = c->getVariable();
- Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
- << v <<") start" << endl;
+ Debug("arith::propagateRow") << "LinearEqualityModule::propagateRow("
+ << ridx << ", " << rowUp << ", " << v << ") start" << endl;
+
+ const Rational& multiple = rowUp ? d_one : d_negOne;
+ Debug("arith::propagateRow") << "multiple: " << multiple << endl;
+
Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
for(; !iter.atEnd(); ++iter){
const Tableau::Entry& entry = *iter;
ArithVar nonbasic = entry.getColVar();
- if(nonbasic == v){ continue; }
-
const Rational& a_ij = entry.getCoefficient();
-
int sgn = a_ij.sgn();
Assert(sgn != 0);
bool selectUb = rowUp ? (sgn > 0) : (sgn < 0);
- ConstraintCP bound = selectUb
- ? d_variables.getUpperBoundConstraint(nonbasic)
- : d_variables.getLowerBoundConstraint(nonbasic);
- Assert(bound != NullConstraint);
- Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
- into.push_back(bound);
+ Assert( nonbasic != v ||
+ ( rowUp && a_ij.sgn() > 0 && c->isLowerBound()) ||
+ ( rowUp && a_ij.sgn() < 0 && c->isUpperBound()) ||
+ (!rowUp && a_ij.sgn() > 0 && c->isUpperBound()) ||
+ (!rowUp && a_ij.sgn() < 0 && c->isLowerBound())
+ );
+
+ if(Debug.isOn("arith::propagateRow")){
+ if(nonbasic == v){
+ Debug("arith::propagateRow") << "(target) "
+ << rowUp << " "
+ << a_ij.sgn() << " "
+ << c->isLowerBound() << " "
+ << c->isUpperBound() << endl;
+
+ Debug("arith::propagateRow") << "(target) ";
+ }
+ Debug("arith::propagateRow") << "propagateRow " << a_ij << " * " << nonbasic ;
+ }
+
+ if(nonbasic == v){
+ if(farkas != RationalVectorPSentinel){
+ Assert(farkas->front().isZero());
+ Rational multAij = multiple * a_ij;
+ Debug("arith::propagateRow") << "("<<multAij<<") ";
+ farkas->front() = multAij;
+ }
+
+ Debug("arith::propagateRow") << c << endl;
+ }else{
+
+ ConstraintCP bound = selectUb
+ ? d_variables.getUpperBoundConstraint(nonbasic)
+ : d_variables.getLowerBoundConstraint(nonbasic);
+
+ if(farkas != RationalVectorPSentinel){
+ Rational multAij = multiple * a_ij;
+ Debug("arith::propagateRow") << "("<<multAij<<") ";
+ farkas->push_back(multAij);
+ }
+ Assert(bound != NullConstraint);
+ Debug("arith::propagateRow") << bound << endl;
+ into.push_back(bound);
+ }
}
- Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
- << v << ") done" << endl;
+ Debug("arith::propagateRow") << "LinearEqualityModule::propagateRow("
+ << ridx << ", " << rowUp << ", " << v << ") done" << endl;
+
}
ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic) const {
@@ -574,13 +655,13 @@ ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRatio
anyWeakening = true;
surplus = surplus - diff;
- Debug("weak") << "found:" << endl;
+ Debug("arith::weak") << "found:" << endl;
if(v == basic){
- Debug("weak") << " basic: ";
+ Debug("arith::weak") << " basic: ";
}
- Debug("weak") << " " << surplus << " "<< diff << endl
- << " " << bound << c << endl
- << " " << weakerBound << weaker << endl;
+ Debug("arith::weak") << " " << surplus << " "<< diff << endl
+ << " " << bound << c << endl
+ << " " << weakerBound << weaker << endl;
Assert(diff.sgn() > 0);
c = weaker;
@@ -591,9 +672,48 @@ ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRatio
return c;
}
-void LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, RaiseConflict& rc) const {
+/* An explanation of the farkas coefficients.
+ *
+ * We are proving a conflict on the basic variable x_b.
+ * If aboveUpper, then the conflict is with the constraint c : x_b <= u_b.
+ * If !aboveUpper, then the conflict is with the constraint c : x_b >= l_b.
+ *
+ * A row has the form:
+ * -x_b sum a_i * x_i = 0
+ * or
+ * -x_b + sum r y + sum q z = 0,
+ * x_b = sum r y + sum q z
+ * where r > 0 and q < 0.
+ *
+ *
+ * If !aboveUp, we are proving ~c: x_b < l_b
+ * g = sum r u_y + sum q l_z
+ * x_b <= g < l_b
+ * and ~c is entailed by x_b <= g
+ *
+ * If aboveUp, we are proving ~c : x_b > u_b
+ * g = sum r l_y + sum q u_z
+ * x_b >= g > u_b
+ * and ~c is entailed by x_b >= g
+ *
+ *
+ * | s | c | ~c | u_i | l_i
+ * if !aboveUp | s > 0 | x >= -g/s | x < -g/s | a_i > 0 | a_i < 0
+ * if !aboveUp | s < 0 | x <= -g/s | x > -g/s | a_i > 0 | a_i < 0
+ * if aboveUp | s > 0 | x <= -g/s | x > -g/s | a_i < 0 | a_i > 0
+ * if aboveUp | s < 0 | x >= -g/s | x < -g/s | a_i < 0 | a_i > 0
+ *
+ * Thus we treat aboveUp as multiplying the row by -1 and !aboveUp as 1
+ * for the entire row.
+ */
+ConstraintCP LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, FarkasConflictBuilder& fcs) const {
+ Assert(!fcs.underConstruction());
TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
+ Debug("arith::weak") << "LinearEqualityModule::minimallyWeakConflict("
+ << aboveUpper <<", "<< basicVar << ", ...) start" << endl;
+
+ const Rational& adjustSgn = aboveUpper ? d_negOne : d_one;
const DeltaRational& assignment = d_variables.getAssignment(basicVar);
DeltaRational surplus;
if(aboveUpper){
@@ -605,7 +725,7 @@ void LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basic
Assert(assignment < d_variables.getLowerBound(basicVar));
surplus = d_variables.getLowerBound(basicVar) - assignment;
}
-
+
bool anyWeakenings = false;
for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){
const Tableau::Entry& entry = *i;
@@ -613,18 +733,29 @@ void LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basic
const Rational& coeff = entry.getCoefficient();
bool weakening = false;
ConstraintP c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar);
- Debug("weak") << "weak : " << weakening << " "
- << c->assertedToTheTheory() << " "
- << d_variables.getAssignment(v) << " "
- << c << endl;
+ Debug("arith::weak") << "weak : " << weakening << " "
+ << c->assertedToTheTheory() << " "
+ << d_variables.getAssignment(v) << " "
+ << c << endl;
anyWeakenings = anyWeakenings || weakening;
- rc.addConstraint(c);
+ fcs.addConstraint(c, coeff, adjustSgn);
+ if(basicVar == v){
+ Assert(! c->negationHasProof() );
+ fcs.makeLastConsequent();
+ }
}
+ Assert(fcs.consequentIsSet());
+
+ ConstraintCP conflicted = fcs.commitConflict();
+
++d_statistics.d_weakeningAttempts;
if(anyWeakenings){
++d_statistics.d_weakeningSuccesses;
}
+ Debug("arith::weak") << "LinearEqualityModule::minimallyWeakConflict("
+ << aboveUpper <<", "<< basicVar << ", ...) done" << endl;
+ return conflicted;
}
ArithVar LinearEqualityModule::minVarOrder(ArithVar x, ArithVar y) const {
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 5e325d799..f6717d141 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -199,6 +199,7 @@ public:
typedef bool (LinearEqualityModule::*UpdatePreferenceFunction)(const UpdateInfo&, const UpdateInfo&) const;
+
private:
/**
* Manages information about the assignment and upper and lower bounds on the
@@ -217,6 +218,8 @@ private:
Maybe<DeltaRational> d_upperBoundDifference;
Maybe<DeltaRational> d_lowerBoundDifference;
+ Rational d_one;
+ Rational d_negOne;
public:
/**
@@ -417,10 +420,20 @@ public:
void propagateBasicFromRow(ConstraintP c);
/**
+ * Let v be the variable for the constraint c.
* Exports either the explanation of an upperbound or a lower bound
- * of the basic variable basic, using the non-basic variables in the row.
+ * of v using the other variables in the row.
+ *
+ * If farkas != RationalVectorPSentinel, this function additionally
+ * stores the farkas coefficients of the constraints stored in into.
+ * Position 0 is the coefficient of v.
+ * Position i > 0, corresponds to the order of the other constraints.
*/
- void propagateRow(ConstraintCPVec& into, RowIndex ridx, bool rowUp, ConstraintP c);
+ void propagateRow(ConstraintCPVec& into
+ , RowIndex ridx
+ , bool rowUp
+ , ConstraintP c
+ , RationalVectorP farkas);
/**
* Computes the value of a basic variable using the assignments
@@ -598,20 +611,22 @@ private:
public:
/**
* Constructs a minimally weak conflict for the basic variable basicVar.
+ *
+ * Returns a constraint that is now in conflict.
*/
- void minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, RaiseConflict& rc) const;
+ ConstraintCP minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, FarkasConflictBuilder& rc) const;
/**
- * Given a non-basic variable that is know to have a conflict on it,
+ * Given a basic variable that is know to have a conflict on it,
* construct and return a conflict.
* Follows section 4.2 in the CAV06 paper.
*/
- inline void generateConflictAboveUpperBound(ArithVar conflictVar, RaiseConflict& rc) const {
- minimallyWeakConflict(true, conflictVar, rc);
+ inline ConstraintCP generateConflictAboveUpperBound(ArithVar conflictVar, FarkasConflictBuilder& rc) const {
+ return minimallyWeakConflict(true, conflictVar, rc);
}
- inline void generateConflictBelowLowerBound(ArithVar conflictVar, RaiseConflict& rc) const {
- minimallyWeakConflict(false, conflictVar, rc);
+ inline ConstraintCP generateConflictBelowLowerBound(ArithVar conflictVar, FarkasConflictBuilder& rc) const {
+ return minimallyWeakConflict(false, conflictVar, rc);
}
/**
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index c5ad46dfc..fda34960a 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -211,6 +211,16 @@ Monomial Monomial::mkMonomial(const Constant& c, const VarList& vl) {
return Monomial(c, vl);
}
}
+
+Monomial Monomial::mkMonomial(const VarList& vl) {
+ // acts like Monomial::mkMonomial( 1, vl)
+ if( vl.empty() ) {
+ return Monomial::mkOne();
+ } else if(true){
+ return Monomial(vl);
+ }
+}
+
Monomial Monomial::parseMonomial(Node n) {
if(n.getKind() == kind::CONST_RATIONAL) {
return Monomial(Constant(n));
@@ -340,6 +350,17 @@ Polynomial Polynomial::operator+(const Polynomial& vl) const {
return result;
}
+Polynomial Polynomial::exactDivide(const Integer& z) const {
+ Assert(isIntegral());
+ if(z.isOne()){
+ return (*this);
+ }else {
+ Constant invz = Constant::mkConstant(Rational(1,z));
+ Polynomial prod = (*this) * Monomial::mkMonomial(invz);
+ Assert(prod.isIntegral());
+ return prod;
+ }
+}
Polynomial Polynomial::sumPolynomials(const std::vector<Polynomial>& ps){
if(ps.empty()){
@@ -368,11 +389,7 @@ Polynomial Polynomial::sumPolynomials(const std::vector<Polynomial>& ps){
Constant c = Constant::mkConstant((*ci).second);
Node n = (*ci).first;
VarList vl = VarList::parseVarList(n);
- if(vl.empty()){
- monos.push_back(Monomial(c));
- }else{
- monos.push_back(Monomial(c, vl));
- }
+ monos.push_back(Monomial::mkMonomial(c, vl));
}
}
Monomial::sort(monos);
@@ -1085,7 +1102,7 @@ Node Comparison::mkRatEquality(const Polynomial& p){
Constant coeffInv = -(minimalVList.getConstant().inverse());
Polynomial newRight = (p - minimalVList) * coeffInv;
- Polynomial newLeft(minimalVList.getVarList());
+ Polynomial newLeft(Monomial::mkMonomial(minimalVList.getVarList()));
return toNode(kind::EQUAL, newLeft, newRight);
}
@@ -1191,7 +1208,7 @@ Node Comparison::mkIntEquality(const Polynomial& p){
Monomial m = varPartMult.selectAbsMinimum();
bool mIsPositive = m.getConstant().isPositive();
- Polynomial noM = (varPartMult + (- m)) + Polynomial(constMult);
+ Polynomial noM = (varPartMult + (- m)) + Polynomial::mkPolynomial(constMult);
// m + noM = 0
Polynomial newRight = mIsPositive ? -noM : noM;
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index ac5ce10e5..97813338f 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -625,6 +625,7 @@ private:
};/* class VarList */
+/** Constructors have side conditions. Use the static mkMonomial functions instead. */
class Monomial : public NodeWrapper {
private:
Constant constant;
@@ -651,12 +652,10 @@ private:
n.getNumChildren() == 2;
}
-public:
-
Monomial(const Constant& c):
NodeWrapper(c.getNode()), constant(c), varList(VarList::mkEmptyVarList())
{ }
-
+
Monomial(const VarList& vl):
NodeWrapper(vl.getNode()), constant(Constant::mkConstant(1)), varList(vl)
{
@@ -672,12 +671,19 @@ public:
Assert(multStructured(getNode()));
}
-
+public:
static bool isMember(TNode n);
/** Makes a monomial with no restrictions on c and vl. */
static Monomial mkMonomial(const Constant& c, const VarList& vl);
+ /** If vl is empty, this make one. */
+ static Monomial mkMonomial(const VarList& vl);
+
+ static Monomial mkMonomial(const Constant& c){
+ return Monomial(c);
+ }
+
static Monomial mkMonomial(const Variable& v){
return Monomial(VarList(v));
}
@@ -692,7 +698,7 @@ public:
}
const Constant& getConstant() const { return constant; }
const VarList& getVarList() const { return varList; }
-
+
bool isConstant() const {
return varList.empty();
}
@@ -881,8 +887,12 @@ public:
Assert( Monomial::isStrictlySorted(m) );
}
+ static Polynomial mkPolynomial(const Constant& c){
+ return Polynomial(Monomial::mkMonomial(c));
+ }
+
static Polynomial mkPolynomial(const Variable& v){
- return Monomial::mkMonomial(v);
+ return Polynomial(Monomial::mkMonomial(v));
}
static Polynomial mkPolynomial(const std::vector<Monomial>& m) {
@@ -1016,13 +1026,8 @@ public:
*/
Integer gcd() const;
- Polynomial exactDivide(const Integer& z) const {
- Assert(isIntegral());
- Constant invz = Constant::mkConstant(Rational(1,z));
- Polynomial prod = (*this) * Monomial(invz);
- Assert(prod.isIntegral());
- return prod;
- }
+ /** z must divide all of the coefficients of the polynomial. */
+ Polynomial exactDivide(const Integer& z) const;
Polynomial operator+(const Polynomial& vl) const;
Polynomial operator-(const Polynomial& vl) const;
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index b37f24d14..49664e0ea 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -20,12 +20,14 @@
#include "theory/arith/options.h"
#include "theory/arith/constraint.h"
+
using namespace std;
namespace CVC4 {
namespace theory {
namespace arith {
+
SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
: d_conflictVariables()
, d_linEq(linEq)
@@ -34,14 +36,23 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq,
, d_errorSet(errors)
, d_numVariables(0)
, d_conflictChannel(conflictChannel)
+ , d_conflictBuilder(NULL)
, d_arithVarMalloc(tvmalloc)
, d_errorSize(0)
, d_zero(0)
+ , d_posOne(1)
+ , d_negOne(-1)
{
d_heuristicRule = options::arithErrorSelectionRule();
d_errorSet.setSelectionRule(d_heuristicRule);
+ d_conflictBuilder = new FarkasConflictBuilder();
}
+SimplexDecisionProcedure::~SimplexDecisionProcedure(){
+ delete d_conflictBuilder;
+}
+
+
bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat& conflicts) {
TimerStat::CodeTimer codeTimer(timer);
Assert( d_conflictVariables.empty() );
@@ -77,37 +88,34 @@ bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat&
void SimplexDecisionProcedure::reportConflict(ArithVar basic){
Assert(!d_conflictVariables.isMember(basic));
Assert(checkBasicForConflict(basic));
- RaiseConflict rc( d_conflictChannel);
- generateConflictForBasic(basic, rc);
+ ConstraintCP conflicted = generateConflictForBasic(basic);
+ Assert(conflicted != NullConstraint);
+ d_conflictChannel.raiseConflict(conflicted);
- // static bool verbose = false;
- // if(verbose) { Message() << "conflict " << basic << " " << conflict << endl; }
- // Assert(!conflict.isNull());
- //d_conflictChannel(conflict);
- rc.commitConflict();
d_conflictVariables.add(basic);
}
-void SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic, RaiseConflict& rc) const {
+ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic) const {
Assert(d_tableau.isBasic(basic));
Assert(checkBasicForConflict(basic));
if(d_variables.cmpAssignmentLowerBound(basic) < 0){
Assert(d_linEq.nonbasicsAtUpperBounds(basic));
- return d_linEq.generateConflictBelowLowerBound(basic, rc);
+ return d_linEq.generateConflictBelowLowerBound(basic, *d_conflictBuilder);
}else if(d_variables.cmpAssignmentUpperBound(basic) > 0){
Assert(d_linEq.nonbasicsAtLowerBounds(basic));
- return d_linEq.generateConflictAboveUpperBound(basic, rc);
+ return d_linEq.generateConflictAboveUpperBound(basic, *d_conflictBuilder);
}else{
Unreachable();
+ return NullConstraint;
}
}
bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const {
if(checkBasicForConflict(basic)){
- RaiseConflict rc(d_conflictChannel);
- generateConflictForBasic(basic, rc);
+ ConstraintCP conflicted = generateConflictForBasic(basic);
+ d_conflictChannel.raiseConflict(conflicted);
return true;
}else{
return false;
@@ -183,9 +191,12 @@ void SimplexDecisionProcedure::removeFromInfeasFunc(TimerStat& timer, ArithVar i
}
ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set){
+ Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction start" << endl;
+
TimerStat::CodeTimer codeTimer(timer);
Assert(!d_errorSet.focusEmpty());
-
+ Assert(debugIsASet(set));
+
ArithVar inf = requestVariable();
Assert(inf != ARITHVAR_SENTINEL);
@@ -199,8 +210,13 @@ ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& time
Assert(!d_variables.assignmentIsConsistent(e));
int sgn = d_errorSet.getSgn(e);
- coeffs.push_back(Rational(sgn));
+ Assert(sgn == -1 || sgn == 1);
+ const Rational& violatedCoeff = sgn < 0 ? d_negOne : d_posOne;
+ coeffs.push_back(violatedCoeff);
variables.push_back(e);
+
+ Debug("constructInfeasiblityFunction") << violatedCoeff << " " << e << endl;
+
}
d_tableau.addRow(inf, coeffs, variables);
DeltaRational newAssignment = d_linEq.computeRowValue(inf, false);
@@ -210,7 +226,7 @@ ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& time
d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf));
Debug("constructInfeasiblityFunction") << inf << " " << newAssignment << endl;
-
+ Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction done" << endl;
return inf;
}
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 91e6e4244..ada9b5efd 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -105,6 +105,9 @@ protected:
/** This is the call back channel for Simplex to report conflicts. */
RaiseConflict d_conflictChannel;
+ /** This is the call back channel for Simplex to report conflicts. */
+ FarkasConflictBuilder* d_conflictBuilder;
+
/** Used for requesting d_opt, bound and error variables for primal.*/
TempVarMalloc d_arithVarMalloc;
@@ -114,6 +117,12 @@ protected:
/** A local copy of 0. */
const Rational d_zero;
+ /** A local copy of 1. */
+ const Rational d_posOne;
+
+ /** A local copy of -1. */
+ const Rational d_negOne;
+
ArithVar constructInfeasiblityFunction(TimerStat& timer);
ArithVar constructInfeasiblityFunction(TimerStat& timer, ArithVar e);
ArithVar constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set);
@@ -126,6 +135,7 @@ protected:
public:
SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
+ ~SimplexDecisionProcedure();
/**
* Tries to update the assignments of variables such that all of the
@@ -166,7 +176,7 @@ protected:
* If a basic variable has a conflict on its row,
* this produces a minimized row on the conflict channel.
*/
- void generateConflictForBasic(ArithVar basic, RaiseConflict& rc) const;
+ ConstraintCP generateConflictForBasic(ArithVar basic) const;
/** Gets a fresh variable from TheoryArith. */
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 34f911b81..0d07c5ffc 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -634,12 +634,16 @@ unsigned SumOfInfeasibilitiesSPD::trySet(const ArithVarVec& set){
}
std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
+ Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets start" << endl;
+
std::vector< ArithVarVec > subsets;
Assert(d_soiVar == ARITHVAR_SENTINEL);
if(d_errorSize <= 2){
ArithVarVec inError;
d_errorSet.pushFocusInto(inError);
+
+ Assert(debugIsASet(inError));
subsets.push_back(inError);
return subsets;
}
@@ -653,9 +657,11 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
ArithVar e = *iter;
addRowSgns(sgns, e, d_errorSet.getSgn(e));
- //cout << "basic error var: " << e << endl;
- //d_tableau.debugPrintIsBasic(e);
- //d_tableau.printBasicRow(e, cout);
+ Debug("arith::greedyConflictSubsets") << "basic error var: " << e << endl;
+ if(Debug.isOn("arith::greedyConflictSubsets")){
+ d_tableau.debugPrintIsBasic(e);
+ d_tableau.printBasicRow(e, Debug("arith::greedyConflictSubsets"));
+ }
}
// Phase 1: Try to find at least 1 pair for every element
@@ -683,9 +689,10 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
tmp[0] = e;
tmp[1] = b;
if(trySet(tmp) == 2){
- //cout << "found a pair" << endl;
+ Debug("arith::greedyConflictSubsets") << "found a pair " << b << " " << e << endl;
hasParticipated.softAdd(b);
hasParticipated.softAdd(e);
+ Assert(debugIsASet(tmp));
subsets.push_back(tmp);
++(d_statistics.d_soiConflicts);
++(d_statistics.d_hasToBeMinimal);
@@ -704,13 +711,15 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
possibleStarts.pop_back();
if(hasParticipated.isMember(v)){ continue; }
+ hasParticipated.add(v);
+
Assert(d_soiVar == ARITHVAR_SENTINEL);
//d_soiVar's row = \sumofinfeasibilites underConstruction
ArithVarVec underConstruction;
underConstruction.push_back(v);
d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, v);
- //cout << "trying " << v << endl;
+ Debug("arith::greedyConflictSubsets") << "trying " << v << endl;
const Tableau::Entry* spoiler = NULL;
while( (spoiler = d_linEq.selectSlackEntry(d_soiVar, false)) != NULL){
@@ -718,16 +727,16 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
int oppositeSgn = -(spoiler->getCoefficient().sgn());
Assert(oppositeSgn != 0);
- //cout << "looking for " << nb << " " << oppositeSgn << endl;
+ Debug("arith::greedyConflictSubsets") << "looking for " << nb << " " << oppositeSgn << endl;
ArithVar basicWithOp = find_basic_in_sgns(sgns, nb, oppositeSgn, hasParticipated, false);
if(basicWithOp == ARITHVAR_SENTINEL){
- //cout << "search did not work for " << nb << endl;
+ Debug("arith::greedyConflictSubsets") << "search did not work for " << nb << endl;
// greedy construction has failed
break;
}else{
- //cout << "found " << basicWithOp << endl;
+ Debug("arith::greedyConflictSubsets") << "found " << basicWithOp << endl;
addToInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, basicWithOp);
hasParticipated.softAdd(basicWithOp);
@@ -735,8 +744,9 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
}
}
if(spoiler == NULL){
- //cout << "success" << endl;
+ Debug("arith::greedyConflictSubsets") << "success" << endl;
//then underConstruction contains a conflicting subset
+ Assert(debugIsASet(underConstruction));
subsets.push_back(underConstruction);
++d_statistics.d_soiConflicts;
if(underConstruction.size() == 3){
@@ -745,7 +755,7 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
++d_statistics.d_maybeNotMinimal;
}
}else{
- //cout << "failure" << endl;
+ Debug("arith::greedyConflictSubsets") << "failure" << endl;
}
tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
d_soiVar = ARITHVAR_SENTINEL;
@@ -762,52 +772,89 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
Assert(d_soiVar == ARITHVAR_SENTINEL);
+ Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets done" << endl;
return subsets;
}
-void SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
+bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
Assert(d_soiVar == ARITHVAR_SENTINEL);
d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, subset);
+ Assert(!subset.empty());
+ Assert(!d_conflictBuilder->underConstruction());
+
+ Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) start" << endl;
- //NodeBuilder<> conflict(kind::AND);
+ bool success = false;
+
for(ArithVarVec::const_iterator iter = subset.begin(), end = subset.end(); iter != end; ++iter){
ArithVar e = *iter;
ConstraintP violated = d_errorSet.getViolated(e);
- //cout << "basic error var: " << violated << endl;
- d_conflictChannel.addConstraint(violated);
- //violated->explainForConflict(conflict);
+ Assert(violated != NullConstraint);
- //d_tableau.debugPrintIsBasic(e);
- //d_tableau.printBasicRow(e, cout);
- }
- for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){
- const Tableau::Entry& entry = *i;
- ArithVar v = entry.getColVar();
- if(v == d_soiVar){ continue; }
- const Rational& coeff = entry.getCoefficient();
- ConstraintP c = (coeff.sgn() > 0) ?
- d_variables.getUpperBoundConstraint(v) :
- d_variables.getLowerBoundConstraint(v);
+ int sgn = d_errorSet.getSgn(e);
+ const Rational& violatedCoeff = sgn > 0 ? d_negOne : d_posOne;
+ Debug("arith::generateSOIConflict") << "basic error var: "
+ << "(" << violatedCoeff << ")"
+ << " " << violated
+ << endl;
- //cout << "nb : " << c << endl;
- d_conflictChannel.addConstraint(c);
+
+ d_conflictBuilder->addConstraint(violated, violatedCoeff);
+ Assert(violated->hasProof());
+ if(!success && !violated->negationHasProof()){
+ success = true;
+ d_conflictBuilder->makeLastConsequent();
+ }
+ }
+
+ if(!success){
+ // failure
+ d_conflictBuilder->reset();
+ } else {
+ // pick a violated constraint arbitrarily. any of them may be selected for the conflict
+ Assert(d_conflictBuilder->underConstruction());
+ Assert(d_conflictBuilder->consequentIsSet());
+
+ for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){
+ const Tableau::Entry& entry = *i;
+ ArithVar v = entry.getColVar();
+ if(v == d_soiVar){ continue; }
+ const Rational& coeff = entry.getCoefficient();
+
+ ConstraintP c = (coeff.sgn() > 0) ?
+ d_variables.getUpperBoundConstraint(v) :
+ d_variables.getLowerBoundConstraint(v);
+
+ Debug("arith::generateSOIConflict") << "non-basic var: "
+ << "(" << coeff << ")"
+ << " " << c
+ << endl;
+ d_conflictBuilder->addConstraint(c, coeff);
+ }
+ ConstraintCP conflicted = d_conflictBuilder->commitConflict();
+ d_conflictChannel.raiseConflict(conflicted);
}
- //Node conf = conflict;
tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
d_soiVar = ARITHVAR_SENTINEL;
- d_conflictChannel.commitConflict();
- //return conf;
+ Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) done" << endl;
+ Assert(d_soiVar == ARITHVAR_SENTINEL);
+ Assert(!d_conflictBuilder->underConstruction());
+ return success;
}
WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
static int instance = 0;
instance++;
- //cout << "SOI conflict " << instance << ": |E| = " << d_errorSize << endl;
- //d_errorSet.debugPrint(cout);
- //cout << endl;
+
+ Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() start "
+ << instance << ": |E| = " << d_errorSize << endl;
+ if(Debug.isOn("arith::SOIConflict")){
+ d_errorSet.debugPrint(cout);
+ }
+ Debug("arith::SOIConflict") << endl;
tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
d_soiVar = ARITHVAR_SENTINEL;
@@ -815,24 +862,22 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
if(options::soiQuickExplain()){
quickExplain();
generateSOIConflict(d_qeConflict);
- //Node conflict = generateSOIConflict(d_qeConflict);
- //cout << conflict << endl;
- //d_conflictChannel(conflict);
}else{
-
vector<ArithVarVec> subsets = greedyConflictSubsets();
Assert( d_soiVar == ARITHVAR_SENTINEL);
-
+ bool anySuccess = false;
Assert(!subsets.empty());
for(vector<ArithVarVec>::const_iterator i = subsets.begin(), end = subsets.end(); i != end; ++i){
const ArithVarVec& subset = *i;
- generateSOIConflict(subset);
+ Assert(debugIsASet(subset));
+ anySuccess = generateSOIConflict(subset) || anySuccess;
//Node conflict = generateSOIConflict(subset);
//cout << conflict << endl;
//reportConflict(conf); do not do this. We need a custom explanations!
//d_conflictChannel(conflict);
}
+ Assert(anySuccess);
}
Assert( d_soiVar == ARITHVAR_SENTINEL);
d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization);
@@ -840,7 +885,8 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
//reportConflict(conf); do not do this. We need a custom explanations!
d_conflictVariables.add(d_soiVar);
- //cout << "SOI conflict " << instance << "end" << endl;
+ Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() done "
+ << instance << "end" << endl;
return ConflictFound;
}
@@ -877,7 +923,6 @@ WitnessImprovement SumOfInfeasibilitiesSPD::soiRound() {
}
bool SumOfInfeasibilitiesSPD::debugSOI(WitnessImprovement w, ostream& out, int instance) const{
-//#warning "Redo SOI"
return true;
// out << "DLV("<<instance<<") ";
// switch(w){
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index d9f6e9707..6dd6373d4 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -171,7 +171,7 @@ private:
WitnessImprovement soiRound();
WitnessImprovement SOIConflict();
std::vector< ArithVarVec > greedyConflictSubsets();
- void generateSOIConflict(const ArithVarVec& subset);
+ bool generateSOIConflict(const ArithVarVec& subset);
// WitnessImprovement focusUsingSignDisagreements(ArithVar basic);
// WitnessImprovement focusDownToLastHalf();
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index ea0bec095..231eb1562 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -95,14 +95,12 @@ void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCa
cb.multiplyRow(rid, -a_rs_sgn);
}
-
-
void Tableau::addRow(ArithVar basic,
const std::vector<Rational>& coefficients,
const std::vector<ArithVar>& variables)
{
Assert(basic < getNumColumns());
-
+ Assert(debugIsASet(variables));
Assert(coefficients.size() == variables.size() );
Assert(!isBasic(basic));
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c8e7991a5..2cf313fc2 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -99,8 +99,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
d_containing(containing),
d_nlIncomplete( false),
d_rowTracking(),
- d_conflictBuffer(),
- d_constraintDatabase(c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this, d_conflictBuffer)),
+ d_constraintDatabase(c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this)),
d_qflraStatus(Result::SAT_UNKNOWN),
d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
@@ -122,15 +121,14 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
d_tableauResetDensity(1.6),
d_tableauResetPeriod(10),
d_conflicts(c),
-
d_blackBoxConflict(c, Node::null()),
- d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseConflict(*this, d_conflictBuffer)),
+ d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseEqualityEngineConflict(*this)),
d_cmEnabled(c, true),
- d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
- d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
- d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
- d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
+ d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+ d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+ d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+ d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
d_pass1SDP(NULL),
d_otherSDP(NULL),
@@ -540,6 +538,17 @@ bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap){
return true;
}
+void TheoryArithPrivate::raiseConflict(ConstraintCP a){
+ Assert(a->inConflict());
+ d_conflicts.push_back(a);
+}
+
+void TheoryArithPrivate::raiseBlackBoxConflict(Node bb){
+ if(d_blackBoxConflict.get().isNull()){
+ d_blackBoxConflict = bb;
+ }
+}
+
void TheoryArithPrivate::revertOutOfConflict(){
d_partialModel.revertAssignmentChanges();
clearUpdates();
@@ -550,20 +559,20 @@ void TheoryArithPrivate::clearUpdates(){
d_updatedBounds.purge();
}
-void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b){
- ConstraintCPVec v;
- v.push_back(a);
- v.push_back(b);
- d_conflicts.push_back(v);
-}
+// void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b){
+// ConstraintCPVec v;
+// v.push_back(a);
+// v.push_back(b);
+// d_conflicts.push_back(v);
+// }
-void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c){
- ConstraintCPVec v;
- v.push_back(a);
- v.push_back(b);
- v.push_back(c);
- d_conflicts.push_back(v);
-}
+// void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c){
+// ConstraintCPVec v;
+// v.push_back(a);
+// v.push_back(b);
+// v.push_back(c);
+// d_conflicts.push_back(v);
+// }
void TheoryArithPrivate::zeroDifferenceDetected(ArithVar x){
if(d_cmEnabled){
@@ -613,6 +622,9 @@ bool TheoryArithPrivate::getDioCuttingResource(){
bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
Assert(constraint != NullConstraint);
Assert(constraint->isLowerBound());
+ Assert(constraint->isTrue());
+ Assert(!constraint->negationHasProof());
+
ArithVar x_i = constraint->getVariable();
const DeltaRational& c_i = constraint->getValue();
@@ -629,17 +641,17 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
if(cmpToUB > 0){ // c_i < \lowerbound(x_i)
ConstraintP ubc = d_partialModel.getUpperBoundConstraint(x_i);
- raiseConflict(ubc, constraint);
+ ConstraintP negation = constraint->getNegation();
+ negation->impliedByUnate(ubc, true);
+
+ raiseConflict(constraint);
- // Node conflict = ConstraintValue::explainConflict(ubc, constraint);
- // Debug("arith") << "AssertLower conflict " << conflict << endl;
- // raiseConflict(conflict);
++(d_statistics.d_statAssertLowerConflicts);
return true;
}else if(cmpToUB == 0){
if(isInteger(x_i)){
d_constantIntegerVariables.push_back(x_i);
- Debug("dio::push") << x_i << endl;
+ Debug("dio::push") << "dio::push " << x_i << endl;
}
ConstraintP ub = d_partialModel.getUpperBoundConstraint(x_i);
@@ -653,26 +665,28 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
}
const ValueCollection& vc = constraint->getValueCollection();
- if(vc.hasDisequality()){
- Assert(vc.hasEquality());
+ if(vc.hasEquality()){
+
+ Assert(vc.hasDisequality());
ConstraintP eq = vc.getEquality();
ConstraintP diseq = vc.getDisequality();
- if(diseq->isTrue()){
- //const ConstraintP ub = vc.getUpperBound();
- raiseConflict(diseq, ub, constraint);
- //Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
-
+ // x <= b, x >= b |= x = b
+ // (x > b or x < b or x = b)
+ Debug("arith::eq") << "lb == ub, propagate eq" << eq << endl;
+ bool triConflict = diseq->isTrue();
+
+ if(!eq->isTrue()){
+ eq->impliedByTrichotomy(constraint, ub, triConflict);
+ eq->tryToPropagate();
+ }
+ if(triConflict){
++(d_statistics.d_statDisequalityConflicts);
- //Debug("eq") << " assert lower conflict " << conflict << endl;
- //raiseConflict(conflict);
+ raiseConflict(eq);
return true;
- }else if(!eq->isTrue()){
- Debug("eq") << "lb == ub, propagate eq" << eq << endl;
- eq->impliedBy(constraint, d_partialModel.getUpperBoundConstraint(x_i));
- // do not need to add to d_learnedBounds
}
}
}else{
+ // l <= x <= u and l < u
Assert(cmpToUB < 0);
const ValueCollection& vc = constraint->getValueCollection();
@@ -680,17 +694,20 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
const ConstraintP diseq = vc.getDisequality();
if(diseq->isTrue()){
const ConstraintP ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
-
- if(ub->hasProof()){
- raiseConflict(diseq, ub, constraint);
+ ConstraintP negUb = ub->getNegation();
+
+ // l <= x, l != x |= l < x
+ // |= not (l >= x)
+ bool ubInConflict = ub->hasProof();
+ bool learnNegUb = !(negUb->hasProof());
+ if(learnNegUb){
+ negUb->impliedByTrichotomy(constraint, diseq, ubInConflict);
+ negUb->tryToPropagate();
+ }
+ if(ubInConflict){
+ raiseConflict(ub);
return true;
- // Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
- // Debug("eq") << " assert upper conflict " << conflict << endl;
- // raiseConflict(conflict);
- // return true;
- }else if(!ub->negationHasProof()){
- ConstraintP negUb = ub->getNegation();
- negUb->impliedBy(constraint, diseq);
+ }else if(learnNegUb){
d_learnedBounds.push_back(negUb);
}
}
@@ -740,13 +757,16 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
/* procedure AssertUpper( x_i <= c_i) */
bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
+ Assert(constraint != NullConstraint);
+ Assert(constraint->isUpperBound());
+ Assert(constraint->isTrue());
+ Assert(!constraint->negationHasProof());
+
ArithVar x_i = constraint->getVariable();
const DeltaRational& c_i = constraint->getValue();
Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
- AssertArgument(constraint != NullConstraint,
- "AssertUpper() called on a NullConstraint.");
- Assert(constraint->isUpperBound());
+
//Too strong because of rounding with integers
//Assert(!constraint->hasLiteral() || original == constraint->getLiteral());
@@ -757,22 +777,25 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
return false; //sat
}
-
+
// cmpToLb = \lowerbound(x_i).cmp(c_i)
int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
if( cmpToLB < 0 ){ // \upperbound(x_i) < \lowerbound(x_i)
+ // l_i <= x_i and c_i < l_i |= c_i < x_i
+ // or ... |= not (x_i <= c_i)
ConstraintP lbc = d_partialModel.getLowerBoundConstraint(x_i);
- raiseConflict(lbc, constraint);
- //Node conflict = ConstraintValue::explainConflict(lbc, constraint);
- //Debug("arith") << "AssertUpper conflict " << conflict << endl;
+ ConstraintP negConstraint = constraint->getNegation();
+ negConstraint->impliedByUnate(lbc, true);
+ raiseConflict(constraint);
++(d_statistics.d_statAssertUpperConflicts);
- //raiseConflict(conflict);
return true;
}else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
if(isInteger(x_i)){
d_constantIntegerVariables.push_back(x_i);
- Debug("dio::push") << x_i << endl;
+ Debug("dio::push") << "dio::push " << x_i << endl;
}
+
+ const ValueCollection& vc = constraint->getValueCollection();
ConstraintP lb = d_partialModel.getLowerBoundConstraint(x_i);
if(d_cmEnabled){
if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
@@ -783,39 +806,47 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
}
}
- const ValueCollection& vc = constraint->getValueCollection();
if(vc.hasDisequality()){
- Assert(vc.hasEquality());
- const ConstraintP diseq = vc.getDisequality();
- const ConstraintP eq = vc.getEquality();
- if(diseq->isTrue()){
- raiseConflict(diseq, lb, constraint);
- //Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
- //Debug("eq") << " assert upper conflict " << conflict << endl;
- //raiseConflict(conflict);
- return true;
- }else if(!eq->isTrue()){
- Debug("eq") << "lb == ub, propagate eq" << eq << endl;
- eq->impliedBy(constraint, d_partialModel.getLowerBoundConstraint(x_i));
- //do not bother to add to d_learnedBounds
+ Assert(vc.hasDisequality());
+ ConstraintP eq = vc.getEquality();
+ ConstraintP diseq = vc.getDisequality();
+ // x <= b, x >= b |= x = b
+ // (x > b or x < b or x = b)
+ Debug("arith::eq") << "lb == ub, propagate eq" << eq << endl;
+ bool triConflict = diseq->isTrue();
+ if(!eq->isTrue()){
+ eq->impliedByTrichotomy(constraint, lb, triConflict);
+ eq->tryToPropagate();
}
+ if(triConflict){
+ ++(d_statistics.d_statDisequalityConflicts);
+ raiseConflict(eq);
+ return true;
+ }
}
}else if(cmpToLB > 0){
+ // l <= x <= u and l < u
+ Assert(cmpToLB > 0);
const ValueCollection& vc = constraint->getValueCollection();
+
if(vc.hasDisequality()){
const ConstraintP diseq = vc.getDisequality();
if(diseq->isTrue()){
- const ConstraintP lb =
- d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
- if(lb->hasProof()){
- raiseConflict(diseq, lb, constraint);
- //Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
- //Debug("eq") << " assert upper conflict " << conflict << endl;
- //raiseConflict(conflict);
+ const ConstraintP lb = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
+ ConstraintP negLb = lb->getNegation();
+
+ // x <= u, u != x |= u < x
+ // |= not (u >= x)
+ bool lbInConflict = lb->hasProof();
+ bool learnNegLb = !(negLb->hasProof());
+ if(learnNegLb){
+ negLb->impliedByTrichotomy(constraint, diseq, lbInConflict);
+ negLb->tryToPropagate();
+ }
+ if(lbInConflict){
+ raiseConflict(lb);
return true;
- }else if(!lb->negationHasProof()){
- ConstraintP negLb = lb->getNegation();
- negLb->impliedBy(constraint, diseq);
+ }else if(learnNegLb){
d_learnedBounds.push_back(negLb);
}
}
@@ -867,8 +898,10 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
/* procedure AssertEquality( x_i == c_i ) */
bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){
- AssertArgument(constraint != NullConstraint,
- "AssertUpper() called on a NullConstraint.");
+ Assert(constraint != NullConstraint);
+ Assert(constraint->isEquality());
+ Assert(constraint->isTrue());
+ Assert(!constraint->negationHasProof());
ArithVar x_i = constraint->getVariable();
const DeltaRational& c_i = constraint->getValue();
@@ -887,22 +920,13 @@ bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){
return false; //sat
}
- if(cmpToUB > 0){
- ConstraintP ubc = d_partialModel.getUpperBoundConstraint(x_i);
- raiseConflict(ubc, constraint);
- //Node conflict = ConstraintValue::explainConflict(ubc, constraint);
- //Debug("arith") << "AssertEquality conflicts with upper bound " << conflict << endl;
- //raiseConflict(conflict);
- return true;
- }
-
- if(cmpToLB < 0){
- ConstraintP lbc = d_partialModel.getLowerBoundConstraint(x_i);
- raiseConflict(lbc, constraint);
-
- // Node conflict = ConstraintValue::explainConflict(lbc, constraint);
- // Debug("arith") << "AssertEquality conflicts with lower bound" << conflict << endl;
- // raiseConflict(conflict);
+ if(cmpToUB > 0 || cmpToLB < 0){
+ ConstraintP cb = (cmpToUB > 0) ? d_partialModel.getUpperBoundConstraint(x_i) :
+ d_partialModel.getLowerBoundConstraint(x_i);
+ ConstraintP diseq = constraint->getNegation();
+ Assert(!diseq->isTrue());
+ diseq->impliedByUnate(cb, true);
+ raiseConflict(constraint);
return true;
}
@@ -913,7 +937,7 @@ bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){
if(isInteger(x_i)){
d_constantIntegerVariables.push_back(x_i);
- Debug("dio::push") << x_i << endl;
+ Debug("dio::push") << "dio::push " << x_i << endl;
}
// Don't bother to check whether x_i != c_i is in d_diseq
@@ -967,12 +991,13 @@ bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){
/* procedure AssertDisequality( x_i != c_i ) */
bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
+ Assert(constraint != NullConstraint);
+ Assert(constraint->isDisequality());
+ Assert(constraint->isTrue());
+ Assert(!constraint->negationHasProof());
- AssertArgument(constraint != NullConstraint,
- "AssertUpper() called on a NullConstraint.");
ArithVar x_i = constraint->getVariable();
const DeltaRational& c_i = constraint->getValue();
-
Debug("arith") << "AssertDisequality(" << x_i << " " << c_i << ")"<< std::endl;
//Should be fine in integers
@@ -992,12 +1017,11 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
const ConstraintP lb = vc.getLowerBound();
const ConstraintP ub = vc.getUpperBound();
if(lb->isTrue() && ub->isTrue()){
+ ConstraintP eq = constraint->getNegation();
+ eq->impliedByTrichotomy(lb, ub, true);
+ raiseConflict(constraint);
//in conflict
- Debug("eq") << "explaining" << endl;
++(d_statistics.d_statDisequalityConflicts);
- raiseConflict(constraint, lb, ub);
- //Node conflict = ConstraintValue::explainConflict(constraint, lb, ub);
- //raiseConflict(conflict);
return true;
}
}
@@ -1005,10 +1029,12 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
const ConstraintP lb = vc.getLowerBound();
if(lb->isTrue()){
const ConstraintP ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
- Debug("eq") << "propagate UpperBound " << constraint << lb << ub << endl;
+ Assert(!ub->isTrue());
+ Debug("arith::eq") << "propagate UpperBound " << constraint << lb << ub << endl;
const ConstraintP negUb = ub->getNegation();
if(!negUb->isTrue()){
- negUb->impliedBy(constraint, lb);
+ negUb->impliedByTrichotomy(constraint, lb, false);
+ negUb->tryToPropagate();
d_learnedBounds.push_back(negUb);
}
}
@@ -1017,11 +1043,13 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
const ConstraintP ub = vc.getUpperBound();
if(ub->isTrue()){
const ConstraintP lb = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
+ Assert(!lb->isTrue());
- Debug("eq") << "propagate LowerBound " << constraint << lb << ub << endl;
+ Debug("arith::eq") << "propagate LowerBound " << constraint << lb << ub << endl;
const ConstraintP negLb = lb->getNegation();
if(!negLb->isTrue()){
- negLb->impliedBy(constraint, ub);
+ negLb->impliedByTrichotomy(constraint, ub, false);
+ negLb->tryToPropagate();
d_learnedBounds.push_back(negLb);
}
}
@@ -1030,19 +1058,19 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
bool split = constraint->isSplit();
if(!split && c_i == d_partialModel.getAssignment(x_i)){
- Debug("eq") << "lemma now! " << constraint << endl;
+ Debug("arith::eq") << "lemma now! " << constraint << endl;
outputLemma(constraint->split());
return false;
}else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
- Debug("eq") << "can drop as less than lb" << constraint << endl;
+ Debug("arith::eq") << "can drop as less than lb" << constraint << endl;
}else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i)){
- Debug("eq") << "can drop as less than ub" << constraint << endl;
+ Debug("arith::eq") << "can drop as less than ub" << constraint << endl;
}else if(!split){
- Debug("eq") << "push back" << constraint << endl;
+ Debug("arith::eq") << "push back" << constraint << endl;
d_diseqQueue.push(constraint);
d_partialModel.invalidateDelta();
}else{
- Debug("eq") << "skipping already split " << constraint << endl;
+ Debug("arith::eq") << "skipping already split " << constraint << endl;
}
return false;
}
@@ -1748,7 +1776,7 @@ Comparison TheoryArithPrivate::mkIntegerEqualityFromAssignment(ArithVar v){
const DeltaRational& beta = d_partialModel.getAssignment(v);
Assert(beta.isIntegral());
- Polynomial betaAsPolynomial( Constant::mkConstant(beta.floor()) );
+ Polynomial betaAsPolynomial = Polynomial::mkPolynomial( Constant::mkConstant(beta.floor()) );
TNode var = d_partialModel.asNode(v);
Polynomial varAsPolynomial = Polynomial::parsePolynomial(var);
@@ -1768,7 +1796,7 @@ Node TheoryArithPrivate::dioCutting(){
// If the bounds are equal this is already in the dioSolver
//Add v = dr as a speculation.
Comparison eq = mkIntegerEqualityFromAssignment(v);
- Debug("dio::push") <<v << " " << eq.getNode() << endl;
+ Debug("dio::push") << "dio::push " << v << " " << eq.getNode() << endl;
Assert(!eq.isBoolean());
d_diosolver.pushInputConstraint(eq, eq.getNode());
// It does not matter what the explanation of eq is.
@@ -1783,7 +1811,7 @@ Node TheoryArithPrivate::dioCutting(){
return Node::null();
}else{
Polynomial p = plane.getPolynomial();
- Polynomial c(plane.getConstant() * Constant::mkConstant(-1));
+ Polynomial c = Polynomial::mkPolynomial(plane.getConstant() * Constant::mkConstant(-1));
Integer gcd = p.gcd();
Assert(p.isIntegral());
Assert(c.isIntegral());
@@ -1808,7 +1836,7 @@ Node TheoryArithPrivate::callDioSolver(){
ArithVar v = d_constantIntegerVariables.front();
d_constantIntegerVariables.pop();
- Debug("arith::dio") << v << endl;
+ Debug("arith::dio") << "callDioSolver " << v << endl;
Assert(isInteger(v));
Assert(d_partialModel.boundsAreEqual(v));
@@ -1823,7 +1851,7 @@ Node TheoryArithPrivate::callDioSolver(){
}else if(ub->isEquality()){
orig = ub->externalExplainByAssertions();
}else {
- orig = Constraint_::externalExplainByAssertions(ub, lb);
+ orig = Constraint::externalExplainByAssertions(ub, lb);
}
Assert(d_partialModel.assignmentIsConsistent(v));
@@ -1838,7 +1866,7 @@ Node TheoryArithPrivate::callDioSolver(){
Assert(orig.getKind() != EQUAL);
return orig;
}else{
- Debug("dio::push") << v << " " << eq.getNode() << " with reason " << orig << endl;
+ Debug("dio::push") << "dio::push " << v << " " << eq.getNode() << " with reason " << orig << endl;
d_diosolver.pushInputConstraint(eq, orig);
}
}
@@ -1863,7 +1891,7 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){
// if is (not true), or false
Assert((reEq.getConst<bool>() && isDistinct) ||
(!reEq.getConst<bool>() && !isDistinct));
- blackBoxConflict(assertion);
+ raiseBlackBoxConflict(assertion);
}
return NullConstraint;
}
@@ -1883,49 +1911,43 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){
Assert(constraint != NullConstraint);
- if(constraint->negationHasProof()){
+ if(constraint->assertedToTheTheory()){
+ //Do nothing
+ return NullConstraint;
+ }
+ Assert(!constraint->assertedToTheTheory());
+ bool inConflict = constraint->negationHasProof();
+ constraint->setAssertedToTheTheory(assertion, inConflict);
+
+ if(!constraint->hasProof()){
+ Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
+ constraint->setAssumption(inConflict);
+ } else {
+ Debug("arith::constraint") << "already has proof: " << constraint->externalExplainByAssertions() << endl;
+ }
+
+
+ if(Debug.isOn("arith::negatedassumption") && inConflict){
ConstraintP negation = constraint->getNegation();
- if(negation->isSelfExplaining()){
- if(Debug.isOn("whytheoryenginewhy")){
- debugPrintFacts();
- }
+ if(Debug.isOn("arith::negatedassumption") && negation->isAssumption()){
+ debugPrintFacts();
}
+ Debug("arith::eq") << "negation has proof" << endl;
Debug("arith::eq") << constraint << endl;
Debug("arith::eq") << negation << endl;
-
- constraint->setAssertedToTheTheoryWithNegationTrue(assertion);
- if(!constraint->hasProof()){
- Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
- constraint->selfExplainingWithNegationTrue();
- }else{
- Debug("arith::constraint") << "already has proof: " << constraint->externalExplainByAssertions() << endl;
- }
-
- raiseConflict(constraint, negation);
- // NodeBuilder<> nb(kind::AND);
- // nb << assertion;
- // negation->explainForConflict(nb);
- // Node conflict = nb;
- // Debug("arith::eq") << "conflict" << conflict << endl;
- // raiseConflict(conflict);
- return NullConstraint;
}
- Assert(!constraint->negationHasProof());
- if(constraint->assertedToTheTheory()){
- //Do nothing
+ if(inConflict){
+ ConstraintP negation = constraint->getNegation();
+ if(Debug.isOn("arith::negatedassumption") && negation->isAssumption()){
+ debugPrintFacts();
+ }
+ Debug("arith::eq") << "negation has proof" << endl;
+ Debug("arith::eq") << constraint << endl;
+ Debug("arith::eq") << negation << endl;
+ raiseConflict(negation);
return NullConstraint;
}else{
- Debug("arith::constraint") << "arith constraint " << constraint << std::endl;
- constraint->setAssertedToTheTheory(assertion);
-
- if(!constraint->hasProof()){
- Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
- constraint->selfExplaining();
- }else{
- Debug("arith::constraint") << "already has proof: " << constraint->externalExplainByAssertions() << endl;
- }
-
return constraint;
}
}
@@ -1941,14 +1963,12 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
if(isInteger(x_i) && constraint->isStrictUpperBound()){
ConstraintP floorConstraint = constraint->getFloor();
if(!floorConstraint->isTrue()){
- if(floorConstraint->negationHasProof()){
- raiseConflict(constraint, floorConstraint->getNegation());
- //Node conf = Constraint_::explainConflict(constraint, floorConstraint->getNegation());
- //raiseConflict(conf);
+ bool inConflict = floorConstraint->negationHasProof();
+ floorConstraint->impliedByIntHole(constraint, inConflict);
+ floorConstraint->tryToPropagate();
+ if(inConflict){
+ raiseConflict(floorConstraint);
return true;
- }else{
- floorConstraint->impliedBy(constraint);
- // Do not need to add to d_learnedBounds
}
}
return AssertUpper(floorConstraint);
@@ -1959,14 +1979,13 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
if(isInteger(x_i) && constraint->isStrictLowerBound()){
ConstraintP ceilingConstraint = constraint->getCeiling();
if(!ceilingConstraint->isTrue()){
- if(ceilingConstraint->negationHasProof()){
- raiseConflict(constraint, ceilingConstraint->getNegation());
- //Node conf = Constraint_::explainConflict(constraint, ceilingConstraint->getNegation());
- //raiseConflict(conf);
+ bool inConflict = ceilingConstraint->negationHasProof();
+ ceilingConstraint->impliedByIntHole(constraint, inConflict);
+ ceilingConstraint->tryToPropagate();
+ if(inConflict){
+ raiseConflict(ceilingConstraint);
return true;
}
- ceilingConstraint->impliedBy(constraint);
- // Do not need to add to learnedBounds
}
return AssertLower(ceilingConstraint);
}else{
@@ -2027,21 +2046,75 @@ bool TheoryArithPrivate::hasIntegerModel(){
}
}
+
+Node flattenAndSort(Node n){
+ Kind k = n.getKind();
+ switch(k){
+ case kind::OR:
+ case kind::AND:
+ case kind::PLUS:
+ case kind::MULT:
+ break;
+ default:
+ return n;
+ }
+
+ std::vector<Node> out;
+ std::vector<Node> process;
+ process.push_back(n);
+ while(!process.empty()){
+ Node b = process.back();
+ process.pop_back();
+ if(b.getKind() == k){
+ for(Node::iterator i=b.begin(), end=b.end(); i!=end; ++i){
+ process.push_back(*i);
+ }
+ } else {
+ out.push_back(b);
+ }
+ }
+ Assert(out.size() >= 2);
+ std::sort(out.begin(), out.end());
+ return NodeManager::currentNM()->mkNode(k, out);
+}
+
+
+
/** Outputs conflicts to the output channel. */
void TheoryArithPrivate::outputConflicts(){
Assert(anyConflict());
+ static unsigned int conflicts = 0;
+
if(!conflictQueueEmpty()){
Assert(!d_conflicts.empty());
for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
- const ConstraintCPVec& vec = d_conflicts[i];
- Node conflict = Constraint_::externalExplainByAssertions(vec);
- Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl;
+ ConstraintCP confConstraint = d_conflicts[i];
+ Assert(confConstraint->inConflict());
+ Node conflict = confConstraint->externalExplainConflict();
+
+ ++conflicts;
+ Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict
+ // << "("<<conflicts<<")"
+ << endl;
+ if(Debug.isOn("arith::normalize::external")){
+ conflict = flattenAndSort(conflict);
+ Debug("arith::conflict") << "(normalized to) " << conflict << endl;
+ }
+
(d_containing.d_out)->conflict(conflict);
}
}
if(!d_blackBoxConflict.get().isNull()){
Node bb = d_blackBoxConflict.get();
- Debug("arith::conflict") << "black box conflict" << bb << endl;
+ ++conflicts;
+ Debug("arith::conflict") << "black box conflict" << bb
+ //<< "("<<conflicts<<")"
+ << endl;
+ if(Debug.isOn("arith::normalize::external")){
+ bb = flattenAndSort(bb);
+ Debug("arith::conflict") << "(normalized to) " << bb << endl;
+ }
+
(d_containing.d_out)->conflict(bb);
}
}
@@ -2134,13 +2207,36 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){
turnOffApproxFor(options::replayNumericFailurePenalty());
}
- for(size_t i =0, N = res.size(); i < N; ++i){
- raiseConflict(res[i]);
- }
+
+
if(res.empty()){
++d_statistics.d_replayAttemptFailed;
}else{
- ++d_statistics.d_mipProofsSuccessful;
+ unsigned successes = 0;
+ for(size_t i =0, N = res.size(); i < N; ++i){
+ ConstraintCPVec& vec = res[i];
+ Assert(vec.size() >= 2);
+ for(size_t j=0, M = vec.size(); j < M; ++j){
+ ConstraintCP at_j = vec[j];
+ Assert(at_j->isTrue());
+ if(!at_j->negationHasProof()){
+ successes++;
+ vec[j] = vec.back();
+ vec.pop_back();
+ ConstraintP neg_at_j = at_j->getNegation();
+
+ Debug("approx::replayLog") << "Setting the proof for the replayLog conflict on:" << endl
+ << " (" << neg_at_j->isTrue() <<") " << neg_at_j << endl
+ << " (" << at_j->isTrue() <<") " << at_j << endl;
+ neg_at_j->impliedByIntHole(vec, true);
+ raiseConflict(at_j);
+ break;
+ }
+ }
+ }
+ if(successes > 0){
+ ++d_statistics.d_mipProofsSuccessful;
+ }
}
if(d_currentPropagationList.size() > enteringPropN){
@@ -2260,6 +2356,25 @@ Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){
return safeConstructNary(nb);
}
+ConstraintCP TheoryArithPrivate::vectorToIntHoleConflict(const ConstraintCPVec& conflict){
+ Assert(conflict.size() >= 2);
+ ConstraintCPVec exp(conflict.begin(), conflict.end()-1);
+ ConstraintCP back = conflict.back();
+ ConstraintP negBack = back->getNegation();
+ negBack->impliedByIntHole(exp, true);
+ return back;
+}
+
+void TheoryArithPrivate::intHoleConflictToVector(ConstraintCP conflicting, ConstraintCPVec& conflict){
+ ConstraintCP negConflicting = conflicting->getNegation();
+ Assert(conflicting->hasProof());
+ Assert(negConflicting->hasProof());
+
+ conflict.push_back(conflicting);
+ conflict.push_back(negConflicting);
+
+ Constraint::assertionFringe(conflict);
+}
void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, BranchCutInfo& bci){
Assert(conflictQueueEmpty());
@@ -2298,9 +2413,23 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
d_partialModel.startQueueingBoundCounts();
}
for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){
- conflicts.push_back(d_conflicts[i]);
- // remove the floor/ceiling contraint implied by bcneg
- Constraint_::assertionFringe(conflicts.back());
+
+ conflicts.push_back(ConstraintCPVec());
+ intHoleConflictToVector(d_conflicts[i], conflicts.back());
+ Constraint::assertionFringe(conflicts.back());
+
+ // ConstraintCP conflicting = d_conflicts[i];
+ // ConstraintCP negConflicting = conflicting->getNegation();
+ // Assert(conflicting->hasProof());
+ // Assert(negConflicting->hasProof());
+
+ // conflicts.push_back(ConstraintCPVec());
+ // ConstraintCPVec& back = conflicts.back();
+ // back.push_back(conflicting);
+ // back.push_back(negConflicting);
+
+ // // remove the floor/ceiling contraint implied by bcneg
+ // Constraint::assertionFringe(back);
}
if(Debug.isOn("approx::branch")){
@@ -2317,7 +2446,8 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
// make sure to be working on the assertion fringe!
if(!contains(conf, bcneg)){
Debug("approx::branch") << "reraise " << conf << endl;
- raiseConflict(conf);
+ ConstraintCP conflicting = vectorToIntHoleConflict(conf);
+ raiseConflict(conflicting);
}else if(!bci.proven()){
drop(conf, bcneg);
bci.setExplanation(conf);
@@ -2328,87 +2458,24 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
void TheoryArithPrivate::replayAssert(ConstraintP c) {
if(!c->assertedToTheTheory()){
- if(c->negationHasProof()){
- ConstraintP neg = c->getNegation();
- raiseConflict(c, neg);
- Debug("approx::replayAssert") << "replayAssertion conflict " << neg << " : " << c << endl;
- }else if(!c->hasProof()){
- c->setInternalDecision();
- assertionCases(c);
+ bool inConflict = c->negationHasProof();
+ if(!c->hasProof()){
+ c->setInternalAssumption(inConflict);
Debug("approx::replayAssert") << "replayAssert " << c << " set internal" << endl;
}else{
- assertionCases(c);
Debug("approx::replayAssert") << "replayAssert " << c << " has explanation" << endl;
}
+ Debug("approx::replayAssert") << "replayAssertion " << c << endl;
+ if(inConflict){
+ raiseConflict(c);
+ }else{
+ assertionCases(c);
+ }
}else{
- Debug("approx::replayAssert") << "replayAssert " << c << " already asserted" << endl;
+ Debug("approx::replayAssert") << "replayAssert " << c << " already asserted" << endl;
}
}
-// ConstraintCPVec TheoryArithPrivate::toExplanation(Node n) const {
-// ConstraintCPVec res;
-// cout << "toExplanation" << endl;
-// if(n.getKind() == kind::AND){
-// for(unsigned i = 0; i < n.getNumChildren(); ++i){
-// ConstraintP c = d_constraintDatabase.lookup(n[i]);
-// if(c == NullConstraint){ return std::vector<Constraint>(); }
-// res.push_back(c);
-// cout << "\t"<<c << endl;
-// }
-// }else{
-// ConstraintP c = d_constraintDatabase.lookup(n);
-// if(c == NullConstraint){ return std::vector<Constraint>(); }
-// res.push_back(c);
-// }
-// return res;
-// }
-
-// void TheoryArithPrivate::enqueueConstraints(std::vector<Constraint>& out, Node n) const{
-// if(n.getKind() == kind::AND){
-// for(unsigned i = 0, N = n.getNumChildren(); i < N; ++i){
-// enqueueConstraints(out, n[i]);
-// }
-// }else{
-// ConstraintP c = d_constraintDatabase.lookup(n);
-// if(c == NullConstraint){
-// cout << "failing on " << n << endl;
-// }
-// Assert(c != NullConstraint);
-// out.push_back(c);
-// }
-// }
-
-// ConstraintCPVec TheoryArithPrivate::resolveOutPropagated(const ConstraintCPVec& v, const std::set<ConstraintCP>& propagated) const {
-// cout << "resolveOutPropagated()" << conf << endl;
-// std::set<ConstraintCP> final;
-// std::set<ConstraintCP> processed;
-// std::vector<ConstraintCP> to_process;
-// enqueueConstraints(to_process, conf);
-// while(!to_process.empty()){
-// ConstraintP c = to_process.back(); to_process.pop_back();
-// if(processed.find(c) != processed.end()){
-// continue;
-// }else{
-// if(propagated.find(c) == propagated.end()){
-// final.insert(c);
-// }else{
-// Node exp = c->explainForPropagation();
-// enqueueConstraints(to_process, exp);
-// }
-// processed.insert(c);
-// }
-// }
-// cout << "final size: " << final.size() << std::endl;
-// NodeBuilder<> nb(kind::AND);
-// std::set<Constraint>::const_iterator iter = final.begin(), end = final.end();
-// for(; iter != end; ++iter){
-// ConstraintP c = *iter;
-// c->explainForConflict(nb);
-// }
-// Node newConf = safeConstructNary(nb);
-// cout << "resolveOutPropagated("<<conf<<", ...) ->" << newConf << endl;
-// return newConf;
-// }
void TheoryArithPrivate::resolveOutPropagated(std::vector<ConstraintCPVec>& confs, const std::set<ConstraintCP>& propagated) const {
Debug("arith::resolveOutPropagated")
@@ -2416,7 +2483,7 @@ void TheoryArithPrivate::resolveOutPropagated(std::vector<ConstraintCPVec>& conf
for(size_t i =0, N = confs.size(); i < N; ++i){
ConstraintCPVec& conf = confs[i];
size_t orig = conf.size();
- Constraint_::assertionFringe(conf);
+ Constraint::assertionFringe(conf);
Debug("arith::resolveOutPropagated")
<< " conf["<<i<<"] " << orig << " to " << conf.size() << endl;
}
@@ -2541,7 +2608,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
if(con->isTrue()){
Debug("approx::replayLogRec") << "not asserted?" << endl;
}else{
- con->impliedBy(exp);
+ con->impliedByIntHole(exp, false);
replayAssert(con);
Debug("approx::replayLogRec") << "cut prop" << endl;
}
@@ -2580,7 +2647,8 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
if(!conflictQueueEmpty()){
/* if a conflict has been found stop */
for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){
- res.push_back(d_conflicts[i]);
+ res.push_back(ConstraintCPVec());
+ intHoleConflictToVector(d_conflicts[i], res.back());
}
++d_statistics.d_replayLogRecEarlyExit;
}else if(nl.isBranch()){
@@ -2818,7 +2886,7 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
Node cutConstraint = cutToLiteral(approx, *cut);
if(!cutConstraint.isNull()){
const ConstraintCPVec& exp = cut->getExplanation();
- Node asLemma = Constraint_::externalExplainByAssertions(exp);
+ Node asLemma = Constraint::externalExplainByAssertions(exp);
Node implied = Rewriter::rewrite(cutConstraint);
anythingnew = anythingnew || !isSatLiteral(implied);
@@ -3113,9 +3181,20 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
bool useApprox = options::useApprox() && ApproximateSimplex::enabled() && getSolveIntegerResource();
+ Debug("TheoryArithPrivate::solveRealRelaxation")
+ << "solveRealRelaxation() approx"
+ << " " << options::useApprox()
+ << " " << ApproximateSimplex::enabled()
+ << " " << useApprox
+ << " " << safeToCallApprox()
+ << endl;
+
bool noPivotLimitPass1 = noPivotLimit && !useApprox;
d_qflraStatus = simplex.findModel(noPivotLimitPass1);
+ Debug("TheoryArithPrivate::solveRealRelaxation")
+ << "solveRealRelaxation()" << " pass1 " << d_qflraStatus << endl;
+
if(d_qflraStatus == Result::SAT_UNKNOWN && useApprox && safeToCallApprox()){
// pass2: fancy-final
static const int32_t relaxationLimit = 10000;
@@ -3484,21 +3563,15 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
break;
case Result::UNSAT:
d_unknownsInARow = 0;
- if(false && previous == Result::SAT){
- ++d_statistics.d_revertsOnConflicts;
- Debug("arith::bt") << "clearing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl;
- revertOutOfConflict();
- d_errorSet.clear();
- }else{
- ++d_statistics.d_commitsOnConflicts;
- Debug("arith::bt") << "committing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl;
- d_partialModel.commitAssignmentChanges();
- revertOutOfConflict();
+ ++d_statistics.d_commitsOnConflicts;
- if(Debug.isOn("arith::consistency::comitonconflict")){
- entireStateIsConsistent("commit on conflict");
- }
+ Debug("arith::bt") << "committing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl;
+ d_partialModel.commitAssignmentChanges();
+ revertOutOfConflict();
+
+ if(Debug.isOn("arith::consistency::comitonconflict")){
+ entireStateIsConsistent("commit on conflict");
}
outputConflicts();
emmittedConflictOrSplit = true;
@@ -3623,7 +3696,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
if(possibleConflict != Node::null()){
revertOutOfConflict();
Debug("arith::conflict") << "dio conflict " << possibleConflict << endl;
- blackBoxConflict(possibleConflict);
+ raiseBlackBoxConflict(possibleConflict);
outputConflicts();
emmittedConflictOrSplit = true;
}
@@ -3768,9 +3841,9 @@ bool TheoryArithPrivate::splitDisequalities(){
d_diseqQueue.pop();
if(front->isSplit()){
- Debug("eq") << "split already" << endl;
+ Debug("arith::eq") << "split already" << endl;
}else{
- Debug("eq") << "not split already" << endl;
+ Debug("arith::eq") << "not split already" << endl;
ArithVar lhsVar = front->getVariable();
@@ -3788,11 +3861,11 @@ bool TheoryArithPrivate::splitDisequalities(){
//cout << "Now " << Rewriter::rewrite(lemma) << endl;
splitSomething = true;
}else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){
- Debug("eq") << "can drop as less than lb" << front << endl;
+ Debug("arith::eq") << "can drop as less than lb" << front << endl;
}else if(d_partialModel.strictlyGreaterThanUpperBound(lhsVar, rhsValue)){
- Debug("eq") << "can drop as greater than ub" << front << endl;
+ Debug("arith::eq") << "can drop as greater than ub" << front << endl;
}else{
- Debug("eq") << "save" << front << ": " <<lhsValue << " != " << rhsValue << endl;
+ Debug("arith::eq") << "save" << front << ": " <<lhsValue << " != " << rhsValue << endl;
save.push_back(front);
}
}
@@ -3852,13 +3925,13 @@ Node TheoryArithPrivate::explain(TNode n) {
ConstraintP c = d_constraintDatabase.lookup(n);
if(c != NullConstraint){
- Assert(!c->isSelfExplaining());
+ Assert(!c->isAssumption());
Node exp = c->externalExplainForPropagation();
Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl;
return exp;
}else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){
c = d_assertionsThatDoNotMatchTheirLiterals[n];
- if(!c->isSelfExplaining()){
+ if(!c->isAssumption()){
Node exp = c->externalExplainForPropagation();
Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
return exp;
@@ -3930,7 +4003,7 @@ void TheoryArithPrivate::propagate(Theory::Effort e) {
normalized[0] : normalized.notNode();
Node lp = flattenAnd(exp.andNode(notNormalized));
Debug("arith::prop") << "propagate conflict" << lp << endl;
- blackBoxConflict(lp);
+ raiseBlackBoxConflict(lp);
outputConflicts();
return;
}else{
@@ -4562,6 +4635,7 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b
ConstraintP implied = d_constraintDatabase.getBestImpliedBound(v, t, bound);
if(implied != NullConstraint){
+
return rowImplicationCanBeApplied(ridx, rowUp, implied);
}
}
@@ -4606,21 +4680,22 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
<< " " << hasProof
<< endl;
- if(implied->negationHasProof()){
- Warning() << "the negation of " << implied << " : " << endl
- << "has proof " << implied->getNegation() << endl
- << implied->getNegation()->externalExplainByAssertions() << endl;
- }
- if(!assertedToTheTheory && canBePropagated && !hasProof ){
+ if( !assertedToTheTheory && canBePropagated && !hasProof ){
ConstraintCPVec explain;
- d_linEq.propagateRow(explain, ridx, rowUp, implied);
+
+ PROOF(d_farkasBuffer.clear());
+ RationalVectorP coeffs = NULLPROOF(&d_farkasBuffer);
+
+ d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs);
if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
Node implication = implied->externalImplication(explain);
Node clause = flattenImplication(implication);
outputLemma(clause);
}else{
- implied->impliedBy(explain);
+ Assert(!implied->negationHasProof());
+ implied->impliedByFarkas(explain, coeffs, false);
+ implied->tryToPropagate();
}
return true;
}
@@ -4636,8 +4711,8 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
double fRand(double fMin, double fMax)
{
- double f = (double)rand() / RAND_MAX;
- return fMin + f * (fMax - fMin);
+ double f = (double)rand() / RAND_MAX;
+ return fMin + f * (fMax - fMin);
}
bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index ff89945b8..4c539c60d 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -119,8 +119,6 @@ private:
BoundInfoMap d_rowTracking;
- ConstraintCPVec d_conflictBuffer;
-
/**
* The constraint database associated with the theory.
* This must be declared before ArithPartialModel.
@@ -327,21 +325,27 @@ private:
/** This is only used by simplex at the moment. */
- context::CDList<ConstraintCPVec> d_conflicts;
+ context::CDList<ConstraintCP> d_conflicts;
+
+ /** This is only used by simplex at the moment. */
context::CDO<Node> d_blackBoxConflict;
public:
- inline void raiseConflict(const ConstraintCPVec& cv){
- d_conflicts.push_back(cv);
- }
- void raiseConflict(ConstraintCP a, ConstraintCP b);
- void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c);
+ /**
+ * This adds the constraint a to the queue of conflicts in d_conflicts.
+ * Both a and ~a must have a proof.
+ */
+ void raiseConflict(ConstraintCP a);
- inline void blackBoxConflict(Node bb){
- if(d_blackBoxConflict.get().isNull()){
- d_blackBoxConflict = bb;
- }
- }
+ // inline void raiseConflict(const ConstraintCPVec& cv){
+ // d_conflicts.push_back(cv);
+ // }
+
+ // void raiseConflict(ConstraintCP a, ConstraintCP b);
+ // void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c);
+
+ /** This is a conflict that is magically known to hold. */
+ void raiseBlackBoxConflict(Node bb);
private:
@@ -356,7 +360,7 @@ private:
/**
* Outputs the contents of d_conflicts onto d_out.
- * Must be inConflict().
+ * The conditions of anyConflict() must hold.
*/
void outputConflicts();
@@ -717,8 +721,10 @@ private:
std::pair<ConstraintP, ArithVar> replayGetConstraint(const DenseMap<Rational>& lhs, Kind k, const Rational& rhs, bool branch);
void replayAssert(ConstraintP c);
- //ConstConstraintVec toExplanation(Node n) const;
+ static ConstraintCP vectorToIntHoleConflict(const ConstraintCPVec& conflict);
+ static void intHoleConflictToVector(ConstraintCP conflicting, ConstraintCPVec& conflict);
+
// Returns true if the node contains a literal
// that is an arithmetic literal and is not a sat literal
// No caching is done so this should likely only
@@ -730,6 +736,8 @@ private:
uint32_t d_solveIntMaybeHelp, d_solveIntAttempts;
+ RationalVector d_farkasBuffer;
+
/** These fields are designed to be accessible to TheoryArith methods. */
class Statistics {
public:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback