// 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);
}
} 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) &&
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();
}
}
+ 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;
+ }
+
};
}
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);
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);
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);
}
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;
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." );
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]),
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());
+
}
}
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;
}
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),
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);
}
}
}
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 ) );
+ }
}
}
-
}
}
/** 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;
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;
}
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
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: {
}//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];
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
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;
}//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]);
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;
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);
}
Node n = NormalForm::elementsToSet(std::set<TNode>(elements.begin(), elements.end()),
getType());
+ Assert(n.isConst());
Assert(n == Rewriter::rewrite(n));
return n;
#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 {
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 */
inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
Assert(n.getKind() == kind::INSERT);
- return n[0].isConst() && n[1].isConst();
+ return false;
}
};/* 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;
}
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;
}
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);
}
projects / cvc5.git / commitdiff