src/theory/subs_minimize.h

   1 /*********************                                                        */
   2 /*! \file subs_minimize.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner
   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 Substitution minimization.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__SUBS_MINIMIZE_H
  18 #define CVC4__THEORY__SUBS_MINIMIZE_H
  19
  20 #include <vector>
  21
  22 #include "expr/node.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 /** SubstitutionMinimize
  28  *
  29  * This class is used for finding a minimal substitution under which an
  30  * evaluation holds.
  31  */
  32 class SubstitutionMinimize
  33 {
  34  public:
  35   SubstitutionMinimize();
  36   ~SubstitutionMinimize() {}
  37   /** find
  38    *
  39    * If t { vars -> subs } rewrites to target, this method returns true, and
  40    * vars[i_1], ..., vars[i_n] are added to reqVars, such that i_1, ..., i_n are
  41    * distinct, and t { vars[i_1] -> subs[i_1], ..., vars[i_n] -> subs[i_n] }
  42    * rewrites to target.
  43    *
  44    * If t { vars -> subs } does not rewrite to target, this method returns
  45    * false.
  46    */
  47   static bool find(Node t,
  48                    Node target,
  49                    const std::vector<Node>& vars,
  50                    const std::vector<Node>& subs,
  51                    std::vector<Node>& reqVars);
  52   /** find with implied
  53    *
  54    * This method should be called on a formula t.
  55    *
  56    * If t { vars -> subs } rewrites to true, this method returns true,
  57    * vars[i_1], ..., vars[i_n] are added to reqVars, and
  58    * vars[i_{n+1}], ..., vars[i_{n+m}] are added to impliedVars such that
  59    * i_1...i_{n+m} are distinct, i_{n+1} < ... < i_{n+m}, and:
  60    *
  61    * (1) t { vars[i_1]->subs[i_1], ..., vars[i_{n+k}]->subs[i_{n+k}] } implies
  62    * vars[i_{n+k+1}] = subs[i_{n+k+1}] for k = 0, ..., m-1.
  63    *
  64    * (2) t { vars[i_1] -> subs[i_1], ..., vars[i_{n+m}] -> subs[i_{n+m}] }
  65    * rewrites to true.
  66    *
  67    * For example, given (x>0 ^ x = y ^ y = z){ x -> 1, y -> 1, z -> 1, w -> 0 },
  68    * this method may add { x } to reqVars, and { y, z } to impliedVars.
  69    *
  70    * Notice that the order of variables in vars matters. By the semantics above,
  71    * variables that appear earlier in the variable list vars are more likely
  72    * to appear in reqVars, whereas those later in the vars are more likely to
  73    * appear in impliedVars.
  74    */
  75   static bool findWithImplied(Node t,
  76                               const std::vector<Node>& vars,
  77                               const std::vector<Node>& subs,
  78                               std::vector<Node>& reqVars,
  79                               std::vector<Node>& impliedVars);
  80
  81  private:
  82   /** Common helper function for the above functions. */
  83   static bool findInternal(Node t,
  84                            Node target,
  85                            const std::vector<Node>& vars,
  86                            const std::vector<Node>& subs,
  87                            std::vector<Node>& reqVars);
  88   /** is singular arg
  89    *
  90    * Returns true if
  91    *   <k>( ... t_{arg-1}, n, t_{arg+1}...) = c
  92    * always holds for some constant c.
  93    */
  94   static bool isSingularArg(Node n, Kind k, unsigned arg);
  95 };
  96
  97 }  // namespace theory
  98 }  // namespace CVC4
  99
 100 #endif /* CVC4__THEORY__SUBS_MINIMIZE_H */