diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-09-09 14:47:53 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-21 07:25:13 -0500 |
commit | 50c26544c83a71e87efa487e4af063b1b5647c0f (patch) | |
tree | 82d4f3b2632a2cf06aff70550f37f80dc80d9543 /src/theory | |
parent | 53b8499f48a00dc876d56c76fbc79aafe5803529 (diff) |
add new theory (sets)
Specification (smt2) -- as per this commit, subject to change
- Parameterized sort Set, e.g. (Set Int)
- Empty set constant (typed), use with "as" to specify the type, e.g.
(as emptyset (Set Int))
- Create a singleton set
(setenum X (Set X)) : creates singleton set
- Functions/operators
(union (Set X) (Set X) (Set X))
(intersection (Set X) (Set X) (Set X))
(setminus (Set X) (Set X) (Set X))
- Predicates
(in X (Set X) Bool) : membership
(subseteq (Set X) (Set X) Bool) : set containment
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/array_info.h | 2 | ||||
-rw-r--r-- | src/theory/logic_info.cpp | 8 | ||||
-rw-r--r-- | src/theory/sets/.gitignore | 1 | ||||
-rw-r--r-- | src/theory/sets/Makefile | 4 | ||||
-rw-r--r-- | src/theory/sets/Makefile.am | 20 | ||||
-rw-r--r-- | src/theory/sets/expr_patterns.h | 51 | ||||
-rw-r--r-- | src/theory/sets/kinds | 55 | ||||
-rw-r--r-- | src/theory/sets/options | 14 | ||||
-rw-r--r-- | src/theory/sets/options_handlers.h | 14 | ||||
-rw-r--r-- | src/theory/sets/term_info.h | 57 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 55 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 65 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 871 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 166 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 110 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.h | 77 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_enumerator.h | 161 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 176 | ||||
-rw-r--r-- | src/theory/theory.h | 3 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 6 |
21 files changed, 1916 insertions, 6 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 1f97c02ca..0a2a96603 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -75,8 +75,6 @@ public: } ~Info() { - //FIXME! - //indices->deleteSelf(); indices->deleteSelf(); stores->deleteSelf(); in_stores->deleteSelf(); diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 525b129cf..a30867ee1 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -122,6 +122,10 @@ std::string LogicInfo::getLogicString() const { } ++seen; } + if(d_theories[THEORY_SETS]) { + ss << "_SETS"; + ++seen; + } if(seen != d_sharingTheories) { Unhandled("can't extract a logic string from LogicInfo; at least one " @@ -256,6 +260,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc arithNonLinear(); p += 4; } + if(!strncmp(p, "_SETS", 5)) { + enableTheory(THEORY_SETS); + p += 5; + } } } if(*p != '\0') { 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 */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 2359d5d86..e8d53e539 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -620,6 +620,9 @@ public: * check() or propagate() method called. A Theory may empty its * assertFact() queue using get(). A Theory can raise conflicts, * add lemmas, and propagate literals during presolve(). + * + * NOTE: The presolve property must be added to the kinds file for + * the theory. */ virtual void presolve() { } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 47ba50aad..63024e5d5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -671,6 +671,7 @@ bool TheoryEngine::presolve() { void TheoryEngine::postsolve() { // Reset the interrupt flag d_interrupted = false; + bool CVC4_UNUSED wasInConflict = d_inConflict; try { // Definition of the statement that is to be run by every theory @@ -680,7 +681,7 @@ void TheoryEngine::postsolve() { #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasPostsolve) { \ theoryOf(THEORY)->postsolve(); \ - Assert(! d_inConflict, "conflict raised during postsolve()"); \ + Assert(! d_inConflict || wasInConflict, "conflict raised during postsolve()"); \ } // Postsolve for each theory using the statement above @@ -961,7 +962,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo bool value; if (d_propEngine->hasValue(assertion, value)) { if (!value) { - Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict" << endl; + Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl; d_inConflict = true; } else { return; @@ -1011,6 +1012,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // Check for propositional conflicts bool value; if (d_propEngine->hasValue(assertion, value) && !value) { + Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)" << endl; d_inConflict = true; } } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f8e361081..8bb849496 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -833,12 +833,14 @@ public: void addTriggerPredicate(TNode predicate); /** - * Returns true if the two are currently in the database and equal. + * Returns true if the two terms are equal. Requires both terms to + * be in the database. */ bool areEqual(TNode t1, TNode t2) const; /** - * Check whether the two term are dis-equal. + * Check whether the two term are dis-equal. Requires both terms to + * be in the database. */ bool areDisequal(TNode t1, TNode t2, bool ensureProof) const; |