diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-10 20:27:00 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-10 20:27:00 +0000 |
| commit | 5ab69fcdf91fb3034bf9e25f515b551124d4e747 (patch) | |
| tree | 2136f2e2ba5d876930bb99e205bd71ebd0604a81 | |
| parent | 3544ad31b067fe6c54fcd34c058646852ef8d605 (diff) | |
Removing rewriter call in SmtEngine::addFormula().
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e308db269..ee0d9debc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1900,6 +1900,8 @@ void SmtEnginePrivate::processAssertions() { return; } + // Assertions are NOT guaranteed to be rewritten by this point + dumpAssertions("pre-definition-expansion", d_assertionsToPreprocess); { Chat() << "expanding definitions..." << endl; @@ -1946,6 +1948,8 @@ void SmtEnginePrivate::processAssertions() { } dumpAssertions("post-substitution", d_assertionsToPreprocess); + // Assertions ARE guaranteed to be rewritten by this point + dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); if( options::preSkolemQuant() ){ //apply pre-skolemization to existential quantifiers @@ -2075,7 +2079,8 @@ void SmtEnginePrivate::addFormula(TNode n) Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl; // Add the normalized formula to the queue - d_assertionsToPreprocess.push_back(Rewriter::rewrite(n)); + d_assertionsToPreprocess.push_back(n); + //d_assertionsToPreprocess.push_back(Rewriter::rewrite(n)); // If the mode of processing is incremental prepreocess and assert immediately if (options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL) { |