src/theory/arith/inference_manager.cpp

   1 /*********************                                                        */
   2 /*! \file inference_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Gereon Kremer
   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 Implementation of the inference manager for the theory of strings.
  13  **/
  14
  15 #include "theory/arith/inference_manager.h"
  16
  17 #include "options/arith_options.h"
  18 #include "theory/arith/theory_arith.h"
  19 #include "theory/rewriter.h"
  20
  21 namespace CVC4 {
  22 namespace theory {
  23 namespace arith {
  24
  25 InferenceManager::InferenceManager(TheoryArith& ta,
  26                                    ArithState& astate,
  27                                    ProofNodeManager* pnm)
  28     : InferenceManagerBuffered(ta, astate, pnm), d_lemmasPp(ta.getUserContext())
  29 {
  30 }
  31
  32 void InferenceManager::addPendingArithLemma(std::shared_ptr<ArithLemma> lemma,
  33                                             bool isWaiting)
  34 {
  35   lemma->d_node = Rewriter::rewrite(lemma->d_node);
  36   if (hasCachedLemma(lemma->d_node, lemma->d_property))
  37   {
  38     return;
  39   }
  40   if (isEntailedFalse(*lemma))
  41   {
  42     if (isWaiting)
  43     {
  44       d_waitingLem.clear();
  45     }
  46     else
  47     {
  48       d_pendingLem.clear();
  49       d_theoryState.notifyInConflict();
  50     }
  51   }
  52   if (isWaiting)
  53   {
  54     d_waitingLem.emplace_back(std::move(lemma));
  55   }
  56   else
  57   {
  58     addPendingLemma(std::move(lemma));
  59   }
  60 }
  61 void InferenceManager::addPendingArithLemma(const ArithLemma& lemma,
  62                                             bool isWaiting)
  63 {
  64   addPendingArithLemma(std::make_shared<ArithLemma>(lemma), isWaiting);
  65 }
  66 void InferenceManager::addPendingArithLemma(const Node& lemma,
  67                                             nl::Inference inftype,
  68                                             bool isWaiting)
  69 {
  70   addPendingArithLemma(std::make_shared<ArithLemma>(
  71                            lemma, LemmaProperty::NONE, nullptr, inftype),
  72                        isWaiting);
  73 }
  74
  75 void InferenceManager::flushWaitingLemmas()
  76 {
  77   for (auto& lem : d_waitingLem)
  78   {
  79     addPendingLemma(std::move(lem));
  80   }
  81   d_waitingLem.clear();
  82 }
  83
  84 void InferenceManager::addConflict(const Node& conf, nl::Inference inftype)
  85 {
  86   conflict(Rewriter::rewrite(conf));
  87 }
  88
  89 std::size_t InferenceManager::numWaitingLemmas() const
  90 {
  91   return d_waitingLem.size();
  92 }
  93
  94 bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
  95 {
  96   if (isLemmaPropertyPreprocess(p))
  97   {
  98     return d_lemmasPp.find(lem) != d_lemmasPp.end();
  99   }
 100   return TheoryInferenceManager::hasCachedLemma(lem, p);
 101 }
 102
 103 bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 104 {
 105   if (isLemmaPropertyPreprocess(p))
 106   {
 107     if (d_lemmasPp.find(lem) != d_lemmasPp.end())
 108     {
 109       return false;
 110     }
 111     d_lemmasPp.insert(lem);
 112     return true;
 113   }
 114   return TheoryInferenceManager::cacheLemma(lem, p);
 115 }
 116
 117 bool InferenceManager::isEntailedFalse(const ArithLemma& lem)
 118 {
 119   if (options::nlExtEntailConflicts())
 120   {
 121     Node ch_lemma = lem.d_node.negate();
 122     ch_lemma = Rewriter::rewrite(ch_lemma);
 123     Trace("arith-inf-manager") << "InferenceManager::Check entailment of "
 124                                << ch_lemma << "..." << std::endl;
 125
 126     std::pair<bool, Node> et = d_theory.getValuation().entailmentCheck(
 127         options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma);
 128     Trace("arith-inf-manager") << "entailment test result : " << et.first << " "
 129                                << et.second << std::endl;
 130     if (et.first)
 131     {
 132       Trace("arith-inf-manager")
 133           << "*** Lemma entailed to be in conflict : " << lem.d_node
 134           << std::endl;
 135       return true;
 136     }
 137   }
 138   return false;
 139 }
 140
 141 }  // namespace arith
 142 }  // namespace theory
 143 }  // namespace CVC4