From 629824db3911ab11ae286e4b14151a537602ba5a Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 10 Jun 2014 17:32:57 -0400 Subject: Merging Tim's pseudoboolean work from his fmcad14 branch. Signed-off-by: Morgan Deters --- src/smt/smt_engine.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/smt/smt_engine.cpp') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6dbef4fe3..b71969d15 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -88,6 +88,8 @@ #include "theory/strings/theory_strings_preprocess.h" #include "printer/options.h" +#include "theory/arith/pseudoboolean_proc.h" + using namespace std; using namespace CVC4; using namespace CVC4::smt; @@ -325,6 +327,9 @@ public: RemoveITE d_iteRemover; private: + + theory::arith::PseudoBooleanProcessor d_pbsProcessor; + /** The top level substitutions */ SubstitutionMap d_topLevelSubstitutions; @@ -419,6 +424,7 @@ public: d_simplifyAssertionsDepth(0), d_iteSkolemMap(), d_iteRemover(smt.d_userContext), + d_pbsProcessor(smt.d_userContext), d_topLevelSubstitutions(smt.d_userContext) { d_smt.d_nodeManager->subscribeEvents(this); @@ -1693,6 +1699,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime); + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl; if(d_propagatorNeedsFinish) { @@ -3014,6 +3021,13 @@ void SmtEnginePrivate::processAssertions() { // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertionsToPreprocess ); //} + if( options::pbRewrites() ){ + d_pbsProcessor.learn(d_assertionsToPreprocess); + if(d_pbsProcessor.likelyToHelp()){ + d_pbsProcessor.applyReplacements(d_assertionsToPreprocess); + } + } + dumpAssertions("pre-simplify", d_assertionsToPreprocess); Chat() << "simplifying assertions..." << endl; bool noConflict = simplifyAssertions(); -- cgit v1.2.3