diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-08 05:56:08 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-08 05:56:08 +0000 |
commit | 8cd22903675724e29249ce089ee77c7c4d3897fb (patch) | |
tree | 64ea92a2a0f8721b7e1b15796824f6259567aa75 /src/smt | |
parent | 6685546d585212559b97d5722161ad52ff5c4121 (diff) |
Merge from decision branch (till r3663)
(no performace or search behavior changes expected)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ed28c23a3..d0f7a0584 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1039,6 +1039,9 @@ void SmtEnginePrivate::simplifyAssertions() expandDefinitions(d_assertionsToPreprocess[i], cache); } } + + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; if(Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) { // Perform non-clausal simplification @@ -1053,6 +1056,9 @@ void SmtEnginePrivate::simplifyAssertions() d_assertionsToCheck.swap(d_assertionsToPreprocess); } + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + if(Options::current()->doITESimp) { // ite simplification simpITE(); @@ -1063,6 +1069,8 @@ void SmtEnginePrivate::simplifyAssertions() } if(Options::current()->repeatSimp && Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) { + Trace("simplify") << "SmtEnginePrivate::simplify(): " + << " doing repeated simplification" << std::endl; d_assertionsToCheck.swap(d_assertionsToPreprocess); // Abuse the user context to make sure circuit propagator gets backtracked d_smt.d_userContext->push(); @@ -1070,6 +1078,9 @@ void SmtEnginePrivate::simplifyAssertions() d_smt.d_userContext->pop(); } + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + if(Options::current()->doStaticLearning) { // Perform static learning Trace("simplify") << "SmtEnginePrivate::simplify(): " @@ -1180,14 +1191,10 @@ void SmtEnginePrivate::processAssertions() { { TimerStat::CodeTimer codeTimer(d_smt.d_iteRemovalTime); - // Remove ITEs - d_smt.d_numAssertionsPre += d_assertionsToCheck.size(); // Remove ITEs, updating d_iteSkolemMap + d_smt.d_numAssertionsPre += d_assertionsToCheck.size(); removeITEs(); d_smt.d_numAssertionsPost += d_assertionsToCheck.size(); - // This may need to be in a try-catch - // block. make regress is passing, so - // skipping for now --K } if(Options::current()->repeatSimp) { |