diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-12-12 09:47:37 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-12-12 09:47:37 +0000 |
commit | 6d04f19e1c1fbf7714fbb95dc62648ac44b419dd (patch) | |
tree | 7f5486f7b4a88323708f693b5905afb6375d8ca3 /src/prop/minisat | |
parent | 933a1ea506fd553e756be942087ef82154b6f959 (diff) |
* merging some uf stuff from incremental_work branch that somehow nobody merged-in
* since two theories can propagate the same literal minisat now explicitly checks that a propagated literal has not been asserted yet
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 8a883b1cb..e1a8ded8e 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -698,9 +698,18 @@ CRef Solver::propagate(TheoryCheckType type) void Solver::propagateTheory() { std::vector<Lit> propagatedLiterals; proxy->theoryPropagate(propagatedLiterals); + int oldTrailSize = trail.size(); for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) { Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl; - uncheckedEnqueue(propagatedLiterals[i], CRef_Lazy); + // multiple theories can propagate the same literal + Lit p = propagatedLiterals[i]; + if (value(p) == l_Undef) { + uncheckedEnqueue(p, CRef_Lazy); + } else { + // but we check that this is the case and that they agree + Assert(trail_index(var(p)) >= oldTrailSize); + Assert(value(p) == lbool(!sign(p))); + } } } |