diff options
author | Tim King <taking@cs.nyu.edu> | 2013-04-30 19:32:08 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-04-30 19:32:08 -0400 |
commit | 88ce3a56088e4f3f509b565944ef8c6d36545423 (patch) | |
tree | 5bc4e8c19a7a51aeb98bebd951be9bd2e03949f6 | |
parent | d833d5790a38dc62d8a4714a13253253767c377e (diff) |
Making propagation more conversative.
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 5b40e03bc..c71f2a6bd 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2662,7 +2662,16 @@ bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{ ConstraintType t = ub ? UpperBound : LowerBound; const DeltaRational& a = d_partialModel.getAssignment(v); - return NullConstraint != d_constraintDatabase.getBestImpliedBound(v, t, a); + Constraint strongestPossible = d_constraintDatabase.getBestImpliedBound(v, t, a); + if(strongestPossible == NullConstraint){ + return false; + }else{ + bool assertedToTheTheory = strongestPossible->assertedToTheTheory(); + bool canBePropagated = strongestPossible->canBePropagated(); + bool hasProof = strongestPossible->hasProof(); + + return !assertedToTheTheory && canBePropagated && !hasProof; + } }else{ return false; } @@ -2800,6 +2809,10 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){ ++instance; cout << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl; + if(rowLength >= options::arithPropagateMaxLength()){ + return false; + } + if(hasCount.lowerBoundCount() == rowLength){ success |= attemptFull(ridx, false); }else if(hasCount.lowerBoundCount() + 1 == rowLength){ |