From d802bd27402c4e370177bc9e32f36ded4c49c860 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Mon, 10 Mar 2014 19:02:32 -0400 Subject: [PATCH] work on set model --- src/theory/sets/expr_patterns.h | 14 +- src/theory/sets/theory_sets.cpp | 4 + src/theory/sets/theory_sets.h | 4 +- src/theory/sets/theory_sets_private.cpp | 201 ++++++++++++++++++++---- src/theory/sets/theory_sets_private.h | 14 +- src/util/emptyset.h | 4 +- 6 files changed, 194 insertions(+), 47 deletions(-) diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h index 75127f5d8..bc5b6b9e0 100644 --- a/src/theory/sets/expr_patterns.h +++ b/src/theory/sets/expr_patterns.h @@ -22,6 +22,7 @@ namespace CVC4 { namespace expr { namespace pattern { +/** Boolean operators */ static Node AND(TNode a, TNode b) { return NodeManager::currentNM()->mkNode(kind::AND, a, b); } @@ -34,16 +35,21 @@ static Node OR(TNode a, TNode b, TNode c) { return NodeManager::currentNM()->mkNode(kind::OR, a, b, c); } +static Node NOT(TNode a) { + return NodeManager::currentNM()->mkNode(kind::NOT, a); +} + +/** Theory operators */ static Node MEMBER(TNode a, TNode b) { return NodeManager::currentNM()->mkNode(kind::MEMBER, a, b); } -static Node EQUAL(TNode a, TNode b) { - return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b); +static Node SET_SINGLETON(TNode a) { + return NodeManager::currentNM()->mkNode(kind::SET_SINGLETON, a); } -static Node NOT(TNode a) { - return NodeManager::currentNM()->mkNode(kind::NOT, a); +static Node EQUAL(TNode a, TNode b) { + return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b); } }/* CVC4::expr::pattern namespace */ diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 91195e67e..73176ff8b 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -38,6 +38,10 @@ void TheorySets::check(Effort e) { d_internal->check(e); } +void TheorySets::collectModelInfo(TheoryModel* m, bool fullModel) { + d_internal->collectModelInfo(m, fullModel); +} + void TheorySets::propagate(Effort e) { d_internal->propagate(e); } diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index c95229f05..8900b0e38 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -48,7 +48,7 @@ public: void check(Effort); - void propagate(Effort); + void collectModelInfo(TheoryModel*, bool fullModel); Node explain(TNode); @@ -56,6 +56,8 @@ public: void preRegisterTerm(TNode node); + void propagate(Effort); + };/* class TheorySets */ }/* CVC4::theory::sets namespace */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 940e8f2d2..bd5324d2c 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -14,12 +14,16 @@ ** Sets theory implementation. **/ +#include + +#include "theory/theory_model.h" #include "theory/sets/theory_sets.h" #include "theory/sets/theory_sets_private.h" #include "theory/sets/options.h" #include "theory/sets/expr_patterns.h" // ONLY included here +#include "util/emptyset.h" #include "util/result.h" using namespace std; @@ -70,14 +74,11 @@ void TheorySetsPrivate::check(Theory::Effort level) { finishPropagation(); Debug("sets") << "[sets] in conflict = " << d_conflict << std::endl; - - if(d_conflict && !d_equalityEngine.consistent()) return; - Assert(!d_conflict); - Assert(d_equalityEngine.consistent()); + Assert( d_conflict ^ d_equalityEngine.consistent() ); + if(d_conflict) return; } Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; - if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) { d_external.d_out->lemma(getLemma()); } @@ -356,8 +357,144 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) { Node learnt_literal = polarity ? Node(atom) : NOT(atom); d_propagationQueue.push_back( make_pair(learnt_literal, reason) ); +}/*TheorySetsPrivate::learnLiteral(...)*/ + + +/******************** Model generation ********************/ +/******************** Model generation ********************/ +/******************** Model generation ********************/ + +typedef set Elements; +typedef hash_map SettermElementsMap; + +const Elements& getElements(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 = 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(); + } + } else { + Assert(numChildren == 0); + Assert(k == kind::VARIABLE); + /* assign emptyset, which is default */ + } + + it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first; + } + return it->second; +} + +Node elementsToShape(Elements elements, + TypeNode setType) +{ + NodeManager* nm = NodeManager::currentNM(); + + if(elements.size() == 0) { + return nm->mkConst(EmptySet(nm->toType(setType))); + } else { + + Elements::iterator it = elements.begin(); + Node cur = SET_SINGLETON(*it); + while( ++it != elements.end() ) { + cur = nm->mkNode(kind::UNION, cur, SET_SINGLETON(*it)); + } + return cur; + } +} + +void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) +{ + Debug("sets-model") << "[sets-model] collectModelInfo(..., fullModel=" + << (fullModel ? "true)" : "false)") << std::endl; + + set terms; + + // Computer terms appearing assertions and shared terms + d_external.computeRelevantTerms(terms); + + // Assert equalities and disequalities to the model + m->assertEqualityEngine(&d_equalityEngine, &terms); + + // Loop over all collect set-terms for which we generate models + set settermsModEq; + SettermElementsMap settermElementsMap; + BOOST_FOREACH(TNode term, terms) { + TNode n = term.getKind() == kind::NOT ? term[0] : term; + + Debug("sets-model-details") << "[sets-model-details] > " << n << std::endl; + + if(n.getKind() == kind::EQUAL) { + // nothing to do + } else if(n.getKind() == kind::MEMBER) { + + TNode true_atom = NodeManager::currentNM()->mkConst(true); + + if(d_equalityEngine.areEqual(n, true_atom)) { + TNode x = d_equalityEngine.getRepresentative(n[0]); + TNode S = d_equalityEngine.getRepresentative(n[1]); + + settermElementsMap[S].insert(x); + } + + } else if(n.getType().isSet()) { + + n = d_equalityEngine.getRepresentative(n); + + if( !n.isConst() ) { + settermsModEq.insert(n); + } + + } + + } + + if(Debug.isOn("sets-model")) { + BOOST_FOREACH( TNode node, settermsModEq ) { + Debug("sets-model") << "[sets-model] " << node << std::endl; + } + } + + // settermElementsMap processing + BOOST_FOREACH( SettermElementsMap::value_type &it, settermElementsMap ) { + BOOST_FOREACH( TNode element, it.second /* elements */ ) { + Debug("sets-model-details") << "[sets-model-details] > " << + (it.first /* setterm */) << ": " << element << std::endl; + } + } + + // assign representatives to equivalence class + BOOST_FOREACH( TNode setterm, settermsModEq ) { + Elements elements = getElements(setterm, settermElementsMap); + Node shape = elementsToShape(elements, setterm.getType()); + m->assertEquality(shape, setterm, true); + m->assertRepresentative(shape); + } } + /********************** Helper functions ***************************/ /********************** Helper functions ***************************/ /********************** Helper functions ***************************/ @@ -551,18 +688,13 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_equalityEngine.addFunctionKind(kind::SUBSET); }/* TheorySetsPrivate::TheorySetsPrivate() */ + TheorySetsPrivate::~TheorySetsPrivate() { delete d_termInfoManager; } - -void TheorySetsPrivate::propagate(Theory::Effort e) -{ - return; -} - bool TheorySetsPrivate::propagate(TNode literal) { Debug("sets-prop") << " propagate(" << literal << ")" << std::endl; @@ -655,7 +787,8 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) { - Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality << " value = " << value << std::endl; + Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality + << " value = " << value << std::endl; if (value) { return d_theory.propagate(equality); } else { @@ -666,7 +799,8 @@ bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, boo bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) { - Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate << " value = " << value << std::endl; + Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate + << " value = " << value << std::endl; if (value) { return d_theory.propagate(predicate); } else { @@ -676,7 +810,8 @@ bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, b bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag << " t1 = " << t1 << " t2 = " << t2 << " value = " << value << std::endl; + Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag + << " t1 = " << t1 << " t2 = " << t2 << " value = " << value << std::endl; if(value) { d_theory.d_termInfoManager->mergeTerms(t1, t2); } @@ -689,25 +824,25 @@ void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t d_theory.conflict(t1, t2); } -void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t) -{ - Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl; -} - -void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2) -{ - Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; -} - -void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2) -{ - Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; -} - -void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) -{ - Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl; -} +// void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t) +// { +// Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl; +// } + +// void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2) +// { +// Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; +// } + +// void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2) +// { +// Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; +// } + +// void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) +// { +// Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl; +// } /**************************** TermInfoManager *****************************/ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index f1a8c0a46..1f43ede42 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -49,14 +49,14 @@ public: void check(Theory::Effort); - void propagate(Theory::Effort); + void collectModelInfo(TheoryModel*, bool fullModel); Node explain(TNode); - std::string identify() const { return "THEORY_SETS_PRIVATE"; } - void preRegisterTerm(TNode node); + void propagate(Theory::Effort) { /* we don't depend on this call */ } + private: TheorySets& d_external; @@ -78,10 +78,10 @@ private: bool eqNotifyTriggerPredicate(TNode predicate, bool value); bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); void eqNotifyConstantTermMerge(TNode t1, TNode t2); - void eqNotifyNewClass(TNode t); - void eqNotifyPreMerge(TNode t1, TNode t2); - void eqNotifyPostMerge(TNode t1, TNode t2); - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + void eqNotifyNewClass(TNode t) {} + void eqNotifyPreMerge(TNode t1, TNode t2) {} + void eqNotifyPostMerge(TNode t1, TNode t2) {} + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {} } d_notify; /** Equality engine */ diff --git a/src/util/emptyset.h b/src/util/emptyset.h index aae08e43b..2d307b2d4 100644 --- a/src/util/emptyset.h +++ b/src/util/emptyset.h @@ -4,8 +4,8 @@ #pragma once namespace CVC4 { - // messy; Expr needs ArrayStoreAll (because it's the payload of a - // CONSTANT-kinded expression), and ArrayStoreAll needs Expr. + // messy; Expr needs EmptySet (because it's the payload of a + // CONSTANT-kinded expression), and EmptySet needs Expr. class CVC4_PUBLIC EmptySet; }/* CVC4 namespace */ -- 2.30.2