From 88ce3a56088e4f3f509b565944ef8c6d36545423 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 30 Apr 2013 19:32:08 -0400 Subject: [PATCH] Making propagation more conversative. --- src/theory/arith/theory_arith_private.cpp | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) 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){ -- 2.30.2