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 {
  35 }
  36
  37 void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
  38 {
  39   d_ee = ee;
  40 }
  41
  42 void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
  43 {
  44   if (!d_theoryState.isInConflict())
  45   {
  46     TrustNode tconf = explainConflictEqConstantMerge(a, b);
  47     d_theoryState.notifyInConflict();
  48     d_out.trustedConflict(tconf);
  49   }
  50 }
  51
  52 void TheoryInferenceManager::conflict(TNode conf)
  53 {
  54   if (!d_theoryState.isInConflict())
  55   {
  56     d_theoryState.notifyInConflict();
  57     d_out.conflict(conf);
  58   }
  59 }
  60
  61 void TheoryInferenceManager::trustedConflict(TrustNode tconf)
  62 {
  63   if (!d_theoryState.isInConflict())
  64   {
  65     d_theoryState.notifyInConflict();
  66     d_out.trustedConflict(tconf);
  67   }
  68 }
  69
  70 bool TheoryInferenceManager::propagateLit(TNode lit)
  71 {
  72   // If already in conflict, no more propagation
  73   if (d_theoryState.isInConflict())
  74   {
  75     return false;
  76   }
  77   // Propagate out
  78   bool ok = d_out.propagate(lit);
  79   if (!ok)
  80   {
  81     d_theoryState.notifyInConflict();
  82   }
  83   return ok;
  84 }
  85
  86 TrustNode TheoryInferenceManager::explainLit(TNode lit)
  87 {
  88   // TODO (project #37): use proof equality engine if it exists
  89   if (d_ee != nullptr)
  90   {
  91     Node exp = d_ee->mkExplainLit(lit);
  92     return TrustNode::mkTrustPropExp(lit, exp, nullptr);
  93   }
  94   Unimplemented() << "Inference manager for " << d_theory.getId()
  95                   << " was asked to explain a propagation but doesn't have an "
  96                      "equality engine or implement the "
  97                      "TheoryInferenceManager::explainLit interface!";
  98 }
  99
 100 TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
 101                                                                  TNode b)
 102 {
 103   // TODO (project #37): use proof equality engine if it exists
 104   if (d_ee != nullptr)
 105   {
 106     Node lit = a.eqNode(b);
 107     Node conf = d_ee->mkExplainLit(lit);
 108     return TrustNode::mkTrustConflict(conf, nullptr);
 109   }
 110   Unimplemented() << "Inference manager for " << d_theory.getId()
 111                   << " mkTrustedConflictEqConstantMerge";
 112 }
 113
 114 LemmaStatus TheoryInferenceManager::lemma(TNode lem, LemmaProperty p)
 115 {
 116   return d_out.lemma(lem, p);
 117 }
 118
 119 LemmaStatus TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
 120                                                  LemmaProperty p)
 121 {
 122   return d_out.trustedLemma(tlem, p);
 123 }
 124
 125 void TheoryInferenceManager::assertInternalFact(TNode atom,
 126                                                 bool pol,
 127                                                 TNode fact)
 128 {
 129   // call the pre-notify fact method with preReg = false, isInternal = true
 130   if (d_theory.preNotifyFact(atom, pol, fact, false, true))
 131   {
 132     // handled in a theory-specific way that doesn't require equality engine
 133     return;
 134   }
 135   Assert(d_ee != nullptr);
 136   Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
 137                          << fact << std::endl;
 138   if (atom.getKind() == kind::EQUAL)
 139   {
 140     d_ee->assertEquality(atom, pol, fact);
 141   }
 142   else
 143   {
 144     d_ee->assertPredicate(atom, pol, fact);
 145   }
 146   // call the notify fact method with isInternal = true
 147   d_theory.notifyFact(atom, pol, fact, true);
 148   Trace("infer-manager")
 149       << "TheoryInferenceManager::finished assertInternalFact" << std::endl;
 150   // Must reference count the equality and its explanation, which is not done
 151   // by the equality engine. Notice that we do *not* need to do this for
 152   // external assertions, which enter as facts in theory check.
 153   d_keep.insert(atom);
 154   d_keep.insert(fact);
 155 }
 156
 157 }  // namespace theory
 158 }  // namespace CVC4