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::unique_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     d_pendingLem.emplace_back(std::move(lemma));
  59   }
  60 }
  61 void InferenceManager::addPendingArithLemma(const ArithLemma& lemma,
  62                                             bool isWaiting)
  63 {
  64   addPendingArithLemma(std::unique_ptr<ArithLemma>(new ArithLemma(lemma)),
  65                        isWaiting);
  66 }
  67 void InferenceManager::addPendingArithLemma(const Node& lemma,
  68                                             nl::Inference inftype,
  69                                             bool isWaiting)
  70 {
  71   addPendingArithLemma(std::unique_ptr<ArithLemma>(new ArithLemma(
  72                            lemma, LemmaProperty::NONE, nullptr, inftype)),
  73                        isWaiting);
  74 }
  75
  76 void InferenceManager::flushWaitingLemmas()
  77 {
  78   for (auto& lem : d_waitingLem)
  79   {
  80     d_pendingLem.emplace_back(std::move(lem));
  81   }
  82   d_waitingLem.clear();
  83 }
  84
  85 void InferenceManager::addConflict(const Node& conf, nl::Inference inftype)
  86 {
  87   conflict(Rewriter::rewrite(conf));
  88 }
  89
  90 std::size_t InferenceManager::numWaitingLemmas() const
  91 {
  92   return d_waitingLem.size();
  93 }
  94
  95 bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
  96 {
  97   if (isLemmaPropertyPreprocess(p))
  98   {
  99     return d_lemmasPp.find(lem) != d_lemmasPp.end();
 100   }
 101   return TheoryInferenceManager::hasCachedLemma(lem, p);
 102 }
 103
 104 bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 105 {
 106   if (isLemmaPropertyPreprocess(p))
 107   {
 108     if (d_lemmasPp.find(lem) != d_lemmasPp.end())
 109     {
 110       return false;
 111     }
 112     d_lemmasPp.insert(lem);
 113     return true;
 114   }
 115   return TheoryInferenceManager::cacheLemma(lem, p);
 116 }
 117
 118 bool InferenceManager::isEntailedFalse(const ArithLemma& lem)
 119 {
 120   if (options::nlExtEntailConflicts())
 121   {
 122     Node ch_lemma = lem.d_node.negate();
 123     ch_lemma = Rewriter::rewrite(ch_lemma);
 124     Trace("arith-inf-manager") << "InferenceManager::Check entailment of "
 125                                << ch_lemma << "..." << std::endl;
 126
 127     std::pair<bool, Node> et = d_theory.getValuation().entailmentCheck(
 128         options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma);
 129     Trace("arith-inf-manager") << "entailment test result : " << et.first << " "
 130                                << et.second << std::endl;
 131     if (et.first)
 132     {
 133       Trace("arith-inf-manager")
 134           << "*** Lemma entailed to be in conflict : " << lem.d_node
 135           << std::endl;
 136       return true;
 137     }
 138   }
 139   return false;
 140 }
 141
 142 }  // namespace arith
 143 }  // namespace theory
 144 }  // namespace CVC4