diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-07 16:25:15 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-07 16:25:15 +0000 |
commit | 62a50760346e130345b24e8a14ad0dac0dca5d38 (patch) | |
tree | 5b4bfd8a6576321a1b08c08920df6e4a4a0d2cc9 /src/theory/uf/theory_uf.h | |
parent | 9d9731007a17375aa242f15faace8c451cf3c258 (diff) |
fixes for uf/equality engine from the quantifiers branch. mainly backtracking issues.
Diffstat (limited to 'src/theory/uf/theory_uf.h')
-rw-r--r-- | src/theory/uf/theory_uf.h | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 1f4c2372f..a3871f3a2 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -37,7 +37,6 @@ namespace theory { namespace uf { class TheoryUF : public Theory { - public: class NotifyClass { @@ -80,7 +79,11 @@ private: void explain(TNode literal, std::vector<TNode>& assumptions); /** Literals to propagate */ - std::vector<TNode> d_literalsToPropagate; + context::CDList<TNode> d_literalsToPropagate; + + /** Index of the next literal to propagate */ + context::CDO<unsigned> d_literalsToPropagateIndex; + /** True node for predicates = true */ Node d_true; @@ -99,7 +102,9 @@ public: d_notify(*this), d_equalityEngine(d_notify, ctxt, "theory::uf::TheoryUF"), d_knownFacts(ctxt), - d_conflict(ctxt, false) + d_conflict(ctxt, false), + d_literalsToPropagate(ctxt), + d_literalsToPropagateIndex(ctxt, 0) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); |