src/theory/sets/inference_manager.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Gereon Kremer, Aina Niemetz
   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  * Implementation of the inference manager for the theory of sets.
  14  */
  15
  16 #include "theory/sets/inference_manager.h"
  17
  18 #include "options/sets_options.h"
  19 #include "theory/rewriter.h"
  20
  21 using namespace std;
  22 using namespace cvc5::kind;
  23
  24 namespace cvc5 {
  25 namespace theory {
  26 namespace sets {
  27
  28 InferenceManager::InferenceManager(Env& env, Theory& t, SolverState& s)
  29     : InferenceManagerBuffered(env, t, s, "theory::sets::"), d_state(s)
  30 {
  31   d_true = NodeManager::currentNM()->mkConst(true);
  32   d_false = NodeManager::currentNM()->mkConst(false);
  33 }
  34
  35 bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int inferType)
  36 {
  37   // should we send this fact out as a lemma?
  38   if ((options().sets.setsInferAsLemmas && inferType != -1) || inferType == 1)
  39   {
  40     if (d_state.isEntailed(fact, true))
  41     {
  42       return false;
  43     }
  44     Node lem = fact;
  45     if (exp != d_true)
  46     {
  47       lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
  48     }
  49     addPendingLemma(lem, id);
  50     return true;
  51   }
  52   Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
  53                      << std::endl;
  54   if (fact.isConst())
  55   {
  56     // either trivial or a conflict
  57     if (fact == d_false)
  58     {
  59       Trace("sets-lemma") << "Conflict : " << exp << std::endl;
  60       conflict(exp, id);
  61       return true;
  62     }
  63     return false;
  64   }
  65   else if (fact.getKind() == AND
  66            || (fact.getKind() == NOT && fact[0].getKind() == OR))
  67   {
  68     bool ret = false;
  69     Node f = fact.getKind() == NOT ? fact[0] : fact;
  70     for (unsigned i = 0; i < f.getNumChildren(); i++)
  71     {
  72       Node factc = fact.getKind() == NOT ? f[i].negate() : f[i];
  73       bool tret = assertFactRec(factc, id, exp, inferType);
  74       ret = ret || tret;
  75       if (d_state.isInConflict())
  76       {
  77         return true;
  78       }
  79     }
  80     return ret;
  81   }
  82   bool polarity = fact.getKind() != NOT;
  83   TNode atom = polarity ? fact : fact[0];
  84   if (d_state.isEntailed(atom, polarity))
  85   {
  86     return false;
  87   }
  88   // things we can assert to equality engine
  89   if (atom.getKind() == MEMBER
  90       || (atom.getKind() == EQUAL && atom[0].getType().isSet()))
  91   {
  92     // send to equality engine
  93     if (assertSetsFact(atom, polarity, id, exp))
  94     {
  95       // return true if this wasn't redundant
  96       return true;
  97     }
  98   }
  99   else
 100   {
 101     // must send as lemma
 102     Node lem = fact;
 103     if (exp != d_true)
 104     {
 105       lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
 106     }
 107     addPendingLemma(lem, id);
 108     return true;
 109   }
 110   return false;
 111 }
 112
 113 bool InferenceManager::assertSetsFact(Node atom,
 114                                       bool polarity,
 115                                       InferenceId id,
 116                                       Node exp)
 117 {
 118   Node conc = polarity ? atom : atom.notNode();
 119   return assertInternalFact(
 120       atom, polarity, id, PfRule::THEORY_INFERENCE, {exp}, {conc});
 121 }
 122
 123 void InferenceManager::assertInference(Node fact,
 124                                        InferenceId id,
 125                                        Node exp,
 126                                        int inferType)
 127 {
 128   if (assertFactRec(fact, id, exp, inferType))
 129   {
 130     Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
 131                         << id << std::endl;
 132     Trace("sets-assertion") << "(assert (=> " << exp << " " << fact
 133                             << ")) ; by " << id << std::endl;
 134   }
 135 }
 136
 137 void InferenceManager::assertInference(Node fact,
 138                                        InferenceId id,
 139                                        std::vector<Node>& exp,
 140                                        int inferType)
 141 {
 142   Node exp_n = exp.empty() ? d_true
 143                            : (exp.size() == 1
 144                                   ? exp[0]
 145                                   : NodeManager::currentNM()->mkNode(AND, exp));
 146   assertInference(fact, id, exp_n, inferType);
 147 }
 148
 149 void InferenceManager::assertInference(std::vector<Node>& conc,
 150                                        InferenceId id,
 151                                        Node exp,
 152                                        int inferType)
 153 {
 154   if (!conc.empty())
 155   {
 156     Node fact = conc.size() == 1 ? conc[0]
 157                                  : NodeManager::currentNM()->mkNode(AND, conc);
 158     assertInference(fact, id, exp, inferType);
 159   }
 160 }
 161 void InferenceManager::assertInference(std::vector<Node>& conc,
 162                                        InferenceId id,
 163                                        std::vector<Node>& exp,
 164                                        int inferType)
 165 {
 166   Node exp_n = exp.empty() ? d_true
 167                            : (exp.size() == 1
 168                                   ? exp[0]
 169                                   : NodeManager::currentNM()->mkNode(AND, exp));
 170   assertInference(conc, id, exp_n, inferType);
 171 }
 172
 173 void InferenceManager::split(Node n, InferenceId id, int reqPol)
 174 {
 175   n = rewrite(n);
 176   Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
 177   // send the lemma
 178   lemma(lem, id);
 179   Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
 180   if (reqPol != 0)
 181   {
 182     Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
 183                         << std::endl;
 184     requirePhase(n, reqPol > 0);
 185   }
 186 }
 187
 188 }  // namespace sets
 189 }  // namespace theory
 190 }  // namespace cvc5