From ff6ac38127fbb03e6c11a210b6b16d647b8785ea Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Thu, 29 Nov 2012 00:59:06 +0000 Subject: [PATCH] Fixing function models with Boolean terms. Also, LAMBDA's should not be const. --- src/smt/smt_engine.cpp | 28 +++++++-------- .../builtin/theory_builtin_type_rules.h | 2 +- src/theory/model.cpp | 36 ++++++++----------- src/theory/model.h | 8 +++-- src/theory/theory_engine.cpp | 4 +-- 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(&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 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(true); -- 2.30.2