src/theory/theory_inference_manager.cpp

   1 /*********************                                                        */
   2 /*! \file theory_inference_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief An inference manager for Theory
  13  **/
  14
  15 #include "theory/theory_inference_manager.h"
  16
  17 #include "theory/theory.h"
  18 #include "theory/uf/equality_engine.h"
  19
  20 using namespace CVC4::kind;
  21
  22 namespace CVC4 {
  23 namespace theory {
  24
  25 TheoryInferenceManager::TheoryInferenceManager(Theory& t,
  26                                                TheoryState& state,
  27                                                ProofNodeManager* pnm)
  28     : d_theory(t),
  29       d_theoryState(state),
  30       d_out(t.getOutputChannel()),
  31       d_ee(nullptr),
  32       d_pnm(pnm),
  33       d_keep(t.getSatContext()),
  34       d_lemmasSent(t.getUserContext()),
  35       d_numCurrentLemmas(0),
  36       d_numCurrentFacts(0)
  37 {
  38 }
  39
  40 void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
  41 {
  42   d_ee = ee;
  43   // if proofs are enabled, also make a proof equality engine to wrap ee
  44   if (d_pnm != nullptr)
  45   {
  46     d_pfee.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
  47                                        d_theoryState.getUserContext(),
  48                                        *d_ee,
  49                                        d_pnm));
  50   }
  51 }
  52
  53 void TheoryInferenceManager::reset()
  54 {
  55   d_numCurrentLemmas = 0;
  56   d_numCurrentFacts = 0;
  57 }
  58
  59 void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
  60 {
  61   if (!d_theoryState.isInConflict())
  62   {
  63     TrustNode tconf = explainConflictEqConstantMerge(a, b);
  64     d_theoryState.notifyInConflict();
  65     d_out.trustedConflict(tconf);
  66   }
  67 }
  68
  69 void TheoryInferenceManager::conflict(TNode conf)
  70 {
  71   if (!d_theoryState.isInConflict())
  72   {
  73     d_theoryState.notifyInConflict();
  74     d_out.conflict(conf);
  75   }
  76 }
  77
  78 void TheoryInferenceManager::trustedConflict(TrustNode tconf)
  79 {
  80   if (!d_theoryState.isInConflict())
  81   {
  82     d_theoryState.notifyInConflict();
  83     d_out.trustedConflict(tconf);
  84   }
  85 }
  86
  87 bool TheoryInferenceManager::propagateLit(TNode lit)
  88 {
  89   // If already in conflict, no more propagation
  90   if (d_theoryState.isInConflict())
  91   {
  92     return false;
  93   }
  94   // Propagate out
  95   bool ok = d_out.propagate(lit);
  96   if (!ok)
  97   {
  98     d_theoryState.notifyInConflict();
  99   }
 100   return ok;
 101 }
 102
 103 TrustNode TheoryInferenceManager::explainLit(TNode lit)
 104 {
 105   if (d_pfee != nullptr)
 106   {
 107     return d_pfee->explain(lit);
 108   }
 109   if (d_ee != nullptr)
 110   {
 111     Node exp = d_ee->mkExplainLit(lit);
 112     return TrustNode::mkTrustPropExp(lit, exp, nullptr);
 113   }
 114   Unimplemented() << "Inference manager for " << d_theory.getId()
 115                   << " was asked to explain a propagation but doesn't have an "
 116                      "equality engine or implement the "
 117                      "TheoryInferenceManager::explainLit interface!";
 118 }
 119
 120 TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
 121                                                                  TNode b)
 122 {
 123   Node lit = a.eqNode(b);
 124   if (d_pfee != nullptr)
 125   {
 126     return d_pfee->explain(lit);
 127   }
 128   if (d_ee != nullptr)
 129   {
 130     Node conf = d_ee->mkExplainLit(lit);
 131     return TrustNode::mkTrustConflict(conf, nullptr);
 132   }
 133   Unimplemented() << "Inference manager for " << d_theory.getId()
 134                   << " mkTrustedConflictEqConstantMerge";
 135 }
 136
 137 bool TheoryInferenceManager::lemma(TNode lem, LemmaProperty p, bool doCache)
 138 {
 139   TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
 140   return trustedLemma(tlem, p, doCache);
 141 }
 142
 143 bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
 144                                           LemmaProperty p,
 145                                           bool doCache)
 146 {
 147   if (doCache)
 148   {
 149     if (!cacheLemma(tlem.getNode(), p))
 150     {
 151       return false;
 152     }
 153   }
 154   d_numCurrentLemmas++;
 155   d_out.trustedLemma(tlem, p);
 156   return true;
 157 }
 158
 159 bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
 160 {
 161   return d_lemmasSent.find(lem) != d_lemmasSent.end();
 162 }
 163
 164 uint32_t TheoryInferenceManager::numAddedLemmas() const
 165 {
 166   return d_numCurrentLemmas;
 167 }
 168
 169 bool TheoryInferenceManager::hasAddedLemma() const
 170 {
 171   return d_numCurrentLemmas != 0;
 172 }
 173
 174 void TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp)
 175 {
 176   processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr);
 177 }
 178
 179 void TheoryInferenceManager::assertInternalFact(TNode atom,
 180                                                 bool pol,
 181                                                 PfRule id,
 182                                                 const std::vector<Node>& exp,
 183                                                 const std::vector<Node>& args)
 184 {
 185   Assert(id != PfRule::UNKNOWN);
 186   processInternalFact(atom, pol, id, exp, args, nullptr);
 187 }
 188
 189 void TheoryInferenceManager::assertInternalFact(TNode atom,
 190                                                 bool pol,
 191                                                 const std::vector<Node>& exp,
 192                                                 ProofGenerator* pg)
 193 {
 194   Assert(pg != nullptr);
 195   processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg);
 196 }
 197
 198 void TheoryInferenceManager::processInternalFact(TNode atom,
 199                                                  bool pol,
 200                                                  PfRule id,
 201                                                  const std::vector<Node>& exp,
 202                                                  const std::vector<Node>& args,
 203                                                  ProofGenerator* pg)
 204 {
 205   // make the node corresponding to the explanation
 206   Node expn = NodeManager::currentNM()->mkAnd(exp);
 207   // call the pre-notify fact method with preReg = false, isInternal = true
 208   if (d_theory.preNotifyFact(atom, pol, expn, false, true))
 209   {
 210     // handled in a theory-specific way that doesn't require equality engine
 211     return;
 212   }
 213   Assert(d_ee != nullptr);
 214   Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
 215                          << expn << std::endl;
 216   d_numCurrentFacts++;
 217   // Now, assert the fact. How to do so depends on whether proofs are enabled.
 218   // If no proof production, or no proof rule was given
 219   if (d_pfee == nullptr || id == PfRule::UNKNOWN)
 220   {
 221     if (atom.getKind() == kind::EQUAL)
 222     {
 223       d_ee->assertEquality(atom, pol, expn);
 224     }
 225     else
 226     {
 227       d_ee->assertPredicate(atom, pol, expn);
 228     }
 229     // Must reference count the equality and its explanation, which is not done
 230     // by the equality engine. Notice that we do *not* need to do this for
 231     // external assertions, which enter as facts in theory check. This is also
 232     // not done if we are asserting to the proof equality engine, which does
 233     // this caching itself within ProofEqEngine::assertFact.
 234     d_keep.insert(atom);
 235     d_keep.insert(expn);
 236   }
 237   else
 238   {
 239     // Note that we reconstruct the original literal lit here, since both the
 240     // original literal is needed for bookkeeping proofs. It is possible to
 241     // optimize this so that a few less nodes are created, but at the cost
 242     // of a more verbose interface to proof equality engine.
 243     Node lit = pol ? Node(atom) : atom.notNode();
 244     if (pg != nullptr)
 245     {
 246       // use the proof generator interface
 247       d_pfee->assertFact(lit, expn, pg);
 248     }
 249     else
 250     {
 251       // use the explict proof step interface
 252       d_pfee->assertFact(lit, id, expn, args);
 253     }
 254   }
 255   // call the notify fact method with isInternal = true
 256   d_theory.notifyFact(atom, pol, expn, true);
 257   Trace("infer-manager")
 258       << "TheoryInferenceManager::finished assertInternalFact" << std::endl;
 259 }
 260
 261 void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions)
 262 {
 263   if (n.getKind() == kind::AND)
 264   {
 265     for (const Node& nc : n)
 266     {
 267       d_ee->explainLit(nc, assumptions);
 268     }
 269   }
 270   else
 271   {
 272     d_ee->explainLit(n, assumptions);
 273   }
 274 }
 275
 276 Node TheoryInferenceManager::mkExplain(TNode n)
 277 {
 278   std::vector<TNode> assumptions;
 279   explain(n, assumptions);
 280   return NodeManager::currentNM()->mkAnd(assumptions);
 281 }
 282
 283 uint32_t TheoryInferenceManager::numAddedFacts() const
 284 {
 285   return d_numCurrentFacts;
 286 }
 287
 288 bool TheoryInferenceManager::hasAddedFact() const
 289 {
 290   return d_numCurrentFacts != 0;
 291 }
 292
 293 bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 294 {
 295   if (d_lemmasSent.find(lem) != d_lemmasSent.end())
 296   {
 297     return false;
 298   }
 299   d_lemmasSent.insert(lem);
 300   return true;
 301 }
 302
 303 }  // namespace theory
 304 }  // namespace CVC4