diff options
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 431c82476..ebc131b60 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -160,11 +160,26 @@ private: Comparison mkIntegerEqualityFromAssignment(ArithVar v); /** - * List of all of the inequalities asserted in the current context. + * List of all of the disequalities asserted in the current context that are not known + * to be satisfied. */ - //context::CDHashSet<Node, NodeHashFunction> d_diseq; context::CDQueue<Constraint> d_diseqQueue; + /** + * Constraints that have yet to be processed by proagation work list. + * All of the elements have type of LowerBound, UpperBound, or + * Equality. + * + * This is empty at the beginning of every check call. + * + * If head()->getType() == LowerBound or UpperBound, + * then d_cPL[1] is the previous constraint in d_partialModel for the + * corresponding bound. + * If head()->getType() == Equality, + * then d_cPL[1] is the previous lowerBound in d_partialModel, + * and d_cPL[2] is the previous upperBound in d_partialModel. + */ + std::deque<Constraint> d_currentPropagationList; /** * Manages information about the assignment and upper and lower bounds on @@ -380,7 +395,9 @@ private: DenseSet d_candidateBasics; bool hasAnyUpdates() { return !d_updatedBounds.empty(); } - void clearUpdates(){ d_updatedBounds.purge(); } + void clearUpdates(); + + void revertOutOfConflict(); void propagateCandidates(); void propagateCandidate(ArithVar basic); @@ -445,6 +462,8 @@ private: TimerStat d_presolveTime; + TimerStat d_newPropTime; + IntStat d_externalBranchAndBounds; IntStat d_initialTableauSize; |