diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 6 | ||||
-rw-r--r-- | src/expr/command.cpp | 152 | ||||
-rw-r--r-- | src/expr/command.h | 54 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 49 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 12 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 82 | ||||
-rw-r--r-- | src/expr/expr_template.h | 31 | ||||
-rwxr-xr-x | src/expr/mkexpr | 4 | ||||
-rw-r--r-- | src/expr/node.h | 10 | ||||
-rw-r--r-- | src/expr/node_builder.h | 12 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_manager.h | 112 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_value.h | 2 | ||||
-rw-r--r-- | src/expr/pickle_data.cpp | 60 | ||||
-rw-r--r-- | src/expr/pickle_data.h | 122 | ||||
-rw-r--r-- | src/expr/pickler.cpp | 477 | ||||
-rw-r--r-- | src/expr/pickler.h | 139 | ||||
-rw-r--r-- | src/expr/type.cpp | 4 | ||||
-rw-r--r-- | src/expr/type.h | 11 | ||||
-rw-r--r-- | src/expr/type_node.h | 10 | ||||
-rw-r--r-- | src/expr/variable_type_map.h | 64 |
22 files changed, 1389 insertions, 28 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 */ |