src/theory/arith/pp_rewrite_eq.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   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  * Preprocess equality rewriter for arithmetic
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__ARITH__PP_REWRITE_EQ__H
  19 #define CVC5__THEORY__ARITH__PP_REWRITE_EQ__H
  20
  21 #include "context/context.h"
  22 #include "expr/node.h"
  23 #include "proof/eager_proof_generator.h"
  24 #include "proof/proof_node_manager.h"
  25 #include "smt/env_obj.h"
  26
  27 namespace cvc5 {
  28 namespace theory {
  29 namespace arith {
  30
  31 /**
  32  * This class is responsible for rewriting arithmetic equalities based on the
  33  * current options.
  34  *
  35  * In particular, we may rewrite (= x y) to (and (>= x y) (<= x y)).
  36  */
  37 class PreprocessRewriteEq : protected EnvObj
  38 {
  39  public:
  40   PreprocessRewriteEq(Env& env);
  41   ~PreprocessRewriteEq() {}
  42   /**
  43    * Preprocess equality, applies ppRewrite for equalities. This method is
  44    * distinct from ppRewrite since it is not allowed to construct lemmas.
  45    */
  46   TrustNode ppRewriteEq(TNode eq);
  47
  48  private:
  49   /** Used to prove pp-rewrites */
  50   EagerProofGenerator d_ppPfGen;
  51 };
  52
  53 }  // namespace arith
  54 }  // namespace theory
  55 }  // namespace cvc5
  56
  57 #endif