diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-19 01:37:55 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-19 01:37:55 +0000 |
commit | 663a6edef6b65d400e2d97dc9c8276da3d3cb0b1 (patch) | |
tree | 29c7782beaf37ea855b9bc9436d61e94f60c9393 /src/prop | |
parent | c21ad20770c41ece116c182d97e0ef824e7b26f4 (diff) |
Merge from ufprop branch, including:
* Theory::staticLearning() for statically adding new T-stuff before
normal preprocessing. UF's staticLearning() does transitivity of
equality/iff, solving the diamonds.
* more aggressive T-propagation for UF
* new KEEP_STATISTIC macro to hide Theories from having to
register/deregister statistics (and also has the advantage of
keeping the statistic type, field name, and the 'tag' used to output
the statistic in the same place---instead of scattered in the theory
definition and constructor initializer list. See documentation for
KEEP_STATISTIC in src/util/stats.h for more of an explanation).
* more statistics for UF
* restart notifications from SAT (through TheoryEngine) via
Theory::notifyRestart()
* StackingMap and UnionFind unit tests
* build fixes/adjustments
* code cleanup; minor other improvements
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 3 | ||||
-rw-r--r-- | src/prop/sat.cpp | 4 | ||||
-rw-r--r-- | src/prop/sat.h | 2 |
3 files changed, 9 insertions, 0 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 4817ec1f5..18ed9b5da 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -986,6 +986,9 @@ lbool Solver::search(int nof_conflicts) // Reached bound on number of conflicts: progress_estimate = progressEstimate(); cancelUntil(0); + // [mdeters] notify theory engine of restarts for deferred + // theory processing + proxy->notifyRestart(); return l_Undef; } // Simplify the set of problem clauses: diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 97c5d1419..b78f20ee8 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -102,5 +102,9 @@ TNode SatSolver::getNode(SatLiteral lit) { return d_cnfStream->getNode(lit); } +void SatSolver::notifyRestart() { + d_theoryEngine->notifyRestart(); +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/sat.h b/src/prop/sat.h index 6e244d9d7..cc81ea5c6 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -247,6 +247,8 @@ public: TNode getNode(SatLiteral lit); + void notifyRestart(); + };/* class SatSolver */ /* Functions that delegate to the concrete SAT solver. */ |