summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--configure.ac3
-rw-r--r--src/expr/command.cpp166
-rw-r--r--src/expr/command.h32
-rw-r--r--src/main/driver.cpp1
-rw-r--r--src/main/driver_portfolio.cpp1
-rw-r--r--src/prop/cnf_stream.cpp4
-rw-r--r--src/prop/minisat/core/Solver.cc2
-rw-r--r--src/prop/minisat/core/Solver.h2
-rw-r--r--src/prop/prop_engine.cpp4
-rw-r--r--src/smt/smt_engine.cpp35
-rw-r--r--src/theory/arrays/theory_arrays.cpp10
-rw-r--r--src/theory/theory.h3
-rw-r--r--src/theory/theory_engine.cpp20
-rw-r--r--src/theory/theory_engine.h3
-rw-r--r--src/util/Makefile.am2
-rw-r--r--src/util/dump.cpp27
-rw-r--r--src/util/dump.h130
-rw-r--r--src/util/ite_removal.cpp8
-rw-r--r--src/util/ite_removal.h1
-rw-r--r--src/util/options.cpp3
-rw-r--r--src/util/output.cpp8
-rw-r--r--src/util/output.h22
22 files changed, 399 insertions, 88 deletions
diff --git a/configure.ac b/configure.ac
index ee6975034..68d7bf026 100644
--- a/configure.ac
+++ b/configure.ac
@@ -891,6 +891,9 @@ if test x$with_portfolio != xyes; then
with_portfolio=no
fi
AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
+if test "$with_portfolio" = yes; then
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
+fi
# Whether to build compatibility library
CVC4_BUILD_LIBCOMPAT=yes
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 3dac28e11..48b6940dd 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -27,6 +27,7 @@
#include "smt/smt_engine.h"
#include "smt/bad_option_exception.h"
#include "util/output.h"
+#include "util/dump.h"
#include "util/sexpr.h"
#include "expr/node.h"
#include "printer/printer.h"
@@ -134,6 +135,10 @@ Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollecti
return new EmptyCommand(d_name);
}
+Command* EmptyCommand::clone() const {
+ return new EmptyCommand(d_name);
+}
+
/* class AssertCommand */
AssertCommand::AssertCommand(const BoolExpr& e) throw() :
@@ -157,6 +162,10 @@ Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollect
return new AssertCommand(d_expr.exportTo(exprManager, variableMap));
}
+Command* AssertCommand::clone() const {
+ return new AssertCommand(d_expr);
+}
+
/* class PushCommand */
void PushCommand::invoke(SmtEngine* smtEngine) throw() {
@@ -169,7 +178,11 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() {
}
Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new PushCommand;
+ return new PushCommand();
+}
+
+Command* PushCommand::clone() const {
+ return new PushCommand();
}
/* class PopCommand */
@@ -193,6 +206,10 @@ Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection
return new PopCommand();
}
+Command* PopCommand::clone() const {
+ return new PopCommand();
+}
+
/* class CheckSatCommand */
CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() :
@@ -230,6 +247,12 @@ Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapColle
return c;
}
+Command* CheckSatCommand::clone() const {
+ CheckSatCommand* c = new CheckSatCommand(d_expr);
+ c->d_result = d_result;
+ return c;
+}
+
/* class QueryCommand */
QueryCommand::QueryCommand(const BoolExpr& e) throw() :
@@ -267,6 +290,12 @@ Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollecti
return c;
}
+Command* QueryCommand::clone() const {
+ QueryCommand* c = new QueryCommand(d_expr);
+ c->d_result = d_result;
+ return c;
+}
+
/* class QuitCommand */
QuitCommand::QuitCommand() throw() {
@@ -281,6 +310,10 @@ Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollectio
return new QuitCommand();
}
+Command* QuitCommand::clone() const {
+ return new QuitCommand();
+}
+
/* class CommentCommand */
CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
@@ -299,6 +332,10 @@ Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollec
return new CommentCommand(d_comment);
}
+Command* CommentCommand::clone() const {
+ return new CommentCommand(d_comment);
+}
+
/* class CommandSequence */
CommandSequence::CommandSequence() throw() :
@@ -315,6 +352,10 @@ void CommandSequence::addCommand(Command* cmd) throw() {
d_commandSequence.push_back(cmd);
}
+void CommandSequence::clear() throw() {
+ d_commandSequence.clear();
+}
+
void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
for(; d_index < d_commandSequence.size(); ++d_index) {
d_commandSequence[d_index]->invoke(smtEngine);
@@ -350,6 +391,15 @@ Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapColle
return seq;
}
+Command* CommandSequence::clone() const {
+ CommandSequence* seq = new CommandSequence();
+ for(const_iterator i = begin(); i != end(); ++i) {
+ seq->addCommand((*i)->clone());
+ }
+ seq->d_index = d_index;
+ return seq;
+}
+
CommandSequence::const_iterator CommandSequence::end() const throw() {
return d_commandSequence.end();
}
@@ -386,7 +436,7 @@ Type DeclareFunctionCommand::getType() const throw() {
}
void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this << endl;
+ Dump("declarations") << *this;
}
Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
@@ -395,6 +445,10 @@ Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
d_type.exportTo(exprManager, variableMap));
}
+Command* DeclareFunctionCommand::clone() const {
+ return new DeclareFunctionCommand(d_symbol, d_type);
+}
+
/* class DeclareTypeCommand */
DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() :
@@ -412,7 +466,7 @@ Type DeclareTypeCommand::getType() const throw() {
}
void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this << endl;
+ Dump("declarations") << *this;
}
Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
@@ -421,6 +475,10 @@ Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
d_type.exportTo(exprManager, variableMap));
}
+Command* DeclareTypeCommand::clone() const {
+ return new DeclareTypeCommand(d_symbol, d_arity, d_type);
+}
+
/* class DefineTypeCommand */
DefineTypeCommand::DefineTypeCommand(const std::string& id,
@@ -447,7 +505,7 @@ Type DefineTypeCommand::getType() const throw() {
}
void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this << endl;
+ Dump("declarations") << *this;
d_commandStatus = CommandSuccess::instance();
}
@@ -459,6 +517,10 @@ Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCol
return new DefineTypeCommand(d_symbol, params, type);
}
+Command* DefineTypeCommand::clone() const {
+ return new DefineTypeCommand(d_symbol, d_params, d_type);
+}
+
/* class DefineFunctionCommand */
DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
@@ -493,7 +555,7 @@ Expr DefineFunctionCommand::getFormula() const throw() {
}
void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
- //Dump("declarations") << *this << endl; -- done by SmtEngine
+ //Dump("declarations") << *this; -- done by SmtEngine
try {
if(!d_func.isNull()) {
smtEngine->defineFunction(d_func, d_formals, d_formula);
@@ -513,6 +575,10 @@ Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMa
return new DefineFunctionCommand(d_symbol, func, formals, formula);
}
+Command* DefineFunctionCommand::clone() const {
+ return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula);
+}
+
/* class DefineNamedFunctionCommand */
DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
@@ -539,6 +605,10 @@ Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprMana
return new DefineNamedFunctionCommand(d_symbol, func, formals, formula);
}
+Command* DefineNamedFunctionCommand::clone() const {
+ return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
+}
+
/* class Simplify */
SimplifyCommand::SimplifyCommand(Expr term) throw() :
@@ -572,6 +642,12 @@ Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapColle
return c;
}
+Command* SimplifyCommand::clone() const {
+ SimplifyCommand* c = new SimplifyCommand(d_term);
+ c->d_result = d_result;
+ return c;
+}
+
/* class GetValueCommand */
GetValueCommand::GetValueCommand(Expr term) throw() :
@@ -610,6 +686,12 @@ Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapColle
return c;
}
+Command* GetValueCommand::clone() const {
+ GetValueCommand* c = new GetValueCommand(d_term);
+ c->d_result = d_result;
+ return c;
+}
+
/* class GetAssignmentCommand */
GetAssignmentCommand::GetAssignmentCommand() throw() {
@@ -637,7 +719,13 @@ void GetAssignmentCommand::printResult(std::ostream& out) const throw() {
}
Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetAssignmentCommand* c = new GetAssignmentCommand;
+ GetAssignmentCommand* c = new GetAssignmentCommand();
+ c->d_result = d_result;
+ return c;
+}
+
+Command* GetAssignmentCommand::clone() const {
+ GetAssignmentCommand* c = new GetAssignmentCommand();
c->d_result = d_result;
return c;
}
@@ -669,7 +757,13 @@ void GetProofCommand::printResult(std::ostream& out) const throw() {
}
Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetProofCommand* c = new GetProofCommand;
+ GetProofCommand* c = new GetProofCommand();
+ c->d_result = d_result;
+ return c;
+}
+
+Command* GetProofCommand::clone() const {
+ GetProofCommand* c = new GetProofCommand();
c->d_result = d_result;
return c;
}
@@ -704,7 +798,13 @@ void GetAssertionsCommand::printResult(std::ostream& out) const throw() {
}
Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetAssertionsCommand* c = new GetAssertionsCommand;
+ GetAssertionsCommand* c = new GetAssertionsCommand();
+ c->d_result = d_result;
+ return c;
+}
+
+Command* GetAssertionsCommand::clone() const {
+ GetAssertionsCommand* c = new GetAssertionsCommand();
c->d_result = d_result;
return c;
}
@@ -732,8 +832,11 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
}
Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- SetBenchmarkStatusCommand* c = new SetBenchmarkStatusCommand(d_status);
- return c;
+ return new SetBenchmarkStatusCommand(d_status);
+}
+
+Command* SetBenchmarkStatusCommand::clone() const {
+ return new SetBenchmarkStatusCommand(d_status);
}
/* class SetBenchmarkLogicCommand */
@@ -756,8 +859,11 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
}
Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- SetBenchmarkLogicCommand* c = new SetBenchmarkLogicCommand(d_logic);
- return c;
+ return new SetBenchmarkLogicCommand(d_logic);
+}
+
+Command* SetBenchmarkLogicCommand::clone() const {
+ return new SetBenchmarkLogicCommand(d_logic);
}
/* class SetInfoCommand */
@@ -787,8 +893,11 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
}
Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- SetInfoCommand* c = new SetInfoCommand(d_flag, d_sexpr);
- return c;
+ return new SetInfoCommand(d_flag, d_sexpr);
+}
+
+Command* SetInfoCommand::clone() const {
+ return new SetInfoCommand(d_flag, d_sexpr);
}
/* class GetInfoCommand */
@@ -832,6 +941,12 @@ Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollec
return c;
}
+Command* GetInfoCommand::clone() const {
+ GetInfoCommand* c = new GetInfoCommand(d_flag);
+ c->d_result = d_result;
+ return c;
+}
+
/* class SetOptionCommand */
SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
@@ -859,8 +974,11 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
}
Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- SetOptionCommand* c = new SetOptionCommand(d_flag, d_sexpr);
- return c;
+ return new SetOptionCommand(d_flag, d_sexpr);
+}
+
+Command* SetOptionCommand::clone() const {
+ return new SetOptionCommand(d_flag, d_sexpr);
}
/* class GetOptionCommand */
@@ -902,6 +1020,12 @@ Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapColl
return c;
}
+Command* GetOptionCommand::clone() const {
+ GetOptionCommand* c = new GetOptionCommand(d_flag);
+ c->d_result = d_result;
+ return c;
+}
+
/* class DatatypeDeclarationCommand */
DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
@@ -919,15 +1043,19 @@ DatatypeDeclarationCommand::getDatatypes() const throw() {
}
void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this << endl;
+ Dump("declarations") << *this;
d_commandStatus = CommandSuccess::instance();
}
Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- std::cout << "We currently do not support exportTo with Datatypes" << std::endl;
- exit(1);
+ Warning() << "We currently do not support exportTo with Datatypes" << std::endl;
return NULL;
}
+
+Command* DatatypeDeclarationCommand::clone() const {
+ return new DatatypeDeclarationCommand(d_datatypes);
+}
+
/* output stream insertion operator for benchmark statuses */
std::ostream& operator<<(std::ostream& out,
BenchmarkStatus status) throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index fa1da4cb1..6bb6fba3d 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -225,6 +225,11 @@ public:
*/
virtual Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) = 0;
+ /**
+ * Clone this Command (make a shallow copy).
+ */
+ virtual Command* clone() const = 0;
+
protected:
class ExportTransformer {
ExprManager* d_exprManager;
@@ -256,6 +261,7 @@ public:
std::string getName() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class EmptyCommand */
class CVC4_PUBLIC AssertCommand : public Command {
@@ -267,6 +273,7 @@ public:
BoolExpr getExpr() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class AssertCommand */
class CVC4_PUBLIC PushCommand : public Command {
@@ -274,6 +281,7 @@ public:
~PushCommand() throw() {}
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class PushCommand */
class CVC4_PUBLIC PopCommand : public Command {
@@ -281,6 +289,7 @@ public:
~PopCommand() throw() {}
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class PopCommand */
class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
@@ -301,6 +310,7 @@ public:
Type getType() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class DeclareFunctionCommand */
class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
@@ -314,6 +324,7 @@ public:
Type getType() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class DeclareTypeCommand */
class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
@@ -328,6 +339,7 @@ public:
Type getType() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class DefineTypeCommand */
class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
@@ -345,6 +357,7 @@ public:
Expr getFormula() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class DefineFunctionCommand */
/**
@@ -358,6 +371,7 @@ public:
const std::vector<Expr>& formals, Expr formula) throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class DefineNamedFunctionCommand */
class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -373,6 +387,7 @@ public:
Result getResult() const throw();
void printResult(std::ostream& out) const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class CheckSatCommand */
class CVC4_PUBLIC QueryCommand : public Command {
@@ -387,6 +402,7 @@ public:
Result getResult() const throw();
void printResult(std::ostream& out) const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class QueryCommand */
// this is TRANSFORM in the CVC presentation language
@@ -402,6 +418,7 @@ public:
Expr getResult() const throw();
void printResult(std::ostream& out) const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class SimplifyCommand */
class CVC4_PUBLIC GetValueCommand : public Command {
@@ -416,6 +433,7 @@ public:
Expr getResult() const throw();
void printResult(std::ostream& out) const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class GetValueCommand */
class CVC4_PUBLIC GetAssignmentCommand : public Command {
@@ -428,6 +446,7 @@ public:
SExpr getResult() const throw();
void printResult(std::ostream& out) const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class GetAssignmentCommand */
class CVC4_PUBLIC GetProofCommand : public Command {
@@ -440,6 +459,7 @@ public:
Proof* getResult() const throw();
void printResult(std::ostream& out) const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class GetProofCommand */
class CVC4_PUBLIC GetAssertionsCommand : public Command {
@@ -452,6 +472,7 @@ public:
std::string getResult() const throw();
void printResult(std::ostream& out) const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class GetAssertionsCommand */
class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
@@ -463,6 +484,7 @@ public:
BenchmarkStatus getStatus() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class SetBenchmarkStatusCommand */
class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
@@ -474,6 +496,7 @@ public:
std::string getLogic() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class SetBenchmarkLogicCommand */
class CVC4_PUBLIC SetInfoCommand : public Command {
@@ -487,6 +510,7 @@ public:
SExpr getSExpr() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class SetInfoCommand */
class CVC4_PUBLIC GetInfoCommand : public Command {
@@ -501,6 +525,7 @@ public:
std::string getResult() const throw();
void printResult(std::ostream& out) const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class GetInfoCommand */
class CVC4_PUBLIC SetOptionCommand : public Command {
@@ -514,6 +539,7 @@ public:
SExpr getSExpr() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class SetOptionCommand */
class CVC4_PUBLIC GetOptionCommand : public Command {
@@ -528,6 +554,7 @@ public:
std::string getResult() const throw();
void printResult(std::ostream& out) const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class GetOptionCommand */
class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
@@ -540,6 +567,7 @@ public:
const std::vector<DatatypeType>& getDatatypes() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class DatatypeDeclarationCommand */
class CVC4_PUBLIC QuitCommand : public Command {
@@ -548,6 +576,7 @@ public:
~QuitCommand() throw() {}
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class QuitCommand */
class CVC4_PUBLIC CommentCommand : public Command {
@@ -558,6 +587,7 @@ public:
std::string getComment() const throw();
void invoke(SmtEngine* smtEngine) throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class CommentCommand */
class CVC4_PUBLIC CommandSequence : public Command {
@@ -571,6 +601,7 @@ public:
~CommandSequence() throw();
void addCommand(Command* cmd) throw();
+ void clear() throw();
void invoke(SmtEngine* smtEngine) throw();
void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
@@ -585,6 +616,7 @@ public:
iterator end() throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
};/* class CommandSequence */
class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index eb70f5c93..ef6b99715 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -38,6 +38,7 @@
#include "util/configuration.h"
#include "util/options.h"
#include "util/output.h"
+#include "util/dump.h"
#include "util/result.h"
#include "util/stats.h"
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index 363901c1d..d8a8e5afa 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -24,6 +24,7 @@
#include "util/configuration.h"
#include "util/options.h"
#include "util/output.h"
+#include "util/dump.h"
#include "util/result.h"
#include "util/stats.h"
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 396454fac..661221441 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -74,7 +74,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
Debug("cnf") << "Inserting into stream " << c << endl;
if(Dump.isOn("clauses")) {
if(c.size() == 1) {
- Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr())) << endl;
+ Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr()));
} else {
Assert(c.size() > 1);
NodeBuilder<> b(kind::OR);
@@ -82,7 +82,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
b << getNode(c[i]);
}
Node n = b;
- Dump("clauses") << AssertCommand(BoolExpr(n.toExpr())) << endl;
+ Dump("clauses") << AssertCommand(BoolExpr(n.toExpr()));
}
}
d_satSolver->addClause(c, d_removable);
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index ac3c5e101..980cb1b3f 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -322,7 +322,7 @@ void Solver::cancelUntil(int level) {
for (int l = trail_lim.size() - level; l > 0; --l) {
context->pop();
if(Dump.isOn("state")) {
- Dump("state") << PopCommand() << std::endl;
+ Dump("state") << PopCommand();
}
}
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 8a5472725..ca5b2c30f 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -454,7 +454,7 @@ inline bool Solver::addClause (Lit p, bool removable)
inline bool Solver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); }
-inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand() << std::endl; } }
+inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } }
inline int Solver::decisionLevel () const { return trail_lim.size(); }
inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2538e6d0c..b7b3c685f 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -97,9 +97,9 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
if(!d_inCheckSat && Dump.isOn("learned")) {
- Dump("learned") << AssertCommand(BoolExpr(node.toExpr())) << endl;
+ Dump("learned") << AssertCommand(BoolExpr(node.toExpr()));
} else if(Dump.isOn("lemmas")) {
- Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr())) << endl;
+ Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr()));
}
//TODO This comment is now false
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)");
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index fd88c751a..03a9d7a4c 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1144,15 +1144,7 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
NodeManager* nm = NodeManager::currentNM();
TypeNode ixType = a.getType()[0];
Node k = nm->mkVar(ixType);
- if(Dump.isOn("declarations")) {
- stringstream kss;
- kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << k;
- string ks = kss.str();
- Dump("declarations")
- << CommentCommand(ks + " is an extensional lemma index variable "
- "from the theory of arrays") << endl
- << DeclareFunctionCommand(ks, ixType.toType()) << endl;
- }
+ Dump.declareVar(k.toExpr(), "an extensional lemma index variable from the theory of arrays");
Node eq = nm->mkNode(kind::EQUAL, a, b);
Node ak = nm->mkNode(kind::SELECT, a, k);
Node bk = nm->mkNode(kind::SELECT, b, k);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1451568ab..c84d10ca1 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -31,6 +31,7 @@
#include "context/cdlist.h"
#include "context/cdo.h"
#include "util/options.h"
+#include "util/dump.h"
#include <string>
#include <iostream>
@@ -199,7 +200,7 @@ protected:
d_factsHead = d_factsHead + 1;
Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
if(Dump.isOn("state")) {
- Dump("state") << AssertCommand(fact.assertion.toExpr()) << std::endl;
+ Dump("state") << AssertCommand(fact.assertion.toExpr());
}
return fact;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2950ad413..ebfc797a1 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -160,8 +160,8 @@ void TheoryEngine::check(Theory::Effort effort) {
if(Dump.isOn("missed-t-conflicts")) {
Dump("missed-t-conflicts")
- << CommentCommand("Completeness check for T-conflicts; expect sat") << endl
- << CheckSatCommand() << endl;
+ << CommentCommand("Completeness check for T-conflicts; expect sat")
+ << CheckSatCommand();
}
Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << std::endl;
@@ -311,8 +311,8 @@ void TheoryEngine::propagate(Theory::Effort effort) {
++i) {
if(d_hasPropagated.find(*i) == d_hasPropagated.end()) {
Dump("missed-t-propagations")
- << CommentCommand("Completeness check for T-propagations; expect invalid") << endl
- << QueryCommand((*i).toExpr()) << endl;
+ << CommentCommand("Completeness check for T-propagations; expect invalid")
+ << QueryCommand((*i).toExpr());
}
}
}
@@ -605,8 +605,8 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
d_propEngine->checkTime();
if(Dump.isOn("t-propagations")) {
- Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl
- << QueryCommand(literal.toExpr()) << std::endl;
+ Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
+ << QueryCommand(literal.toExpr());
}
if(Dump.isOn("missed-t-propagations")) {
d_hasPropagated.insert(literal);
@@ -717,8 +717,8 @@ Node TheoryEngine::getExplanation(TNode node) {
Assert(!explanation.isNull());
if(Dump.isOn("t-explanations")) {
- Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") << std::endl
- << QueryCommand(explanation.impNode(node).toExpr()) << std::endl;
+ Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid")
+ << QueryCommand(explanation.impNode(node).toExpr());
}
Assert(properExplanation(node, explanation));
@@ -731,8 +731,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
d_inConflict = true;
if(Dump.isOn("t-conflicts")) {
- Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << std::endl
- << CheckSatCommand(conflict.toExpr()) << std::endl;
+ Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
+ << CheckSatCommand(conflict.toExpr());
}
if (d_sharedTermsExist) {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 4c9309fb6..a8aa62d35 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -390,8 +390,7 @@ class TheoryEngine {
theory::LemmaStatus lemma(TNode node, bool negated, bool removable) {
if(Dump.isOn("t-lemmas")) {
Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
- << std::endl
- << QueryCommand(node.toExpr()) << std::endl;
+ << QueryCommand(node.toExpr());
}
// Share with other portfolio threads
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index e8d33fbd4..d52f23a9c 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -57,6 +57,8 @@ libutil_la_SOURCES = \
ntuple.h \
recursion_breaker.h \
subrange_bound.h \
+ dump.h \
+ dump.cpp \
predicate.h \
predicate.cpp \
cardinality.h \
diff --git a/src/util/dump.cpp b/src/util/dump.cpp
new file mode 100644
index 000000000..2b10158d4
--- /dev/null
+++ b/src/util/dump.cpp
@@ -0,0 +1,27 @@
+/********************* */
+/*! \file dump.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Dump utility classes and functions
+ **
+ ** Dump utility classes and functions.
+ **/
+
+#include "util/dump.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+DumpC DumpChannel CVC4_PUBLIC;
+
+}/* CVC4 namespace */
diff --git a/src/util/dump.h b/src/util/dump.h
new file mode 100644
index 000000000..7318af1a5
--- /dev/null
+++ b/src/util/dump.h
@@ -0,0 +1,130 @@
+/********************* */
+/*! \file dump.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Dump utility classes and functions
+ **
+ ** Dump utility classes and functions.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__DUMP_H
+#define __CVC4__DUMP_H
+
+#include "util/output.h"
+#include "expr/command.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC CVC4dumpstream {
+
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+ std::ostream* d_os;
+#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
+
+#ifdef CVC4_PORTFOLIO
+ CommandSequence* d_commands;
+#endif /* CVC4_PORTFOLIO */
+
+public:
+ CVC4dumpstream() throw()
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
+ : d_os(NULL), d_commands(NULL)
+#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+ : d_os(NULL)
+#elif defined(CVC4_PORTFOLIO)
+ : d_commands(NULL)
+#endif /* CVC4_PORTFOLIO */
+ { }
+
+ CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw()
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
+ : d_os(&os), d_commands(&commands)
+#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+ : d_os(&os)
+#elif defined(CVC4_PORTFOLIO)
+ : d_commands(&commands)
+#endif /* CVC4_PORTFOLIO */
+ { }
+
+ CVC4dumpstream& operator<<(const Command& c) {
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+ if(d_os != NULL) {
+ (*d_os) << c << std::endl;
+ }
+#endif
+#if defined(CVC4_PORTFOLIO)
+ if(d_commands != NULL) {
+ d_commands->addCommand(c.clone());
+ }
+#endif
+ return *this;
+ }
+};/* class CVC4dumpstream */
+
+/** The dump class */
+class CVC4_PUBLIC DumpC {
+ std::set<std::string> d_tags;
+ CommandSequence d_commands;
+
+public:
+ CVC4dumpstream operator()(const char* tag) {
+ if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+ return CVC4dumpstream(getStream(), d_commands);
+ } else {
+ return CVC4dumpstream();
+ }
+ }
+ CVC4dumpstream operator()(std::string tag) {
+ if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+ return CVC4dumpstream(getStream(), d_commands);
+ } else {
+ return CVC4dumpstream();
+ }
+ }
+
+ void clear() { d_commands.clear(); }
+ const CommandSequence& getCommands() const { return d_commands; }
+
+ void declareVar(Expr e, std::string comment) {
+ if(isOn("declarations")) {
+ std::stringstream ss;
+ ss << Expr::setlanguage(Expr::setlanguage::getLanguage(getStream())) << e;
+ std::string s = ss.str();
+ CVC4dumpstream(getStream(), d_commands)
+ << CommentCommand(s + " is " + comment)
+ << DeclareFunctionCommand(s, e.getType());
+ }
+ }
+
+ bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+ bool on (std::string tag) { d_tags.insert(tag); return true; }
+ bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+ bool off(std::string tag) { d_tags.erase (tag); return false; }
+ bool off() { d_tags.clear(); return false; }
+
+ bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+ bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
+ std::ostream& setStream(std::ostream& os) { DumpOut.setStream(os); return os; }
+ std::ostream& getStream() { return DumpOut.getStream(); }
+};/* class DumpC */
+
+/** The dump singleton */
+extern DumpC DumpChannel CVC4_PUBLIC;
+
+#define Dump ::CVC4::DumpChannel
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DUMP_H */
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index bd5048040..dfa6e3cba 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -55,13 +55,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output) {
// Make the skolem to represent the ITE
Node skolem = nodeManager->mkVar(nodeType);
- if(Dump.isOn("declarations")) {
- stringstream kss;
- kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << skolem;
- string ks = kss.str();
- Dump("declarations") << CommentCommand(ks + " is a variable introduced due to term-level ITE removal") << endl
- << DeclareFunctionCommand(ks, nodeType.toType()) << endl;
- }
+ Dump.declareVar(skolem.toExpr(), "a variable introduced due to term-level ITE removal");
// The new assertion
Node newAssertion =
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 8861d612c..bfb0d4ac8 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -22,6 +22,7 @@
#include <vector>
#include "expr/node.h"
+#include "util/dump.h"
namespace CVC4 {
diff --git a/src/util/options.cpp b/src/util/options.cpp
index d21df27ac..f9ab0b480 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -34,6 +34,7 @@
#include "util/language.h"
#include "util/options.h"
#include "util/output.h"
+#include "util/dump.h"
#include "cvc4autoconfig.h"
@@ -609,7 +610,7 @@ throw(OptionException) {
if(optarg == NULL || *optarg == '\0') {
throw OptionException(string("Bad file name for --dump-to"));
} else if(!strcmp(optarg, "-")) {
- Dump.setStream(DumpC::dump_cout);
+ Dump.setStream(DumpOutC::dump_cout);
} else {
ostream* dumpTo = new ofstream(optarg, ofstream::out | ofstream::trunc);
if(!*dumpTo) {
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 3823f7be6..48a7d51fd 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -40,8 +40,8 @@ MessageC MessageChannel CVC4_PUBLIC (&cout);
NoticeC NoticeChannel CVC4_PUBLIC (&cout);
ChatC ChatChannel CVC4_PUBLIC (&cout);
TraceC TraceChannel CVC4_PUBLIC (&cout);
-std::ostream DumpC::dump_cout(cout.rdbuf());// copy cout stream buffer
-DumpC DumpChannel CVC4_PUBLIC (&DumpC::dump_cout);
+std::ostream DumpOutC::dump_cout(cout.rdbuf());// copy cout stream buffer
+DumpOutC DumpOutChannel CVC4_PUBLIC (&DumpOutC::dump_cout);
#ifndef CVC4_MUZZLE
@@ -159,7 +159,7 @@ int TraceC::printf(std::string tag, const char* fmt, ...) {
# ifdef CVC4_DUMPING
-int DumpC::printf(const char* tag, const char* fmt, ...) {
+int DumpOutC::printf(const char* tag, const char* fmt, ...) {
if(d_tags.find(string(tag)) == d_tags.end()) {
return 0;
}
@@ -174,7 +174,7 @@ int DumpC::printf(const char* tag, const char* fmt, ...) {
return retval;
}
-int DumpC::printf(std::string tag, const char* fmt, ...) {
+int DumpOutC::printf(std::string tag, const char* fmt, ...) {
if(d_tags.find(tag) == d_tags.end()) {
return 0;
}
diff --git a/src/util/output.h b/src/util/output.h
index 8afb4e05a..308cfcac2 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -347,7 +347,7 @@ public:
};/* class TraceC */
/** The dump output class */
-class CVC4_PUBLIC DumpC {
+class CVC4_PUBLIC DumpOutC {
std::set<std::string> d_tags;
std::ostream* d_os;
@@ -358,7 +358,7 @@ public:
* unlimited). */
static std::ostream dump_cout;
- explicit DumpC(std::ostream* os) : d_os(os) {}
+ explicit DumpOutC(std::ostream* os) : d_os(os) {}
int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
@@ -389,7 +389,7 @@ public:
std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
std::ostream& getStream() { return *d_os; }
-};/* class DumpC */
+};/* class DumpOutC */
/** The debug output singleton */
extern DebugC DebugChannel CVC4_PUBLIC;
@@ -404,7 +404,7 @@ extern ChatC ChatChannel CVC4_PUBLIC;
/** The trace output singleton */
extern TraceC TraceChannel CVC4_PUBLIC;
/** The dump output singleton */
-extern DumpC DumpChannel CVC4_PUBLIC;
+extern DumpOutC DumpOutChannel CVC4_PUBLIC;
#ifdef CVC4_MUZZLE
@@ -415,7 +415,7 @@ extern DumpC DumpChannel CVC4_PUBLIC;
# define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
# define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
# define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
-# define Dump ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpChannel
+# define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel
inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
@@ -425,8 +425,8 @@ inline int NoticeC::printf(const char* fmt, ...) { return 0; }
inline int ChatC::printf(const char* fmt, ...) { return 0; }
inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
-inline int DumpC::printf(const char* tag, const char* fmt, ...) { return 0; }
-inline int DumpC::printf(std::string tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; }
#else /* CVC4_MUZZLE */
@@ -450,11 +450,11 @@ inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
# endif /* CVC4_TRACING */
# ifdef CVC4_DUMPING
-# define Dump ::CVC4::DumpChannel
+# define DumpOut ::CVC4::DumpOutChannel
# else /* CVC4_DUMPING */
-# define Dump ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpChannel
-inline int DumpC::printf(const char* tag, const char* fmt, ...) { return 0; }
-inline int DumpC::printf(std::string tag, const char* fmt, ...) { return 0; }
+# define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel
+inline int DumpOutC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; }
# endif /* CVC4_DUMPING */
#endif /* CVC4_MUZZLE */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback