void TheorySetsPrivate::check(Theory::Effort level) {
- CodeTimer checkCodeTimer(d_statistics.d_checkTime);
-
while(!d_external.done() && !d_conflict) {
// Get all the assertions
Assertion assertion = d_external.get();
void TheorySetsPrivate::addSharedTerm(TNode n) {
Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
+ d_termInfoManager->addTerm(n);
d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
}
void TheorySetsPrivate::dumpAssertionsHumanified() const
{
std::string tag = "sets-assertions";
+
+ if(Trace.isOn(tag)) { /* condition can't be !Trace.isOn, that's why this empty block */ }
+ else { return; }
+
context::CDList<Assertion>::const_iterator it = d_external.facts_begin(), it_end = d_external.facts_end();
std::map<TNode, std::set<TNode> > equalities;
FORIT(jt, (*kt).second.first) {
TNode x = (*jt);
if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
- Trace(tag) << x;
+ Trace(tag) << x << ", ";
} else {
- Trace(tag) << "x" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
+ Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
}
}
Trace(tag) << std::endl;
FORIT(jt, (*kt).second.second) {
TNode x = (*jt);
if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
- Trace(tag) << x;
+ Trace(tag) << x << ", ";
} else {
- Trace(tag) << "x" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
+ Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
}
}
Trace(tag) << std::endl;
dumpAssertionsHumanified();
}
+ CVC4_UNUSED unsigned edgesAddedCnt = 0;
+
unsigned i_st = 0;
if(options::setsCare1()) { i_st = d_ccg_i; }
for (unsigned i = i_st; i < d_external.d_sharedTerms.size(); ++ i) {
break;
case EQUALITY_TRUE_IN_MODEL:
d_external.addCarePair(a, b);
+ if(Trace.isOn("sharing")) {
+ ++edgesAddedCnt;
+ }
+ if(Debug.isOn("sets-care")) {
+ Debug("sets-care") << "[sets-care] Requesting split between" << a << " and "
+ << b << "." << std::endl << "[sets-care] "
+ << " Both current have value "
+ << d_external.d_valuation.getModelValue(a) << std::endl;
+ }
case EQUALITY_FALSE_IN_MODEL:
if(Trace.isOn("sets-care-performance-test")) {
// TODO: delete these lines, only for performance testing for now
}
}
}
+ Trace("sharing") << "TheorySetsPrivate::computeCareGraph(): size = " << edgesAddedCnt << std::endl;
}
EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
if( !alreadyCalculated ) {
Kind k = setterm.getKind();
- unsigned numChildren = setterm.getNumChildren();
Elements cur;
- if(numChildren == 2) {
+
+ switch(k) {
+ case kind::UNION: {
const Elements& left = getElements(setterm[0], settermElementsMap);
const Elements& right = getElements(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();
+ if(left.size() >= right.size()) {
+ cur = left; cur.insert(right.begin(), right.end());
+ } else {
+ cur = right; cur.insert(left.begin(), left.end());
}
- } else {
- Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM,
- (std::string("Expect variable or UF got ") + kindToString(k)).c_str() );
+ break;
+ }
+ case kind::INTERSECTION: {
+ const Elements& left = getElements(setterm[0], settermElementsMap);
+ const Elements& right = getElements(setterm[1], settermElementsMap);
+ std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
+ std::inserter(cur, cur.begin()) );
+ break;
+ }
+ case kind::SETMINUS: {
+ const Elements& left = getElements(setterm[0], settermElementsMap);
+ const Elements& right = getElements(setterm[1], settermElementsMap);
+ std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
+ std::inserter(cur, cur.begin()) );
+ break;
+ }
+ default:
+ Assert(theory::kindToTheoryId(k) != theory::THEORY_SETS,
+ (std::string("Kind belonging to set theory not explicitly handled: ") + kindToString(k)).c_str());
+ // Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM,
+ // (std::string("Expect variable or UF got ") + kindToString(k)).c_str() );
/* assign emptyset, which is default */
}
BOOST_FOREACH(TNode element, saved) { Debug("sets-model") << element << ", "; }
Debug("sets-model") << " }" << std::endl;
- if(S.getNumChildren() == 2) {
+ if(theory::kindToTheoryId(S.getKind()) == THEORY_SETS && S.getNumChildren() == 2) {
Elements cur;
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." );
TheorySetsPrivate::Statistics::Statistics() :
- d_checkTime("theory::sets::time")
- , d_getModelValueTime("theory::sets::getModelValueTime")
+ d_getModelValueTime("theory::sets::getModelValueTime")
+ , d_memberLemmas("theory::sets::lemmas::member", 0)
+ , d_disequalityLemmas("theory::sets::lemmas::disequality", 0)
{
- StatisticsRegistry::registerStat(&d_checkTime);
StatisticsRegistry::registerStat(&d_getModelValueTime);
+ StatisticsRegistry::registerStat(&d_memberLemmas);
+ StatisticsRegistry::registerStat(&d_disequalityLemmas);
}
TheorySetsPrivate::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_checkTime);
StatisticsRegistry::unregisterStat(&d_getModelValueTime);
+ StatisticsRegistry::unregisterStat(&d_memberLemmas);
+ StatisticsRegistry::unregisterStat(&d_disequalityLemmas);
}
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_pending.push(n);
- } else {
- Debug("sets-pending") << "[sets-pending] \u2514 added to equality queue"
- << std::endl;
- Assert(n.getKind() == kind::EQUAL);
- 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;
}
context::UserContext* u):
d_external(external),
d_notify(*this),
- d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
+ d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate", false),
+ d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)),
+ d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)),
d_conflict(c),
d_termInfoManager(NULL),
d_propagationQueue(c),
Assert(d_scrutinize != NULL);
delete d_scrutinize;
}
-}
+}/* TheorySetsPrivate::~TheorySetsPrivate() */
+
+void TheorySetsPrivate::propagate(Theory::Effort effort) {
+ if(effort != Theory::EFFORT_FULL || !options::setsPropFull()) {
+ return;
+ }
+ // build a model
+ Trace("sets-prop-full") << "[sets-prop-full] propagate(FULL_EFFORT)" << std::endl;
+ if(Trace.isOn("sets-assertions")) {
+ dumpAssertionsHumanified();
+ }
+
+ const CDNodeSet& terms = (d_termInfoManager->d_terms);
+ for(typeof(terms.key_begin()) it = terms.key_begin(); it != terms.key_end(); ++it) {
+ Node node = (*it);
+ Kind k = node.getKind();
+ if(k == kind::UNION && node[0].getKind() == kind::SINGLETON ) {
+
+ if(holds(MEMBER(node[0][0], node[1]))) {
+ Trace("sets-prop-full") << "[sets-prop-full] " << MEMBER(node[0][0], node[1])
+ << " => " << EQUAL(node[1], node) << std::endl;
+ learnLiteral(EQUAL(node[1], node), MEMBER(node[0][0], node[1]));
+ }
+
+ } else if(k == kind::UNION && node[1].getKind() == kind::SINGLETON ) {
+
+ if(holds(MEMBER(node[1][0], node[0]))) {
+ Trace("sets-prop-full") << "[sets-prop-full] " << MEMBER(node[1][0], node[0])
+ << " => " << EQUAL(node[0], node) << std::endl;
+ learnLiteral(EQUAL(node[0], node), MEMBER(node[1][0], node[0]));
+ }
+
+ }
+ }
+
+ finishPropagation();
+}
bool TheorySetsPrivate::propagate(TNode literal) {
Debug("sets-prop") << " propagate(" << literal << ")" << std::endl;
}
return ok;
-}/* TheorySetsPropagate::propagate(TNode) */
+}/* TheorySetsPrivate::propagate(TNode) */
void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
+
void TheorySetsPrivate::conflict(TNode a, TNode b)
{
if (a.getKind() == kind::CONST_BOOLEAN) {
return mkAnd(assumptions);
}
+
void TheorySetsPrivate::preRegisterTerm(TNode node)
{
Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << 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);
}
}
}
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 ) );
+ }
}
}
-
}
}
Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n)
{
+ if(d_terms.find(n) == d_terms.end()) {
+ return Node();
+ }
Assert(n.getType().isSet());
set<Node> elements, elements_const;
Node S = d_eqEngine->getRepresentative(n);
projects / cvc5.git / blobdiff