src/theory/arith/arith_preprocess.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, 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  * Arithmetic preprocess.
  14  */
  15
  16 #include "theory/arith/arith_preprocess.h"
  17
  18 #include "theory/arith/arith_state.h"
  19 #include "theory/arith/inference_manager.h"
  20 #include "theory/skolem_lemma.h"
  21
  22 namespace cvc5 {
  23 namespace theory {
  24 namespace arith {
  25
  26 ArithPreprocess::ArithPreprocess(Env& env,
  27                                  ArithState& state,
  28                                  InferenceManager& im,
  29                                  ProofNodeManager* pnm,
  30                                  OperatorElim& oe)
  31     : EnvObj(env), d_im(im), d_opElim(oe), d_reduced(userContext())
  32 {
  33 }
  34 TrustNode ArithPreprocess::eliminate(TNode n,
  35                                      std::vector<SkolemLemma>& lems,
  36                                      bool partialOnly)
  37 {
  38   return d_opElim.eliminate(n, lems, partialOnly);
  39 }
  40
  41 bool ArithPreprocess::reduceAssertion(TNode atom)
  42 {
  43   context::CDHashMap<Node, bool>::const_iterator it = d_reduced.find(atom);
  44   if (it != d_reduced.end())
  45   {
  46     // already computed
  47     return (*it).second;
  48   }
  49   std::vector<SkolemLemma> lems;
  50   TrustNode tn = eliminate(atom, lems);
  51   for (const SkolemLemma& lem : lems)
  52   {
  53     d_im.trustedLemma(lem.d_lemma, InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA);
  54   }
  55   if (tn.isNull())
  56   {
  57     // did not reduce
  58     d_reduced[atom] = false;
  59     return false;
  60   }
  61   Assert(tn.getKind() == TrustNodeKind::REWRITE);
  62   // tn is of kind REWRITE, turn this into a LEMMA here
  63   TrustNode tlem = TrustNode::mkTrustLemma(tn.getProven(), tn.getGenerator());
  64   // send the trusted lemma
  65   d_im.trustedLemma(tlem, InferenceId::ARITH_PP_ELIM_OPERATORS);
  66   // mark the atom as reduced
  67   d_reduced[atom] = true;
  68   return true;
  69 }
  70
  71 bool ArithPreprocess::isReduced(TNode atom) const
  72 {
  73   context::CDHashMap<Node, bool>::const_iterator it = d_reduced.find(atom);
  74   if (it == d_reduced.end())
  75   {
  76     return false;
  77   }
  78   return (*it).second;
  79 }
  80
  81 }  // namespace arith
  82 }  // namespace theory
  83 }  // namespace cvc5