diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 35 |
1 files changed, 17 insertions, 18 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8b5a93fa9..fee77df39 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -295,7 +295,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : void SmtEngine::shutdown() { if(Dump.isOn("benchmark")) { - Dump("benchmark") << QuitCommand() << endl; + Dump("benchmark") << QuitCommand(); } // check to see if a postsolve() is pending @@ -351,7 +351,7 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) { } if(Dump.isOn("benchmark")) { - Dump("benchmark") << SetBenchmarkLogicCommand(s) << endl; + Dump("benchmark") << SetBenchmarkLogicCommand(s); } setLogicInternal(s); @@ -377,7 +377,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOptionException, ModalException) { Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << SetInfoCommand(key, value) << endl; + Dump("benchmark") << SetInfoCommand(key, value); } // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") @@ -462,7 +462,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOptionException, ModalException) { Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << SetOptionCommand(key, value) << endl; + Dump("benchmark") << SetOptionCommand(key, value); } if(key == ":print-success") { @@ -508,7 +508,7 @@ SExpr SmtEngine::getOption(const std::string& key) const throw(BadOptionException) { Trace("smt") << "SMT getOption(" << key << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetOptionCommand(key) << endl; + Dump("benchmark") << GetOptionCommand(key); } if(key == ":print-success") { return SExpr("true"); @@ -543,10 +543,9 @@ void SmtEngine::defineFunction(Expr func, Trace("smt") << "SMT defineFunction(" << func << ")" << endl; if(Dump.isOn("declarations")) { stringstream ss; - ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) + ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream())) << func; - Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula) - << endl; + Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula); } NodeManagerScope nms(d_nodeManager); @@ -995,7 +994,7 @@ void SmtEnginePrivate::processAssertions() { // Push the simplified assertions to the dump output stream for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { Dump("assertions") - << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())) << endl; + << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())); } } @@ -1077,7 +1076,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) { // Dump the query if requested if(Dump.isOn("benchmark")) { // the expr already got dumped out if assertion-dumping is on - Dump("benchmark") << CheckSatCommand() << endl; + Dump("benchmark") << CheckSatCommand(); } // Pop the context @@ -1134,7 +1133,7 @@ Result SmtEngine::query(const BoolExpr& e) { // Dump the query if requested if(Dump.isOn("benchmark")) { // the expr already got dumped out if assertion-dumping is on - Dump("benchmark") << CheckSatCommand() << endl; + Dump("benchmark") << CheckSatCommand(); } // Pop the context @@ -1170,7 +1169,7 @@ Expr SmtEngine::simplify(const Expr& e) { } Trace("smt") << "SMT simplify(" << e << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << SimplifyCommand(e) << endl; + Dump("benchmark") << SimplifyCommand(e); } return d_private->applySubstitutions(e).toExpr(); } @@ -1185,7 +1184,7 @@ Expr SmtEngine::getValue(const Expr& e) Trace("smt") << "SMT getValue(" << e << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetValueCommand(e) << endl; + Dump("benchmark") << GetValueCommand(e); } if(!Options::current()->produceModels) { const char* msg = @@ -1251,7 +1250,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Trace("smt") << "SMT getAssignment()" << endl; NodeManagerScope nms(d_nodeManager); if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetAssignmentCommand() << endl; + Dump("benchmark") << GetAssignmentCommand(); } if(!Options::current()->produceAssignments) { const char* msg = @@ -1307,7 +1306,7 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { Trace("smt") << "SMT getProof()" << endl; NodeManagerScope nms(d_nodeManager); if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetProofCommand() << endl; + Dump("benchmark") << GetProofCommand(); } #ifdef CVC4_PROOF if(!Options::current()->proof) { @@ -1332,7 +1331,7 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { vector<Expr> SmtEngine::getAssertions() throw(ModalException, AssertionException) { if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetAssertionsCommand() << endl; + Dump("benchmark") << GetAssertionsCommand(); } NodeManagerScope nms(d_nodeManager); Trace("smt") << "SMT getAssertions()" << endl; @@ -1356,7 +1355,7 @@ void SmtEngine::push() { Trace("smt") << "SMT push()" << endl; d_private->processAssertions(); if(Dump.isOn("benchmark")) { - Dump("benchmark") << PushCommand() << endl; + Dump("benchmark") << PushCommand(); } if(!Options::current()->incrementalSolving) { throw ModalException("Cannot push when not solving incrementally (use --incremental)"); @@ -1378,7 +1377,7 @@ void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); Trace("smt") << "SMT pop()" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << PopCommand() << endl; + Dump("benchmark") << PopCommand(); } if(!Options::current()->incrementalSolving) { throw ModalException("Cannot pop when not solving incrementally (use --incremental)"); |