src/theory/theory_inference.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Gereon Kremer, Aina Niemetz
   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  * The theory inference utility.
  14  */
  15
  16 #include "theory/theory_inference.h"
  17
  18 #include "theory/theory_inference_manager.h"
  19
  20 using namespace cvc5::kind;
  21
  22 namespace cvc5 {
  23 namespace theory {
  24
  25 SimpleTheoryLemma::SimpleTheoryLemma(InferenceId id,
  26                                      Node n,
  27                                      LemmaProperty p,
  28                                      ProofGenerator* pg)
  29     : TheoryInference(id), d_node(n), d_property(p), d_pg(pg)
  30 {
  31 }
  32
  33 TrustNode SimpleTheoryLemma::processLemma(LemmaProperty& p)
  34 {
  35   Assert(!d_node.isNull());
  36   p = d_property;
  37   return TrustNode::mkTrustLemma(d_node, d_pg);
  38 }
  39
  40 SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id,
  41                                                    Node conc,
  42                                                    Node exp,
  43                                                    ProofGenerator* pg)
  44     : TheoryInference(id), d_conc(conc), d_exp(exp), d_pg(pg)
  45 {
  46 }
  47
  48 Node SimpleTheoryInternalFact::processFact(std::vector<Node>& exp,
  49                                            ProofGenerator*& pg)
  50 {
  51   exp.push_back(d_exp);
  52   pg = d_pg;
  53   return d_conc;
  54 }
  55
  56 }  // namespace theory
  57 }  // namespace cvc5