src/theory/quantifiers/quantifiers_attributes.h

   1 /*********************                                                        */
   2 /*! \file quantifiers_attributes.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Paul Meng, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 quantifiers that are axioms */
  31 struct AxiomAttributeId {};
  32 typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
  33
  34 /** Attribute true for quantifiers that are conjecture */
  35 struct ConjectureAttributeId {};
  36 typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
  37
  38 /** Attribute true for function definition quantifiers */
  39 struct FunDefAttributeId {};
  40 typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
  41
  42 /** Attribute true for quantifiers that we are doing quantifier elimination on */
  43 struct QuantElimAttributeId {};
  44 typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute;
  45
  46 /** Attribute true for quantifiers that we are doing partial quantifier elimination on */
  47 struct QuantElimPartialAttributeId {};
  48 typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;
  49
  50 /** Attribute true for quantifiers that are SyGus conjectures */
  51 struct SygusAttributeId {};
  52 typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
  53
  54 /** Attribute true for quantifiers that are synthesis conjectures */
  55 struct SynthesisAttributeId {};
  56 typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
  57
  58 /** Attribute for setting printing information for sygus variables
  59  *
  60  * For variable d of sygus datatype type, if
  61  * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t.
  62  */
  63 struct SygusPrintProxyAttributeId
  64 {
  65 };
  66 typedef expr::Attribute<SygusPrintProxyAttributeId, Node>
  67     SygusPrintProxyAttribute;
  68
  69 namespace quantifiers {
  70
  71 /** Attribute priority for rewrite rules */
  72 //struct RrPriorityAttributeId {};
  73 //typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute;
  74
  75 /** This struct stores attributes for a single quantified formula */
  76 struct QAttributes
  77 {
  78  public:
  79   QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
  80                   d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
  81   ~QAttributes(){}
  82   /** does the quantified formula have a pattern? */
  83   bool d_hasPattern;
  84   /** if non-null, this is the rewrite rule representation of the quantified
  85    * formula */
  86   Node d_rr;
  87   /** is this formula marked a conjecture? */
  88   bool d_conjecture;
  89   /** is this formula marked an axiom? */
  90   bool d_axiom;
  91   /** if non-null, this quantified formula is a function definition for function
  92    * d_fundef_f */
  93   Node d_fundef_f;
  94   /** is this formula marked as a sygus conjecture? */
  95   bool d_sygus;
  96   /** is this formula marked as a synthesis (non-sygus) conjecture? */
  97   bool d_synthesis;
  98   /** if a rewrite rule, then this is the priority value for the rewrite rule */
  99   int d_rr_priority;
 100   /** stores the maximum instantiation level allowed for this quantified formula
 101    * (-1 means allow any) */
 102   int d_qinstLevel;
 103   /** is this formula marked for quantifier elimination? */
 104   bool d_quant_elim;
 105   /** is this formula marked for partial quantifier elimination? */
 106   bool d_quant_elim_partial;
 107   /** the instantiation pattern list for this quantified formula (its 3rd child)
 108    */
 109   Node d_ipl;
 110   /** the quantifier id associated with this formula */
 111   Node d_qid_num;
 112   /** is this quantified formula a rewrite rule? */
 113   bool isRewriteRule() { return !d_rr.isNull(); }
 114   /** is this quantified formula a function definition? */
 115   bool isFunDef() { return !d_fundef_f.isNull(); }
 116 };
 117
 118 /** This class caches information about attributes of quantified formulas
 119 *
 120 * It also has static utility functions used for determining attributes and
 121 * information about
 122 * quantified formulas.
 123 */
 124 class QuantAttributes
 125 {
 126 public:
 127   QuantAttributes( QuantifiersEngine * qe );
 128   ~QuantAttributes(){}
 129   /** set user attribute
 130   * This function applies an attribute
 131   * This can be called when we mark expressions with attributes, e.g. (! q
 132   * :attribute attr [node_values, str_value...]),
 133   * It can also be called internally in various ways (for SyGus, quantifier
 134   * elimination, etc.)
 135   */
 136   static void setUserAttribute(const std::string& attr,
 137                                Node q,
 138                                std::vector<Node>& node_values,
 139                                std::string str_value);
 140
 141   /** compute quantifier attributes */
 142   static void computeQuantAttributes(Node q, QAttributes& qa);
 143   /** compute the attributes for q */
 144   void computeAttributes(Node q);
 145
 146   /** is quantifier treated as a rewrite rule? */
 147   static bool checkRewriteRule( Node q );
 148   /** get the rewrite rule associated with the quanfied formula */
 149   static Node getRewriteRule( Node q );
 150   /** is fun def */
 151   static bool checkFunDef( Node q );
 152   /** is fun def */
 153   static bool checkFunDefAnnotation( Node ipl );
 154   /** is sygus conjecture */
 155   static bool checkSygusConjecture( Node q );
 156   /** is sygus conjecture */
 157   static bool checkSygusConjectureAnnotation( Node ipl );
 158   /** get fun def body */
 159   static Node getFunDefHead( Node q );
 160   /** get fun def body */
 161   static Node getFunDefBody( Node q );
 162   /** is quant elim annotation */
 163   static bool checkQuantElimAnnotation( Node ipl );
 164
 165   /** is conjecture */
 166   bool isConjecture( Node q );
 167   /** is axiom */
 168   bool isAxiom( Node q );
 169   /** is function definition */
 170   bool isFunDef( Node q );
 171   /** is sygus conjecture */
 172   bool isSygus( Node q );
 173   /** is synthesis conjecture */
 174   bool isSynthesis( Node q );
 175   /** get instantiation level */
 176   int getQuantInstLevel( Node q );
 177   /** get rewrite rule priority */
 178   int getRewriteRulePriority( Node q );
 179   /** is quant elim */
 180   bool isQuantElim( Node q );
 181   /** is quant elim partial */
 182   bool isQuantElimPartial( Node q );
 183   /** get quant id num */
 184   int getQuantIdNum( Node q );
 185   /** get quant id num */
 186   Node getQuantIdNumNode( Node q );
 187
 188 private:
 189   /** pointer to quantifiers engine */
 190   QuantifiersEngine * d_quantEngine;
 191   /** cache of attributes */
 192   std::map< Node, QAttributes > d_qattr;
 193   /** function definitions */
 194   std::map< Node, bool > d_fun_defs;
 195 };
 196
 197 }
 198 }
 199 }
 200
 201 #endif