summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/constraint.cpp22
-rw-r--r--src/theory/arith/constraint.h2
-rw-r--r--src/theory/arith/linear_equality.cpp7
-rw-r--r--src/theory/arith/linear_equality.h2
-rw-r--r--src/theory/arith/options3
-rw-r--r--src/theory/arith/theory_arith_private.cpp101
6 files changed, 104 insertions, 33 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index e26687bf1..78b9d3494 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -922,6 +922,28 @@ bool ConstraintValue::proofIsEmpty() const{
return result;
}
+Node ConstraintValue::makeImplication(const std::vector<Constraint>& b) const{
+ Node antecedent = makeConjunction(b);
+ Node implied = getLiteral();
+ return antecedent.impNode(implied);
+}
+
+
+Node ConstraintValue::makeConjunction(const std::vector<Constraint>& b){
+ NodeBuilder<> nb(kind::AND);
+ for(vector<Constraint>::const_iterator i = b.begin(), end = b.end(); i != end; ++i){
+ Constraint b_i = *i;
+ b_i->explainBefore(nb, AssertionOrderSentinel);
+ }
+ if(nb.getNumChildren() >= 2){
+ return nb;
+ }else if(nb.getNumChildren() == 1){
+ return nb[0];
+ }else{
+ return mkBoolNode(true);
+ }
+}
+
void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) const{
Assert(hasProof());
Assert(!isSelfExplaining() || assertedToTheTheory());
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index a5d64a652..4966115d2 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -598,6 +598,8 @@ public:
void impliedBy(Constraint a, Constraint b);
void impliedBy(const std::vector<Constraint>& b);
+ Node makeImplication(const std::vector<Constraint>& b) const;
+ static Node makeConjunction(const std::vector<Constraint>& b);
/** The node must have a proof already and be eligible for propagation! */
void propagate();
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 4779b1012..bde771102 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -581,7 +581,7 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
<< basic << ") done" << endl;
}
-void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c){
+void LinearEqualityModule::propagateRow(vector<Constraint>& into, RowIndex ridx, bool rowUp, Constraint c){
Assert(!c->assertedToTheTheory());
Assert(c->canBePropagated());
Assert(!c->hasProof());
@@ -589,7 +589,7 @@ void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c)
ArithVar v = c->getVariable();
Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
<< v <<") start" << endl;
- vector<Constraint> bounds;
+ //vector<Constraint> bounds;
Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
for(; !iter.atEnd(); ++iter){
@@ -608,9 +608,8 @@ void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c)
Assert(bound != NullConstraint);
Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
- bounds.push_back(bound);
+ into.push_back(bound);
}
- c->impliedBy(bounds);
Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
<< v << ") done" << endl;
}
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 767c09340..b1f3d00d7 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -431,7 +431,7 @@ public:
* Exports either the explanation of an upperbound or a lower bound
* of the basic variable basic, using the non-basic variables in the row.
*/
- void propagateRow(RowIndex ridx, bool rowUp, Constraint c);
+ void propagateRow(std::vector<Constraint>& into, RowIndex ridx, bool rowUp, Constraint c);
/**
* Computes the value of a basic variable using the assignments
diff --git a/src/theory/arith/options b/src/theory/arith/options
index cf0782a92..1366addae 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -94,4 +94,7 @@ option exportDioDecompositions --dio-decomps bool :default false :read-write
option newProp --new-prop bool :default false :read-write
Use the new row propagation system
+option arithPropAsLemmaLength --arith-prop-clauses int :default 8 :read-write
+ Rows shorter than this are propagated as clauses
+
endmodule
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c71f2a6bd..31b6cd032 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -116,6 +116,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
d_cutInContext(c),
d_statistics()
{
+ srand(79);
}
TheoryArithPrivate::~TheoryArithPrivate(){ }
@@ -2548,18 +2549,21 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound
}
// I think this can be skipped if canBePropagated is true
//d_learnedBounds.push(bestImplied);
- cout << "success " << bestImplied << endl;
- d_partialModel.printModel(basic, cout);
-
+ if(Debug.isOn("arith::prop")){
+ Debug("arith::prop") << "success " << bestImplied << endl;
+ d_partialModel.printModel(basic, Debug("arith::prop"));
+ }
return true;
}
- cout << "failed " << basic << " " << bound << assertedToTheTheory << " " <<
- canBePropagated << " " << hasProof << endl;
- d_partialModel.printModel(basic, cout);
+ if(Debug.isOn("arith::prop")){
+ Debug("arith::prop") << "failed " << basic << " " << bound << assertedToTheTheory << " " <<
+ canBePropagated << " " << hasProof << endl;
+ d_partialModel.printModel(basic, Debug("arith::prop"));
+ }
}
- }else{
- cout << "false " << bound << " ";
- d_partialModel.printModel(basic, cout);
+ }else if(Debug.isOn("arith::prop")){
+ Debug("arith::prop") << "false " << bound << " ";
+ d_partialModel.printModel(basic, Debug("arith::prop"));
}
return false;
}
@@ -2580,7 +2584,7 @@ void TheoryArithPrivate::propagateCandidate(ArithVar basic){
void TheoryArithPrivate::propagateCandidates(){
TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
- cout << "propagateCandidates begin" << endl;
+ Debug("arith::prop") << "propagateCandidates begin" << endl;
Assert(d_candidateBasics.empty());
@@ -2615,7 +2619,7 @@ void TheoryArithPrivate::propagateCandidates(){
Assert(d_tableau.isBasic(candidate));
propagateCandidate(candidate);
}
- cout << "propagateCandidates end" << endl << endl << endl;
+ Debug("arith::prop") << "propagateCandidates end" << endl << endl << endl;
}
void TheoryArithPrivate::propagateCandidatesNew(){
@@ -2634,7 +2638,7 @@ void TheoryArithPrivate::propagateCandidatesNew(){
*/
TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
- cout << "propagateCandidatesNew begin" << endl;
+ Debug("arith::prop") << "propagateCandidatesNew begin" << endl;
Assert(d_qflraStatus == Result::SAT);
if(d_updatedBounds.empty()){ return; }
@@ -2651,7 +2655,7 @@ void TheoryArithPrivate::propagateCandidatesNew(){
d_candidateRows.pop_back();
propagateCandidateRow(candidate);
}
- cout << "propagateCandidatesNew end" << endl << endl << endl;
+ Debug("arith::prop") << "propagateCandidatesNew end" << endl << endl << endl;
}
bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{
@@ -2678,7 +2682,7 @@ bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{
}
bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){
- cout << " attemptSingleton" << ridx;
+ Debug("arith::prop") << " attemptSingleton" << ridx;
const Tableau::Entry* ep;
ep = d_linEq.rowLacksBound(ridx, rowUp, ARITHVAR_SENTINEL);
@@ -2698,8 +2702,8 @@ bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){
// if c < 0, v \geq -D/c so !vUp
bool vUp = (rowUp == ( coeff.sgn() < 0));
- cout << " " << rowUp << " " << v << " " << coeff << " " << vUp << endl;
- cout << " " << propagateMightSucceed(v, vUp) << endl;
+ Debug("arith::prop") << " " << rowUp << " " << v << " " << coeff << " " << vUp << endl;
+ Debug("arith::prop") << " " << propagateMightSucceed(v, vUp) << endl;
if(propagateMightSucceed(v, vUp)){
DeltaRational dr = d_linEq.computeRowBound(ridx, rowUp, v);
@@ -2710,7 +2714,7 @@ bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){
}
bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){
- cout << " attemptFull" << ridx << endl;
+ Debug("arith::prop") << " attemptFull" << ridx << endl;
vector<const Tableau::Entry*> candidates;
@@ -2746,11 +2750,6 @@ bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){
DeltaRational impliedBound = (slack - contribution)/(-c);
bool success = tryToPropagate(ridx, rowUp, v, vUb, impliedBound);
- if(success){
- cout << " success " << v << endl;
- }else{
- cout << " fail " << v << endl;
- }
any |= success;
}
return any;
@@ -2770,6 +2769,30 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b
return false;
}
+Node flattenImplication(Node imp){
+ NodeBuilder<> nb(kind::OR);
+ Node left = imp[0];
+ Node right = imp[1];
+
+ if(left.getKind() == kind::AND){
+ for(Node::iterator i = left.begin(), iend = left.end(); i != iend; ++i) {
+ nb << (*i).negate();
+ }
+ }else{
+ nb << left.negate();
+ }
+
+ if(right.getKind() == kind::OR){
+ for(Node::iterator i = right.begin(), iend = right.end(); i != iend; ++i) {
+ nb << *i;
+ }
+ }else{
+ nb << right;
+ }
+
+ return nb;
+}
+
bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, Constraint implied){
Assert(implied != NullConstraint);
ArithVar v = implied->getVariable();
@@ -2791,15 +2814,33 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
}
if(!assertedToTheTheory && canBePropagated && !hasProof ){
- d_linEq.propagateRow(ridx, rowUp, implied);
+ vector<Constraint> explain;
+ d_linEq.propagateRow(explain, ridx, rowUp, implied);
+ if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
+ Node implication = implied->makeImplication(explain);
+ Node clause = flattenImplication(implication);
+ outputLemma(clause);
+ }else{
+ implied->impliedBy(explain);
+ }
return true;
}
- cout << "failed " << v << " " << assertedToTheTheory << " " <<
- canBePropagated << " " << hasProof << " " << implied << endl;
- d_partialModel.printModel(v, cout);
+
+ if(Debug.isOn("arith::prop")){
+ Debug("arith::prop")
+ << "failed " << v << " " << assertedToTheTheory << " "
+ << canBePropagated << " " << hasProof << " " << implied << endl;
+ d_partialModel.printModel(v, Debug("arith::prop"));
+ }
return false;
}
+double fRand(double fMin, double fMax)
+{
+ double f = (double)rand() / RAND_MAX;
+ return fMin + f * (fMax - fMin);
+}
+
bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
BoundCounts hasCount = d_linEq.hasBoundCount(ridx);
uint32_t rowLength = d_tableau.getRowLength(ridx);
@@ -2807,10 +2848,14 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
bool success = false;
static int instance = 0;
++instance;
- cout << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl;
+
+ Debug("arith::prop")
+ << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl;
if(rowLength >= options::arithPropagateMaxLength()){
- return false;
+ if(fRand(0.0,1.0) >= double(options::arithPropagateMaxLength())/rowLength){
+ return false;
+ }
}
if(hasCount.lowerBoundCount() == rowLength){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback