summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/sets/theory_sets_private.cpp115
-rw-r--r--src/theory/sets/theory_sets_private.h8
-rw-r--r--src/theory/theory_model.cpp14
-rw-r--r--test/regress/regress0/sets/Makefile.am2
-rw-r--r--test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt289
-rw-r--r--test/regress/regress0/sets/mar2014/sharing-preregister.smt212
6 files changed, 222 insertions, 18 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index b45874bf2..2675b73eb 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -89,9 +89,9 @@ void TheorySetsPrivate::check(Theory::Effort level) {
Debug("sets") << "[sets] in conflict = " << d_conflict << std::endl;
Assert( d_conflict ^ d_equalityEngine.consistent() );
if(d_conflict) return;
+ Debug("sets") << "[sets] is complete = " << isComplete() << std::endl;
}
- Debug("sets") << "[sets] is complete = " << isComplete() << std::endl;
if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
d_external.d_out->lemma(getLemma());
}
@@ -377,12 +377,11 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
/******************** Model generation ********************/
/******************** Model generation ********************/
-typedef set<TNode> Elements;
-typedef hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
-
-const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap) {
+const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
+(TNode setterm, SettermElementsMap& settermElementsMap) {
SettermElementsMap::const_iterator it = settermElementsMap.find(setterm);
- if(it == settermElementsMap.end() ) {
+ bool alreadyCalculated = (it != settermElementsMap.end());
+ if( !alreadyCalculated ) {
Kind k = setterm.getKind();
unsigned numChildren = setterm.getNumChildren();
@@ -419,15 +418,82 @@ const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMa
return it->second;
}
-Node elementsToShape(Elements elements,
- TypeNode setType)
+
+void printSet(std::ostream& out, const std::set<TNode>& elements) {
+ out << "{ ";
+ std::copy(elements.begin(),
+ elements.end(),
+ std::ostream_iterator<TNode>(out, ", ")
+ );
+ out << " }";
+}
+
+
+void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const {
+
+ Debug("sets-model") << "[sets-model] checkModel(..., " << S << "): "
+ << std::endl;
+
+ Assert(S.getType().isSet());
+
+ Elements emptySetOfElements;
+ const Elements& saved =
+ d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ?
+ emptySetOfElements :
+ settermElementsMap.find(d_equalityEngine.getRepresentative(S))->second;
+ Debug("sets-model") << "[sets-model] saved : ";
+ printSet(Debug("sets-model"), saved);
+ Debug("sets-model") << std::endl;
+
+ if(S.getNumChildren() == 2) {
+
+ Elements cur, left, right;
+ left = settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second;
+ right = settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second;
+ switch(S.getKind()) {
+ 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();
+ }
+
+ Debug("sets-model") << "[sets-model] cur : ";
+ printSet(Debug("sets-model"), cur);
+ Debug("sets-model") << std::endl;
+
+ if(saved != cur) {
+ Debug("sets-model") << "[sets-model] *** ERRROR *** cur != saved "
+ << std::endl;
+ Debug("sets-model") << "[sets-model] FYI: "
+ << " [" << S << "] = " << d_equalityEngine.getRepresentative(S) << ", "
+ << " [" << S[0] << "] = " << d_equalityEngine.getRepresentative(S[0]) << ", "
+ << " [" << S[1] << "] = " << d_equalityEngine.getRepresentative(S[1]) << "\n";
+
+ }
+ Assert( saved == cur );
+ }
+}
+
+Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) const
{
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() ) {
@@ -444,10 +510,10 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
set<Node> terms;
- // Computer terms appearing assertions and shared terms
+ // Compute terms appearing assertions and shared terms
d_external.computeRelevantTerms(terms);
- // compute for each setterm elements that it contains
+ // 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);
@@ -501,6 +567,14 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
m->assertEquality(shape, setterm, true);
m->assertRepresentative(shape);
}
+
+#ifdef CVC4_ASSERTIONS
+ BOOST_FOREACH(TNode term, terms) {
+ if( term.getType().isSet() ) {
+ checkModel(settermElementsMap, term);
+ }
+ }
+#endif
}
@@ -550,6 +624,7 @@ Node mkAnd(const std::vector<TNode>& conjunctions) {
TheorySetsPrivate::Statistics::Statistics() :
d_checkTime("theory::sets::time") {
+
StatisticsRegistry::registerStat(&d_checkTime);
}
@@ -620,20 +695,27 @@ 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_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);
}
- d_pendingEverInserted.insert(n);
}
}
bool TheorySetsPrivate::isComplete() {
- while(!d_pending.empty() && present(d_pending.front()))
+ while(!d_pending.empty() && present(d_pending.front())) {
+ Debug("sets-pending") << "[sets-pending] removing as already present: "
+ << d_pending.front() << std::endl;
d_pending.pop();
+ }
return d_pending.empty() && d_pendingDisequal.empty();
}
@@ -645,6 +727,7 @@ Node TheorySetsPrivate::getLemma() {
if(!d_pending.empty()) {
Node n = d_pending.front();
d_pending.pop();
+ d_pendingEverInserted.insert(n);
Assert(!present(n));
Assert(n.getKind() == kind::MEMBER);
@@ -653,16 +736,12 @@ Node TheorySetsPrivate::getLemma() {
} else {
Node n = d_pendingDisequal.front();
d_pendingDisequal.pop();
+ d_pendingEverInserted.insert(n);
Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType());
Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
- // d_equalityEngine.addTerm(x);
- // d_equalityEngine.addTerm(l1);
- // d_equalityEngine.addTerm(l2);
- // d_terms.insert(x);
-
lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
}
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 58000e435..daf0843e5 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -159,8 +159,16 @@ private:
void addToPending(Node n);
bool isComplete();
Node getLemma();
+
+ /** model generation and helper function */
+ typedef std::set<TNode> Elements;
+ typedef std::hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
+ const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap);
+ Node elementsToShape(Elements elements, TypeNode setType) const;
+ void checkModel(const SettermElementsMap& settermElementsMap, TNode S) const;
};/* class TheorySetsPrivate */
+
}/* CVC4::theory::sets namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 8ec25dffd..6e0a71641 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -56,14 +56,26 @@ void TheoryModel::reset(){
}
Node TheoryModel::getValue(TNode n) const {
+ Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) "
+ << std::endl;
+
//apply substitutions
Node nn = d_substitutions.apply(n);
+ Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) post-sub:"
+ << nn << std::endl;
+
//get value in model
nn = getModelValue(nn);
+ Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) getmodelvalue: "
+ << nn << std::endl;
+
if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
//normalize
nn = Rewriter::rewrite(nn);
}
+
+ Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): returning"
+ << nn << std::endl;
return nn;
}
@@ -228,6 +240,8 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){
/** add substitution */
void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
+ Debug("model-builder") << "TheoryModel::addSubstitution("<< x << ", " << t
+ << ", invalidateCache = " << invalidateCache << ")\n";
if( !d_substitutions.hasSubstitution( x ) ){
d_substitutions.addSubstitution( x, t, invalidateCache );
} else {
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index f040a6cd0..04d3433eb 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -51,6 +51,8 @@ TESTS = \
jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \
sets-sample.smt2 \
eqtest.smt2 \
+ mar2014/lemmabug-ListElts317minimized.smt2 \
+ mar2014/sharing-preregister.smt2 \
emptyset.smt2 \
error2.smt2
diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
new file mode 100644
index 000000000..a7be520e4
--- /dev/null
+++ b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
@@ -0,0 +1,89 @@
+; EXPECT: sat
+
+; Observed behavior:
+; --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143))
+; with different set of elements in the model for representative and the node
+; itself.
+;
+; Issue:
+; The trouble with data structure being mainted to ensure that things
+; for which lemmas have been generated are not generated again. This
+; data structure (d_pendingEverInserted) needs to be user context
+; dependent. The bug was in the sequence of steps from requesting that
+; a lemma be generated to when it actually was. Sequence was:
+; addToPending (and also adds to pending ever inserted) ->
+; isComplete (might remove things from pending if requirment met in other ways) ->
+; getLemma (actually generated the lemma, if requirement not already met)
+;
+; Resolution:
+; adding terms to d_pendingEverInserted was moved from addToPending()
+; to getLemma().
+
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(assert (distinct z3v58 z3v59))
+
+(declare-fun z3f60 (Int) Bool)
+(declare-fun z3v61 () Int)
+(declare-fun z3f62 (Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v67 () Int)
+(declare-fun z3f68 (Int) Int)
+(declare-fun z3f69 (Int) mySet)
+(declare-fun z3f70 (Int) mySet)
+(declare-fun z3f71 (Int) Bool)
+(declare-fun z3v90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3f92 (Int Int) Int)
+(declare-fun z3v140 () Int)
+(declare-fun z3v141 () Int)
+(declare-fun z3v142 () Int)
+(declare-fun z3v143 () Int)
+(declare-fun z3v144 () Int)
+(declare-fun z3v145 () Int)
+(declare-fun z3v147 () Int)
+(declare-fun z3v150 () Int)
+(declare-fun z3v151 () Int)
+(declare-fun z3v152 () Int)
+
+(assert (not (= (z3f69 z3v152)
+ (z3f69 z3v140))))
+
+(assert (= (z3f69 z3v151)
+ (smt_set_cup (z3f69 z3v141)
+ (z3f69 z3v140))))
+
+(assert (= (z3f69 z3v152)
+ (smt_set_cup (setenum z3v143) (z3f69 z3v151))))
+
+(assert (= (z3f70 z3v152)
+ (smt_set_cup (setenum z3v143) (z3f70 z3v151))))
+
+(assert (and
+ (= (z3f69 z3v142)
+ (smt_set_cup (setenum z3v143) (z3f69 z3v141)))
+ (= (z3f70 z3v142)
+ (smt_set_cup (setenum z3v143) (z3f70 z3v141)))
+ (= z3v142 (z3f92 z3v143 z3v141))
+ (= z3v142 z3v144)
+ (= (z3f62 z3v61) z3v61)
+ (= (z3f62 z3v63) z3v63)
+ )
+ )
+
+(check-sat)
diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
new file mode 100644
index 000000000..dc42abfa2
--- /dev/null
+++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+(set-logic QF_UFLIA_SETS)
+(set-info :status sat)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+(assert (= x (setenum a)))
+(assert (= y (setenum b)))
+(assert (not (= x y)))
+(assert (and (< 1 a) (< a 3) (< 1 b) (< b 3)))
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback