diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 81 |
1 files changed, 67 insertions, 14 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 08e335717..4cccb8d10 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -59,6 +59,7 @@ #include "theory/theory_traits.h" #include "theory/logic_info.h" #include "util/ite_removal.h" +#include "theory/model.h" using namespace std; using namespace CVC4; @@ -743,7 +744,8 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) } else if(key == ":produce-unsat-cores") { throw BadOptionException(); } else if(key == ":produce-models") { - throw BadOptionException(); + //throw BadOptionException(); + const_cast<Options*>( Options::s_current )->produceModels = true; } else if(key == ":produce-assignments") { throw BadOptionException(); } else { @@ -935,7 +937,7 @@ void SmtEnginePrivate::removeITEs() { for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { d_assertionsToCheck[i] = Rewriter::rewrite(d_assertionsToCheck[i]); } - + } void SmtEnginePrivate::staticLearning() { @@ -1467,7 +1469,7 @@ void SmtEnginePrivate::processAssertions() { expandDefinitions(d_assertionsToPreprocess[i], cache); } } - + // Apply the substitutions we already have, and normalize Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "applying substitutions" << endl; @@ -1766,16 +1768,15 @@ Expr SmtEngine::getValue(const Expr& e) throw ModalException(msg); } if(d_status.isNull() || - d_status.asSatisfiabilityResult() != Result::SAT || + d_status.asSatisfiabilityResult() == Result::UNSAT || d_problemExtended) { const char* msg = - "Cannot get value unless immediately preceded by SAT/INVALID response."; + "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response."; throw ModalException(msg); } - if(type.isFunction() || type.isPredicate() || - type.isKind() || type.isSortConstructor()) { + if(type.isKind() || type.isSortConstructor()) { const char* msg = - "Cannot get value of a function, predicate, or sort."; + "Cannot get value of a sort."; throw ModalException(msg); } @@ -1786,10 +1787,14 @@ Expr SmtEngine::getValue(const Expr& e) n = Rewriter::rewrite(n); Trace("smt") << "--- getting value of " << n << endl; - Node resultNode = d_theoryEngine->getValue(n); - + theory::TheoryModel* m = d_theoryEngine->getModel(); + Node resultNode; + if( m ){ + resultNode = m->getValue( n ); + } + Trace("smt") << "--- got value " << n << " = " << resultNode << endl; // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType() == n.getType()); + Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf( n.getType() )); return Expr(d_exprManager, new Node(resultNode)); } @@ -1835,11 +1840,11 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { throw ModalException(msg); } if(d_status.isNull() || - d_status.asSatisfiabilityResult() != Result::SAT || + d_status.asSatisfiabilityResult() == Result::UNSAT || d_problemExtended) { const char* msg = "Cannot get the current assignment unless immediately " - "preceded by SAT/INVALID response."; + "preceded by SAT/INVALID or UNKNOWN response."; throw ModalException(msg); } @@ -1859,7 +1864,11 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Node n = Rewriter::rewrite(*i); Trace("smt") << "--- getting value of " << n << endl; - Node resultNode = d_theoryEngine->getValue(n); + theory::TheoryModel* m = d_theoryEngine->getModel(); + Node resultNode; + if( m ){ + resultNode = m->getValue( n ); + } // type-check the result we got Assert(resultNode.isNull() || resultNode.getType() == boolType); @@ -1878,6 +1887,45 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { return SExpr(sexprs); } + +void SmtEngine::addToModelType( Type& t ){ + Trace("smt") << "SMT addToModelType(" << t << ")" << endl; + NodeManagerScope nms(d_nodeManager); + if( Options::current()->produceModels ) { + d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) ); + } +} + +void SmtEngine::addToModelFunction( Expr& e ){ + Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl; + NodeManagerScope nms(d_nodeManager); + if( Options::current()->produceModels ) { + d_theoryEngine->getModel()->addDefineFunction( e.getNode() ); + } +} + + +Model* SmtEngine::getModel() throw(ModalException, AssertionException){ + Trace("smt") << "SMT getModel()" << endl; + NodeManagerScope nms(d_nodeManager); + + if(!Options::current()->produceModels) { + const char* msg = + "Cannot get value when produce-models options is off."; + throw ModalException(msg); + } + if(d_status.isNull() || + d_status.asSatisfiabilityResult() == Result::UNSAT || + d_problemExtended) { + const char* msg = + "Cannot get the current model unless immediately " + "preceded by SAT/INVALID or UNKNOWN response."; + throw ModalException(msg); + } + + return d_theoryEngine->getModel(); +} + Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { Trace("smt") << "SMT getProof()" << endl; NodeManagerScope nms(d_nodeManager); @@ -2063,4 +2111,9 @@ StatisticsRegistry* SmtEngine::getStatisticsRegistry() const { return d_exprManager->d_nodeManager->getStatisticsRegistry(); } +void SmtEngine::printModel( std::ostream& out, Model* m ){ + NodeManagerScope nms(d_nodeManager); + m->toStream(out); +} + }/* CVC4 namespace */ |