src/theory/quantifiers/single_inv_partition.h

   1 /*********************                                                        */
   2 /*! \file single_inv_partition.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-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.\endverbatim
  11  **
  12  ** \brief utility for single invocation partitioning
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
  18 #define CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
  19
  20 #include <map>
  21 #include <vector>
  22
  23 #include "expr/node.h"
  24 #include "expr/type_node.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace quantifiers {
  29
  30 /** single invocation partition
  31  *
  32  * This is a utility to group formulas into single invocation/non-single
  33  * invocation parts, relative to a set of "input functions".
  34  * It can be used when either the set of input functions is fixed,
  35  * or is unknown.
  36  *
  37  * (EX1) For example, if input functions are { f },
  38  * then the formula is ( f( x, y ) = g( y ) V f( x, y ) = b )
  39  * is single invocation since there is only one
  40  * unique application of f, that is, f( x, y ).
  41  * Notice that
  42  *   exists f. forall xy. f( x, y ) = g( y ) V f( x, y ) = b
  43  * is equivalent to:
  44  *   forall xy. exists z. z = g( y ) V z = b
  45  *
  46  * When handling multiple input functions, we only infer a formula
  47  * is single invocation if all (relevant) input functions have the
  48  * same argument types. An input function is relevant if it is
  49  * specified by the input in a call to init() or occurs in the
  50  * formula we are processing.
  51  *
  52  * Notice that this class may introduce auxiliary variables to
  53  * coerce a formula into being single invocation. For example,
  54  * see Example 5 of Reynolds et al. SYNT 2017.
  55  *
  56  */
  57 class SingleInvocationPartition
  58 {
  59  public:
  60   SingleInvocationPartition() : d_has_input_funcs(false) {}
  61   ~SingleInvocationPartition() {}
  62   /** initialize this partition for formula n, with input functions funcs
  63    *
  64    * This initializes this class to check whether formula n is single
  65    * invocation with respect to the input functions in funcs only.
  66    * Below, the "processed formula" is a formula generated by this
  67    * call that is equivalent to n (if this call is successful).
  68    *
  69    * This method returns true if all input functions have identical
  70    * argument types, and false otherwise. Notice that all
  71    * access functions below are only valid if this class is
  72    * successfully initialized.
  73    */
  74   bool init(std::vector<Node>& funcs, Node n);
  75
  76   /** initialize this partition for formula n
  77    *
  78    * In contrast to the above method, this version assumes that
  79    * all uninterpreted functions are input functions. That is, this
  80    * method is equivalent to the above function with funcs containing
  81    * all uninterpreted functions occurring in n.
  82    */
  83   bool init(Node n);
  84
  85   /** is the processed formula purely single invocation?
  86    *
  87    * A formula is purely single invocation if it is equivalent to:
  88    *   t[ f1( x ), ..., fn( x ), x ],
  89    * for some F, where f1...fn are the input functions.
  90    * Notice that the free variables of t are exactly x.
  91    */
  92   bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); }
  93   /** is the processed formula non-ground single invocation?
  94    *
  95    * A formula is non-ground single invocation if it is equivalent to:
  96    *   F[ f1( x ), ..., fn( x ), x, y ],
  97    * for some F, where f1...fn are the input functions.
  98    */
  99   bool isNonGroundSingleInvocation()
 100   {
 101     return d_conjuncts[3].size() == d_conjuncts[1].size();
 102   }
 103
 104   /** Get the (portion of) the processed formula that is single invocation
 105    *
 106    * Notice this method returns the anti-skolemized version of the input
 107    * formula. In (EX1), this method returns:
 108    *   z = g( y ) V z = b
 109    * where z is the first-order variable for f (see
 110    * getFirstOrderVariableForFunction).
 111    */
 112   Node getSingleInvocation() { return getConjunct(0); }
 113   /** Get the (portion of) the processed formula that is not single invocation
 114    *
 115    * This formula and the above form a partition of the conjuncts of the
 116    * processed formula, that is:
 117    *   getSingleInvocation() * sigma ^ getNonSingleInvocation()
 118    * is equivalent to the processed formula, where sigma is a substitution of
 119    * the form:
 120    *   z_1 -> f_1( x ) .... z_n -> f_n( x )
 121    * where z_i are the first-order variables for input functions f_i
 122    * for all i=1,...,n, and x are the single invocation arguments of the input
 123    * formulas (see d_si_vars).
 124    */
 125   Node getNonSingleInvocation() { return getConjunct(1); }
 126   /** get full specification
 127    *
 128    * This returns getSingleInvocation() * sigma ^ getNonSingleInvocation(),
 129    * which is equivalent to the processed formula, where sigma is the
 130    * substitution described above.
 131    */
 132   Node getFullSpecification() { return getConjunct(2); }
 133   /** get first order variable for input function f
 134    *
 135    * This corresponds to the variable that we used when anti-skolemizing
 136    * function f. For example, in (EX1), if getSingleInvocation() returns:
 137    *   z = g( y ) V z = b
 138    * Then, getFirstOrderVariableForFunction(f) = z.
 139    */
 140   Node getFirstOrderVariableForFunction(Node f) const;
 141
 142   /** get function for first order variable
 143    *
 144    * Opposite direction of above, where:
 145    *   getFunctionForFirstOrderVariable(z) = f.
 146    */
 147   Node getFunctionForFirstOrderVariable(Node v) const;
 148
 149   /** get function invocation for
 150    *
 151    * Returns f( x ) where x are the single invocation arguments of the input
 152    * formulas (see d_si_vars). If f is not an input function, it returns null.
 153    */
 154   Node getFunctionInvocationFor(Node f) const;
 155
 156   /** get single invocation variables, appends them to sivars */
 157   void getSingleInvocationVariables(std::vector<Node>& sivars) const;
 158
 159   /** get all variables
 160    *
 161    * Appends all free variables of the processed formula to vars.
 162    */
 163   void getAllVariables(std::vector<Node>& vars) const;
 164
 165   /** get function variables
 166    *
 167    * Appends all first-order variables corresponding to input functions to
 168    * fvars.
 169    */
 170   void getFunctionVariables(std::vector<Node>& fvars) const;
 171
 172   /** get functions
 173    *
 174    * Gets all input functions. This has the same order as the list of
 175    * function variables above.
 176    */
 177   void getFunctions(std::vector<Node>& fs) const;
 178
 179   /** print debugging information on Trace c */
 180   void debugPrint(const char* c);
 181
 182  private:
 183   /** map from input functions to whether they have an anti-skolemizable type
 184    * An anti-skolemizable type is one of the form:
 185    *   ( T1, ..., Tn ) -> T
 186    * where Ti = d_arg_types[i] for i = 1,...,n.
 187    */
 188   std::map<Node, bool> d_funcs;
 189
 190   /** map from functions to the invocation we inferred for them */
 191   std::map<Node, Node> d_func_inv;
 192
 193   /** the list of first-order variables for functions
 194    * In (EX1), this is the list { z }.
 195    */
 196   std::vector<Node> d_func_vars;
 197
 198   /** the arguments that we based the anti-skolemization on.
 199    * In (EX1), this is the list { x, y }.
 200    */
 201   std::vector<Node> d_si_vars;
 202
 203   /** every free variable of conjuncts[2] */
 204   std::unordered_set<Node, NodeHashFunction> d_all_vars;
 205   /** map from functions to first-order variables that anti-skolemized them */
 206   std::map<Node, Node> d_func_fo_var;
 207   /** map from first-order variables to the function it anti-skolemized */
 208   std::map<Node, Node> d_fo_var_to_func;
 209
 210   /** The argument types for this single invocation partition.
 211    * These are the argument types of the input functions we are
 212    * processing, where notice that:
 213    *   d_si_vars[i].getType()==d_arg_types[i]
 214    */
 215   std::vector<TypeNode> d_arg_types;
 216
 217   /** the list of conjuncts with various properties :
 218    * 0 : the single invocation conjuncts (stored in anti-skolemized form),
 219    * 1 : the non-single invocation conjuncts,
 220    * 2 : all conjuncts,
 221    * 3 : non-ground single invocation conjuncts.
 222    */
 223   std::vector<Node> d_conjuncts[4];
 224
 225   /** did we initialize this class with input functions? */
 226   bool d_has_input_funcs;
 227   /** the input functions we initialized this class with */
 228   std::vector<Node> d_input_funcs;
 229   /** all input functions */
 230   std::vector<Node> d_all_funcs;
 231   /** skolem of the same type as input functions */
 232   std::vector<Node> d_input_func_sks;
 233
 234   /** infer the argument types of uninterpreted function applications
 235    *
 236    * If this method returns true, then typs contains the list of types of
 237    * the arguments (in order) of all uninterpreted functions in n.
 238    * If this method returns false, then there exists (at least) two
 239    * uninterpreted functions in n whose argument types are not identical.
 240    */
 241   bool inferArgTypes(Node n,
 242                      std::vector<TypeNode>& typs,
 243                      std::map<Node, bool>& visited);
 244
 245   /** is anti-skolemizable type
 246    *
 247    * This method returns true if f's argument types are equal to the
 248    * argument types we have fixed in this class (see d_arg_types).
 249    */
 250   bool isAntiSkolemizableType(Node f);
 251
 252   /**
 253    * This is the entry point for initializing this class,
 254    * which is called by the public init(...) methods.
 255    *   funcs are the input functions (if any were explicitly provide),
 256    *   typs is the types of the arguments of funcs,
 257    *   n is the formula to process,
 258    *   has_funcs is whether input functions were explicitly provided.
 259    */
 260   bool init(std::vector<Node>& funcs,
 261             std::vector<TypeNode>& typs,
 262             Node n,
 263             bool has_funcs);
 264
 265   /**
 266    * Collect the top-level conjuncts of the formula (equivalent to)
 267    * n or the negation of n if pol=false, and store them in conj.
 268    */
 269   bool collectConjuncts(Node n, bool pol, std::vector<Node>& conj);
 270
 271   /** process conjunct n
 272    *
 273    * This function is called when n is a top-level conjunction in a
 274    * formula that is equivalent to the input formula given to this
 275    * class via init.
 276    *
 277    * args : stores the arguments (if any) that we have seen in an application
 278    *   of an application of an input function in this conjunct.
 279    * terms/subs : this stores a term substitution with entries of the form:
 280    *     f(args) -> z
 281    *   where z is the first-order variable for input function f.
 282    */
 283   bool processConjunct(Node n,
 284                        std::map<Node, bool>& visited,
 285                        std::vector<Node>& args,
 286                        std::vector<Node>& terms,
 287                        std::vector<Node>& subs);
 288
 289   /** get the and node corresponding to d_conjuncts[index] */
 290   Node getConjunct(int index);
 291 };
 292
 293 } /* namespace CVC4::theory::quantifiers */
 294 } /* namespace CVC4::theory */
 295 } /* namespace CVC4 */
 296
 297 #endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */