summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine.cpp81
-rw-r--r--src/smt/smt_engine.h25
2 files changed, 92 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 */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index ae9caf0eb..aef98d75b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -29,6 +29,7 @@
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "util/proof.h"
+#include "util/model.h"
#include "smt/bad_option_exception.h"
#include "smt/modal_exception.h"
#include "smt/no_such_function_exception.h"
@@ -386,6 +387,25 @@ public:
SExpr getAssignment() throw(ModalException, AssertionException);
/**
+ * Add to Model Type. This is used for recording which types should be reported
+ * during a get-model call.
+ */
+ void addToModelType( Type& t );
+
+ /**
+ * Add to Model Function. This is used for recording which functions should be reported
+ * during a get-model call.
+ */
+ void addToModelFunction( Expr& e );
+
+ /**
+ * Get the model (only if immediately preceded by a SAT
+ * or INVALID query). Only permitted if CVC4 was built with model
+ * support and produce-models is on.
+ */
+ Model* getModel() throw(ModalException, AssertionException);
+
+ /**
* Get the last proof (only if immediately preceded by an UNSAT
* or VALID query). Only permitted if CVC4 was built with proof
* support and produce-proofs is on.
@@ -520,6 +540,11 @@ public:
return d_status;
}
+ /**
+ * print model function (need this?)
+ */
+ void printModel( std::ostream& out, Model* m );
+
};/* class SmtEngine */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback