diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
commit | 25e9c72dd689d3b621b901220794c652a3ba589a (patch) | |
tree | 58b14dd3818f3e7a8ca3311a0457716e7753a95e /src/smt | |
parent | 587520ce888b88294fb9e4ca476e2425d8bf026e (diff) |
merge from symmetry branch
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d85f28b23..fe5628dd0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -669,6 +669,18 @@ void SmtEnginePrivate::processAssertions() { // Simplify the assertions simplifyAssertions(); + if(Options::current()->preprocessOnly) { + if(Message.isOn()) { + // Push the formula to the Message() stream + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + expr::ExprSetDepth::Scope sdScope(Message.getStream(), -1); + Message() << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())) << endl; + } + } + // We still call into SAT below so that we can output theory + // contributions that come from presolve(). + } + // Push the formula to SAT for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); |