diff options
Diffstat (limited to 'src')
60 files changed, 3370 insertions, 527 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 6a070a88a..6baa4613f 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -28,6 +28,12 @@ libexpr_la_SOURCES = \ declaration_scope.cpp \ expr_manager_scope.h \ node_self_iterator.h \ + variable_type_map.h \ + pickle_data.h \ + pickle_data.cpp \ + pickler.h \ + pickler.cpp \ + node_self_iterator.h \ expr_stream.h \ kind_map.h diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 7d060186a..ba29b6c34 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -126,6 +126,10 @@ void EmptyCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new EmptyCommand(d_name); +} + /* class AssertCommand */ AssertCommand::AssertCommand(const BoolExpr& e) throw() : @@ -145,6 +149,10 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new AssertCommand(d_expr.exportTo(exprManager, variableMap)); +} + /* class PushCommand */ void PushCommand::invoke(SmtEngine* smtEngine) throw() { @@ -156,6 +164,10 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PushCommand; +} + /* class PopCommand */ void PopCommand::invoke(SmtEngine* smtEngine) throw() { @@ -173,6 +185,12 @@ CheckSatCommand::CheckSatCommand() throw() : d_expr() { } +Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PopCommand(); +} + +/* class CheckSatCommand */ + CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() : d_expr(expr) { } @@ -202,6 +220,12 @@ void CheckSatCommand::printResult(std::ostream& out) const throw() { } } +Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap)); + c->d_result = d_result; + return c; +} + /* class QueryCommand */ QueryCommand::QueryCommand(const BoolExpr& e) throw() : @@ -233,6 +257,12 @@ void QueryCommand::printResult(std::ostream& out) const throw() { } } +Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap)); + c->d_result = d_result; + return c; +} + /* class QuitCommand */ QuitCommand::QuitCommand() throw() { @@ -243,6 +273,10 @@ void QuitCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new QuitCommand(); +} + /* class CommentCommand */ CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { @@ -257,6 +291,10 @@ void CommentCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new CommentCommand(d_comment); +} + /* class CommandSequence */ CommandSequence::CommandSequence() throw() : @@ -299,6 +337,15 @@ CommandSequence::const_iterator CommandSequence::begin() const throw() { return d_commandSequence.begin(); } +Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + CommandSequence* seq = new CommandSequence(); + for(iterator i = begin(); i != end(); ++i) { + seq->addCommand((*i)->exportTo(exprManager, variableMap)); + } + seq->d_index = d_index; + return seq; +} + CommandSequence::const_iterator CommandSequence::end() const throw() { return d_commandSequence.end(); } @@ -338,6 +385,12 @@ void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; } +Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + return new DeclareFunctionCommand(d_symbol, + d_type.exportTo(exprManager, variableMap)); +} + /* class DeclareTypeCommand */ DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : @@ -358,6 +411,12 @@ void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; } +Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + return new DeclareTypeCommand(d_symbol, d_arity, + d_type.exportTo(exprManager, variableMap)); +} + /* class DefineTypeCommand */ DefineTypeCommand::DefineTypeCommand(const std::string& id, @@ -388,6 +447,14 @@ void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + vector<Type> params; + transform(d_params.begin(), d_params.end(), back_inserter(params), + ExportTransformer(exprManager, variableMap)); + Type type = d_type.exportTo(exprManager, variableMap); + return new DefineTypeCommand(d_symbol, params, type); +} + /* class DefineFunctionCommand */ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, @@ -429,6 +496,15 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Expr func = d_func.exportTo(exprManager, variableMap); + vector<Expr> formals; + transform(d_formals.begin(), d_formals.end(), back_inserter(formals), + ExportTransformer(exprManager, variableMap)); + Expr formula = d_formula.exportTo(exprManager, variableMap); + return new DefineFunctionCommand(d_symbol, func, formals, formula); +} + /* class DefineNamedFunctionCommand */ DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, @@ -446,6 +522,15 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Expr func = d_func.exportTo(exprManager, variableMap); + vector<Expr> formals; + transform(d_formals.begin(), d_formals.end(), back_inserter(formals), + ExportTransformer(exprManager, variableMap)); + Expr formula = d_formula.exportTo(exprManager, variableMap); + return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); +} + /* class Simplify */ SimplifyCommand::SimplifyCommand(Expr term) throw() : @@ -473,6 +558,12 @@ void SimplifyCommand::printResult(std::ostream& out) const throw() { } } +Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + /* class GetValueCommand */ GetValueCommand::GetValueCommand(Expr term) throw() : @@ -505,6 +596,12 @@ void GetValueCommand::printResult(std::ostream& out) const throw() { } } +Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetValueCommand* c = new GetValueCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + /* class GetAssignmentCommand */ GetAssignmentCommand::GetAssignmentCommand() throw() { @@ -531,6 +628,12 @@ void GetAssignmentCommand::printResult(std::ostream& out) const throw() { } } +Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssignmentCommand* c = new GetAssignmentCommand; + c->d_result = d_result; + return c; +} + /* class GetProofCommand */ GetProofCommand::GetProofCommand() throw() { @@ -557,6 +660,12 @@ void GetProofCommand::printResult(std::ostream& out) const throw() { } } +Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetProofCommand* c = new GetProofCommand; + c->d_result = d_result; + return c; +} + /* class GetAssertionsCommand */ GetAssertionsCommand::GetAssertionsCommand() throw() { @@ -586,6 +695,12 @@ void GetAssertionsCommand::printResult(std::ostream& out) const throw() { } } +Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssertionsCommand* c = new GetAssertionsCommand; + c->d_result = d_result; + return c; +} + /* class SetBenchmarkStatusCommand */ SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : @@ -608,6 +723,11 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetBenchmarkStatusCommand* c = new SetBenchmarkStatusCommand(d_status); + return c; +} + /* class SetBenchmarkLogicCommand */ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : @@ -627,6 +747,11 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetBenchmarkLogicCommand* c = new SetBenchmarkLogicCommand(d_logic); + return c; +} + /* class SetInfoCommand */ SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() : @@ -653,6 +778,11 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetInfoCommand* c = new SetInfoCommand(d_flag, d_sexpr); + return c; +} + /* class GetInfoCommand */ GetInfoCommand::GetInfoCommand(std::string flag) throw() : @@ -688,6 +818,12 @@ void GetInfoCommand::printResult(std::ostream& out) const throw() { } } +Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetInfoCommand* c = new GetInfoCommand(d_flag); + c->d_result = d_result; + return c; +} + /* class SetOptionCommand */ SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : @@ -714,6 +850,11 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetOptionCommand* c = new SetOptionCommand(d_flag, d_sexpr); + return c; +} + /* class GetOptionCommand */ GetOptionCommand::GetOptionCommand(std::string flag) throw() : @@ -747,6 +888,12 @@ void GetOptionCommand::printResult(std::ostream& out) const throw() { } } +Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetOptionCommand* c = new GetOptionCommand(d_flag); + c->d_result = d_result; + return c; +} + /* class DatatypeDeclarationCommand */ DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : @@ -768,6 +915,11 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { 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); + return NULL; +} /* 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 cf8c1b615..2d87fefc2 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -32,6 +32,7 @@ #include "expr/expr.h" #include "expr/type.h" +#include "expr/variable_type_map.h" #include "util/result.h" #include "util/sexpr.h" #include "util/datatype.h" @@ -177,6 +178,10 @@ public: };/* class CommandFailure */ class CVC4_PUBLIC Command { + // intentionally not permitted + Command(const Command&) CVC4_UNDEFINED; + Command& operator=(const Command&) CVC4_UNDEFINED; + protected: /** * This field contains a command status if the command has been @@ -210,6 +215,29 @@ public: virtual void printResult(std::ostream& out) const throw(); + /** + * Maps this Command into one for a different ExprManager, using + * variableMap for the translation and extending it with any new + * mappings. + */ + virtual Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) = 0; + +protected: + class ExportTransformer { + ExprManager* d_exprManager; + ExprManagerMapCollection& d_variableMap; + public: + ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) : + d_exprManager(exprManager), + d_variableMap(variableMap) { + } + Expr operator()(Expr e) { + return e.exportTo(d_exprManager, d_variableMap); + } + Type operator()(Type t) { + return t.exportTo(d_exprManager, d_variableMap); + } + };/* class Command::ExportTransformer */ };/* class Command */ /** @@ -224,6 +252,7 @@ public: ~EmptyCommand() throw() {} std::string getName() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class EmptyCommand */ class CVC4_PUBLIC AssertCommand : public Command { @@ -234,18 +263,21 @@ public: ~AssertCommand() throw() {} BoolExpr getExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class AssertCommand */ class CVC4_PUBLIC PushCommand : public Command { public: ~PushCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class PushCommand */ class CVC4_PUBLIC PopCommand : public Command { public: ~PopCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class PopCommand */ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { @@ -265,6 +297,7 @@ public: ~DeclareFunctionCommand() throw() {} Type getType() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DeclareFunctionCommand */ class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { @@ -277,6 +310,7 @@ public: size_t getArity() const throw(); Type getType() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DeclareTypeCommand */ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { @@ -290,6 +324,7 @@ public: const std::vector<Type>& getParameters() const throw(); Type getType() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DefineTypeCommand */ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { @@ -306,6 +341,7 @@ public: const std::vector<Expr>& getFormals() const throw(); Expr getFormula() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DefineFunctionCommand */ /** @@ -318,6 +354,7 @@ public: DefineNamedFunctionCommand(const std::string& id, Expr func, const std::vector<Expr>& formals, Expr formula) throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DefineNamedFunctionCommand */ class CVC4_PUBLIC CheckSatCommand : public Command { @@ -332,6 +369,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Result getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { @@ -345,6 +383,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Result getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class QueryCommand */ // this is TRANSFORM in the CVC presentation language @@ -359,6 +398,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Expr getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class SimplifyCommand */ class CVC4_PUBLIC GetValueCommand : public Command { @@ -372,6 +412,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Expr getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetValueCommand */ class CVC4_PUBLIC GetAssignmentCommand : public Command { @@ -383,6 +424,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); SExpr getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetAssignmentCommand */ class CVC4_PUBLIC GetProofCommand : public Command { @@ -394,6 +436,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Proof* getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetProofCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command { @@ -405,6 +448,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); std::string getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetAssertionsCommand */ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { @@ -415,6 +459,7 @@ public: ~SetBenchmarkStatusCommand() throw() {} BenchmarkStatus getStatus() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class SetBenchmarkStatusCommand */ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { @@ -425,6 +470,7 @@ public: ~SetBenchmarkLogicCommand() throw() {} std::string getLogic() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC SetInfoCommand : public Command { @@ -437,6 +483,7 @@ public: std::string getFlag() const throw(); SExpr getSExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class SetInfoCommand */ class CVC4_PUBLIC GetInfoCommand : public Command { @@ -450,6 +497,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); std::string getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetInfoCommand */ class CVC4_PUBLIC SetOptionCommand : public Command { @@ -462,6 +510,7 @@ public: std::string getFlag() const throw(); SExpr getSExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class SetOptionCommand */ class CVC4_PUBLIC GetOptionCommand : public Command { @@ -475,6 +524,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); std::string getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetOptionCommand */ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { @@ -486,6 +536,7 @@ public: DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw(); const std::vector<DatatypeType>& getDatatypes() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DatatypeDeclarationCommand */ class CVC4_PUBLIC QuitCommand : public Command { @@ -493,6 +544,7 @@ public: QuitCommand() throw(); ~QuitCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class QuitCommand */ class CVC4_PUBLIC CommentCommand : public Command { @@ -502,6 +554,7 @@ public: ~CommentCommand() throw() {} std::string getComment() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class CommentCommand */ class CVC4_PUBLIC CommandSequence : public Command { @@ -528,6 +581,7 @@ public: iterator begin() throw(); iterator end() throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class CommandSequence */ class CVC4_PUBLIC DeclarationSequence : public CommandSequence { diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 576d0324d..83a80ed13 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -18,6 +18,7 @@ #include "expr/node_manager.h" #include "expr/expr_manager.h" +#include "expr/variable_type_map.h" #include "context/context.h" #include "util/options.h" #include "util/stats.h" @@ -30,7 +31,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 34 "${template}" +#line 35 "${template}" #ifdef CVC4_STATISTICS_ON #define INC_STAT(kind) \ @@ -829,6 +830,52 @@ Context* ExprManager::getContext() const { return d_ctxt; } +namespace expr { + +Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); + +TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) { + Debug("export") << "type: " << n << std::endl; + Assert(n.getKind() == kind::SORT_TYPE || + n.getMetaKind() != kind::metakind::PARAMETERIZED, + "PARAMETERIZED-kinded types (other than SORT_KIND) not supported"); + if(n.getKind() == kind::TYPE_CONSTANT) { + return to->mkTypeConst(n.getConst<TypeConstant>()); + } else if(n.getKind() == kind::BITVECTOR_TYPE) { + return to->mkBitVectorType(n.getConst<BitVectorSize>()); + } + Type from_t = from->toType(n); + Type& to_t = vmap.d_typeMap[from_t]; + if(! to_t.isNull()) { + Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl; + return *Type::getTypeNode(to_t); + } + NodeBuilder<> children(to, n.getKind()); + if(n.getKind() == kind::SORT_TYPE) { + Debug("export") << "type: operator: " << n.getOperator() << std::endl; + // make a new sort tag in target node manager + Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG); + children << sortTag; + } + for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { + Debug("export") << "type: child: " << *i << std::endl; + children << exportTypeInternal(*i, from, to, vmap); + } + TypeNode out = children.constructTypeNode();// FIXME thread safety + to_t = to->toType(out); + return out; +}/* exportTypeInternal() */ + +}/* CVC4::expr namespace */ + +Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) { + Assert(t.d_nodeManager != em->d_nodeManager, + "Can't export a Type to the same ExprManager"); + NodeManagerScope ems(t.d_nodeManager); + return Type(em->d_nodeManager, + new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap))); +} + ${mkConst_implementations} }/* CVC4 namespace */ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 81d30fd1e..eecb40f3e 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -42,6 +42,13 @@ class SmtEngine; class NodeManager; struct Options; class IntStat; +class ExprManagerMapCollection; + +namespace expr { + namespace pickle { + class Pickler; + }/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ namespace context { class Context; @@ -404,6 +411,11 @@ public: Expr mkVar(const std::string& name, Type type); Expr mkVar(Type type); + /** Export an expr to a different ExprManager */ + //static Expr exportExpr(const Expr& e, ExprManager* em); + /** Export a type to a different ExprManager */ + static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap); + /** Returns the minimum arity of the given kind. */ static unsigned minArity(Kind kind); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 3c376f632..c510ce381 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -19,8 +19,10 @@ #include "expr/expr.h" #include "expr/node.h" #include "expr/expr_manager_scope.h" +#include "expr/variable_type_map.h" #include "util/Assert.h" +#include <vector> #include <iterator> #include <utility> @@ -30,7 +32,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 34 "${template}" +#line 36 "${template}" using namespace CVC4::kind; using namespace std; @@ -105,6 +107,72 @@ ExprManager* Expr::getExprManager() const { return d_exprManager; } +namespace expr { + +static Node exportConstant(TNode n, NodeManager* to); + +Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) { + if(n.getMetaKind() == kind::metakind::CONSTANT) { + return exportConstant(n, NodeManager::fromExprManager(to)); + } else if(n.getMetaKind() == kind::metakind::VARIABLE) { + Expr from_e(from, new Node(n)); + Expr& to_e = vmap.d_typeMap[from_e]; + if(! to_e.isNull()) { +Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl; + return to_e.getNode(); + } else { + // construct new variable in other manager: + // to_e is a ref, so this inserts from_e -> to_e + std::string name; + Type type = from->exportType(from_e.getType(), to, vmap); + if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) { + to_e = to->mkVar(name, type);// FIXME thread safety +Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl; + } else { + to_e = to->mkVar(type);// FIXME thread safety +Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl; + } + uint64_t to_int = (uint64_t)(to_e.getNode().d_nv); + uint64_t from_int = (uint64_t)(from_e.getNode().d_nv); + vmap.d_from[to_int] = from_int; + vmap.d_to[from_int] = to_int; + vmap.d_typeMap[to_e] = from_e;// insert other direction too + return Node::fromExpr(to_e); + } + } else { + std::vector<Node> children; +Debug("export") << "n: " << n << std::endl; + if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { +Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl; + children.reserve(n.getNumChildren() + 1); + children.push_back(exportInternal(n.getOperator(), from, to, vmap)); + } else { + children.reserve(n.getNumChildren()); + } + for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { +Debug("export") << "+ child: " << *i << std::endl; + children.push_back(exportInternal(*i, from, to, vmap)); + } + if(Debug.isOn("export")) { + ExprManagerScope ems(*to); + Debug("export") << "children for export from " << n << std::endl; + for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) { + Debug("export") << " child: " << *i << std::endl; + } + } + return NodeManager::fromExprManager(to)->mkNode(n.getKind(), children);// FIXME thread safety + } +}/* exportInternal() */ + +}/* CVC4::expr namespace */ + +Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Assert(d_exprManager != exprManager, + "No sense in cloning an Expr in the same ExprManager"); + ExprManagerScope ems(*this); + return Expr(exprManager, new Node(expr::exportInternal(*d_node, d_exprManager, exprManager, variableMap))); +} + Expr& Expr::operator=(const Expr& e) { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); @@ -449,4 +517,16 @@ void Expr::debugPrint() { ${getConst_implementations} +namespace expr { + +static Node exportConstant(TNode n, NodeManager* to) { + Assert(n.getMetaKind() == kind::metakind::CONSTANT); + switch(n.getKind()) { +${exportConstant_cases} + + default: Unhandled(n.getKind()); + } +}/* exportConstant() */ + +}/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index b54ec20d4..56396da01 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -49,6 +49,8 @@ namespace CVC4 { template <bool ref_count> class NodeTemplate; +class NodeManager; + class Expr; class ExprManager; class SmtEngine; @@ -56,6 +58,20 @@ class Type; class TypeCheckingException; class TypeCheckingExceptionPrivate; +namespace expr { + namespace pickle { + class Pickler; + }/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ + +namespace prop { + class SatSolver; +}/* CVC4::prop namespace */ + +class ExprManagerMapCollection; + +struct ExprHashFunction; + namespace smt { class SmtEnginePrivate; }/* CVC4::smt namespace */ @@ -64,6 +80,8 @@ namespace expr { class CVC4_PUBLIC ExprSetDepth; class CVC4_PUBLIC ExprPrintTypes; class CVC4_PUBLIC ExprSetLanguage; + + NodeTemplate<true> exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); }/* CVC4::expr namespace */ /** @@ -437,6 +455,13 @@ public: ExprManager* getExprManager() const; /** + * Maps this Expr into one for a different ExprManager, using + * variableMap for the translation and extending it with any new + * mappings. + */ + Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + + /** * IOStream manipulator to set the maximum depth of Exprs when * pretty-printing. -1 means print to any depth. E.g.: * @@ -510,6 +535,10 @@ protected: friend class ExprManager; friend class NodeManager; friend class TypeCheckingException; + friend class expr::pickle::Pickler; + friend class prop::SatSolver; + friend NodeTemplate<true> expr::exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); + friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e); template <bool ref_count> friend class NodeTemplate; @@ -828,7 +857,7 @@ public: ${getConst_instantiations} -#line 832 "${template}" +#line 861 "${template}" namespace expr { diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 69f7019ab..0cae68ed0 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -60,6 +60,7 @@ getConst_instantiations= getConst_implementations= mkConst_instantiations= mkConst_implementations= +exportConstant_cases= seen_theory=false seen_theory_builtin=false @@ -193,6 +194,8 @@ template <> $2 const & Expr::getConst() const { return d_node->getConst< $2 >(); } " + exportConstant_cases="${exportConstant_cases} + case $1: return to->mkConst(n.getConst< $2 >());" } function check_theory_seen { @@ -244,6 +247,7 @@ for var in \ getConst_implementations \ mkConst_instantiations \ mkConst_implementations \ + exportConstant_cases \ typechecker_includes \ typerules \ ; do diff --git a/src/expr/node.h b/src/expr/node.h index 57b02b05b..37499c3bf 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -49,6 +49,12 @@ namespace CVC4 { class TypeNode; class NodeManager; +namespace expr { + namespace pickle { + class PicklerPrivate; + }/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ + template <bool ref_count> class NodeTemplate; @@ -177,6 +183,9 @@ class NodeTemplate { */ friend class expr::NodeValue; + friend class expr::pickle::PicklerPrivate; + friend Node expr::exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); + /** A convenient null-valued encapsulated pointer */ static NodeTemplate s_null; @@ -200,6 +209,7 @@ class NodeTemplate { friend class NodeTemplate<true>; friend class NodeTemplate<false>; + friend class TypeNode; friend class NodeManager; template <unsigned nchild_thresh> diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index ded7ad8fe..c5d41816e 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -928,7 +928,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { // reference counts in this case. nv->d_nchildren = 0; nv->d_kind = d_nv->d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading nv->d_rc = 0; setUsed(); if(Debug.isOn("gc")) { @@ -1015,7 +1015,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { } nv->d_nchildren = d_inlineNv.d_nchildren; nv->d_kind = d_inlineNv.d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading nv->d_rc = 0; std::copy(d_inlineNv.d_children, @@ -1069,7 +1069,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { crop(); expr::NodeValue* nv = d_nv; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading d_nv = &d_inlineNv; d_nvMaxChildren = nchild_thresh; setUsed(); @@ -1118,7 +1118,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { // reference counts in this case. nv->d_nchildren = 0; nv->d_kind = d_nv->d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading nv->d_rc = 0; Debug("gc") << "creating node value " << nv << " [" << nv->d_id << "]: " << *nv << "\n"; @@ -1194,7 +1194,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { } nv->d_nchildren = d_inlineNv.d_nchildren; nv->d_kind = d_inlineNv.d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading nv->d_rc = 0; std::copy(d_inlineNv.d_children, @@ -1248,7 +1248,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { } nv->d_nchildren = d_nv->d_nchildren; nv->d_kind = d_nv->d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading nv->d_rc = 0; std::copy(d_nv->d_children, diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 2bf0a864a..1d4b7d3d1 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -84,6 +84,7 @@ NodeManager::NodeManager(context::Context* ctxt, d_optionsAllocated(new Options()), d_options(d_optionsAllocated), d_statisticsRegistry(new StatisticsRegistry()), + next_id(0), d_attrManager(ctxt), d_exprManager(exprManager), d_nodeUnderDeletion(NULL), @@ -98,6 +99,7 @@ NodeManager::NodeManager(context::Context* ctxt, d_optionsAllocated(NULL), d_options(&options), d_statisticsRegistry(new StatisticsRegistry()), + next_id(0), d_attrManager(ctxt), d_exprManager(exprManager), d_nodeUnderDeletion(NULL), diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 3646e91c5..e446b7d71 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -88,6 +88,8 @@ class NodeManager { NodeValuePool d_nodeValuePool; + size_t next_id; + expr::attr::AttributeManager d_attrManager; /** The associated ExprManager */ @@ -503,6 +505,60 @@ public: const AttrKind& attr, const typename AttrKind::value_type& value); + /** + * Retrieve an attribute for a TypeNode. + * + * @param n the type node + * @param attr an instance of the attribute kind to retrieve. + * @returns the attribute, if set, or a default-constructed + * <code>AttrKind::value_type</code> if not. + */ + template <class AttrKind> + inline typename AttrKind::value_type + getAttribute(TypeNode n, const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a TypeNode. + * + * @param n the type node + * @param attr an instance of the attribute kind to check + * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>. + */ + template <class AttrKind> + inline bool hasAttribute(TypeNode n, + const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a TypeNode and, if so, retieve + * it. + * + * @param n the type node + * @param attr an instance of the attribute kind to check + * @param value a reference to an object of the attribute's value type. + * <code>value</code> will be set to the value of the attribute, if it is + * set for <code>nv</code>; otherwise, it will be set to the default value of + * the attribute. + * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>. + */ + template <class AttrKind> + inline bool getAttribute(TypeNode n, + const AttrKind& attr, + typename AttrKind::value_type& value) const; + + /** + * Set an attribute for a type node. If the node doesn't have the + * attribute, this function assigns one. If the type node has one, + * this overwrites it. + * + * @param n the type node + * @param attr an instance of the attribute kind to set + * @param value the value of <code>attr</code> for <code>n</code> + */ + template <class AttrKind> + inline void setAttribute(TypeNode n, + const AttrKind& attr, + const typename AttrKind::value_type& value); + /** Get the (singleton) type for Booleans. */ inline TypeNode booleanType(); @@ -762,6 +818,32 @@ NodeManager::setAttribute(TNode n, const AttrKind&, d_attrManager.setAttribute(n.d_nv, AttrKind(), value); } +template <class AttrKind> +inline typename AttrKind::value_type +NodeManager::getAttribute(TypeNode n, const AttrKind&) const { + return d_attrManager.getAttribute(n.d_nv, AttrKind()); +} + +template <class AttrKind> +inline bool +NodeManager::hasAttribute(TypeNode n, const AttrKind&) const { + return d_attrManager.hasAttribute(n.d_nv, AttrKind()); +} + +template <class AttrKind> +inline bool +NodeManager::getAttribute(TypeNode n, const AttrKind&, + typename AttrKind::value_type& ret) const { + return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret); +} + +template <class AttrKind> +inline void +NodeManager::setAttribute(TypeNode n, const AttrKind&, + const typename AttrKind::value_type& value) { + d_attrManager.setAttribute(n.d_nv, AttrKind(), value); +} + /** Get the (singleton) type for booleans. */ inline TypeNode NodeManager::booleanType() { @@ -965,7 +1047,7 @@ inline TypeNode NodeManager::mkSort() { inline TypeNode NodeManager::mkSort(const std::string& name) { TypeNode type = mkSort(); - type.setAttribute(expr::VarNameAttr(), name); + setAttribute(type, expr::VarNameAttr(), name); return type; } @@ -986,7 +1068,7 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor, nb << sortTag; nb.append(children); TypeNode type = nb.constructTypeNode(); - type.setAttribute(expr::VarNameAttr(), name); + setAttribute(type, expr::VarNameAttr(), name); return type; } @@ -997,8 +1079,8 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name, Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); nb << sortTag; TypeNode type = nb.constructTypeNode(); - type.setAttribute(expr::VarNameAttr(), name); - type.setAttribute(expr::SortArityAttr(), arity); + setAttribute(type, expr::VarNameAttr(), name); + setAttribute(type, expr::SortArityAttr(), arity); return type; } @@ -1211,37 +1293,37 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { Node n = mkVar(type); - n.setAttribute(TypeAttr(), type); - n.setAttribute(expr::VarNameAttr(), name); + setAttribute(n, TypeAttr(), type); + setAttribute(n, expr::VarNameAttr(), name); return n; } inline Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) { Node* n = mkVarPtr(type); - n->setAttribute(TypeAttr(), type); - n->setAttribute(expr::VarNameAttr(), name); + setAttribute(*n, TypeAttr(), type); + setAttribute(*n, expr::VarNameAttr(), name); return n; } inline Node NodeManager::mkVar(const TypeNode& type) { Node n = NodeBuilder<0>(this, kind::VARIABLE); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); return n; } inline Node* NodeManager::mkVarPtr(const TypeNode& type) { Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); - n->setAttribute(TypeAttr(), type); - n->setAttribute(TypeCheckedAttr(), true); + setAttribute(*n, TypeAttr(), type); + setAttribute(*n, TypeCheckedAttr(), true); return n; } inline Node NodeManager::mkSkolem(const TypeNode& type) { Node n = NodeBuilder<0>(this, kind::SKOLEM); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); return n; } @@ -1282,7 +1364,7 @@ NodeClass NodeManager::mkConstInternal(const T& val) { nv->d_nchildren = 0; nv->d_kind = kind::metakind::ConstantMap<T>::kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = next_id++;// FIXME multithreading nv->d_rc = 0; //OwningTheory::mkConst(val); diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 89ac7ffca..970d2e0fc 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -33,8 +33,6 @@ using namespace std; namespace CVC4 { namespace expr { -size_t NodeValue::next_id = 1; - NodeValue NodeValue::s_null(0); string NodeValue::toString() const { diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 95af57719..e5ecfbc48 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -126,8 +126,6 @@ class NodeValue { void inc(); void dec(); - static size_t next_id; - /** * Uninitializing constructor for NodeBuilder's use. */ diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp new file mode 100644 index 000000000..1de8f2cf7 --- /dev/null +++ b/src/expr/pickle_data.cpp @@ -0,0 +1,60 @@ +/********************* */ +/*! \file pickle_data.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 This is a "pickle" for expressions, CVC4-internal view + ** + ** This is the CVC4-internal view (private data structure) for a + ** "pickle" for expressions. The public-facing view is a "Pickle", + ** which just points to a PickleData. A pickle is a binary + ** serialization of an expression that can be converted back into an + ** expression in the same or another ExprManager. + **/ + +#include <iostream> +#include <sstream> +#include <string> + +#include "expr/pickle_data.h" +#include "expr/expr.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/node_value.h" +#include "expr/expr_manager_scope.h" +#include "expr/variable_type_map.h" +#include "util/Assert.h" +#include "expr/kind.h" +#include "expr/metakind.h" + +namespace CVC4 { +namespace expr { +namespace pickle { + +void PickleData::writeToStringStream(std::ostringstream& oss) const { + BlockDeque::const_iterator i = d_blocks.begin(), end = d_blocks.end(); + for(; i != end; ++i) { + Block b = *i; + Assert(sizeof(b) * 8 == NBITS_BLOCK); + oss << b.d_body.d_data << " "; + } +} + +std::string PickleData::toString() const { + std::ostringstream oss; + oss.flags(std::ios::oct | std::ios::showbase); + writeToStringStream(oss); + return oss.str(); +} + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h new file mode 100644 index 000000000..dab6e56c3 --- /dev/null +++ b/src/expr/pickle_data.h @@ -0,0 +1,122 @@ +/********************* */ +/*! \file pickle_data.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 This is a "pickle" for expressions, CVC4-internal view + ** + ** This is the CVC4-internal view (private data structure) for a + ** "pickle" for expressions. The public-facing view is a "Pickle", + ** which just points to a PickleData. A pickle is a binary + ** serialization of an expression that can be converted back into an + ** expression in the same or another ExprManager. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PICKLE_DATA_H +#define __CVC4__PICKLE_DATA_H + +#include <sstream> +#include <deque> +#include <stack> +#include <exception> + +#include "expr/expr.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/expr_manager.h" +#include "expr/variable_type_map.h" +#include "expr/kind.h" +#include "expr/metakind.h" + +namespace CVC4 { + +class NodeManager; + +namespace expr { +namespace pickle { + +const unsigned NBITS_BLOCK = 32; +const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND; +const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; +const unsigned NBITS_CONSTBLOCKS = 32; + +struct BlockHeader { + unsigned d_kind : NBITS_KIND; +};/* struct BlockHeader */ + +struct BlockHeaderOperator { + unsigned d_kind : NBITS_KIND; + unsigned d_nchildren : NBITS_NCHILDREN; + unsigned : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN); +};/* struct BlockHeaderOperator */ + +struct BlockHeaderConstant { + unsigned d_kind : NBITS_KIND; + unsigned d_constblocks : NBITS_BLOCK - NBITS_KIND; +};/* struct BlockHeaderConstant */ + +struct BlockHeaderVariable { + unsigned d_kind : NBITS_KIND; + unsigned : NBITS_BLOCK - NBITS_KIND; +};/* struct BlockHeaderVariable */ + +struct BlockBody { + unsigned d_data : NBITS_BLOCK; +};/* struct BlockBody */ + +union Block { + BlockHeader d_header; + BlockHeaderConstant d_headerConstant; + BlockHeaderOperator d_headerOperator; + BlockHeaderVariable d_headerVariable; + + BlockBody d_body; +};/* union Block */ + +class PickleData { + typedef std::deque<Block> BlockDeque; + BlockDeque d_blocks; + +public: + PickleData& operator<<(Block b) { + enqueue(b); + return (*this); + } + + std::string toString() const; + + void enqueue(Block b) { + d_blocks.push_back(b); + } + + Block dequeue() { + Block b = d_blocks.front(); + d_blocks.pop_front(); + return b; + } + + bool empty() const { return d_blocks.empty(); } + uint32_t size() const { return d_blocks.size(); } + + void swap(PickleData& other){ + d_blocks.swap(other.d_blocks); + } + + void writeToStringStream(std::ostringstream& oss) const; +};/* class PickleData */ + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PICKLE_DATA_H */ diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp new file mode 100644 index 000000000..f09c552d1 --- /dev/null +++ b/src/expr/pickler.cpp @@ -0,0 +1,477 @@ +/********************* */ +/*! \file pickler.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 This is a "pickler" for expressions + ** + ** This is a "pickler" for expressions. It produces a binary + ** serialization of an expression that can be converted back + ** into an expression in the same or another ExprManager. + **/ + +#include <iostream> +#include <sstream> +#include <string> + +#include "expr/pickler.h" +#include "expr/pickle_data.h" +#include "expr/expr.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/node_value.h" +#include "expr/expr_manager_scope.h" +#include "expr/variable_type_map.h" +#include "util/Assert.h" +#include "expr/kind.h" +#include "expr/metakind.h" +#include "util/output.h" + +namespace CVC4 { +namespace expr { +namespace pickle { + +class PicklerPrivate { +public: + typedef std::stack<Node> NodeStack; + NodeStack d_stack; + + PickleData d_current; + + Pickler& d_pickler; + + NodeManager* const d_nm; + + PicklerPrivate(Pickler& pickler, ExprManager* em) : + d_pickler(pickler), + d_nm(NodeManager::fromExprManager(em)) { + } + + bool atDefaultState(){ + return d_stack.empty() && d_current.empty(); + } + + /* Helper functions for toPickle */ + void toCaseNode(TNode n) throw(AssertionException, PicklingException); + void toCaseVariable(TNode n) throw(AssertionException, PicklingException); + void toCaseConstant(TNode n); + void toCaseOperator(TNode n) throw(AssertionException, PicklingException); + void toCaseString(Kind k, const std::string& s); + + /* Helper functions for toPickle */ + Node fromCaseOperator(Kind k, uint32_t nchildren); + Node fromCaseConstant(Kind k, uint32_t nblocks); + std::string fromCaseString(uint32_t nblocks); + Node fromCaseVariable(Kind k); + +};/* class PicklerPrivate */ + +static Block mkBlockBody4Chars(char a, char b, char c, char d) { + Block newBody; + newBody.d_body.d_data = (a << 24) | (b << 16) | (c << 8) | d; + return newBody; +} + +static char getCharBlockBody(BlockBody body, int i) { + Assert(0 <= i && i <= 3); + + switch(i) { + case 0: return (body.d_data & 0xff000000) >> 24; + case 1: return (body.d_data & 0x00ff0000) >> 16; + case 2: return (body.d_data & 0x0000ff00) >> 8; + case 3: return (body.d_data & 0x000000ff); + default: + Unreachable(); + } + return '\0'; +} + +static Block mkBlockBody(unsigned data) { + Block newBody; + newBody.d_body.d_data = data; + return newBody; +} + +static Block mkOperatorHeader(Kind k, unsigned numChildren) { + Block newHeader; + newHeader.d_headerOperator.d_kind = k; + newHeader.d_headerOperator.d_nchildren = numChildren; + return newHeader; +} + +static Block mkVariableHeader(Kind k) { + Block newHeader; + newHeader.d_header.d_kind = k; + return newHeader; +} + +static Block mkConstantHeader(Kind k, unsigned numBlocks) { + Block newHeader; + newHeader.d_headerConstant.d_kind = k; + newHeader.d_headerConstant.d_constblocks = numBlocks; + return newHeader; +} + +Pickler::Pickler(ExprManager* em) : + d_private(new PicklerPrivate(*this, em)) { +} + +Pickler::~Pickler() { + delete d_private; +} + +void Pickler::toPickle(Expr e, Pickle& p) + throw(AssertionException, PicklingException) { + Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm); + Assert(d_private->atDefaultState()); + + try{ + d_private->d_current.swap(*p.d_data); + d_private->toCaseNode(e.getTNode()); + d_private->d_current.swap(*p.d_data); + }catch(PicklingException& pe){ + d_private->d_current = PickleData(); + Assert(d_private->atDefaultState()); + throw pe; + } + + Assert(d_private->atDefaultState()); +} + +void PicklerPrivate::toCaseNode(TNode n) + throw(AssertionException, PicklingException) { + Debug("pickler") << "toCaseNode: " << n << std::endl; + Kind k = n.getKind(); + kind::MetaKind m = metaKindOf(k); + switch(m) { + case kind::metakind::CONSTANT: + toCaseConstant(n); + break; + case kind::metakind::VARIABLE: + toCaseVariable(n); + break; + case kind::metakind::OPERATOR: + case kind::metakind::PARAMETERIZED: + toCaseOperator(n); + break; + default: + Unhandled(m); + } +} + +void PicklerPrivate::toCaseOperator(TNode n) + throw(AssertionException, PicklingException) { + Kind k = n.getKind(); + kind::MetaKind m = metaKindOf(k); + Assert(m == kind::metakind::PARAMETERIZED || m == kind::metakind::OPERATOR); + if(m == kind::metakind::PARAMETERIZED) { + toCaseNode(n.getOperator()); + } + for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { + toCaseNode(*i); + } + d_current << mkOperatorHeader(k, n.getNumChildren()); +} + +void PicklerPrivate::toCaseVariable(TNode n) + throw(AssertionException, PicklingException) { + Kind k = n.getKind(); + Assert(metaKindOf(k) == kind::metakind::VARIABLE); + + const NodeValue* nv = n.d_nv; + uint64_t asInt = reinterpret_cast<uint64_t>(nv); + uint64_t mapped = d_pickler.variableToMap(asInt); + + uint32_t firstHalf = mapped >> 32; + uint32_t secondHalf = mapped & 0xffffffff; + + d_current << mkVariableHeader(k); + d_current << mkBlockBody(firstHalf); + d_current << mkBlockBody(secondHalf); +} + + +void PicklerPrivate::toCaseConstant(TNode n) { + Kind k = n.getKind(); + Assert(metaKindOf(k) == kind::metakind::CONSTANT); + switch(k) { + case kind::CONST_BOOLEAN: + d_current << mkConstantHeader(k, 1); + d_current << mkBlockBody(n.getConst<bool>()); + break; + case kind::CONST_INTEGER: + case kind::CONST_RATIONAL: { + std::string asString; + if(k == kind::CONST_INTEGER) { + const Integer& i = n.getConst<Integer>(); + asString = i.toString(16); + } else { + Assert(k == kind::CONST_RATIONAL); + const Rational& q = n.getConst<Rational>(); + asString = q.toString(16); + } + toCaseString(k, asString); + break; + } + case kind::BITVECTOR_EXTRACT_OP: { + BitVectorExtract bve = n.getConst<BitVectorExtract>(); + d_current << mkConstantHeader(k, 2); + d_current << mkBlockBody(bve.high); + d_current << mkBlockBody(bve.low); + break; + } + case kind::CONST_BITVECTOR: { + // irritating: we incorporate the size of the string in with the + // size of this constant, so it appears as one big constant and + // doesn't confuse anybody + BitVector bv = n.getConst<BitVector>(); + std::string asString = bv.getValue().toString(16); + d_current << mkConstantHeader(k, 2 + asString.size()); + d_current << mkBlockBody(bv.getSize()); + toCaseString(k, asString); + break; + } + default: + Unhandled(k); + } +} + +void PicklerPrivate::toCaseString(Kind k, const std::string& s) { + d_current << mkConstantHeader(k, s.size()); + + unsigned size = s.size(); + unsigned i; + for(i = 0; i + 4 <= size; i += 4) { + d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], s[i + 3]); + } + switch(size % 4) { + case 0: break; + case 1: d_current << mkBlockBody4Chars(s[i + 0], '\0','\0', '\0'); break; + case 2: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1], '\0', '\0'); break; + case 3: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], '\0'); break; + default: + Unreachable(); + } + +} + +void Pickler::debugPickleTest(Expr e) { + + //ExprManager *em = e.getExprManager(); + //Expr e1 = mkVar("x", makeType()); + //return ; + + Pickler pickler(e.getExprManager()); + + Pickle p; + pickler.toPickle(e, p); + + uint32_t size = p.d_data->size(); + std::string str = p.d_data->toString(); + + Expr from = pickler.fromPickle(p); + ExprManagerScope ems(e); + + Debug("pickle") << "before: " << e << std::endl; + Debug("pickle") << "after: " << from.getNode() << std::endl; + Debug("pickle") << "pickle: (oct) "<< size << " " << str.length() << " " << str << std::endl; + + Assert(p.d_data->empty()); + Assert(e == from); +} + +Expr Pickler::fromPickle(Pickle& p) { + Assert(d_private->atDefaultState()); + + d_private->d_current.swap(*p.d_data); + + while(!d_private->d_current.empty()) { + Block front = d_private->d_current.dequeue(); + + Kind k = (Kind)front.d_header.d_kind; + kind::MetaKind m = metaKindOf(k); + + Node result = Node::null(); + switch(m) { + case kind::metakind::VARIABLE: + result = d_private->fromCaseVariable(k); + break; + case kind::metakind::CONSTANT: + result = d_private->fromCaseConstant(k, front.d_headerConstant.d_constblocks); + break; + case kind::metakind::OPERATOR: + case kind::metakind::PARAMETERIZED: + result = d_private->fromCaseOperator(k, front.d_headerOperator.d_nchildren); + break; + default: + Unhandled(m); + } + Assert(result != Node::null()); + d_private->d_stack.push(result); + } + + Assert(d_private->d_current.empty()); + Assert(d_private->d_stack.size() == 1); + Node res = d_private->d_stack.top(); + d_private->d_stack.pop(); + + Assert(d_private->atDefaultState()); + + return d_private->d_nm->toExpr(res); +} + +Node PicklerPrivate::fromCaseVariable(Kind k) { + Assert(metaKindOf(k) == kind::metakind::VARIABLE); + + Block firstHalf = d_current.dequeue(); + Block secondHalf = d_current.dequeue(); + + uint64_t asInt = firstHalf.d_body.d_data; + asInt = asInt << 32; + asInt = asInt | (secondHalf.d_body.d_data); + + uint64_t mapped = d_pickler.variableFromMap(asInt); + + NodeValue* nv = reinterpret_cast<NodeValue*>(mapped); + Node fromNodeValue(nv); + + Assert(fromNodeValue.getKind() == k); + + return fromNodeValue; +} + +Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) { + switch(k) { + case kind::CONST_BOOLEAN: { + Assert(constblocks == 1); + Block val = d_current.dequeue(); + + bool b= val.d_body.d_data; + return d_nm->mkConst<bool>(b); + } + case kind::CONST_INTEGER: + case kind::CONST_RATIONAL: { + std::string s = fromCaseString(constblocks); + if(k == kind::CONST_INTEGER) { + Integer i(s, 16); + return d_nm->mkConst<Integer>(i); + } else { + Rational q(s, 16); + return d_nm->mkConst<Rational>(q); + } + } + case kind::BITVECTOR_EXTRACT_OP: { + Block high = d_current.dequeue(); + Block low = d_current.dequeue(); + BitVectorExtract bve(high.d_body.d_data, low.d_body.d_data); + return d_nm->mkConst<BitVectorExtract>(bve); + } + case kind::CONST_BITVECTOR: { + unsigned size = d_current.dequeue().d_body.d_data; + Block header CVC4_UNUSED = d_current.dequeue(); + Assert(header.d_headerConstant.d_kind == kind::CONST_BITVECTOR); + Assert(header.d_headerConstant.d_constblocks == constblocks - 2); + Integer value(fromCaseString(constblocks - 2)); + BitVector bv(size, value); + return d_nm->mkConst(bv); + } + default: + Unhandled(k); + } +} + +std::string PicklerPrivate::fromCaseString(uint32_t size) { + std::stringstream ss; + unsigned i; + for(i = 0; i + 4 <= size; i += 4) { + Block front = d_current.dequeue(); + BlockBody body = front.d_body; + + ss << getCharBlockBody(body,0) + << getCharBlockBody(body,1) + << getCharBlockBody(body,2) + << getCharBlockBody(body,3); + } + Assert(i == size - (size%4) ); + if(size % 4 != 0) { + Block front = d_current.dequeue(); + BlockBody body = front.d_body; + switch(size % 4) { + case 1: + ss << getCharBlockBody(body,0); + break; + case 2: + ss << getCharBlockBody(body,0) + << getCharBlockBody(body,1); + break; + case 3: + ss << getCharBlockBody(body,0) + << getCharBlockBody(body,1) + << getCharBlockBody(body,2); + break; + default: + Unreachable(); + } + } + return ss.str(); +} + +Node PicklerPrivate::fromCaseOperator(Kind k, uint32_t nchildren) { + kind::MetaKind m = metaKindOf(k); + bool parameterized = (m == kind::metakind::PARAMETERIZED); + uint32_t npops = nchildren + (parameterized? 1 : 0); + + NodeStack aux; + while(npops > 0) { + Assert(!d_stack.empty()); + Node top = d_stack.top(); + aux.push(top); + d_stack.pop(); + --npops; + } + + NodeBuilder<> nb(d_nm, k); + while(!aux.empty()) { + Node top = aux.top(); + nb << top; + aux.pop(); + } + + return nb; +} + +Pickle::Pickle() { + d_data = new PickleData(); +} + +// Just copying the pointer isn't right, we have to copy the +// underlying data. Otherwise user-level Pickles will delete the data +// twice! (once in each thread) +Pickle::Pickle(const Pickle& p) { + d_data = new PickleData(*p.d_data); +} + +Pickle& Pickle::operator = (const Pickle& other) { + if (this != &other) { + delete d_data; + d_data = new PickleData(*other.d_data); + } + return *this; +} + + +Pickle::~Pickle() { + delete d_data; +} + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/pickler.h b/src/expr/pickler.h new file mode 100644 index 000000000..264ae0e4b --- /dev/null +++ b/src/expr/pickler.h @@ -0,0 +1,139 @@ +/********************* */ +/*! \file pickle.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 This is a "pickler" for expressions + ** + ** This is a "pickler" for expressions. It produces a binary + ** serialization of an expression that can be converted back + ** into an expression in the same or another ExprManager. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__PICKLER_H +#define __CVC4__PICKLER_H + +#include "expr/variable_type_map.h" +#include "expr/expr.h" +#include "util/exception.h" + +#include <exception> +#include <stack> + +namespace CVC4 { + +class ExprManager; + +namespace expr { +namespace pickle { + +class Pickler; +class PicklerPrivate; + +class PickleData;// CVC4-internal representation + +class CVC4_PUBLIC Pickle { + PickleData* d_data; + friend class Pickler; + friend class PicklerPrivate; +public: + Pickle(); + Pickle(const Pickle& p); + ~Pickle(); + Pickle& operator = (const Pickle& other); +};/* class Pickle */ + +class CVC4_PUBLIC PicklingException : public Exception { +public: + PicklingException() : + Exception("Pickling failed") { + } +};/* class PicklingException */ + +class CVC4_PUBLIC Pickler { + PicklerPrivate* d_private; + + friend class PicklerPrivate; + +protected: + virtual uint64_t variableToMap(uint64_t x) const + throw(AssertionException, PicklingException) { + return x; + } + virtual uint64_t variableFromMap(uint64_t x) const { + return x; + } + +public: + Pickler(ExprManager* em); + ~Pickler(); + + /** + * Constructs a new Pickle of the node n. + * n must be a node allocated in the node manager specified at initialization + * time. The new pickle has variables mapped using the VariableIDMap provided + * at initialization. + * TODO: Fix comment + * + * @return the pickle, which should be dispose()'d when you're done with it + */ + void toPickle(Expr e, Pickle& p) throw(AssertionException, PicklingException); + + /** + * Constructs a node from a Pickle. + * This destroys the contents of the Pickle. + * The node is created in the NodeManager getNM(); + * TODO: Fix comment + */ + Expr fromPickle(Pickle& p); + + static void debugPickleTest(Expr e); + +};/* class Pickler */ + +class MapPickler : public Pickler { +private: + const VarMap& d_toMap; + const VarMap& d_fromMap; + +public: + MapPickler(ExprManager* em, const VarMap& to, const VarMap& from): + Pickler(em), + d_toMap(to), + d_fromMap(from) { + } + +protected: + + virtual uint64_t variableToMap(uint64_t x) const + throw(AssertionException, PicklingException){ + VarMap::const_iterator i = d_toMap.find(x); + if(i != d_toMap.end()){ + return i->second; + }else{ + throw PicklingException(); + } + } + + virtual uint64_t variableFromMap(uint64_t x) const { + VarMap::const_iterator i = d_fromMap.find(x); + Assert(i != d_fromMap.end()); + return i->second; + } +};/* class MapPickler */ + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PICKLER_H */ diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 7e06a05ae..a901af73a 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -162,6 +162,10 @@ ExprManager* Type::getExprManager() const { return d_nodeManager->toExprManager(); } +Type Type::exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) { + return ExprManager::exportType(*this, exprManager, vmap); +} + void Type::toStream(std::ostream& out) const { NodeManagerScope nms(d_nodeManager); out << *d_typeNode; diff --git a/src/expr/type.h b/src/expr/type.h index 0b50fbd3c..34cc925f6 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -35,6 +35,7 @@ class NodeManager; class ExprManager; class Expr; class TypeNode; +class ExprManagerMapCollection; class SmtEngine; @@ -75,6 +76,10 @@ struct CVC4_PUBLIC TypeHashFunction { */ std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC; +namespace expr { + TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap); +}/* CVC4::expr namespace */ + /** * Class encapsulating CVC4 expression types. */ @@ -86,6 +91,7 @@ class CVC4_PUBLIC Type { friend class TypeNode; friend struct TypeHashStrategy; friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t); + friend TypeNode expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap); protected: @@ -166,6 +172,11 @@ public: ExprManager* getExprManager() const; /** + * Exports this type into a different ExprManager. + */ + Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap); + + /** * Assignment operator. * @param t the type to assign to this type * @return this type after assignment. diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 553f83276..c7da5ceb7 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -229,6 +229,16 @@ public: } /** + * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these) + * have an operator. "Little-p parameterized" types (like Array), + * are OPERATORs, not PARAMETERIZEDs. + */ + inline Node getOperator() const { + Assert(getMetaKind() == kind::metakind::PARAMETERIZED); + return Node(d_nv->getChild(-1)); + } + + /** * Returns the unique id of this node * * @return the id diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h new file mode 100644 index 000000000..a34bec846 --- /dev/null +++ b/src/expr/variable_type_map.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \file variable_type_map.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, 2010, 2011 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__VARIABLE_TYPE_MAP_H +#define __CVC4__VARIABLE_TYPE_MAP_H + +#include "expr/expr.h" +#include "util/hash.h" + +namespace CVC4 { + +class Expr; +struct ExprHashFunction; +class Type; +struct TypeHashFunction; + +class CVC4_PUBLIC VariableTypeMap { + /** + * A map Expr -> Expr, intended to be used for a mapping of variables + * between two ExprManagers. + */ + std::hash_map<Expr, Expr, ExprHashFunction> d_variables; + + /** + * A map Type -> Type, intended to be used for a mapping of types + * between two ExprManagers. + */ + std::hash_map<Type, Type, TypeHashFunction> d_types; + +public: + Expr& operator[](Expr e) { return d_variables[e]; } + Type& operator[](Type t) { return d_types[t]; } + +};/* class VariableTypeMap */ + +typedef __gnu_cxx::hash_map<uint64_t, uint64_t> VarMap; + +struct CVC4_PUBLIC ExprManagerMapCollection { + VariableTypeMap d_typeMap; + VarMap d_to; + VarMap d_from; +}; + +}/* CVC4 namespace */ + +#endif /* __CVC4__VARIABLE_MAP_H */ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 78d468000..ae7764e32 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -4,16 +4,42 @@ AM_CPPFLAGS = \ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas bin_PROGRAMS = cvc4 + noinst_LIBRARIES = libmain.a libmain_a_SOURCES = \ interactive_shell.h \ interactive_shell.cpp \ main.h \ - main.cpp \ util.cpp -cvc4_SOURCES = +if CVC4_HAS_THREADS +bin_PROGRAMS += pcvc4 +pcvc4_SOURCES = \ + main.cpp \ + portfolio.cpp \ + portfolio.h \ + driver_portfolio.cpp +pcvc4_LDADD = \ + libmain.a \ + @builddir@/../parser/libcvc4parser.la \ + @builddir@/../libcvc4.la \ + @builddir@/../lib/libreplacements.la \ + $(READLINE_LIBS) +pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS) +pcvc4_LDADD += $(BOOST_THREAD_LIBS) -lpthread +pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS) + +if STATIC_BINARY +pcvc4_LINK = $(CXXLINK) -all-static +else +pcvc4_LINK = $(CXXLINK) +endif +endif + +cvc4_SOURCES = \ + main.cpp \ + driver.cpp cvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @@ -44,3 +70,4 @@ cvc4_LINK = $(CXXLINK) -all-static else cvc4_LINK = $(CXXLINK) endif + diff --git a/src/main/driver.cpp b/src/main/driver.cpp new file mode 100644 index 000000000..e9bfde024 --- /dev/null +++ b/src/main/driver.cpp @@ -0,0 +1,355 @@ +/********************* */ +/*! \file driver.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: cconway + ** Minor contributors (to current version): barrett, dejan, taking + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011, 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 Driver for (sequential) CVC4 executable + ** + ** Driver for (sequential) CVC4 executable. + **/ + +#include <cstdlib> +#include <cstring> +#include <fstream> +#include <iostream> +#include <new> + +#include <stdio.h> +#include <unistd.h> + +#include "cvc4autoconfig.h" +#include "main/main.h" +#include "main/interactive_shell.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "parser/parser_exception.h" +#include "expr/expr_manager.h" +#include "smt/smt_engine.h" +#include "expr/command.h" +#include "util/Assert.h" +#include "util/configuration.h" +#include "util/options.h" +#include "util/output.h" +#include "util/result.h" +#include "util/stats.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::main; + +static bool doCommand(SmtEngine&, Command*, Options&); + +namespace CVC4 { + namespace main { + /** Global options variable */ + CVC4_THREADLOCAL(Options*) pOptions; + + /** Full argv[0] */ + const char *progPath; + + /** Just the basename component of argv[0] */ + const char *progName; + + /** A pointer to the StatisticsRegistry (the signal handlers need it) */ + CVC4::StatisticsRegistry* pStatistics; + } +} + + +void printUsage(Options& options, bool full) { + stringstream ss; + ss << "usage: " << options.binary_name << " [options] [input-file]" << endl + << endl + << "Without an input file, or with `-', CVC4 reads from standard input." << endl + << endl + << "CVC4 options:" << endl; + if(full) { + Options::printUsage( ss.str(), *options.out ); + } else { + Options::printShortUsage( ss.str(), *options.out ); + } +} + +int runCvc4(int argc, char* argv[], Options& options) { + + // For the signal handlers' benefit + pOptions = &options; + + // Initialize the signal handlers + cvc4_init(); + + progPath = argv[0]; + + // Parse the options + int firstArgIndex = options.parseOptions(argc, argv); + + progName = options.binary_name.c_str(); + + if( options.help ) { + printUsage(options, true); + exit(1); + } else if( options.languageHelp ) { + Options::printLanguageHelp(*options.out); + exit(1); + } else if( options.version ) { + *options.out << Configuration::about().c_str() << flush; + exit(0); + } + + segvNoSpin = options.segvNoSpin; + + // If in competition mode, set output stream option to flush immediately +#ifdef CVC4_COMPETITION_MODE + *options.out << unitbuf; +#endif + + // We only accept one input file + if(argc > firstArgIndex + 1) { + throw Exception("Too many input files specified."); + } + + // If no file supplied we will read from standard input + const bool inputFromStdin = + firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); + + // if we're reading from stdin on a TTY, default to interactive mode + if(!options.interactiveSetByUser) { + options.interactive = inputFromStdin && isatty(fileno(stdin)); + } + + // Determine which messages to show based on smtcomp_mode and verbosity + if(Configuration::isMuzzledBuild()) { + Debug.setStream(CVC4::null_os); + Trace.setStream(CVC4::null_os); + Notice.setStream(CVC4::null_os); + Chat.setStream(CVC4::null_os); + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + Dump.setStream(CVC4::null_os); + } else { + if(options.verbosity < 2) { + Chat.setStream(CVC4::null_os); + } + if(options.verbosity < 1) { + Notice.setStream(CVC4::null_os); + } + if(options.verbosity < 0) { + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + } + } + + // Create the expression manager + ExprManager exprMgr(options); + + // Create the SmtEngine + SmtEngine smt(&exprMgr); + + // signal handlers need access + pStatistics = smt.getStatisticsRegistry(); + + // Auto-detect input language by filename extension + const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex]; + + ReferenceStat< const char* > s_statFilename("filename", filename); + RegisterStatistic statFilenameReg(exprMgr, &s_statFilename); + + if(options.inputLanguage == language::input::LANG_AUTO) { + if( inputFromStdin ) { + // We can't do any fancy detection on stdin + options.inputLanguage = language::input::LANG_CVC4; + } else { + unsigned len = strlen(filename); + if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { + options.inputLanguage = language::input::LANG_SMTLIB_V2; + } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { + options.inputLanguage = language::input::LANG_SMTLIB; + } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) + || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { + options.inputLanguage = language::input::LANG_CVC4; + } + } + } + + if(options.outputLanguage == language::output::LANG_AUTO) { + options.outputLanguage = language::toOutputLanguage(options.inputLanguage); + } + + // Determine which messages to show based on smtcomp_mode and verbosity + if(Configuration::isMuzzledBuild()) { + Debug.setStream(CVC4::null_os); + Trace.setStream(CVC4::null_os); + Notice.setStream(CVC4::null_os); + Chat.setStream(CVC4::null_os); + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + Dump.setStream(CVC4::null_os); + } else { + if(options.verbosity < 2) { + Chat.setStream(CVC4::null_os); + } + if(options.verbosity < 1) { + Notice.setStream(CVC4::null_os); + } + if(options.verbosity < 0) { + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + } + + Debug.getStream() << Expr::setlanguage(options.outputLanguage); + Trace.getStream() << Expr::setlanguage(options.outputLanguage); + Notice.getStream() << Expr::setlanguage(options.outputLanguage); + Chat.getStream() << Expr::setlanguage(options.outputLanguage); + Message.getStream() << Expr::setlanguage(options.outputLanguage); + Warning.getStream() << Expr::setlanguage(options.outputLanguage); + Dump.getStream() << Expr::setlanguage(options.outputLanguage) + << Expr::setdepth(-1) + << Expr::printtypes(false); + } + + Parser* replayParser = NULL; + if( options.replayFilename != "" ) { + ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options); + + if( options.replayFilename == "-") { + if( inputFromStdin ) { + throw OptionException("Replay file and input file can't both be stdin."); + } + replayParserBuilder.withStreamInput(cin); + } + replayParser = replayParserBuilder.build(); + options.replayStream = new Parser::ExprStream(replayParser); + } + if( options.replayLog != NULL ) { + *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1); + } + + // Parse and execute commands until we are done + Command* cmd; + bool status = true; + if( options.interactive ) { + InteractiveShell shell(exprMgr, options); + Message() << Configuration::getPackageName() + << " " << Configuration::getVersionString(); + if(Configuration::isSubversionBuild()) { + Message() << " [" << Configuration::getSubversionId() << "]"; + } + Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") + << " assertions:" + << (Configuration::isAssertionBuild() ? "on" : "off") + << endl; + if(replayParser != NULL) { + // have the replay parser use the declarations input interactively + replayParser->useDeclarationsFrom(shell.getParser()); + } + while((cmd = shell.readCommand())) { + status = doCommand(smt,cmd, options) && status; + delete cmd; + } + } else { + ParserBuilder parserBuilder(&exprMgr, filename, options); + + if( inputFromStdin ) { + parserBuilder.withStreamInput(cin); + } + + Parser *parser = parserBuilder.build(); + if(replayParser != NULL) { + // have the replay parser use the file's declarations + replayParser->useDeclarationsFrom(parser); + } + while((cmd = parser->nextCommand())) { + status = doCommand(smt, cmd, options) && status; + delete cmd; + } + // Remove the parser + delete parser; + } + + if( options.replayStream != NULL ) { + // this deletes the expression parser too + delete options.replayStream; + options.replayStream = NULL; + } + + int returnValue; + string result = "unknown"; + if(status) { + result = smt.getInfo(":status").getValue(); + + if(result == "sat") { + returnValue = 10; + } else if(result == "unsat") { + returnValue = 20; + } else { + returnValue = 0; + } + } else { + // there was some kind of error + returnValue = 1; + } + +#ifdef CVC4_COMPETITION_MODE + // exit, don't return + // (don't want destructors to run) + exit(returnValue); +#endif + + ReferenceStat< Result > s_statSatResult("sat/unsat", result); + RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult); + + if(options.statistics) { + pStatistics->flushInformation(*options.err); + } + + return returnValue; +} + +/** Executes a command. Deletes the command after execution. */ +static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { + if( options.parseOnly ) { + return true; + } + + // assume no error + bool status = true; + + CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd); + if(seq != NULL) { + for(CommandSequence::iterator subcmd = seq->begin(); + subcmd != seq->end(); + ++subcmd) { + status = doCommand(smt, *subcmd, options) && status; + } + } else { + // by default, symmetry breaker is on only for QF_UF + if(! options.ufSymmetryBreakerSetByUser) { + SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd); + if(logic != NULL) { + options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF"); + } + } + + if(options.verbosity > 0) { + *options.out << "Invoking: " << *cmd << endl; + } + + if(options.verbosity >= 0) { + cmd->invoke(&smt, *options.out); + } else { + cmd->invoke(&smt); + } + status = status && cmd->ok(); + } + + return status; +} diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp new file mode 100644 index 000000000..5c8f908f8 --- /dev/null +++ b/src/main/driver_portfolio.cpp @@ -0,0 +1,808 @@ +#include <cstdio> +#include <cstdlib> +#include <iostream> +#include <sys/time.h> // for gettimeofday() + +#include <queue> + +#include <boost/thread.hpp> +#include <boost/thread/condition.hpp> +#include <boost/exception_ptr.hpp> +#include <boost/lexical_cast.hpp> + +#include "cvc4autoconfig.h" +#include "main/main.h" +#include "main/interactive_shell.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "parser/parser_exception.h" +#include "expr/expr_manager.h" +#include "expr/variable_type_map.h" +#include "smt/smt_engine.h" +#include "expr/command.h" +#include "util/Assert.h" +#include "util/configuration.h" +#include "util/options.h" +#include "util/output.h" +#include "util/result.h" +#include "util/stats.h" + +#include "expr/pickler.h" +#include "util/channel.h" + +#include "main/portfolio.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::main; + +/* Global variables */ + +namespace CVC4 { + namespace main { + + StatisticsRegistry theStatisticsRegistry; + + /** A pointer to the StatisticsRegistry (the signal handlers need it) */ + CVC4::StatisticsRegistry* pStatistics; + + }/* CVC4::main namespace */ +}/* CVC4 namespace */ + +/* Function declarations */ + +static bool doCommand(SmtEngine&, Command*, Options&); + +Result doSmt(SmtEngine &smt, Command *cmd, Options &options); + +template<typename T> +void sharingManager(int numThreads, + SharedChannel<T>* channelsOut[], + SharedChannel<T>* channelsIn[], + SmtEngine* smts[]); + + +/* To monitor for activity on shared channels */ +bool global_activity; +bool global_activity_true() { return global_activity; } +bool global_activity_false() { return not global_activity; } +boost::condition global_activity_cond; + +typedef expr::pickle::Pickle channelFormat; /* Remove once we are using Pickle */ + +template <typename T> +class EmptySharedChannel: public SharedChannel<T> { +public: + EmptySharedChannel(int) {} + bool push(const T&) { return true; } + T pop() { return T(); } + bool empty() { return true; } + bool full() { return false; } +}; + +class PortfolioLemmaOutputChannel : public LemmaOutputChannel { +private: + string d_tag; + SharedChannel<channelFormat>* d_sharedChannel; + expr::pickle::MapPickler d_pickler; + +public: + int cnt; + PortfolioLemmaOutputChannel(string tag, + SharedChannel<channelFormat> *c, + ExprManager* em, + VarMap& to, + VarMap& from) : + d_tag(tag), + d_sharedChannel(c), + d_pickler(em, to, from) + ,cnt(0) + {} + + void notifyNewLemma(Expr lemma) { + if(Debug.isOn("disable-lemma-sharing")) return; + const Options *options = Options::current(); + if(options->sharingFilterByLength >= 0) { // 0 would mean no-sharing effectively + if( int(lemma.getNumChildren()) > options->sharingFilterByLength) + return; + } + ++cnt; + Trace("sharing") << d_tag << ": " << lemma << std::endl; + expr::pickle::Pickle pkl; + try{ + d_pickler.toPickle(lemma, pkl); + d_sharedChannel->push(pkl); + if(Trace.isOn("showSharing") and options->thread_id == 0) { + *(Options::current()->out) << "thread #0: notifyNewLemma: " << lemma << endl; + } + }catch(expr::pickle::PicklingException& p){ + Trace("sharing::blocked") << lemma << std::endl; + } + } + +}; + +/* class PortfolioLemmaInputChannel */ +class PortfolioLemmaInputChannel : public LemmaInputChannel { +private: + string d_tag; + SharedChannel<channelFormat>* d_sharedChannel; + expr::pickle::MapPickler d_pickler; + +public: + PortfolioLemmaInputChannel(string tag, + SharedChannel<channelFormat>* c, + ExprManager* em, + VarMap& to, + VarMap& from) : + d_tag(tag), + d_sharedChannel(c), + d_pickler(em, to, from){ + } + + bool hasNewLemma(){ + Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << endl; + return !d_sharedChannel->empty(); + } + + Expr getNewLemma() { + Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << endl; + expr::pickle::Pickle pkl = d_sharedChannel->pop(); + + Expr e = d_pickler.fromPickle(pkl); + if(Trace.isOn("showSharing") and Options::current()->thread_id == 0) { + *(Options::current()->out) << "thread #0: getNewLemma: " << e << endl; + } + return e; + } + +};/* class PortfolioLemmaInputChannel */ + + + +int runCvc4(int argc, char *argv[], Options& options) { + +#ifdef CVC4_CLN_IMP + Warning() << "WARNING:" << endl + << "WARNING: This build of portfolio-CVC4 uses the CLN library" << endl + << "WARNING: which is not thread-safe! Expect crashes and" << endl + << "WARNING: incorrect answers." << endl + << "WARNING:" << endl; +#endif /* CVC4_CLN_IMP */ + + /************************************************************************** + * runCvc4 outline: + * -> Start a couple of timers + * -> Processing of options, including thread specific ones + * -> Statistics related stuff + * -> Create ExprManager, parse commands, duplicate exprMgrs using export + * -> Create smtEngines + * -> Lemma sharing init + * -> Run portfolio, exit/print stats etc. + * (This list might become outdated, a timestamp might be good: 7 Dec '11.) + **************************************************************************/ + + // Timer statistic + TimerStat s_totalTime("totalTime"); + TimerStat s_beforePortfolioTime("beforePortfolioTime"); + s_totalTime.start(); + s_beforePortfolioTime.start(); + + // For the signal handlers' benefit + pOptions = &options; + + // Initialize the signal handlers + cvc4_init(); + + progPath = argv[0]; + + + /****************************** Options Processing ************************/ + + // Parse the options + int firstArgIndex = options.parseOptions(argc, argv); + + progName = options.binary_name.c_str(); + + if( options.help ) { + printUsage(options, true); + exit(1); + } else if( options.languageHelp ) { + Options::printLanguageHelp(*options.out); + exit(1); + } else if( options.version ) { + *options.out << Configuration::about().c_str() << flush; + exit(0); + } + + int numThreads = options.threads; + + if(options.threadArgv.size() > size_t(numThreads)) { + stringstream ss; + ss << "--thread" << (options.threadArgv.size() - 1) + << " configuration string seen but this portfolio will only contain " + << numThreads << " thread(s)!"; + throw OptionException(ss.str()); + } + + segvNoSpin = options.segvNoSpin; + + // If in competition mode, set output stream option to flush immediately +#ifdef CVC4_COMPETITION_MODE + *options.out << unitbuf; +#endif + + // We only accept one input file + if(argc > firstArgIndex + 1) { + throw Exception("Too many input files specified."); + } + + // If no file supplied we will read from standard input + const bool inputFromStdin = + firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); + + // if we're reading from stdin on a TTY, default to interactive mode + if(!options.interactiveSetByUser) { + options.interactive = inputFromStdin && isatty(fileno(stdin)); + } + + // Auto-detect input language by filename extension + const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex]; + + if(options.inputLanguage == language::input::LANG_AUTO) { + if( inputFromStdin ) { + // We can't do any fancy detection on stdin + options.inputLanguage = language::input::LANG_CVC4; + } else { + unsigned len = strlen(filename); + if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { + options.inputLanguage = language::input::LANG_SMTLIB_V2; + } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { + options.inputLanguage = language::input::LANG_SMTLIB; + } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) + || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { + options.inputLanguage = language::input::LANG_CVC4; + } + } + } + + // Determine which messages to show based on smtcomp_mode and verbosity + if(Configuration::isMuzzledBuild()) { + Debug.setStream(CVC4::null_os); + Trace.setStream(CVC4::null_os); + Notice.setStream(CVC4::null_os); + Chat.setStream(CVC4::null_os); + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + } else { + if(options.verbosity < 2) { + Chat.setStream(CVC4::null_os); + } + if(options.verbosity < 1) { + Notice.setStream(CVC4::null_os); + } + if(options.verbosity < 0) { + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + } + + OutputLanguage language = language::toOutputLanguage(options.inputLanguage); + Debug.getStream() << Expr::setlanguage(language); + Trace.getStream() << Expr::setlanguage(language); + Notice.getStream() << Expr::setlanguage(language); + Chat.getStream() << Expr::setlanguage(language); + Message.getStream() << Expr::setlanguage(language); + Warning.getStream() << Expr::setlanguage(language); + } + + vector<Options> threadOptions; + for(int i = 0; i < numThreads; ++i) { + threadOptions.push_back(options); + Options& opts = threadOptions.back(); + + // Set thread identifier + opts.thread_id = i; + + // If the random-seed is negative, pick a random seed randomly + if(options.satRandomSeed < 0) + opts.satRandomSeed = (double)rand(); + + if(i < (int)options.threadArgv.size() && !options.threadArgv[i].empty()) { + // separate out the thread's individual configuration string + stringstream optidss; + optidss << "--thread" << i; + string optid = optidss.str(); + int targc = 1; + char* tbuf = strdup(options.threadArgv[i].c_str()); + char* p = tbuf; + // string length is certainly an upper bound on size needed + char** targv = new char*[options.threadArgv[i].size()]; + char** vp = targv; + *vp++ = strdup(optid.c_str()); + p = strtok(p, " "); + while(p != NULL) { + *vp++ = p; + ++targc; + p = strtok(NULL, " "); + } + *vp++ = NULL; + if(targc > 1) { // this is necessary in case you do e.g. --thread0=" " + try { + opts.parseOptions(targc, targv); + } catch(OptionException& e) { + stringstream ss; + ss << optid << ": " << e.getMessage(); + throw OptionException(ss.str()); + } + if(optind != targc) { + stringstream ss; + ss << "unused argument `" << targv[optind] + << "' in thread configuration " << optid << " !"; + throw OptionException(ss.str()); + } + if(opts.threads != numThreads || opts.threadArgv != options.threadArgv) { + stringstream ss; + ss << "not allowed to set thread options in " << optid << " !"; + throw OptionException(ss.str()); + } + } + free(targv[0]); + delete targv; + free(tbuf); + } + } + + // Some more options related stuff + + /* Use satRandomSeed for generating random numbers, in particular satRandomSeed-s */ + srand((unsigned int)(-options.satRandomSeed)); + + assert(numThreads >= 1); //do we need this? + + /* Output to string stream */ + vector<stringstream*> ss_out(numThreads); + if(options.verbosity == 0 or options.separateOutput) { + for(int i = 0;i <numThreads; ++i) { + ss_out[i] = new stringstream; + threadOptions[i].out = ss_out[i]; + } + } + + /****************************** Driver Statistics *************************/ + + // Statistics init + pStatistics = &theStatisticsRegistry; + + StatisticsRegistry driverStatisticsRegistry("driver"); + theStatisticsRegistry.registerStat_((&driverStatisticsRegistry)); + + // Timer statistic + RegisterStatistic* statTotatTime = + new RegisterStatistic(&driverStatisticsRegistry, &s_totalTime); + RegisterStatistic* statBeforePortfolioTime = + new RegisterStatistic(&driverStatisticsRegistry, &s_beforePortfolioTime); + + // Filename statistics + ReferenceStat< const char* > s_statFilename("filename", filename); + RegisterStatistic* statFilenameReg = + new RegisterStatistic(&driverStatisticsRegistry, &s_statFilename); + + + /****************** ExprManager + CommandParsing + Export *****************/ + + // Create the expression manager + ExprManager* exprMgrs[numThreads]; + exprMgrs[0] = new ExprManager(threadOptions[0]); + ExprManager* exprMgr = exprMgrs[0]; // to avoid having to change code which uses that + + // Parse commands until we are done + Command* cmd; + // bool status = true; // Doesn't seem to be use right now: commenting it out + CommandSequence* seq = new CommandSequence(); + if( options.interactive ) { + InteractiveShell shell(*exprMgr, options); + Message() << Configuration::getPackageName() + << " " << Configuration::getVersionString(); + if(Configuration::isSubversionBuild()) { + Message() << " [subversion " << Configuration::getSubversionBranchName() + << " r" << Configuration::getSubversionRevision() + << (Configuration::hasSubversionModifications() ? + " (with modifications)" : "") + << "]"; + } + Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") + << " assertions:" + << (Configuration::isAssertionBuild() ? "on" : "off") + << endl; + while((cmd = shell.readCommand())) { + seq->addCommand(cmd); + } + } else { + ParserBuilder parserBuilder = + ParserBuilder(exprMgr, filename). + withOptions(options); + + if( inputFromStdin ) { + parserBuilder.withStreamInput(cin); + } + + Parser *parser = parserBuilder.build(); + while((cmd = parser->nextCommand())) { + seq->addCommand(cmd); + // doCommand(smt, cmd, options); + // delete cmd; + } + // Remove the parser + delete parser; + } + + exprMgr = NULL; // don't want to use that variable + // after this point + + /* Duplication, Individualisation */ + ExprManagerMapCollection* vmaps[numThreads]; // vmaps[0] is generally empty + Command *seqs[numThreads]; + seqs[0] = seq; seq = NULL; + for(int i = 1; i < numThreads; ++i) { + vmaps[i] = new ExprManagerMapCollection(); + exprMgrs[i] = new ExprManager(threadOptions[i]); + seqs[i] = seqs[0]->exportTo(exprMgrs[i], *(vmaps[i]) ); + } + /** + * vmaps[i].d_from [x] = y means + * that in thread #0's expr manager id is y + * and in thread #i's expr manager id is x + * opposite for d_to + * + * d_from[x] : in a sense gives the id if converting *from* it to + * first thread + */ + + /** + * Create identity variable map for the first thread, with only + * those variables which have a corresponding variable in another + * thread. (TODO:Also assert, all threads have the same set of + * variables mapped.) + */ + if(numThreads >= 2) { + // Get keys from the first thread + //Set<uint64_t> s = vmaps[1]->d_to.keys(); + vmaps[0] = new ExprManagerMapCollection(); // identity be default? + for(typeof(vmaps[1]->d_to.begin()) i=vmaps[1]->d_to.begin(); i!=vmaps[1]->d_to.end(); ++i) { + (vmaps[0]->d_from)[i->first] = i->first; + } + vmaps[0]->d_to = vmaps[0]->d_from; + } + + // Create the SmtEngine(s) + SmtEngine *smts[numThreads]; + for(int i = 0; i < numThreads; ++i) { + smts[i] = new SmtEngine(exprMgrs[i]); + + // Register the statistics registry of the thread + string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id); + smts[i]->getStatisticsRegistry()->setName(tag); + theStatisticsRegistry.registerStat_( (Stat*)smts[i]->getStatisticsRegistry() ); + } + + /************************* Lemma sharing init ************************/ + + /* Sharing channels */ + SharedChannel<channelFormat> *channelsOut[numThreads], *channelsIn[numThreads]; + + if(numThreads == 1) { + // Disable sharing + threadOptions[0].sharingFilterByLength = 0; + } else { + // Setup sharing channels + const unsigned int sharingChannelSize = 1000000; + + for(int i = 0; i<numThreads; ++i){ + if(Debug.isOn("channel-empty")) { + channelsOut[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize); + channelsIn[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize); + continue; + } + channelsOut[i] = new SynchronizedSharedChannel<channelFormat>(sharingChannelSize); + channelsIn[i] = new SynchronizedSharedChannel<channelFormat>(sharingChannelSize); + } + + /* Lemma output channel */ + for(int i = 0; i<numThreads; ++i) { + string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id); + threadOptions[i].lemmaOutputChannel = + new PortfolioLemmaOutputChannel(tag, channelsOut[i], exprMgrs[i], + vmaps[i]->d_from, vmaps[i]->d_to); + threadOptions[i].lemmaInputChannel = + new PortfolioLemmaInputChannel(tag, channelsIn[i], exprMgrs[i], + vmaps[i]->d_from, vmaps[i]->d_to); + } + } + + /************************** End of initialization ***********************/ + + /* Portfolio */ + boost::function<Result()> fns[numThreads]; + + for(int i = 0; i < numThreads; ++i) { + fns[i] = boost::bind(doSmt, boost::ref(*smts[i]), seqs[i], boost::ref(threadOptions[i])); + } + + boost::function<void()> + smFn = boost::bind(sharingManager<channelFormat>, numThreads, channelsOut, channelsIn, smts); + + s_beforePortfolioTime.stop(); + pair<int, Result> portfolioReturn = runPortfolio(numThreads, smFn, fns, true); + int winner = portfolioReturn.first; + Result result = portfolioReturn.second; + + cout << result << endl; + + /************************* Post printing answer ***********************/ + + if(options.printWinner){ + cout << "The winner is #" << winner << endl; + } + + Result satRes = result.asSatisfiabilityResult(); + int returnValue; + if(satRes.isSat() == Result::SAT) { + returnValue = 10; + } else if(satRes.isSat() == Result::UNSAT) { + returnValue = 20; + } else { + returnValue = 0; + } + +#ifdef CVC4_COMPETITION_MODE + // exit, don't return + // (don't want destructors to run) + exit(returnValue); +#endif + + // ReferenceStat< Result > s_statSatResult("sat/unsat", result); + // RegisterStatistic statSatResultReg(*exprMgr, &s_statSatResult); + + // Stop timers, enough work done + s_totalTime.stop(); + + if(options.statistics) { + pStatistics->flushInformation(*options.err); + } + + if(options.separateOutput) { + for(int i = 0; i < numThreads; ++i) { + *options.out << "--- Output from thread #" << i << " ---" << endl; + *options.out << ss_out[i]->str(); + } + } + + /*if(options.statistics) { + double totalTime = double(s_totalTime.getData().tv_sec) + + double(s_totalTime.getData().tv_nsec)/1000000000.0; + cout.precision(6); + *options.err << "real time: " << totalTime << "s\n"; + int th0_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(options.lemmaOutputChannel)).cnt; + int th1_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(threadOptions[1].lemmaOutputChannel)).cnt; + *options.err << "lemmas shared by thread #0: " << th0_lemcnt << endl; + *options.err << "lemmas shared by thread #1: " << th1_lemcnt << endl; + *options.err << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime) + << " lem/sec" << endl; + *options.err << "winner: #" << (winner == 0 ? 0 : 1) << endl; + }*/ + + // destruction is causing segfaults, let us just exit + exit(returnValue); + + //delete vmaps; + + delete statTotatTime; + delete statBeforePortfolioTime; + delete statFilenameReg; + + // delete seq; + // delete exprMgr; + + // delete seq2; + // delete exprMgr2; + + return returnValue; +} + +/**** Code shared with driver.cpp ****/ + +namespace CVC4 { + namespace main {/* Global options variable */ + CVC4_THREADLOCAL(Options*) pOptions; + + /** Full argv[0] */ + const char *progPath; + + /** Just the basename component of argv[0] */ + const char *progName; + } +} + +void printUsage(Options& options, bool full) { + stringstream ss; + ss << "usage: " << options.binary_name << " [options] [input-file]" << endl + << endl + << "Without an input file, or with `-', CVC4 reads from standard input." << endl + << endl + << "CVC4 options:" << endl; + if(full) { + Options::printUsage( ss.str(), *options.out ); + } else { + Options::printShortUsage( ss.str(), *options.out ); + } +} + +/** Executes a command. Deletes the command after execution. */ +static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { + if( options.parseOnly ) { + return true; + } + + // assume no error + bool status = true; + + CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd); + if(seq != NULL) { + for(CommandSequence::iterator subcmd = seq->begin(); + subcmd != seq->end(); + ++subcmd) { + status = doCommand(smt, *subcmd, options) && status; + } + } else { + // by default, symmetry breaker is on only for QF_UF + if(! options.ufSymmetryBreakerSetByUser) { + SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd); + if(logic != NULL) { + options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF"); + } + } + + if(options.verbosity > 0) { + *options.out << "Invoking: " << *cmd << endl; + } + + if(options.verbosity >= 0) { + cmd->invoke(&smt, *options.out); + } else { + cmd->invoke(&smt); + } + status = status && cmd->ok(); + } + + return status; +} + +/**** End of code shared with driver.cpp ****/ + +/** Create the SMT engine and execute the commands */ +Result doSmt(SmtEngine &smt, Command *cmd, Options &options) { + + try { + // For the signal handlers' benefit + pOptions = &options; + + // Execute the commands + bool status = doCommand(smt, cmd, options); + + // if(options.statistics) { + // smt.getStatisticsRegistry()->flushInformation(*options.err); + // *options.err << "Statistics printing of my thread complete " << endl; + // } + + return status ? smt.getStatusOfLastCommand() : Result::SAT_UNKNOWN; + } catch(OptionException& e) { + *pOptions->out << "unknown" << endl; + cerr << "CVC4 Error:" << endl << e << endl; + printUsage(*pOptions); + return Result::SAT_UNKNOWN; + } catch(Exception& e) { +#ifdef CVC4_COMPETITION_MODE + *pOptions->out << "unknown" << endl; +#endif + *pOptions->err << "CVC4 Error:" << endl << e << endl; + if(pOptions->statistics) { + pStatistics->flushInformation(*pOptions->err); + } + return Result::SAT_UNKNOWN; + } catch(bad_alloc) { +#ifdef CVC4_COMPETITION_MODE + *pOptions->out << "unknown" << endl; +#endif + *pOptions->err << "CVC4 ran out of memory." << endl; + if(pOptions->statistics) { + pStatistics->flushInformation(*pOptions->err); + } + return Result::SAT_UNKNOWN; + } catch(...) { +#ifdef CVC4_COMPETITION_MODE + *pOptions->out << "unknown" << endl; +#endif + *pOptions->err << "CVC4 threw an exception of unknown type." << endl; + return Result::SAT_UNKNOWN; + } +} + +template<typename T> +void sharingManager(int numThreads, + SharedChannel<T> *channelsOut[], // out and in with respect + SharedChannel<T> *channelsIn[], + SmtEngine *smts[]) // to smt engines +{ + Trace("sharing") << "sharing: thread started " << std::endl; + vector <int> cnt(numThreads); // Debug("sharing") + + vector< queue<T> > queues; + for(int i = 0; i < numThreads; ++i){ + queues.push_back(queue<T>()); + } + + const unsigned int sharingBroadcastInterval = 1; + + boost::mutex mutex_activity; + + /* Disable interruption, so that we can check manually */ + boost::this_thread::disable_interruption di; + + while(not boost::this_thread::interruption_requested()) { + + boost::this_thread::sleep(boost::posix_time::milliseconds(sharingBroadcastInterval)); + + for(int t = 0; t < numThreads; ++t) { + + if(channelsOut[t]->empty()) continue; /* No activity on this channel */ + + /* Alert if channel full, so that we increase sharingChannelSize + or decrease sharingBroadcastInterval */ + Assert(not channelsOut[t]->full()); + + T data = channelsOut[t]->pop(); + + if(Trace.isOn("sharing")) { + ++cnt[t]; + Trace("sharing") << "sharing: Got data. Thread #" << t + << ". Chunk " << cnt[t] << std :: endl; + } + + for(int u = 0; u < numThreads; ++u) { + if(u != t){ + Trace("sharing") << "sharing: adding to queue " << u << std::endl; + queues[u].push(data); + } + }/* end of inner for: broadcast activity */ + + } /* end of outer for: look for activity */ + + for(int t = 0; t < numThreads; ++t){ + /* Alert if channel full, so that we increase sharingChannelSize + or decrease sharingBroadcastInterval */ + Assert(not channelsIn[t]->full()); + + while(!queues[t].empty() && !channelsIn[t]->full()){ + Trace("sharing") << "sharing: pushing on channel " << t << std::endl; + T data = queues[t].front(); + channelsIn[t]->push(data); + queues[t].pop(); + } + } + } /* end of infinite while */ + + Trace("interrupt") << "sharing thread interuppted, interrupting all smtEngines" << std::endl; + + for(int t = 0; t < numThreads; ++t) { + Trace("interrupt") << "Interuppting thread #" << t << std::endl; + try{ + smts[t]->interrupt(); + }catch(ModalException &e){ + // It's fine, the thread is probably not there. + Trace("interrupt") << "Could not interrupt thread #" << t << std::endl; + } + } + + Trace("sharing") << "sharing: Interuppted, exiting." << std::endl; +} diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index dca554330..a63d6c67b 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -85,7 +85,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, d_out(*options.out), d_language(options.inputLanguage), d_quit(false) { - ParserBuilder parserBuilder(&exprManager,INPUT_FILENAME,options); + ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options); /* Create parser with bogus input. */ d_parser = parserBuilder.withStringInput("").build(); diff --git a/src/main/main.cpp b/src/main/main.cpp index ecef7e79f..5d051cdad 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -20,12 +20,10 @@ #include <cstring> #include <fstream> #include <iostream> -#include <new> #include <stdio.h> #include <unistd.h> -#include "cvc4autoconfig.h" #include "main/main.h" #include "main/interactive_shell.h" #include "parser/parser.h" @@ -43,42 +41,8 @@ using namespace std; using namespace CVC4; -using namespace CVC4::parser; using namespace CVC4::main; -static int runCvc4(int argc, char* argv[]); -static bool doCommand(SmtEngine&, Command*); -static void printUsage(bool full = false); - -namespace CVC4 { - namespace main { - /** Global options variable */ - Options options; - - /** Full argv[0] */ - const char *progPath; - - /** Just the basename component of argv[0] */ - const char *progName; - - /** A pointer to the StatisticsRegistry (the signal handlers need it) */ - CVC4::StatisticsRegistry* pStatistics; - } -} - -static void printUsage(bool full) { - stringstream ss; - ss << "usage: " << options.binary_name << " [options] [input-file]" << endl - << endl - << "Without an input file, or with `-', CVC4 reads from standard input." << endl - << endl; - if(full) { - Options::printUsage( ss.str(), *options.out ); - } else { - Options::printShortUsage( ss.str(), *options.out ); - } -} - /** * CVC4's main() routine is just an exception-safe wrapper around CVC4. * Please don't construct anything here. Even if the constructor is @@ -87,14 +51,15 @@ static void printUsage(bool full) { * Put everything in runCvc4(). */ int main(int argc, char* argv[]) { + Options options; try { - return runCvc4(argc, argv); + return runCvc4(argc, argv, options); } catch(OptionException& e) { #ifdef CVC4_COMPETITION_MODE *options.out << "unknown" << endl; #endif cerr << "CVC4 Error:" << endl << e << endl; - printUsage(); + printUsage(options); exit(1); } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE @@ -102,7 +67,7 @@ int main(int argc, char* argv[]) { #endif *options.err << "CVC4 Error:" << endl << e << endl; if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(*options.err); + pStatistics->flushInformation(*options.err); } exit(1); } catch(bad_alloc&) { @@ -111,7 +76,7 @@ int main(int argc, char* argv[]) { #endif *options.err << "CVC4 ran out of memory." << endl; if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(*options.err); + pStatistics->flushInformation(*options.err); } exit(1); } catch(...) { @@ -122,276 +87,3 @@ int main(int argc, char* argv[]) { exit(1); } } - - -static int runCvc4(int argc, char* argv[]) { - - // Initialize the signal handlers - cvc4_init(); - - progPath = argv[0]; - - // Parse the options - int firstArgIndex = options.parseOptions(argc, argv); - - progName = options.binary_name.c_str(); - - if( options.help ) { - printUsage(true); - exit(1); - } else if( options.languageHelp ) { - Options::printLanguageHelp(*options.out); - exit(1); - } else if( options.version ) { - *options.out << Configuration::about().c_str() << flush; - exit(0); - } - - segvNoSpin = options.segvNoSpin; - - // If in competition mode, set output stream option to flush immediately -#ifdef CVC4_COMPETITION_MODE - *options.out << unitbuf; -#endif - - // We only accept one input file - if(argc > firstArgIndex + 1) { - throw Exception("Too many input files specified."); - } - - // If no file supplied we will read from standard input - const bool inputFromStdin = - firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); - - // if we're reading from stdin on a TTY, default to interactive mode - if(!options.interactiveSetByUser) { - options.interactive = inputFromStdin && isatty(fileno(stdin)); - } - - // Determine which messages to show based on smtcomp_mode and verbosity - if(Configuration::isMuzzledBuild()) { - Debug.setStream(CVC4::null_os); - Trace.setStream(CVC4::null_os); - Notice.setStream(CVC4::null_os); - Chat.setStream(CVC4::null_os); - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - Dump.setStream(CVC4::null_os); - } else { - if(options.verbosity < 2) { - Chat.setStream(CVC4::null_os); - } - if(options.verbosity < 1) { - Notice.setStream(CVC4::null_os); - } - if(options.verbosity < 0) { - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - } - } - - // Create the expression manager - ExprManager exprMgr(options); - - // Create the SmtEngine - SmtEngine smt(&exprMgr); - - // signal handlers need access - pStatistics = smt.getStatisticsRegistry(); - - // Auto-detect input language by filename extension - const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex]; - - ReferenceStat< const char* > s_statFilename("filename", filename); - RegisterStatistic statFilenameReg(exprMgr, &s_statFilename); - - if(options.inputLanguage == language::input::LANG_AUTO) { - if( inputFromStdin ) { - // We can't do any fancy detection on stdin - options.inputLanguage = language::input::LANG_CVC4; - } else { - unsigned len = strlen(filename); - if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - options.inputLanguage = language::input::LANG_SMTLIB_V2; - } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { - options.inputLanguage = language::input::LANG_SMTLIB; - } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) - || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - options.inputLanguage = language::input::LANG_CVC4; - } - } - } - - if(options.outputLanguage == language::output::LANG_AUTO) { - options.outputLanguage = language::toOutputLanguage(options.inputLanguage); - } - - // Determine which messages to show based on smtcomp_mode and verbosity - if(Configuration::isMuzzledBuild()) { - Debug.setStream(CVC4::null_os); - Trace.setStream(CVC4::null_os); - Notice.setStream(CVC4::null_os); - Chat.setStream(CVC4::null_os); - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - Dump.setStream(CVC4::null_os); - } else { - if(options.verbosity < 2) { - Chat.setStream(CVC4::null_os); - } - if(options.verbosity < 1) { - Notice.setStream(CVC4::null_os); - } - if(options.verbosity < 0) { - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - } - - Debug.getStream() << Expr::setlanguage(options.outputLanguage); - Trace.getStream() << Expr::setlanguage(options.outputLanguage); - Notice.getStream() << Expr::setlanguage(options.outputLanguage); - Chat.getStream() << Expr::setlanguage(options.outputLanguage); - Message.getStream() << Expr::setlanguage(options.outputLanguage); - Warning.getStream() << Expr::setlanguage(options.outputLanguage); - Dump.getStream() << Expr::setlanguage(options.outputLanguage) - << Expr::setdepth(-1) - << Expr::printtypes(false); - } - - Parser* replayParser = NULL; - if( options.replayFilename != "" ) { - ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options); - - if( options.replayFilename == "-") { - if( inputFromStdin ) { - throw OptionException("Replay file and input file can't both be stdin."); - } - replayParserBuilder.withStreamInput(cin); - } - replayParser = replayParserBuilder.build(); - options.replayStream = new Parser::ExprStream(replayParser); - } - if( options.replayLog != NULL ) { - *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1); - } - - // Parse and execute commands until we are done - Command* cmd; - bool status = true; - if( options.interactive ) { - InteractiveShell shell(exprMgr, options); - Message() << Configuration::getPackageName() - << " " << Configuration::getVersionString(); - if(Configuration::isSubversionBuild()) { - Message() << " [" << Configuration::getSubversionId() << "]"; - } - Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") - << " assertions:" - << (Configuration::isAssertionBuild() ? "on" : "off") - << endl; - if(replayParser != NULL) { - // have the replay parser use the declarations input interactively - replayParser->useDeclarationsFrom(shell.getParser()); - } - while((cmd = shell.readCommand())) { - status = doCommand(smt, cmd) && status; - delete cmd; - } - } else { - ParserBuilder parserBuilder(&exprMgr, filename, options); - - if( inputFromStdin ) { - parserBuilder.withStreamInput(cin); - } - - Parser *parser = parserBuilder.build(); - if(replayParser != NULL) { - // have the replay parser use the file's declarations - replayParser->useDeclarationsFrom(parser); - } - while((cmd = parser->nextCommand())) { - status = doCommand(smt, cmd) && status; - delete cmd; - } - // Remove the parser - delete parser; - } - - if( options.replayStream != NULL ) { - // this deletes the expression parser too - delete options.replayStream; - options.replayStream = NULL; - } - - int returnValue; - string result = "unknown"; - if(status) { - result = smt.getInfo(":status").getValue(); - - if(result == "sat") { - returnValue = 10; - } else if(result == "unsat") { - returnValue = 20; - } else { - returnValue = 0; - } - } else { - // there was some kind of error - returnValue = 1; - } - -#ifdef CVC4_COMPETITION_MODE - // exit, don't return - // (don't want destructors to run) - exit(returnValue); -#endif - - ReferenceStat< Result > s_statSatResult("sat/unsat", result); - RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult); - - if(options.statistics) { - smt.getStatisticsRegistry()->flushStatistics(*options.err); - } - - return returnValue; -} - -/** Executes a command. Deletes the command after execution. */ -static bool doCommand(SmtEngine& smt, Command* cmd) { - if( options.parseOnly ) { - return true; - } - - // assume no error - bool status = true; - - CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd); - if(seq != NULL) { - for(CommandSequence::iterator subcmd = seq->begin(); - subcmd != seq->end(); - ++subcmd) { - status = doCommand(smt, *subcmd) && status; - } - } else { - // by default, symmetry breaker is on only for QF_UF - if(! options.ufSymmetryBreakerSetByUser) { - SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd); - if(logic != NULL) { - options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF"); - } - } - - if(options.verbosity > 0) { - *options.out << "Invoking: " << *cmd << endl; - } - - if(options.verbosity >= 0) { - cmd->invoke(&smt, *options.out); - } else { - cmd->invoke(&smt); - } - status = status && cmd->ok(); - } - - return status; -} diff --git a/src/main/main.h b/src/main/main.h index 1771198f4..4df5ccc49 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -22,6 +22,7 @@ #include "util/options.h" #include "util/exception.h" #include "util/stats.h" +#include "util/tls.h" #include "cvc4autoconfig.h" #ifndef __CVC4__MAIN__MAIN_H @@ -46,8 +47,8 @@ extern CVC4::StatisticsRegistry* pStatistics; */ extern bool segvNoSpin; -/** The options currently in play */ -extern Options options; +/** A pointer to the options in play */ +extern CVC4_THREADLOCAL(Options*) pOptions; /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(Exception); @@ -55,4 +56,8 @@ void cvc4_init() throw(Exception); }/* CVC4::main namespace */ }/* CVC4 namespace */ +/** Actual Cvc4 driver functions **/ +int runCvc4(int argc, char* argv[], CVC4::Options&); +void printUsage(CVC4::Options&, bool full = false); + #endif /* __CVC4__MAIN__MAIN_H */ diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp new file mode 100644 index 000000000..fc22374cf --- /dev/null +++ b/src/main/portfolio.cpp @@ -0,0 +1,93 @@ +/********************* */ +/*! \file portfolio.cpp + ** \verbatim + ** Original author: kshitij + ** 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include <boost/function.hpp> +#include <boost/thread.hpp> +#include <boost/bind.hpp> +#include <boost/thread/condition.hpp> +#include <boost/exception_ptr.hpp> + +#include "smt/smt_engine.h" +#include "util/result.h" +#include "util/options.h" + +using namespace boost; + +namespace CVC4 { + +mutex mutex_done; +mutex mutex_main_wait; +condition condition_var_main_wait; + +bool global_flag_done = false; +int global_winner = -1; + +template<typename S> +void runThread(int thread_id, function<S()> threadFn, S& returnValue) { + returnValue = threadFn(); + + if( mutex_done.try_lock() ) { + if(global_flag_done == false) { + global_flag_done = true; + global_winner = thread_id; + } + mutex_done.unlock(); + condition_var_main_wait.notify_all(); // we want main thread to quit + } +} + +template<typename T, typename S> +std::pair<int, S> runPortfolio(int numThreads, + function<T()> driverFn, + function<S()> threadFns[], + bool optionWaitToJoin) { + thread thread_driver; + thread threads[numThreads]; + S threads_returnValue[numThreads]; + + for(int t = 0; t < numThreads; ++t) { + threads[t] = thread(bind(runThread<S>, t, threadFns[t], ref(threads_returnValue[t]) )); + } + + if(not driverFn.empty()) + thread_driver = boost::thread(driverFn); + + while(global_flag_done == false) + condition_var_main_wait.wait(mutex_main_wait); + + if(not driverFn.empty()) { + thread_driver.interrupt(); + thread_driver.join(); + } + + for(int t = 0; t < numThreads; ++t) { + if(optionWaitToJoin) { + threads[t].join(); + } + } + + return std::pair<int, S>(global_winner,threads_returnValue[global_winner]); +} + +// instantiation +template +std::pair<int, Result> +runPortfolio<void, Result>(int, boost::function<void()>, boost::function<Result()>*, bool); + +}/* CVC4 namespace */ diff --git a/src/main/portfolio.h b/src/main/portfolio.h new file mode 100644 index 000000000..9bc911be3 --- /dev/null +++ b/src/main/portfolio.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file portfolio.h + ** \verbatim + ** Original author: kshitij + ** 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#ifndef __CVC4__PORTFOLIO_H +#define __CVC4__PORTFOLIO_H + +#include <boost/function.hpp> +#include <utility> + +#include "smt/smt_engine.h" +#include "expr/command.h" +#include "util/options.h" + +namespace CVC4 { + +template<typename T, typename S> +std::pair<int, S> runPortfolio(int numThreads, + boost::function<T()> driverFn, + boost::function<S()> threadFns[], + bool optionWaitToJoin); +// as we have defined things, S=void would give compile errors +// do we want to fix this? yes, no, maybe? + +}/* CVC4 namespace */ + +#endif /* __CVC4__PORTFOLIO_H */ diff --git a/src/main/util.cpp b/src/main/util.cpp index 89aa5c6aa..35cff4abd 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -51,8 +51,8 @@ bool segvNoSpin = false; /** Handler for SIGXCPU, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by timeout.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); } @@ -60,8 +60,8 @@ void timeout_handler(int sig, siginfo_t* info, void*) { /** Handler for SIGINT, i.e., when the user hits control C. */ void sigint_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by user.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); } @@ -85,8 +85,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) { if(segvNoSpin) { fprintf(stderr, "No-spin requested, aborting...\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); } else { @@ -105,8 +105,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) { } else if(addr < 10*1024) { cerr << "Looks like a NULL pointer was dereferenced." << endl; } - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); #endif /* CVC4_DEBUG */ @@ -118,8 +118,8 @@ void ill_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n"); if(segvNoSpin) { fprintf(stderr, "No-spin requested, aborting...\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); } else { @@ -131,8 +131,8 @@ void ill_handler(int sig, siginfo_t* info, void*) { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 executed an illegal instruction.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); #endif /* CVC4_DEBUG */ @@ -155,8 +155,8 @@ void cvc4unexpected() { } if(segvNoSpin) { fprintf(stderr, "No-spin requested.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } set_terminate(default_terminator); } else { @@ -168,8 +168,8 @@ void cvc4unexpected() { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } set_terminate(default_terminator); #endif /* CVC4_DEBUG */ @@ -181,16 +181,16 @@ void cvc4terminate() { "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding. " "(Don't do that.)\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } default_terminator(); #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } default_terminator(); #endif /* CVC4_DEBUG */ diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 5c755b5f6..c17956e62 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -28,26 +28,25 @@ #include "util/options.h" namespace CVC4 { - namespace parser { -ParserBuilder::ParserBuilder(ExprManager* exprManager, - const std::string& filename) : +ParserBuilder::ParserBuilder(ExprManager* exprManager, + const std::string& filename) : d_filename(filename), d_exprManager(exprManager) { - init(exprManager,filename); + init(exprManager, filename); } -ParserBuilder::ParserBuilder(ExprManager* exprManager, - const std::string& filename, +ParserBuilder::ParserBuilder(ExprManager* exprManager, + const std::string& filename, const Options& options) : d_filename(filename), d_exprManager(exprManager) { - init(exprManager,filename); + init(exprManager, filename); withOptions(options); } -void ParserBuilder::init(ExprManager* exprManager, +void ParserBuilder::init(ExprManager* exprManager, const std::string& filename) { d_inputType = FILE_INPUT; d_lang = language::input::LANG_AUTO; @@ -60,26 +59,26 @@ void ParserBuilder::init(ExprManager* exprManager, d_parseOnly = false; } -Parser *ParserBuilder::build() - throw (InputStreamException,AssertionException) { - Input *input = NULL; +Parser* ParserBuilder::build() + throw (InputStreamException, AssertionException) { + Input* input = NULL; switch( d_inputType ) { case FILE_INPUT: - input = Input::newFileInput(d_lang,d_filename,d_mmap); + input = Input::newFileInput(d_lang, d_filename, d_mmap); break; case STREAM_INPUT: AlwaysAssert( d_streamInput != NULL, "Uninitialized stream input in ParserBuilder::build()" ); - input = Input::newStreamInput(d_lang,*d_streamInput,d_filename); + input = Input::newStreamInput(d_lang, *d_streamInput, d_filename); break; case STRING_INPUT: - input = Input::newStringInput(d_lang,d_stringInput,d_filename); + input = Input::newStringInput(d_lang, d_stringInput, d_filename); break; default: Unreachable(); } - Parser *parser = NULL; + Parser* parser = NULL; switch(d_lang) { case language::input::LANG_SMTLIB: parser = new Smt(d_exprManager, input, d_strictMode, d_parseOnly); @@ -162,6 +161,5 @@ ParserBuilder& ParserBuilder::withStringInput(const std::string& input) { return *this; } -} /* namespace parser */ - -} /* namespace CVC4 */ +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 0463a079f..ce01d3c53 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -61,7 +61,7 @@ class CVC4_PUBLIC ParserBuilder { std::string d_stringInput; /** The stream input, if any. */ - std::istream *d_streamInput; + std::istream* d_streamInput; /** The expression manager */ ExprManager* d_exprManager; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 09e072370..7f1456639 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -43,8 +43,9 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) : +CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar, bool fullLitToNodeMap) : d_satSolver(satSolver), + d_fullLitToNodeMap(fullLitToNodeMap), d_registrar(registrar) { } @@ -129,7 +130,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) { n.toString().c_str(), n.getType().toString().c_str()); - bool negated = false; + bool negated CVC4_UNUSED = false; SatLiteral lit; if(n.getKind() == kind::NOT) { @@ -178,7 +179,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { d_translationCache[node.notNode()].level = level; // If it's a theory literal, need to store it for back queries - if ( theoryLiteral || + if ( theoryLiteral || d_fullLitToNodeMap || ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) || Dump.isOn("clauses") ) { d_nodeCache[lit] = node; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 5eaeeef94..c9fd4a08b 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -69,6 +69,13 @@ protected: TranslationCache d_translationCache; NodeCache d_nodeCache; + /** + * True if the lit-to-Node map should be kept for all lits, not just + * theory lits. This is true if e.g. replay logging is on, which + * dumps the Nodes corresponding to decision literals. + */ + const bool d_fullLitToNodeMap; + /** The "registrar" for pre-registration of terms */ theory::Registrar d_registrar; @@ -179,8 +186,10 @@ public: * set of clauses and sends them to the given sat solver. * @param satSolver the sat solver to use * @param registrar the entity that takes care of preregistration of Nodes + * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, + * even for non-theory literals. */ - CnfStream(SatInputInterface* satSolver, theory::Registrar registrar); + CnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -283,7 +292,7 @@ public: private: /** - * Same as above, except that removable is rememebered. + * Same as above, except that removable is remembered. */ void convertAndAssert(TNode node, bool negated); diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 36f411df4..7df7535dd 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -22,6 +22,7 @@ #include "prop/sat.h" #include "context/context.h" #include "theory/theory_engine.h" +#include "theory/rewriter.h" #include "expr/expr_stream.h" namespace CVC4 { @@ -89,6 +90,55 @@ TNode SatSolver::getNode(SatLiteral lit) { void SatSolver::notifyRestart() { d_propEngine->checkTime(); d_theoryEngine->notifyRestart(); + + static uint32_t lemmaCount = 0; + + if(Options::current()->lemmaInputChannel != NULL) { + while(Options::current()->lemmaInputChannel->hasNewLemma()) { + Debug("shared") << "shared" << std::endl; + Expr lemma = Options::current()->lemmaInputChannel->getNewLemma(); + Node asNode = lemma.getNode(); + asNode = theory::Rewriter::rewrite(asNode); + + if(d_shared.find(asNode) == d_shared.end()) { + d_shared.insert(asNode); + if(asNode.getKind() == kind::OR) { + ++lemmaCount; + if(lemmaCount % 1 == 0) { + Debug("shared") << "=) " << asNode << std::endl; + } + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true); + } else { + Debug("shared") << "=(" << asNode << std::endl; + } + } else { + Debug("shared") <<"drop shared " << asNode << std::endl; + } + } + } +} + +void SatSolver::notifyNewLemma(SatClause& lemma) { + Assert(lemma.size() > 0); + if(Options::current()->lemmaOutputChannel != NULL) { + if(lemma.size() == 1) { + // cannot share units yet + //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); + } else { + NodeBuilder<> b(kind::OR); + for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) { + b << d_cnfStream->getNode(lemma[i]); + } + Node n = b; + + if(d_shared.find(n) == d_shared.end()) { + d_shared.insert(n); + Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr()); + } else { + Debug("shared") <<"drop new " << n << std::endl; + } + } + } } SatLiteral SatSolver::getNextReplayDecision() { diff --git a/src/prop/sat.h b/src/prop/sat.h index be3ed244b..e86443827 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -137,6 +137,12 @@ class SatSolver : public SatInputInterface { /** Context we will be using to synchronzie the sat solver */ context::Context* d_context; + /** + * Set of all lemmas that have been "shared" in the portfolio---i.e., + * all imported and exported lemmas. + */ + std::hash_set<Node, NodeHashFunction> d_shared; + /* Pointer to the concrete SAT solver. Including this via the preprocessor saves us a level of indirection vs, e.g., defining a sub-class for each solver. */ @@ -263,6 +269,8 @@ public: void notifyRestart(); + void notifyNewLemma(SatClause& lemma); + SatLiteral getNextReplayDecision(); void logDecision(SatLiteral lit); @@ -294,6 +302,12 @@ inline SatSolver::SatSolver(PropEngine* propEngine, d_minisat->random_var_freq = Options::current()->satRandomFreq; d_minisat->random_seed = Options::current()->satRandomSeed; + // Give access to all possible options in the sat solver + d_minisat->var_decay = Options::current()->satVarDecay; + d_minisat->clause_decay = Options::current()->satClauseDecay; + d_minisat->restart_first = Options::current()->satRestartFirst; + d_minisat->restart_inc = Options::current()->satRestartInc; + d_statistics.init(d_minisat); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a8f2d5700..52a98f414 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -455,6 +455,10 @@ public: */ StatisticsRegistry* getStatisticsRegistry() const; + Result getStatusOfLastCommand() const { + return d_status; + } + };/* class SmtEngine */ }/* CVC4 namespace */ diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index 3b1f5f395..e74a250a3 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -191,12 +191,15 @@ void ArithPriorityQueue::transitionToDifferenceMode() { switch(d_pivotRule){ case MINIMUM: + Debug("arith::pivotRule") << "Making the minimum heap." << endl; make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule); break; case BREAK_TIES: + Debug("arith::pivotRule") << "Making the break ties heap." << endl; make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules); break; case MAXIMUM: + Debug("arith::pivotRule") << "Making the maximum heap." << endl; make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule); break; } diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 27fb0bb02..26cdb2cdb 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -619,9 +619,9 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ if(d_queue.empty()){ return Node::null(); } - static unsigned int instance = 0; - ++instance; + static CVC4_THREADLOCAL(unsigned int) instance = 0; + ++instance; Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() " << instance << endl; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 64e713b0a..268829105 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1223,7 +1223,7 @@ void TheoryArith::presolve(){ if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } - static int callCount = 0; + static CVC4_THREADLOCAL(unsigned) callCount = 0; Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl; d_learner.clear(); diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 9c69ec684..511982d48 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -29,7 +29,7 @@ namespace arith { class ArithConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType(); return nodeManager->integerType(); } @@ -38,7 +38,7 @@ public: class ArithOperatorTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode integerType = nodeManager->integerType(); TypeNode realType = nodeManager->realType(); TNode::iterator child_it = n.begin(); @@ -65,7 +65,7 @@ public: class ArithPredicateTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TypeNode integerType = nodeManager->integerType(); TypeNode realType = nodeManager->realType(); diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index bd3c8ad67..fd9e7cb2f 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -27,7 +27,7 @@ namespace arrays { struct ArraySelectTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { Assert(n.getKind() == kind::SELECT); TypeNode arrayType = n[0].getType(check); if( check ) { @@ -45,7 +45,7 @@ struct ArraySelectTypeRule { struct ArrayStoreTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { Assert(n.getKind() == kind::STORE); TypeNode arrayType = n[0].getType(check); if( check ) { diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index e6c3e0f54..3b30b9f59 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -28,7 +28,7 @@ namespace boolean { class BooleanTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode booleanType = nodeManager->booleanType(); if( check ) { TNode::iterator child_it = n.begin(); @@ -49,7 +49,7 @@ public: class IteTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode iteType = n[1].getType(check); if( check ) { TypeNode booleanType = nodeManager->booleanType(); diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 86603f004..cd3e1437f 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -34,7 +34,7 @@ namespace builtin { class ApplyTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TNode f = n.getOperator(); TypeNode fType = f.getType(check); if( !fType.isFunction() && n.getNumChildren() > 0 ) { @@ -72,7 +72,7 @@ class ApplyTypeRule { class EqualityTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode booleanType = nodeManager->booleanType(); if( check ) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index a232ad33b..566bf3a68 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -84,7 +84,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { return RewriteResponse(REWRITE_DONE, result); } -AllRewriteRules* TheoryBVRewriter::s_allRules = NULL; +CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL; void TheoryBVRewriter::init() { s_allRules = new AllRewriteRules; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 11a55ca61..f0eb621ca 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -32,7 +32,7 @@ struct AllRewriteRules; class TheoryBVRewriter { - static AllRewriteRules* s_allRules; + static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules; public: diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 926ceb767..192295bc0 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -30,7 +30,7 @@ namespace bv { class BitVectorConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize()); } }; @@ -38,7 +38,7 @@ public: class BitVectorCompRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TypeNode lhs = n[0].getType(check); TypeNode rhs = n[1].getType(check); @@ -53,7 +53,7 @@ public: class BitVectorArithRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { unsigned maxWidth = 0; TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); @@ -72,7 +72,7 @@ public: class BitVectorFixedWidthTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TNode::iterator it = n.begin(); TypeNode t = (*it).getType(check); if( check ) { @@ -93,7 +93,7 @@ public: class BitVectorPredicateTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TypeNode lhsType = n[0].getType(check); if (!lhsType.isBitVector()) { @@ -111,7 +111,7 @@ public: class BitVectorExtractTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>(); // NOTE: We're throwing a type-checking exception here even @@ -137,7 +137,7 @@ public: class BitVectorConcatRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { unsigned size = 0; TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); @@ -158,7 +158,7 @@ public: class BitVectorRepeatTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode t = n[0].getType(check); // NOTE: We're throwing a type-checking exception here even // when check is false, bc if the argument isn't a bit-vector @@ -174,7 +174,7 @@ public: class BitVectorExtendTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode t = n[0].getType(check); // NOTE: We're throwing a type-checking exception here even // when check is false, bc if the argument isn't a bit-vector diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 147fb868e..6385d1467 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -364,6 +364,12 @@ class TheoryEngine { << std::endl << QueryCommand(node.toExpr()) << std::endl; } + + // Share with other portfolio threads + if(Options::current()->lemmaOutputChannel != NULL) { + Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr()); + } + // Remove the ITEs and assert to prop engine std::vector<Node> additionalLemmas; additionalLemmas.push_back(node); @@ -514,13 +520,13 @@ public: void staticLearning(TNode in, NodeBuilder<>& learned); /** - * Calls presolve() on all active theories and returns true + * Calls presolve() on all theories and returns true * if one of the theories discovers a conflict. */ bool presolve(); /** - * Calls postsolve() on all active theories. + * Calls postsolve() on all theories. */ void postsolve(); diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 927a31e01..9b622bc15 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -28,7 +28,7 @@ namespace uf { class UfTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TNode f = n.getOperator(); TypeNode fType = f.getType(check); if( !fType.isFunction() ) { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index c5a20cd5d..3cb6ea16f 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -50,6 +50,9 @@ libutil_la_SOURCES = \ stats.cpp \ dynamic_array.h \ language.h \ + lemma_output_channel.h \ + channel.h \ + channel.cpp \ language.cpp \ ntuple.h \ recursion_breaker.h \ diff --git a/src/util/channel.cpp b/src/util/channel.cpp new file mode 100644 index 000000000..998550f8e --- /dev/null +++ b/src/util/channel.cpp @@ -0,0 +1,2 @@ +#include "channel.h" + diff --git a/src/util/channel.h b/src/util/channel.h new file mode 100644 index 000000000..1701feba9 --- /dev/null +++ b/src/util/channel.h @@ -0,0 +1,96 @@ + +#ifndef __CVC4__CHANNEL_H +#define __CVC4__CHANNEL_H + +#include <boost/circular_buffer.hpp> +#include <boost/thread/mutex.hpp> +#include <boost/thread/condition.hpp> +#include <boost/thread/thread.hpp> +#include <boost/call_traits.hpp> +#include <boost/progress.hpp> +#include <boost/bind.hpp> + + +namespace CVC4 { + +template <typename T> +class SharedChannel { +private: + int d_maxsize; // just call it size? +public: + SharedChannel() {} + SharedChannel(int maxsize) : d_maxsize(maxsize) {} + + /* Tries to add element and returns true if successful */ + virtual bool push(const T&) = 0; + + /* Removes an element from the channel */ + virtual T pop() = 0; + + /* */ + virtual bool empty() = 0; + + /* */ + virtual bool full() = 0; +}; + +/* +This code is from + +http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.html#boundedbuffer +*/ +template <typename T> +class SynchronizedSharedChannel: public SharedChannel<T> { +public: + typedef boost::circular_buffer<T> container_type; + typedef typename container_type::size_type size_type; + typedef typename container_type::value_type value_type; + typedef typename boost::call_traits<value_type>::param_type param_type; + + explicit SynchronizedSharedChannel(size_type capacity) : m_unread(0), m_container(capacity) {} + + bool push(param_type item){ + // param_type represents the "best" way to pass a parameter of type value_type to a method + + boost::mutex::scoped_lock lock(m_mutex); + m_not_full.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_full, this)); + m_container.push_front(item); + ++m_unread; + lock.unlock(); + m_not_empty.notify_one(); + return true; + }//function definitions need to be moved to cpp + + value_type pop(){ + value_type ret; + boost::mutex::scoped_lock lock(m_mutex); + m_not_empty.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_empty, this)); + ret = m_container[--m_unread]; + lock.unlock(); + m_not_full.notify_one(); + return ret; + } + + + bool empty() { return not is_not_empty(); } + bool full() { return not is_not_full(); } + +private: + SynchronizedSharedChannel(const SynchronizedSharedChannel&); // Disabled copy constructor + SynchronizedSharedChannel& operator = (const SynchronizedSharedChannel&); // Disabled assign operator + + bool is_not_empty() const { return m_unread > 0; } + bool is_not_full() const { return m_unread < m_container.capacity(); } + + size_type m_unread; + container_type m_container; + boost::mutex m_mutex; + boost::condition m_not_empty; + boost::condition m_not_full; +}; + +} + +#endif /* __CVC4__CHANNEL_H */ + + diff --git a/src/util/hash.h b/src/util/hash.h index 6183c5208..5f0189d44 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -26,6 +26,22 @@ namespace __gnu_cxx {} #include <ext/hash_map> + +namespace __gnu_cxx { + +#if __WORDSIZE == 32 +// on 32-bit, we need a specialization of hash for 64-bit values +template <> +struct hash<uint64_t> { + size_t operator()(uint64_t v) const { + return v; + } +};/* struct hash<uint64_t> */ +#endif /* 32-bit */ + +}/* __gnu_cxx namespace */ + +// hackish: treat hash stuff as if it were in std namespace namespace std { using namespace __gnu_cxx; } namespace CVC4 { diff --git a/src/util/lemma_input_channel.h b/src/util/lemma_input_channel.h new file mode 100644 index 000000000..1627711ee --- /dev/null +++ b/src/util/lemma_input_channel.h @@ -0,0 +1,19 @@ +#include "cvc4_public.h" + +#ifndef __CVC4__LEMMA_INPUT_CHANNEL_H +#define __CVC4__LEMMA_INPUT_CHANNEL_H + +#include "expr/expr.h" + +namespace CVC4 { + +class CVC4_PUBLIC LemmaInputChannel { +public: + virtual bool hasNewLemma() = 0; + virtual Expr getNewLemma() = 0; + +};/* class LemmaOutputChannel */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_INPUT_CHANNEL_H */ diff --git a/src/util/lemma_output_channel.h b/src/util/lemma_output_channel.h new file mode 100644 index 000000000..720dd6512 --- /dev/null +++ b/src/util/lemma_output_channel.h @@ -0,0 +1,46 @@ +/********************* */ +/*! \file lemma_output_channel.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, 2010, 2011 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 Mechanism for communication about new lemmas + ** + ** This file defines an interface for use by the theory and propositional + ** engines to communicate new lemmas to the "outside world," for example + ** for lemma sharing between threads. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_H +#define __CVC4__LEMMA_OUTPUT_CHANNEL_H + +#include "expr/expr.h" + +namespace CVC4 { + +/** + * This interface describes a mechanism for the propositional and theory + * engines to communicate with the "outside world" about new lemmas being + * discovered. + */ +class CVC4_PUBLIC LemmaOutputChannel { +public: + /** + * Notifies this output channel that there's a new lemma. + * The lemma may or may not be in CNF. + */ + virtual void notifyNewLemma(Expr lemma) = 0; +};/* class LemmaOutputChannel */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_OUTPUT_CHANNEL_H */ diff --git a/src/util/options.cpp b/src/util/options.cpp index d33064c73..e33fbc263 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -64,6 +64,9 @@ Options::Options() : verbosity(0), inputLanguage(language::input::LANG_AUTO), outputLanguage(language::output::LANG_AUTO), + help(false), + version(false), + languageHelp(false), parseOnly(false), preprocessOnly(false), semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT), @@ -71,6 +74,7 @@ Options::Options() : memoryMap(false), strictParsing(false), lazyDefinitionExpansion(false), + printWinner(false), simplificationMode(SIMPLIFICATION_MODE_BATCH), doStaticLearning(true), interactive(false), @@ -93,12 +97,23 @@ Options::Options() : arithPropagation(true), satRandomFreq(0.0), satRandomSeed(91648253),// Minisat's default value + satVarDecay(0.95), + satClauseDecay(0.999), + satRestartFirst(25), + satRestartInc(3.0), pivotRule(MINIMUM), arithPivotThreshold(16), arithPropagateMaxLength(16), ufSymmetryBreaker(false), ufSymmetryBreakerSetByUser(false), - dioSolver(true) + dioSolver(true), + lemmaOutputChannel(NULL), + lemmaInputChannel(NULL), + threads(2),// default should be 1 probably, but say 2 for now + threadArgv(), + thread_id(-1), + separateOutput(false), + sharingFilterByLength(-1) { } @@ -141,6 +156,7 @@ Additional CVC4 options:\n\ --no-type-checking never type check expressions\n\ --no-checking disable ALL semantic checks, including type checks\n\ --no-theory-registration disable theory reg (not safe for some theories)\n\ + --print-winner enable printing the winning thread (pcvc4 only)\n\ --trace | -t trace something (e.g. -t pushpop), can repeat\n\ --debug | -d debug something (e.g. -d arith), can repeat\n\ --show-debug-tags show all avalable tags for debugging\n\ @@ -157,13 +173,19 @@ Additional CVC4 options:\n\ --prop-row-length=N sets the maximum row length to be used in propagation\n\ --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ + --restart-int-base=I sets the base restart interval for the sat solver (I=25 by default)\n\ + --restart-int-inc=F sets the restart interval increase factor for the sat solver (F=3.0 by default)\n\ --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --disable-arithmetic-propagation turns on arithmetic propagation\n\ --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ + --threads=N sets the number of solver threads\n\ + --threadN=string configures thread N (0..#threads-1)\n\ + --filter-lemma-length=N don't share lemmas strictly longer than N\n\ "; + #warning "Change CL options as --disable-variable-removal cannot do anything currently." static const string languageDescription = "\ @@ -322,8 +344,11 @@ enum OptionValue { REPLAY, REPLAY_LOG, PIVOT_RULE, + PRINT_WINNER, RANDOM_FREQUENCY, RANDOM_SEED, + SAT_RESTART_FIRST, + SAT_RESTART_INC, ARITHMETIC_VARIABLE_REMOVAL, ARITHMETIC_PROPAGATION, ARITHMETIC_PIVOT_THRESHOLD, @@ -331,6 +356,9 @@ enum OptionValue { ARITHMETIC_DIO_SOLVER, ENABLE_SYMMETRY_BREAKER, DISABLE_SYMMETRY_BREAKER, + PARALLEL_THREADS, + PARALLEL_SEPARATE_OUTPUT, + PORTFOLIO_FILTER_LENGTH, TIME_LIMIT, TIME_LIMIT_PER, RESOURCE_LIMIT, @@ -409,11 +437,17 @@ static struct option cmdlineOptions[] = { { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH }, { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, { "random-seed" , required_argument, NULL, RANDOM_SEED }, + { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST }, + { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC }, + { "print-winner", no_argument , NULL, PRINT_WINNER }, { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL }, { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER }, { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, + { "threads", required_argument, NULL, PARALLEL_THREADS }, + { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT }, + { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH }, { "tlimit" , required_argument, NULL, TIME_LIMIT }, { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER }, { "rlimit" , required_argument, NULL, RESOURCE_LIMIT }, @@ -428,6 +462,13 @@ throw(OptionException) { const char *progName = argv[0]; int c; + // Reset getopt(), in the case of multiple calls. + // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. + optind = 0; +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this +#endif /* HAVE_DECL_OPTRESET */ + // find the base name of the program const char *x = strrchr(progName, '/'); if(x != NULL) { @@ -595,6 +636,10 @@ throw(OptionException) { memoryMap = true; break; + case PRINT_WINNER: + printWinner = true; + break; + case STRICT_PARSING: strictParsing = true; break; @@ -807,6 +852,26 @@ throw(OptionException) { optarg + "' is not between 0.0 and 1.0."); } break; + + case SAT_RESTART_FIRST: + { + int i = atoi(optarg); + if(i < 1) { + throw OptionException("--restart-int-base requires a number bigger than 1"); + } + satRestartFirst = i; + break; + } + + case SAT_RESTART_INC: + { + int i = atoi(optarg); + if(i < 1) { + throw OptionException("--restart-int-inc requires a number bigger than 1.0"); + } + satRestartInc = i; + } + break; case PIVOT_RULE: if(!strcmp(optarg, "min")) { @@ -905,11 +970,40 @@ throw(OptionException) { printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); + case PARALLEL_THREADS: + threads = atoi(optarg); + break; + + case PARALLEL_SEPARATE_OUTPUT: + separateOutput = true; + break; + + case PORTFOLIO_FILTER_LENGTH: + sharingFilterByLength = atoi(optarg); + break; + case ':': throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); case '?': default: + if(optopt == 0 && + !strncmp(argv[optind - 1], "--thread", 8) && + strlen(argv[optind - 1]) > 8 && + isdigit(argv[optind - 1][8])) { + int tnum = atoi(argv[optind - 1] + 8); + threadArgv.resize(tnum + 1); + if(threadArgv[tnum] != "") { + threadArgv[tnum] += " "; + } + const char* p = strchr(argv[optind - 1] + 9, '='); + if(p == NULL) { // e.g., we have --thread0 "foo" + threadArgv[tnum] += argv[optind++]; + } else { // e.g., we have --thread0="foo" + threadArgv[tnum] += p + 1; + } + break; + } throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); } } diff --git a/src/util/options.h b/src/util/options.h index d04947b02..6b8054a13 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -27,8 +27,12 @@ #include "util/exception.h" #include "util/language.h" +#include "util/lemma_output_channel.h" +#include "util/lemma_input_channel.h" #include "util/tls.h" +#include <vector> + namespace CVC4 { class ExprStream; @@ -104,6 +108,9 @@ struct CVC4_PUBLIC Options { /** Should we expand function definitions lazily? */ bool lazyDefinitionExpansion; + /** Parallel Only: Whether the winner is printed at the end or not. */ + bool printWinner; + /** Enumeration of simplification modes (when to simplify). */ typedef enum { /** Simplify the assertions as they come in */ @@ -187,6 +194,18 @@ struct CVC4_PUBLIC Options { **/ double satRandomSeed; + /** Variable activity decay factor for Minisat */ + double satVarDecay; + + /** Clause activity decay factor for Minisat */ + double satClauseDecay; + + /** Base restart interval for Minisat */ + int satRestartFirst; + + /** Restart interval increase factor for Minisat */ + double satRestartInc; + /** The pivot rule for arithmetic */ typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule; ArithPivotRule pivotRule; @@ -220,6 +239,28 @@ struct CVC4_PUBLIC Options { */ bool dioSolver; + /** The output channel to receive notfication events for new lemmas */ + LemmaOutputChannel* lemmaOutputChannel; + LemmaInputChannel* lemmaInputChannel; + + /** Total number of threads */ + int threads; + + /** Thread configuration (a string to be passed to parseOptions) */ + std::vector<std::string> threadArgv; + + /** Thread ID, for internal use in case of multi-threaded run */ + int thread_id; + + /** + * In multi-threaded setting print output of each thread at the + * end of run, separated by a divider ("----"). + **/ + bool separateOutput; + + /** Filter depending on length of lemma */ + int sharingFilterByLength; + Options(); /** diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 474d8fa7a..709f80b04 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -31,6 +31,7 @@ using namespace CVC4; std::string Stat::s_delim(","); +std::string StatisticsRegistry::s_regDelim("::"); StatisticsRegistry* StatisticsRegistry::current() { return NodeManager::currentNM()->getStatisticsRegistry(); @@ -45,6 +46,14 @@ void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat() */ +void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) +{ +#ifdef CVC4_STATISTICS_ON + AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); + d_registeredStats.insert(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::registerStat_() */ + void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; @@ -54,17 +63,33 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ -void StatisticsRegistry::flushStatistics(std::ostream& out) { +void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { +#ifdef CVC4_STATISTICS_ON + AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); + d_registeredStats.erase(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::unregisterStat_() */ + +void StatisticsRegistry::flushInformation(std::ostream& out) const { #ifdef CVC4_STATISTICS_ON for(StatSet::iterator i = d_registeredStats.begin(); i != d_registeredStats.end(); ++i) { Stat* s = *i; + if(d_name != "") { + out << d_name << s_regDelim; + } s->flushStat(out); out << std::endl; } #endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::flushStatistics() */ +}/* StatisticsRegistry::flushInformation() */ + +void StatisticsRegistry::flushStat(std::ostream &out) const {; +#ifdef CVC4_STATISTICS_ON + flushInformation(out); +#endif /* CVC4_STATISTICS_ON */ +} StatisticsRegistry::const_iterator StatisticsRegistry::begin() { return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin(); @@ -93,16 +118,9 @@ void TimerStat::stop() { }/* TimerStat::stop() */ RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : - d_em(&em), d_stat(stat) { - ExprManagerScope ems(*d_em); - StatisticsRegistry::registerStat(d_stat); -}/* RegisterStatistic::RegisterStatistic(ExprManager&, Stat*) */ - -RegisterStatistic::~RegisterStatistic() { - if(d_em != NULL) { - ExprManagerScope ems(*d_em); - StatisticsRegistry::unregisterStat(d_stat); - } else { - StatisticsRegistry::unregisterStat(d_stat); - } -}/* RegisterStatistic::~RegisterStatistic() */ + d_reg(NULL), + d_stat(stat) { + ExprManagerScope ems(em); + d_reg = StatisticsRegistry::current(); + d_reg->registerStat_(d_stat); +} diff --git a/src/util/stats.h b/src/util/stats.h index 719bbaab6..63e732305 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -2,7 +2,7 @@ /*! \file stats.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters + ** Major contributors: mdeters, kshitij ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -47,84 +47,32 @@ class ExprManager; class CVC4_PUBLIC Stat; /** - * The main statistics registry. This registry maintains the list of - * currently active statistics and is able to "flush" them all. - */ -class CVC4_PUBLIC StatisticsRegistry { -private: - /** A helper class for comparing two statistics */ - struct StatCmp { - inline bool operator()(const Stat* s1, const Stat* s2) const; - };/* class StatisticsRegistry::StatCmp */ - - /** A type for a set of statistics */ - typedef std::set< Stat*, StatCmp > StatSet; - - /** The set of currently active statistics */ - StatSet d_registeredStats; - - /** Private copy constructor undefined (no copy permitted). */ - StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; - -public: - - /** Construct a statistics registry */ - StatisticsRegistry() { } - - /** An iterator type over a set of statistics */ - typedef StatSet::const_iterator const_iterator; - - /** Get a pointer to the current statistics registry */ - static StatisticsRegistry* current(); - - /** Flush all statistics to the given output stream. */ - void flushStatistics(std::ostream& out); - - /** Register a new statistic, making it active. */ - static void registerStat(Stat* s) throw(AssertionException); - - /** Unregister an active statistic, making it inactive. */ - static void unregisterStat(Stat* s) throw(AssertionException); - - /** - * Get an iterator to the beginning of the range of the set of active - * (registered) statistics. - */ - static const_iterator begin(); - - /** - * Get an iterator to the end of the range of the set of active - * (registered) statistics. - */ - static const_iterator end(); - -};/* class StatisticsRegistry */ - - -/** * The base class for all statistics. * - * This base class keeps the name of the statistic and declares two (pure) - * virtual functionss flushInformation() and getValue(). Derived classes - * must implement these functions and pass their name to the base class - * constructor. + * This base class keeps the name of the statistic and declares the (pure) + * virtual function flushInformation(). Derived classes must implement + * this function and pass their name to the base class constructor. * * This class also (statically) maintains the delimiter used to separate * the name and the value when statistics are output. */ class CVC4_PUBLIC Stat { private: - /** The name of this statistic */ - std::string d_name; - /** * The delimiter between name and value to use when outputting a * statistic. */ static std::string s_delim; +protected: + /** The name of this statistic */ + std::string d_name; + public: + /** Nullary constructor, does nothing */ + Stat() { } + /** * Construct a statistic with the given name. Debug builds of CVC4 * will throw an assertion exception if the given name contains the @@ -149,8 +97,10 @@ public: /** * Flush the name,value pair of this statistic to an output stream. * Uses the statistic delimiter string between name and value. + * + * May be redefined by a child class */ - void flushStat(std::ostream& out) const { + virtual void flushStat(std::ostream& out) const { if(__CVC4_USE_STATISTICS) { out << d_name << s_delim; flushInformation(out); @@ -163,21 +113,18 @@ public: } /** Get the value of this statistic as a string. */ - virtual std::string getValue() const = 0; + std::string getValue() const { + std::stringstream ss; + flushInformation(ss); + return ss.str(); + } };/* class Stat */ -inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, - const Stat* s2) const { - return s1->getName() < s2->getName(); -} - /** * A class to represent a "read-only" data statistic of type T. Adds to * the Stat base class the pure virtual function getData(), which returns - * type T, along with an implementation of getValue(), which converts the - * type T to a string using an existing stream insertion operator defined - * on T, and flushInformation(), which outputs the statistic value to an + * type T, and flushInformation(), which outputs the statistic value to an * output stream (using the same existing stream insertion operator). * * Template class T must have stream insertion operation defined: @@ -204,13 +151,6 @@ public: } } - /** Get the value of the statistic as a string. */ - std::string getValue() const { - std::stringstream ss; - ss << getData(); - return ss.str(); - } - };/* class ReadOnlyDataStat<T> */ @@ -480,20 +420,20 @@ private: * have seen so far. */ uint32_t d_count; + double d_sum; public: /** Construct an average statistic with the given name. */ AverageStat(const std::string& name) : - BackedStat<double>(name, 0.0), d_count(0) { + BackedStat<double>(name, 0.0), d_count(0), d_sum(0.0) { } /** Add an entry to the running-average calculation. */ void addEntry(double e) { if(__CVC4_USE_STATISTICS) { - double oldSum = d_count * getData(); ++d_count; - double newSum = oldSum + e; - setData(newSum / d_count); + d_sum += e; + setData(d_sum / d_count); } } @@ -535,13 +475,102 @@ public: return (*this); } - std::string getValue() const { - std::stringstream ss; - flushInformation(ss); - return ss.str(); +};/* class ListStat */ + +/****************************************************************************/ +/* Statistics Registry */ +/****************************************************************************/ + +/** + * The main statistics registry. This registry maintains the list of + * currently active statistics and is able to "flush" them all. + */ +class CVC4_PUBLIC StatisticsRegistry : public Stat { +private: + /** A helper class for comparing two statistics */ + struct StatCmp { + inline bool operator()(const Stat* s1, const Stat* s2) const; + };/* class StatisticsRegistry::StatCmp */ + + /** A type for a set of statistics */ + typedef std::set< Stat*, StatCmp > StatSet; + + /** The set of currently active statistics */ + StatSet d_registeredStats; + + /** Private copy constructor undefined (no copy permitted). */ + StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; + + static std::string s_regDelim; +public: + + /** Construct an nameless statistics registry */ + StatisticsRegistry() {} + + /** Construct a statistics registry */ + StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) : + Stat(name) { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(d_name.find(s_regDelim) == std::string::npos); + } } -};/* class ListStat */ + /** + * Set the name of this statistic registry, used as prefix during + * output. + * + * TODO: Get rid of this function once we have ability to set the + * name of StatisticsRegistry at creation time. + */ + void setName(const std::string& name) { + d_name = name; + } + + /** An iterator type over a set of statistics */ + typedef StatSet::const_iterator const_iterator; + + /** Get a pointer to the current statistics registry */ + static StatisticsRegistry* current(); + + /** Flush all statistics to the given output stream. */ + void flushInformation(std::ostream& out) const; + + /** Obsolete flushStatistics -- use flushInformation */ + //void flushStatistics(std::ostream& out) const; + + /** Overridden to avoid the name being printed */ + void flushStat(std::ostream &out) const; + + /** Register a new statistic, making it active. */ + static void registerStat(Stat* s) throw(AssertionException); + + /** Register a new statistic */ + void registerStat_(Stat* s) throw(AssertionException); + + /** Unregister an active statistic, making it inactive. */ + static void unregisterStat(Stat* s) throw(AssertionException); + + /** Unregister a new statistic */ + void unregisterStat_(Stat* s) throw(AssertionException); + + /** + * Get an iterator to the beginning of the range of the set of active + * (registered) statistics. + */ + static const_iterator begin(); + + /** + * Get an iterator to the end of the range of the set of active + * (registered) statistics. + */ + static const_iterator end(); + +};/* class StatisticsRegistry */ + +inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, + const Stat* s2) const { + return s1->getName() < s2->getName(); +} /****************************************************************************/ /* Some utility functions for timespec */ @@ -753,19 +782,30 @@ public: * registration and unregistration. */ class CVC4_PUBLIC RegisterStatistic { - ExprManager* d_em; + StatisticsRegistry* d_reg; Stat* d_stat; public: - RegisterStatistic(Stat* stat) : d_stat(stat) { - Assert(StatisticsRegistry::current() != NULL, - "You need to specify an expression manager " - "on which to set the statistic"); + RegisterStatistic(Stat* stat) : + d_reg(StatisticsRegistry::current()), + d_stat(stat) { + Assert(d_reg != NULL, "There is no current statistics registry!"); StatisticsRegistry::registerStat(d_stat); } + RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : + d_reg(reg), + d_stat(stat) { + Assert(d_reg != NULL, + "You need to specify a statistics registry" + "on which to set the statistic"); + d_reg->registerStat_(d_stat); + } + RegisterStatistic(ExprManager& em, Stat* stat); - ~RegisterStatistic(); + ~RegisterStatistic() { + d_reg->unregisterStat_(d_stat); + } };/* class RegisterStatistic */ |