src/theory/datatypes/theory_datatypes_utils.h

   1 /*********************                                                        */
   2 /*! \file theory_datatypes_utils.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 Util functions for theory datatypes.
  13  **
  14  ** Util functions for theory datatypes.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H
  20 #define CVC4__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H
  21
  22 #include <vector>
  23
  24 #include "expr/dtype.h"
  25 #include "expr/node.h"
  26 #include "expr/node_manager_attributes.h"
  27
  28 namespace CVC4 {
  29 namespace theory {
  30
  31 // ----------------------- sygus datatype attributes
  32 /** sygus var num */
  33 struct SygusVarNumAttributeId
  34 {
  35 };
  36 typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
  37
  38 /**
  39  * Attribute true for enumerators whose current model values were registered by
  40  * the datatypes sygus solver, and were not excluded by sygus symmetry breaking.
  41  * This is set by the datatypes sygus solver during LAST_CALL effort checks for
  42  * each active sygus enumerator.
  43  */
  44 struct SygusSymBreakOkAttributeId
  45 {
  46 };
  47 typedef expr::Attribute<SygusSymBreakOkAttributeId, bool>
  48     SygusSymBreakOkAttribute;
  49
  50 /** sygus var free
  51  *
  52  * This attribute is used to mark whether sygus operators have free occurrences
  53  * of variables from the formal argument list of the function-to-synthesize.
  54  *
  55  * We store three possible cases for sygus operators op:
  56  * (1) op.getAttribute(SygusVarFreeAttribute())==Node::null()
  57  * In this case, op has no free variables from the formal argument list of the
  58  * function-to-synthesize.
  59  * (2) op.getAttribute(SygusVarFreeAttribute())==v, where v is a bound variable.
  60  * In this case, op has exactly one free variable, v.
  61  * (3) op.getAttribute(SygusVarFreeAttribute())==op
  62  * In this case, op has an arbitrary set (cardinality >1) of free variables from
  63  * the formal argument list of the function to synthesize.
  64  *
  65  * This attribute is used to compute applySygusArgs below.
  66  */
  67 struct SygusVarFreeAttributeId
  68 {
  69 };
  70 typedef expr::Attribute<SygusVarFreeAttributeId, Node> SygusVarFreeAttribute;
  71 // ----------------------- end sygus datatype attributes
  72
  73 namespace datatypes {
  74 namespace utils {
  75
  76 /** get instantiate cons
  77  *
  78  * This returns the term C( sel^{C,1}( n ), ..., sel^{C,m}( n ) ),
  79  * where C is the index^{th} constructor of datatype dt.
  80  */
  81 Node getInstCons(Node n, const DType& dt, int index);
  82 /** is instantiation cons
  83  *
  84  * If this method returns a value >=0, then that value, call it index,
  85  * is such that n = C( sel^{C,1}( t ), ..., sel^{C,m}( t ) ),
  86  * where C is the index^{th} constructor of dt.
  87  */
  88 int isInstCons(Node t, Node n, const DType& dt);
  89 /** is tester
  90  *
  91  * This method returns a value >=0 if n is a tester predicate. The return
  92  * value indicates the constructor index that the tester n is for. If this
  93  * method returns a value >=0, then it updates a to the argument that the
  94  * tester n applies to.
  95  */
  96 int isTester(Node n, Node& a);
  97 /** is tester, same as above but does not update an argument */
  98 int isTester(Node n);
  99 /**
 100  * Get the index of a constructor or tester in its datatype, or the
 101  * index of a selector in its constructor.  (Zero is always the
 102  * first index.)
 103  */
 104 size_t indexOf(Node n);
 105 /**
 106  * Get the index of constructor corresponding to selector.
 107  * (Zero is always the first index.)
 108  */
 109 size_t cindexOf(Node n);
 110 /**
 111  * Get the datatype of n.
 112  */
 113 const DType& datatypeOf(Node n);
 114 /** make tester is-C( n ), where C is the i^{th} constructor of dt */
 115 Node mkTester(Node n, int i, const DType& dt);
 116 /** make tester split
 117  *
 118  * Returns the formula (OR is-C1( n ) ... is-Ck( n ) ), where C1...Ck
 119  * are the constructors of n's type (dt).
 120  */
 121 Node mkSplit(Node n, const DType& dt);
 122 /** returns true iff n is a constructor term with no datatype children */
 123 bool isNullaryApplyConstructor(Node n);
 124 /** returns true iff c is a constructor with no datatype children */
 125 bool isNullaryConstructor(const DTypeConstructor& c);
 126 /** check clash
 127  *
 128  * This method returns true if and only if n1 and n2 have a skeleton that has
 129  * conflicting constructors at some term position.
 130  * Examples of terms that clash are:
 131  *   C( x, y ) and D( z )
 132  *   C( D( x ), y ) and C( E( x ), y )
 133  * Examples of terms that do not clash are:
 134  *   C( x, y ) and C( D( x ), y )
 135  *   C( D( x ), y ) and C( x, E( z ) )
 136  *   C( x, y ) and z
 137  */
 138 bool checkClash(Node n1, Node n2, std::vector<Node>& rew);
 139
 140 // ------------------------ sygus utils
 141
 142 /** get operator kind for sygus builtin
 143  *
 144  * This returns the Kind corresponding to applications of the operator op
 145  * when building the builtin version of sygus terms. This is used by the
 146  * function mkSygusTerm.
 147  */
 148 Kind getOperatorKindForSygusBuiltin(Node op);
 149 /**
 150  * Returns the total version of Kind k if it is a partial operator, or
 151  * otherwise k itself.
 152  */
 153 Kind getEliminateKind(Kind k);
 154 /**
 155  * Returns a version of n where all partial functions such as bvudiv
 156  * have been replaced by their total versions like bvudiv_total.
 157  */
 158 Node eliminatePartialOperators(Node n);
 159 /** make sygus term
 160  *
 161  * This function returns a builtin term f( children[0], ..., children[n] )
 162  * where f is the builtin op that the i^th constructor of sygus datatype dt
 163  * encodes. If doBetaReduction is true, then lambdas are eagerly eliminated
 164  * via beta reduction.
 165  *
 166  * If isExternal is true, then the returned term respects the original grammar
 167  * that was provided. This includes the use of defined functions.
 168  */
 169 Node mkSygusTerm(const DType& dt,
 170                  unsigned i,
 171                  const std::vector<Node>& children,
 172                  bool doBetaReduction = true,
 173                  bool isExternal = false);
 174 /**
 175  * Same as above, but we already have the sygus operator op. The above method
 176  * is syntax sugar for calling this method on dt[i].getSygusOp().
 177  */
 178 Node mkSygusTerm(Node op,
 179                  const std::vector<Node>& children,
 180                  bool doBetaReduction = true);
 181 /**
 182  * n is a builtin term that is an application of operator op.
 183  *
 184  * This returns an n' such that (eval n args) is n', where n' is a instance of
 185  * n for the appropriate substitution.
 186  *
 187  * For example, given a function-to-synthesize with formal argument list (x,y),
 188  * say we have grammar:
 189  *   A -> A+A | A+x | A+(x+y) | y
 190  * These lead to constructors with sygus ops:
 191  *   C1 / (lambda w1 w2. w1+w2)
 192  *   C2 / (lambda w1. w1+x)
 193  *   C3 / (lambda w1. w1+(x+y))
 194  *   C4 / y
 195  * Examples of calling this function:
 196  *   applySygusArgs( dt, C1, (APPLY_UF (lambda w1 w2. w1+w2) t1 t2), { 3, 5 } )
 197  *     ... returns (APPLY_UF (lambda w1 w2. w1+w2) t1 t2).
 198  *   applySygusArgs( dt, C2, (APPLY_UF (lambda w1. w1+x) t1), { 3, 5 } )
 199  *     ... returns (APPLY_UF (lambda w1. w1+3) t1).
 200  *   applySygusArgs( dt, C3, (APPLY_UF (lambda w1. w1+(x+y)) t1), { 3, 5 } )
 201  *     ... returns (APPLY_UF (lambda w1. w1+(3+5)) t1).
 202  *   applySygusArgs( dt, C4, y, { 3, 5 } )
 203  *     ... returns 5.
 204  * Notice the attribute SygusVarFreeAttribute is applied to C1, C2, C3, C4,
 205  * to cache the results of whether the evaluation of this constructor needs
 206  * a substitution over the formal argument list of the function-to-synthesize.
 207  */
 208 Node applySygusArgs(const DType& dt,
 209                     Node op,
 210                     Node n,
 211                     const std::vector<Node>& args);
 212 /** Sygus to builtin
 213  *
 214  * This method converts a constant term of SyGuS datatype type to its builtin
 215  * equivalent. For example, given input C_*( C_x(), C_y() ), this method returns
 216  * x*y, assuming C_+, C_x, and C_y have sygus operators *, x, and y
 217  * respectively.
 218  *
 219  * If isExternal is true, then the returned term respects the original grammar
 220  * that was provided. This includes the use of defined functions. This argument
 221  * should typically be false, unless we are e.g. exporting the value of the
 222  * term as a final solution.
 223  */
 224 Node sygusToBuiltin(Node c, bool isExternal = false);
 225 /** Sygus to builtin eval
 226  *
 227  * This method returns the rewritten form of (DT_SYGUS_EVAL n args). Notice that
 228  * n does not necessarily need to be a constant.
 229  *
 230  * It does so by (1) converting constant subterms of n to builtin terms and
 231  * evaluating them on the arguments args, (2) unfolding non-constant
 232  * applications of sygus constructors in n with respect to args and (3)
 233  * converting all other non-constant subterms of n to applications of
 234  * DT_SYGUS_EVAL.
 235  *
 236  * For example, if
 237  *   n = C_+( C_*( C_x(), C_y() ), n' ), and args = { 3, 4 }
 238  * where n' is a variable, then this method returns:
 239  *   12 + (DT_SYGUS_EVAL n' 3 4)
 240  * Notice that the subterm C_*( C_x(), C_y() ) is converted to its builtin
 241  * equivalent x*y and evaluated under the substition { x -> 3, x -> 4 } giving
 242  * 12. The subterm n' is non-constant and thus we return its evaluation under
 243  * 3,4, giving the term (DT_SYGUS_EVAL n' 3 4). Since the top-level constructor
 244  * is C_+, these terms are added together to give the result.
 245  */
 246 Node sygusToBuiltinEval(Node n, const std::vector<Node>& args);
 247
 248 // ------------------------ end sygus utils
 249
 250 }  // namespace utils
 251 }  // namespace datatypes
 252 }  // namespace theory
 253 }  // namespace CVC4
 254
 255 #endif