From: Kshitij Bansal Date: Mon, 10 Nov 2014 18:11:20 +0000 (-0500) Subject: Set Constant's normal form and other short fixes X-Git-Tag: cvc5-1.0.0~6484^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=07a2c86207758b504ed744840990ff143ffc7af7;p=cvc5.git Set Constant's normal form and other short fixes Other short fixes: * use debug tag "theory::assertions::fulleffort" to dump assertions only at FULL_EFFORT * theoryof-mode fix in smt_engine.cpp * hack in TheoryModel::getModelValue [TODO: notify Clark/Andy] * Lemma generation when it rewrites to true/false fix * TermInfoManager::addTerm(..) fix * Move SUBSET rewrite to preRewrite * On preRegister, queue up propagation to be done upfront ** Hospital4 fails when all other fixes have been applied but not this one. Good to have an actual benchmark which relies on this code. * TheorySetsProperties::getCardinality(..) fix Thanks to Alvise Rabitti and Stefano Calzavara for reporting some of these; and to Morgan and Clark for help in fixing! --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a80177429..86b0faaf6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1029,7 +1029,10 @@ void SmtEngine::setDefaults() { // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { - if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV) && !d_logic.isTheoryEnabled(THEORY_STRINGS)) { + if(d_logic.isSharingEnabled() && + !d_logic.isTheoryEnabled(THEORY_BV) && + !d_logic.isTheoryEnabled(THEORY_STRINGS) && + !d_logic.isTheoryEnabled(THEORY_SETS) ) { Trace("smt") << "setting theoryof-mode to term-based" << endl; options::theoryOfMode.set(THEORY_OF_TERM_BASED); } @@ -1057,7 +1060,10 @@ void SmtEngine::setDefaults() { } else { Theory::setUninterpretedSortOwner(THEORY_UF); } + // Turn on ite simplification for QF_LIA and QF_AUFBV + // WARNING: These checks match much more than just QF_AUFBV and + // QF_LIA logics. --K [2014/10/15] if(! options::doITESimp.wasSetByUser()) { bool qf_aufbv = !d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_ARRAY) && diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index bc34ea6f1..13da6d57e 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -26,7 +26,8 @@ namespace sets { class NormalForm { public: - static Node elementsToSet(std::set elements, TypeNode setType) + template + static Node elementsToSet(std::set > elements, TypeNode setType) { NodeManager* nm = NodeManager::currentNM(); @@ -43,6 +44,63 @@ public: } } + static bool checkNormalConstant(TNode n) { + Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :" << std::endl; + if(n.getKind() == kind::EMPTYSET) { + return true; + } else if(n.getKind() == kind::SINGLETON) { + return n[0].isConst(); + } else if(n.getKind() == kind::UNION) { + + // assuming (union ... (union {SmallestNodeID} {BiggerNodeId}) ... {BiggestNodeId}) + + // store BiggestNodeId in prvs + if(n[1].getKind() != kind::SINGLETON) return false; + if( !n[1][0].isConst() ) return false; + Debug("sets-checknormal") << "[sets-checknormal] frst element = " << n[1][0] << " " << n[1][0].getId() << std::endl; + TNode prvs = n[1][0]; + n = n[0]; + + // check intermediate nodes + while(n.getKind() == kind::UNION) { + if(n[1].getKind() != kind::SINGLETON) return false; + if( !n[1].isConst() ) return false; + Debug("sets-checknormal") << "[sets-checknormal] element = " << n[1][0] << " " << n[1][0].getId() << std::endl; + if( n[1][0] >= prvs ) return false; + TNode prvs = n[1][0]; + n = n[0]; + } + + // check SmallestNodeID is smallest + if(n.getKind() != kind::SINGLETON) return false; + if( !n[0].isConst() ) return false; + Debug("sets-checknormal") << "[sets-checknormal] lst element = " << n[0] << " " << n[0].getId() << std::endl; + if( n[0] >= prvs ) return false; + + // we made it + return true; + + } else { + return false; + } + } + + static std::set getElementsFromNormalConstant(TNode n) { + Assert(n.isConst()); + std::set ret; + if(n.getKind() == kind::EMPTYSET) { + return ret; + } + while(n.getKind() == kind::UNION) { + Assert(n[1].getKind() == kind::SINGLETON); + ret.insert(ret.begin(), n[1][0]); + n = n[0]; + } + Assert(n.getKind() == kind::SINGLETON); + ret.insert(n[0]); + return ret; + } + }; } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 55bd0eefd..e229d3a6f 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -732,7 +732,7 @@ Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) con NodeManager* nm = NodeManager::currentNM(); if(elements.size() == 0) { - return nm->mkConst(EmptySet(nm->toType(setType))); + return nm->mkConst(EmptySet(nm->toType(setType))); } else { Elements::iterator it = elements.begin(); Node cur = SINGLETON(*it); @@ -747,7 +747,7 @@ Node TheorySetsPrivate::elementsToShape(set elements, TypeNode setType) co NodeManager* nm = NodeManager::currentNM(); if(elements.size() == 0) { - return nm->mkConst(EmptySet(nm->toType(setType))); + return nm->mkConst(EmptySet(nm->toType(setType))); } else { typeof(elements.begin()) it = elements.begin(); Node cur = SINGLETON(*it); @@ -765,18 +765,20 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) set terms; + if(Trace.isOn("sets-assertions")) { + dumpAssertionsHumanified(); + } + // Compute terms appearing assertions and shared terms d_external.computeRelevantTerms(terms); // Compute for each setterm elements that it contains SettermElementsMap settermElementsMap; - TNode true_atom = NodeManager::currentNM()->mkConst(true); - TNode false_atom = NodeManager::currentNM()->mkConst(false); - for(eq::EqClassIterator it_eqclasses(true_atom, &d_equalityEngine); + for(eq::EqClassIterator it_eqclasses(d_trueNode, &d_equalityEngine); ! it_eqclasses.isFinished() ; ++it_eqclasses) { TNode n = (*it_eqclasses); if(n.getKind() == kind::MEMBER) { - Assert(d_equalityEngine.areEqual(n, true_atom)); + Assert(d_equalityEngine.areEqual(n, d_trueNode)); TNode x = d_equalityEngine.getRepresentative(n[0]); TNode S = d_equalityEngine.getRepresentative(n[1]); settermElementsMap[S].insert(x); @@ -793,7 +795,7 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) } if(Debug.isOn("sets-model-details")) { - for(eq::EqClassIterator it_eqclasses(false_atom, &d_equalityEngine); + for(eq::EqClassIterator it_eqclasses(d_trueNode, &d_equalityEngine); ! it_eqclasses.isFinished() ; ++it_eqclasses) { TNode n = (*it_eqclasses); vector explanation; @@ -854,8 +856,8 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) checkPassed &= checkModel(settermElementsMap, term); } } - if(Debug.isOn("sets-checkmodel-ignore")) { - Debug("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl; + if(Trace.isOn("sets-checkmodel-ignore")) { + Trace("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl; } else { Assert( checkPassed, "THEORY_SETS check-model failed. Run with -d sets-model for details." ); @@ -937,7 +939,7 @@ bool TheorySetsPrivate::present(TNode atom) { bool TheorySetsPrivate::holds(TNode atom, bool polarity) { - Node polarity_atom = NodeManager::currentNM()->mkConst(polarity); + TNode polarity_atom = polarity ? d_trueNode : d_falseNode; Node atomModEq = NodeManager::currentNM()->mkNode (atom.getKind(), d_equalityEngine.getRepresentative(atom[0]), @@ -993,21 +995,44 @@ void TheorySetsPrivate::finishPropagation() void TheorySetsPrivate::addToPending(Node n) { Debug("sets-pending") << "[sets-pending] addToPending " << n << std::endl; - if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) { - if(n.getKind() == kind::MEMBER) { - Debug("sets-pending") << "[sets-pending] \u2514 added to member queue" - << std::endl; - ++d_statistics.d_memberLemmas; - d_pending.push(n); - } else { - Debug("sets-pending") << "[sets-pending] \u2514 added to equality queue" - << std::endl; - Assert(n.getKind() == kind::EQUAL); - ++d_statistics.d_disequalityLemmas; - d_pendingDisequal.push(n); + + if(d_pendingEverInserted.find(n) != d_pendingEverInserted.end()) { + Debug("sets-pending") << "[sets-pending] \u2514 skipping " << n + << " as lemma already generated." << std::endl; + return; + } + + if(n.getKind() == kind::MEMBER) { + + Node nRewritten = theory::Rewriter::rewrite(n); + + if(nRewritten.isConst()) { + Debug("sets-pending") << "[sets-pending] \u2514 skipping " << n + << " as we can learn one of the sides." << std::endl; + Assert(nRewritten == d_trueNode || nRewritten == d_falseNode); + + bool polarity = (nRewritten == d_trueNode); + learnLiteral(n, polarity, d_trueNode); + return; } - d_external.d_out->lemma(getLemma()); + + Debug("sets-pending") << "[sets-pending] \u2514 added to member queue" + << std::endl; + ++d_statistics.d_memberLemmas; + d_pending.push(n); + d_external.d_out->splitLemma(getLemma()); Assert(isComplete()); + + } else { + + Debug("sets-pending") << "[sets-pending] \u2514 added to equality queue" + << std::endl; + Assert(n.getKind() == kind::EQUAL); + ++d_statistics.d_disequalityLemmas; + d_pendingDisequal.push(n); + d_external.d_out->splitLemma(getLemma()); + Assert(isComplete()); + } } @@ -1042,13 +1067,15 @@ Node TheorySetsPrivate::getLemma() { d_pendingEverInserted.insert(n); Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet()); - Node x = NodeManager::currentNM()->mkSkolem("sde_", n[0].getType().getSetElementType() ); + TypeNode elementType = n[0].getType().getSetElementType(); + Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType); Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]); lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2)); } - Debug("sets-lemma") << "[sets-lemma] Generating for " << n << ", lemma: " << lemma << std::endl; + Debug("sets-lemma") << "[sets-lemma] Generating for " << n + << ", lemma: " << lemma << std::endl; return lemma; } @@ -1060,6 +1087,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_external(external), d_notify(*this), d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"), + d_trueNode(NodeManager::currentNM()->mkConst(true)), + d_falseNode(NodeManager::currentNM()->mkConst(false)), d_conflict(c), d_termInfoManager(NULL), d_propagationQueue(c), @@ -1214,12 +1243,10 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) default: d_termInfoManager->addTerm(node); d_equalityEngine.addTriggerTerm(node, THEORY_SETS); - // d_equalityEngine.addTerm(node); } + if(node.getKind() == kind::SINGLETON) { - Node true_node = NodeManager::currentNM()->mkConst(true); - learnLiteral(MEMBER(node[0], node), true, true_node); - //intentional fallthrough + learnLiteral(MEMBER(node[0], node), true, d_trueNode); } } @@ -1356,25 +1383,40 @@ const CDTNodeList* TheorySetsPrivate::TermInfoManager::getNonMembers(TNode S) { } void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) { - unsigned numChild = n.getNumChildren(); + if(d_terms.contains(n)) { + return; + } + d_terms.insert(n); - if(!d_terms.contains(n)) { - d_terms.insert(n); - d_info[n] = new TheorySetsTermInfo(d_context); + if(d_info.find(n) == d_info.end()) { + d_info.insert(make_pair(n, new TheorySetsTermInfo(d_context))); } if(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION || n.getKind() == kind::SETMINUS) { + unsigned numChild = n.getNumChildren(); + for(unsigned i = 0; i < numChild; ++i) { + Assert(d_terms.contains(n[i])); if(d_terms.contains(n[i])) { Debug("sets-parent") << "Adding " << n << " to parent list of " << n[i] << std::endl; d_info[n[i]]->parents->push_back(n); + + typeof(d_info.begin()) ita = d_info.find(d_eqEngine->getRepresentative(n[i])); + Assert(ita != d_info.end()); + CDTNodeList* l = (*ita).second->elementsNotInThisSet; + for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) { + d_theory.d_settermPropagationQueue.push_back( std::make_pair( (*it), n ) ); + } + l = (*ita).second->elementsInThisSet; + for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) { + d_theory.d_settermPropagationQueue.push_back( std::make_pair( (*it), n ) ); + } } } - } } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 643f2ab7f..ad273c546 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -100,6 +100,10 @@ private: /** Equality engine */ eq::EqualityEngine d_equalityEngine; + /** True and false constant nodes */ + Node d_trueNode; + Node d_falseNode; + context::CDO d_conflict; Node d_conflictNode; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 226eca62b..635f9856a 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -26,9 +26,6 @@ typedef std::hash_map SettermElementsMap; bool checkConstantMembership(TNode elementTerm, TNode setTerm) { - // Assume from pre-rewrite constant sets look like the following: - // (union (setenum bla) (union (setenum bla) ... (union (setenum bla) (setenum bla) ) ... )) - if(setTerm.getKind() == kind::EMPTYSET) { return false; } @@ -40,25 +37,9 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm) Assert(setTerm.getKind() == kind::UNION && setTerm[1].getKind() == kind::SINGLETON, "kind was %d, term: %s", setTerm.getKind(), setTerm.toString().c_str()); - return elementTerm == setTerm[1][0] || checkConstantMembership(elementTerm, setTerm[0]); - - // switch(setTerm.getKind()) { - // case kind::EMPTYSET: - // return false; - // case kind::SINGLETON: - // return elementTerm == setTerm[0]; - // case kind::UNION: - // return checkConstantMembership(elementTerm, setTerm[0]) || - // checkConstantMembership(elementTerm, setTerm[1]); - // case kind::INTERSECTION: - // return checkConstantMembership(elementTerm, setTerm[0]) && - // checkConstantMembership(elementTerm, setTerm[1]); - // case kind::SETMINUS: - // return checkConstantMembership(elementTerm, setTerm[0]) && - // !checkConstantMembership(elementTerm, setTerm[1]); - // default: - // Unhandled(); - // } + return + elementTerm == setTerm[1][0] || + checkConstantMembership(elementTerm, setTerm[0]); } // static @@ -66,6 +47,12 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager* nm = NodeManager::currentNM(); Kind kind = node.getKind(); + + if(node.isConst()) { + // Dare you touch the const and mangle it to something else. + return RewriteResponse(REWRITE_DONE, node); + } + switch(kind) { case kind::MEMBER: { @@ -79,6 +66,10 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { }//kind::MEMBER case kind::SUBSET: { + Assert(false, "TheorySets::postRrewrite(): Subset is handled in preRewrite."); + + // but in off-chance we do end up here, let us do our best + // rewrite (A subset-or-equal B) as (A union B = B) TNode A = node[0]; TNode B = node[1]; @@ -118,6 +109,16 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { node[1].getKind() == kind::EMPTYSET) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; return RewriteResponse(REWRITE_DONE, node[0]); + } else if(node[0].isConst() && node[1].isConst()) { + std::set left = NormalForm::getElementsFromNormalConstant(node[0]); + std::set right = NormalForm::getElementsFromNormalConstant(node[1]); + std::set newSet; + std::set_difference(left.begin(), left.end(), right.begin(), right.end(), + std::inserter(newSet, newSet.begin())); + Node newNode = NormalForm::elementsToSet(newSet, node.getType()); + Assert(newNode.isConst()); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; + return RewriteResponse(REWRITE_DONE, newNode); } break; }//kind::INTERSECION @@ -130,6 +131,16 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { return RewriteResponse(REWRITE_DONE, node[0]); } else if(node[1].getKind() == kind::EMPTYSET) { return RewriteResponse(REWRITE_DONE, node[1]); + } else if(node[0].isConst() && node[1].isConst()) { + std::set left = NormalForm::getElementsFromNormalConstant(node[0]); + std::set right = NormalForm::getElementsFromNormalConstant(node[1]); + std::set newSet; + std::set_intersection(left.begin(), left.end(), right.begin(), right.end(), + std::inserter(newSet, newSet.begin())); + Node newNode = NormalForm::elementsToSet(newSet, node.getType()); + Assert(newNode.isConst()); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; + return RewriteResponse(REWRITE_DONE, newNode); } else if (node[0] > node[1]) { Node newNode = nm->mkNode(node.getKind(), node[1], node[0]); Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; @@ -139,6 +150,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { }//kind::INTERSECION case kind::UNION: { + // NOTE: case where it is CONST is taken care of at the top if(node[0] == node[1]) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; return RewriteResponse(REWRITE_DONE, node[0]); @@ -146,6 +158,16 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { return RewriteResponse(REWRITE_DONE, node[1]); } else if(node[1].getKind() == kind::EMPTYSET) { return RewriteResponse(REWRITE_DONE, node[0]); + } else if(node[0].isConst() && node[1].isConst()) { + std::set left = NormalForm::getElementsFromNormalConstant(node[0]); + std::set right = NormalForm::getElementsFromNormalConstant(node[1]); + std::set newSet; + std::set_union(left.begin(), left.end(), right.begin(), right.end(), + std::inserter(newSet, newSet.begin())); + Node newNode = NormalForm::elementsToSet(newSet, node.getType()); + Assert(newNode.isConst()); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; + return RewriteResponse(REWRITE_DONE, newNode); } else if (node[0] > node[1]) { Node newNode = nm->mkNode(node.getKind(), node[1], node[0]); Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; @@ -162,83 +184,42 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { return RewriteResponse(REWRITE_DONE, node); } -const Elements& collectConstantElements(TNode setterm, SettermElementsMap& settermElementsMap) { - SettermElementsMap::const_iterator it = settermElementsMap.find(setterm); - if(it == settermElementsMap.end() ) { - - Kind k = setterm.getKind(); - unsigned numChildren = setterm.getNumChildren(); - Elements cur; - if(numChildren == 2) { - const Elements& left = collectConstantElements(setterm[0], settermElementsMap); - const Elements& right = collectConstantElements(setterm[1], settermElementsMap); - switch(k) { - case kind::UNION: - if(left.size() >= right.size()) { - cur = left; cur.insert(right.begin(), right.end()); - } else { - cur = right; cur.insert(left.begin(), left.end()); - } - break; - case kind::INTERSECTION: - std::set_intersection(left.begin(), left.end(), right.begin(), right.end(), - std::inserter(cur, cur.begin()) ); - break; - case kind::SETMINUS: - std::set_difference(left.begin(), left.end(), right.begin(), right.end(), - std::inserter(cur, cur.begin()) ); - break; - default: - Unhandled(); - } - } else { - switch(k) { - case kind::EMPTYSET: - /* assign emptyset, which is default */ - break; - case kind::SINGLETON: - Assert(setterm[0].isConst()); - cur.insert(TheorySetsRewriter::preRewrite(setterm[0]).node); - break; - default: - Unhandled(); - } - } - Debug("sets-rewrite-constant") << "[sets-rewrite-constant] "<< setterm << " " << setterm.getId() << std::endl; - - it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first; - } - return it->second; -} - // static RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { NodeManager* nm = NodeManager::currentNM(); - // do nothing - if(node.getKind() == kind::EQUAL && node[0] == node[1]) - return RewriteResponse(REWRITE_DONE, nm->mkConst(true)); - // Further optimization, if constants but differing ones + if(node.getKind() == kind::EQUAL) { + + if(node[0] == node[1]) { + return RewriteResponse(REWRITE_DONE, nm->mkConst(true)); + } + + }//kind::EQUAL + else if(node.getKind() == kind::INSERT) { - if(node.getKind() == kind::INSERT) { Node insertedElements = nm->mkNode(kind::SINGLETON, node[0]); size_t setNodeIndex = node.getNumChildren()-1; for(size_t i = 1; i < setNodeIndex; ++i) { - insertedElements = nm->mkNode(kind::UNION, insertedElements, nm->mkNode(kind::SINGLETON, node[i])); + insertedElements = nm->mkNode(kind::UNION, + insertedElements, + nm->mkNode(kind::SINGLETON, node[i])); } - return RewriteResponse(REWRITE_AGAIN, nm->mkNode(kind::UNION, insertedElements, node[setNodeIndex])); + return RewriteResponse(REWRITE_AGAIN, + nm->mkNode(kind::UNION, + insertedElements, + node[setNodeIndex])); + }//kind::INSERT + else if(node.getKind() == kind::SUBSET) { - if(node.getType().isSet() && node.isConst()) { - //rewrite set to normal form - SettermElementsMap setTermElementsMap; // cache - const Elements& elements = collectConstantElements(node, setTermElementsMap); - RewriteResponse response(REWRITE_DONE, NormalForm::elementsToSet(elements, node.getType())); - Debug("sets-rewrite-constant") << "[sets-rewrite-constant] Rewriting " << node << std::endl - << "[sets-rewrite-constant] to " << response.node << std::endl; - return response; - } + // rewrite (A subset-or-equal B) as (A union B = B) + return RewriteResponse(REWRITE_AGAIN, + nm->mkNode(kind::EQUAL, + nm->mkNode(kind::UNION, node[0], node[1]), + node[1]) ); + + }//kind::SUBSET return RewriteResponse(REWRITE_DONE, node); } diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 718c329fd..551c0b0ee 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -97,6 +97,7 @@ public: Node n = NormalForm::elementsToSet(std::set(elements.begin(), elements.end()), getType()); + Assert(n.isConst()); Assert(n == Rewriter::rewrite(n)); return n; diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 6754bbb9e..d0e1f18f1 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -19,6 +19,8 @@ #ifndef __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H #define __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H +#include "theory/sets/normal_form.h" + namespace CVC4 { namespace theory { namespace sets { @@ -67,7 +69,11 @@ struct SetsBinaryOperatorTypeRule { Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION || n.getKind() == kind::SETMINUS); - return n[0].isConst() && n[1].isConst(); + if(n.getKind() == kind::UNION) { + return NormalForm::checkNormalConstant(n); + } else { + return false; + } } };/* struct SetUnionTypeRule */ @@ -154,7 +160,7 @@ struct InsertTypeRule { inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { Assert(n.getKind() == kind::INSERT); - return n[0].isConst() && n[1].isConst(); + return false; } };/* struct InsertTypeRule */ @@ -162,7 +168,8 @@ struct InsertTypeRule { struct SetsProperties { inline static Cardinality computeCardinality(TypeNode type) { Assert(type.getKind() == kind::SET_TYPE); - Cardinality elementCard = type[0].getCardinality(); + Cardinality elementCard = 2; + elementCard ^= type[0].getCardinality(); return elementCard; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d83626a6b..9d91c096a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -379,6 +379,13 @@ void TheoryEngine::check(Theory::Effort effort) { printAssertions("theory::assertions"); } + if(Theory::fullEffort(effort)) { + Trace("theory::assertions::fulleffort") << endl; + if (Trace.isOn("theory::assertions::fulleffort")) { + printAssertions("theory::assertions::fulleffort"); + } + } + // Note that we've discharged all the facts d_factsAsserted = false; @@ -1194,6 +1201,7 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { } Node TheoryEngine::getModelValue(TNode var) { + if(var.isConst()) return var; // FIXME: HACK!!! Assert(d_sharedTerms.isShared(var)); return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); }