src/preprocessing/passes/foreign_theory_rewrite.h

   1 /*********************                                                        */
   2 /*! \file foreign_theory_rewrite.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Yoni Zohar
   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 The foreign_theory_rewrite preprocessing pass
  13  **
  14  ** Simplifies nodes of one theory using rewrites from another.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H
  20 #define CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H
  21
  22 #include "context/cdhashmap.h"
  23 #include "context/cdo.h"
  24 #include "context/context.h"
  25 #include "preprocessing/preprocessing_pass.h"
  26 #include "preprocessing/preprocessing_pass_context.h"
  27
  28 namespace CVC4 {
  29 namespace preprocessing {
  30 namespace passes {
  31
  32 using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
  33
  34 class ForeignTheoryRewrite : public PreprocessingPass
  35 {
  36  public:
  37   ForeignTheoryRewrite(PreprocessingPassContext* preprocContext);
  38
  39  protected:
  40   PreprocessingPassResult applyInternal(
  41       AssertionPipeline* assertionsToPreprocess) override;
  42   /** the main function that simplifies n.
  43    * does a traversal on n and call rewriting fucntions.
  44    */
  45   Node simplify(Node n);
  46   /** A specific simplification function specific for GEQ
  47    * constraints in strings.
  48    */
  49   static Node rewriteStringsGeq(Node n);
  50   /** invoke rewrite functions for n.
  51    * based on the structure of n (typically its kind)
  52    * we invoke rewrites from other theories.
  53    * For example: when encountering a `>=` node,
  54    * we invoke rewrites from the theory of strings.
  55    */
  56   static Node foreignRewrite(Node n);
  57   /** construct a node with the same operator as originalNode whose children are
  58    * processedChildren
  59    */
  60   static Node reconstructNode(Node originalNode, vector<Node> newChildren);
  61   /** A cache to store the simplified nodes */
  62   CDNodeMap d_cache;
  63 };
  64
  65 }  // namespace passes
  66 }  // namespace preprocessing
  67 }  // namespace CVC4
  68
  69 #endif /* CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H */