diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-17 16:32:47 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:39 -0400 |
| commit | 51dc426b0e217a4f1292be995f5473a7f2d27ad8 (patch) | |
| tree | 43e962d153ad87d9c21501413f23dfac08862af0 /src/smt | |
| parent | 5a7e8c7127ccd914633441adbc039f0c8a1fdac2 (diff) | |
Fix for new CASC features, fixes Java builds.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 11 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 2 |
2 files changed, 6 insertions, 7 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 247c367b4..28a45206f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3020,8 +3020,8 @@ void SmtEnginePrivate::processAssertions() { 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 ); + d_smt.setPrintFuncInModel( it->first.toExpr(), false ); + d_smt.setPrintFuncInModel( it->second.toExpr(), true ); } } @@ -4125,14 +4125,13 @@ void SmtEngine::setUserAttribute(const std::string& attr, Expr expr) { d_theoryEngine->setUserAttribute(attr, expr.getNode()); } -void SmtEngine::setPrintFuncInModel( Node f, bool p ) { +void SmtEngine::setPrintFuncInModel(Expr 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 ){ + if( dfc->getFunction()==f ){ dfc->setPrintInModel( p ); } } @@ -4141,7 +4140,7 @@ void SmtEngine::setPrintFuncInModel( Node f, bool p ) { Command * c = (*d_modelCommands)[i]; DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c); if(dfc != NULL) { - if( dfc->getFunction()==fe ){ + if( dfc->getFunction()==f ){ dfc->setPrintInModel( p ); } } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index c53156a3c..acf7954bc 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -656,7 +656,7 @@ public: /** * Set print function in model */ - void setPrintFuncInModel( Node f, bool p ); + void setPrintFuncInModel(Expr f, bool p); };/* class SmtEngine */ |