src/theory/bags/theory_bags.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mudathir Mohamed, Haniel Barbosa, Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Bags theory.
  14  */
  15
  16 #include "theory/bags/theory_bags.h"
  17
  18 #include "proof/proof_checker.h"
  19 #include "smt/logic_exception.h"
  20 #include "theory/bags/normal_form.h"
  21 #include "theory/rewriter.h"
  22 #include "theory/theory_model.h"
  23
  24 using namespace cvc5::kind;
  25
  26 namespace cvc5 {
  27 namespace theory {
  28 namespace bags {
  29
  30 TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
  31     : Theory(THEORY_BAGS, env, out, valuation),
  32       d_state(getSatContext(), getUserContext(), valuation),
  33       d_im(*this, d_state, d_pnm),
  34       d_ig(&d_state, &d_im),
  35       d_notify(*this, d_im),
  36       d_statistics(),
  37       d_rewriter(&d_statistics.d_rewrites),
  38       d_termReg(d_state, d_im),
  39       d_solver(d_state, d_im, d_termReg)
  40 {
  41   // use the official theory state and inference manager objects
  42   d_theoryState = &d_state;
  43   d_inferManager = &d_im;
  44 }
  45
  46 TheoryBags::~TheoryBags() {}
  47
  48 TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; }
  49
  50 ProofRuleChecker* TheoryBags::getProofChecker() { return nullptr; }
  51
  52 bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi)
  53 {
  54   esi.d_notify = &d_notify;
  55   esi.d_name = "theory::bags::ee";
  56   return true;
  57 }
  58
  59 void TheoryBags::finishInit()
  60 {
  61   Assert(d_equalityEngine != nullptr);
  62
  63   // choice is used to eliminate witness
  64   d_valuation.setUnevaluatedKind(WITNESS);
  65
  66   // functions we are doing congruence over
  67   d_equalityEngine->addFunctionKind(UNION_MAX);
  68   d_equalityEngine->addFunctionKind(UNION_DISJOINT);
  69   d_equalityEngine->addFunctionKind(INTERSECTION_MIN);
  70   d_equalityEngine->addFunctionKind(DIFFERENCE_SUBTRACT);
  71   d_equalityEngine->addFunctionKind(DIFFERENCE_REMOVE);
  72   d_equalityEngine->addFunctionKind(BAG_COUNT);
  73   d_equalityEngine->addFunctionKind(DUPLICATE_REMOVAL);
  74   d_equalityEngine->addFunctionKind(MK_BAG);
  75   d_equalityEngine->addFunctionKind(BAG_CARD);
  76   d_equalityEngine->addFunctionKind(BAG_FROM_SET);
  77   d_equalityEngine->addFunctionKind(BAG_TO_SET);
  78 }
  79
  80 void TheoryBags::postCheck(Effort effort)
  81 {
  82   d_im.doPendingFacts();
  83   // TODO issue #78: add Assert(d_strat.isStrategyInit());
  84   if (!d_state.isInConflict() && !d_valuation.needCheck())
  85   // TODO issue #78:  add && d_strat.hasStrategyEffort(e))
  86   {
  87     Trace("bags::TheoryBags::postCheck") << "effort: " << std::endl;
  88
  89     // TODO issue #78: add ++(d_statistics.d_checkRuns);
  90     bool sentLemma = false;
  91     bool hadPending = false;
  92     Trace("bags-check") << "Full effort check..." << std::endl;
  93     do
  94     {
  95       d_im.reset();
  96       // TODO issue #78: add ++(d_statistics.d_strategyRuns);
  97       Trace("bags-check") << "  * Run strategy..." << std::endl;
  98       // TODO issue #78: add runStrategy(e);
  99
 100       d_solver.postCheck();
 101
 102       // remember if we had pending facts or lemmas
 103       hadPending = d_im.hasPending();
 104       // Send the facts *and* the lemmas. We send lemmas regardless of whether
 105       // we send facts since some lemmas cannot be dropped. Other lemmas are
 106       // otherwise avoided by aborting the strategy when a fact is ready.
 107       d_im.doPending();
 108       // Did we successfully send a lemma? Notice that if hasPending = true
 109       // and sentLemma = false, then the above call may have:
 110       // (1) had no pending lemmas, but successfully processed pending facts,
 111       // (2) unsuccessfully processed pending lemmas.
 112       // In either case, we repeat the strategy if we are not in conflict.
 113       sentLemma = d_im.hasSentLemma();
 114       if (Trace.isOn("bags-check"))
 115       {
 116         // TODO: clean this Trace("bags-check") << "  ...finish run strategy: ";
 117         Trace("bags-check") << (hadPending ? "hadPending " : "");
 118         Trace("bags-check") << (sentLemma ? "sentLemma " : "");
 119         Trace("bags-check") << (d_state.isInConflict() ? "conflict " : "");
 120         if (!hadPending && !sentLemma && !d_state.isInConflict())
 121         {
 122           Trace("bags-check") << "(none)";
 123         }
 124         Trace("bags-check") << std::endl;
 125       }
 126       // repeat if we did not add a lemma or conflict, and we had pending
 127       // facts or lemmas.
 128     } while (!d_state.isInConflict() && !sentLemma && hadPending);
 129   }
 130   Trace("bags-check") << "Theory of bags, done check : " << effort << std::endl;
 131   Assert(!d_im.hasPendingFact());
 132   Assert(!d_im.hasPendingLemma());
 133 }
 134
 135 void TheoryBags::notifyFact(TNode atom,
 136                             bool polarity,
 137                             TNode fact,
 138                             bool isInternal)
 139 {
 140 }
 141
 142 bool TheoryBags::collectModelValues(TheoryModel* m,
 143                                     const std::set<Node>& termSet)
 144 {
 145   Trace("bags-model") << "TheoryBags : Collect model values" << std::endl;
 146
 147   Trace("bags-model") << "Term set: " << termSet << std::endl;
 148
 149   std::set<Node> processedBags;
 150
 151   // get the relevant bag equivalence classes
 152   for (const Node& n : termSet)
 153   {
 154     TypeNode tn = n.getType();
 155     if (!tn.isBag())
 156     {
 157       // we are only concerned here about bag terms
 158       continue;
 159     }
 160     Node r = d_state.getRepresentative(n);
 161     if (processedBags.find(r) != processedBags.end())
 162     {
 163       // skip bags whose representatives are already processed
 164       continue;
 165     }
 166
 167     processedBags.insert(r);
 168
 169     std::set<Node> solverElements = d_state.getElements(r);
 170     std::set<Node> elements;
 171     // only consider terms in termSet and ignore other elements in the solver
 172     std::set_intersection(termSet.begin(),
 173                           termSet.end(),
 174                           solverElements.begin(),
 175                           solverElements.end(),
 176                           std::inserter(elements, elements.begin()));
 177     Trace("bags-model") << "Elements of bag " << n << " are: " << std::endl
 178                         << elements << std::endl;
 179     std::map<Node, Node> elementReps;
 180     for (const Node& e : elements)
 181     {
 182       Node key = d_state.getRepresentative(e);
 183       Node countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, r);
 184       Node value = d_state.getRepresentative(countTerm);
 185       elementReps[key] = value;
 186     }
 187     Node rep = NormalForm::constructBagFromElements(tn, elementReps);
 188     rep = Rewriter::rewrite(rep);
 189
 190     Trace("bags-model") << "rep of " << n << " is: " << rep << std::endl;
 191     for (std::pair<Node, Node> pair : elementReps)
 192     {
 193       m->assertSkeleton(pair.first);
 194       m->assertSkeleton(pair.second);
 195     }
 196     m->assertEquality(rep, n, true);
 197     m->assertSkeleton(rep);
 198   }
 199   return true;
 200 }
 201
 202 TrustNode TheoryBags::explain(TNode node) { return d_im.explainLit(node); }
 203
 204 Node TheoryBags::getModelValue(TNode node) { return Node::null(); }
 205
 206 void TheoryBags::preRegisterTerm(TNode n)
 207 {
 208   Trace("bags::TheoryBags::preRegisterTerm") << n << std::endl;
 209   switch (n.getKind())
 210   {
 211     case BAG_CARD:
 212     case BAG_FROM_SET:
 213     case BAG_TO_SET:
 214     case BAG_IS_SINGLETON:
 215     {
 216       std::stringstream ss;
 217       ss << "Term of kind " << n.getKind() << " is not supported yet";
 218       throw LogicException(ss.str());
 219     }
 220     default: break;
 221   }
 222 }
 223
 224 void TheoryBags::presolve() {}
 225
 226 /**************************** eq::NotifyClass *****************************/
 227
 228 void TheoryBags::eqNotifyNewClass(TNode n) {}
 229
 230 void TheoryBags::eqNotifyMerge(TNode n1, TNode n2) {}
 231
 232 void TheoryBags::eqNotifyDisequal(TNode n1, TNode n2, TNode reason) {}
 233
 234 void TheoryBags::NotifyClass::eqNotifyNewClass(TNode n)
 235 {
 236   Debug("bags-eq") << "[bags-eq] eqNotifyNewClass:"
 237                    << " n = " << n << std::endl;
 238   d_theory.eqNotifyNewClass(n);
 239 }
 240
 241 void TheoryBags::NotifyClass::eqNotifyMerge(TNode n1, TNode n2)
 242 {
 243   Debug("bags-eq") << "[bags-eq] eqNotifyMerge:"
 244                    << " n1 = " << n1 << " n2 = " << n2 << std::endl;
 245   d_theory.eqNotifyMerge(n1, n2);
 246 }
 247
 248 void TheoryBags::NotifyClass::eqNotifyDisequal(TNode n1, TNode n2, TNode reason)
 249 {
 250   Debug("bags-eq") << "[bags-eq] eqNotifyDisequal:"
 251                    << " n1 = " << n1 << " n2 = " << n2 << " reason = " << reason
 252                    << std::endl;
 253   d_theory.eqNotifyDisequal(n1, n2, reason);
 254 }
 255
 256 }  // namespace bags
 257 }  // namespace theory
 258 }  // namespace cvc5