From fd29170106da3401dd183b479c84984a16ddcc41 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 23 Jan 2013 17:00:56 -0500 Subject: [PATCH] partially address bug 486: allow some model inspection of quantifiers --- src/theory/model.cpp | 111 +++++++++--------- src/theory/quantifiers/theory_quantifiers.cpp | 4 +- test/regress/regress0/Makefile.am | 3 +- test/regress/regress0/bug486.cvc | 25 ++++ 4 files changed, 87 insertions(+), 56 deletions(-) create mode 100644 test/regress/regress0/bug486.cvc diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 3880aaad9..2333a4394 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -77,66 +77,69 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const { - Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS); - 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; - } - - TypeNode t = n.getType(); - if (t.isFunction() || t.isPredicate()) { - if (d_enableFuncModels) { - std::map< Node, Node >::const_iterator it = d_uf_models.find(n); - if (it != d_uf_models.end()) { - // Existing function - return it->second; - } - // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type - vector argTypes = t.getArgTypes(); - vector args; + if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL) { + CheckArgument(d_equalityEngine.hasTerm(n), n, "Cannot get the model value for a previously-unseen quantifier: %s", n.toString().c_str()); + } else { + if(n.getKind() == kind::LAMBDA) { NodeManager* nm = NodeManager::currentNM(); - for (unsigned i = 0; i < argTypes.size(); ++i) { - args.push_back(nm->mkBoundVar(argTypes[i])); - } - Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args); - TypeEnumerator te(t.getRangeType()); - return nm->mkNode(kind::LAMBDA, boundVarList, *te); + 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); } - // TODO: if func models not enabled, throw an error? - Unreachable(); - } - - if (n.getNumChildren() > 0) { - std::vector children; - if (n.getKind() == APPLY_UF) { - Node op = getModelValue(n.getOperator(), hasBoundVars); - children.push_back(op); + if(n.isConst() || (hasBoundVars && n.getKind() == kind::BOUND_VARIABLE)) { + return n; } - else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { - children.push_back(n.getOperator()); + + TypeNode t = n.getType(); + if (t.isFunction() || t.isPredicate()) { + if (d_enableFuncModels) { + std::map< Node, Node >::const_iterator it = d_uf_models.find(n); + if (it != d_uf_models.end()) { + // Existing function + return it->second; + } + // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type + vector argTypes = t.getArgTypes(); + vector args; + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0; i < argTypes.size(); ++i) { + args.push_back(nm->mkBoundVar(argTypes[i])); + } + Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args); + TypeEnumerator te(t.getRangeType()); + return nm->mkNode(kind::LAMBDA, boundVarList, *te); + } + // TODO: if func models not enabled, throw an error? + Unreachable(); } - //evaluate the children - for (unsigned i = 0; i < n.getNumChildren(); ++i) { - Node val = getModelValue(n[i], hasBoundVars); - children.push_back(val); + + if (n.getNumChildren() > 0) { + std::vector children; + if (n.getKind() == APPLY_UF) { + 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], hasBoundVars); + children.push_back(val); + } + Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children)); + Assert(hasBoundVars || val.isConst()); + return val; } - Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children)); - Assert(hasBoundVars || val.isConst()); - return val; - } - if (!d_equalityEngine.hasTerm(n)) { - // Unknown term - return first enumerated value for this type - TypeEnumerator te(n.getType()); - return *te; + if (!d_equalityEngine.hasTerm(n)) { + // Unknown term - return first enumerated value for this type + TypeEnumerator te(n.getType()); + return *te; + } } Node val = d_equalityEngine.getRepresentative(n); Assert(d_reps.find(val) != d_reps.end()); diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index b1a7c9927..b5287fff4 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -93,7 +93,9 @@ Node TheoryQuantifiers::getValue(TNode n) { } void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){ - + for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { + m->assertPredicate(*i, true); + } } void TheoryQuantifiers::check(Effort e) { diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 3b30a8d9e..d5b35594f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -149,7 +149,8 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ simplification_bug4.smt2.expect \ - bug216.smt2.expect + bug216.smt2.expect \ + bug486.cvc if CVC4_BUILD_PROFILE_COMPETITION else diff --git a/test/regress/regress0/bug486.cvc b/test/regress/regress0/bug486.cvc new file mode 100644 index 000000000..6e8ee0018 --- /dev/null +++ b/test/regress/regress0/bug486.cvc @@ -0,0 +1,25 @@ +prin:TYPE; +form:TYPE; + +signed:(prin,form)->BOOLEAN; +says:(prin,form)->BOOLEAN; + +speaksfor:(prin,prin)->form; +signedE:BOOLEAN = FORALL(x:prin,y:form) : signed(x,y) => says(x,y); +saysE:BOOLEAN = FORALL(x,y:prin,z:form) : says(x,speaksfor(y,x)) AND says(y,z) => says(x,z); + +ASSERT(signedE); +ASSERT(saysE); + +julie:prin; +dave:prin; +alice:prin; +openfile:form; + +x2:BOOLEAN = signed(alice,openfile); +ASSERT(x2); +x3:BOOLEAN = signed(dave,speaksfor(alice,dave)); +ASSERT(x3); + +QUERY NOT says(dave,openfile); % this is invalid +QUERY says(dave,openfile); % this is valid -- 2.30.2