diff options
27 files changed, 746 insertions, 245 deletions
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index af4752d13..eb5c8a6f8 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -149,6 +149,9 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { if(isPredicateSubtype()) { return getSubtypeParentType().isSubtypeOf(t); } + if(isSet() && t.isSet()) { + return getSetElementType().isSubtypeOf(t.getSetElementType()); + } return false; } @@ -336,167 +339,178 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ if(__builtin_expect( (t0 == t1), true )) { return t0; - } else { // t0 != t1 - if(t0.getKind() == kind::TYPE_CONSTANT) { - switch(t0.getConst<TypeConstant>()) { - case INTEGER_TYPE: - if(t1.isInteger()) { - // t0 == IntegerType && t1.isInteger() - return t0; //IntegerType - } else if(t1.isReal()) { - // t0 == IntegerType && t1.isReal() && !t1.isInteger() - return NodeManager::currentNM()->realType(); // RealType - } else { - return TypeNode(); // null type - } - case REAL_TYPE: - if(t1.isReal()) { - return t0; // RealType - } else { - return TypeNode(); // null type - } - default: - if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { - return t0; // t0 is a constant type - } else { - return TypeNode(); // null type - } + } + + // t0 != t1 && + if(t0.getKind() == kind::TYPE_CONSTANT) { + switch(t0.getConst<TypeConstant>()) { + case INTEGER_TYPE: + if(t1.isInteger()) { + // t0 == IntegerType && t1.isInteger() + return t0; //IntegerType + } else if(t1.isReal()) { + // t0 == IntegerType && t1.isReal() && !t1.isInteger() + return NodeManager::currentNM()->realType(); // RealType + } else { + return TypeNode(); // null type } - } else if(t1.getKind() == kind::TYPE_CONSTANT) { - return leastCommonTypeNode(t1, t0); // decrease the number of special cases + case REAL_TYPE: + if(t1.isReal()) { + return t0; // RealType + } else { + return TypeNode(); // null type + } + default: + if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { + return t0; // t0 is a constant type + } else { + return TypeNode(); // null type + } + } + } else if(t1.getKind() == kind::TYPE_CONSTANT) { + return leastCommonTypeNode(t1, t0); // decrease the number of special cases + } + + // t0 != t1 && + // t0.getKind() == kind::TYPE_CONSTANT && + // t1.getKind() == kind::TYPE_CONSTANT + switch(t0.getKind()) { + case kind::ARRAY_TYPE: + case kind::BITVECTOR_TYPE: + case kind::SORT_TYPE: + case kind::CONSTRUCTOR_TYPE: + case kind::SELECTOR_TYPE: + case kind::TESTER_TYPE: + if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { + return t0; } else { - // t0 != t1 && - // t0.getKind() == kind::TYPE_CONSTANT && - // t1.getKind() == kind::TYPE_CONSTANT - switch(t0.getKind()) { - case kind::ARRAY_TYPE: - case kind::BITVECTOR_TYPE: - case kind::SORT_TYPE: - case kind::CONSTRUCTOR_TYPE: - case kind::SELECTOR_TYPE: - case kind::TESTER_TYPE: - if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { - return t0; - } else { - return TypeNode(); - } - case kind::FUNCTION_TYPE: - return TypeNode(); // Not sure if this is right - case kind::SEXPR_TYPE: - Unimplemented("haven't implemented leastCommonType for symbolic expressions yet"); - return TypeNode(); - case kind::SUBTYPE_TYPE: - if(t1.isPredicateSubtype()){ - // This is the case where both t0 and t1 are predicate subtypes. - return leastCommonPredicateSubtype(t0, t1); - }else{ // t0 is a predicate subtype and t1 is not - return leastCommonTypeNode(t1, t0); //decrease the number of special cases - } - case kind::SUBRANGE_TYPE: - if(t1.isSubrange()) { - const SubrangeBounds& t0SR = t0.getSubrangeBounds(); - const SubrangeBounds& t1SR = t1.getSubrangeBounds(); - if(SubrangeBounds::joinIsBounded(t0SR, t1SR)) { - SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR); - return NodeManager::currentNM()->mkSubrangeType(j); - } else { - return NodeManager::currentNM()->integerType(); - } - } else if(t1.isPredicateSubtype()) { - // t0 is a subrange - // t1 is not a subrange - // t1 is a predicate subtype - if(t1.isInteger()) { - return NodeManager::currentNM()->integerType(); - } else if(t1.isReal()) { - return NodeManager::currentNM()->realType(); - } else { - return TypeNode(); - } - } else { - // t0 is a subrange - // t1 is not a subrange - // t1 is not a type constant && is not a predicate subtype - // t1 cannot be real subtype or integer. - Assert(t1.isReal()); - Assert(t1.isInteger()); - return TypeNode(); - } - case kind::TUPLE_TYPE: { - // if the other == this one, we returned already, above - if(t0.getBaseType() == t1) { - return t1; - } - if(!t1.isTuple() || t0.getNumChildren() != t1.getNumChildren()) { - // no compatibility between t0, t1 - return TypeNode(); - } - std::vector<TypeNode> types; - // construct childwise leastCommonType, if one exists - for(const_iterator i = t0.begin(), j = t1.begin(); i != t0.end(); ++i, ++j) { - TypeNode kid = leastCommonTypeNode(*i, *j); - if(kid.isNull()) { - // no common supertype: types t0, t1 not compatible - return TypeNode(); - } - types.push_back(kid); - } - // if we make it here, we constructed the least common type - return NodeManager::currentNM()->mkTupleType(types); + return TypeNode(); + } + case kind::FUNCTION_TYPE: + return TypeNode(); // Not sure if this is right + case kind::SET_TYPE: { + // take the least common subtype of element types + TypeNode elementType; + if(t1.isSet() && + ! (elementType = leastCommonTypeNode(t0[0], t1[0])).isNull() ) { + return NodeManager::currentNM()->mkSetType(elementType); + } else { + return TypeNode(); + } + } + case kind::SEXPR_TYPE: + Unimplemented("haven't implemented leastCommonType for symbolic expressions yet"); + return TypeNode(); + case kind::SUBTYPE_TYPE: + if(t1.isPredicateSubtype()){ + // This is the case where both t0 and t1 are predicate subtypes. + return leastCommonPredicateSubtype(t0, t1); + }else{ // t0 is a predicate subtype and t1 is not + return leastCommonTypeNode(t1, t0); //decrease the number of special cases + } + case kind::SUBRANGE_TYPE: + if(t1.isSubrange()) { + const SubrangeBounds& t0SR = t0.getSubrangeBounds(); + const SubrangeBounds& t1SR = t1.getSubrangeBounds(); + if(SubrangeBounds::joinIsBounded(t0SR, t1SR)) { + SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR); + return NodeManager::currentNM()->mkSubrangeType(j); + } else { + return NodeManager::currentNM()->integerType(); } - case kind::RECORD_TYPE: { - // if the other == this one, we returned already, above - if(t0.getBaseType() == t1) { - return t1; - } - const Record& r0 = t0.getConst<Record>(); - if(!t1.isRecord() || r0.getNumFields() != t1.getConst<Record>().getNumFields()) { - // no compatibility between t0, t1 - return TypeNode(); - } - std::vector< std::pair<std::string, Type> > fields; - const Record& r1 = t1.getConst<Record>(); - // construct childwise leastCommonType, if one exists - for(Record::const_iterator i = r0.begin(), j = r1.begin(); i != r0.end(); ++i, ++j) { - TypeNode kid = leastCommonTypeNode(TypeNode::fromType((*i).second), TypeNode::fromType((*j).second)); - if((*i).first != (*j).first || kid.isNull()) { - // if field names differ, or no common supertype, then - // types t0, t1 not compatible - return TypeNode(); - } - fields.push_back(std::make_pair((*i).first, kid.toType())); - } - // if we make it here, we constructed the least common type - return NodeManager::currentNM()->mkRecordType(Record(fields)); + } else if(t1.isPredicateSubtype()) { + // t0 is a subrange + // t1 is not a subrange + // t1 is a predicate subtype + if(t1.isInteger()) { + return NodeManager::currentNM()->integerType(); + } else if(t1.isReal()) { + return NodeManager::currentNM()->realType(); + } else { + return TypeNode(); } - case kind::DATATYPE_TYPE: - // t1 might be a subtype tuple or record - if(t1.getBaseType() == t0) { - return t0; - } - // otherwise no common ancestor + } else { + // t0 is a subrange + // t1 is not a subrange + // t1 is not a type constant && is not a predicate subtype + // t1 cannot be real subtype or integer. + Assert(t1.isReal()); + Assert(t1.isInteger()); + return TypeNode(); + } + case kind::TUPLE_TYPE: { + // if the other == this one, we returned already, above + if(t0.getBaseType() == t1) { + return t1; + } + if(!t1.isTuple() || t0.getNumChildren() != t1.getNumChildren()) { + // no compatibility between t0, t1 + return TypeNode(); + } + std::vector<TypeNode> types; + // construct childwise leastCommonType, if one exists + for(const_iterator i = t0.begin(), j = t1.begin(); i != t0.end(); ++i, ++j) { + TypeNode kid = leastCommonTypeNode(*i, *j); + if(kid.isNull()) { + // no common supertype: types t0, t1 not compatible return TypeNode(); - case kind::PARAMETRIC_DATATYPE: { - if(!t1.isParametricDatatype()) { - return TypeNode(); - } - while(t1.getKind() != kind::PARAMETRIC_DATATYPE) { - t1 = t1.getSubtypeParentType(); - } - if(t0[0] != t1[0] || t0.getNumChildren() != t1.getNumChildren()) { - return TypeNode(); - } - vector<Type> v; - for(size_t i = 1; i < t0.getNumChildren(); ++i) { - v.push_back(leastCommonTypeNode(t0[i], t1[i]).toType()); - } - return TypeNode::fromType(t0[0].getDatatype().getDatatypeType(v)); } - default: - Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str()); + types.push_back(kid); + } + // if we make it here, we constructed the least common type + return NodeManager::currentNM()->mkTupleType(types); + } + case kind::RECORD_TYPE: { + // if the other == this one, we returned already, above + if(t0.getBaseType() == t1) { + return t1; + } + const Record& r0 = t0.getConst<Record>(); + if(!t1.isRecord() || r0.getNumFields() != t1.getConst<Record>().getNumFields()) { + // no compatibility between t0, t1 + return TypeNode(); + } + std::vector< std::pair<std::string, Type> > fields; + const Record& r1 = t1.getConst<Record>(); + // construct childwise leastCommonType, if one exists + for(Record::const_iterator i = r0.begin(), j = r1.begin(); i != r0.end(); ++i, ++j) { + TypeNode kid = leastCommonTypeNode(TypeNode::fromType((*i).second), TypeNode::fromType((*j).second)); + if((*i).first != (*j).first || kid.isNull()) { + // if field names differ, or no common supertype, then + // types t0, t1 not compatible return TypeNode(); } + fields.push_back(std::make_pair((*i).first, kid.toType())); + } + // if we make it here, we constructed the least common type + return NodeManager::currentNM()->mkRecordType(Record(fields)); + } + case kind::DATATYPE_TYPE: + // t1 might be a subtype tuple or record + if(t1.getBaseType() == t0) { + return t0; + } + // otherwise no common ancestor + return TypeNode(); + case kind::PARAMETRIC_DATATYPE: { + if(!t1.isParametricDatatype()) { + return TypeNode(); + } + while(t1.getKind() != kind::PARAMETRIC_DATATYPE) { + t1 = t1.getSubtypeParentType(); + } + if(t0[0] != t1[0] || t0.getNumChildren() != t1.getNumChildren()) { + return TypeNode(); } + vector<Type> v; + for(size_t i = 1; i < t0.getNumChildren(); ++i) { + v.push_back(leastCommonTypeNode(t0[i], t1[i]).toType()); + } + return TypeNode::fromType(t0[0].getDatatype().getDatatypeType(v)); + } + default: + Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str()); + return TypeNode(); } } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 72a04ae29..2991ab21b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -277,9 +277,6 @@ class CVC4_PUBLIC SmtEngine { * as often as you like. Should be called whenever the final options * and logic for the problem are set (at least, those options that are * not permitted to change after assertions and queries are made). - * - * FIXME: Above comment not true. Please don't call this more than - * once. (6/14/2012 -- K) */ void finalOptionsAreSet(); 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/kinds b/src/theory/sets/kinds index 68941489f..e46f3a4f8 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -8,6 +8,7 @@ theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h" typechecker "theory/sets/theory_sets_type_rules.h" rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h" +properties parametric properties check propagate #presolve postsolve # Theory content goes here. diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 91195e67e..3a5b61390 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -34,10 +34,18 @@ TheorySets::~TheorySets() { delete d_internal; } +void TheorySets::addSharedTerm(TNode n) { + d_internal->addSharedTerm(n); +} + 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..f40031514 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -46,9 +46,11 @@ public: ~TheorySets(); + void addSharedTerm(TNode); + void check(Effort); - void propagate(Effort); + void collectModelInfo(TheoryModel*, bool fullModel); Node explain(TNode); @@ -56,6 +58,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..70b757f0c 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 <boost/foreach.hpp> + +#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; @@ -50,6 +54,19 @@ void TheorySetsPrivate::check(Theory::Effort level) { bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; + if (!assertion.isPreregistered) { + if (atom.getKind() == kind::EQUAL) { + if (!d_equalityEngine.hasTerm(atom[0])) { + Assert(atom[0].isConst()); + d_equalityEngine.addTerm(atom[0]); + } + if (!d_equalityEngine.hasTerm(atom[1])) { + Assert(atom[1].isConst()); + d_equalityEngine.addTerm(atom[1]); + } + } + } + // Solve each switch(atom.getKind()) { case kind::EQUAL: @@ -70,14 +87,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; } - Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; - if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) { d_external.d_out->lemma(getLemma()); } @@ -356,8 +370,205 @@ 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 ********************/ + +const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements +(TNode setterm, SettermElementsMap& settermElementsMap) const { + SettermElementsMap::const_iterator it = settermElementsMap.find(setterm); + bool alreadyCalculated = (it != settermElementsMap.end()); + if( !alreadyCalculated ) { + + 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(k == kind::VARIABLE || k == kind::APPLY_UF); + /* assign emptyset, which is default */ + } + + it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first; + } + return it->second; } + + +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 : { "; + BOOST_FOREACH(TNode element, saved) { Debug("sets-model") << element << ", "; } + 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 : { "; + BOOST_FOREACH(TNode element, cur) { Debug("sets-model") << element << ", "; } + 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() ) { + 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<Node> terms; + + // 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); + ! it_eqclasses.isFinished() ; ++it_eqclasses) { + TNode n = (*it_eqclasses); + if(n.getKind() == kind::MEMBER) { + Assert(d_equalityEngine.areEqual(n, true_atom)); + TNode x = d_equalityEngine.getRepresentative(n[0]); + TNode S = d_equalityEngine.getRepresentative(n[1]); + settermElementsMap[S].insert(x); + } + } + + // Assert equalities and disequalities to the model + m->assertEqualityEngine(&d_equalityEngine, &terms); + + // Loop over terms to collect set-terms for which we generate models + set<Node> settermsModEq; + 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.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; + } + } + + 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); + } + +#ifdef CVC4_ASSERTIONS + BOOST_FOREACH(TNode term, terms) { + if( term.getType().isSet() ) { + checkModel(settermElementsMap, term); + } + } +#endif +} + + /********************** Helper functions ***************************/ /********************** Helper functions ***************************/ /********************** Helper functions ***************************/ @@ -404,6 +615,7 @@ Node mkAnd(const std::vector<TNode>& conjunctions) { TheorySetsPrivate::Statistics::Statistics() : d_checkTime("theory::sets::time") { + StatisticsRegistry::registerStat(&d_checkTime); } @@ -474,20 +686,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(); } @@ -499,6 +718,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); @@ -507,16 +727,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)); } @@ -551,18 +767,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; @@ -582,6 +793,11 @@ bool TheorySetsPrivate::propagate(TNode literal) { }/* TheorySetsPropagate::propagate(TNode) */ +void TheorySetsPrivate::addSharedTerm(TNode n) { + Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl; + d_equalityEngine.addTriggerTerm(n, THEORY_SETS); +} + void TheorySetsPrivate::conflict(TNode a, TNode b) { if (a.getKind() == kind::CONST_BOOLEAN) { @@ -655,7 +871,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 +883,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 +894,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 +908,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..62274e1ce 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -47,16 +47,18 @@ public: ~TheorySetsPrivate(); + void addSharedTerm(TNode); + 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 +80,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 */ @@ -157,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) const; + 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/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index db67576d8..109d8bb0e 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -20,47 +20,68 @@ namespace CVC4 { namespace theory { namespace sets { +typedef std::set<TNode> Elements; +typedef std::hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap; + bool checkConstantMembership(TNode elementTerm, TNode setTerm) { - switch(setTerm.getKind()) { - case kind::EMPTYSET: + // 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; - case kind::SET_SINGLETON: + } + + if(setTerm.getKind() == kind::SET_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(); } + + Assert(setTerm.getKind() == kind::UNION && setTerm[1].getKind() == kind::SET_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::SET_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(); + // } } // static RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager* nm = NodeManager::currentNM(); + Kind kind = node.getKind(); - switch(node.getKind()) { + switch(kind) { case kind::MEMBER: { if(!node[0].isConst() || !node[1].isConst()) break; // both are constants - bool isMember = checkConstantMembership(node[0], node[1]); + TNode S = preRewrite(node[1]).node; + bool isMember = checkConstantMembership(node[0], S); return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember)); - } + }//kind::MEMBER case kind::SUBSET: { // rewrite (A subset-or-equal B) as (A union B = B) TNode A = node[0]; TNode B = node[1]; - return RewriteResponse(REWRITE_AGAIN, + return RewriteResponse(REWRITE_AGAIN_FULL, nm->mkNode(kind::EQUAL, nm->mkNode(kind::UNION, A, B), B) ); @@ -85,30 +106,133 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { return RewriteResponse(REWRITE_DONE, newNode); } break; - } + }//kind::IFF + + case kind::SETMINUS: { + if(node[0] == node[1]) { + Node newNode = nm->mkConst(EmptySet(nm->toType(node[0].getType()))); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; + return RewriteResponse(REWRITE_DONE, newNode); + } else if(node[0].getKind() == kind::EMPTYSET || + 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] > 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, newNode); + } + break; + }//kind::INTERSECION - case kind::UNION: case kind::INTERSECTION: { if(node[0] == node[1]) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; return RewriteResponse(REWRITE_DONE, node[0]); + } else if(node[0].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, node[0]); + } else if(node[1].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, node[1]); } 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, newNode); } break; - } + }//kind::INTERSECION - default: + case kind::UNION: { + if(node[0] == node[1]) { + Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; + return RewriteResponse(REWRITE_DONE, node[0]); + } else if(node[0].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, node[1]); + } else if(node[1].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, node[0]); + } 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, newNode); + } break; + }//kind::UNION + default: + break; }//switch(node.getKind()) // This default implementation 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::SET_SINGLETON: + Assert(setterm[0].isConst()); + cur.insert(setterm[0]); + break; + default: + Unhandled(); + } + } + + it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first; + } + return it->second; +} + +Node elementsToNormalConstant(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 = nm->mkNode(kind::SET_SINGLETON, *it); + while( ++it != elements.end() ) { + cur = nm->mkNode(kind::UNION, cur, + nm->mkNode(kind::SET_SINGLETON, *it)); + } + return cur; + } +} + + // static RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { NodeManager* nm = NodeManager::currentNM(); @@ -118,6 +242,13 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { return RewriteResponse(REWRITE_DONE, nm->mkConst(true)); // Further optimization, if constants but differing ones + if(node.getType().isSet() && node.isConst()) { + //rewrite set to normal form + SettermElementsMap setTermElementsMap; // cache + const Elements& elements = collectConstantElements(node, setTermElementsMap); + return RewriteResponse(REWRITE_DONE, elementsToNormalConstant(elements, node.getType())); + } + return RewriteResponse(REWRITE_DONE, node); } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 4f753187f..405fceb6f 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -64,6 +64,8 @@ Node TheoryModel::getValue(TNode n) const { //normalize nn = Rewriter::rewrite(nn); } + Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): returning" + << nn << std::endl; return nn; } @@ -779,7 +781,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) << "n: " << n << endl << "getValue(n): " << tm->getValue(n) << endl << "rep: " << rep << endl; - Assert(tm->getValue(*eqc_i) == rep); + Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details"); } } } 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 */ diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 32a96ec21..fe53838be 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -53,6 +53,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/error1.smt2 b/test/regress/regress0/sets/error1.smt2 index c4b3dd551..1241b117f 100644 --- a/test/regress/regress0/sets/error1.smt2 +++ b/test/regress/regress0/sets/error1.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_UFLIA_SETS) (set-info :status sat) diff --git a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 index 290ee95d5..7a8661e4d 100644 --- a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 +++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 index bcc4c33da..0aa6c88ae 100644 --- a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 +++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 index 5a44c0344..35110d831 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 index 67d64bd05..d0fda8b86 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) 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..1ea3ea6b5 --- /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) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index c85ae4837..accb09799 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2 new file mode 100644 index 000000000..9dd257401 --- /dev/null +++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +(set-logic QF_UFLIA_SETS) +(set-info :status sat) +(declare-fun x () (Set Int)) +(declare-fun y () (Set Int)) +(assert (not (= x y))) +(check-sat) diff --git a/test/regress/regress0/sets/sets-testlemma-reals.smt2 b/test/regress/regress0/sets/sets-testlemma-reals.smt2 new file mode 100644 index 000000000..16e7780b4 --- /dev/null +++ b/test/regress/regress0/sets/sets-testlemma-reals.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +(set-logic QF_UFLRA_SETS) +(set-info :status sat) +(declare-fun x () (Set Real)) +(declare-fun y () (Set Real)) +(assert (not (= x y))) +(check-sat) diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2 index 74ce72747..183f54242 100644 --- a/test/regress/regress0/sets/sets-testlemma.smt2 +++ b/test/regress/regress0/sets/sets-testlemma.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFBV_SETS) (set-info :status sat) (declare-fun x () (Set (_ BitVec 2))) (declare-fun y () (Set (_ BitVec 2))) diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2 index 6f6d3e019..656a0bc88 100644 --- a/test/regress/regress0/sets/sets-union.smt2 +++ b/test/regress/regress0/sets/sets-union.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-check-model +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: unsat (set-logic ALL_SUPPORTED) diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2 index 59c2a2024..7bbe442e1 100644 --- a/test/regress/regress0/sets/union-1a-flip.smt2 +++ b/test/regress/regress0/sets/union-1a-flip.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-check-models +; COMMAND-LINE: --incremental ; EXPECT: unsat ; EXPECT: sat diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2 index 86fed459b..72c544553 100644 --- a/test/regress/regress0/sets/union-1b-flip.smt2 +++ b/test/regress/regress0/sets/union-1b-flip.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-check-models +; COMMAND-LINE: --incremental ; EXPECT: unsat ; EXPECT: sat diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2 index 32d949a53..e5e96be5a 100644 --- a/test/regress/regress0/sets/union-2.smt2 +++ b/test/regress/regress0/sets/union-2.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) |