summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/logic_info.cpp6
-rw-r--r--src/theory/quantifiers/term_database.cpp2
-rw-r--r--src/theory/quantifiers/trigger.cpp2
-rw-r--r--src/theory/sets/expr_patterns.h4
-rw-r--r--src/theory/sets/kinds17
-rw-r--r--src/theory/sets/options4
-rw-r--r--src/theory/sets/theory_sets.cpp18
-rw-r--r--src/theory/sets/theory_sets.h6
-rw-r--r--src/theory/sets/theory_sets_private.cpp55
-rw-r--r--src/theory/sets/theory_sets_private.h2
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp21
-rw-r--r--src/theory/sets/theory_sets_type_enumerator.h2
-rw-r--r--src/theory/sets/theory_sets_type_rules.h42
13 files changed, 130 insertions, 51 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 78f4996b8..bc2f1286b 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -129,7 +129,7 @@ std::string LogicInfo::getLogicString() const {
++seen;
}
if(d_theories[THEORY_SETS]) {
- ss << "_SETS";
+ ss << "FS";
++seen;
}
@@ -272,9 +272,9 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
arithNonLinear();
p += 4;
}
- if(!strncmp(p, "_SETS", 5)) {
+ if(!strncmp(p, "FS", 2)) {
enableTheory(THEORY_SETS);
- p += 5;
+ p += 2;
}
}
}
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9f25b0825..2c309899d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -74,7 +74,7 @@ unsigned TermDb::getNumGroundTerms( Node f ) {
Node TermDb::getOperator( Node n ) {
//return n.getOperator();
Kind k = n.getKind();
- if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON ){
+ if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ){
//since it is parametric, use a particular one as op
TypeNode tn = n[0].getType();
Node op = n.getOperator();
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 77a4efff5..0d8f2c06d 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -330,7 +330,7 @@ bool Trigger::isAtomicTrigger( Node n ){
bool Trigger::isAtomicTriggerKind( Kind k ) {
return k==APPLY_UF || k==SELECT || k==STORE ||
k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
- k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON;
+ k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON;
}
bool Trigger::isSimpleTrigger( Node n ){
diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h
index bc5b6b9e0..93307d227 100644
--- a/src/theory/sets/expr_patterns.h
+++ b/src/theory/sets/expr_patterns.h
@@ -44,8 +44,8 @@ static Node MEMBER(TNode a, TNode b) {
return NodeManager::currentNM()->mkNode(kind::MEMBER, a, b);
}
-static Node SET_SINGLETON(TNode a) {
- return NodeManager::currentNM()->mkNode(kind::SET_SINGLETON, a);
+static Node SINGLETON(TNode a) {
+ return NodeManager::currentNM()->mkNode(kind::SINGLETON, a);
}
static Node EQUAL(TNode a, TNode b) {
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 12f114fc0..39e7883c6 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -19,10 +19,10 @@ constant EMPTYSET \
::CVC4::EmptySet \
::CVC4::EmptySetHashFunction \
"util/emptyset.h" \
- "empty set"
+ "the empty set constant; payload is an instance of the CVC4::EmptySet class"
# the type
-operator SET_TYPE 1 "set type"
+operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
cardinality SET_TYPE \
"::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
"theory/sets/theory_sets_type_rules.h"
@@ -38,21 +38,24 @@ enumerator SET_TYPE \
operator UNION 2 "set union"
operator INTERSECTION 2 "set intersection"
operator SETMINUS 2 "set subtraction"
-operator SUBSET 2 "subset"
-operator MEMBER 2 "set membership"
-operator SET_SINGLETON 1 "singleton set"
+operator SUBSET 2 "subset predicate; first parameter a subset of second"
+operator MEMBER 2 "set membership predicate; first parameter a member of second"
+operator SINGLETON 1 "the set of the single element given as a parameter"
+operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule SUBSET ::CVC4::theory::sets::SubsetTypeRule
typerule MEMBER ::CVC4::theory::sets::MemberTypeRule
-typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule
typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
+typerule INSERT ::CVC4::theory::sets::InsertTypeRule
construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
-construle SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule
+construle INSERT ::CVC4::theory::sets::InsertTypeRule
endtheory
diff --git a/src/theory/sets/options b/src/theory/sets/options
index dc6c6e907..1c95e78e4 100644
--- a/src/theory/sets/options
+++ b/src/theory/sets/options
@@ -8,7 +8,7 @@ module SETS "theory/sets/options.h" Sets
option setsPropagate --sets-propagate bool :default true
determines whether to propagate learnt facts to Theory Engine / SAT solver
-option setsEagerLemmas --sets-eager-lemmas bool :default false
- if true, will add lemmas even if not at FULL_EFFORT
+option setsEagerLemmas --sets-eager-lemmas bool :default true
+ add lemmas even at regular effort
endmodule
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index c230b9ac5..5d5e1f9ee 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -34,10 +34,6 @@ TheorySets::~TheorySets() {
delete d_internal;
}
-void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_internal->setMasterEqualityEngine(eq);
-}
-
void TheorySets::addSharedTerm(TNode n) {
d_internal->addSharedTerm(n);
}
@@ -50,8 +46,8 @@ void TheorySets::collectModelInfo(TheoryModel* m, bool fullModel) {
d_internal->collectModelInfo(m, fullModel);
}
-void TheorySets::propagate(Effort e) {
- d_internal->propagate(e);
+void TheorySets::computeCareGraph() {
+ d_internal->computeCareGraph();
}
Node TheorySets::explain(TNode node) {
@@ -59,7 +55,15 @@ Node TheorySets::explain(TNode node) {
}
void TheorySets::preRegisterTerm(TNode node) {
- return d_internal->preRegisterTerm(node);
+ d_internal->preRegisterTerm(node);
+}
+
+void TheorySets::propagate(Effort e) {
+ d_internal->propagate(e);
+}
+
+void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_internal->setMasterEqualityEngine(eq);
}
}/* CVC4::theory::sets namespace */
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 6ff41d5f5..84d91de72 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -48,14 +48,14 @@ public:
~TheorySets();
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
void addSharedTerm(TNode);
void check(Effort);
void collectModelInfo(TheoryModel*, bool fullModel);
+ void computeCareGraph();
+
Node explain(TNode);
std::string identify() const { return "THEORY_SETS"; }
@@ -64,6 +64,8 @@ public:
void propagate(Effort);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
};/* 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 f768bd62d..be2b48f81 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -97,7 +97,7 @@ void TheorySetsPrivate::check(Theory::Effort level) {
Debug("sets") << "[sets] is complete = " << isComplete() << std::endl;
}
- if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
+ if( (level == Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
d_external.d_out->lemma(getLemma());
return;
}
@@ -225,7 +225,7 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
if(S.getKind() == kind::UNION ||
S.getKind() == kind::INTERSECTION ||
S.getKind() == kind::SETMINUS ||
- S.getKind() == kind::SET_SINGLETON) {
+ S.getKind() == kind::SINGLETON) {
doSettermPropagation(x, S);
if(d_conflict) return;
}// propagation: children
@@ -276,7 +276,7 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
left_literal = MEMBER(x, S[0]) ;
right_literal = NOT( MEMBER(x, S[1]) );
break;
- case kind::SET_SINGLETON: {
+ case kind::SINGLETON: {
Node atom = MEMBER(x, S);
if(holds(atom, true)) {
learnLiteral(EQUAL(x, S[0]), true, atom);
@@ -408,6 +408,42 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
}/*TheorySetsPrivate::learnLiteral(...)*/
+/************************ Sharing ************************/
+/************************ Sharing ************************/
+/************************ Sharing ************************/
+
+void TheorySetsPrivate::addSharedTerm(TNode n) {
+ Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
+ d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
+}
+
+
+void TheorySetsPrivate::computeCareGraph() {
+ Debug("sharing") << "Theory::computeCareGraph<" << d_external.identify() << ">()" << endl;
+ for (unsigned i = 0; i < d_external.d_sharedTerms.size(); ++ i) {
+ TNode a = d_external.d_sharedTerms[i];
+ TypeNode aType = a.getType();
+ for (unsigned j = i + 1; j < d_external.d_sharedTerms.size(); ++ j) {
+ TNode b = d_external.d_sharedTerms[j];
+ if (b.getType() != aType) {
+ // We don't care about the terms of different types
+ continue;
+ }
+ switch (d_external.d_valuation.getEqualityStatus(a, b)) {
+ case EQUALITY_TRUE_AND_PROPAGATED:
+ case EQUALITY_FALSE_AND_PROPAGATED:
+ // If we know about it, we should have propagated it, so we can skip
+ break;
+ default:
+ // Let's split on it
+ d_external.addCarePair(a, b);
+ break;
+ }
+ }
+ }
+}
+
+
/******************** Model generation ********************/
/******************** Model generation ********************/
/******************** Model generation ********************/
@@ -535,9 +571,9 @@ Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) con
return nm->mkConst(EmptySet(nm->toType(setType)));
} else {
Elements::iterator it = elements.begin();
- Node cur = SET_SINGLETON(*it);
+ Node cur = SINGLETON(*it);
while( ++it != elements.end() ) {
- cur = nm->mkNode(kind::UNION, cur, SET_SINGLETON(*it));
+ cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
}
return cur;
}
@@ -886,11 +922,6 @@ void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
-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) {
@@ -948,7 +979,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
// d_equalityEngine.addTerm(node);
}
- if(node.getKind() == kind::SET_SINGLETON) {
+ if(node.getKind() == kind::SINGLETON) {
Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
learnLiteral(MEMBER(node[0], node), true, true_node);
//intentional fallthrough
@@ -1125,7 +1156,7 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
if(S.getKind() == kind::UNION ||
S.getKind() == kind::INTERSECTION ||
S.getKind() == kind::SETMINUS ||
- S.getKind() == kind::SET_SINGLETON) {
+ S.getKind() == kind::SINGLETON) {
d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
}// propagation: children
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 90dec7c0b..e5d7beb2c 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -56,6 +56,8 @@ public:
void collectModelInfo(TheoryModel*, bool fullModel);
+ void computeCareGraph();
+
Node explain(TNode);
void preRegisterTerm(TNode node);
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 7b02c1bfb..8716d1065 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -32,11 +32,11 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
return false;
}
- if(setTerm.getKind() == kind::SET_SINGLETON) {
+ if(setTerm.getKind() == kind::SINGLETON) {
return elementTerm == setTerm[0];
}
- Assert(setTerm.getKind() == kind::UNION && setTerm[1].getKind() == kind::SET_SINGLETON,
+ 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]);
@@ -44,7 +44,7 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
// switch(setTerm.getKind()) {
// case kind::EMPTYSET:
// return false;
- // case kind::SET_SINGLETON:
+ // case kind::SINGLETON:
// return elementTerm == setTerm[0];
// case kind::UNION:
// return checkConstantMembership(elementTerm, setTerm[0]) ||
@@ -195,7 +195,7 @@ const Elements& collectConstantElements(TNode setterm, SettermElementsMap& sette
case kind::EMPTYSET:
/* assign emptyset, which is default */
break;
- case kind::SET_SINGLETON:
+ case kind::SINGLETON:
Assert(setterm[0].isConst());
cur.insert(TheorySetsRewriter::preRewrite(setterm[0]).node);
break;
@@ -220,10 +220,10 @@ Node elementsToNormalConstant(Elements elements,
} else {
Elements::iterator it = elements.begin();
- Node cur = nm->mkNode(kind::SET_SINGLETON, *it);
+ Node cur = nm->mkNode(kind::SINGLETON, *it);
while( ++it != elements.end() ) {
cur = nm->mkNode(kind::UNION, cur,
- nm->mkNode(kind::SET_SINGLETON, *it));
+ nm->mkNode(kind::SINGLETON, *it));
}
return cur;
}
@@ -239,6 +239,15 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
// Further optimization, if constants but differing ones
+ 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]));
+ }
+ return RewriteResponse(REWRITE_AGAIN, nm->mkNode(kind::UNION, insertedElements, node[setNodeIndex]));
+ }//kind::INSERT
+
if(node.getType().isSet() && node.isConst()) {
//rewrite set to normal form
SettermElementsMap setTermElementsMap; // cache
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index 2f4cc6a2f..97fbfe94f 100644
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -76,7 +76,7 @@ public:
Assert(d_index == 0 || d_index == 1);
if(d_index == 1) {
- n = d_nm->mkNode(kind::SET_SINGLETON, *(*(d_constituentVec[0])));
+ n = d_nm->mkNode(kind::SINGLETON, *(*(d_constituentVec[0])));
}
// for (unsigned i = 0; i < d_indexVec.size(); ++i) {
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 3b2acd956..fa1183e07 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -105,20 +105,20 @@ struct MemberTypeRule {
}
return nodeManager->booleanType();
}
-};/* struct SetInTypeRule */
+};/* struct MemberTypeRule */
-struct SetSingletonTypeRule {
+struct SingletonTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate, AssertionException) {
- Assert(n.getKind() == kind::SET_SINGLETON);
+ Assert(n.getKind() == kind::SINGLETON);
return nodeManager->mkSetType(n[0].getType(check));
}
inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
- Assert(n.getKind() == kind::SET_SINGLETON);
+ Assert(n.getKind() == kind::SINGLETON);
return n[0].isConst();
}
-};/* struct SetInTypeRule */
+};/* struct SingletonTypeRule */
struct EmptySetTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -128,7 +128,35 @@ struct EmptySetTypeRule {
Type setType = emptySet.getType();
return TypeNode::fromType(setType);
}
-};
+};/* struct EmptySetTypeRule */
+
+struct InsertTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::INSERT);
+ size_t numChildren = n.getNumChildren();
+ Assert( numChildren >= 2 );
+ TypeNode setType = n[numChildren-1].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "inserting into a non-set");
+ }
+ for(size_t i = 0; i < numChildren-1; ++i) {
+ TypeNode elementType = n[i].getType(check);
+ if(elementType != setType.getSetElementType()) {
+ throw TypeCheckingExceptionPrivate
+ (n, "type of element should be same as element type of set being inserted into");
+ }
+ }
+ }
+ return setType;
+ }
+
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ Assert(n.getKind() == kind::INSERT);
+ return n[0].isConst() && n[1].isConst();
+ }
+};/* struct InsertTypeRule */
struct SetsProperties {
@@ -146,7 +174,7 @@ struct SetsProperties {
Assert(type.isSet());
return NodeManager::currentNM()->mkConst(EmptySet(type.toType()));
}
-};
+};/* struct SetsProperties */
}/* CVC4::theory::sets namespace */
}/* CVC4::theory namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback