summaryrefslogtreecommitdiff
path: root/src/theory/sets
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sets')
-rw-r--r--src/theory/sets/.gitignore1
-rw-r--r--src/theory/sets/Makefile4
-rw-r--r--src/theory/sets/Makefile.am20
-rw-r--r--src/theory/sets/expr_patterns.h51
-rw-r--r--src/theory/sets/kinds55
-rw-r--r--src/theory/sets/options14
-rw-r--r--src/theory/sets/options_handlers.h14
-rw-r--r--src/theory/sets/term_info.h57
-rw-r--r--src/theory/sets/theory_sets.cpp55
-rw-r--r--src/theory/sets/theory_sets.h65
-rw-r--r--src/theory/sets/theory_sets_private.cpp871
-rw-r--r--src/theory/sets/theory_sets_private.h166
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp110
-rw-r--r--src/theory/sets/theory_sets_rewriter.h77
-rw-r--r--src/theory/sets/theory_sets_type_enumerator.h161
-rw-r--r--src/theory/sets/theory_sets_type_rules.h176
16 files changed, 1897 insertions, 0 deletions
diff --git a/src/theory/sets/.gitignore b/src/theory/sets/.gitignore
new file mode 100644
index 000000000..4c83ffd6f
--- /dev/null
+++ b/src/theory/sets/.gitignore
@@ -0,0 +1 @@
+README.WHATS-NEXT
diff --git a/src/theory/sets/Makefile b/src/theory/sets/Makefile
new file mode 100644
index 000000000..68a2c5cb6
--- /dev/null
+++ b/src/theory/sets/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/sets
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/sets/Makefile.am b/src/theory/sets/Makefile.am
new file mode 100644
index 000000000..00678628f
--- /dev/null
+++ b/src/theory/sets/Makefile.am
@@ -0,0 +1,20 @@
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libsets.la
+
+libsets_la_SOURCES = \
+ theory_sets.h \
+ theory_sets.cpp \
+ theory_sets_private.h \
+ theory_sets_private.cpp \
+ theory_sets_rewriter.h \
+ theory_sets_rewriter.cpp \
+ theory_sets_type_rules.h \
+ theory_set_type_enumerator.h
+
+EXTRA_DIST = \
+ kinds \
+ options_handlers.h
diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h
new file mode 100644
index 000000000..089549457
--- /dev/null
+++ b/src/theory/sets/expr_patterns.h
@@ -0,0 +1,51 @@
+/********************* */
+/*! \file expr_patterns.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Expr patterns.
+ **
+ ** Expr patterns.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace expr {
+namespace pattern {
+
+static Node AND(TNode a, TNode b) {
+ return NodeManager::currentNM()->mkNode(kind::AND, a, b);
+}
+
+static Node OR(TNode a, TNode b) {
+ return NodeManager::currentNM()->mkNode(kind::OR, a, b);
+}
+
+static Node OR(TNode a, TNode b, TNode c) {
+ return NodeManager::currentNM()->mkNode(kind::OR, a, b, c);
+}
+
+static Node IN(TNode a, TNode b) {
+ return NodeManager::currentNM()->mkNode(kind::IN, a, b);
+}
+
+static Node EQUAL(TNode a, TNode b) {
+ return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
+}
+
+static Node NOT(TNode a) {
+ return NodeManager::currentNM()->mkNode(kind::NOT, a);
+}
+
+}/* CVC4::expr::pattern namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
new file mode 100644
index 000000000..bae0c5f1d
--- /dev/null
+++ b/src/theory/sets/kinds
@@ -0,0 +1,55 @@
+# kinds -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+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 check propagate #presolve postsolve
+
+# Theory content goes here.
+
+# constants...
+constant EMPTYSET \
+ ::CVC4::EmptySet \
+ ::CVC4::EmptySetHashFunction \
+ "util/emptyset.h" \
+ "empty set"
+
+# types...
+operator SET_TYPE 1 "set type" # the type
+cardinality SET_TYPE \
+ "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
+ "theory/sets/theory_sets_type_rules.h"
+well-founded SET_TYPE \
+ "::CVC4::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
+ "::CVC4::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
+ "theory/sets/theory_sets_type_rules.h"
+enumerator SET_TYPE \
+ "::CVC4::theory::sets::SetEnumerator" \
+ "theory/sets/theory_sets_type_enumerator.h"
+
+# operators...
+operator UNION 2 "set union"
+operator INTERSECTION 2 "set intersection"
+operator SETMINUS 2 "set subtraction"
+operator SUBSET 2 "subset"
+operator IN 2 "set membership"
+
+operator SET_SINGLETON 1 "singleton set"
+
+typerule UNION ::CVC4::theory::sets::SetUnionTypeRule
+typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule
+typerule SETMINUS ::CVC4::theory::sets::SetSetminusTypeRule
+typerule SUBSET ::CVC4::theory::sets::SetSubsetTypeRule
+typerule IN ::CVC4::theory::sets::SetInTypeRule
+typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
+
+construle SET_SINGLETON ::CVC4::theory::sets::SetConstTypeRule
+construle UNION ::CVC4::theory::sets::SetConstTypeRule
+
+endtheory
diff --git a/src/theory/sets/options b/src/theory/sets/options
new file mode 100644
index 000000000..dc6c6e907
--- /dev/null
+++ b/src/theory/sets/options
@@ -0,0 +1,14 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+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
+
+endmodule
diff --git a/src/theory/sets/options_handlers.h b/src/theory/sets/options_handlers.h
new file mode 100644
index 000000000..ff535945e
--- /dev/null
+++ b/src/theory/sets/options_handlers.h
@@ -0,0 +1,14 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H */
diff --git a/src/theory/sets/term_info.h b/src/theory/sets/term_info.h
new file mode 100644
index 000000000..ea435d9b7
--- /dev/null
+++ b/src/theory/sets/term_info.h
@@ -0,0 +1,57 @@
+/********************* */
+/*! \file term_info.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Term info.
+ **
+ ** Term info.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+
+typedef context::CDList<TNode> CDTNodeList;
+typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+
+class TheorySetsTermInfo {
+public:
+ CDTNodeList* elementsInThisSet;
+ CDTNodeList* elementsNotInThisSet;
+ CDTNodeList* parents;
+
+ TheorySetsTermInfo(context::Context* c)
+ {
+ elementsInThisSet = new(true)CDTNodeList(c);
+ elementsNotInThisSet = new(true)CDTNodeList(c);
+ parents = new(true)CDTNodeList(c);
+ }
+
+ void addToElementList(TNode n, bool polarity) {
+ if(polarity) elementsInThisSet -> push_back(n);
+ else elementsNotInThisSet -> push_back(n);
+ }
+
+ ~TheorySetsTermInfo() {
+ elementsInThisSet -> deleteSelf();
+ elementsNotInThisSet -> deleteSelf();
+ parents -> deleteSelf();
+ }
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
new file mode 100644
index 000000000..91195e67e
--- /dev/null
+++ b/src/theory/sets/theory_sets.cpp
@@ -0,0 +1,55 @@
+/********************* */
+/*! \file theory_sets.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory.
+ **
+ ** Sets theory.
+ **/
+
+#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+TheorySets::TheorySets(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo) :
+ Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
+ d_internal(new TheorySetsPrivate(*this, c, u)) {
+}
+
+TheorySets::~TheorySets() {
+ delete d_internal;
+}
+
+void TheorySets::check(Effort e) {
+ d_internal->check(e);
+}
+
+void TheorySets::propagate(Effort e) {
+ d_internal->propagate(e);
+}
+
+Node TheorySets::explain(TNode node) {
+ return d_internal->explain(node);
+}
+
+void TheorySets::preRegisterTerm(TNode node) {
+ return d_internal->preRegisterTerm(node);
+}
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
new file mode 100644
index 000000000..c95229f05
--- /dev/null
+++ b/src/theory/sets/theory_sets.h
@@ -0,0 +1,65 @@
+/********************* */
+/*! \file theory_sets.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory.
+ **
+ ** Sets theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_H
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsPrivate;
+
+class TheorySets : public Theory {
+private:
+ friend class TheorySetsPrivate;
+ TheorySetsPrivate* d_internal;
+public:
+
+ /**
+ * Constructs a new instance of TheorySets w.r.t. the provided
+ * contexts.
+ */
+ TheorySets(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo);
+
+ ~TheorySets();
+
+ void check(Effort);
+
+ void propagate(Effort);
+
+ Node explain(TNode);
+
+ std::string identify() const { return "THEORY_SETS"; }
+
+ void preRegisterTerm(TNode node);
+
+};/* class TheorySets */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_H */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
new file mode 100644
index 000000000..8fd490554
--- /dev/null
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -0,0 +1,871 @@
+/********************* */
+/*! \file theory_sets_private.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory implementation.
+ **
+ ** Sets theory implementation.
+ **/
+
+#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/result.h"
+
+using namespace std;
+using namespace CVC4::expr::pattern;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+const char* element_of_str = " \u2208 ";
+
+/**************************** TheorySetsPrivate *****************************/
+/**************************** TheorySetsPrivate *****************************/
+/**************************** TheorySetsPrivate *****************************/
+
+void TheorySetsPrivate::check(Theory::Effort level) {
+
+ CodeTimer checkCodeTimer(d_statistics.d_checkTime);
+
+ while(!d_external.done() && !d_conflict) {
+ // Get all the assertions
+ Assertion assertion = d_external.get();
+ TNode fact = assertion.assertion;
+
+ Debug("sets") << "\n\n[sets] TheorySetsPrivate::check(): processing "
+ << fact << std::endl;
+
+ bool polarity = fact.getKind() != kind::NOT;
+ TNode atom = polarity ? fact : fact[0];
+
+ // Solve each
+ switch(atom.getKind()) {
+ case kind::EQUAL:
+ Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
+ << "be equal to " << atom[1] << std::endl;
+ assertEquality(fact, fact, /* learnt = */ false);
+ break;
+
+ case kind::IN:
+ Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
+ << "be in " << atom[1] << std::endl;
+ assertMemebership(fact, fact, /* learnt = */ false);
+ break;
+
+ default:
+ Unhandled(fact.getKind());
+ }
+ finishPropagation();
+
+ Debug("sets") << "[sets] in conflict = " << d_conflict << std::endl;
+
+ if(d_conflict && !d_equalityEngine.consistent()) return;
+ Assert(!d_conflict);
+ Assert(d_equalityEngine.consistent());
+ }
+
+ Debug("sets") << "[sets] is complete = " << isComplete() << std::endl;
+
+ if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
+ d_external.d_out->lemma(getLemma());
+ }
+
+ return;
+}/* TheorySetsPrivate::check() */
+
+
+void TheorySetsPrivate::assertEquality(TNode fact, TNode reason, bool learnt)
+{
+ Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
+ << ", " << reason
+ << ", " << learnt << std::endl;
+
+ bool polarity = fact.getKind() != kind::NOT;
+ TNode atom = polarity ? fact : fact[0];
+
+ // fact already holds
+ if( holds(atom, polarity) ) {
+ Debug("sets-assert") << "[sets-assert] already present, skipping" << std::endl;
+ return;
+ }
+
+ // assert fact & check for conflict
+ if(learnt) {
+ registerReason(reason, /*save=*/ true);
+ }
+ d_equalityEngine.assertEquality(atom, polarity, reason);
+
+ if(!d_equalityEngine.consistent()) {
+ Debug("sets-assert") << "[sets-assert] running into a conflict" << std::endl;
+ d_conflict = true;
+ return;
+ }
+
+ if(!polarity && atom[0].getType().isSet()) {
+ addToPending(atom);
+ }
+
+}/* TheorySetsPrivate::assertEquality() */
+
+
+void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
+{
+ Debug("sets-assert") << "\n[sets-assert] adding membership: " << fact
+ << ", " << reason
+ << ", " << learnt << std::endl;
+
+ bool polarity = fact.getKind() == kind::NOT ? false : true;
+ TNode atom = polarity ? fact : fact[0];
+
+ // fact already holds
+ if( holds(atom, polarity) ) {
+ Debug("sets-assert") << "[sets-assert] already present, skipping" << std::endl;
+ return;
+ }
+
+ // assert fact & check for conflict
+ if(learnt) {
+ registerReason(reason, true);
+ }
+ d_equalityEngine.assertPredicate(atom, polarity, reason);
+
+ if(!d_equalityEngine.consistent()) {
+ Debug("sets-assert") << "[sets-assert] running into a conflict" << std::endl;
+ d_conflict = true;
+ return;
+ }
+
+ // update term info data structures
+ d_termInfoManager->notifyMembership(fact);
+
+ // propagation
+ TNode x = d_equalityEngine.getRepresentative(atom[0]);
+ eq::EqClassIterator j(d_equalityEngine.getRepresentative(atom[1]),
+ &d_equalityEngine);
+ TNode S = (*j);
+ Node cur_atom = IN(x, S);
+
+ /**
+ * It is sufficient to do emptyset propagation outside the loop as
+ * constant term is guaranteed to be class representative.
+ */
+ if(polarity && S.getKind() == kind::EMPTYSET) {
+ Debug("sets-prop") << "[sets-prop] something in empty set? conflict."
+ << std::endl;
+ learnLiteral(cur_atom, false, cur_atom);
+ Assert(d_conflict);
+ return;
+ }
+
+ for(; !j.isFinished(); ++j) {
+ TNode S = (*j);
+ Node cur_atom = IN(x, S);
+
+ // propagation : children
+ Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
+ << x << element_of_str << S << std::endl;
+ if(S.getKind() == kind::UNION ||
+ S.getKind() == kind::INTERSECTION ||
+ S.getKind() == kind::SETMINUS ||
+ S.getKind() == kind::SET_SINGLETON) {
+ doSettermPropagation(x, S);
+ if(d_conflict) return;
+ }// propagation: children
+
+
+ // propagation : parents
+ Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
+ << x << element_of_str << S << std::endl;
+ const CDTNodeList* parentList = d_termInfoManager->getParents(S);
+ for(typeof(parentList->begin()) k = parentList->begin();
+ k != parentList->end(); ++k) {
+ doSettermPropagation(x, *k);
+ if(d_conflict) return;
+ }// propagation : parents
+
+
+ }//j loop
+
+}/* TheorySetsPrivate::assertMemebership() */
+
+
+void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
+{
+ Debug("sets-prop") << "[sets-prop] doSettermPropagation("
+ << x << ", " << S << std::endl;
+
+ Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType());
+
+ Node literal, left_literal, right_literal;
+
+ // axiom: literal <=> left_literal AND right_literal
+ switch(S.getKind()) {
+ case kind::INTERSECTION:
+ literal = IN(x, S) ;
+ left_literal = IN(x, S[0]) ;
+ right_literal = IN(x, S[1]) ;
+ break;
+ case kind::UNION:
+ literal = NOT( IN(x, S) );
+ left_literal = NOT( IN(x, S[0]) );
+ right_literal = NOT( IN(x, S[1]) );
+ break;
+ case kind::SETMINUS:
+ literal = IN(x, S) ;
+ left_literal = IN(x, S[0]) ;
+ right_literal = NOT( IN(x, S[1]) );
+ break;
+ case kind::SET_SINGLETON: {
+ Node atom = IN(x, S);
+ if(holds(atom, true)) {
+ learnLiteral(EQUAL(x, S[0]), true, atom);
+ } else if(holds(atom, false)) {
+ learnLiteral(EQUAL(x, S[0]), false, NOT(atom));
+ }
+ return;
+ }
+ default:
+ Unhandled();
+ }
+
+ Debug("sets-prop-details")
+ << "[sets-prop-details] " << literal << " IFF " << left_literal
+ << " AND " << right_literal << std::endl;
+
+ Debug("sets-prop-details")
+ << "[sets-prop-details] "
+ << (holds(literal) ? "yes" : (holds(literal.negate()) ? " no" : " _ "))
+ << " IFF "
+ << (holds(left_literal) ? "yes" : (holds(left_literal.negate()) ? "no " : " _ "))
+ << " AND "
+ << (holds(right_literal) ? "yes" : (holds(right_literal.negate()) ? "no " : " _ "))
+ << std::endl;
+
+ Assert( present( IN(x, S) ) ||
+ present( IN(x, S[0]) ) ||
+ present( IN(x, S[1]) ) );
+
+ if( holds(literal) ) {
+ // 1a. literal => left_literal
+ Debug("sets-prop") << "[sets-prop] ... via case 1a. ..." << std::endl;
+ learnLiteral(left_literal, literal);
+ if(d_conflict) return;
+
+ // 1b. literal => right_literal
+ Debug("sets-prop") << "[sets-prop] ... via case 1b. ..." << std::endl;
+ learnLiteral(right_literal, literal);
+ if(d_conflict) return;
+
+ // subsumption requirement met, exit
+ return;
+ }
+ else if( holds(literal.negate() ) ) {
+ // 4. neg(literal), left_literal => neg(right_literal)
+ if( holds(left_literal) ) {
+ Debug("sets-prop") << "[sets-prop] ... via case 4. ..." << std::endl;
+ learnLiteral(right_literal.negate(), AND( literal.negate(),
+ left_literal) );
+ if(d_conflict) return;
+ }
+
+ // 5. neg(literal), right_literal => neg(left_literal)
+ if( holds(right_literal) ) {
+ Debug("sets-prop") << "[sets-prop] ... via case 5. ..." << std::endl;
+ learnLiteral(left_literal.negate(), AND( literal.negate(),
+ right_literal) );
+ if(d_conflict) return;
+ }
+ }
+ else {
+ // 2,3. neg(left_literal) v neg(right_literal) => neg(literal)
+ if(holds(left_literal.negate())) {
+ Debug("sets-prop") << "[sets-prop] ... via case 2. ..." << std::endl;
+ learnLiteral(literal.negate(), left_literal.negate());
+ if(d_conflict) return;
+ }
+ else if(holds(right_literal.negate())) {
+ Debug("sets-prop") << "[sets-prop] ... via case 3. ..." << std::endl;
+ learnLiteral(literal.negate(), right_literal.negate());
+ if(d_conflict) return;
+ }
+
+ // 6. the axiom itself:
+ else if(holds(left_literal) && holds(right_literal)) {
+ Debug("sets-prop") << "[sets-prop] ... via case 6. ..." << std::endl;
+ learnLiteral(literal, AND(left_literal, right_literal) );
+ if(d_conflict) return;
+ }
+ }
+
+ // check fulfilling rule
+ Node n;
+ switch(S.getKind()) {
+ case kind::UNION:
+ if( holds(IN(x, S)) &&
+ !present( IN(x, S[0]) ) )
+ addToPending( IN(x, S[0]) );
+ break;
+ case kind::SETMINUS: // intentional fallthrough
+ case kind::INTERSECTION:
+ if( holds(IN(x, S[0])) &&
+ !present( IN(x, S[1]) ))
+ addToPending( IN(x, S[1]) );
+ break;
+ default:
+ Assert(false, "MembershipEngine::doSettermPropagation");
+ }
+}
+
+
+void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
+ Debug("sets-learn") << "[sets-learn] learnLiteral(" << atom
+ << ", " << polarity << ")" << std::endl;
+
+ if( holds(atom, polarity) ) {
+ Debug("sets-learn") << "[sets-learn] \u2514 already known, skipping" << std::endl;
+ return;
+ }
+
+ if( holds(atom, !polarity) ) {
+ Debug("sets-learn") << "[sets-learn] \u2514 conflict found" << std::endl;
+
+ registerReason(reason, /*save=*/ true);
+
+ if(atom.getKind() == kind::EQUAL) {
+ d_equalityEngine.assertEquality(atom, polarity, reason);
+ } else {
+ d_equalityEngine.assertPredicate(atom, polarity, reason);
+ }
+ Assert(d_conflict); // should be marked due to equality engine
+ return;
+ }
+
+ Assert(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IN);
+
+ Node learnt_literal = polarity ? Node(atom) : NOT(atom);
+ d_propagationQueue.push_back( make_pair(learnt_literal, reason) );
+}
+
+/********************** Helper functions ***************************/
+/********************** Helper functions ***************************/
+/********************** Helper functions ***************************/
+
+Node mkAnd(const std::vector<TNode>& conjunctions) {
+ Assert(conjunctions.size() > 0);
+
+ std::set<TNode> all;
+
+ for (unsigned i = 0; i < conjunctions.size(); ++i) {
+ TNode t = conjunctions[i];
+
+ if (t.getKind() == kind::AND) {
+ for(TNode::iterator child_it = t.begin();
+ child_it != t.end(); ++child_it) {
+ Assert((*child_it).getKind() != kind::AND);
+ all.insert(*child_it);
+ }
+ }
+ else {
+ all.insert(t);
+ }
+
+ }
+
+ Assert(all.size() > 0);
+
+ if (all.size() == 1) {
+ // All the same, or just one
+ return conjunctions[0];
+ }
+
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::const_iterator it_end = all.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+
+ return conjunction;
+}/* mkAnd() */
+
+
+TheorySetsPrivate::Statistics::Statistics() :
+ d_checkTime("theory::sets::time") {
+ StatisticsRegistry::registerStat(&d_checkTime);
+}
+
+
+TheorySetsPrivate::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_checkTime);
+}
+
+
+bool TheorySetsPrivate::present(TNode atom) {
+ return holds(atom) || holds(atom.notNode());
+}
+
+
+bool TheorySetsPrivate::holds(TNode atom, bool polarity) {
+ Node polarity_atom = NodeManager::currentNM()->mkConst<bool>(polarity);
+
+ Node atomModEq = NodeManager::currentNM()->mkNode
+ (atom.getKind(), d_equalityEngine.getRepresentative(atom[0]),
+ d_equalityEngine.getRepresentative(atom[1]) );
+
+ d_equalityEngine.addTerm(atomModEq);
+
+ return d_equalityEngine.areEqual(atomModEq, polarity_atom);
+}
+
+
+void TheorySetsPrivate::registerReason(TNode reason, bool save)
+{
+ if(save) d_nodeSaver.insert(reason);
+
+ if(reason.getKind() == kind::AND) {
+ Assert(reason.getNumChildren() == 2);
+ registerReason(reason[0], false);
+ registerReason(reason[1], false);
+ } else if(reason.getKind() == kind::NOT) {
+ registerReason(reason[0], false);
+ } else if(reason.getKind() == kind::IN) {
+ d_equalityEngine.addTerm(reason);
+ Assert(present(reason));
+ } else if(reason.getKind() == kind::EQUAL) {
+ d_equalityEngine.addTerm(reason);
+ Assert(present(reason));
+ } else if(reason.getKind() == kind::CONST_BOOLEAN) {
+ // That's OK, already in EqEngine
+ } else {
+ Unhandled();
+ }
+}
+
+void TheorySetsPrivate::finishPropagation()
+{
+ while(!d_conflict && !d_settermPropagationQueue.empty()) {
+ std::pair<TNode,TNode> np = d_settermPropagationQueue.front();
+ d_settermPropagationQueue.pop();
+ doSettermPropagation(np.first, np.second);
+ }
+ while(!d_conflict && !d_propagationQueue.empty()) {
+ std::pair<Node,Node> np = d_propagationQueue.front();
+ d_propagationQueue.pop();
+ TNode atom = np.first.getKind() == kind::NOT ? np.first[0] : np.first;
+ if(atom.getKind() == kind::IN) {
+ assertMemebership(np.first, np.second, /* learnt = */ true);
+ } else {
+ assertEquality(np.first, np.second, /* learnt = */ true);
+ }
+ }
+}
+
+void TheorySetsPrivate::addToPending(Node n) {
+ if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) {
+ if(n.getKind() == kind::IN) {
+ d_pending.push(n);
+ } else {
+ Assert(n.getKind() == kind::EQUAL);
+ d_pendingDisequal.push(n);
+ }
+ d_pendingEverInserted.insert(n);
+ }
+}
+
+bool TheorySetsPrivate::isComplete() {
+ while(!d_pending.empty() && present(d_pending.front()))
+ d_pending.pop();
+ return d_pending.empty() && d_pendingDisequal.empty();
+}
+
+Node TheorySetsPrivate::getLemma() {
+ Assert(!d_pending.empty() || !d_pendingDisequal.empty());
+
+ Node lemma;
+
+ if(!d_pending.empty()) {
+ Node n = d_pending.front();
+ d_pending.pop();
+
+ Assert(!present(n));
+ Assert(n.getKind() == kind::IN);
+
+ lemma = OR(n, NOT(n));
+ } else {
+ Node n = d_pendingDisequal.front();
+ d_pendingDisequal.pop();
+
+ Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
+ Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType());
+ Node l1 = IN(x, n[0]), l2 = IN(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));
+ }
+
+ Debug("sets-lemma") << "[sets-lemma] " << lemma << std::endl;
+
+ return lemma;
+}
+
+
+TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
+ context::Context* c,
+ context::UserContext* u):
+ d_external(external),
+ d_notify(*this),
+ d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
+ d_conflict(c),
+ d_termInfoManager(NULL),
+ d_propagationQueue(c),
+ d_settermPropagationQueue(c),
+ d_nodeSaver(c),
+ d_pending(u),
+ d_pendingDisequal(u),
+ d_pendingEverInserted(u)
+{
+ d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
+
+ d_equalityEngine.addFunctionKind(kind::UNION);
+ d_equalityEngine.addFunctionKind(kind::INTERSECTION);
+ d_equalityEngine.addFunctionKind(kind::SETMINUS);
+
+ d_equalityEngine.addFunctionKind(kind::IN);
+ 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;
+
+ // If already in conflict, no more propagation
+ if (d_conflict) {
+ Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
+ return false;
+ }
+
+ // Propagate out
+ bool ok = d_external.d_out->propagate(literal);
+ if (!ok) {
+ d_conflict = true;
+ }
+
+ return ok;
+}/* TheorySetsPropagate::propagate(TNode) */
+
+
+void TheorySetsPrivate::conflict(TNode a, TNode b)
+{
+ if (a.getKind() == kind::CONST_BOOLEAN) {
+ d_conflictNode = explain(a.iffNode(b));
+ } else {
+ d_conflictNode = explain(a.eqNode(b));
+ }
+ d_external.d_out->conflict(d_conflictNode);
+ Debug("sets") << "[sets] conflict: " << a << " iff " << b
+ << ", explaination " << d_conflictNode << std::endl;
+ d_conflict = true;
+}
+
+Node TheorySetsPrivate::explain(TNode literal)
+{
+ Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
+ << std::endl;
+
+ bool polarity = literal.getKind() != kind::NOT;
+ TNode atom = polarity ? literal : literal[0];
+ std::vector<TNode> assumptions;
+
+ if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+ } else if(atom.getKind() == kind::IN) {
+ if( !d_equalityEngine.hasTerm(atom)) {
+ d_equalityEngine.addTerm(atom);
+ }
+ d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+ } else {
+ Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
+ << polarity << "); kind" << atom.getKind() << std::endl;
+ Unhandled();
+ }
+
+ return mkAnd(assumptions);
+}
+
+void TheorySetsPrivate::preRegisterTerm(TNode node)
+{
+ Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
+ << std::endl;
+
+ switch(node.getKind()) {
+ case kind::EQUAL:
+ // TODO: what's the point of this
+ d_equalityEngine.addTriggerEquality(node);
+ break;
+ case kind::IN:
+ // TODO: what's the point of this
+ d_equalityEngine.addTriggerPredicate(node);
+ break;
+ default:
+ d_termInfoManager->addTerm(node);
+ d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
+ // d_equalityEngine.addTerm(node);
+ }
+ if(node.getKind() == kind::SET_SINGLETON) {
+ Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
+ learnLiteral(IN(node[0], node), true, true_node);
+ //intentional fallthrough
+ }
+}
+
+
+
+/**************************** eq::NotifyClass *****************************/
+/**************************** eq::NotifyClass *****************************/
+/**************************** eq::NotifyClass *****************************/
+
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality << " value = " << value << std::endl;
+ if (value) {
+ return d_theory.propagate(equality);
+ } else {
+ // We use only literal triggers so taking not is safe
+ return d_theory.propagate(equality.notNode());
+ }
+}
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate << " value = " << value << std::endl;
+ if (value) {
+ return d_theory.propagate(predicate);
+ } else {
+ return d_theory.propagate(predicate.notNode());
+ }
+}
+
+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;
+ if(value) {
+ d_theory.d_termInfoManager->mergeTerms(t1, t2);
+ }
+ return true;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+ 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;
+}
+
+
+/**************************** TermInfoManager *****************************/
+/**************************** TermInfoManager *****************************/
+/**************************** TermInfoManager *****************************/
+
+void TheorySetsPrivate::TermInfoManager::mergeLists
+(CDTNodeList* la, const CDTNodeList* lb) const {
+ // straight from theory/arrays/array_info.cpp
+ std::set<TNode> temp;
+ CDTNodeList::const_iterator it;
+ for(it = la->begin() ; it != la->end(); it++ ) {
+ temp.insert((*it));
+ }
+
+ for(it = lb->begin() ; it!= lb->end(); it++ ) {
+ if(temp.count(*it) == 0) {
+ la->push_back(*it);
+ }
+ }
+}
+
+TheorySetsPrivate::TermInfoManager::TermInfoManager
+(TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
+ d_theory(theory),
+ d_context(satContext),
+ d_eqEngine(eq),
+ d_terms(satContext),
+ d_info()
+{ }
+
+TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
+ for( typeof(d_info.begin()) it = d_info.begin();
+ it != d_info.end(); ++it) {
+ delete (*it).second;
+ }
+}
+
+void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
+ bool polarity = fact.getKind() != kind::NOT;
+ TNode atom = polarity ? fact : fact[0];
+
+ TNode x = d_eqEngine->getRepresentative(atom[0]);
+ TNode S = d_eqEngine->getRepresentative(atom[1]);
+
+ Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
+ << " in " << S << " " << polarity << std::endl;
+
+ d_info[S]->addToElementList(x, polarity);
+}
+
+const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
+ return d_info[x]->parents;
+}
+
+void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
+ unsigned numChild = n.getNumChildren();
+
+ if(!d_terms.contains(n)) {
+ d_terms.insert(n);
+ d_info[n] = new TheorySetsTermInfo(d_context);
+ }
+
+ if(n.getKind() == kind::UNION ||
+ n.getKind() == kind::INTERSECTION ||
+ n.getKind() == kind::SETMINUS ||
+ n.getKind() == kind::SET_SINGLETON) {
+
+ for(unsigned i = 0; i < numChild; ++i) {
+ if(d_terms.contains(n[i])) {
+ Debug("sets-parent") << "Adding " << n << " to parent list of "
+ << n[i] << std::endl;
+ d_info[n[i]]->parents->push_back(n);
+ }
+ }
+
+ }
+}
+
+void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
+(CDTNodeList* l, TNode S, bool polarity)
+{
+ for(typeof(l->begin()) i = l->begin(); i != l->end(); ++i) {
+ Debug("sets-prop") << "[sets-terminfo] setterm todo: "
+ << IN(*i, d_eqEngine->getRepresentative(S))
+ << std::endl;
+
+ d_eqEngine->addTerm(IN(d_eqEngine->getRepresentative(*i),
+ d_eqEngine->getRepresentative(S)));
+
+ for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
+ !j.isFinished(); ++j) {
+
+ TNode x = (*i);
+ TNode S = (*j);
+ Node cur_atom = IN(x, S);
+
+ // propagation : empty set
+ if(polarity && S.getKind() == kind::EMPTYSET) {
+ Debug("sets-prop") << "[sets-prop] something in empty set? conflict."
+ << std::endl;
+ d_theory.learnLiteral(cur_atom, false, cur_atom);
+ return;
+ }// propagation: empty set
+
+ // propagation : children
+ if(S.getKind() == kind::UNION ||
+ S.getKind() == kind::INTERSECTION ||
+ S.getKind() == kind::SETMINUS ||
+ S.getKind() == kind::SET_SINGLETON) {
+ d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
+ }// propagation: children
+
+ // propagation : parents
+ const CDTNodeList* parentList = getParents(S);
+ for(typeof(parentList->begin()) k = parentList->begin();
+ k != parentList->end(); ++k) {
+ d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
+ }// propagation : parents
+
+
+ }//j loop
+
+ }
+
+}
+
+void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
+ // merge b into a
+
+ if(!a.getType().isSet()) return;
+
+ Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
+ << ", b = " << b << std::endl;
+ Debug("sets-terminfo") << "[sets-terminfo] reps"
+ << ", a: " << d_eqEngine->getRepresentative(a)
+ << ", b: " << d_eqEngine->getRepresentative(b)
+ << std::endl;
+
+ typeof(d_info.begin()) ita = d_info.find(a);
+ typeof(d_info.begin()) itb = d_info.find(b);
+
+ Assert(ita != d_info.end());
+ Assert(itb != d_info.end());
+
+ pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
+ pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
+ pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
+ pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
+
+ mergeLists((*ita).second->elementsInThisSet,
+ (*itb).second->elementsInThisSet);
+
+ mergeLists((*ita).second->elementsNotInThisSet,
+ (*itb).second->elementsNotInThisSet);
+}
+
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
new file mode 100644
index 000000000..f1a8c0a46
--- /dev/null
+++ b/src/theory/sets/theory_sets_private.h
@@ -0,0 +1,166 @@
+/********************* */
+/*! \file theory_sets_private.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory implementation.
+ **
+ ** Sets theory implementation.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+
+#include "context/cdhashset.h"
+#include "context/cdqueue.h"
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/sets/term_info.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+/** Internal classes, forward declared here */
+class TheorySetsTermInfoManager;
+class TheorySets;
+
+class TheorySetsPrivate {
+public:
+
+ /**
+ * Constructs a new instance of TheorySetsPrivate w.r.t. the provided
+ * contexts.
+ */
+ TheorySetsPrivate(TheorySets& external,
+ context::Context* c,
+ context::UserContext* u);
+
+ ~TheorySetsPrivate();
+
+ void check(Theory::Effort);
+
+ void propagate(Theory::Effort);
+
+ Node explain(TNode);
+
+ std::string identify() const { return "THEORY_SETS_PRIVATE"; }
+
+ void preRegisterTerm(TNode node);
+
+private:
+ TheorySets& d_external;
+
+ class Statistics {
+ public:
+ TimerStat d_checkTime;
+
+ Statistics();
+ ~Statistics();
+ } d_statistics;
+
+ /** Functions to handle callbacks from equality engine */
+ class NotifyClass : public eq::EqualityEngineNotify {
+ TheorySetsPrivate& d_theory;
+
+ public:
+ NotifyClass(TheorySetsPrivate& theory): d_theory(theory) {}
+ bool eqNotifyTriggerEquality(TNode equality, bool value);
+ 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);
+ } d_notify;
+
+ /** Equality engine */
+ eq::EqualityEngine d_equalityEngine;
+
+ context::CDO<bool> d_conflict;
+ Node d_conflictNode;
+
+ /** Proagate out to output channel */
+ bool propagate(TNode);
+
+ /** generate and send out conflict node */
+ void conflict(TNode, TNode);
+
+ class TermInfoManager {
+ TheorySetsPrivate& d_theory;
+ context::Context* d_context;
+ eq::EqualityEngine* d_eqEngine;
+
+ CDNodeSet d_terms;
+ std::hash_map<TNode, TheorySetsTermInfo*, TNodeHashFunction> d_info;
+
+ void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const;
+ void pushToSettermPropagationQueue(CDTNodeList* l, TNode S, bool polarity);
+ public:
+ TermInfoManager(TheorySetsPrivate&,
+ context::Context* satContext,
+ eq::EqualityEngine*);
+ ~TermInfoManager();
+ void notifyMembership(TNode fact);
+ const CDTNodeList* getParents(TNode x);
+ void addTerm(TNode n);
+ void mergeTerms(TNode a, TNode b);
+ };
+ TermInfoManager* d_termInfoManager;
+
+ /** Assertions and helper functions */
+ bool present(TNode atom);
+ bool holds(TNode lit) {
+ bool polarity = lit.getKind() == kind::NOT ? false : true;
+ TNode atom = polarity ? lit : lit[0];
+ return holds(atom, polarity);
+ }
+ bool holds(TNode atom, bool polarity);
+
+ void assertEquality(TNode fact, TNode reason, bool learnt);
+ void assertMemebership(TNode fact, TNode reason, bool learnt);
+
+ /** Propagation / learning and helper functions. */
+ context::CDQueue< std::pair<Node, Node> > d_propagationQueue;
+ context::CDQueue< std::pair<TNode, TNode> > d_settermPropagationQueue;
+
+ void doSettermPropagation(TNode x, TNode S);
+ void registerReason(TNode reason, bool save);
+ void learnLiteral(TNode atom, bool polarity, Node reason);
+ void learnLiteral(TNode lit, Node reason) {
+ if(lit.getKind() == kind::NOT) {
+ learnLiteral(lit[0], false, reason);
+ } else {
+ learnLiteral(lit, true, reason);
+ }
+ }
+ void finishPropagation();
+
+ // for any nodes we need to save, because others use TNode
+ context::CDHashSet <Node, NodeHashFunction> d_nodeSaver;
+
+ /** Lemmas and helper functions */
+ context::CDQueue <TNode> d_pending;
+ context::CDQueue <TNode> d_pendingDisequal;
+ context::CDHashSet <Node, NodeHashFunction> d_pendingEverInserted;
+
+ void addToPending(Node n);
+ bool isComplete();
+ Node getLemma();
+};/* class TheorySetsPrivate */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
new file mode 100644
index 000000000..11a2e9297
--- /dev/null
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -0,0 +1,110 @@
+#include "theory/sets/theory_sets_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+bool checkConstantMembership(TNode elementTerm, TNode setTerm)
+{
+ 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();
+
+ switch(node.getKind()) {
+
+ case kind::IN: {
+ if(!node[0].isConst() || !node[1].isConst())
+ break;
+
+ // both are constants
+ bool isMember = checkConstantMembership(node[0], node[1]);
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
+ }
+
+ 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,
+ nm->mkNode(kind::EQUAL,
+ nm->mkNode(kind::UNION, A, B),
+ B) );
+ }//kind::SUBSET
+
+ case kind::EQUAL:
+ case kind::IFF: {
+ //rewrite: t = t with true (t term)
+ //rewrite: c = c' with c different from c' false (c, c' constants)
+ //otherwise: sort them
+ if(node[0] == node[1]) {
+ Trace("sets-postrewrite") << "Sets::postRewrite returning true" << std::endl;
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
+ }
+ else if (node[0].isConst() && node[1].isConst()) {
+ Trace("sets-postrewrite") << "Sets::postRewrite returning false" << std::endl;
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(false));
+ }
+ 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;
+ }
+
+ 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] > 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;
+ }
+
+ default:
+ break;
+
+ }//switch(node.getKind())
+
+ // This default implementation
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
+// static
+RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
+ NodeManager* nm = NodeManager::currentNM();
+
+ // do nothing
+ if(node.getKind() == kind::EQUAL && node[0] == node[1])
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
+ // Further optimization, if constants but differing ones
+
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
new file mode 100644
index 000000000..f01d198cf
--- /dev/null
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -0,0 +1,77 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsRewriter {
+public:
+
+ /**
+ * Rewrite a node into the normal form for the theory of sets.
+ * Called in post-order (really reverse-topological order) when
+ * traversing the expression DAG during rewriting. This is the
+ * main function of the rewriter, and because of the ordering,
+ * it can assume its children are all rewritten already.
+ *
+ * This function can return one of three rewrite response codes
+ * along with the rewritten node:
+ *
+ * REWRITE_DONE indicates that no more rewriting is needed.
+ * REWRITE_AGAIN means that the top-level expression should be
+ * rewritten again, but that its children are in final form.
+ * REWRITE_AGAIN_FULL means that the entire returned expression
+ * should be rewritten again (top-down with preRewrite(), then
+ * bottom-up with postRewrite()).
+ *
+ * Even if this function returns REWRITE_DONE, if the returned
+ * expression belongs to a different theory, it will be fully
+ * rewritten by that theory's rewriter.
+ */
+ static RewriteResponse postRewrite(TNode node);
+
+ /**
+ * Rewrite a node into the normal form for the theory of sets
+ * in pre-order (really topological order)---meaning that the
+ * children may not be in the normal form. This is an optimization
+ * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
+ * in arithmetic rewrites to 0 without the need to look at the big
+ * nasty expression). Since it's only an optimization, the
+ * implementation here can do nothing.
+ */
+ static RewriteResponse preRewrite(TNode node);
+
+ /**
+ * Rewrite an equality, in case special handling is required.
+ */
+ static Node rewriteEquality(TNode equality) {
+ // often this will suffice
+ return postRewrite(equality).node;
+ }
+
+ /**
+ * Initialize the rewriter.
+ */
+ static inline void init() {
+ // nothing to do
+ }
+
+ /**
+ * Shut down the rewriter.
+ */
+ static inline void shutdown() {
+ // nothing to do
+ }
+
+};/* class TheorySetsRewriter */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
new file mode 100644
index 000000000..2f4cc6a2f
--- /dev/null
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -0,0 +1,161 @@
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> {
+ unsigned d_index;
+ TypeNode d_constituentType;
+ NodeManager* d_nm;
+ std::vector<bool> d_indexVec;
+ std::vector<TypeEnumerator*> d_constituentVec;
+ bool d_finished;
+ Node d_setConst;
+
+public:
+
+ SetEnumerator(TypeNode type) throw(AssertionException) :
+ TypeEnumeratorBase<SetEnumerator>(type),
+ d_index(0),
+ d_constituentType(type.getSetElementType()),
+ d_nm(NodeManager::currentNM()),
+ d_indexVec(),
+ d_constituentVec(),
+ d_finished(false),
+ d_setConst()
+ {
+ // d_indexVec.push_back(false);
+ // d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ d_setConst = d_nm->mkConst(EmptySet(type.toType()));
+ }
+
+ // An set enumerator could be large, and generally you don't want to
+ // go around copying these things; but a copy ctor is presently required
+ // by the TypeEnumerator framework.
+ SetEnumerator(const SetEnumerator& ae) throw() :
+ TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)),
+ d_constituentType(ae.d_constituentType),
+ d_nm(ae.d_nm),
+ d_indexVec(ae.d_indexVec),
+ d_constituentVec(),// copied below
+ d_finished(ae.d_finished),
+ d_setConst(ae.d_setConst)
+ {
+ for(std::vector<TypeEnumerator*>::const_iterator i =
+ ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
+ i != i_end;
+ ++i) {
+ d_constituentVec.push_back(new TypeEnumerator(**i));
+ }
+ }
+
+ ~SetEnumerator() {
+ while (!d_constituentVec.empty()) {
+ delete d_constituentVec.back();
+ d_constituentVec.pop_back();
+ }
+ }
+
+ Node operator*() throw(NoMoreValuesException) {
+ if (d_finished) {
+ throw NoMoreValuesException(getType());
+ }
+ Node n = d_setConst;
+
+ // For now only support only sets of size 1
+ Assert(d_index == 0 || d_index == 1);
+
+ if(d_index == 1) {
+ n = d_nm->mkNode(kind::SET_SINGLETON, *(*(d_constituentVec[0])));
+ }
+
+ // for (unsigned i = 0; i < d_indexVec.size(); ++i) {
+ // n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i])));
+ // }
+ Trace("set-type-enum") << "operator * prerewrite: " << n << std::endl;
+ n = Rewriter::rewrite(n);
+ Trace("set-type-enum") << "operator * returning: " << n << std::endl;
+ return n;
+ }
+
+ SetEnumerator& operator++() throw() {
+ Trace("set-type-enum") << "operator++ called, **this = " << **this << std::endl;
+
+ if (d_finished) {
+ Trace("set-type-enum") << "operator++ finished!" << std::endl;
+ return *this;
+ }
+
+ // increment by one, at the same time deleting all elements that
+ // cannot be incremented any further (note: we are keeping a set
+ // -- no repetitions -- thus some trickery to know what to pop and
+ // what not to.)
+ if(d_index > 0) {
+ Assert(d_index == d_constituentVec.size());
+
+ Node last_pre_increment;
+ last_pre_increment = *(*d_constituentVec.back());
+
+ ++(*d_constituentVec.back());
+
+ if (d_constituentVec.back()->isFinished()) {
+ delete d_constituentVec.back();
+ d_constituentVec.pop_back();
+
+ while(!d_constituentVec.empty()) {
+ Node cur_pre_increment = *(*d_constituentVec.back());
+ ++(*d_constituentVec.back());
+ Node cur_post_increment = *(*d_constituentVec.back());
+ if(last_pre_increment == cur_post_increment) {
+ delete d_constituentVec.back();
+ d_constituentVec.pop_back();
+ last_pre_increment = cur_pre_increment;
+ } else {
+ break;
+ }
+ }
+ }
+ }
+
+ if (d_constituentVec.empty()) {
+ ++d_index;
+ d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ }
+
+ while (d_constituentVec.size() < d_index) {
+ TypeEnumerator *d_newEnumerator = new TypeEnumerator(*d_constituentVec.back());
+ ++(*d_newEnumerator);
+ if( (*d_newEnumerator).isFinished() ) {
+ Trace("set-type-enum") << "operator++ finished!" << std::endl;
+ d_finished = true;
+ return *this;
+ }
+ d_constituentVec.push_back(d_newEnumerator);
+ }
+
+ Trace("set-type-enum") << "operator++ returning, **this = " << **this << std::endl;
+ return *this;
+ }
+
+ bool isFinished() throw() {
+ Trace("set-type-enum") << "isFinished returning: " << d_finished << std::endl;
+ return d_finished;
+ }
+
+};/* class SetEnumerator */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
new file mode 100644
index 000000000..026c90ca4
--- /dev/null
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -0,0 +1,176 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class SetsTypeRule {
+public:
+
+ /**
+ * Compute the type for (and optionally typecheck) a term belonging
+ * to the theory of sets.
+ *
+ * @param check if true, the node's type should be checked as well
+ * as computed.
+ */
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+ bool check)
+ throw (TypeCheckingExceptionPrivate) {
+
+ // TODO: implement me!
+ Unimplemented();
+
+ }
+
+};/* class SetsTypeRule */
+
+// TODO: Union, Intersection and Setminus should be combined to one check
+struct SetUnionTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::UNION);
+ TypeNode setType = n[0].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "set union operating on non-set");
+ }
+ TypeNode secondSetType = n[1].getType(check);
+ if(secondSetType != setType) {
+ throw TypeCheckingExceptionPrivate(n, "set union operating on sets of different types");
+ }
+ }
+ return setType;
+ }
+};/* struct SetUnionTypeRule */
+
+struct SetIntersectionTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::INTERSECTION);
+ TypeNode setType = n[0].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "set intersection operating on non-set");
+ }
+ TypeNode secondSetType = n[1].getType(check);
+ if(secondSetType != setType) {
+ throw TypeCheckingExceptionPrivate(n, "set intersection operating on sets of different types");
+ }
+ }
+ return setType;
+ }
+};/* struct SetIntersectionTypeRule */
+
+struct SetSetminusTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::SETMINUS);
+ TypeNode setType = n[0].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "set setminus operating on non-set");
+ }
+ TypeNode secondSetType = n[1].getType(check);
+ if(secondSetType != setType) {
+ throw TypeCheckingExceptionPrivate(n, "set setminus operating on sets of different types");
+ }
+ }
+ return setType;
+ }
+};/* struct SetSetminusTypeRule */
+
+struct SetSubsetTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::SUBSET);
+ TypeNode setType = n[0].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set");
+ }
+ TypeNode secondSetType = n[1].getType(check);
+ if(secondSetType != setType) {
+ throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};/* struct SetSubsetTypeRule */
+
+struct SetInTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::IN);
+ TypeNode setType = n[1].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set");
+ }
+ TypeNode elementType = n[0].getType(check);
+ if(elementType != setType.getSetElementType()) {
+ throw TypeCheckingExceptionPrivate(n, "set in operating on sets of different types");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};/* struct SetInTypeRule */
+
+struct SetSingletonTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::SET_SINGLETON);
+ return nodeManager->mkSetType(n[0].getType(check));
+ }
+};/* struct SetInTypeRule */
+
+struct SetConstTypeRule {
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ switch(n.getKind()) {
+ case kind::SET_SINGLETON:
+ return n[0].isConst();
+ case kind::UNION:
+ return n[0].isConst() && n[1].isConst();
+ default:
+ Unhandled();
+ }
+ }
+};
+
+struct EmptySetTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+
+ Assert(n.getKind() == kind::EMPTYSET);
+ EmptySet emptySet = n.getConst<EmptySet>();
+ Type setType = emptySet.getType();
+ return TypeNode::fromType(setType);
+ }
+};
+
+
+struct SetsProperties {
+ inline static Cardinality computeCardinality(TypeNode type) {
+ Assert(type.getKind() == kind::SET_TYPE);
+ Cardinality elementCard = type[0].getCardinality();
+ return elementCard;
+ }
+
+ inline static bool isWellFounded(TypeNode type) {
+ return type[0].isWellFounded();
+ }
+
+ inline static Node mkGroundTerm(TypeNode type) {
+ Assert(type.isSet());
+ return NodeManager::currentNM()->mkConst(EmptySet(type.toType()));
+ }
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback