summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp28
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h2
-rw-r--r--src/theory/model.cpp36
-rw-r--r--src/theory/model.h8
-rw-r--r--src/theory/theory_engine.cpp4
5 files changed, 38 insertions, 40 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7df98ef08..8330b2a20 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2778,21 +2778,9 @@ void SmtEngine::checkModel(bool hardFailure) {
Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl;
- // (1) check that the value is actually a value
- if(!val.isConst()) {
- Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl;
- stringstream ss;
- ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
- << "model value for " << func << endl
- << " is " << val << endl
- << "and that is not a constant (.isConst() == false)." << endl
- << "Run with `--check-models -v' for additional diagnostics.";
- InternalError(ss.str());
- }
-
- // (2) if the value is a lambda, ensure the lambda doesn't contain the
+ // (1) if the value is a lambda, ensure the lambda doesn't contain the
// function symbol (since then the definition is recursive)
- if(val.getKind() == kind::LAMBDA) {
+ if (val.getKind() == kind::LAMBDA) {
// first apply the model substitutions we have so far
Node n = substitutions.apply(val[1]);
// now check if n contains func by doing a substitution
@@ -2816,6 +2804,18 @@ void SmtEngine::checkModel(bool hardFailure) {
}
}
+ // (2) check that the value is actually a value
+ else if (!val.isConst()) {
+ Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl;
+ stringstream ss;
+ ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
+ << "model value for " << func << endl
+ << " is " << val << endl
+ << "and that is not a constant (.isConst() == false)." << endl
+ << "Run with `--check-models -v' for additional diagnostics.";
+ InternalError(ss.str());
+ }
+
// (3) checks complete, add the substitution
substitutions.addSubstitution(func, val);
}
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 4aa7c0982..40f838623 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -173,7 +173,7 @@ public:
inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
Assert(n.getKind() == kind::LAMBDA);
- return true;
+ return false;
}
};/* class LambdaTypeRule */
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index b117aa1af..826e729fc 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -26,7 +26,7 @@ using namespace CVC4::kind;
using namespace CVC4::context;
using namespace CVC4::theory;
-TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels ) :
+TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) :
d_substitutions(c), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
{
d_true = NodeManager::currentNM()->mkConst( true );
@@ -75,13 +75,19 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
}
}
-Node TheoryModel::getModelValue(TNode n) const
+Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
{
Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS);
- if(n.isConst()) {
- return n;
- }
if(n.getKind() == kind::LAMBDA) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node body = getModelValue(n[1], true);
+ // This is a bit ugly, but cache inside simplifier can change, so can't be const
+ // The ite simplifier is needed to get rid of artifacts created by Boolean terms
+ body = const_cast<ITESimplifier*>(&d_iteSimp)->simpITE(body);
+ body = Rewriter::rewrite(body);
+ return nm->mkNode(kind::LAMBDA, n[0], body);
+ }
+ if(n.isConst() || (hasBoundVars && n.getKind() == kind::BOUND_VARIABLE)) {
return n;
}
@@ -111,31 +117,19 @@ Node TheoryModel::getModelValue(TNode n) const
if (n.getNumChildren() > 0) {
std::vector<Node> children;
if (n.getKind() == APPLY_UF) {
- Node op = n.getOperator();
- if (op.getKind() == kind::LAMBDA) {
- Node rw = Rewriter::rewrite(n);
- return getModelValue(rw);
- }
- std::map< Node, Node >::const_iterator it = d_uf_models.find(op);
- if (it == d_uf_models.end()) {
- // Unknown term - return first enumerated value for this type
- TypeEnumerator te(n.getType());
- return *te;
- }else{
- // Plug in uninterpreted function model
- children.push_back(it->second);
- }
+ Node op = getModelValue(n.getOperator(), hasBoundVars);
+ children.push_back(op);
}
else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
children.push_back(n.getOperator());
}
//evaluate the children
for (unsigned i = 0; i < n.getNumChildren(); ++i) {
- Node val = getModelValue(n[i]);
+ Node val = getModelValue(n[i], hasBoundVars);
children.push_back(val);
}
Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));
- Assert(val.isConst());
+ Assert(hasBoundVars || val.isConst());
return val;
}
diff --git a/src/theory/model.h b/src/theory/model.h
index 19415ae7b..7ccbe2fc3 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -22,10 +22,13 @@
#include "theory/rep_set.h"
#include "theory/substitutions.h"
#include "theory/type_enumerator.h"
+#include "theory/ite_simplifier.h"
namespace CVC4 {
+
namespace theory {
+
/** Theory Model class
* For Model m, should call m.initialize() before using
*/
@@ -35,8 +38,9 @@ class TheoryModel : public Model
protected:
/** substitution map for this model */
SubstitutionMap d_substitutions;
+ ITESimplifier d_iteSimp;
public:
- TheoryModel( context::Context* c, std::string name, bool enableFuncModels );
+ TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
virtual ~TheoryModel(){}
/** equality engine containing all known equalities/disequalities */
eq::EqualityEngine d_equalityEngine;
@@ -55,7 +59,7 @@ protected:
/**
* Get model value function. This function is called by getValue
*/
- Node getModelValue( TNode n ) const;
+ Node getModelValue(TNode n, bool hasBoundVars = false) const;
public:
/**
* Get value function. This should be called only after a ModelBuilder has called buildModel(...)
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 42fe10cb9..1742a32a5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -106,8 +106,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
d_quantEngine = new QuantifiersEngine(context, this);
// build model information if applicable
- d_curr_model = new theory::TheoryModel( userContext, "DefaultModel", true );
- d_curr_model_builder = new theory::TheoryEngineModelBuilder( this );
+ d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);
+ d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
StatisticsRegistry::registerStat(&d_combineTheoriesTime);
d_true = NodeManager::currentNM()->mkConst<bool>(true);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback