summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp35
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)");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback