diff options
author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-06-17 15:25:58 +0200 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:39 -0400 |
commit | 0fe78eebc0c0f2d01c7aa64725bee08ba5aa2274 (patch) | |
tree | 475b094989b0828d7d82e41160a010a6134e8674 /src/smt | |
parent | 35cdae503bd88633a52333bf06fbf80cd81926e2 (diff) |
For casc : print models of functions rewritten by sort inference.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 30 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 |
2 files changed, 34 insertions, 1 deletions
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<d_modelGlobalCommands.size(); i++ ){ + Command * c = d_modelGlobalCommands[i]; + DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c); + if(dfc != NULL) { + if( dfc->getFunction()==fe ){ + dfc->setPrintInModel( p ); + } + } + } + for( unsigned i=0; i<d_modelCommands->size(); i++ ){ + Command * c = (*d_modelCommands)[i]; + DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(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 */ |