diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-11-16 21:11:11 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-11-16 21:11:11 +0000 |
| commit | bb2a0e0e12f39a1b4dea8fb0c990decba4708a1c (patch) | |
| tree | 6e5824f8cf1b0f1cb32e6cae5cbd214b1b48d965 /src/prop | |
| parent | e66924cb0f425ca70969058532340e68c9c17a54 (diff) | |
Added Theory::presolve().
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/prop_engine.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index ab1afceba..4939ecb43 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -118,6 +118,9 @@ Result PropEngine::checkSat() { ScopedBool scopedBool(d_inCheckSat); d_inCheckSat = true; + // TODO This currently ignores conflicts (a dangerous practice). + d_theoryEngine->presolve(); + // Check the problem bool result = d_satSolver->solve(); |