diff options
-rw-r--r-- | configure.ac | 3 | ||||
-rw-r--r-- | src/expr/command.cpp | 166 | ||||
-rw-r--r-- | src/expr/command.h | 32 | ||||
-rw-r--r-- | src/main/driver.cpp | 1 | ||||
-rw-r--r-- | src/main/driver_portfolio.cpp | 1 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 4 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 2 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 4 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 35 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 10 | ||||
-rw-r--r-- | src/theory/theory.h | 3 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 20 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 3 | ||||
-rw-r--r-- | src/util/Makefile.am | 2 | ||||
-rw-r--r-- | src/util/dump.cpp | 27 | ||||
-rw-r--r-- | src/util/dump.h | 130 | ||||
-rw-r--r-- | src/util/ite_removal.cpp | 8 | ||||
-rw-r--r-- | src/util/ite_removal.h | 1 | ||||
-rw-r--r-- | src/util/options.cpp | 3 | ||||
-rw-r--r-- | src/util/output.cpp | 8 | ||||
-rw-r--r-- | src/util/output.h | 22 |
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 */ |