From 0fe78eebc0c0f2d01c7aa64725bee08ba5aa2274 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 17 Jun 2014 15:25:58 +0200 Subject: [PATCH] For casc : print models of functions rewritten by sort inference. --- src/expr/command.cpp | 29 +++++++++++++++++++++++++---- src/expr/command.h | 5 +++++ src/printer/smt2/smt2_printer.cpp | 9 +++++++-- src/smt/smt_engine.cpp | 30 +++++++++++++++++++++++++++++- src/smt/smt_engine.h | 5 +++++ src/util/sort_inference.cpp | 2 ++ src/util/sort_inference.h | 6 ++++-- 7 files changed, 77 insertions(+), 9 deletions(-) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 9f502c2ea..23a2b74c2 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -519,7 +519,9 @@ std::string DeclarationDefinitionCommand::getSymbol() const throw() { DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() : DeclarationDefinitionCommand(id), d_func(func), - d_type(t) { + d_type(t), + d_printInModel(true), + d_printInModelSetByUser(false){ } Expr DeclareFunctionCommand::getFunction() const throw() { @@ -530,18 +532,37 @@ Type DeclareFunctionCommand::getType() const throw() { return d_type; } +bool DeclareFunctionCommand::getPrintInModel() const throw() { + return d_printInModel; +} + +bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() { + return d_printInModelSetByUser; +} + +void DeclareFunctionCommand::setPrintInModel( bool p ) { + d_printInModel = p; + d_printInModelSetByUser = true; +} + void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), - d_type.exportTo(exprManager, variableMap)); + DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), + d_type.exportTo(exprManager, variableMap)); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; } Command* DeclareFunctionCommand::clone() const { - return new DeclareFunctionCommand(d_symbol, d_func, d_type); + DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; } std::string DeclareFunctionCommand::getCommandName() const throw() { diff --git a/src/expr/command.h b/src/expr/command.h index ed6be86de..c3d0363bb 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -351,11 +351,16 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { protected: Expr d_func; Type d_type; + bool d_printInModel; + bool d_printInModelSetByUser; public: DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw(); ~DeclareFunctionCommand() throw() {} Expr getFunction() const throw(); Type getType() const throw(); + bool getPrintInModel() const throw(); + bool getPrintInModelSetByUser() const throw(); + void setPrintInModel( bool p ); void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8e5a9dae4..95f35a5a6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -797,8 +797,13 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) } } } else if(dynamic_cast(c) != NULL) { - Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() ); - if(n.getKind() == kind::SKOLEM) { + const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c; + Node n = Node::fromExpr( dfc->getFunction() ); + if(dfc->getPrintInModelSetByUser()){ + if(!dfc->getPrintInModel()){ + return; + } + }else if(n.getKind() == kind::SKOLEM) { // don't print out internal stuff return; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ab805a6c5..247c367b4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3017,7 +3017,12 @@ void SmtEnginePrivate::processAssertions() { if( options::sortInference() ){ //sort inference technique - d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess ); + SortInference * si = d_smt.d_theoryEngine->getSortInference(); + si->simplify( d_assertionsToPreprocess ); + for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){ + d_smt.setPrintFuncInModel( it->first, false ); + d_smt.setPrintFuncInModel( it->second, true ); + } } //if( options::quantConflictFind() ){ @@ -4120,4 +4125,27 @@ void SmtEngine::setUserAttribute(const std::string& attr, Expr expr) { d_theoryEngine->setUserAttribute(attr, expr.getNode()); } +void SmtEngine::setPrintFuncInModel( Node f, bool p ) { + Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl; + Expr fe = f.toExpr(); + for( unsigned i=0; i(c); + if(dfc != NULL) { + if( dfc->getFunction()==fe ){ + dfc->setPrintInModel( p ); + } + } + } + for( unsigned i=0; isize(); i++ ){ + Command * c = (*d_modelCommands)[i]; + DeclareFunctionCommand* dfc = dynamic_cast(c); + if(dfc != NULL) { + if( dfc->getFunction()==fe ){ + dfc->setPrintInModel( p ); + } + } + } +} + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 72237ff1c..c53156a3c 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -653,6 +653,11 @@ public: */ void setUserAttribute(const std::string& attr, Expr expr); + /** + * Set print function in model + */ + void setPrintFuncInModel( Node f, bool p ); + };/* class SmtEngine */ }/* CVC4 namespace */ diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index b38ed7d63..90382c365 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -580,6 +580,8 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ ss << "io_" << op; TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType ); d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" ); + Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl; + d_model_replace_f[op] = d_symbol_map[op]; }else{ d_symbol_map[op] = op; } diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h index cd80f57d8..4cf2ab732 100644 --- a/src/util/sort_inference.h +++ b/src/util/sort_inference.h @@ -26,7 +26,7 @@ namespace CVC4 { -class SortInference{ +class SortInference { private: //all subsorts std::vector< int > d_sub_sorts; @@ -69,7 +69,6 @@ private: void printSort( const char* c, int t ); //process int process( Node n, std::map< Node, Node >& var_bound ); - //for monotonicity inference private: void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ); @@ -107,6 +106,9 @@ public: bool isWellSorted( Node n ); //get constraints for being well-typed according to computed sub-types void getSortConstraints( Node n, SortInference::UnionFind& uf ); +public: + //list of all functions and the uninterpreted symbols they were replaced with + std::map< Node, Node > d_model_replace_f; }; } -- 2.30.2