theory/sep/theory_sep_rewriter.cpp
theory/sep/theory_sep_rewriter.h
theory/sep/theory_sep_type_rules.h
+ theory/sets/cardinality_extension.cpp
+ theory/sets/cardinality_extension.h
+ theory/sets/inference_manager.cpp
+ theory/sets/inference_manager.h
theory/sets/normal_form.h
theory/sets/rels_utils.h
theory/sets/skolem_cache.cpp
theory/sets/skolem_cache.h
+ theory/sets/solver_state.cpp
+ theory/sets/solver_state.h
theory/sets/theory_sets.cpp
theory/sets/theory_sets.h
theory/sets/theory_sets_private.cpp
--- /dev/null
+/********************* */
+/*! \file cardinality_extension.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of an extension of the theory sets for handling
+ ** cardinality constraints.
+ **/
+
+#include "theory/sets/cardinality_extension.h"
+
+#include "expr/emptyset.h"
+#include "expr/node_algorithm.h"
+#include "options/sets_options.h"
+#include "theory/sets/normal_form.h"
+#include "theory/valuation.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+CardinalityExtension::CardinalityExtension(SolverState& s,
+ InferenceManager& im,
+ eq::EqualityEngine& e,
+ context::Context* c,
+ context::UserContext* u)
+ : d_state(s), d_im(im), d_ee(e), d_card_processed(u)
+{
+ d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ // we do congruence over cardinality
+ d_ee.addFunctionKind(CARD);
+}
+
+void CardinalityExtension::reset()
+{
+ d_eqc_to_card_term.clear();
+ d_t_card_enabled.clear();
+}
+void CardinalityExtension::registerTerm(Node n)
+{
+ Trace("sets-card-debug") << "Register term : " << n << std::endl;
+ Assert(n.getKind() == CARD);
+ TypeNode tnc = n[0].getType().getSetElementType();
+ d_t_card_enabled[tnc] = true;
+ Node r = d_ee.getRepresentative(n[0]);
+ if (d_eqc_to_card_term.find(r) == d_eqc_to_card_term.end())
+ {
+ d_eqc_to_card_term[r] = n;
+ registerCardinalityTerm(n[0]);
+ }
+ if (tnc.isInterpretedFinite())
+ {
+ std::stringstream ss;
+ ss << "ERROR: cannot use cardinality on sets with finite element "
+ "type (term is "
+ << n << ")." << std::endl;
+ throw LogicException(ss.str());
+ // TODO (#1123): extend approach for this case
+ }
+ Trace("sets-card-debug") << "...finished register term" << std::endl;
+}
+
+void CardinalityExtension::check()
+{
+ checkRegister();
+ if (d_im.hasProcessed())
+ {
+ return;
+ }
+ checkMinCard();
+ if (d_im.hasProcessed())
+ {
+ return;
+ }
+ checkCardCycles();
+ if (d_im.hasProcessed())
+ {
+ return;
+ }
+ // The last step will either do nothing (in which case we are SAT), or request
+ // that a new set term is introduced.
+ std::vector<Node> intro_sets;
+ checkNormalForms(intro_sets);
+ if (intro_sets.empty())
+ {
+ return;
+ }
+ Assert(intro_sets.size() == 1);
+ Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl;
+ Trace("sets-intro") << " Actual Intro : ";
+ d_state.debugPrintSet(intro_sets[0], "sets-nf");
+ Trace("sets-nf") << std::endl;
+ Node k = d_state.getProxy(intro_sets[0]);
+ AlwaysAssert(!k.isNull());
+}
+
+void CardinalityExtension::checkRegister()
+{
+ Trace("sets") << "Cardinality graph..." << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
+ // first, ensure cardinality relationships are added as lemmas for all
+ // non-basic set terms
+ const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
+ for (const Node& eqc : setEqc)
+ {
+ const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
+ for (Node n : nvsets)
+ {
+ if (!d_state.isCongruent(n))
+ {
+ // if setminus, do for intersection instead
+ if (n.getKind() == SETMINUS)
+ {
+ n = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
+ }
+ registerCardinalityTerm(n);
+ }
+ }
+ }
+ Trace("sets") << "Done cardinality graph" << std::endl;
+}
+
+void CardinalityExtension::registerCardinalityTerm(Node n)
+{
+ TypeNode tnc = n.getType().getSetElementType();
+ if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end())
+ {
+ // if no cardinality constraints for sets of this type, we can ignore
+ return;
+ }
+ if (d_card_processed.find(n) != d_card_processed.end())
+ {
+ // already processed
+ return;
+ }
+ d_card_processed.insert(n);
+ NodeManager* nm = NodeManager::currentNM();
+ Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
+ std::vector<Node> cterms;
+ if (n.getKind() == INTERSECTION)
+ {
+ for (unsigned e = 0; e < 2; e++)
+ {
+ Node s = nm->mkNode(SETMINUS, n[e], n[1 - e]);
+ cterms.push_back(s);
+ }
+ Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, n), d_zero);
+ d_im.assertInference(pos_lem, d_emp_exp, "pcard", 1);
+ }
+ else
+ {
+ cterms.push_back(n);
+ }
+ for (unsigned k = 0, csize = cterms.size(); k < csize; k++)
+ {
+ Node nn = cterms[k];
+ Node nk = d_state.getProxy(nn);
+ Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, nk), d_zero);
+ d_im.assertInference(pos_lem, d_emp_exp, "pcard", 1);
+ if (nn != nk)
+ {
+ Node lem = nm->mkNode(EQUAL, nm->mkNode(CARD, nk), nm->mkNode(CARD, nn));
+ lem = Rewriter::rewrite(lem);
+ Trace("sets-card") << " " << k << " : " << lem << std::endl;
+ d_im.assertInference(lem, d_emp_exp, "card", 1);
+ }
+ }
+ d_im.flushPendingLemmas();
+}
+
+void CardinalityExtension::checkCardCycles()
+{
+ Trace("sets") << "Check cardinality cycles..." << std::endl;
+ // build order of equivalence classes, also build cardinality graph
+ const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
+ d_oSetEqc.clear();
+ d_card_parent.clear();
+ for (const Node& s : setEqc)
+ {
+ std::vector<Node> curr;
+ std::vector<Node> exp;
+ checkCardCyclesRec(s, curr, exp);
+ if (d_im.hasProcessed())
+ {
+ return;
+ }
+ }
+ Trace("sets") << "Done check cardinality cycles" << std::endl;
+}
+
+void CardinalityExtension::checkCardCyclesRec(Node eqc,
+ std::vector<Node>& curr,
+ std::vector<Node>& exp)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ if (std::find(curr.begin(), curr.end(), eqc) != curr.end())
+ {
+ Trace("sets-debug") << "Found venn region loop..." << std::endl;
+ if (curr.size() > 1)
+ {
+ // all regions must be equal
+ std::vector<Node> conc;
+ for (const Node& cc : curr)
+ {
+ conc.push_back(curr[0].eqNode(cc));
+ }
+ Node fact = conc.size() == 1 ? conc[0] : nm->mkNode(AND, conc);
+ d_im.assertInference(fact, exp, "card_cycle");
+ d_im.flushPendingLemmas();
+ }
+ else
+ {
+ // should be guaranteed based on not exploring equal parents
+ Assert(false);
+ }
+ return;
+ }
+ if (std::find(d_oSetEqc.begin(), d_oSetEqc.end(), eqc) != d_oSetEqc.end())
+ {
+ // already processed
+ return;
+ }
+ const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
+ if (nvsets.empty())
+ {
+ // no non-variable sets, trivial
+ d_oSetEqc.push_back(eqc);
+ return;
+ }
+ curr.push_back(eqc);
+ TypeNode tn = eqc.getType();
+ bool is_empty = eqc == d_state.getEmptySetEqClass(tn);
+ Node emp_set = d_state.getEmptySet(tn);
+ for (const Node& n : nvsets)
+ {
+ Kind nk = n.getKind();
+ if (nk != INTERSECTION && nk != SETMINUS)
+ {
+ continue;
+ }
+ Trace("sets-debug") << "Build cardinality parents for " << n << "..."
+ << std::endl;
+ std::vector<Node> sib;
+ unsigned true_sib = 0;
+ if (n.getKind() == INTERSECTION)
+ {
+ d_localBase[n] = n;
+ for (unsigned e = 0; e < 2; e++)
+ {
+ Node sm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[e], n[1 - e]));
+ sib.push_back(sm);
+ }
+ true_sib = 2;
+ }
+ else
+ {
+ Node si = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
+ sib.push_back(si);
+ d_localBase[n] = si;
+ Node osm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[1], n[0]));
+ sib.push_back(osm);
+ true_sib = 1;
+ }
+ Node u = Rewriter::rewrite(nm->mkNode(UNION, n[0], n[1]));
+ if (!d_ee.hasTerm(u))
+ {
+ u = Node::null();
+ }
+ unsigned n_parents = true_sib + (u.isNull() ? 0 : 1);
+ // if this set is empty
+ if (is_empty)
+ {
+ Assert(d_state.areEqual(n, emp_set));
+ Trace("sets-debug") << " empty, parents equal siblings" << std::endl;
+ std::vector<Node> conc;
+ // parent equal siblings
+ for (unsigned e = 0; e < true_sib; e++)
+ {
+ if (d_ee.hasTerm(sib[e]) && !d_state.areEqual(n[e], sib[e]))
+ {
+ conc.push_back(n[e].eqNode(sib[e]));
+ }
+ }
+ d_im.assertInference(conc, n.eqNode(emp_set), "cg_emp");
+ d_im.flushPendingLemmas();
+ if (d_im.hasProcessed())
+ {
+ return;
+ }
+ else
+ {
+ // justify why there is no edge to parents (necessary?)
+ for (unsigned e = 0; e < n_parents; e++)
+ {
+ Node p = (e == true_sib) ? u : n[e];
+ }
+ }
+ continue;
+ }
+ std::vector<Node> card_parents;
+ std::vector<int> card_parent_ids;
+ // check if equal to a parent
+ for (unsigned e = 0; e < n_parents; e++)
+ {
+ Trace("sets-debug") << " check parent " << e << "/" << n_parents
+ << std::endl;
+ bool is_union = e == true_sib;
+ Node p = (e == true_sib) ? u : n[e];
+ Trace("sets-debug") << " check relation to parent " << p
+ << ", isu=" << is_union << "..." << std::endl;
+ // if parent is empty
+ if (d_state.areEqual(p, emp_set))
+ {
+ Trace("sets-debug") << " it is empty..." << std::endl;
+ Assert(!d_state.areEqual(n, emp_set));
+ d_im.assertInference(n.eqNode(emp_set), p.eqNode(emp_set), "cg_emppar");
+ d_im.flushPendingLemmas();
+ if (d_im.hasProcessed())
+ {
+ return;
+ }
+ // if we are equal to a parent
+ }
+ else if (d_state.areEqual(p, n))
+ {
+ Trace("sets-debug") << " it is equal to this..." << std::endl;
+ std::vector<Node> conc;
+ std::vector<int> sib_emp_indices;
+ if (is_union)
+ {
+ for (unsigned s = 0; s < sib.size(); s++)
+ {
+ sib_emp_indices.push_back(s);
+ }
+ }
+ else
+ {
+ sib_emp_indices.push_back(e);
+ }
+ // sibling(s) are empty
+ for (unsigned si : sib_emp_indices)
+ {
+ if (!d_state.areEqual(sib[si], emp_set))
+ {
+ conc.push_back(sib[si].eqNode(emp_set));
+ }
+ else
+ {
+ Trace("sets-debug")
+ << "Sibling " << sib[si] << " is already empty." << std::endl;
+ }
+ }
+ if (!is_union && nk == INTERSECTION && !u.isNull())
+ {
+ // union is equal to other parent
+ if (!d_state.areEqual(u, n[1 - e]))
+ {
+ conc.push_back(u.eqNode(n[1 - e]));
+ }
+ }
+ Trace("sets-debug")
+ << "...derived " << conc.size() << " conclusions" << std::endl;
+ d_im.assertInference(conc, n.eqNode(p), "cg_eqpar");
+ d_im.flushPendingLemmas();
+ if (d_im.hasProcessed())
+ {
+ return;
+ }
+ }
+ else
+ {
+ Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
+ // otherwise, we a syntactic subset of p
+ card_parents.push_back(p);
+ card_parent_ids.push_back(is_union ? 2 : e);
+ }
+ }
+ Assert(d_card_parent[n].empty());
+ Trace("sets-debug") << "get parent representatives..." << std::endl;
+ // for each parent, take their representatives
+ for (unsigned k = 0, numcp = card_parents.size(); k < numcp; k++)
+ {
+ Node cpk = card_parents[k];
+ Node eqcc = d_ee.getRepresentative(cpk);
+ Trace("sets-debug") << "Check card parent " << k << "/"
+ << card_parents.size() << std::endl;
+
+ // if parent is singleton, then we should either be empty to equal to it
+ Node eqccSingleton = d_state.getSingletonEqClass(eqcc);
+ if (!eqccSingleton.isNull())
+ {
+ bool eq_parent = false;
+ std::vector<Node> exps;
+ d_state.addEqualityToExp(cpk, eqccSingleton, exps);
+ if (d_state.areDisequal(n, emp_set))
+ {
+ exps.push_back(n.eqNode(emp_set).negate());
+ eq_parent = true;
+ }
+ else
+ {
+ const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
+ if (!pmemsE.empty())
+ {
+ Node pmem = pmemsE.begin()->second;
+ exps.push_back(pmem);
+ d_state.addEqualityToExp(n, pmem[1], exps);
+ eq_parent = true;
+ }
+ }
+ // must be equal to parent
+ if (eq_parent)
+ {
+ Node conc = n.eqNode(cpk);
+ d_im.assertInference(conc, exps, "cg_par_sing");
+ d_im.flushPendingLemmas();
+ }
+ else
+ {
+ // split on empty
+ Trace("sets-nf") << "Split empty : " << n << std::endl;
+ d_im.split(n.eqNode(emp_set), 1);
+ }
+ Assert(d_im.hasProcessed());
+ return;
+ }
+ else
+ {
+ bool dup = false;
+ for (unsigned l = 0, numcpn = d_card_parent[n].size(); l < numcpn; l++)
+ {
+ Node cpnl = d_card_parent[n][l];
+ if (eqcc != cpnl)
+ {
+ continue;
+ }
+ Trace("sets-debug") << " parents " << l << " and " << k
+ << " are equal, ids = " << card_parent_ids[l]
+ << " " << card_parent_ids[k] << std::endl;
+ dup = true;
+ if (n.getKind() != INTERSECTION)
+ {
+ continue;
+ }
+ Assert(card_parent_ids[l] != 2);
+ std::vector<Node> conc;
+ if (card_parent_ids[k] == 2)
+ {
+ // intersection is equal to other parent
+ unsigned pid = 1 - card_parent_ids[l];
+ if (!d_state.areEqual(n[pid], n))
+ {
+ Trace("sets-debug")
+ << " one of them is union, make equal to other..."
+ << std::endl;
+ conc.push_back(n[pid].eqNode(n));
+ }
+ }
+ else
+ {
+ if (!d_state.areEqual(cpk, n))
+ {
+ Trace("sets-debug")
+ << " neither is union, make equal to one parent..."
+ << std::endl;
+ // intersection is equal to one of the parents
+ conc.push_back(cpk.eqNode(n));
+ }
+ }
+ d_im.assertInference(conc, cpk.eqNode(cpnl), "cg_pareq");
+ d_im.flushPendingLemmas();
+ if (d_im.hasProcessed())
+ {
+ return;
+ }
+ }
+ if (!dup)
+ {
+ d_card_parent[n].push_back(eqcc);
+ }
+ }
+ }
+ // now recurse on parents (to ensure their normal will be computed after
+ // this eqc)
+ exp.push_back(eqc.eqNode(n));
+ for (const Node& cpnc : d_card_parent[n])
+ {
+ checkCardCyclesRec(cpnc, curr, exp);
+ if (d_im.hasProcessed())
+ {
+ return;
+ }
+ }
+ exp.pop_back();
+ }
+ curr.pop_back();
+ // parents now processed, can add to ordered list
+ d_oSetEqc.push_back(eqc);
+}
+
+void CardinalityExtension::checkNormalForms(std::vector<Node>& intro_sets)
+{
+ Trace("sets") << "Check normal forms..." << std::endl;
+ // now, build normal form for each equivalence class
+ // d_oSetEqc is now sorted such that for each d_oSetEqc[i], d_oSetEqc[j],
+ // if d_oSetEqc[i] is a strict syntactic subterm of d_oSetEqc[j], then i<j.
+ d_ff.clear();
+ d_nf.clear();
+ for (int i = (int)(d_oSetEqc.size() - 1); i >= 0; i--)
+ {
+ checkNormalForm(d_oSetEqc[i], intro_sets);
+ if (d_im.hasProcessed() || !intro_sets.empty())
+ {
+ return;
+ }
+ }
+ Trace("sets") << "Done check normal forms" << std::endl;
+}
+
+void CardinalityExtension::checkNormalForm(Node eqc,
+ std::vector<Node>& intro_sets)
+{
+ TypeNode tn = eqc.getType();
+ Trace("sets") << "Compute normal form for " << eqc << std::endl;
+ Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
+ if (eqc == d_state.getEmptySetEqClass(tn))
+ {
+ d_nf[eqc].clear();
+ Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
+ return;
+ }
+ // flat/normal forms are sets of equivalence classes
+ Node base;
+ std::vector<Node> comps;
+ std::map<Node, std::map<Node, std::vector<Node> > >::iterator it =
+ d_ff.find(eqc);
+ if (it != d_ff.end())
+ {
+ for (std::pair<const Node, std::vector<Node> >& itf : it->second)
+ {
+ std::sort(itf.second.begin(), itf.second.end());
+ if (base.isNull())
+ {
+ base = itf.first;
+ }
+ else
+ {
+ comps.push_back(itf.first);
+ }
+ Trace("sets-nf") << " F " << itf.first << " : " << itf.second
+ << std::endl;
+ Trace("sets-nf-debug") << " ...";
+ d_state.debugPrintSet(itf.first, "sets-nf-debug");
+ Trace("sets-nf-debug") << std::endl;
+ }
+ }
+ else
+ {
+ Trace("sets-nf") << "(no flat forms)" << std::endl;
+ }
+ std::map<Node, std::vector<Node> >& ffeqc = d_ff[eqc];
+ Assert(d_nf.find(eqc) == d_nf.end());
+ std::vector<Node>& nfeqc = d_nf[eqc];
+ NodeManager* nm = NodeManager::currentNM();
+ bool success = true;
+ Node emp_set = d_state.getEmptySet(tn);
+ if (!base.isNull())
+ {
+ for (unsigned j = 0, csize = comps.size(); j < csize; j++)
+ {
+ // compare if equal
+ std::vector<Node> c;
+ c.push_back(base);
+ c.push_back(comps[j]);
+ std::vector<Node> only[2];
+ std::vector<Node> common;
+ Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs "
+ << comps[j] << std::endl;
+ unsigned k[2] = {0, 0};
+ while (k[0] < ffeqc[c[0]].size() || k[1] < ffeqc[c[1]].size())
+ {
+ bool proc = true;
+ for (unsigned e = 0; e < 2; e++)
+ {
+ if (k[e] == ffeqc[c[e]].size())
+ {
+ for (; k[1 - e] < ffeqc[c[1 - e]].size(); ++k[1 - e])
+ {
+ only[1 - e].push_back(ffeqc[c[1 - e]][k[1 - e]]);
+ }
+ proc = false;
+ }
+ }
+ if (proc)
+ {
+ if (ffeqc[c[0]][k[0]] == ffeqc[c[1]][k[1]])
+ {
+ common.push_back(ffeqc[c[0]][k[0]]);
+ k[0]++;
+ k[1]++;
+ }
+ else if (ffeqc[c[0]][k[0]] < ffeqc[c[1]][k[1]])
+ {
+ only[0].push_back(ffeqc[c[0]][k[0]]);
+ k[0]++;
+ }
+ else
+ {
+ only[1].push_back(ffeqc[c[1]][k[1]]);
+ k[1]++;
+ }
+ }
+ }
+ if (!only[0].empty() || !only[1].empty())
+ {
+ if (Trace.isOn("sets-nf-debug"))
+ {
+ Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
+ for (unsigned e = 0; e < 2; e++)
+ {
+ Trace("sets-nf-debug") << " " << c[e] << " : { ";
+ for (unsigned l = 0; l < only[e].size(); l++)
+ {
+ if (l > 0)
+ {
+ Trace("sets-nf-debug") << ", ";
+ }
+ Trace("sets-nf-debug") << "[" << only[e][l] << "]";
+ }
+ Trace("sets-nf-debug") << " }" << std::endl;
+ }
+ }
+ // try to make one empty, prefer the unique ones first
+ for (unsigned e = 0; e < 3; e++)
+ {
+ unsigned sz = e == 2 ? common.size() : only[e].size();
+ for (unsigned l = 0; l < sz; l++)
+ {
+ Node r = e == 2 ? common[l] : only[e][l];
+ Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
+ Trace("sets-nf-debug") << " actual : ";
+ d_state.debugPrintSet(r, "sets-nf-debug");
+ Trace("sets-nf-debug") << std::endl;
+ Assert(!d_state.areEqual(r, emp_set));
+ if (!d_state.areDisequal(r, emp_set) && !d_state.hasMembers(r))
+ {
+ // guess that its equal empty if it has no explicit members
+ Trace("sets-nf") << " Split empty : " << r << std::endl;
+ Trace("sets-nf") << "Actual Split : ";
+ d_state.debugPrintSet(r, "sets-nf");
+ Trace("sets-nf") << std::endl;
+ d_im.split(r.eqNode(emp_set), 1);
+ Assert(d_im.hasProcessed());
+ return;
+ }
+ }
+ }
+ for (const Node& o0 : only[0])
+ {
+ for (const Node& o1 : only[1])
+ {
+ bool disjoint = false;
+ Trace("sets-nf-debug")
+ << "Try split " << o0 << " against " << o1 << std::endl;
+ // split them
+ for (unsigned e = 0; e < 2; e++)
+ {
+ Node r1 = e == 0 ? o0 : o1;
+ Node r2 = e == 0 ? o1 : o0;
+ // check if their intersection exists modulo equality
+ Node r1r2i = d_state.getBinaryOpTerm(INTERSECTION, r1, r2);
+ if (!r1r2i.isNull())
+ {
+ Trace("sets-nf-debug")
+ << "Split term already exists, but not in cardinality "
+ "graph : "
+ << r1r2i << ", should be empty." << std::endl;
+ // their intersection is empty (probably?)
+ // e.g. these are two disjoint venn regions, proceed to next
+ // pair
+ Assert(d_state.areEqual(emp_set, r1r2i));
+ disjoint = true;
+ break;
+ }
+ }
+ if (!disjoint)
+ {
+ // simply introduce their intersection
+ Assert(o0 != o1);
+ Node kca = d_state.getProxy(o0);
+ Node kcb = d_state.getProxy(o1);
+ Node intro =
+ Rewriter::rewrite(nm->mkNode(INTERSECTION, kca, kcb));
+ Trace("sets-nf") << " Intro split : " << o0 << " against " << o1
+ << ", term is " << intro << std::endl;
+ intro_sets.push_back(intro);
+ Assert(!d_ee.hasTerm(intro));
+ return;
+ }
+ }
+ }
+ // should never get here
+ success = false;
+ }
+ }
+ if (success)
+ {
+ // normal form is flat form of base
+ nfeqc.insert(nfeqc.end(), ffeqc[base].begin(), ffeqc[base].end());
+ Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
+ }
+ else
+ {
+ Trace("sets-nf") << "failed to build N " << eqc << std::endl;
+ }
+ }
+ else
+ {
+ // must ensure disequal from empty
+ if (!eqc.isConst() && !d_state.areDisequal(eqc, emp_set)
+ && !d_state.hasMembers(eqc))
+ {
+ Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
+ d_im.split(eqc.eqNode(emp_set));
+ success = false;
+ }
+ else
+ {
+ // normal form is this equivalence class
+ nfeqc.push_back(eqc);
+ Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }"
+ << std::endl;
+ }
+ }
+ if (!success)
+ {
+ Assert(d_im.hasProcessed());
+ return;
+ }
+ // Send to parents (a parent is a set that contains a term in this equivalence
+ // class as a direct child).
+ const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
+ if (nvsets.empty())
+ {
+ // no non-variable sets
+ return;
+ }
+ std::map<Node, std::map<Node, bool> > parents_proc;
+ for (const Node& n : nvsets)
+ {
+ Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
+ if (d_card_parent[n].empty())
+ {
+ // nothing to do
+ continue;
+ }
+ Assert(d_localBase.find(n) != d_localBase.end());
+ Node cbase = d_localBase[n];
+ Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
+ for (const Node& p : d_card_parent[n])
+ {
+ Trace("sets-nf-debug") << "Check parent " << p << std::endl;
+ if (parents_proc[cbase].find(p) != parents_proc[cbase].end())
+ {
+ Trace("sets-nf-debug") << "..already processed parent " << p << " for "
+ << cbase << std::endl;
+ continue;
+ }
+ parents_proc[cbase][p] = true;
+ Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p
+ << "] ), from " << n << "..." << std::endl;
+
+ std::vector<Node>& ffpc = d_ff[p][cbase];
+ for (const Node& nfeqci : nfeqc)
+ {
+ if (std::find(ffpc.begin(), ffpc.end(), nfeqci) == ffpc.end())
+ {
+ ffpc.insert(ffpc.end(), nfeqc.begin(), nfeqc.end());
+ }
+ else
+ {
+ // if it is a duplicate venn region, it must be empty since it is
+ // coming from syntactically disjoint siblings
+ }
+ }
+ }
+ }
+}
+
+void CardinalityExtension::checkMinCard()
+{
+ NodeManager* nm = NodeManager::currentNM();
+ const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
+ for (int i = (int)(setEqc.size() - 1); i >= 0; i--)
+ {
+ Node eqc = setEqc[i];
+ TypeNode tn = eqc.getType().getSetElementType();
+ if (d_t_card_enabled.find(tn) == d_t_card_enabled.end())
+ {
+ // cardinality is not enabled for this type, skip
+ continue;
+ }
+ // get members in class
+ const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
+ if (pmemsE.empty())
+ {
+ // no members, trivial
+ continue;
+ }
+ std::vector<Node> exp;
+ std::vector<Node> members;
+ Node cardTerm;
+ std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
+ if (it != d_eqc_to_card_term.end())
+ {
+ cardTerm = it->second;
+ }
+ else
+ {
+ cardTerm = nm->mkNode(CARD, eqc);
+ }
+ for (const std::pair<const Node, Node>& itmm : pmemsE)
+ {
+ members.push_back(itmm.first);
+ exp.push_back(nm->mkNode(MEMBER, itmm.first, cardTerm[0]));
+ }
+ if (members.size() > 1)
+ {
+ exp.push_back(nm->mkNode(DISTINCT, members));
+ }
+ if (!members.empty())
+ {
+ Node conc =
+ nm->mkNode(GEQ, cardTerm, nm->mkConst(Rational(members.size())));
+ Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
+ d_im.assertInference(conc, expn, "mincard", 1);
+ }
+ }
+ // flush the lemmas
+ d_im.flushPendingLemmas();
+}
+
+bool CardinalityExtension::isModelValueBasic(Node eqc)
+{
+ return d_nf[eqc].size() == 1 && d_nf[eqc][0] == eqc;
+}
+
+void CardinalityExtension::mkModelValueElementsFor(
+ Valuation& val,
+ Node eqc,
+ std::vector<Node>& els,
+ const std::map<Node, Node>& mvals)
+{
+ TypeNode elementType = eqc.getType().getSetElementType();
+ if (isModelValueBasic(eqc))
+ {
+ std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
+ if (it != d_eqc_to_card_term.end())
+ {
+ // slack elements from cardinality value
+ Node v = val.getModelValue(it->second);
+ Trace("sets-model") << "Cardinality of " << eqc << " is " << v
+ << std::endl;
+ Assert(v.getConst<Rational>() <= LONG_MAX,
+ "Exceeded LONG_MAX in sets model");
+ unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
+ Assert(els.size() <= vu);
+ NodeManager* nm = NodeManager::currentNM();
+ while (els.size() < vu)
+ {
+ els.push_back(nm->mkNode(SINGLETON, nm->mkSkolem("msde", elementType)));
+ }
+ }
+ else
+ {
+ Trace("sets-model") << "No slack elements for " << eqc << std::endl;
+ }
+ }
+ else
+ {
+ Trace("sets-model") << "Build value for " << eqc
+ << " based on normal form, size = " << d_nf[eqc].size()
+ << std::endl;
+ // it is union of venn regions
+ for (unsigned j = 0; j < d_nf[eqc].size(); j++)
+ {
+ std::map<Node, Node>::const_iterator itm = mvals.find(d_nf[eqc][j]);
+ if (itm != mvals.end())
+ {
+ els.push_back(itm->second);
+ }
+ else
+ {
+ Assert(false);
+ }
+ }
+ }
+}
+
+} // namespace sets
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file cardinality_extension.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief An extension of the theory sets for handling cardinality constraints
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SETS__CARDINALITY_EXTENSION_H
+#define CVC4__THEORY__SETS__CARDINALITY_EXTENSION_H
+
+#include "context/cdhashset.h"
+#include "context/context.h"
+#include "theory/sets/inference_manager.h"
+#include "theory/sets/solver_state.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+/**
+ * This class implements a variant of the procedure from Bansal et al, IJCAR
+ * 2016. It is used during a full effort check in the following way:
+ * reset(); { registerTerm(n,lemmas); | n in CardTerms } check();
+ * where CardTerms is the set of all applications of CARD in the current
+ * context.
+ *
+ * The remaining public methods are used during model construction, i.e.
+ * the collectModelInfo method of the theory of sets.
+ *
+ * The procedure from Bansal et al IJCAR 2016 introduces the notion of a
+ * "cardinality graph", where the nodes of this graph are sets and (directed)
+ * edges connect sets to their Venn regions wrt to other sets. For example,
+ * if (A \ B) is a term in the current context, then the node A is
+ * connected via an edge to child (A \ B). The node (A ^ B) is a child
+ * of both A and B. The notion of a cardinality graph is loosely followed
+ * in the procedure implemented by this class.
+ *
+ * The main difference wrt Bansal et al IJCAR 2016 is that the nodes of the
+ * cardinality graph considered by this class are not arbitrary set terms, but
+ * are instead representatives of equivalence classes. For more details, see
+ * documentation of the inference schemas in the private methods of this class.
+ *
+ * This variant of the procedure takes inspiration from the procedure
+ * for word equations in Liang et al, CAV 2014. In that procedure, "normal
+ * forms" are generated for String terms by recursively expanding
+ * concatentations modulo equality. This procedure similarly maintains
+ * normal forms, where the normal form for Set terms is a set of (equivalence
+ * class representatives of) Venn regions that do not contain the empty set.
+ */
+class CardinalityExtension
+{
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+ /**
+ * Constructs a new instance of the cardinality solver w.r.t. the provided
+ * contexts.
+ */
+ CardinalityExtension(SolverState& s,
+ InferenceManager& im,
+ eq::EqualityEngine& e,
+ context::Context* c,
+ context::UserContext* u);
+
+ ~CardinalityExtension() {}
+ /** reset
+ *
+ * Called at the beginning of a full effort check. This resets the data
+ * structures used by this class during a full effort check.
+ */
+ void reset();
+ /** register term
+ *
+ * Register that the term n exists in the current context, where n is an
+ * application of CARD.
+ */
+ void registerTerm(Node n);
+ /** check
+ *
+ * Invoke a full effort check of the cardinality solver. At a high level,
+ * this asserts inferences via the inference manager object d_im. If no
+ * inferences are made, then the current set of assertions is satisfied
+ * with respect to constraints involving set cardinality.
+ *
+ * This method applies various inference schemas in succession until an
+ * inference is made. These inference schemas are given in the private
+ * methods of this class (e.g. checkMinCard, checkCardBuildGraph, etc.).
+ */
+ void check();
+ /** Is model value basic?
+ *
+ * This returns true if equivalence class eqc is a "leaf" in the cardinality
+ * graph.
+ */
+ bool isModelValueBasic(Node eqc);
+ /** get model elements
+ *
+ * This method updates els so that it is the set of elements that occur in
+ * an equivalence class (whose representative is eqc) in the model we are
+ * building. Notice that els may already have elements in it (from explicit
+ * memberships from the base set solver for leaf nodes of the cardinality
+ * graph). This method is used during the collectModelInfo method of theory
+ * of sets.
+ *
+ * The argument v is the Valuation utility of the theory of sets, which is
+ * used by this method to query the value assigned to cardinality terms by
+ * the theory of arithmetic.
+ *
+ * The argument mvals maps set equivalence classes to their model values.
+ * Due to our model construction algorithm, it can be assumed that all
+ * sets in the normal form of eqc occur in the domain of mvals by the order
+ * in which sets are assigned.
+ */
+ void mkModelValueElementsFor(Valuation& v,
+ Node eqc,
+ std::vector<Node>& els,
+ const std::map<Node, Node>& mvals);
+ /** get ordered sets equivalence classes
+ *
+ * Get the ordered set of equivalence classes computed by this class. This
+ * ordering ensures the invariant mentioned above mkModelValueElementsFor.
+ *
+ * This ordering ensures that all children of a node in the cardinality
+ * graph computed by this class occur before it in this list.
+ */
+ const std::vector<Node>& getOrderedSetsEqClasses() { return d_oSetEqc; }
+
+ private:
+ /** constants */
+ Node d_zero;
+ /** the empty vector */
+ std::vector<Node> d_emp_exp;
+ /** Reference to the state object for the theory of sets */
+ SolverState& d_state;
+ /** Reference to the inference manager for the theory of sets */
+ InferenceManager& d_im;
+ /** Reference to the equality engine of theory of sets */
+ eq::EqualityEngine& d_ee;
+ /** register cardinality term
+ *
+ * This method add lemmas corresponding to the definition of
+ * the cardinality of set term n. For example, if n is A^B (denoting set
+ * intersection as ^), then we consider the lemmas card(A^B)>=0,
+ * card(A) = card(A\B) + card(A^B) and card(B) = card(B\A) + card(A^B).
+ *
+ * The exact form of this lemma is modified such that proxy variables are
+ * introduced for set terms as needed (see SolverState::getProxy).
+ */
+ void registerCardinalityTerm(Node n);
+ /** check register
+ *
+ * This ensures that all (non-redundant, relevant) non-variable set terms in
+ * the current context have been passed to registerCardinalityTerm. In other
+ * words, this ensures that the cardinality graph for these terms can be
+ * constructed since the cardinality relationships for these terms have been
+ * elaborated as lemmas.
+ *
+ * Notice a term is redundant in a context if it is congruent to another
+ * term that is already in the context; it is not relevant if no cardinality
+ * constraints exist for its type.
+ */
+ void checkRegister();
+ /** check minimum cardinality
+ *
+ * This adds lemmas to the argument of the method of the form
+ * distinct(x1,...,xn) ^ member(x1,S) ^ ... ^ member(xn,S) => card(S) >= n
+ * This lemma enforces the rules GUESS_LOWER_BOUND and PROPAGATE_MIN_SIZE
+ * from Bansal et. al IJCAR 2016.
+ *
+ * Notice that member(x1,S) is implied to hold in the current context. This
+ * means that it may be the case that member(x,T) ^ T = S are asserted
+ * literals. Furthermore, x1, ..., xn reside in distinct equivalence classes
+ * but are not necessarily entailed to be distinct.
+ */
+ void checkMinCard();
+ /** check cardinality cycles
+ *
+ * The purpose of this inference schema is to construct two data structures:
+ *
+ * (1) d_card_parent, which maps set terms (A op B) for op in { \, ^ } to
+ * equivalence class representatives of their "parents", where:
+ * parent( A ^ B ) = A, B
+ * parent( A \ B ) = A
+ * Additionally, (A union B) is a parent of all three of the above sets
+ * if it exists as a term in the current context. As exceptions,
+ * if A op B = A, then A is not a parent of A ^ B and similarly for B.
+ * If A ^ B is empty, then it has no parents.
+ *
+ * We say the cardinality graph induced by the current set of equalities
+ * is an (irreflexive, acyclic) graph whose nodes are equivalence classes and
+ * which contains a (directed) edge r1 to r2 if there exists a term t2 in r2
+ * that has some parent t1 in r1.
+ *
+ * (2) d_oSetEqc, an ordered set of equivalence classes whose types are set.
+ * These equivalence classes have the property that if r1 is a descendant
+ * of r2 in the cardinality graph, then r1 must come before r2 in d_oSetEqc.
+ *
+ * This inference schema may make various inferences while building these
+ * two data structures if the current equality arrangement of sets is not
+ * as expected. For example, it will infer equalities between sets based on
+ * the emptiness and equalities of sets in adjacent children in the
+ * cardinality graph, to give some examples:
+ * (A \ B = empty) => A = A ^ B
+ * A^B = B => B \ A = empty
+ * A union B = A ^ B => A \ B = empty AND B \ A = empty
+ * and so on.
+ *
+ * It will also recognize when a cycle occurs in the cardinality graph, in
+ * which case an equality chain between sets can be inferred. For an example,
+ * see checkCardCyclesRec below.
+ *
+ * This method is inspired by the checkCycles inference schema in the theory
+ * of strings.
+ */
+ void checkCardCycles();
+ /**
+ * Helper function for above. Called when wish to process equivalence class
+ * eqc.
+ *
+ * Argument curr contains the equivalence classes we are currently processing,
+ * which are descendants of eqc in the cardinality graph, where eqc is the
+ * representative of some equivalence class.
+ *
+ * Argument exp contains an explanation of why the chain of children curr
+ * are descedants of . For example, say we are in context with equivalence
+ * classes:
+ * { A, B, C^D }, { D, B ^ C, A ^ E }
+ * We may recursively call this method via the following steps:
+ * eqc = D, curr = {}, exp = {}
+ * eqc = A, curr = { D }, exp = { D = B^C }
+ * eqc = A, curr = { D, A }, exp = { D = B^C, A = C^D }
+ * after which we discover a cycle in the cardinality graph. We infer
+ * that A must be equal to D, where exp is an explanation of the cycle.
+ */
+ void checkCardCyclesRec(Node eqc,
+ std::vector<Node>& curr,
+ std::vector<Node>& exp);
+ /** check normal forms
+ *
+ * This method attempts to assign "normal forms" to all set equivalence
+ * classes whose types have cardinality constraints. Normal forms are
+ * defined recursively.
+ *
+ * A "normal form" of an equivalence class [r] (where [r] denotes the
+ * equivalence class whose representative is r) is a set of representatives
+ * U = { r1, ..., rn }. If there exists at least one set in [r] that has a
+ * "flat form", then all sets in the equivalence class have flat form U.
+ * If no set in U has a flat form, then U = { r } if r does not contain
+ * the empty set, and {} otherwise. Notice that the choice of representative
+ * r is determined by the equality engine.
+ *
+ * A "flat form" of a set term T is the union of the normal forms of the
+ * equivalence classes that contain sets whose parent is T.
+ *
+ * In terms of the cardinality graph, the "flat form" of term t is the set
+ * of leaves of t that are descendants of it in the cardinality graph induced
+ * by the current set of assertions. Notice a flat form is only defined if t
+ * has children. If all terms in an equivalence class E with flat forms have
+ * the same flat form, then E is added as a node to the cardinality graph with
+ * edges connecting to all equivalence classes with terms that have a parent
+ * in E.
+ *
+ * In the following inference schema, the argument intro_sets is updated to
+ * contain the set of new set terms that the procedure is requesting to
+ * introduce for the purpose of forcing the flat forms of two equivalent sets
+ * to become identical. If any equivalence class cannot be assigned a normal
+ * form, then the resulting intro_sets is guaranteed to be non-empty.
+ *
+ * As an example, say we have a context with equivalence classes:
+ * {A, D}, {C, A^B}, {E, C^D}, {C\D}, {D\C}, {A\B}, {empty, B\A},
+ * where assume the first term in each set is its representative. An ordered
+ * list d_oSetEqc for this context:
+ * A, C, E, C\D, D\C, A\B, empty, ...
+ * The normal form of {empty, B\A} is {}, since it contains the empty set.
+ * The normal forms for each of the singleton equivalence classes are
+ * themselves.
+ * The flat form of each of E and C^D does not exist, hence the normal form
+ * of {E, C^D} is {E}.
+ * The flat form of C is {E, C\D}, noting that C^D and C\D are terms whose
+ * parent is C, hence {E, C\D} is the normal form for class {C, A^B}.
+ * The flat form of A is {E, C\D, A\B} and the flat form of D is {E, D\C}.
+ * Hence, no normal form can be assigned to class {A, D}. Instead this method
+ * will e.g. add (C\D)^E to intro_sets, which will force the solver
+ * to explore a model where the Venn regions (C\D)^E (C\D)\E and E\(C\D) are
+ * considered while constructing flat forms. Splitting on whether these sets
+ * are empty will eventually lead to a model where the flat forms of A and D
+ * are the same.
+ */
+ void checkNormalForms(std::vector<Node>& intro_sets);
+ /**
+ * Called for each equivalence class, in order of d_oSetEqc, by the above
+ * function.
+ */
+ void checkNormalForm(Node eqc, std::vector<Node>& intro_sets);
+ /** element types of sets for which cardinality is enabled */
+ std::map<TypeNode, bool> d_t_card_enabled;
+ /**
+ * This maps equivalence classes r to an application of cardinality of the
+ * form card( t ), where t = r holds in the current context.
+ */
+ std::map<Node, Node> d_eqc_to_card_term;
+ /**
+ * User-context-dependent set of set terms for which we have called
+ * registerCardinalityTerm on.
+ */
+ NodeSet d_card_processed;
+ /** The ordered set of equivalence classes, see checkCardCycles. */
+ std::vector<Node> d_oSetEqc;
+ /**
+ * This maps set terms to the set of representatives of their "parent" sets,
+ * see checkCardCycles.
+ */
+ std::map<Node, std::vector<Node> > d_card_parent;
+ /**
+ * Maps equivalence classes + set terms in that equivalence class to their
+ * "flat form" (see checkNormalForms).
+ */
+ std::map<Node, std::map<Node, std::vector<Node> > > d_ff;
+ /** Maps equivalence classes to their "normal form" (see checkNormalForms). */
+ std::map<Node, std::vector<Node> > d_nf;
+ /** The local base node map
+ *
+ * This maps set terms to the "local base node" of its cardinality graph.
+ * The local base node of S is the intersection node that is either S itself
+ * or is adjacent to S in the cardinality graph. This maps
+ *
+ * For example, the ( A ^ B ) is the local base of each of the sets (A \ B),
+ * ( A ^ B ), and (B \ A).
+ */
+ std::map<Node, Node> d_localBase;
+}; /* class CardinalityExtension */
+
+} // namespace sets
+} // namespace theory
+} // namespace CVC4
+
+#endif
--- /dev/null
+/********************* */
+/*! \file inference_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of the inference manager for the theory of sets
+ **/
+
+#include "theory/sets/inference_manager.h"
+
+#include "options/sets_options.h"
+#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+InferenceManager::InferenceManager(TheorySetsPrivate& p,
+ SolverState& s,
+ eq::EqualityEngine& e,
+ context::Context* c,
+ context::UserContext* u)
+ : d_parent(p), d_state(s), d_ee(e), d_lemmas_produced(u), d_keep(c)
+{
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+void InferenceManager::reset()
+{
+ d_sentLemma = false;
+ d_addedFact = false;
+ d_pendingLemmas.clear();
+}
+
+bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
+{
+ // should we send this fact out as a lemma?
+ if ((options::setsInferAsLemmas() && inferType != -1) || inferType == 1)
+ {
+ if (d_state.isEntailed(fact, true))
+ {
+ return false;
+ }
+ Node lem = fact;
+ if (exp != d_true)
+ {
+ lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
+ }
+ d_pendingLemmas.push_back(lem);
+ return true;
+ }
+ Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
+ << std::endl;
+ if (fact.isConst())
+ {
+ // either trivial or a conflict
+ if (fact == d_false)
+ {
+ Trace("sets-lemma") << "Conflict : " << exp << std::endl;
+ d_state.setConflict(exp);
+ return true;
+ }
+ return false;
+ }
+ else if (fact.getKind() == AND
+ || (fact.getKind() == NOT && fact[0].getKind() == OR))
+ {
+ bool ret = false;
+ Node f = fact.getKind() == NOT ? fact[0] : fact;
+ for (unsigned i = 0; i < f.getNumChildren(); i++)
+ {
+ Node factc = fact.getKind() == NOT ? f[i].negate() : f[i];
+ bool tret = assertFactRec(factc, exp, inferType);
+ ret = ret || tret;
+ if (d_state.isInConflict())
+ {
+ return true;
+ }
+ }
+ return ret;
+ }
+ bool polarity = fact.getKind() != NOT;
+ TNode atom = polarity ? fact : fact[0];
+ // things we can assert to equality engine
+ if (atom.getKind() == MEMBER
+ || (atom.getKind() == EQUAL && atom[0].getType().isSet()))
+ {
+ // send to equality engine
+ if (d_parent.assertFact(fact, exp))
+ {
+ d_addedFact = true;
+ return true;
+ }
+ }
+ else if (!d_state.isEntailed(fact, true))
+ {
+ // must send as lemma
+ Node lem = fact;
+ if (exp != d_true)
+ {
+ lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
+ }
+ d_pendingLemmas.push_back(lem);
+ return true;
+ }
+ return false;
+}
+void InferenceManager::assertInference(Node fact,
+ Node exp,
+ const char* c,
+ int inferType)
+{
+ d_keep.insert(exp);
+ d_keep.insert(fact);
+ if (assertFactRec(fact, exp, inferType))
+ {
+ Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
+ << c << std::endl;
+ Trace("sets-assertion")
+ << "(assert (=> " << exp << " " << fact << ")) ; by " << c << std::endl;
+ }
+}
+
+void InferenceManager::assertInference(Node fact,
+ std::vector<Node>& exp,
+ const char* c,
+ int inferType)
+{
+ Node exp_n = exp.empty() ? d_true
+ : (exp.size() == 1
+ ? exp[0]
+ : NodeManager::currentNM()->mkNode(AND, exp));
+ assertInference(fact, exp_n, c, inferType);
+}
+
+void InferenceManager::assertInference(std::vector<Node>& conc,
+ Node exp,
+ const char* c,
+ int inferType)
+{
+ if (!conc.empty())
+ {
+ Node fact = conc.size() == 1 ? conc[0]
+ : NodeManager::currentNM()->mkNode(AND, conc);
+ assertInference(fact, exp, c, inferType);
+ }
+}
+void InferenceManager::assertInference(std::vector<Node>& conc,
+ std::vector<Node>& exp,
+ const char* c,
+ int inferType)
+{
+ Node exp_n = exp.empty() ? d_true
+ : (exp.size() == 1
+ ? exp[0]
+ : NodeManager::currentNM()->mkNode(AND, exp));
+ assertInference(conc, exp_n, c, inferType);
+}
+
+void InferenceManager::split(Node n, int reqPol)
+{
+ n = Rewriter::rewrite(n);
+ Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
+ flushLemma(lem);
+ Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
+ if (reqPol != 0)
+ {
+ Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
+ << std::endl;
+ d_parent.getOutputChannel()->requirePhase(n, reqPol > 0);
+ }
+}
+void InferenceManager::flushLemmas(std::vector<Node>& lemmas, bool preprocess)
+{
+ for (const Node& l : lemmas)
+ {
+ flushLemma(l, preprocess);
+ }
+ lemmas.clear();
+}
+
+void InferenceManager::flushLemma(Node lem, bool preprocess)
+{
+ if (d_lemmas_produced.find(lem) != d_lemmas_produced.end())
+ {
+ Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
+ return;
+ }
+ Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
+ d_lemmas_produced.insert(lem);
+ d_parent.getOutputChannel()->lemma(lem, false, preprocess);
+ d_sentLemma = true;
+}
+
+void InferenceManager::flushPendingLemmas(bool preprocess)
+{
+ for (const Node& l : d_pendingLemmas)
+ {
+ flushLemma(l, preprocess);
+ }
+ d_pendingLemmas.clear();
+}
+
+bool InferenceManager::hasLemmaCached(Node lem) const
+{
+ return d_lemmas_produced.find(lem) != d_lemmas_produced.end();
+}
+
+bool InferenceManager::hasProcessed() const
+{
+ return d_state.isInConflict() || d_sentLemma || d_addedFact;
+}
+bool InferenceManager::hasSentLemma() const { return d_sentLemma; }
+bool InferenceManager::hasAddedFact() const { return d_addedFact; }
+
+} // namespace sets
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file inference_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The inference manager for the theory of sets.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SETS__INFERENCE_MANAGER_H
+#define CVC4__THEORY__SETS__INFERENCE_MANAGER_H
+
+#include "theory/sets/solver_state.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsPrivate;
+
+/** Inference manager
+ *
+ * This class manages inferences produced by the theory of sets. It manages
+ * whether inferences are processed as external lemmas on the output channel
+ * of theory of sets or internally as literals asserted to the equality engine
+ * of theory of sets. The latter literals are referred to as "facts".
+ */
+class InferenceManager
+{
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+ InferenceManager(TheorySetsPrivate& p,
+ SolverState& s,
+ eq::EqualityEngine& e,
+ context::Context* c,
+ context::UserContext* u);
+ /** reset
+ *
+ * Called at the beginning of a full effort check. Resets the information
+ * related to this class regarding whether facts and lemmas have been
+ * processed.
+ */
+ void reset();
+ /**
+ * Add facts corresponding to ( exp => fact ) via calls to the assertFact
+ * method of TheorySetsPrivate.
+ *
+ * The portions of fact that were unable to be processed as facts are added
+ * to the data member d_pendingLemmas.
+ *
+ * The argument inferType is used for overriding the policy on whether
+ * fact is processed as a lemma, where inferType=1 forces fact to be
+ * set as a lemma, and inferType=-1 forces fact to be processed as a fact
+ * (if possible).
+ *
+ * The argument c is the name of the inference, which is used for debugging.
+ */
+ void assertInference(Node fact, Node exp, const char* c, int inferType = 0);
+ /** same as above, where exp is interpreted as a conjunction */
+ void assertInference(Node fact,
+ std::vector<Node>& exp,
+ const char* c,
+ int inferType = 0);
+ /** same as above, where conc is interpreted as a conjunction */
+ void assertInference(std::vector<Node>& conc,
+ Node exp,
+ const char* c,
+ int inferType = 0);
+ /** same as above, where both exp and conc are interpreted as conjunctions */
+ void assertInference(std::vector<Node>& conc,
+ std::vector<Node>& exp,
+ const char* c,
+ int inferType = 0);
+
+ /** Flush lemmas
+ *
+ * This sends lemmas on the output channel of the theory of sets.
+ *
+ * The argument preprocess indicates whether preprocessing should be applied
+ * (by TheoryEngine) on each of lemmas.
+ */
+ void flushLemmas(std::vector<Node>& lemmas, bool preprocess = false);
+ /** singular version of above */
+ void flushLemma(Node lem, bool preprocess = false);
+ /** Do we have pending lemmas? */
+ bool hasPendingLemmas() const { return !d_pendingLemmas.empty(); }
+ /** Applies flushLemmas on d_pendingLemmas */
+ void flushPendingLemmas(bool preprocess = false);
+ /** flush the splitting lemma ( n OR (NOT n) )
+ *
+ * If reqPol is not 0, then a phase requirement for n is requested with
+ * polarity ( reqPol>0 ).
+ */
+ void split(Node n, int reqPol = 0);
+ /** Have we sent a lemma during the current call to a full effort check? */
+ bool hasSentLemma() const;
+ /** Have we added a fact during the current call to a full effort check? */
+ bool hasAddedFact() const;
+ /** Have we processed an inference (fact, lemma, or conflict)? */
+ bool hasProcessed() const;
+ /** Have we sent lem as a lemma in the current user context? */
+ bool hasLemmaCached(Node lem) const;
+
+ private:
+ /** constants */
+ Node d_true;
+ Node d_false;
+ /** the theory of sets which owns this */
+ TheorySetsPrivate& d_parent;
+ /** Reference to the state object for the theory of sets */
+ SolverState& d_state;
+ /** Reference to the equality engine of theory of sets */
+ eq::EqualityEngine& d_ee;
+ /** pending lemmas */
+ std::vector<Node> d_pendingLemmas;
+ /** sent lemma
+ *
+ * This flag is set to true during a full effort check if this theory
+ * called d_out->lemma(...).
+ */
+ bool d_sentLemma;
+ /** added fact
+ *
+ * This flag is set to true during a full effort check if this theory
+ * added an internal fact to its equality engine.
+ */
+ bool d_addedFact;
+ /** A user-context-dependent cache of all lemmas produced */
+ NodeSet d_lemmas_produced;
+ /**
+ * A set of nodes to ref-count. Nodes that are facts or are explanations of
+ * facts must be added to this set since the equality engine does not
+ * ref count nodes.
+ */
+ NodeSet d_keep;
+ /** Assert fact recursive
+ *
+ * This is a helper function for assertInference, which calls assertFact
+ * in theory of sets and adds to d_pendingLemmas based on fact.
+ * The argument inferType determines the policy on whether fact is processed
+ * as a fact or as a lemma (see assertInference above).
+ */
+ bool assertFactRec(Node fact, Node exp, int inferType = 0);
+};
+
+} // namespace sets
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__SETS__INFERENCE_MANAGER_H */
--- /dev/null
+/********************* */
+/*! \file solver_state.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sets state object
+ **/
+
+#include "theory/sets/solver_state.h"
+
+#include "expr/emptyset.h"
+#include "options/sets_options.h"
+#include "theory/sets/theory_sets_private.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+SolverState::SolverState(TheorySetsPrivate& p,
+ eq::EqualityEngine& e,
+ context::Context* c,
+ context::UserContext* u)
+ : d_conflict(c), d_parent(p), d_ee(e), d_proxy(u), d_proxy_to_term(u)
+{
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+void SolverState::reset()
+{
+ d_set_eqc.clear();
+ d_eqc_emptyset.clear();
+ d_eqc_univset.clear();
+ d_eqc_singleton.clear();
+ d_congruent.clear();
+ d_nvar_sets.clear();
+ d_var_set.clear();
+ d_pol_mems[0].clear();
+ d_pol_mems[1].clear();
+ d_members_index.clear();
+ d_singleton_index.clear();
+ d_bop_index.clear();
+ d_op_list.clear();
+}
+
+void SolverState::registerEqc(TypeNode tn, Node r)
+{
+ if (tn.isSet())
+ {
+ d_set_eqc.push_back(r);
+ }
+}
+
+void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
+{
+ Kind nk = n.getKind();
+ if (nk == MEMBER)
+ {
+ if (r.isConst())
+ {
+ Node s = d_ee.getRepresentative(n[1]);
+ Node x = d_ee.getRepresentative(n[0]);
+ int pindex = r == d_true ? 0 : (r == d_false ? 1 : -1);
+ if (pindex != -1)
+ {
+ if (d_pol_mems[pindex][s].find(x) == d_pol_mems[pindex][s].end())
+ {
+ d_pol_mems[pindex][s][x] = n;
+ Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n
+ << ", pindex = " << pindex << std::endl;
+ }
+ if (d_members_index[s].find(x) == d_members_index[s].end())
+ {
+ d_members_index[s][x] = n;
+ d_op_list[MEMBER].push_back(n);
+ }
+ }
+ else
+ {
+ Assert(false);
+ }
+ }
+ }
+ else if (nk == SINGLETON || nk == UNION || nk == INTERSECTION
+ || nk == SETMINUS || nk == EMPTYSET || nk == UNIVERSE_SET)
+ {
+ if (nk == SINGLETON)
+ {
+ // singleton lemma
+ getProxy(n);
+ Node re = d_ee.getRepresentative(n[0]);
+ if (d_singleton_index.find(re) == d_singleton_index.end())
+ {
+ d_singleton_index[re] = n;
+ d_eqc_singleton[r] = n;
+ d_op_list[SINGLETON].push_back(n);
+ }
+ else
+ {
+ d_congruent[n] = d_singleton_index[re];
+ }
+ }
+ else if (nk == EMPTYSET)
+ {
+ d_eqc_emptyset[tnn] = r;
+ }
+ else if (nk == UNIVERSE_SET)
+ {
+ Assert(options::setsExt());
+ d_eqc_univset[tnn] = r;
+ }
+ else
+ {
+ Node r1 = d_ee.getRepresentative(n[0]);
+ Node r2 = d_ee.getRepresentative(n[1]);
+ std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
+ std::map<Node, Node>::iterator itb = binr1.find(r2);
+ if (itb == binr1.end())
+ {
+ binr1[r2] = n;
+ d_op_list[nk].push_back(n);
+ }
+ else
+ {
+ d_congruent[n] = itb->second;
+ }
+ }
+ d_nvar_sets[r].push_back(n);
+ Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
+ }
+ else if (nk == VARIABLE)
+ {
+ // it is important that we check kind VARIABLE, due to the semantics of the
+ // universe set.
+ if (tnn.isSet())
+ {
+ if (d_var_set.find(r) == d_var_set.end())
+ {
+ d_var_set[r] = n;
+ }
+ }
+ }
+}
+
+bool SolverState::areEqual(Node a, Node b) const
+{
+ if (a == b)
+ {
+ return true;
+ }
+ if (d_ee.hasTerm(a) && d_ee.hasTerm(b))
+ {
+ return d_ee.areEqual(a, b);
+ }
+ return false;
+}
+
+bool SolverState::areDisequal(Node a, Node b) const
+{
+ if (a == b)
+ {
+ return false;
+ }
+ else if (d_ee.hasTerm(a) && d_ee.hasTerm(b))
+ {
+ return d_ee.areDisequal(a, b, false);
+ }
+ return a.isConst() && b.isConst();
+}
+
+void SolverState::setConflict() { d_conflict = true; }
+void SolverState::setConflict(Node conf)
+{
+ d_parent.getOutputChannel()->conflict(conf);
+ d_conflict = true;
+}
+
+void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
+{
+ if (a != b)
+ {
+ Assert(areEqual(a, b));
+ exp.push_back(a.eqNode(b));
+ }
+}
+
+Node SolverState::getEmptySetEqClass(TypeNode tn) const
+{
+ std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
+ if (it != d_eqc_emptyset.end())
+ {
+ return it->second;
+ }
+ return Node::null();
+}
+
+Node SolverState::getUnivSetEqClass(TypeNode tn) const
+{
+ std::map<TypeNode, Node>::const_iterator it = d_univset.find(tn);
+ if (it != d_univset.end())
+ {
+ return it->second;
+ }
+ return Node::null();
+}
+
+Node SolverState::getSingletonEqClass(Node r) const
+{
+ std::map<Node, Node>::const_iterator it = d_eqc_singleton.find(r);
+ if (it != d_eqc_singleton.end())
+ {
+ return it->second;
+ }
+ return Node::null();
+}
+
+Node SolverState::getBinaryOpTerm(Kind k, Node r1, Node r2) const
+{
+ std::map<Kind, std::map<Node, std::map<Node, Node> > >::const_iterator itk =
+ d_bop_index.find(k);
+ if (itk == d_bop_index.end())
+ {
+ return Node::null();
+ }
+ std::map<Node, std::map<Node, Node> >::const_iterator it1 =
+ itk->second.find(r1);
+ if (it1 == itk->second.end())
+ {
+ return Node::null();
+ }
+ std::map<Node, Node>::const_iterator it2 = it1->second.find(r2);
+ if (it2 == it1->second.end())
+ {
+ return Node::null();
+ }
+ return it2->second;
+}
+
+bool SolverState::isEntailed(Node n, bool polarity) const
+{
+ if (n.getKind() == NOT)
+ {
+ return isEntailed(n[0], !polarity);
+ }
+ else if (n.getKind() == EQUAL)
+ {
+ if (polarity)
+ {
+ return areEqual(n[0], n[1]);
+ }
+ return areDisequal(n[0], n[1]);
+ }
+ else if (n.getKind() == MEMBER)
+ {
+ if (areEqual(n, polarity ? d_true : d_false))
+ {
+ return true;
+ }
+ // check members cache
+ if (polarity && d_ee.hasTerm(n[1]))
+ {
+ Node r = d_ee.getRepresentative(n[1]);
+ if (d_parent.isMember(n[0], r))
+ {
+ return true;
+ }
+ }
+ }
+ else if (n.getKind() == AND || n.getKind() == OR)
+ {
+ bool conj = (n.getKind() == AND) == polarity;
+ for (const Node& nc : n)
+ {
+ bool isEnt = isEntailed(nc, polarity);
+ if (isEnt != conj)
+ {
+ return !conj;
+ }
+ }
+ return conj;
+ }
+ else if (n.isConst())
+ {
+ return (polarity && n == d_true) || (!polarity && n == d_false);
+ }
+ return false;
+}
+
+bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
+{
+ Assert(d_ee.hasTerm(r1) && d_ee.getRepresentative(r1) == r1);
+ Assert(d_ee.hasTerm(r2) && d_ee.getRepresentative(r2) == r2);
+ TypeNode tn = r1.getType();
+ Node re = getEmptySetEqClass(tn);
+ for (unsigned e = 0; e < 2; e++)
+ {
+ Node a = e == 0 ? r1 : r2;
+ Node b = e == 0 ? r2 : r1;
+ if (isSetDisequalityEntailedInternal(a, b, re))
+ {
+ return true;
+ }
+ }
+ return false;
+}
+
+bool SolverState::isSetDisequalityEntailedInternal(Node a,
+ Node b,
+ Node re) const
+{
+ // if there are members in a
+ std::map<Node, std::map<Node, Node> >::const_iterator itpma =
+ d_pol_mems[0].find(a);
+ if (itpma == d_pol_mems[0].end())
+ {
+ // no positive members, continue
+ return false;
+ }
+ // if b is empty
+ if (b == re)
+ {
+ if (!itpma->second.empty())
+ {
+ Trace("sets-deq") << "Disequality is satisfied because members are in "
+ << a << " and " << b << " is empty" << std::endl;
+ return true;
+ }
+ else
+ {
+ // a should not be singleton
+ Assert(d_eqc_singleton.find(a) == d_eqc_singleton.end());
+ }
+ return false;
+ }
+ std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
+ std::map<Node, std::map<Node, Node> >::const_iterator itpmb =
+ d_pol_mems[1].find(b);
+ std::vector<Node> prev;
+ for (const std::pair<const Node, Node>& itm : itpma->second)
+ {
+ // if b is a singleton
+ if (itsb != d_eqc_singleton.end())
+ {
+ if (areDisequal(itm.first, itsb->second[0]))
+ {
+ Trace("sets-deq") << "Disequality is satisfied because of "
+ << itm.second << ", singleton eq " << itsb->second[0]
+ << std::endl;
+ return true;
+ }
+ // or disequal with another member
+ for (const Node& p : prev)
+ {
+ if (areDisequal(itm.first, p))
+ {
+ Trace("sets-deq")
+ << "Disequality is satisfied because of disequal members "
+ << itm.first << " " << p << ", singleton eq " << std::endl;
+ return true;
+ }
+ }
+ // if a has positive member that is negative member in b
+ }
+ else if (itpmb != d_pol_mems[1].end())
+ {
+ for (const std::pair<const Node, Node>& itnm : itpmb->second)
+ {
+ if (areEqual(itm.first, itnm.first))
+ {
+ Trace("sets-deq") << "Disequality is satisfied because of "
+ << itm.second << " " << itnm.second << std::endl;
+ return true;
+ }
+ }
+ }
+ prev.push_back(itm.first);
+ }
+ return false;
+}
+
+Node SolverState::getProxy(Node n)
+{
+ Kind nk = n.getKind();
+ if (nk != EMPTYSET && nk != SINGLETON && nk != INTERSECTION && nk != SETMINUS
+ && nk != UNION)
+ {
+ return n;
+ }
+ NodeMap::const_iterator it = d_proxy.find(n);
+ if (it != d_proxy.end())
+ {
+ return (*it).second;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ Node k = nm->mkSkolem("sp", n.getType(), "proxy for set");
+ d_proxy[n] = k;
+ d_proxy_to_term[k] = n;
+ Node eq = k.eqNode(n);
+ Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
+ d_parent.getOutputChannel()->lemma(eq);
+ if (nk == SINGLETON)
+ {
+ Node slem = nm->mkNode(MEMBER, n[0], k);
+ Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton"
+ << std::endl;
+ d_parent.getOutputChannel()->lemma(slem);
+ }
+ return k;
+}
+
+Node SolverState::getCongruent(Node n) const
+{
+ Assert(d_ee.hasTerm(n));
+ std::map<Node, Node>::const_iterator it = d_congruent.find(n);
+ if (it == d_congruent.end())
+ {
+ return n;
+ }
+ return it->second;
+}
+bool SolverState::isCongruent(Node n) const
+{
+ return d_congruent.find(n) != d_congruent.end();
+}
+
+Node SolverState::getEmptySet(TypeNode tn)
+{
+ std::map<TypeNode, Node>::iterator it = d_emptyset.find(tn);
+ if (it != d_emptyset.end())
+ {
+ return it->second;
+ }
+ Node n = NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
+ d_emptyset[tn] = n;
+ return n;
+}
+Node SolverState::getUnivSet(TypeNode tn)
+{
+ std::map<TypeNode, Node>::iterator it = d_univset.find(tn);
+ if (it != d_univset.end())
+ {
+ return it->second;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ Node n = nm->mkNullaryOperator(tn, UNIVERSE_SET);
+ for (it = d_univset.begin(); it != d_univset.end(); ++it)
+ {
+ Node n1;
+ Node n2;
+ if (tn.isSubtypeOf(it->first))
+ {
+ n1 = n;
+ n2 = it->second;
+ }
+ else if (it->first.isSubtypeOf(tn))
+ {
+ n1 = it->second;
+ n2 = n;
+ }
+ if (!n1.isNull())
+ {
+ Node ulem = nm->mkNode(SUBSET, n1, n2);
+ Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type"
+ << std::endl;
+ d_parent.getOutputChannel()->lemma(ulem);
+ }
+ }
+ d_univset[tn] = n;
+ return n;
+}
+
+Node SolverState::getTypeConstraintSkolem(Node n, TypeNode tn)
+{
+ std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
+ if (it == d_tc_skolem[n].end())
+ {
+ Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn);
+ d_tc_skolem[n][tn] = k;
+ return k;
+ }
+ return it->second;
+}
+
+const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
+{
+ std::map<Node, std::vector<Node> >::const_iterator it = d_nvar_sets.find(r);
+ if (it == d_nvar_sets.end())
+ {
+ return d_emptyVec;
+ }
+ return it->second;
+}
+
+Node SolverState::getVariableSet(Node r) const
+{
+ std::map<Node, Node>::const_iterator it = d_var_set.find(r);
+ if (it != d_var_set.end())
+ {
+ return it->second;
+ }
+ return Node::null();
+}
+const std::map<Node, Node>& SolverState::getMembers(Node r) const
+{
+ return getMembersInternal(r, 0);
+}
+const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
+{
+ return getMembersInternal(r, 1);
+}
+const std::map<Node, Node>& SolverState::getMembersInternal(Node r,
+ unsigned i) const
+{
+ std::map<Node, std::map<Node, Node> >::const_iterator itp =
+ d_pol_mems[i].find(r);
+ if (itp == d_pol_mems[i].end())
+ {
+ return d_emptyMap;
+ }
+ return itp->second;
+}
+
+bool SolverState::hasMembers(Node r) const
+{
+ std::map<Node, std::map<Node, Node> >::const_iterator it =
+ d_pol_mems[0].find(r);
+ if (it == d_pol_mems[0].end())
+ {
+ return false;
+ }
+ return !it->second.empty();
+}
+const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
+SolverState::getBinaryOpIndex() const
+{
+ return d_bop_index;
+}
+const std::map<Kind, std::vector<Node> >& SolverState::getOperatorList() const
+{
+ return d_op_list;
+}
+
+void SolverState::debugPrintSet(Node s, const char* c) const
+{
+ if (s.getNumChildren() == 0)
+ {
+ NodeMap::const_iterator it = d_proxy_to_term.find(s);
+ if (it != d_proxy_to_term.end())
+ {
+ debugPrintSet((*it).second, c);
+ }
+ else
+ {
+ Trace(c) << s;
+ }
+ }
+ else
+ {
+ Trace(c) << "(" << s.getOperator();
+ for (const Node& sc : s)
+ {
+ Trace(c) << " ";
+ debugPrintSet(sc, c);
+ }
+ Trace(c) << ")";
+ }
+}
+
+} // namespace sets
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file solver_state.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Sets state object
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H
+#define CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashset.h"
+#include "theory/sets/skolem_cache.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsPrivate;
+
+/** Sets state
+ *
+ * The purpose of this class is to:
+ * (1) Maintain information concerning the current set of assertions during a
+ * full effort check,
+ * (2) Maintain a database of commonly used terms.
+ *
+ * During a full effort check, the solver for theory of sets should call:
+ * reset; ( registerEqc | registerTerm )*
+ * to initialize the information in this class regarding full effort checks.
+ * Other query calls are then valid for the remainder of the full effort check.
+ */
+class SolverState
+{
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+
+ public:
+ SolverState(TheorySetsPrivate& p,
+ eq::EqualityEngine& e,
+ context::Context* c,
+ context::UserContext* u);
+ //-------------------------------- initialize
+ /** reset, clears the data structures maintained by this class. */
+ void reset();
+ /** register equivalence class whose type is tn */
+ void registerEqc(TypeNode tn, Node r);
+ /** register term n of type tnn in the equivalence class of r */
+ void registerTerm(Node r, TypeNode tnn, Node n);
+ //-------------------------------- end initialize
+ /** Are we currently in conflict? */
+ bool isInConflict() const { return d_conflict; }
+ /**
+ * Indicate that we are in conflict, without a conflict clause. This is
+ * called, for instance, when we have propagated a conflicting literal.
+ */
+ void setConflict();
+ /** Set conf is a conflict node to be sent on the output channel. */
+ void setConflict(Node conf);
+ /** Is a=b according to equality reasoning in the current context? */
+ bool areEqual(Node a, Node b) const;
+ /** Is a!=b according to equality reasoning in the current context? */
+ bool areDisequal(Node a, Node b) const;
+ /** add equality to explanation
+ *
+ * This adds a = b to exp if a and b are syntactically disequal. The equality
+ * a = b should hold in the current context.
+ */
+ void addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const;
+ /** Is formula n entailed to have polarity pol in the current context? */
+ bool isEntailed(Node n, bool pol) const;
+ /**
+ * Is the disequality between sets s and t entailed in the current context?
+ */
+ bool isSetDisequalityEntailed(Node s, Node t) const;
+ /**
+ * Get the equivalence class of the empty set of type tn, or null if it does
+ * not exist as a term in the current context.
+ */
+ Node getEmptySetEqClass(TypeNode tn) const;
+ /**
+ * Get the equivalence class of the universe set of type tn, or null if it
+ * does not exist as a term in the current context.
+ */
+ Node getUnivSetEqClass(TypeNode tn) const;
+ /**
+ * Get the singleton set in the equivalence class of representative r if it
+ * exists, or null if none exists.
+ */
+ Node getSingletonEqClass(Node r) const;
+ /** get binary operator term (modulo equality)
+ *
+ * This method returns a non-null node n if and only if a term n that is
+ * congruent to <k>(r1,r2) exists in the current context.
+ */
+ Node getBinaryOpTerm(Kind k, Node r1, Node r2) const;
+ /**
+ * Returns a term that is congruent to n in the current context.
+ *
+ * To ensure that inferences and processing is not redundant,
+ * this class computes congruence over all terms that exist in the current
+ * context. If a set of terms f( t1 ), ... f( tn ) are pairwise congruent
+ * (call this a "congruence class"), it selects one of these terms as a
+ * representative. All other terms return the representative term from
+ * its congruence class.
+ */
+ Node getCongruent(Node n) const;
+ /**
+ * This method returns true if n is not the representative of its congruence
+ * class.
+ */
+ bool isCongruent(Node n) const;
+ /** Get the list of all equivalence classes of set type */
+ const std::vector<Node>& getSetsEqClasses() const { return d_set_eqc; }
+ /**
+ * Get the list of non-variable sets that exists in the equivalence class
+ * whose representative is r.
+ */
+ const std::vector<Node>& getNonVariableSets(Node r) const;
+ /**
+ * Get a variable set in the equivalence class with representative r, or null
+ * if none exist.
+ */
+ Node getVariableSet(Node r) const;
+ /** Get (positive) members of the set equivalence class r
+ *
+ * The members are return as a map, which maps members to their explanation.
+ * For example, if x = y, (member 5 y), (member 6 x), then getMembers(x)
+ * returns the map [ 5 -> (member 5 y), 6 -> (member 6 x)].
+ */
+ const std::map<Node, Node>& getMembers(Node r) const;
+ /** Get negative members of the set equivalence class r, similar to above */
+ const std::map<Node, Node>& getNegativeMembers(Node r) const;
+ /** Is the (positive) members list of set equivalence class r non-empty? */
+ bool hasMembers(Node r) const;
+ /** Get binary operator index
+ *
+ * This returns a mapping from binary operator kinds (INTERSECT, SETMINUS,
+ * UNION) to index of terms of that kind. Each kind k maps to a map whose
+ * entries are of the form [r1 -> r2 -> t], where t is a term in the current
+ * context, and t is of the form <k>(t1,t2) where t1=r1 and t2=r2 hold in the
+ * current context. The term t is the representative of its congruence class.
+ */
+ const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
+ getBinaryOpIndex() const;
+ /** get operator list
+ *
+ * This returns a mapping from set kinds to a list of terms of that kind
+ * that exist in the current context. Each of the terms in the range of this
+ * map is a representative of its congruence class.
+ */
+ const std::map<Kind, std::vector<Node> >& getOperatorList() const;
+
+ // --------------------------------------- commonly used terms
+ /** Get type constraint skolem
+ *
+ * The sets theory solver outputs equality lemmas of the form:
+ * n = d_tc_skolem[n][tn]
+ * where the type of d_tc_skolem[n][tn] is tn, and the type
+ * of n is not a subtype of tn. This is required to handle benchmarks like
+ * test/regress/regress0/sets/sets-of-sets-subtypes.smt2
+ * where for s : (Set Int) and t : (Set Real), we have that
+ * ( s = t ^ y in t ) implies ( exists k : Int. y = k )
+ * The type constraint Skolem for (y, Int) is the skolemization of k above.
+ */
+ Node getTypeConstraintSkolem(Node n, TypeNode tn);
+ /** get the proxy variable for set n
+ *
+ * Proxy variables are used to communicate information that otherwise would
+ * not be possible due to rewriting. For example, the literal
+ * card( singleton( 0 ) ) = 1
+ * is rewritten to true. Instead, to communicate this fact (e.g. to other
+ * theories), we require introducing a proxy variable x for singleton( 0 ).
+ * Then:
+ * card( x ) = 1 ^ x = singleton( 0 )
+ * communicates the equivalent of the above literal.
+ */
+ Node getProxy(Node n);
+ /** Get the empty set of type tn */
+ Node getEmptySet(TypeNode tn);
+ /** Get the universe set of type tn */
+ Node getUnivSet(TypeNode tn);
+ /**
+ * Get the skolem cache of this theory, which manages a database of introduced
+ * skolem variables used for various inferences.
+ */
+ SkolemCache& getSkolemCache() { return d_skCache; }
+ // --------------------------------------- end commonly used terms
+ /** debug print set */
+ void debugPrintSet(Node s, const char* c) const;
+
+ private:
+ /** constants */
+ Node d_true;
+ Node d_false;
+ /** the empty vector and map */
+ std::vector<Node> d_emptyVec;
+ std::map<Node, Node> d_emptyMap;
+ /** Whether or not we are in conflict. This flag is SAT context dependent. */
+ context::CDO<bool> d_conflict;
+ /** Reference to the parent theory of sets */
+ TheorySetsPrivate& d_parent;
+ /** Reference to the equality engine of theory of sets */
+ eq::EqualityEngine& d_ee;
+ /** The list of all equivalence classes of type set in the current context */
+ std::vector<Node> d_set_eqc;
+ /** Maps types to the equivalence class containing empty set of that type */
+ std::map<TypeNode, Node> d_eqc_emptyset;
+ /** Maps types to the equivalence class containing univ set of that type */
+ std::map<TypeNode, Node> d_eqc_univset;
+ /** Maps equivalence classes to a singleton set that exists in it. */
+ std::map<Node, Node> d_eqc_singleton;
+ /** Map from terms to the representative of their congruence class */
+ std::map<Node, Node> d_congruent;
+ /** Map from equivalence classes to the list of non-variable sets in it */
+ std::map<Node, std::vector<Node> > d_nvar_sets;
+ /** Map from equivalence classes to a variable sets in it */
+ std::map<Node, Node> d_var_set;
+ /** polarity memberships
+ *
+ * d_pol_mems[0] maps equivalence class to their positive membership list
+ * with explanations (see getMembers), d_pol_mems[1] maps equivalence classes
+ * to their negative memberships.
+ */
+ std::map<Node, std::map<Node, Node> > d_pol_mems[2];
+ // --------------------------------------- commonly used terms
+ /** Map from set terms to their proxy variables */
+ NodeMap d_proxy;
+ /** Backwards map of above */
+ NodeMap d_proxy_to_term;
+ /** Cache of type constraint skolems (see getTypeConstraintSkolem) */
+ std::map<Node, std::map<TypeNode, Node> > d_tc_skolem;
+ /** Map from types to empty set of that type */
+ std::map<TypeNode, Node> d_emptyset;
+ /** Map from types to universe set of that type */
+ std::map<TypeNode, Node> d_univset;
+ // --------------------------------------- end commonly used terms
+ // -------------------------------- term indices
+ /** Term index for MEMBER
+ *
+ * A term index maps equivalence class representatives to the representative
+ * of their congruence class.
+ *
+ * For example, the term index for member may contain an entry
+ * [ r1 -> r2 -> (member t1 t2) ] where r1 and r2 are representatives of their
+ * equivalence classes, (member t1 t2) is the representative of its congruence
+ * class, and r1=t1 and r2=t2 hold in the current context.
+ */
+ std::map<Node, std::map<Node, Node> > d_members_index;
+ /** Term index for SINGLETON */
+ std::map<Node, Node> d_singleton_index;
+ /** Indices for the binary kinds INTERSECT, SETMINUS and UNION. */
+ std::map<Kind, std::map<Node, std::map<Node, Node> > > d_bop_index;
+ // -------------------------------- end term indices
+ std::map<Kind, std::vector<Node> > d_op_list;
+ /** the skolem cache */
+ SkolemCache d_skCache;
+ /** is set disequality entailed internal
+ *
+ * This returns true if disequality between sets a and b is entailed in the
+ * current context. We use an incomplete test based on equality and membership
+ * information.
+ *
+ * re is the representative of the equivalence class of the empty set
+ * whose type is the same as a and b.
+ */
+ bool isSetDisequalityEntailedInternal(Node a, Node b, Node re) const;
+ /**
+ * Get members internal, returns the positive members if i=0, or negative
+ * members if i=1.
+ */
+ const std::map<Node, Node>& getMembersInternal(Node r, unsigned i) const;
+}; /* class TheorySetsPrivate */
+
+} // namespace sets
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H */
d_internal->check(e);
}
-bool TheorySets::needsCheckLastEffort() {
- return d_internal->needsCheckLastEffort();
-}
-
bool TheorySets::collectModelInfo(TheoryModel* m)
{
return d_internal->collectModelInfo(m);
void addSharedTerm(TNode) override;
void check(Effort) override;
- bool needsCheckLastEffort() override;
bool collectModelInfo(TheoryModel* m) override;
void computeCareGraph() override;
Node explain(TNode) override;
d_deq(c),
d_deq_processed(u),
d_keep(c),
- d_sentLemma(false),
- d_addedFact(false),
d_full_check_incomplete(false),
- d_proxy(u),
- d_proxy_to_term(u),
- d_lemmas_produced(u),
- d_card_enabled(false),
- d_card_processed(u),
- d_var_elim(u),
d_external(external),
d_notify(*this),
d_equalityEngine(d_notify, c, "theory::sets::ee", true),
- d_conflict(c),
- d_rels(new TheorySetsRels(c, u, &d_equalityEngine, *this)),
- d_rels_enabled(false)
+ d_state(*this, d_equalityEngine, c, u),
+ d_im(*this, d_state, d_equalityEngine, c, u),
+ d_rels(new TheorySetsRels(d_state, d_im, d_equalityEngine, u)),
+ d_cardSolver(
+ new CardinalityExtension(d_state, d_im, d_equalityEngine, c, u)),
+ d_rels_enabled(false),
+ d_card_enabled(false)
{
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
d_equalityEngine.addFunctionKind(kind::MEMBER);
d_equalityEngine.addFunctionKind(kind::SUBSET);
-
- d_equalityEngine.addFunctionKind(kind::CARD);
}
TheorySetsPrivate::~TheorySetsPrivate(){
}
void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
- if( !d_conflict ){
+ if (!d_state.isInConflict())
+ {
Trace("sets-prop-debug") << "Merge " << t1 << " and " << t2 << "..." << std::endl;
Node s1, s2;
EqcInfo * e2 = getOrMakeEqcInfo( t2 );
bool add = true;
for( int j=0; j<n_members; j++ ){
Assert( j<(int)d_members_data[t1].size() && d_members_data[t1][j].getKind()==kind::MEMBER );
- if( ee_areEqual( m2[0], d_members_data[t1][j][0] ) ){
+ if (d_state.areEqual(m2[0], d_members_data[t1][j][0]))
+ {
add = false;
break;
}
if( add ){
if( !s1.isNull() && s2.isNull() ){
Assert( m2[1].getType().isComparableTo( s1.getType() ) );
- Assert( ee_areEqual( m2[1], s1 ) );
+ Assert(d_state.areEqual(m2[1], s1));
Node exp = NodeManager::currentNM()->mkNode( kind::AND, m2[1].eqNode( s1 ), m2 );
if( s1.getKind()==kind::SINGLETON ){
if( s1[0]!=m2[0] ){
}else{
//conflict
Trace("sets-prop") << "Propagate eq-mem conflict : " << exp << std::endl;
- d_conflict = true;
- d_external.d_out->conflict( exp );
+ d_state.setConflict(exp);
return;
}
}
}
}
-
-bool TheorySetsPrivate::ee_areEqual( Node a, Node b ) {
- if( a==b ){
- return true;
- }else{
- if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
- return d_equalityEngine.areEqual( a, b );
- }else{
- return false;
- }
- }
-}
-
-bool TheorySetsPrivate::ee_areDisequal( Node a, Node b ) {
- if( a==b ){
- return false;
- }else{
- if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
- return d_equalityEngine.areDisequal( a, b, false );
- }else{
- return a.isConst() && b.isConst();
- }
- }
-}
-
-bool TheorySetsPrivate::ee_areCareDisequal( Node a, Node b ) {
+bool TheorySetsPrivate::areCareDisequal(Node a, Node b)
+{
if( d_equalityEngine.isTriggerTerm(a, THEORY_SETS) && d_equalityEngine.isTriggerTerm(b, THEORY_SETS) ){
TNode a_shared = d_equalityEngine.getTriggerTermRepresentative(a, THEORY_SETS);
TNode b_shared = d_equalityEngine.getTriggerTermRepresentative(b, THEORY_SETS);
return false;
}
-bool TheorySetsPrivate::isEntailed( Node n, bool polarity ) {
- if( n.getKind()==kind::NOT ){
- return isEntailed( n[0], !polarity );
- }else if( n.getKind()==kind::EQUAL ){
- if( polarity ){
- return ee_areEqual( n[0], n[1] );
- }else{
- return ee_areDisequal( n[0], n[1] );
- }
- }else if( n.getKind()==kind::MEMBER ){
- if( ee_areEqual( n, polarity ? d_true : d_false ) ){
- return true;
- }
- //check members cache
- if( polarity && d_equalityEngine.hasTerm( n[1] ) ){
- Node r = d_equalityEngine.getRepresentative( n[1] );
- if( isMember( n[0], r ) ){
- return true;
- }
- }
- }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
- bool conj = (n.getKind()==kind::AND)==polarity;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- bool isEnt = isEntailed( n[i], polarity );
- if( isEnt!=conj ){
- return !conj;
- }
- }
- return conj;
- }else if( n.isConst() ){
- return ( polarity && n==d_true ) || ( !polarity && n==d_false );
- }
- return false;
-}
-
bool TheorySetsPrivate::isMember( Node x, Node s ) {
Assert( d_equalityEngine.hasTerm( s ) && d_equalityEngine.getRepresentative( s )==s );
NodeIntMap::iterator mem_i = d_members.find( s );
if( mem_i != d_members.end() ) {
for( int i=0; i<(*mem_i).second; i++ ){
- if( ee_areEqual( d_members_data[s][i][0], x ) ){
+ if (d_state.areEqual(d_members_data[s][i][0], x))
+ {
return true;
}
}
}
return false;
}
-
-bool TheorySetsPrivate::isSetDisequalityEntailed( Node r1, Node r2 ) {
- Assert( d_equalityEngine.hasTerm( r1 ) && d_equalityEngine.getRepresentative( r1 )==r1 );
- Assert( d_equalityEngine.hasTerm( r2 ) && d_equalityEngine.getRepresentative( r2 )==r2 );
- TypeNode tn = r1.getType();
- Node eqc_es = d_eqc_emptyset[tn];
- bool is_sat = false;
- for( unsigned e=0; e<2; e++ ){
- Node a = e==0 ? r1 : r2;
- Node b = e==0 ? r2 : r1;
- //if there are members in a
- std::map< Node, std::map< Node, Node > >::iterator itpma = d_pol_mems[0].find( a );
- if( itpma!=d_pol_mems[0].end() ){
- Assert( !itpma->second.empty() );
- //if b is empty
- if( b==eqc_es ){
- if( !itpma->second.empty() ){
- is_sat = true;
- Trace("sets-deq") << "Disequality is satisfied because members are in " << a << " and " << b << " is empty" << std::endl;
- }else{
- //a should not be singleton
- Assert( d_eqc_singleton.find( a )==d_eqc_singleton.end() );
- }
- }else{
- std::map< Node, Node >::iterator itsb = d_eqc_singleton.find( b );
- std::map< Node, std::map< Node, Node > >::iterator itpmb = d_pol_mems[1].find( b );
- std::vector< Node > prev;
- for( std::map< Node, Node >::iterator itm = itpma->second.begin(); itm != itpma->second.end(); ++itm ){
- //if b is a singleton
- if( itsb!=d_eqc_singleton.end() ){
- if( ee_areDisequal( itm->first, itsb->second[0] ) ){
- Trace("sets-deq") << "Disequality is satisfied because of " << itm->second << ", singleton eq " << itsb->second[0] << std::endl;
- is_sat = true;
- }
- //or disequal with another member
- for( unsigned k=0; k<prev.size(); k++ ){
- if( ee_areDisequal( itm->first, prev[k] ) ){
- Trace("sets-deq") << "Disequality is satisfied because of disequal members " << itm->first << " " << prev[k] << ", singleton eq " << std::endl;
- is_sat = true;
- break;
- }
- }
- //TODO: this can be generalized : maintain map to abstract domain ( set -> cardinality )
- //if a has positive member that is negative member in b
- }else if( itpmb!=d_pol_mems[1].end() ){
- for( std::map< Node, Node >::iterator itnm = itpmb->second.begin(); itnm != itpmb->second.end(); ++itnm ){
- if( ee_areEqual( itm->first, itnm->first ) ){
- Trace("sets-deq") << "Disequality is satisfied because of " << itm->second << " " << itnm->second << std::endl;
- is_sat = true;
- break;
- }
- }
- }
- if( is_sat ){
- break;
- }
- prev.push_back( itm->first );
- }
- }
- if( is_sat ){
- break;
- }
- }
- }
- return is_sat;
-}
bool TheorySetsPrivate::assertFact( Node fact, Node exp ){
Trace("sets-assert") << "TheorySets::assertFact : " << fact << ", exp = " << exp << std::endl;
bool polarity = fact.getKind() != kind::NOT;
TNode atom = polarity ? fact : fact[0];
- if( !isEntailed( atom, polarity ) ){
+ if (!d_state.isEntailed(atom, polarity))
+ {
if( atom.getKind()==kind::EQUAL ){
d_equalityEngine.assertEquality( atom, polarity, exp );
}else{
d_equalityEngine.assertPredicate( atom, polarity, exp );
}
- if( !d_conflict ){
+ if (!d_state.isInConflict())
+ {
if( atom.getKind()==kind::MEMBER && polarity ){
//check if set has a value, if so, we can propagate
Node r = d_equalityEngine.getRepresentative( atom[1] );
}
}else{
Trace("sets-prop") << "Propagate mem-eq conflict : " << exp << std::endl;
- d_conflict = true;
- d_external.d_out->conflict( exp );
+ d_state.setConflict(exp);
}
}
}
}
}
return true;
- }else{
- return false;
}
-}
-
-bool TheorySetsPrivate::assertFactRec( Node fact, Node exp, std::vector< Node >& lemma, int inferType ) {
- if( ( options::setsInferAsLemmas() && inferType!=-1 ) || inferType==1 ){
- if( !isEntailed( fact, true ) ){
- lemma.push_back( exp==d_true ? fact : NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, fact ) );
- return true;
- }
- }else{
- Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp << std::endl;
- if( fact.isConst() ){
- //either trivial or a conflict
- if( fact==d_false ){
- Trace("sets-lemma") << "Conflict : " << exp << std::endl;
- d_conflict = true;
- d_external.d_out->conflict( exp );
- return true;
- }
- }else if( fact.getKind()==kind::AND || ( fact.getKind()==kind::NOT && fact[0].getKind()==kind::OR ) ){
- bool ret = false;
- Node f = fact.getKind()==kind::NOT ? fact[0] : fact;
- for( unsigned i=0; i<f.getNumChildren(); i++ ){
- Node factc = fact.getKind()==kind::NOT ? f[i].negate() : f[i];
- bool tret = assertFactRec( factc, exp, lemma, inferType );
- ret = ret || tret;
- if( d_conflict ){
- return true;
- }
- }
- return ret;
- }else{
- bool polarity = fact.getKind() != kind::NOT;
- TNode atom = polarity ? fact : fact[0];
- //things we can assert to equality engine
- if( atom.getKind()==kind::MEMBER || ( atom.getKind()==kind::EQUAL && atom[0].getType().isSet() ) ){
- //send to equality engine
- if( assertFact( fact, exp ) ){
- d_addedFact = true;
- return true;
- }
- }else{
- if( !isEntailed( fact, true ) ){
- //must send as lemma
- lemma.push_back( exp==d_true ? fact : NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, fact ) );
- return true;
- }
- }
- }
- }
- return false;
-}
-void TheorySetsPrivate::assertInference( Node fact, Node exp, std::vector< Node >& lemmas, const char * c, int inferType ) {
- d_keep.insert( exp );
- d_keep.insert( fact );
- if( assertFactRec( fact, exp, lemmas, inferType ) ){
- Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by " << c << std::endl;
- Trace("sets-assertion") << "(assert (=> " << exp << " " << fact << ")) ; by " << c << std::endl;
- }
-}
-
-void TheorySetsPrivate::assertInference( Node fact, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType ){
- Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ) );
- assertInference( fact, exp_n, lemmas, c, inferType );
-}
-
-void TheorySetsPrivate::assertInference( std::vector< Node >& conc, Node exp, std::vector< Node >& lemmas, const char * c, int inferType ){
- if( !conc.empty() ){
- Node fact = conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::AND, conc );
- assertInference( fact, exp, lemmas, c, inferType );
+ else
+ {
+ return false;
}
}
-void TheorySetsPrivate::assertInference( std::vector< Node >& conc, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType ) {
- Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ) );
- assertInference( conc, exp_n, lemmas, c, inferType );
-}
-void TheorySetsPrivate::split( Node n, int reqPol ) {
- n = Rewriter::rewrite( n );
- Node lem = NodeManager::currentNM()->mkNode( kind::OR, n, n.negate() );
- std::vector< Node > lemmas;
- lemmas.push_back( lem );
- flushLemmas( lemmas );
- Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
- if( reqPol!=0 ){
- Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol>0) << std::endl;
- d_external.getOutputChannel().requirePhase( n, reqPol>0 );
- }
+void TheorySetsPrivate::fullEffortReset()
+{
+ Assert(d_equalityEngine.consistent());
+ d_full_check_incomplete = false;
+ d_most_common_type.clear();
+ d_most_common_type_term.clear();
+ d_card_enabled = false;
+ d_rels_enabled = false;
+ // reset the state object
+ d_state.reset();
+ // reset the inference manager
+ d_im.reset();
+ // reset the cardinality solver
+ d_cardSolver->reset();
}
void TheorySetsPrivate::fullEffortCheck(){
Trace("sets") << "----- Full effort check ------" << std::endl;
do{
Trace("sets") << "...iterate full effort check..." << std::endl;
- Assert( d_equalityEngine.consistent() );
- d_sentLemma = false;
- d_addedFact = false;
- d_full_check_incomplete = false;
- d_set_eqc.clear();
- d_set_eqc_list.clear();
- d_eqc_emptyset.clear();
- d_eqc_univset.clear();
- d_eqc_singleton.clear();
- d_congruent.clear();
- d_nvar_sets.clear();
- d_var_set.clear();
- d_most_common_type.clear();
- d_most_common_type_term.clear();
- d_pol_mems[0].clear();
- d_pol_mems[1].clear();
- d_members_index.clear();
- d_singleton_index.clear();
- d_bop_index.clear();
- d_op_list.clear();
- d_card_enabled = false;
- d_t_card_enabled.clear();
- d_rels_enabled = false;
- d_eqc_to_card_term.clear();
-
- std::vector< Node > lemmas;
+ fullEffortReset();
+
Trace("sets-eqc") << "Equality Engine:" << std::endl;
std::map<TypeNode, unsigned> eqcTypeCount;
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
Node eqc = (*eqcs_i);
bool isSet = false;
TypeNode tn = eqc.getType();
+ d_state.registerEqc(tn, eqc);
eqcTypeCount[tn]++;
//common type node and term
TypeNode tnc;
Node tnct;
if( tn.isSet() ){
isSet = true;
- d_set_eqc.push_back( eqc );
tnc = tn.getSetElementType();
tnct = eqc;
}
tnct = n;
}
}
- if( n.getKind()==kind::MEMBER ){
- if( eqc.isConst() ){
- Node s = d_equalityEngine.getRepresentative( n[1] );
- Node x = d_equalityEngine.getRepresentative( n[0] );
- int pindex = eqc==d_true ? 0 : ( eqc==d_false ? 1 : -1 );
- if( pindex!=-1 ){
- if( d_pol_mems[pindex][s].find( x )==d_pol_mems[pindex][s].end() ){
- d_pol_mems[pindex][s][x] = n;
- Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n << ", pindex = " << pindex << std::endl;
- }
- if( d_members_index[s].find( x )==d_members_index[s].end() ){
- d_members_index[s][x] = n;
- d_op_list[kind::MEMBER].push_back( n );
- }
- }else{
- Assert( false );
- }
- }
- }else if( n.getKind()==kind::SINGLETON || n.getKind()==kind::UNION || n.getKind()==kind::INTERSECTION ||
- n.getKind()==kind::SETMINUS || n.getKind()==kind::EMPTYSET || n.getKind()==kind::UNIVERSE_SET ){
- if( n.getKind()==kind::SINGLETON ){
- //singleton lemma
- getProxy( n );
- Node r = d_equalityEngine.getRepresentative( n[0] );
- if( d_singleton_index.find( r )==d_singleton_index.end() ){
- d_singleton_index[r] = n;
- d_eqc_singleton[eqc] = n;
- d_op_list[kind::SINGLETON].push_back( n );
- }else{
- d_congruent[n] = d_singleton_index[r];
- }
- }else if( n.getKind()==kind::EMPTYSET ){
- d_eqc_emptyset[tnn] = eqc;
- }else if( n.getKind()==kind::UNIVERSE_SET ){
- Assert( options::setsExt() );
- d_eqc_univset[tnn] = eqc;
- }else{
- Node r1 = d_equalityEngine.getRepresentative( n[0] );
- Node r2 = d_equalityEngine.getRepresentative( n[1] );
- std::map<Node, Node>& binr1 = d_bop_index[n.getKind()][r1];
- std::map<Node, Node>::iterator itb = binr1.find(r2);
- if (itb == binr1.end())
- {
- binr1[r2] = n;
- d_op_list[n.getKind()].push_back( n );
- }else{
- d_congruent[n] = itb->second;
- }
- }
- d_nvar_sets[eqc].push_back( n );
- Trace("sets-debug2") << "Non-var-set[" << eqc << "] : " << n << std::endl;
- d_set_eqc_list[eqc].push_back( n );
- }else if( n.getKind()==kind::CARD ){
+ // register it with the state
+ d_state.registerTerm(eqc, tnn, n);
+ if (n.getKind() == kind::CARD)
+ {
d_card_enabled = true;
- TypeNode tnc = n[0].getType().getSetElementType();
- d_t_card_enabled[tnc] = true;
- if( tnc.isInterpretedFinite() ){
- std::stringstream ss;
- ss << "ERROR: cannot use cardinality on sets with finite element "
- "type (term is "
- << n << ")." << std::endl;
- throw LogicException(ss.str());
- //TODO: extend approach for this case
- }
+ // register it with the cardinality solver
+ d_cardSolver->registerTerm(n);
// if we do not handle the kind, set incomplete
Kind nk = n[0].getKind();
+ // some kinds of cardinality we cannot handle
if (nk == kind::UNIVERSE_SET || d_rels->isRelationKind(nk))
{
d_full_check_incomplete = true;
Trace("sets-incomplete")
<< "Sets : incomplete because of " << n << "." << std::endl;
+ // TODO (#1124) handle this case
}
- Node r = d_equalityEngine.getRepresentative( n[0] );
- if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){
- d_eqc_to_card_term[ r ] = n;
- registerCardinalityTerm( n[0], lemmas );
- }
- }else{
+ }
+ else
+ {
if( d_rels->isRelationKind( n.getKind() ) ){
d_rels_enabled = true;
}
- if( isSet ){
- d_set_eqc_list[eqc].push_back( n );
- if( n.getKind()==kind::VARIABLE ){
- if( d_var_set.find( eqc )==d_var_set.end() ){
- d_var_set[eqc] = n;
- }
- }
- }
}
++eqc_i;
}
++eqcs_i;
}
+ Trace("sets-eqc") << "...finished equality engine." << std::endl;
+
if (Trace.isOn("sets-state"))
{
Trace("sets-state") << "Equivalence class counters:" << std::endl;
}
}
- flushLemmas( lemmas );
- if( !hasProcessed() ){
+ // We may have sent lemmas while registering the terms in the loop above,
+ // e.g. the cardinality solver.
+ if (!d_im.hasProcessed())
+ {
if( Trace.isOn("sets-mem") ){
- for( unsigned i=0; i<d_set_eqc.size(); i++ ){
- Node s = d_set_eqc[i];
+ const std::vector<Node>& sec = d_state.getSetsEqClasses();
+ for (const Node& s : sec)
+ {
Trace("sets-mem") << "Eqc " << s << " : ";
- std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].find( s );
- if( it!=d_pol_mems[0].end() ){
+ const std::map<Node, Node>& smem = d_state.getMembers(s);
+ if (!smem.empty())
+ {
Trace("sets-mem") << "Memberships : ";
- for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- Trace("sets-mem") << it2->first << " ";
+ for (const std::pair<const Node, Node>& it2 : smem)
+ {
+ Trace("sets-mem") << it2.first << " ";
}
}
- std::map< Node, Node >::iterator its = d_eqc_singleton.find( s );
- if( its!=d_eqc_singleton.end() ){
- Trace("sets-mem") << " : Singleton : " << its->second;
+ Node ss = d_state.getSingletonEqClass(s);
+ if (!ss.isNull())
+ {
+ Trace("sets-mem") << " : Singleton : " << ss;
}
Trace("sets-mem") << std::endl;
}
}
- checkSubtypes( lemmas );
- flushLemmas( lemmas, true );
- if( !hasProcessed() ){
-
- checkDownwardsClosure( lemmas );
+ checkSubtypes();
+ d_im.flushPendingLemmas(true);
+ if (!d_im.hasProcessed())
+ {
+ checkDownwardsClosure();
if( options::setsInferAsLemmas() ){
- flushLemmas( lemmas );
+ d_im.flushPendingLemmas();
}
- if( !hasProcessed() ){
- checkUpwardsClosure( lemmas );
- flushLemmas( lemmas );
- if( !hasProcessed() ){
- checkDisequalities(lemmas);
- flushLemmas(lemmas);
- if (!hasProcessed() && d_card_enabled)
+ if (!d_im.hasProcessed())
+ {
+ checkUpwardsClosure();
+ d_im.flushPendingLemmas();
+ if (!d_im.hasProcessed())
+ {
+ checkDisequalities();
+ d_im.flushPendingLemmas();
+ if (!d_im.hasProcessed() && d_card_enabled)
{
- // for cardinality
- checkCardBuildGraph( lemmas );
- flushLemmas( lemmas );
- if( !hasProcessed() ){
- checkMinCard( lemmas );
- flushLemmas( lemmas );
- if( !hasProcessed() ){
- checkCardCycles( lemmas );
- flushLemmas( lemmas );
- if( !hasProcessed() ){
- std::vector<Node> intro_sets;
- checkNormalForms( lemmas, intro_sets );
- flushLemmas( lemmas );
- if (!hasProcessed() && !intro_sets.empty())
- {
- Assert(intro_sets.size() == 1);
- Trace("sets-intro")
- << "Introduce term : " << intro_sets[0] << std::endl;
- Trace("sets-intro") << " Actual Intro : ";
- debugPrintSet(intro_sets[0], "sets-nf");
- Trace("sets-nf") << std::endl;
- Node k = getProxy(intro_sets[0]);
- d_sentLemma = true;
- }
- }
- }
- }
+ // call the check method of the cardinality solver
+ d_cardSolver->check();
}
}
}
}
}
- if (!hasProcessed())
+ if (!d_im.hasProcessed())
{
// invoke relations solver
d_rels->check(Theory::EFFORT_FULL);
}
- }while( !d_sentLemma && !d_conflict && d_addedFact );
- Trace("sets") << "----- End full effort check, conflict=" << d_conflict << ", lemma=" << d_sentLemma << std::endl;
+ Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
+ } while (!d_im.hasSentLemma() && !d_state.isInConflict()
+ && d_im.hasAddedFact());
+ Trace("sets") << "----- End full effort check, conflict="
+ << d_state.isInConflict() << ", lemma=" << d_im.hasSentLemma()
+ << std::endl;
}
-void TheorySetsPrivate::checkSubtypes( std::vector< Node >& lemmas ) {
- for( unsigned i=0; i<d_set_eqc.size(); i++ ){
- Node s = d_set_eqc[i];
+void TheorySetsPrivate::checkSubtypes()
+{
+ Trace("sets") << "TheorySetsPrivate: check Subtypes..." << std::endl;
+ const std::vector<Node>& sec = d_state.getSetsEqClasses();
+ for (const Node& s : sec)
+ {
TypeNode mct = d_most_common_type[s];
- std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].find( s );
- if( it!=d_pol_mems[0].end() ){
- for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- if (!it2->first.getType().isSubtypeOf(mct))
+ Assert(!mct.isNull());
+ const std::map<Node, Node>& smems = d_state.getMembers(s);
+ if (!smems.empty())
+ {
+ for (const std::pair<const Node, Node>& it2 : smems)
+ {
+ Trace("sets") << " check subtype " << it2.first << " " << it2.second
+ << std::endl;
+ Trace("sets") << " types : " << it2.first.getType() << " " << mct
+ << std::endl;
+ if (!it2.first.getType().isSubtypeOf(mct))
{
Node mctt = d_most_common_type_term[s];
+ Assert(!mctt.isNull());
+ Trace("sets") << " most common type term is " << mctt << std::endl;
std::vector< Node > exp;
- exp.push_back( it2->second );
- Assert( ee_areEqual( mctt, it2->second[1] ) );
- exp.push_back( mctt.eqNode( it2->second[1] ) );
- Node tc_k = getTypeConstraintSkolem(it2->first, mct);
+ exp.push_back(it2.second);
+ Assert(d_state.areEqual(mctt, it2.second[1]));
+ exp.push_back(mctt.eqNode(it2.second[1]));
+ Node tc_k = d_state.getTypeConstraintSkolem(it2.first, mct);
if (!tc_k.isNull())
{
- Node etc = tc_k.eqNode(it2->first);
- assertInference( etc, exp, lemmas, "subtype-clash" );
- if( d_conflict ){
+ Node etc = tc_k.eqNode(it2.first);
+ d_im.assertInference(etc, exp, "subtype-clash");
+ if (d_state.isInConflict())
+ {
return;
}
}
}
}
}
+ Trace("sets") << "TheorySetsPrivate: finished." << std::endl;
}
-void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) {
- Trace("sets") << "Downwards closure..." << std::endl;
+void TheorySetsPrivate::checkDownwardsClosure()
+{
+ Trace("sets") << "TheorySetsPrivate: check downwards closure..." << std::endl;
//downwards closure
- for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){
- std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( it->first );
- if( itn!=d_nvar_sets.end() ){
- for( unsigned j=0; j<itn->second.size(); j++ ){
- if( d_congruent.find( itn->second[j] )==d_congruent.end() ){
- for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- Node mem = it2->second;
- Node eq_set = itn->second[j];
+ const std::vector<Node>& sec = d_state.getSetsEqClasses();
+ for (const Node& s : sec)
+ {
+ const std::vector<Node>& nvsets = d_state.getNonVariableSets(s);
+ if (!nvsets.empty())
+ {
+ const std::map<Node, Node>& smem = d_state.getMembers(s);
+ for (const Node& nv : nvsets)
+ {
+ if (!d_state.isCongruent(nv))
+ {
+ for (const std::pair<const Node, Node>& it2 : smem)
+ {
+ Node mem = it2.second;
+ Node eq_set = nv;
Assert( d_equalityEngine.areEqual( mem[1], eq_set ) );
if( mem[1]!=eq_set ){
Trace("sets-debug") << "Downwards closure based on " << mem << ", eq_set = " << eq_set << std::endl;
std::vector< Node > exp;
exp.push_back( mem );
exp.push_back( mem[1].eqNode( eq_set ) );
- assertInference( nmem, exp, lemmas, "downc" );
- if( d_conflict ){
+ d_im.assertInference(nmem, exp, "downc");
+ if (d_state.isInConflict())
+ {
return;
}
}else{
//use proxy set
- Node k = getProxy( eq_set );
+ Node k = d_state.getProxy(eq_set);
Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k );
Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
nmem = Rewriter::rewrite( nmem );
std::vector< Node > exp;
- if( ee_areEqual( mem, pmem ) ){
+ if (d_state.areEqual(mem, pmem))
+ {
exp.push_back( pmem );
- }else{
+ }
+ else
+ {
nmem = NodeManager::currentNM()->mkNode( kind::OR, pmem.negate(), nmem );
}
- assertInference( nmem, exp, lemmas, "downc" );
+ d_im.assertInference(nmem, exp, "downc");
}
}
}
}
}
-void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) {
+void TheorySetsPrivate::checkUpwardsClosure()
+{
//upwards closure
- for( std::map< Kind, std::map< Node, std::map< Node, Node > > >::iterator itb = d_bop_index.begin(); itb != d_bop_index.end(); ++itb ){
- Kind k = itb->first;
- Trace("sets") << "Upwards closure " << k << "..." << std::endl;
- for( std::map< Node, std::map< Node, Node > >::iterator it = itb->second.begin(); it != itb->second.end(); ++it ){
- Node r1 = it->first;
+ NodeManager* nm = NodeManager::currentNM();
+ const std::map<Kind, std::map<Node, std::map<Node, Node> > >& boi =
+ d_state.getBinaryOpIndex();
+ for (const std::pair<const Kind, std::map<Node, std::map<Node, Node> > >&
+ itb : boi)
+ {
+ Kind k = itb.first;
+ Trace("sets") << "TheorySetsPrivate: check upwards closure " << k << "..."
+ << std::endl;
+ for (const std::pair<const Node, std::map<Node, Node> >& it : itb.second)
+ {
+ Node r1 = it.first;
//see if there are members in first argument r1
- std::map< Node, std::map< Node, Node > >::iterator itm1 = d_pol_mems[0].find( r1 );
- if( itm1!=d_pol_mems[0].end() || k==kind::UNION ){
- for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- Node r2 = it2->first;
+ const std::map<Node, Node>& r1mem = d_state.getMembers(r1);
+ if (!r1mem.empty() || k == kind::UNION)
+ {
+ for (const std::pair<const Node, Node>& it2 : it.second)
+ {
+ Node r2 = it2.first;
+ Node term = it2.second;
//see if there are members in second argument
- std::map< Node, std::map< Node, Node > >::iterator itm2 = d_pol_mems[0].find( r2 );
- std::map< Node, std::map< Node, Node > >::iterator itm2n = d_pol_mems[1].find( r2 );
- if( itm2!=d_pol_mems[0].end() || k!=kind::INTERSECTION ){
- Trace("sets-debug") << "Checking " << it2->second << ", members = " << (itm1!=d_pol_mems[0].end()) << ", " << (itm2!=d_pol_mems[0].end()) << std::endl;
+ const std::map<Node, Node>& r2mem = d_state.getMembers(r2);
+ const std::map<Node, Node>& r2nmem = d_state.getNegativeMembers(r2);
+ if (!r2mem.empty() || k != kind::INTERSECTION)
+ {
+ Trace("sets-debug")
+ << "Checking " << term << ", members = " << (!r1mem.empty())
+ << ", " << (!r2mem.empty()) << std::endl;
//for all members of r1
- if( itm1!=d_pol_mems[0].end() ){
- for( std::map< Node, Node >::iterator itm1m = itm1->second.begin(); itm1m != itm1->second.end(); ++itm1m ){
- Node xr = itm1m->first;
- Node x = itm1m->second[0];
- Trace("sets-debug") << "checking membership " << xr << " " << itm1m->second << std::endl;
+ if (!r1mem.empty())
+ {
+ for (const std::pair<const Node, Node>& itm1m : r1mem)
+ {
+ Node xr = itm1m.first;
+ Node x = itm1m.second[0];
+ Trace("sets-debug") << "checking membership " << xr << " "
+ << itm1m.second << std::endl;
std::vector< Node > exp;
- exp.push_back( itm1m->second );
- addEqualityToExp( it2->second[0], itm1m->second[1], exp );
+ exp.push_back(itm1m.second);
+ d_state.addEqualityToExp(term[0], itm1m.second[1], exp);
bool valid = false;
int inferType = 0;
if( k==kind::UNION ){
valid = true;
}else if( k==kind::INTERSECTION ){
- //conclude x is in it2->second
- //if also existing in members of r2
- bool in_r2 = itm2!=d_pol_mems[0].end() && itm2->second.find( xr )!=itm2->second.end();
- if( in_r2 ){
- exp.push_back( itm2->second[xr] );
- addEqualityToExp( it2->second[1], itm2->second[xr][1], exp );
- addEqualityToExp( x, itm2->second[xr][0], exp );
+ // conclude x is in term
+ // if also existing in members of r2
+ std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
+ if (itm != r2mem.end())
+ {
+ exp.push_back(itm->second);
+ d_state.addEqualityToExp(term[1], itm->second[1], exp);
+ d_state.addEqualityToExp(x, itm->second[0], exp);
valid = true;
- }else{
+ }
+ else
+ {
// if not, check whether it is definitely not a member, if unknown, split
- bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2n->second.end();
- if( !not_in_r2 ){
- exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ) );
+ if (r2nmem.find(xr) == r2nmem.end())
+ {
+ exp.push_back(nm->mkNode(kind::MEMBER, x, term[1]));
valid = true;
inferType = 1;
}
}
}else{
Assert( k==kind::SETMINUS );
- /*
- std::map< Node, std::map< Node, Node > >::iterator itnm2 = d_pol_mems[1].find( r2 );
- if( itnm2!=d_pol_mems[1].end() ){
- bool not_in_r2 = itnm2->second.find( xr )!=itnm2->second.end();
- if( not_in_r2 ){
- exp.push_back( itnm2->second[xr] );
- if( it2->second[1]!=itnm2->second[xr][1] ){
- Assert( d_equalityEngine.areEqual( it2->second[1], itnm2->second[xr][1] ) );
- exp.push_back( it2->second[1].eqNode( itnm2->second[xr][1] ) );
- }
- if( x!=itnm2->second[xr][0] ){
- Assert( d_equalityEngine.areEqual( x, itnm2->second[xr][0] ) );
- exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, x, itnm2->second[xr][0] ) );
- }
- valid = true;
- }
- }
- */
- if( !valid ){
- bool in_r2 = itm2!=d_pol_mems[0].end() && itm2->second.find( xr )!=itm2->second.end();
- if( !in_r2 ){
- // must add lemma for set minus since non-membership in this case is not explained
- exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ).negate() );
- valid = true;
- inferType = 1;
- }
+ std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
+ if (itm == r2mem.end())
+ {
+ // must add lemma for set minus since non-membership in this
+ // case is not explained
+ exp.push_back(
+ nm->mkNode(kind::MEMBER, x, term[1]).negate());
+ valid = true;
+ inferType = 1;
}
}
if( valid ){
- Node rr = d_equalityEngine.getRepresentative( it2->second );
+ Node rr = d_equalityEngine.getRepresentative(term);
if( !isMember( x, rr ) ){
- Node kk = getProxy( it2->second );
- Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, x, kk );
- assertInference( fact, exp, lemmas, "upc", inferType );
- if( d_conflict ){
+ Node kk = d_state.getProxy(term);
+ Node fact = nm->mkNode(kind::MEMBER, x, kk);
+ d_im.assertInference(fact, exp, "upc", inferType);
+ if (d_state.isInConflict())
+ {
return;
}
}
}
- Trace("sets-debug") << "done checking membership " << xr << " " << itm1m->second << std::endl;
+ Trace("sets-debug") << "done checking membership " << xr << " "
+ << itm1m.second << std::endl;
}
}
if( k==kind::UNION ){
- if( itm2!=d_pol_mems[0].end() ){
+ if (!r2mem.empty())
+ {
//for all members of r2
- for( std::map< Node, Node >::iterator itm2m = itm2->second.begin(); itm2m != itm2->second.end(); ++itm2m ){
- Node x = itm2m->second[0];
- Node rr = d_equalityEngine.getRepresentative( it2->second );
+ for (const std::pair<const Node, Node>& itm2m : r2mem)
+ {
+ Node x = itm2m.second[0];
+ Node rr = d_equalityEngine.getRepresentative(term);
if( !isMember( x, rr ) ){
std::vector< Node > exp;
- exp.push_back( itm2m->second );
- addEqualityToExp( it2->second[1], itm2m->second[1], exp );
- Node k = getProxy( it2->second );
- Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, x, k );
- assertInference( fact, exp, lemmas, "upc2" );
- if( d_conflict ){
+ exp.push_back(itm2m.second);
+ d_state.addEqualityToExp(term[1], itm2m.second[1], exp);
+ Node k = d_state.getProxy(term);
+ Node fact = nm->mkNode(kind::MEMBER, x, k);
+ d_im.assertInference(fact, exp, "upc2");
+ if (d_state.isInConflict())
+ {
return;
}
}
}
}
- }
- }
+ }
+ }
}
}
}
}
- if( !hasProcessed() ){
+ if (!d_im.hasProcessed())
+ {
if( options::setsExt() ){
//universal sets
Trace("sets-debug") << "Check universe sets..." << std::endl;
//all elements must be in universal set
- for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){
+ const std::vector<Node>& sec = d_state.getSetsEqClasses();
+ for (const Node& s : sec)
+ {
//if equivalence class contains a variable
- std::map< Node, Node >::iterator itv = d_var_set.find( it->first );
- if( itv!=d_var_set.end() ){
+ Node v = d_state.getVariableSet(s);
+ if (!v.isNull())
+ {
//the variable in the equivalence class
- Node v = itv->second;
std::map< TypeNode, Node > univ_set;
- for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- Node e = it2->second[0];
+ const std::map<Node, Node>& smems = d_state.getMembers(s);
+ for (const std::pair<const Node, Node>& it2 : smems)
+ {
+ Node e = it2.second[0];
TypeNode tn = NodeManager::currentNM()->mkSetType( e.getType() );
Node u;
std::map< TypeNode, Node >::iterator itu = univ_set.find( tn );
if( itu==univ_set.end() ){
- std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn );
+ Node ueqc = d_state.getUnivSetEqClass(tn);
// if the universe does not yet exist, or is not in this equivalence class
- if( itu==d_eqc_univset.end() || itu->second!=it->first ){
- u = getUnivSet( tn );
+ if (s != ueqc)
+ {
+ u = d_state.getUnivSet(tn);
}
univ_set[tn] = u;
}else{
u = itu->second;
}
if( !u.isNull() ){
- Assert( it2->second.getKind()==kind::MEMBER );
+ Assert(it2.second.getKind() == kind::MEMBER);
std::vector< Node > exp;
- exp.push_back( it2->second );
- if( v!=it2->second[1] ){
- exp.push_back( v.eqNode( it2->second[1] ) );
+ exp.push_back(it2.second);
+ if (v != it2.second[1])
+ {
+ exp.push_back(v.eqNode(it2.second[1]));
}
- Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, it2->second[0], u );
- assertInference( fact, exp, lemmas, "upuniv" );
- if( d_conflict ){
+ Node fact = nm->mkNode(kind::MEMBER, it2.second[0], u);
+ d_im.assertInference(fact, exp, "upuniv");
+ if (d_state.isInConflict())
+ {
return;
}
}
}
}
-void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) {
+void TheorySetsPrivate::checkDisequalities()
+{
//disequalities
- Trace("sets") << "Disequalities..." << std::endl;
+ Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl;
for(NodeBoolMap::const_iterator it=d_deq.begin(); it !=d_deq.end(); ++it) {
if( (*it).second ){
Node deq = (*it).first;
Assert( d_equalityEngine.hasTerm( deq[0] ) && d_equalityEngine.hasTerm( deq[1] ) );
Node r1 = d_equalityEngine.getRepresentative( deq[0] );
Node r2 = d_equalityEngine.getRepresentative( deq[1] );
- bool is_sat = isSetDisequalityEntailed( r1, r2 );
+ bool is_sat = d_state.isSetDisequalityEntailed(r1, r2);
/*
if( !is_sat ){
//try to make one of them empty
Node mem2 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[1] );
Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::EQUAL, mem1, mem2 ).negate() );
lem = Rewriter::rewrite( lem );
- assertInference( lem, d_emp_exp, lemmas, "diseq", 1 );
- flushLemmas( lemmas );
- if( hasProcessed() ){
+ d_im.assertInference(lem, d_emp_exp, "diseq", 1);
+ d_im.flushPendingLemmas();
+ if (d_im.hasProcessed())
+ {
return;
}
}
}
}
-void TheorySetsPrivate::checkCardBuildGraph( std::vector< Node >& lemmas ) {
- Trace("sets") << "Cardinality graph..." << std::endl;
- //first, ensure cardinality relationships are added as lemmas for all non-basic set terms
- for( unsigned i=0; i<d_set_eqc.size(); i++ ){
- Node eqc = d_set_eqc[i];
- std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
- if( itn!=d_nvar_sets.end() ){
- for( unsigned j=0; j<itn->second.size(); j++ ){
- Node n = itn->second[j];
- if( d_congruent.find( n )==d_congruent.end() ){
- //if setminus, do for intersection instead
- if( n.getKind()==kind::SETMINUS ){
- n = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, n[0], n[1] ) );
- }
- registerCardinalityTerm( n, lemmas );
- }
- }
- }
- }
- Trace("sets") << "Done cardinality graph" << std::endl;
-}
-
-void TheorySetsPrivate::registerCardinalityTerm( Node n, std::vector< Node >& lemmas ){
- TypeNode tnc = n.getType().getSetElementType();
- if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end())
- {
- // if no cardinality constraints for sets of this type, we can ignore
- return;
- }
- if( d_card_processed.find( n )==d_card_processed.end() ){
- d_card_processed.insert( n );
- Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
- std::vector< Node > cterms;
- if( n.getKind()==kind::INTERSECTION ){
- for( unsigned e=0; e<2; e++ ){
- Node s = NodeManager::currentNM()->mkNode( kind::SETMINUS, n[e], n[1-e] );
- cterms.push_back( s );
- }
- Node pos_lem = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::CARD, n ), d_zero );
- assertInference( pos_lem, d_emp_exp, lemmas, "pcard", 1 );
- }else{
- cterms.push_back( n );
- }
- for( unsigned k=0; k<cterms.size(); k++ ){
- Node nn = cterms[k];
- Node nk = getProxy( nn );
- Node pos_lem = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::CARD, nk ), d_zero );
- assertInference( pos_lem, d_emp_exp, lemmas, "pcard", 1 );
- if( nn!=nk ){
- Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::CARD, nk ),
- NodeManager::currentNM()->mkNode( kind::CARD, nn ) );
- lem = Rewriter::rewrite( lem );
- Trace("sets-card") << " " << k << " : " << lem << std::endl;
- assertInference( lem, d_emp_exp, lemmas, "card", 1 );
- }
- }
- }
-}
-
-void TheorySetsPrivate::checkCardCycles( std::vector< Node >& lemmas ) {
- Trace("sets") << "Check cardinality cycles..." << std::endl;
- //build order of equivalence classes, also build cardinality graph
- std::vector< Node > set_eqc_tmp;
- set_eqc_tmp.insert( set_eqc_tmp.end(), d_set_eqc.begin(), d_set_eqc.end() );
- d_set_eqc.clear();
- d_card_parent.clear();
- for( unsigned i=0; i<set_eqc_tmp.size(); i++ ){
- std::vector< Node > curr;
- std::vector< Node > exp;
- checkCardCyclesRec( set_eqc_tmp[i], curr, exp, lemmas );
- flushLemmas( lemmas );
- if( hasProcessed() ){
- return;
- }
- }
- Trace("sets") << "Done check cardinality cycles" << std::endl;
-}
-
-void TheorySetsPrivate::checkCardCyclesRec( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp, std::vector< Node >& lemmas ) {
- if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
- Trace("sets-debug") << "Found venn region loop..." << std::endl;
- if( curr.size()>1 ){
- //all regions must be equal
- std::vector< Node > conc;
- for( unsigned i=1; i<curr.size(); i++ ){
- conc.push_back( curr[0].eqNode( curr[i] ) );
- }
- Node fact = conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::AND, conc );
- assertInference( fact, exp, lemmas, "card_cycle" );
- flushLemmas( lemmas );
- }else{
- //should be guaranteed based on not exploring equal parents
- Assert( false );
- }
- }else if( std::find( d_set_eqc.begin(), d_set_eqc.end(), eqc )==d_set_eqc.end() ){
- curr.push_back( eqc );
- TypeNode tn = eqc.getType();
- bool is_empty = eqc==d_eqc_emptyset[tn];
- Node emp_set = getEmptySet( tn );
- std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
- if( itn!=d_nvar_sets.end() ){
- for( unsigned j=0; j<itn->second.size(); j++ ){
- Node n = itn->second[j];
- if( n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS ){
- Trace("sets-debug") << "Build cardinality parents for " << n << "..." << std::endl;
- std::vector< Node > sib;
- unsigned true_sib = 0;
- if( n.getKind()==kind::INTERSECTION ){
- d_card_base[n] = n;
- for( unsigned e=0; e<2; e++ ){
- Node sm = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::SETMINUS, n[e], n[1-e] ) );
- sib.push_back( sm );
- }
- true_sib = 2;
- }else{
- Node si = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, n[0], n[1] ) );
- sib.push_back( si );
- d_card_base[n] = si;
- Node osm = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::SETMINUS, n[1], n[0] ) );
- sib.push_back( osm );
- true_sib = 1;
- }
- Node u = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::UNION, n[0], n[1] ) );
- if( !d_equalityEngine.hasTerm( u ) ){
- u = Node::null();
- }
- unsigned n_parents = true_sib + ( u.isNull() ? 0 : 1 );
- //if this set is empty
- if( is_empty ){
- Assert( ee_areEqual( n, emp_set ) );
- Trace("sets-debug") << " empty, parents equal siblings" << std::endl;
- std::vector< Node > conc;
- //parent equal siblings
- for( unsigned e=0; e<true_sib; e++ ){
- if( d_equalityEngine.hasTerm( sib[e] ) && !ee_areEqual( n[e], sib[e] ) ){
- conc.push_back( n[e].eqNode( sib[e] ) );
- }
- }
- assertInference( conc, n.eqNode( emp_set ), lemmas, "cg_emp" );
- flushLemmas( lemmas );
- if( hasProcessed() ){
- return;
- }else{
- //justify why there is no edge to parents (necessary?)
- for( unsigned e=0; e<n_parents; e++ ){
- Node p = (e==true_sib) ? u : n[e];
-
- }
- }
- }else{
- std::vector< Node > card_parents;
- std::vector< int > card_parent_ids;
- //check if equal to a parent
- for( unsigned e=0; e<n_parents; e++ ){
- Trace("sets-debug") << " check parent " << e << "/" << n_parents << std::endl;
- bool is_union = e==true_sib;
- Node p = (e==true_sib) ? u : n[e];
- Trace("sets-debug") << " check relation to parent " << p << ", isu=" << is_union << "..." << std::endl;
- //if parent is empty
- if( ee_areEqual( p, emp_set ) ){
- Trace("sets-debug") << " it is empty..." << std::endl;
- Assert( !ee_areEqual( n, emp_set ) );
- assertInference( n.eqNode( emp_set ), p.eqNode( emp_set ), lemmas, "cg_emppar" );
- if( hasProcessed() ){
- return;
- }
- //if we are equal to a parent
- }else if( ee_areEqual( p, n ) ){
- Trace("sets-debug") << " it is equal to this..." << std::endl;
- std::vector< Node > conc;
- std::vector< int > sib_emp_indices;
- if( is_union ){
- for( unsigned s=0; s<sib.size(); s++ ){
- sib_emp_indices.push_back( s );
- }
- }else{
- sib_emp_indices.push_back( e );
- }
- //sibling(s) are empty
- for( unsigned s=0; s<sib_emp_indices.size(); s++ ){
- unsigned si = sib_emp_indices[s];
- if( !ee_areEqual( sib[si], emp_set ) ){
- conc.push_back( sib[si].eqNode( emp_set ) );
- }else{
- Trace("sets-debug") << "Sibling " << sib[si] << " is already empty." << std::endl;
- }
- }
- if( !is_union && n.getKind()==kind::INTERSECTION && !u.isNull() ){
- //union is equal to other parent
- if( !ee_areEqual( u, n[1-e] ) ){
- conc.push_back( u.eqNode( n[1-e] ) );
- }
- }
- Trace("sets-debug") << "...derived " << conc.size() << " conclusions" << std::endl;
- assertInference( conc, n.eqNode( p ), lemmas, "cg_eqpar" );
- flushLemmas( lemmas );
- if( hasProcessed() ){
- return;
- }
- }else{
- Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
- //otherwise, we a syntactic subset of p
- card_parents.push_back( p );
- card_parent_ids.push_back( is_union ? 2 : e );
- }
- }
- Assert( d_card_parent[n].empty() );
- Trace("sets-debug") << "get parent representatives..." << std::endl;
- //for each parent, take their representatives
- for( unsigned k=0; k<card_parents.size(); k++ ){
- Node eqcc = d_equalityEngine.getRepresentative( card_parents[k] );
- Trace("sets-debug") << "Check card parent " << k << "/" << card_parents.size() << std::endl;
-
- //if parent is singleton, then we should either be empty to equal to it
- std::map< Node, Node >::iterator itps = d_eqc_singleton.find( eqcc );
- if( itps!=d_eqc_singleton.end() ){
- bool eq_parent = false;
- std::vector< Node > exp;
- addEqualityToExp( card_parents[k], itps->second, exp );
- if( ee_areDisequal( n, emp_set ) ){
- exp.push_back( n.eqNode( emp_set ).negate() );
- eq_parent = true;
- }else{
- std::map< Node, std::map< Node, Node > >::iterator itpm = d_pol_mems[0].find( eqc );
- if( itpm!=d_pol_mems[0].end() && !itpm->second.empty() ){
- Node pmem = itpm->second.begin()->second;
- exp.push_back( pmem );
- addEqualityToExp( n, pmem[1], exp );
- eq_parent = true;
- }
- }
- //must be equal to parent
- if( eq_parent ){
- Node conc = n.eqNode( card_parents[k] );
- assertInference( conc, exp, lemmas, "cg_par_sing" );
- flushLemmas( lemmas );
- }else{
- //split on empty
- Trace("sets-nf") << "Split empty : " << n << std::endl;
- split( n.eqNode( emp_set ), 1 );
- }
- Assert( hasProcessed() );
- return;
- }else{
- bool dup = false;
- for( unsigned l=0; l<d_card_parent[n].size(); l++ ){
- if( eqcc==d_card_parent[n][l] ){
- Trace("sets-debug") << " parents " << l << " and " << k << " are equal, ids = " << card_parent_ids[l] << " " << card_parent_ids[k] << std::endl;
- dup = true;
- if( n.getKind()==kind::INTERSECTION ){
- Assert( card_parent_ids[l]!=2 );
- std::vector< Node > conc;
- if( card_parent_ids[k]==2 ){
- //intersection is equal to other parent
- unsigned pid = 1-card_parent_ids[l];
- if( !ee_areEqual( n[pid], n ) ){
- Trace("sets-debug") << " one of them is union, make equal to other..." << std::endl;
- conc.push_back( n[pid].eqNode( n ) );
- }
- }else{
- if( !ee_areEqual( card_parents[k], n ) ){
- Trace("sets-debug") << " neither is union, make equal to one parent..." << std::endl;
- //intersection is equal to one of the parents
- conc.push_back( card_parents[k].eqNode( n ) );
- }
- }
- assertInference( conc, card_parents[k].eqNode( d_card_parent[n][l] ), lemmas, "cg_pareq" );
- flushLemmas( lemmas );
- if( hasProcessed() ){
- return;
- }
- }
- }
- }
- if( !dup ){
- d_card_parent[n].push_back( eqcc );
- }
- }
- }
- //now recurse on parents (to ensure their normal will be computed after this eqc)
- exp.push_back( eqc.eqNode( n ) );
- for( unsigned k=0; k<d_card_parent[n].size(); k++ ){
- checkCardCyclesRec( d_card_parent[n][k], curr, exp, lemmas );
- if( hasProcessed() ){
- return;
- }
- }
- exp.pop_back();
- }
- }
- }
- }
- curr.pop_back();
- //parents now processed, can add to ordered list
- d_set_eqc.push_back( eqc );
- }else{
- //already processed
- }
-}
-
-void TheorySetsPrivate::checkNormalForms( std::vector< Node >& lemmas, std::vector< Node >& intro_sets ){
- Trace("sets") << "Check normal forms..." << std::endl;
- // now, build normal form for each equivalence class
- // d_set_eqc is now sorted such that for each d_set_eqc[i], d_set_eqc[j],
- // if d_set_eqc[i] is a strict syntactic subterm of d_set_eqc[j], then i<j.
- d_ff.clear();
- d_nf.clear();
- for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
- checkNormalForm( d_set_eqc[i], intro_sets );
- if( hasProcessed() || !intro_sets.empty() ){
- return;
- }
- }
- Trace("sets") << "Done check normal forms" << std::endl;
-}
-
-void TheorySetsPrivate::checkNormalForm( Node eqc, std::vector< Node >& intro_sets ){
- TypeNode tn = eqc.getType();
- Trace("sets") << "Compute normal form for " << eqc << std::endl;
- Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
- if( eqc==d_eqc_emptyset[tn] ){
- d_nf[eqc].clear();
- Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
- }else{
- //flat/normal forms are sets of equivalence classes
- Node base;
- std::vector< Node > comps;
- std::map< Node, std::map< Node, std::vector< Node > > >::iterator it = d_ff.find( eqc );
- if( it!=d_ff.end() ){
- for( std::map< Node, std::vector< Node > >::iterator itf = it->second.begin(); itf != it->second.end(); ++itf ){
- std::sort( itf->second.begin(), itf->second.end() );
- if( base.isNull() ){
- base = itf->first;
- }else{
- comps.push_back( itf->first );
- }
- Trace("sets-nf") << " F " << itf->first << " : ";
- if( Trace.isOn("sets-nf") ){
- Trace("sets-nf") << "{ ";
- for( unsigned k=0; k<itf->second.size(); k++ ){
- if( k>0 ){ Trace("sets-nf") << ", "; }
- Trace("sets-nf") << "[" << itf->second[k] << "]";
- }
- Trace("sets-nf") << " }" << std::endl;
- }
- Trace("sets-nf-debug") << " ...";
- debugPrintSet( itf->first, "sets-nf-debug" );
- Trace("sets-nf-debug") << std::endl;
- }
- }else{
- Trace("sets-nf") << "(no flat forms)" << std::endl;
- }
-
- Assert( d_nf.find( eqc )==d_nf.end() );
- bool success = true;
- Node emp_set = getEmptySet(tn);
- if( !base.isNull() ){
- for( unsigned j=0; j<comps.size(); j++ ){
- //compare if equal
- std::vector< Node > c;
- c.push_back( base );
- c.push_back( comps[j] );
- std::vector< Node > only[2];
- std::vector< Node > common;
- Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs " << comps[j] << std::endl;
- unsigned k[2] = { 0, 0 };
- while( k[0]<d_ff[eqc][c[0]].size() || k[1]<d_ff[eqc][c[1]].size() ){
- bool proc = true;
- for( unsigned e=0; e<2; e++ ){
- if( k[e]==d_ff[eqc][c[e]].size() ){
- for( ; k[1-e]<d_ff[eqc][c[1-e]].size(); ++k[1-e] ){
- only[1-e].push_back( d_ff[eqc][c[1-e]][k[1-e]] );
- }
- proc = false;
- }
- }
- if( proc ){
- if( d_ff[eqc][c[0]][k[0]]==d_ff[eqc][c[1]][k[1]] ){
- common.push_back( d_ff[eqc][c[0]][k[0]] );
- k[0]++;
- k[1]++;
- }else if( d_ff[eqc][c[0]][k[0]]<d_ff[eqc][c[1]][k[1]] ){
- only[0].push_back( d_ff[eqc][c[0]][k[0]] );
- k[0]++;
- }else{
- only[1].push_back( d_ff[eqc][c[1]][k[1]] );
- k[1]++;
- }
- }
- }
- if( !only[0].empty() || !only[1].empty() ){
- if( Trace.isOn("sets-nf-debug") ){
- Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
- for( unsigned e=0; e<2; e++ ){
- Trace("sets-nf-debug") << " " << c[e] << " : { ";
- for( unsigned l=0; l<only[e].size(); l++ ){
- if( l>0 ){ Trace("sets-nf-debug") << ", "; }
- Trace("sets-nf-debug") << "[" << only[e][l] << "]";
- }
- Trace("sets-nf-debug") << " }" << std::endl;
- }
- }
- //try to make one empty, prefer the unique ones first
- for( unsigned e=0; e<3; e++ ){
- unsigned sz = e==2 ? common.size() : only[e].size();
- for( unsigned l=0; l<sz; l++ ){
- Node r = e==2 ? common[l] : only[e][l];
- Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
- Trace("sets-nf-debug") << " actual : ";
- debugPrintSet( r, "sets-nf-debug" );
- Trace("sets-nf-debug") << std::endl;
- Assert( !ee_areEqual( r, emp_set ) );
- if( !ee_areDisequal( r, emp_set ) && ( d_pol_mems[0].find( r )==d_pol_mems[0].end() || d_pol_mems[0][r].empty() ) ){
- //guess that its equal empty if it has no explicit members
- Trace("sets-nf") << " Split empty : " << r << std::endl;
- Trace("sets-nf") << "Actual Split : ";
- debugPrintSet( r, "sets-nf" );
- Trace("sets-nf") << std::endl;
- split( r.eqNode( emp_set ), 1 );
- Assert( hasProcessed() );
- return;
- }
- }
- }
- for( unsigned l=0; l<only[0].size(); l++ ){
- for( unsigned m=0; m<only[1].size(); m++ ){
- bool disjoint = false;
- Trace("sets-nf-debug") << "Try split " << only[0][l] << " against " << only[1][m] << std::endl;
- //split them
- for( unsigned e=0; e<2; e++ ){
- Node r1 = e==0 ? only[0][l] : only[1][m];
- Node r2 = e==0 ? only[1][m] : only[0][l];
- //check if their intersection exists modulo equality
- std::map< Node, Node >::iterator itb = d_bop_index[kind::INTERSECTION][r1].find( r2 );
- if( itb!=d_bop_index[kind::INTERSECTION][r1].end() ){
- Trace("sets-nf-debug") << "Split term already exists, but not in cardinality graph : " << itb->second << ", should be empty." << std::endl;
- //their intersection is empty (probably?)
- // e.g. these are two disjoint venn regions, proceed to next pair
- Assert( ee_areEqual( emp_set, itb->second ) );
- disjoint = true;
- break;
- }
- }
- if( !disjoint ){
- //simply introduce their intersection
- Assert( only[0][l]!=only[1][m] );
- Node kca = getProxy( only[0][l] );
- Node kcb = getProxy( only[1][m] );
- Node intro = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, kca, kcb ) );
- Trace("sets-nf") << " Intro split : " << only[0][l] << " against " << only[1][m] << ", term is " << intro << std::endl;
- intro_sets.push_back( intro );
- Assert( !d_equalityEngine.hasTerm( intro ) );
- return;
- }
- }
- }
- //should never get here
- success = false;
- }
- }
- if( success ){
- //normal form is flat form of base
- d_nf[eqc].insert( d_nf[eqc].end(), d_ff[eqc][base].begin(), d_ff[eqc][base].end() );
- Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
- }else{
- Trace("sets-nf") << "failed to build N " << eqc << std::endl;
- }
- }else{
- // must ensure disequal from empty
- if (!eqc.isConst() && !ee_areDisequal(eqc, emp_set)
- && (d_pol_mems[0].find(eqc) == d_pol_mems[0].end()
- || d_pol_mems[0][eqc].empty()))
- {
- Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
- split(eqc.eqNode(emp_set));
- success = false;
- }
- else
- {
- // normal form is this equivalence class
- d_nf[eqc].push_back(eqc);
- Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }"
- << std::endl;
- }
- }
- if( success ){
- //send to parents
- std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
- if( itn!=d_nvar_sets.end() ){
- std::map< Node, std::map< Node, bool > > parents_proc;
- for( unsigned j=0; j<itn->second.size(); j++ ){
- Node n = itn->second[j];
- Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
- if( !d_card_parent[n].empty() ){
- Assert( d_card_base.find( n )!=d_card_base.end() );
- Node cbase = d_card_base[n];
- Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
- for( unsigned k=0; k<d_card_parent[n].size(); k++ ){
- Node p = d_card_parent[n][k];
- Trace("sets-nf-debug") << "Check parent " << p << std::endl;
- if( parents_proc[cbase].find( p )==parents_proc[cbase].end() ){
- parents_proc[cbase][p] = true;
- Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p << "] ), from " << n << "..." << std::endl;
- //for( unsigned i=0; i<d_nf[eqc].size(); i++ ){
- // Assert( std::find( d_ff[p][cbase].begin(), d_ff[p][cbase].end(), d_nf[eqc][i] )==d_ff[p][cbase].end() );
- //}
- for( unsigned i=0; i<d_nf[eqc].size(); i++ ){
- if( std::find( d_ff[p][cbase].begin(), d_ff[p][cbase].end(), d_nf[eqc][i] )==d_ff[p][cbase].end() ){
- d_ff[p][cbase].insert( d_ff[p][cbase].end(), d_nf[eqc].begin(), d_nf[eqc].end() );
- }else{
- //if it is a duplicate venn region, it must be empty since it is coming from syntactically disjoint siblings TODO?
- }
- }
- }else{
- Trace("sets-nf-debug") << "..already processed parent " << p << " for " << cbase << std::endl;
- }
- }
- }
- }
- }
- }else{
- Assert( hasProcessed() );
- }
- }
-}
-
-void TheorySetsPrivate::checkMinCard( std::vector< Node >& lemmas ) {
-
- for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
- Node eqc = d_set_eqc[i];
- TypeNode tn = eqc.getType().getSetElementType();
- if (d_t_card_enabled.find(tn) == d_t_card_enabled.end())
- {
- // cardinality is not enabled for this type, skip
- continue;
- }
- //get members in class
- std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc );
- if( itm!=d_pol_mems[0].end() ){
- std::vector< Node > exp;
- std::vector< Node > members;
- Node cardTerm;
- std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc );
- if( it!=d_eqc_to_card_term.end() ){
- cardTerm = it->second;
- }else{
- cardTerm = NodeManager::currentNM()->mkNode( kind::CARD, eqc );
- }
- for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){
- /*
- for( unsigned j=0; j<members.size(); j++ ){
- if( !ee_areDisequal( members[j], itmm->second ) ){
- Assert( !ee_areEqual( members[j], itmm->second ) );
-
- }
- }
- */
- members.push_back( itmm->first );
- exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, itmm->first, cardTerm[0] ) );
- }
- if( members.size()>1 ){
- exp.push_back( NodeManager::currentNM()->mkNode( kind::DISTINCT, members ) );
- }
- if( !members.empty() ){
- Node conc = NodeManager::currentNM()->mkNode( kind::GEQ, cardTerm, NodeManager::currentNM()->mkConst( Rational( members.size() ) ) );
- Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ), conc );
- Trace("sets-lemma") << "Sets::Lemma : " << lem << " by mincard" << std::endl;
- lemmas.push_back( lem );
- }
- }
- }
-}
-
-void TheorySetsPrivate::flushLemmas( std::vector< Node >& lemmas, bool preprocess ) {
- for( unsigned i=0; i<lemmas.size(); i++ ){
- flushLemma( lemmas[i], preprocess );
- }
- lemmas.clear();
-}
-
-void TheorySetsPrivate::flushLemma( Node lem, bool preprocess ) {
- if( d_lemmas_produced.find(lem)==d_lemmas_produced.end() ){
- Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
- d_lemmas_produced.insert(lem);
- d_external.d_out->lemma(lem, false, preprocess);
- d_sentLemma = true;
- }else{
- Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
- }
-}
-
-Node TheorySetsPrivate::getProxy( Node n ) {
- if( n.getKind()==kind::EMPTYSET || n.getKind()==kind::SINGLETON || n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS || n.getKind()==kind::UNION ){
- NodeMap::const_iterator it = d_proxy.find( n );
- if( it==d_proxy.end() ){
- Node k = NodeManager::currentNM()->mkSkolem( "sp", n.getType(), "proxy for set" );
- d_proxy[n] = k;
- d_proxy_to_term[k] = n;
- Node eq = k.eqNode( n );
- Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
- d_external.d_out->lemma( eq );
- if( n.getKind()==kind::SINGLETON ){
- Node slem = NodeManager::currentNM()->mkNode( kind::MEMBER, n[0], k );
- Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton" << std::endl;
- d_external.d_out->lemma( slem );
- d_sentLemma = true;
- }
- return k;
- }else{
- return (*it).second;
- }
- }else{
- return n;
- }
-}
-
-Node TheorySetsPrivate::getCongruent( Node n ) {
- Assert( d_equalityEngine.hasTerm( n ) );
- std::map< Node, Node >::iterator it = d_congruent.find( n );
- if( it==d_congruent.end() ){
- return n;
- }else{
- return it->second;
- }
-}
-
-Node TheorySetsPrivate::getEmptySet( TypeNode tn ) {
- std::map< TypeNode, Node >::iterator it = d_emptyset.find( tn );
- if( it==d_emptyset.end() ){
- Node n = NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
- d_emptyset[tn] = n;
- return n;
- }else{
- return it->second;
- }
-}
-Node TheorySetsPrivate::getUnivSet( TypeNode tn ) {
- std::map< TypeNode, Node >::iterator it = d_univset.find( tn );
- if( it==d_univset.end() ){
- Node n = NodeManager::currentNM()->mkNullaryOperator(tn, kind::UNIVERSE_SET);
- for( it = d_univset.begin(); it != d_univset.end(); ++it ){
- Node n1;
- Node n2;
- if( tn.isSubtypeOf( it->first ) ){
- n1 = n;
- n2 = it->second;
- }else if( it->first.isSubtypeOf( tn ) ){
- n1 = it->second;
- n2 = n;
- }
- if( !n1.isNull() ){
- Node ulem = NodeManager::currentNM()->mkNode( kind::SUBSET, n1, n2 );
- Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" << std::endl;
- d_external.d_out->lemma( ulem );
- d_sentLemma = true;
- }
- }
- d_univset[tn] = n;
- return n;
- }else{
- return it->second;
- }
-}
-
-bool TheorySetsPrivate::hasLemmaCached( Node lem ) {
- return d_lemmas_produced.find(lem)!=d_lemmas_produced.end();
-}
-
-bool TheorySetsPrivate::hasProcessed() {
- return d_conflict || d_sentLemma || d_addedFact;
-}
-
-void TheorySetsPrivate::debugPrintSet( Node s, const char * c ) {
- if( s.getNumChildren()==0 ){
- NodeMap::const_iterator it = d_proxy_to_term.find( s );
- if( it!=d_proxy_to_term.end() ){
- debugPrintSet( (*it).second, c );
- }else{
- Trace(c) << s;
- }
- }else{
- Trace(c) << "(" << s.getOperator();
- for( unsigned i=0; i<s.getNumChildren(); i++ ){
- Trace(c) << " ";
- debugPrintSet( s[i], c );
- }
- Trace(c) << ")";
- }
-}
-
-void TheorySetsPrivate::lastCallEffortCheck() {
- Trace("sets") << "----- Last call effort check ------" << std::endl;
-
-}
-
-Node TheorySetsPrivate::getTypeConstraintSkolem(Node n, TypeNode tn)
-{
- std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
- if (it == d_tc_skolem[n].end())
- {
- Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn);
- d_tc_skolem[n][tn] = k;
- return k;
- }
- return it->second;
-}
-
/**************************** TheorySetsPrivate *****************************/
/**************************** TheorySetsPrivate *****************************/
/**************************** TheorySetsPrivate *****************************/
void TheorySetsPrivate::check(Theory::Effort level) {
Trace("sets-check") << "Sets check effort " << level << std::endl;
if( level == Theory::EFFORT_LAST_CALL ){
- lastCallEffortCheck();
return;
}
- while(!d_external.done() && !d_conflict) {
+ while (!d_external.done() && !d_state.isInConflict())
+ {
// Get all the assertions
Assertion assertion = d_external.get();
TNode fact = assertion.assertion;
//assert the fact
assertFact( fact, fact );
}
- d_sentLemma = false;
Trace("sets-check") << "Sets finished assertions effort " << level << std::endl;
//invoke full effort check, relations check
- if( !d_conflict ){
+ if (!d_state.isInConflict())
+ {
if( level == Theory::EFFORT_FULL ){
if( !d_external.d_valuation.needCheck() ){
fullEffortCheck();
- if (!d_conflict && !d_sentLemma && d_full_check_incomplete)
+ if (!d_state.isInConflict() && !d_im.hasSentLemma()
+ && d_full_check_incomplete)
{
d_external.d_out->setIncomplete();
}
Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
}/* TheorySetsPrivate::check() */
-bool TheorySetsPrivate::needsCheckLastEffort() {
- if( !d_var_elim.empty() ){
- return true;
- }
- return false;
-}
-
/************************ Sharing ************************/
/************************ Sharing ************************/
/************************ Sharing ************************/
void TheorySetsPrivate::addSharedTerm(TNode n) {
- Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
+ Debug("sets") << "[sets] TheorySetsPrivate::addSharedTerm( " << n << ")"
+ << std::endl;
d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
}
if( t2!=NULL ){
Node f1 = t1->getData();
Node f2 = t2->getData();
- if( !ee_areEqual( f1, f2 ) ){
+ if (!d_state.areEqual(f1, f2))
+ {
Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
vector< pair<TNode, TNode> > currentPairs;
for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
TNode y = f2[k];
Assert( d_equalityEngine.hasTerm(x) );
Assert( d_equalityEngine.hasTerm(y) );
- Assert( !ee_areDisequal( x, y ) );
- Assert( !ee_areCareDisequal( x, y ) );
+ Assert(!d_state.areDisequal(x, y));
+ Assert(!areCareDisequal(x, y));
if( !d_equalityEngine.areEqual( x, y ) ){
Trace("sets-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
if( d_equalityEngine.isTriggerTerm(x, THEORY_SETS) && d_equalityEngine.isTriggerTerm(y, THEORY_SETS) ){
//splitting on sets (necessary for handling set of sets properly)
if( x.getType().isSet() ){
Assert( y.getType().isSet() );
- if( !ee_areDisequal( x, y ) ){
+ if (!d_state.areDisequal(x, y))
+ {
Trace("sets-cg-lemma") << "Should split on : " << x << "==" << y << std::endl;
- split( x.eqNode( y ) );
+ d_im.split(x.eqNode(y));
}
}
}
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
- if( !ee_areCareDisequal(it->first, it2->first) ){
+ if (!areCareDisequal(it->first, it2->first))
+ {
addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
}
}
{
if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
{
- if (!ee_areCareDisequal(tt1.first, tt2.first))
+ if (!areCareDisequal(tt1.first, tt2.first))
{
addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
}
}
void TheorySetsPrivate::computeCareGraph() {
- for( std::map< Kind, std::vector< Node > >::iterator it = d_op_list.begin(); it != d_op_list.end(); ++it ){
- if( it->first==kind::SINGLETON || it->first==kind::MEMBER ){
+ const std::map<Kind, std::vector<Node> >& ol = d_state.getOperatorList();
+ for (const std::pair<const Kind, std::vector<Node> >& it : ol)
+ {
+ Kind k = it.first;
+ if (k == kind::SINGLETON || k == kind::MEMBER)
+ {
unsigned n_pairs = 0;
- Trace("sets-cg-summary") << "Compute graph for sets, op=" << it->first << "..." << it->second.size() << std::endl;
- Trace("sets-cg") << "Build index for " << it->first << "..." << std::endl;
+ Trace("sets-cg-summary") << "Compute graph for sets, op=" << k << "..."
+ << it.second.size() << std::endl;
+ Trace("sets-cg") << "Build index for " << k << "..." << std::endl;
std::map<TypeNode, TNodeTrie> index;
unsigned arity = 0;
//populate indices
- for( unsigned i=0; i<it->second.size(); i++ ){
- TNode f1 = it->second[i];
+ for (TNode f1 : it.second)
+ {
+ Assert(d_equalityEngine.hasTerm(f1));
Trace("sets-cg-debug") << "...build for " << f1 << std::endl;
Assert(d_equalityEngine.hasTerm(f1));
//break into index based on operator, and type of first argument (since some operators are parametric)
return false;
}
+ NodeManager* nm = NodeManager::currentNM();
std::map< Node, Node > mvals;
- for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
- Node eqc = d_set_eqc[i];
+ // If cardinality is enabled, we need to use the ordered equivalence class
+ // list computed by the cardinality solver, where sets equivalence classes
+ // are assigned model values based on their position in the cardinality
+ // graph.
+ const std::vector<Node>& sec = d_card_enabled
+ ? d_cardSolver->getOrderedSetsEqClasses()
+ : d_state.getSetsEqClasses();
+ Valuation& val = getValuation();
+ for (int i = (int)(sec.size() - 1); i >= 0; i--)
+ {
+ Node eqc = sec[i];
if( termSet.find( eqc )==termSet.end() ){
Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl;
}else{
std::vector< Node > els;
- bool is_base = !d_card_enabled || ( d_nf[eqc].size()==1 && d_nf[eqc][0]==eqc );
+ bool is_base = !d_card_enabled || d_cardSolver->isModelValueBasic(eqc);
if( is_base ){
Trace("sets-model") << "Collect elements of base eqc " << eqc << std::endl;
// members that must be in eqc
- std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc );
- if( itm!=d_pol_mems[0].end() ){
- for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){
- Node t = NodeManager::currentNM()->mkNode( kind::SINGLETON, itmm->first );
+ const std::map<Node, Node>& emems = d_state.getMembers(eqc);
+ if (!emems.empty())
+ {
+ for (const std::pair<const Node, Node>& itmm : emems)
+ {
+ Node t = nm->mkNode(kind::SINGLETON, itmm.first);
els.push_back( t );
}
}
}
if( d_card_enabled ){
- TypeNode elementType = eqc.getType().getSetElementType();
- if( is_base ){
- std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc );
- if( it!=d_eqc_to_card_term.end() ){
- //slack elements from cardinality value
- Node v = d_external.d_valuation.getModelValue(it->second);
- Trace("sets-model") << "Cardinality of " << eqc << " is " << v << std::endl;
- Assert(v.getConst<Rational>() <= LONG_MAX, "Exceeded LONG_MAX in sets model");
- unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
- Assert( els.size()<=vu );
- while( els.size()<vu ){
- els.push_back( NodeManager::currentNM()->mkNode( kind::SINGLETON, NodeManager::currentNM()->mkSkolem( "msde", elementType ) ) );
- }
- }else{
- Trace("sets-model") << "No slack elements for " << eqc << std::endl;
- }
- }else{
- Trace("sets-model") << "Build value for " << eqc << " based on normal form, size = " << d_nf[eqc].size() << std::endl;
- //it is union of venn regions
- for( unsigned j=0; j<d_nf[eqc].size(); j++ ){
- Assert( mvals.find( d_nf[eqc][j] )!=mvals.end() );
- els.push_back( mvals[d_nf[eqc][j]] );
- }
- }
+ // make the slack elements for the equivalence class based on set
+ // cardinality
+ d_cardSolver->mkModelValueElementsFor(val, eqc, els, mvals);
}
Node rep = NormalForm::mkBop( kind::UNION, els, eqc.getType() );
rep = Rewriter::rewrite( rep );
/********************** Helper functions ***************************/
/********************** Helper functions ***************************/
-void TheorySetsPrivate::addEqualityToExp( Node a, Node b, std::vector< Node >& exp ) {
- if( a!=b ){
- Assert( ee_areEqual( a, b ) );
- exp.push_back( a.eqNode( b ) );
- }
-}
-
Node mkAnd(const std::vector<TNode>& conjunctions) {
Assert(conjunctions.size() > 0);
conjunction << *it;
++ it;
}
-
return conjunction;
}/* mkAnd() */
-
-TheorySetsPrivate::Statistics::Statistics() :
- d_getModelValueTime("theory::sets::getModelValueTime")
- , d_mergeTime("theory::sets::merge_nodes::time")
- , d_processCard2Time("theory::sets::processCard2::time")
- , d_memberLemmas("theory::sets::lemmas::member", 0)
- , d_disequalityLemmas("theory::sets::lemmas::disequality", 0)
- , d_numVertices("theory::sets::vertices", 0)
- , d_numVerticesMax("theory::sets::vertices-max", 0)
- , d_numMergeEq1or2("theory::sets::merge1or2", 0)
- , d_numMergeEq3("theory::sets::merge3", 0)
- , d_numLeaves("theory::sets::leaves", 0)
- , d_numLeavesMax("theory::sets::leaves-max", 0)
-{
- smtStatisticsRegistry()->registerStat(&d_getModelValueTime);
- smtStatisticsRegistry()->registerStat(&d_mergeTime);
- smtStatisticsRegistry()->registerStat(&d_processCard2Time);
- smtStatisticsRegistry()->registerStat(&d_memberLemmas);
- smtStatisticsRegistry()->registerStat(&d_disequalityLemmas);
- smtStatisticsRegistry()->registerStat(&d_numVertices);
- smtStatisticsRegistry()->registerStat(&d_numVerticesMax);
- smtStatisticsRegistry()->registerStat(&d_numMergeEq1or2);
- smtStatisticsRegistry()->registerStat(&d_numMergeEq3);
- smtStatisticsRegistry()->registerStat(&d_numLeaves);
- smtStatisticsRegistry()->registerStat(&d_numLeavesMax);
-}
-
-
-TheorySetsPrivate::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_getModelValueTime);
- smtStatisticsRegistry()->unregisterStat(&d_mergeTime);
- smtStatisticsRegistry()->unregisterStat(&d_processCard2Time);
- smtStatisticsRegistry()->unregisterStat(&d_memberLemmas);
- smtStatisticsRegistry()->unregisterStat(&d_disequalityLemmas);
- smtStatisticsRegistry()->unregisterStat(&d_numVertices);
- smtStatisticsRegistry()->unregisterStat(&d_numVerticesMax);
- smtStatisticsRegistry()->unregisterStat(&d_numMergeEq1or2);
- smtStatisticsRegistry()->unregisterStat(&d_numMergeEq3);
- smtStatisticsRegistry()->unregisterStat(&d_numLeaves);
- smtStatisticsRegistry()->unregisterStat(&d_numLeavesMax);
-}
-
void TheorySetsPrivate::propagate(Theory::Effort effort) {
}
Debug("sets-prop") << " propagate(" << literal << ")" << std::endl;
// If already in conflict, no more propagation
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
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;
+ d_state.setConflict();
}
return ok;
}/* TheorySetsPrivate::propagate(TNode) */
-void TheorySetsPrivate::processInference(Node lem,
- const char* c,
- std::vector<Node>& lemmas)
-{
- Trace("sets-pinfer") << "Process inference: " << lem << std::endl;
- if (lem.getKind() != IMPLIES || !isEntailed(lem[0], true))
- {
- Trace("sets-pinfer") << " must assert as lemma" << std::endl;
- lemmas.push_back(lem);
- return;
- }
- // try to assert it as a fact
- Trace("sets-pinfer") << "Process conclusion: " << lem[1] << std::endl;
- Trace("sets-pinfer") << " assert as fact" << std::endl;
- assertInference(lem[1], lem[0], lemmas, c);
-}
-
-bool TheorySetsPrivate::isInConflict() const { return d_conflict.get(); }
-bool TheorySetsPrivate::sentLemma() const { return d_sentLemma; }
-
OutputChannel* TheorySetsPrivate::getOutputChannel()
{
return d_external.d_out;
}
+Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; }
+
void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
void TheorySetsPrivate::conflict(TNode a, TNode b)
{
- 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;
- Trace("sets-lemma") << "Equality Conflict : " << d_conflictNode << std::endl;
- d_conflict = true;
+ Node conf = explain(a.eqNode(b));
+ d_state.setConflict(conf);
+ Debug("sets") << "[sets] conflict: " << a << " iff " << b << ", explanation "
+ << conf << std::endl;
+ Trace("sets-lemma") << "Equality Conflict : " << conf << std::endl;
}
Node TheorySetsPrivate::explain(TNode literal)
//TODO: allow variable elimination for sets when setsExt = true
//this is based off of Theory::ppAssert
- Node var;
if (in.getKind() == kind::EQUAL)
{
if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
if (!in[0].getType().isSet() || !options::setsExt())
{
outSubstitutions.addSubstitution(in[0], in[1]);
- var = in[0];
status = Theory::PP_ASSERT_STATUS_SOLVED;
}
}
if (!in[1].getType().isSet() || !options::setsExt())
{
outSubstitutions.addSubstitution(in[1], in[0]);
- var = in[1];
status = Theory::PP_ASSERT_STATUS_SOLVED;
}
}
}
}
}
-
- if( status==Theory::PP_ASSERT_STATUS_SOLVED ){
- Trace("sets-var-elim") << "Sets : ppAssert variable eliminated : " << in << ", var = " << var << std::endl;
- /*
- if( var.getType().isSet() ){
- //we must ensure that subs is included in the universe set
- d_var_elim[var] = true;
- }
- */
- if( options::setsExt() ){
- Assert( !var.getType().isSet() );
- }
- }
return status;
}
-
-void TheorySetsPrivate::presolve() {
- d_op_list.clear();
-}
+
+void TheorySetsPrivate::presolve() { d_state.reset(); }
/**************************** eq::NotifyClass *****************************/
/**************************** eq::NotifyClass *****************************/
#include "context/cdhashset.h"
#include "context/cdqueue.h"
#include "expr/node_trie.h"
-#include "theory/sets/skolem_cache.h"
+#include "theory/sets/cardinality_extension.h"
+#include "theory/sets/inference_manager.h"
+#include "theory/sets/solver_state.h"
#include "theory/sets/theory_sets_rels.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
namespace sets {
/** Internal classes, forward declared here */
-class TheorySetsTermInfoManager;
class TheorySets;
-class TheorySetsScrutinize;
class TheorySetsPrivate {
-//new implementation
typedef context::CDHashMap< Node, bool, NodeHashFunction> NodeBoolMap;
typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
- typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
-public:
+
+ public:
void eqNotifyNewClass(TNode t);
void eqNotifyPreMerge(TNode t1, TNode t2);
void eqNotifyPostMerge(TNode t1, TNode t2);
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
-private:
- bool ee_areEqual( Node a, Node b );
- bool ee_areDisequal( Node a, Node b );
- bool ee_areCareDisequal( Node a, Node b );
+ /** Assert fact holds in the current context with explanation exp.
+ *
+ * exp should be explainable by the equality engine of this class, and fact
+ * should be a literal.
+ */
+ bool assertFact(Node fact, Node exp);
+
+ private:
+ /** Are a and b trigger terms in the equality engine that may be disequal? */
+ bool areCareDisequal(Node a, Node b);
NodeIntMap d_members;
std::map< Node, std::vector< Node > > d_members_data;
- bool assertFact( Node fact, Node exp );
- // inferType : 1 : must send out as lemma, -1 : do internal inferences if possible, 0 : default.
- bool assertFactRec( Node fact, Node exp, std::vector< Node >& lemma, int inferType = 0 );
- // add inferences corresponding to ( exp => fact ) to lemmas, equality engine
- void assertInference( Node fact, Node exp, std::vector< Node >& lemmas, const char * c, int inferType = 0 );
- void assertInference( Node fact, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType = 0 );
- void assertInference( std::vector< Node >& conc, Node exp, std::vector< Node >& lemmas, const char * c, int inferType = 0 );
- void assertInference( std::vector< Node >& conc, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType = 0 );
- // send lemma ( n OR (NOT n) ) immediately
- void split( Node n, int reqPol=0 );
+ /**
+ * Invoke the decision procedure for this theory, which is run at
+ * full effort. This will either send a lemma or conflict on the output
+ * channel of this class, or otherwise the current set of constraints is
+ * satisfiable w.r.t. the theory of sets.
+ */
void fullEffortCheck();
- void checkSubtypes( std::vector< Node >& lemmas );
- void checkDownwardsClosure( std::vector< Node >& lemmas );
- void checkUpwardsClosure( std::vector< Node >& lemmas );
- void checkDisequalities( std::vector< Node >& lemmas );
- bool isMember( Node x, Node s );
- bool isSetDisequalityEntailed( Node s, Node t );
-
- Node getProxy( Node n );
- Node getCongruent( Node n );
- Node getEmptySet( TypeNode tn );
- Node getUnivSet( TypeNode tn );
- bool hasLemmaCached( Node lem );
- bool hasProcessed();
+ /**
+ * Reset the information for a full effort check.
+ */
+ void fullEffortReset();
+ /**
+ * This ensures that subtype constraints are met for all set terms. In
+ * particular, for a set equivalence class E, let Set(T) be the most
+ * common type among the types of terms in that class. In other words,
+ * if E contains two terms of Set(Int) and Set(Real), then Set(Int) is the
+ * most common type. Then, for each membership x in S where S is a set in
+ * this equivalence class, we ensure x has type T by asserting:
+ * x = k
+ * for a fresh constant k of type T. This is done only if the type of x is not
+ * a subtype of Int (e.g. if x is of type Real). We call k the "type
+ * constraint skolem for x of type Int".
+ */
+ void checkSubtypes();
+ /**
+ * This implements an inference schema based on the "downwards closure" of
+ * set membership. This roughly corresponds to the rules UNION DOWN I and II,
+ * INTER DOWN I and II from Bansal et al IJCAR 2016, as well as rules for set
+ * difference.
+ */
+ void checkDownwardsClosure();
+ /**
+ * This implements an inference schema based on the "upwards closure" of
+ * set membership. This roughly corresponds to the rules UNION UP, INTER
+ * UP I and II from Bansal et al IJCAR 2016, as well as rules for set
+ * difference.
+ */
+ void checkUpwardsClosure();
+ /**
+ * This implements a strategy for splitting for set disequalities which
+ * roughly corresponds the SET DISEQUALITY rule from Bansal et al IJCAR 2016.
+ */
+ void checkDisequalities();
void addCarePairs(TNodeTrie* t1,
TNodeTrie* t2,
std::map< Node, EqcInfo* > d_eqc_info;
/** get or make eqc info */
EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
-
- void addEqualityToExp( Node a, Node b, std::vector< Node >& exp );
-
- void debugPrintSet( Node s, const char * c );
- /** sent lemma
- *
- * This flag is set to true during a full effort check if this theory
- * called d_out->lemma(...).
- */
- bool d_sentLemma;
- /** added fact
- *
- * This flag is set to true during a full effort check if this theory
- * added an internal fact to its equality engine.
- */
- bool d_addedFact;
/** full check incomplete
*
* This flag is set to true during a full effort check if this theory
* with a relation or extended function kind).
*/
bool d_full_check_incomplete;
- NodeMap d_proxy;
- NodeMap d_proxy_to_term;
- NodeSet d_lemmas_produced;
- std::vector< Node > d_set_eqc;
- std::map< Node, bool > d_set_eqc_relevant;
- std::map< Node, std::vector< Node > > d_set_eqc_list;
- std::map< TypeNode, Node > d_eqc_emptyset;
- std::map< TypeNode, Node > d_eqc_univset;
- std::map< Node, Node > d_eqc_singleton;
- std::map< TypeNode, Node > d_emptyset;
- std::map< TypeNode, Node > d_univset;
- std::map< Node, Node > d_congruent;
- std::map< Node, std::vector< Node > > d_nvar_sets;
- std::map< Node, Node > d_var_set;
std::map< Node, TypeNode > d_most_common_type;
std::map< Node, Node > d_most_common_type_term;
- std::map< Node, std::map< Node, Node > > d_pol_mems[2];
- std::map< Node, std::map< Node, Node > > d_members_index;
- std::map< Node, Node > d_singleton_index;
- std::map< Kind, std::map< Node, std::map< Node, Node > > > d_bop_index;
- std::map< Kind, std::vector< Node > > d_op_list;
- //cardinality
- private:
- /** is cardinality enabled?
- *
- * This flag is set to true during a full effort check if any constraint
- * involving cardinality constraints is asserted to this theory.
- */
- bool d_card_enabled;
- /** element types of sets for which cardinality is enabled */
- std::map<TypeNode, bool> d_t_card_enabled;
- std::map< Node, Node > d_eqc_to_card_term;
- NodeSet d_card_processed;
- std::map< Node, std::vector< Node > > d_card_parent;
- std::map< Node, std::map< Node, std::vector< Node > > > d_ff;
- std::map< Node, std::vector< Node > > d_nf;
- std::map< Node, Node > d_card_base;
- void checkCardBuildGraph( std::vector< Node >& lemmas );
- void registerCardinalityTerm( Node n, std::vector< Node >& lemmas );
- void checkCardCycles( std::vector< Node >& lemmas );
- void checkCardCyclesRec( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp, std::vector< Node >& lemmas );
- void checkNormalForms( std::vector< Node >& lemmas, std::vector< Node >& intro_sets );
- void checkNormalForm( Node eqc, std::vector< Node >& intro_sets );
- void checkMinCard( std::vector< Node >& lemmas );
-private: //for universe set
- NodeBoolMap d_var_elim;
- void lastCallEffortCheck();
-
- private:
- /** type constraint skolems
- *
- * The sets theory solver outputs equality lemmas of the form:
- * n = d_tc_skolem[n][tn]
- * where the type of d_tc_skolem[n][tn] is tn, and the type
- * of n is not a subtype of tn. This is required to handle benchmarks like
- * test/regress/regress0/sets/sets-of-sets-subtypes.smt2
- * where for s : (Set Int) and t : (Set Real), we have that
- * ( s = t ^ y in t ) implies ( exists k : Int. y = k )
- * The type constraint Skolem for (y, Int) is the skolemization of k above.
- */
- std::map<Node, std::map<TypeNode, Node> > d_tc_skolem;
- /** get type constraint skolem for n and tn */
- Node getTypeConstraintSkolem(Node n, TypeNode tn);
public:
void addSharedTerm(TNode);
void check(Theory::Effort);
-
- bool needsCheckLastEffort();
bool collectModelInfo(TheoryModel* m);
EqualityStatus getEqualityStatus(TNode a, TNode b);
- /**
- * Get the skolem cache of this theory, which manages a database of introduced
- * skolem variables used for various inferences.
- */
- SkolemCache& getSkolemCache() { return d_skCache; }
-
void preRegisterTerm(TNode node);
/** expandDefinition
void propagate(Theory::Effort);
- /** Process inference
- *
- * Argument lem specifies an inference inferred by this theory. If lem is
- * an IMPLIES node, then its antecendant is the explanation of the conclusion.
- *
- * Argument c is used for debugging, typically the name of the inference.
- *
- * This method may add facts to the equality engine of theory of sets.
- * Any (portion of) the conclusion of lem that is not sent to the equality
- * engine is added to the argument lemmas, which should be processed via the
- * caller of this method.
- */
- void processInference(Node lem, const char* c, std::vector<Node>& lemmas);
- /** Flush lemmas
- *
- * This sends lemmas on the output channel of the theory of sets.
- *
- * The argument preprocess indicates whether preprocessing should be applied
- * (by TheoryEngine) on each of lemmas.
- */
- void flushLemmas(std::vector<Node>& lemmas, bool preprocess = false);
- /** singular version of above */
- void flushLemma(Node lem, bool preprocess = false);
- /** Are we currently in conflict? */
- bool isInConflict() const;
- /** Have we sent out a lemma during a call to a full effort check? */
- bool sentLemma() const;
-
/** get default output channel */
OutputChannel* getOutputChannel();
+ /** get the valuation */
+ Valuation& getValuation();
private:
TheorySets& d_external;
- class Statistics {
- public:
- TimerStat d_getModelValueTime;
- TimerStat d_mergeTime;
- TimerStat d_processCard2Time;
- IntStat d_memberLemmas;
- IntStat d_disequalityLemmas;
- IntStat d_numVertices;
- IntStat d_numVerticesMax;
- IntStat d_numMergeEq1or2;
- IntStat d_numMergeEq3;
- IntStat d_numLeaves;
- IntStat d_numLeavesMax;
-
- Statistics();
- ~Statistics();
- } d_statistics;
-
/** Functions to handle callbacks from equality engine */
class NotifyClass : public eq::EqualityEngineNotify {
TheorySetsPrivate& d_theory;
/** Equality engine */
eq::EqualityEngine d_equalityEngine;
- context::CDO<bool> d_conflict;
- Node d_conflictNode;
-
/** Proagate out to output channel */
bool propagate(TNode);
void conflict(TNode, TNode);
bool isCareArg( Node n, unsigned a );
-public:
- bool isEntailed( Node n, bool pol );
+
+ public:
+ /** Is formula n entailed to have polarity pol in the current context? */
+ bool isEntailed(Node n, bool pol) { return d_state.isEntailed(n, pol); }
+ /** Is x entailed to be a member of set s in the current context? */
+ bool isMember(Node x, Node s);
private:
+ /** The state of the sets solver at full effort */
+ SolverState d_state;
+ /** The inference manager of the sets solver */
+ InferenceManager d_im;
/** subtheory solver for the theory of relations */
std::unique_ptr<TheorySetsRels> d_rels;
- /** the skolem cache */
- SkolemCache d_skCache;
+ /** subtheory solver for the theory of sets with cardinality */
+ std::unique_ptr<CardinalityExtension> d_cardSolver;
/** are relations enabled?
*
* This flag is set to true during a full effort check if any constraint
* involving relational constraints is asserted to this theory.
*/
bool d_rels_enabled;
+ /** is cardinality enabled?
+ *
+ * This flag is set to true during a full effort check if any constraint
+ * involving cardinality constraints is asserted to this theory.
+ */
+ bool d_card_enabled;
};/* class TheorySetsPrivate */
typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT;
typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator TC_IT;
-TheorySetsRels::TheorySetsRels(context::Context* c,
- context::UserContext* u,
- eq::EqualityEngine* eq,
- TheorySetsPrivate& set)
- : d_eqEngine(eq),
- d_sets_theory(set),
- d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)),
- d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)),
- d_shared_terms(u),
- d_satContext(c)
+TheorySetsRels::TheorySetsRels(SolverState& s,
+ InferenceManager& im,
+ eq::EqualityEngine& e,
+ context::UserContext* u)
+ : d_state(s), d_im(im), d_ee(e), d_shared_terms(u)
{
- d_eqEngine->addFunctionKind(PRODUCT);
- d_eqEngine->addFunctionKind(JOIN);
- d_eqEngine->addFunctionKind(TRANSPOSE);
- d_eqEngine->addFunctionKind(TCLOSURE);
- d_eqEngine->addFunctionKind(JOIN_IMAGE);
- d_eqEngine->addFunctionKind(IDEN);
- d_eqEngine->addFunctionKind(APPLY_CONSTRUCTOR);
+ d_trueNode = NodeManager::currentNM()->mkConst(true);
+ d_falseNode = NodeManager::currentNM()->mkConst(false);
+ d_ee.addFunctionKind(PRODUCT);
+ d_ee.addFunctionKind(JOIN);
+ d_ee.addFunctionKind(TRANSPOSE);
+ d_ee.addFunctionKind(TCLOSURE);
+ d_ee.addFunctionKind(JOIN_IMAGE);
+ d_ee.addFunctionKind(IDEN);
+ d_ee.addFunctionKind(APPLY_CONSTRUCTOR);
}
TheorySetsRels::~TheorySetsRels() {}
void TheorySetsRels::collectRelsInfo() {
Trace("rels") << "[sets-rels] Start collecting relational terms..." << std::endl;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine );
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_ee);
while( !eqcs_i.isFinished() ){
Node eqc_rep = (*eqcs_i);
- eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc_rep, d_eqEngine );
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc_rep, &d_ee);
TypeNode erType = eqc_rep.getType();
Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << " with type " << eqc_rep.getType() << std::endl;
NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR,
Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ),
join_image_term);
- if (d_sets_theory.isEntailed(new_membership, true))
+ if (d_state.isEntailed(new_membership, true))
{
++mem_rep_it;
++mem_rep_exp_it;
Node r1_rep = getRepresentative(join_rel[0]);
Node r2_rep = getRepresentative(join_rel[1]);
TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0];
- Node shared_x = d_sets_theory.getSkolemCache().mkTypedSkolemCached(
+ Node shared_x = d_state.getSkolemCache().mkTypedSkolemCached(
shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj");
Datatype dt = join_rel[0].getType().getSetElementType().getDatatype();
unsigned int s1_len = join_rel[0].getType().getSetElementType().getTupleLength();
void TheorySetsRels::doPendingInfers()
{
// process the inferences in d_pending
- if (!d_sets_theory.isInConflict())
+ if (!d_state.isInConflict())
{
- std::vector<Node> lemmas;
for (const Node& p : d_pending)
{
- d_sets_theory.processInference(p, "rels", lemmas);
- if (d_sets_theory.isInConflict())
+ if (p.getKind() == IMPLIES)
+ {
+ processInference(p[1], p[0], "rels");
+ }
+ else
+ {
+ processInference(p, d_trueNode, "rels");
+ }
+ if (d_state.isInConflict())
{
break;
}
}
// if we are still not in conflict, send lemmas
- if (!d_sets_theory.isInConflict())
+ if (!d_state.isInConflict())
{
- d_sets_theory.flushLemmas(lemmas);
+ d_im.flushPendingLemmas();
}
}
d_pending.clear();
}
+ void TheorySetsRels::processInference(Node conc, Node exp, const char* c)
+ {
+ Trace("sets-pinfer") << "Process inference: " << exp << " => " << conc
+ << std::endl;
+ if (!d_state.isEntailed(exp, true))
+ {
+ Trace("sets-pinfer") << " must assert as lemma" << std::endl;
+ // we wrap the spurious explanation into a splitting lemma
+ Node lem = NodeManager::currentNM()->mkNode(OR, exp.negate(), conc);
+ d_im.assertInference(lem, d_trueNode, c, 1);
+ return;
+ }
+ // try to assert it as a fact
+ d_im.assertInference(conc, exp, c);
+ }
+
bool TheorySetsRels::isRelationKind( Kind k ) {
- return k == kind::TRANSPOSE || k == kind::PRODUCT || k == kind::JOIN || k == kind::TCLOSURE;
+ return k == TRANSPOSE || k == PRODUCT || k == JOIN || k == TCLOSURE
+ || k == IDEN || k == JOIN_IMAGE;
}
Node TheorySetsRels::getRepresentative( Node t ) {
- if( d_eqEngine->hasTerm( t ) ){
- return d_eqEngine->getRepresentative( t );
- }else{
+ if (d_ee.hasTerm(t))
+ {
+ return d_ee.getRepresentative(t);
+ }
+ else
+ {
return t;
}
}
- bool TheorySetsRels::hasTerm( Node a ){
- return d_eqEngine->hasTerm( a );
- }
+ bool TheorySetsRels::hasTerm(Node a) { return d_ee.hasTerm(a); }
bool TheorySetsRels::areEqual( Node a, Node b ){
Assert(a.getType() == b.getType());
if(a == b) {
return true;
} else if( hasTerm( a ) && hasTerm( b ) ){
- return d_eqEngine->areEqual( a, b );
+ return d_ee.areEqual(a, b);
} else if(a.getType().isTuple()) {
bool equal = true;
for(unsigned int i = 0; i < a.getType().getTupleLength(); i++) {
Node skEq =
skolem.eqNode(NodeManager::currentNM()->mkNode(kind::SINGLETON, n));
// force lemma to be sent immediately
- d_sets_theory.getOutputChannel()->lemma(skEq);
+ d_im.assertInference(skEq, d_trueNode, "shared-term");
+ d_im.flushPendingLemmas();
d_shared_terms.insert(n);
}
}
#include "context/cdhashset.h"
#include "context/cdlist.h"
+#include "theory/sets/inference_manager.h"
#include "theory/sets/rels_utils.h"
+#include "theory/sets/solver_state.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
public:
- TheorySetsRels(context::Context* c,
- context::UserContext* u,
- eq::EqualityEngine* eq,
- TheorySetsPrivate& set);
+ TheorySetsRels(SolverState& s,
+ InferenceManager& im,
+ eq::EqualityEngine& e,
+ context::UserContext* u);
~TheorySetsRels();
/**
/** True and false constant nodes */
Node d_trueNode;
Node d_falseNode;
- /** The parent theory of sets object */
- TheorySetsPrivate& d_sets_theory;
- /** pointer to the equality engine of the theory of sets */
- eq::EqualityEngine* d_eqEngine;
+
+ /** Reference to the state object for the theory of sets */
+ SolverState& d_state;
+ /** Reference to the inference manager for the theory of sets */
+ InferenceManager& d_im;
+ /** Reference to the equality engine of theory of sets */
+ eq::EqualityEngine& d_ee;
/** A list of pending inferences to process */
std::vector<Node> d_pending;
NodeSet d_shared_terms;
std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_tcr_tcGraph;
std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps;
- context::Context* d_satContext;
-
private:
/** Send infer
*
* the equality engine.
*/
void doPendingInfers();
+ /** Process inference
+ *
+ * A wrapper around d_im.assertInference that ensures that we do not send
+ * inferences with explanations that are not entailed.
+ *
+ * Argument c is used for debugging, typically the name of the inference.
+ */
+ void processInference(Node conc, Node exp, const char* c);
/** Methods used in full effort */
void check();
projects / cvc5.git / commitdiff