summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp8
-rw-r--r--src/theory/sets/normal_form.h60
-rw-r--r--src/theory/sets/theory_sets_private.cpp110
-rw-r--r--src/theory/sets/theory_sets_private.h4
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp155
-rw-r--r--src/theory/sets/theory_sets_type_enumerator.h1
-rw-r--r--src/theory/sets/theory_sets_type_rules.h13
-rw-r--r--src/theory/theory_engine.cpp8
8 files changed, 233 insertions, 126 deletions
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<TNode> elements, TypeNode setType)
+ template<bool ref_count>
+ static Node elementsToSet(std::set<NodeTemplate<ref_count> > 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<Node> getElementsFromNormalConstant(TNode n) {
+ Assert(n.isConst());
+ std::set<Node> 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>(EmptySet(nm->toType(setType)));
} else {
Elements::iterator it = elements.begin();
Node cur = SINGLETON(*it);
@@ -747,7 +747,7 @@ Node TheorySetsPrivate::elementsToShape(set<Node> elements, TypeNode setType) co
NodeManager* nm = NodeManager::currentNM();
if(elements.size() == 0) {
- return nm->mkConst(EmptySet(nm->toType(setType)));
+ return nm->mkConst<EmptySet>(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<Node> 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<bool>(true);
- TNode false_atom = NodeManager::currentNM()->mkConst<bool>(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<TNode> 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<bool>(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<bool>(true)),
+ d_falseNode(NodeManager::currentNM()->mkConst<bool>(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<bool>(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<bool> 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<TNode, Elements, TNodeHashFunction> 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<Node> left = NormalForm::getElementsFromNormalConstant(node[0]);
+ std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
+ std::set<Node> 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<Node> left = NormalForm::getElementsFromNormalConstant(node[0]);
+ std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
+ std::set<Node> 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<Node> left = NormalForm::getElementsFromNormalConstant(node[0]);
+ std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
+ std::set<Node> 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<TNode>(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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback