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, Morgan Deters
   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 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 namespace datatypes {
  31 namespace utils {
  32
  33 /** get instantiate cons
  34  *
  35  * This returns the term C( sel^{C,1}( n ), ..., sel^{C,m}( n ) ),
  36  * where C is the index^{th} constructor of datatype dt.
  37  */
  38 Node getInstCons(Node n, const DType& dt, int index);
  39 /** is instantiation cons
  40  *
  41  * If this method returns a value >=0, then that value, call it index,
  42  * is such that n = C( sel^{C,1}( t ), ..., sel^{C,m}( t ) ),
  43  * where C is the index^{th} constructor of dt.
  44  */
  45 int isInstCons(Node t, Node n, const DType& dt);
  46 /** is tester
  47  *
  48  * This method returns a value >=0 if n is a tester predicate. The return
  49  * value indicates the constructor index that the tester n is for. If this
  50  * method returns a value >=0, then it updates a to the argument that the
  51  * tester n applies to.
  52  */
  53 int isTester(Node n, Node& a);
  54 /** is tester, same as above but does not update an argument */
  55 int isTester(Node n);
  56 /**
  57  * Get the index of a constructor or tester in its datatype, or the
  58  * index of a selector in its constructor.  (Zero is always the
  59  * first index.)
  60  */
  61 size_t indexOf(Node n);
  62 /**
  63  * Get the index of constructor corresponding to selector.
  64  * (Zero is always the first index.)
  65  */
  66 size_t cindexOf(Node n);
  67 /**
  68  * Get the datatype of n.
  69  */
  70 const DType& datatypeOf(Node n);
  71 /** make tester is-C( n ), where C is the i^{th} constructor of dt */
  72 Node mkTester(Node n, int i, const DType& dt);
  73 /** make tester split
  74  *
  75  * Returns the formula (OR is-C1( n ) ... is-Ck( n ) ), where C1...Ck
  76  * are the constructors of n's type (dt).
  77  */
  78 Node mkSplit(Node n, const DType& dt);
  79 /** returns true iff n is a constructor term with no datatype children */
  80 bool isNullaryApplyConstructor(Node n);
  81 /** returns true iff c is a constructor with no datatype children */
  82 bool isNullaryConstructor(const DTypeConstructor& c);
  83 /** check clash
  84  *
  85  * This method returns true if and only if n1 and n2 have a skeleton that has
  86  * conflicting constructors at some term position.
  87  * Examples of terms that clash are:
  88  *   C( x, y ) and D( z )
  89  *   C( D( x ), y ) and C( E( x ), y )
  90  * Examples of terms that do not clash are:
  91  *   C( x, y ) and C( D( x ), y )
  92  *   C( D( x ), y ) and C( x, E( z ) )
  93  *   C( x, y ) and z
  94  */
  95 bool checkClash(Node n1, Node n2, std::vector<Node>& rew);
  96
  97 }  // namespace utils
  98 }  // namespace datatypes
  99 }  // namespace theory
 100 }  // namespace CVC4
 101
 102 #endif