src/theory/quantifiers/quantifiers_attributes.h

   1 /*********************                                                        */
   2 /*! \file quantifiers_attributes.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 Attributes for the theory quantifiers
  13  **
  14  ** Attributes for the theory quantifiers.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
  20 #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
  21
  22 #include "expr/attribute.h"
  23 #include "expr/node.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 class QuantifiersEngine;
  29
  30 /** Attribute true for function definition quantifiers */
  31 struct FunDefAttributeId {};
  32 typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
  33
  34 /** Attribute true for quantifiers that we are doing quantifier elimination on */
  35 struct QuantElimAttributeId {};
  36 typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute;
  37
  38 /** Attribute true for quantifiers that we are doing partial quantifier elimination on */
  39 struct QuantElimPartialAttributeId {};
  40 typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;
  41
  42 /** Attribute true for quantifiers that are SyGus conjectures */
  43 struct SygusAttributeId {};
  44 typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
  45
  46 /**Attribute to give names to quantified formulas */
  47 struct QuantNameAttributeId
  48 {
  49 };
  50 typedef expr::Attribute<QuantNameAttributeId, bool> QuantNameAttribute;
  51
  52 struct InstLevelAttributeId
  53 {
  54 };
  55 typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
  56
  57 /** Attribute for setting printing information for sygus variables
  58  *
  59  * For variable d of sygus datatype type, if
  60  * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t.
  61  */
  62 struct SygusPrintProxyAttributeId
  63 {
  64 };
  65 typedef expr::Attribute<SygusPrintProxyAttributeId, Node>
  66     SygusPrintProxyAttribute;
  67
  68 /** Attribute for specifying a "side condition" for a sygus conjecture
  69  *
  70  * A sygus conjecture of the form exists f. forall x. P[f,x] whose side
  71  * condition is C[f] has the semantics exists f. C[f] ^ forall x. P[f,x].
  72  */
  73 struct SygusSideConditionAttributeId
  74 {
  75 };
  76 typedef expr::Attribute<SygusSideConditionAttributeId, Node>
  77     SygusSideConditionAttribute;
  78
  79 /** Attribute for indicating that a sygus variable encodes a term
  80  *
  81  * This is used, e.g., for abduction where the formal argument list of the
  82  * abduct-to-synthesize corresponds to the free variables of the sygus
  83  * problem.
  84  */
  85 struct SygusVarToTermAttributeId
  86 {
  87 };
  88 typedef expr::Attribute<SygusVarToTermAttributeId, Node>
  89     SygusVarToTermAttribute;
  90
  91 namespace quantifiers {
  92
  93 /** Attribute priority for rewrite rules */
  94 //struct RrPriorityAttributeId {};
  95 //typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute;
  96
  97 /** This struct stores attributes for a single quantified formula */
  98 struct QAttributes
  99 {
 100  public:
 101   QAttributes()
 102       : d_hasPattern(false),
 103         d_sygus(false),
 104         d_qinstLevel(-1),
 105         d_quant_elim(false),
 106         d_quant_elim_partial(false)
 107   {
 108   }
 109   ~QAttributes(){}
 110   /** does the quantified formula have a pattern? */
 111   bool d_hasPattern;
 112   /** if non-null, this quantified formula is a function definition for function
 113    * d_fundef_f */
 114   Node d_fundef_f;
 115   /** is this formula marked as a sygus conjecture? */
 116   bool d_sygus;
 117   /** side condition for sygus conjectures */
 118   Node d_sygusSideCondition;
 119   /** stores the maximum instantiation level allowed for this quantified formula
 120    * (-1 means allow any) */
 121   int d_qinstLevel;
 122   /** is this formula marked for quantifier elimination? */
 123   bool d_quant_elim;
 124   /** is this formula marked for partial quantifier elimination? */
 125   bool d_quant_elim_partial;
 126   /** the instantiation pattern list for this quantified formula (its 3rd child)
 127    */
 128   Node d_ipl;
 129   /** The name of this quantified formula, used for :qid */
 130   Node d_name;
 131   /** The (internal) quantifier id associated with this formula */
 132   Node d_qid_num;
 133   /** is this quantified formula a function definition? */
 134   bool isFunDef() const { return !d_fundef_f.isNull(); }
 135   /**
 136    * Is this a standard quantifier? A standard quantifier is one that we can
 137    * perform destructive updates (variable elimination, miniscoping, etc).
 138    *
 139    * A quantified formula is not standard if it is sygus, one for which
 140    * we are performing quantifier elimination, is a function definition, or
 141    * has a name.
 142    */
 143   bool isStandard() const;
 144 };
 145
 146 /** This class caches information about attributes of quantified formulas
 147 *
 148 * It also has static utility functions used for determining attributes and
 149 * information about
 150 * quantified formulas.
 151 */
 152 class QuantAttributes
 153 {
 154 public:
 155   QuantAttributes( QuantifiersEngine * qe );
 156   ~QuantAttributes(){}
 157   /** set user attribute
 158   * This function applies an attribute
 159   * This can be called when we mark expressions with attributes, e.g. (! q
 160   * :attribute attr [node_values, str_value...]),
 161   * It can also be called internally in various ways (for SyGus, quantifier
 162   * elimination, etc.)
 163   */
 164   static void setUserAttribute(const std::string& attr,
 165                                Node q,
 166                                std::vector<Node>& node_values,
 167                                std::string str_value);
 168
 169   /** compute quantifier attributes */
 170   static void computeQuantAttributes(Node q, QAttributes& qa);
 171   /** compute the attributes for q */
 172   void computeAttributes(Node q);
 173
 174   /** is fun def */
 175   static bool checkFunDef( Node q );
 176   /** is fun def */
 177   static bool checkFunDefAnnotation( Node ipl );
 178   /** is sygus conjecture */
 179   static bool checkSygusConjecture( Node q );
 180   /** is sygus conjecture */
 181   static bool checkSygusConjectureAnnotation( Node ipl );
 182   /** get fun def body */
 183   static Node getFunDefHead( Node q );
 184   /** get fun def body */
 185   static Node getFunDefBody( Node q );
 186   /** is quant elim annotation */
 187   static bool checkQuantElimAnnotation( Node ipl );
 188
 189   /** is function definition */
 190   bool isFunDef( Node q );
 191   /** is sygus conjecture */
 192   bool isSygus( Node q );
 193   /** get instantiation level */
 194   int getQuantInstLevel( Node q );
 195   /** get rewrite rule priority */
 196   int getRewriteRulePriority( Node q );
 197   /** is quant elim */
 198   bool isQuantElim( Node q );
 199   /** is quant elim partial */
 200   bool isQuantElimPartial( Node q );
 201   /** get quant name, which is used for :qid */
 202   Node getQuantName(Node q) const;
 203   /** get (internal) quant id num */
 204   int getQuantIdNum( Node q );
 205   /** get (internal)quant id num */
 206   Node getQuantIdNumNode( Node q );
 207
 208   /** set instantiation level attr */
 209   static void setInstantiationLevelAttr(Node n, uint64_t level);
 210   /** set instantiation level attr */
 211   static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level);
 212
 213  private:
 214   /** pointer to quantifiers engine */
 215   QuantifiersEngine * d_quantEngine;
 216   /** cache of attributes */
 217   std::map< Node, QAttributes > d_qattr;
 218   /** function definitions */
 219   std::map< Node, bool > d_fun_defs;
 220 };
 221
 222 }
 223 }
 224 }
 225
 226 #endif