From bfd8e5426cfa5d8955e62c822d61536e42b3eff9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 Sep 2019 12:56:21 -0500 Subject: [PATCH] Split, refactor and document the theory of sets (#3085) --- src/CMakeLists.txt | 6 + src/theory/sets/cardinality_extension.cpp | 911 +++++++++++ src/theory/sets/cardinality_extension.h | 347 +++++ src/theory/sets/inference_manager.cpp | 229 +++ src/theory/sets/inference_manager.h | 159 ++ src/theory/sets/solver_state.cpp | 580 +++++++ src/theory/sets/solver_state.h | 290 ++++ src/theory/sets/theory_sets.cpp | 4 - src/theory/sets/theory_sets.h | 1 - src/theory/sets/theory_sets_private.cpp | 1718 ++++----------------- src/theory/sets/theory_sets_private.h | 248 +-- src/theory/sets/theory_sets_rels.cpp | 94 +- src/theory/sets/theory_sets_rels.h | 31 +- 13 files changed, 3011 insertions(+), 1607 deletions(-) create mode 100644 src/theory/sets/cardinality_extension.cpp create mode 100644 src/theory/sets/cardinality_extension.h create mode 100644 src/theory/sets/inference_manager.cpp create mode 100644 src/theory/sets/inference_manager.h create mode 100644 src/theory/sets/solver_state.cpp create mode 100644 src/theory/sets/solver_state.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4f56be8a9..db92d2b3f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -618,10 +618,16 @@ libcvc4_add_sources( 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 diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp new file mode 100644 index 000000000..37dfedd15 --- /dev/null +++ b/src/theory/sets/cardinality_extension.cpp @@ -0,0 +1,911 @@ +/********************* */ +/*! \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 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& setEqc = d_state.getSetsEqClasses(); + for (const Node& eqc : setEqc) + { + const std::vector& 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 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& setEqc = d_state.getSetsEqClasses(); + d_oSetEqc.clear(); + d_card_parent.clear(); + for (const Node& s : setEqc) + { + std::vector curr; + std::vector 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& curr, + std::vector& 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 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& 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 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 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 card_parents; + std::vector 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 conc; + std::vector 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 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& 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 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& 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= 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& 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 comps; + std::map > >::iterator it = + d_ff.find(eqc); + if (it != d_ff.end()) + { + for (std::pair >& 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 >& ffeqc = d_ff[eqc]; + Assert(d_nf.find(eqc) == d_nf.end()); + std::vector& 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 c; + c.push_back(base); + c.push_back(comps[j]); + std::vector only[2]; + std::vector 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& nvsets = d_state.getNonVariableSets(eqc); + if (nvsets.empty()) + { + // no non-variable sets + return; + } + std::map > 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& 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& 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& pmemsE = d_state.getMembers(eqc); + if (pmemsE.empty()) + { + // no members, trivial + continue; + } + std::vector exp; + std::vector members; + Node cardTerm; + std::map::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& 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& els, + const std::map& mvals) +{ + TypeNode elementType = eqc.getType().getSetElementType(); + if (isModelValueBasic(eqc)) + { + std::map::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() <= LONG_MAX, + "Exceeded LONG_MAX in sets model"); + unsigned vu = v.getConst().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::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 diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h new file mode 100644 index 000000000..d9c5dd64a --- /dev/null +++ b/src/theory/sets/cardinality_extension.h @@ -0,0 +1,347 @@ +/********************* */ +/*! \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 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& els, + const std::map& 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& getOrderedSetsEqClasses() { return d_oSetEqc; } + + private: + /** constants */ + Node d_zero; + /** the empty vector */ + std::vector 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& curr, + std::vector& 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& intro_sets); + /** + * Called for each equivalence class, in order of d_oSetEqc, by the above + * function. + */ + void checkNormalForm(Node eqc, std::vector& intro_sets); + /** element types of sets for which cardinality is enabled */ + std::map 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 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 d_oSetEqc; + /** + * This maps set terms to the set of representatives of their "parent" sets, + * see checkCardCycles. + */ + std::map > d_card_parent; + /** + * Maps equivalence classes + set terms in that equivalence class to their + * "flat form" (see checkNormalForms). + */ + std::map > > d_ff; + /** Maps equivalence classes to their "normal form" (see checkNormalForms). */ + std::map > 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 d_localBase; +}; /* class CardinalityExtension */ + +} // namespace sets +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp new file mode 100644 index 000000000..e29e574be --- /dev/null +++ b/src/theory/sets/inference_manager.cpp @@ -0,0 +1,229 @@ +/********************* */ +/*! \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& 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& 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& conc, + std::vector& 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& 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 diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h new file mode 100644 index 000000000..29b0e2bca --- /dev/null +++ b/src/theory/sets/inference_manager.h @@ -0,0 +1,159 @@ +/********************* */ +/*! \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 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& exp, + const char* c, + int inferType = 0); + /** same as above, where conc is interpreted as a conjunction */ + void assertInference(std::vector& 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& conc, + std::vector& 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& 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 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 */ diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp new file mode 100644 index 000000000..76c7c3884 --- /dev/null +++ b/src/theory/sets/solver_state.cpp @@ -0,0 +1,580 @@ +/********************* */ +/*! \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& binr1 = d_bop_index[nk][r1]; + std::map::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& exp) const +{ + if (a != b) + { + Assert(areEqual(a, b)); + exp.push_back(a.eqNode(b)); + } +} + +Node SolverState::getEmptySetEqClass(TypeNode tn) const +{ + std::map::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::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::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 > >::const_iterator itk = + d_bop_index.find(k); + if (itk == d_bop_index.end()) + { + return Node::null(); + } + std::map >::const_iterator it1 = + itk->second.find(r1); + if (it1 == itk->second.end()) + { + return Node::null(); + } + std::map::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 >::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::const_iterator itsb = d_eqc_singleton.find(b); + std::map >::const_iterator itpmb = + d_pol_mems[1].find(b); + std::vector prev; + for (const std::pair& 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& 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::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::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::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::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& SolverState::getNonVariableSets(Node r) const +{ + std::map >::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::const_iterator it = d_var_set.find(r); + if (it != d_var_set.end()) + { + return it->second; + } + return Node::null(); +} +const std::map& SolverState::getMembers(Node r) const +{ + return getMembersInternal(r, 0); +} +const std::map& SolverState::getNegativeMembers(Node r) const +{ + return getMembersInternal(r, 1); +} +const std::map& SolverState::getMembersInternal(Node r, + unsigned i) const +{ + std::map >::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 >::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 > >& +SolverState::getBinaryOpIndex() const +{ + return d_bop_index; +} +const std::map >& 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 diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h new file mode 100644 index 000000000..2b4d93ed3 --- /dev/null +++ b/src/theory/sets/solver_state.h @@ -0,0 +1,290 @@ +/********************* */ +/*! \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 +#include + +#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 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& 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 (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& 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& 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& getMembers(Node r) const; + /** Get negative members of the set equivalence class r, similar to above */ + const std::map& 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 (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 > >& + 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 >& 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 d_emptyVec; + std::map d_emptyMap; + /** Whether or not we are in conflict. This flag is SAT context dependent. */ + context::CDO 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 d_set_eqc; + /** Maps types to the equivalence class containing empty set of that type */ + std::map d_eqc_emptyset; + /** Maps types to the equivalence class containing univ set of that type */ + std::map d_eqc_univset; + /** Maps equivalence classes to a singleton set that exists in it. */ + std::map d_eqc_singleton; + /** Map from terms to the representative of their congruence class */ + std::map d_congruent; + /** Map from equivalence classes to the list of non-variable sets in it */ + std::map > d_nvar_sets; + /** Map from equivalence classes to a variable sets in it */ + std::map 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 > 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 > d_tc_skolem; + /** Map from types to empty set of that type */ + std::map d_emptyset; + /** Map from types to universe set of that type */ + std::map 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 > d_members_index; + /** Term index for SINGLETON */ + std::map d_singleton_index; + /** Indices for the binary kinds INTERSECT, SETMINUS and UNION. */ + std::map > > d_bop_index; + // -------------------------------- end term indices + std::map > 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& getMembersInternal(Node r, unsigned i) const; +}; /* class TheorySetsPrivate */ + +} // namespace sets +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H */ diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 563a981b1..869cb8926 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -52,10 +52,6 @@ void TheorySets::check(Effort e) { d_internal->check(e); } -bool TheorySets::needsCheckLastEffort() { - return d_internal->needsCheckLastEffort(); -} - bool TheorySets::collectModelInfo(TheoryModel* m) { return d_internal->collectModelInfo(m); diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 414ba4b28..4c145aedb 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -44,7 +44,6 @@ class TheorySets : public Theory void addSharedTerm(TNode) override; void check(Effort) override; - bool needsCheckLastEffort() override; bool collectModelInfo(TheoryModel* m) override; void computeCareGraph() override; Node explain(TNode) override; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 6e71ab2ad..472395e1b 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -40,21 +40,17 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, 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 ); @@ -67,8 +63,6 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_equalityEngine.addFunctionKind(kind::MEMBER); d_equalityEngine.addFunctionKind(kind::SUBSET); - - d_equalityEngine.addFunctionKind(kind::CARD); } TheorySetsPrivate::~TheorySetsPrivate(){ @@ -89,7 +83,8 @@ void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2){ } 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 ); @@ -138,7 +133,8 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){ bool add = true; for( int j=0; jmkNode( kind::AND, m2[1].eqNode( s1 ), m2 ); if( s1.getKind()==kind::SINGLETON ){ if( s1[0]!=m2[0] ){ @@ -159,8 +155,7 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){ }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; } } @@ -204,32 +199,8 @@ TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo( TNode n, bool d } } - -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); @@ -241,131 +212,33 @@ bool TheorySetsPrivate::ee_areCareDisequal( Node a, Node b ) { 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 >::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; kfirst, 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] ); @@ -384,8 +257,7 @@ bool TheorySetsPrivate::assertFact( Node fact, Node exp ){ } }else{ Trace("sets-prop") << "Propagate mem-eq conflict : " << exp << std::endl; - d_conflict = true; - d_external.d_out->conflict( exp ); + d_state.setConflict(exp); } } } @@ -404,128 +276,35 @@ bool TheorySetsPrivate::assertFact( Node fact, Node 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; imkNode( 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 eqcTypeCount; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); @@ -533,13 +312,13 @@ void TheorySetsPrivate::fullEffortCheck(){ 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; } @@ -561,95 +340,29 @@ void TheorySetsPrivate::fullEffortCheck(){ 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& binr1 = d_bop_index[n.getKind()][r1]; - std::map::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; } @@ -662,6 +375,8 @@ void TheorySetsPrivate::fullEffortCheck(){ ++eqcs_i; } + Trace("sets-eqc") << "...finished equality engine." << std::endl; + if (Trace.isOn("sets-state")) { Trace("sets-state") << "Equivalence class counters:" << std::endl; @@ -672,103 +387,103 @@ void TheorySetsPrivate::fullEffortCheck(){ } } - 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& 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& 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& 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 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& 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& smems = d_state.getMembers(s); + if (!smems.empty()) + { + for (const std::pair& 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; } } @@ -776,19 +491,28 @@ void TheorySetsPrivate::checkSubtypes( std::vector< Node >& lemmas ) { } } } + 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; jsecond.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& sec = d_state.getSetsEqClasses(); + for (const Node& s : sec) + { + const std::vector& nvsets = d_state.getNonVariableSets(s); + if (!nvsets.empty()) + { + const std::map& smem = d_state.getMembers(s); + for (const Node& nv : nvsets) + { + if (!d_state.isCongruent(nv)) + { + for (const std::pair& 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; @@ -798,23 +522,27 @@ void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) { 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"); } } } @@ -824,160 +552,176 @@ void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) { } } -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 > >& boi = + d_state.getBinaryOpIndex(); + for (const std::pair > >& + itb : boi) + { + Kind k = itb.first; + Trace("sets") << "TheorySetsPrivate: check upwards closure " << k << "..." + << std::endl; + for (const std::pair >& 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& r1mem = d_state.getMembers(r1); + if (!r1mem.empty() || k == kind::UNION) + { + for (const std::pair& 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& r2mem = d_state.getMembers(r2); + const std::map& 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& 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::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::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& 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& 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& smems = d_state.getMembers(s); + for (const std::pair& 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; } } @@ -988,9 +732,10 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) { } } -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; @@ -998,7 +743,7 @@ void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) { 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 @@ -1021,9 +766,10 @@ void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) { 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; } } @@ -1032,713 +778,6 @@ void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) { } } -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 >::iterator itn = d_nvar_sets.find( eqc ); - if( itn!=d_nvar_sets.end() ){ - for( unsigned j=0; jsecond.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; kmkNode( 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 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; imkNode( 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; jsecond.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 card_parents; - std::vector< int > card_parent_ids; - //check if equal to a parent - for( unsigned e=0; e conc; - std::vector< int > sib_emp_indices; - if( is_union ){ - for( unsigned s=0; s " << 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::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 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& 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=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; ksecond.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 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]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::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; jsecond.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& 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; jsecond ) ){ - 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; ilemma(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::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 *****************************/ @@ -1746,10 +785,10 @@ Node TheorySetsPrivate::getTypeConstraintSkolem(Node n, TypeNode tn) 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; @@ -1757,14 +796,15 @@ void TheorySetsPrivate::check(Theory::Effort level) { //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(); } @@ -1774,19 +814,13 @@ void TheorySetsPrivate::check(Theory::Effort level) { 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); } @@ -1800,7 +834,8 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, 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 > currentPairs; for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { @@ -1808,8 +843,8 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, 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) ){ @@ -1820,9 +855,10 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, //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)); } } } @@ -1853,7 +889,8 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, ++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 ); } } @@ -1867,7 +904,7 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, { 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); } @@ -1879,16 +916,22 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, } 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 >& ol = d_state.getOperatorList(); + for (const std::pair >& 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 index; unsigned arity = 0; //populate indices - for( unsigned i=0; isecond.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) @@ -1978,50 +1021,41 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m) 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& 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& emems = d_state.getMembers(eqc); + if (!emems.empty()) + { + for (const std::pair& 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() <= LONG_MAX, "Exceeded LONG_MAX in sets model"); - unsigned vu = v.getConst().getNumerator().toUnsignedInt(); - Assert( els.size()<=vu ); - while( els.size()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; jmkModelValueElementsFor(val, eqc, els, mvals); } Node rep = NormalForm::mkBop( kind::UNION, els, eqc.getType() ); rep = Rewriter::rewrite( rep ); @@ -2041,13 +1075,6 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m) /********************** 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& conjunctions) { Assert(conjunctions.size() > 0); @@ -2079,52 +1106,9 @@ Node mkAnd(const std::vector& conjunctions) { 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) { } @@ -2133,7 +1117,8 @@ bool TheorySetsPrivate::propagate(TNode literal) { 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; } @@ -2141,37 +1126,19 @@ bool TheorySetsPrivate::propagate(TNode literal) { // 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& 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); } @@ -2179,12 +1146,11 @@ void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* 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) @@ -2254,7 +1220,6 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou //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]) @@ -2263,7 +1228,6 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou if (!in[0].getType().isSet() || !options::setsExt()) { outSubstitutions.addSubstitution(in[0], in[1]); - var = in[0]; status = Theory::PP_ASSERT_STATUS_SOLVED; } } @@ -2273,7 +1237,6 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou if (!in[1].getType().isSet() || !options::setsExt()) { outSubstitutions.addSubstitution(in[1], in[0]); - var = in[1]; status = Theory::PP_ASSERT_STATUS_SOLVED; } } @@ -2285,25 +1248,10 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou } } } - - 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 *****************************/ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index fcb5859d4..0468e5fb7 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -22,7 +22,9 @@ #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" @@ -32,51 +34,73 @@ namespace theory { 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 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, @@ -105,23 +129,7 @@ private: 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 @@ -129,69 +137,8 @@ private: * 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 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 > d_tc_skolem; - /** get type constraint skolem for n and tn */ - Node getTypeConstraintSkolem(Node n, TypeNode tn); public: @@ -210,8 +157,6 @@ private: //for universe set void addSharedTerm(TNode); void check(Theory::Effort); - - bool needsCheckLastEffort(); bool collectModelInfo(TheoryModel* m); @@ -221,12 +166,6 @@ private: //for universe set 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 @@ -266,58 +205,14 @@ private: //for universe set 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& 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& 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; @@ -340,9 +235,6 @@ private: //for universe set /** Equality engine */ eq::EqualityEngine d_equalityEngine; - context::CDO d_conflict; - Node d_conflictNode; - /** Proagate out to output channel */ bool propagate(TNode); @@ -350,20 +242,34 @@ private: //for universe set 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 d_rels; - /** the skolem cache */ - SkolemCache d_skCache; + /** subtheory solver for the theory of sets with cardinality */ + std::unique_ptr 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 */ diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 2bbaa3bc8..e2b779cbd 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -32,24 +32,21 @@ typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator 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(true)), - d_falseNode(NodeManager::currentNM()->mkConst(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() {} @@ -188,10 +185,10 @@ void TheorySetsRels::check(Theory::Effort level) 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; @@ -307,7 +304,7 @@ void TheorySetsRels::check(Theory::Effort level) 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; @@ -793,7 +790,7 @@ void TheorySetsRels::check(Theory::Effort level) 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(); @@ -1058,41 +1055,65 @@ void TheorySetsRels::check(Theory::Effort level) void TheorySetsRels::doPendingInfers() { // process the inferences in d_pending - if (!d_sets_theory.isInConflict()) + if (!d_state.isInConflict()) { - std::vector 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()); @@ -1100,7 +1121,7 @@ void TheorySetsRels::check(Theory::Effort level) 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++) { @@ -1146,7 +1167,8 @@ void TheorySetsRels::check(Theory::Effort level) 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); } } diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index d4a91007b..3a0458309 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -21,7 +21,9 @@ #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" @@ -63,10 +65,10 @@ class TheorySetsRels { 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(); /** @@ -83,10 +85,13 @@ private: /** 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 d_pending; NodeSet d_shared_terms; @@ -113,8 +118,6 @@ private: std::map< Node, std::map< Node, std::unordered_set > > d_tcr_tcGraph; std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps; - context::Context* d_satContext; - private: /** Send infer * @@ -133,6 +136,14 @@ private: * 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(); -- 2.30.2