diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-03 22:07:38 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-03 22:07:38 +0000 |
| commit | c5000befcf95c03a42a2f73a40c3dac6dc3492be (patch) | |
| tree | 4a87ace04da1c62d1474673d485843d820e5cbd8 /src/smt | |
| parent | 40253236078988fecc3becd2619dd5ccad5e3077 (diff) | |
user push/pop support in minisat and simplification; also bindings work
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 42b21b79a..f80d9a135 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -574,14 +574,17 @@ void SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "applying substitutions" << endl; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << std::endl; d_assertionsToPreprocess[i] = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])); + Trace("simplify") << " got " << d_assertionsToPreprocess[i] << std::endl; } // Assert all the assertions to the propagator Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "asserting to propagator" << endl; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << std::endl; d_propagator.assert(d_assertionsToPreprocess[i]); } @@ -591,6 +594,7 @@ void SmtEnginePrivate::nonClausalSimplify() { // If in conflict, just return false Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "conflict in non-clausal propagation" << endl; + d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); return; } else { @@ -610,6 +614,7 @@ void SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "conflict with " << d_nonClausalLearnedLiterals[i] << endl; + d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); return; } @@ -625,6 +630,7 @@ void SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "conflict while solving " << learnedLiteral << endl; + d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); return; case Theory::SOLVE_STATUS_SOLVED: |