src/theory/strings/infer_info.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Mudathir Mohamed, Gereon Kremer
   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 inference information utility.
  14  */
  15
  16 #include "theory/strings/infer_info.h"
  17
  18 #include "theory/strings/inference_manager.h"
  19 #include "theory/strings/theory_strings_utils.h"
  20 #include "theory/theory.h"
  21
  22 namespace cvc5 {
  23 namespace theory {
  24 namespace strings {
  25
  26 InferInfo::InferInfo(InferenceId id): TheoryInference(id), d_sim(nullptr), d_idRev(false)
  27 {
  28 }
  29
  30 TrustNode InferInfo::processLemma(LemmaProperty& p)
  31 {
  32   return d_sim->processLemma(*this, p);
  33 }
  34
  35 Node InferInfo::processFact(std::vector<Node>& exp, ProofGenerator*& pg)
  36 {
  37   for (const Node& ec : d_premises)
  38   {
  39     utils::flattenOp(kind::AND, ec, exp);
  40   }
  41   d_sim->processFact(*this, pg);
  42   return d_conc;
  43 }
  44
  45 bool InferInfo::isTrivial() const
  46 {
  47   Assert(!d_conc.isNull());
  48   return d_conc.isConst() && d_conc.getConst<bool>();
  49 }
  50
  51 bool InferInfo::isConflict() const
  52 {
  53   Assert(!d_conc.isNull());
  54   return d_conc.isConst() && !d_conc.getConst<bool>() && d_noExplain.empty();
  55 }
  56
  57 bool InferInfo::isFact() const
  58 {
  59   Assert(!d_conc.isNull());
  60   TNode atom = d_conc.getKind() == kind::NOT ? d_conc[0] : d_conc;
  61   // we could process inferences with conjunctive conclusions as facts, where
  62   // the explanation is copied. However, for simplicity, we always send these
  63   // as lemmas. This case happens very infrequently.
  64   return !atom.isConst() && Theory::theoryOf(atom) == THEORY_STRINGS
  65          && d_noExplain.empty();
  66 }
  67
  68 Node InferInfo::getPremises() const
  69 {
  70   // d_noExplain is a subset of d_ant
  71   return utils::mkAnd(d_premises);
  72 }
  73
  74 std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
  75 {
  76   out << "(infer " << ii.getId() << " " << ii.d_conc;
  77   if (ii.d_idRev)
  78   {
  79     out << " :rev";
  80   }
  81   if (!ii.d_premises.empty())
  82   {
  83     out << " :ant (" << ii.d_premises << ")";
  84   }
  85   if (!ii.d_noExplain.empty())
  86   {
  87     out << " :no-explain (" << ii.d_noExplain << ")";
  88   }
  89   out << ")";
  90   return out;
  91 }
  92
  93 }  // namespace strings
  94 }  // namespace theory
  95 }  // namespace cvc5