LCOV - code coverage report
Current view: top level - buildbot/coverage/build/src/theory/quantifiers - quantifiers_attributes.h (source / functions) Hit Total Coverage
Test: coverage.info Lines: 8 8 100.0 %
Date: 2024-11-05 12:39:23 Functions: 5 5 100.0 %
Branches: 0 0 -

           Branch data     Line data    Source code
       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Attributes for the theory quantifiers.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
      19                 :            : #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
      20                 :            : 
      21                 :            : #include "expr/attribute.h"
      22                 :            : #include "expr/node.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace theory {
      26                 :            : 
      27                 :            : /** Attribute true for function definition quantifiers */
      28                 :            : struct FunDefAttributeId {};
      29                 :            : typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
      30                 :            : 
      31                 :            : /** Attribute true for quantifiers that we are doing partial quantifier elimination on */
      32                 :            : struct QuantElimPartialAttributeId {};
      33                 :            : typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;
      34                 :            : 
      35                 :            : /** Attribute true for quantifiers that are SyGus conjectures */
      36                 :            : struct SygusAttributeId {};
      37                 :            : typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
      38                 :            : 
      39                 :            : /**
      40                 :            :  * Attribute set to the name of the binary for quantifiers that are oracle
      41                 :            :  * interfaces. In detail, an oracle interface is a quantified formula of the
      42                 :            :  * form:
      43                 :            :  *   (FORALL
      44                 :            :  *     (BOUND_VAR_LIST i1 ... in o1 ... om)
      45                 :            :  *     (ORACLE_FORMULA_GEN A C)
      46                 :            :  *     (INST_PATTERN_LIST k))
      47                 :            :  * where i1 ... in are the inputs to the interface, o1 ... om are the outputs
      48                 :            :  * of the interface, A is the "assumption" formula, C is the "constraint"
      49                 :            :  * formula, and k is a dummy skolem that has been marked with this attribute.
      50                 :            :  * The string value of this attribute specifies a binary whose I/O behavior
      51                 :            :  * should match the types of inputs and outputs specified by i1 ... in and
      52                 :            :  * o1 ... om respectively.
      53                 :            :  */
      54                 :            : struct OracleInterfaceAttributeId
      55                 :            : {
      56                 :            : };
      57                 :            : typedef expr::Attribute<OracleInterfaceAttributeId, Node>
      58                 :            :     OracleInterfaceAttribute;
      59                 :            : 
      60                 :            : /**Attribute to give names to quantified formulas */
      61                 :            : struct QuantNameAttributeId
      62                 :            : {
      63                 :            : };
      64                 :            : typedef expr::Attribute<QuantNameAttributeId, bool> QuantNameAttribute;
      65                 :            : 
      66                 :            : /** Attribute for setting printing information for sygus variables
      67                 :            :  *
      68                 :            :  * For variable d of sygus datatype type, if
      69                 :            :  * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t.
      70                 :            :  */
      71                 :            : struct SygusPrintProxyAttributeId
      72                 :            : {
      73                 :            : };
      74                 :            : typedef expr::Attribute<SygusPrintProxyAttributeId, Node>
      75                 :            :     SygusPrintProxyAttribute;
      76                 :            : 
      77                 :            : /** Attribute for specifying a "side condition" for a sygus conjecture
      78                 :            :  *
      79                 :            :  * A sygus conjecture of the form exists f. forall x. P[f,x] whose side
      80                 :            :  * condition is C[f] has the semantics exists f. C[f] ^ forall x. P[f,x].
      81                 :            :  */
      82                 :            : struct SygusSideConditionAttributeId
      83                 :            : {
      84                 :            : };
      85                 :            : typedef expr::Attribute<SygusSideConditionAttributeId, Node>
      86                 :            :     SygusSideConditionAttribute;
      87                 :            : 
      88                 :            : /** Attribute for indicating that a sygus variable encodes a term
      89                 :            :  *
      90                 :            :  * This is used, e.g., for abduction where the formal argument list of the
      91                 :            :  * abduct-to-synthesize corresponds to the free variables of the sygus
      92                 :            :  * problem.
      93                 :            :  */
      94                 :            : struct SygusVarToTermAttributeId
      95                 :            : {
      96                 :            : };
      97                 :            : typedef expr::Attribute<SygusVarToTermAttributeId, Node>
      98                 :            :     SygusVarToTermAttribute;
      99                 :            : 
     100                 :            : /**
     101                 :            :  * Attribute marked true for types that are used as abstraction types in
     102                 :            :  * the finite model finding for function definitions algorithm.
     103                 :            :  */
     104                 :            : struct AbsTypeFunDefAttributeId
     105                 :            : {
     106                 :            : };
     107                 :            : typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
     108                 :            : 
     109                 :            : namespace quantifiers {
     110                 :            : 
     111                 :            : /** This struct stores attributes for a single quantified formula */
     112                 :            : struct QAttributes
     113                 :            : {
     114                 :            :  public:
     115                 :     551741 :   QAttributes()
     116                 :     551741 :       : d_hasPattern(false),
     117                 :            :         d_hasPool(false),
     118                 :            :         d_sygus(false),
     119                 :            :         d_qinstLevel(-1),
     120                 :            :         d_preserveStructure(false),
     121                 :            :         d_quant_elim(false),
     122                 :            :         d_quant_elim_partial(false),
     123                 :     551741 :         d_isQuantBounded(false)
     124                 :            :   {
     125                 :     551741 :   }
     126                 :     551720 :   ~QAttributes(){}
     127                 :            :   /** does the quantified formula have a pattern? */
     128                 :            :   bool d_hasPattern;
     129                 :            :   /** does the quantified formula have a pool? */
     130                 :            :   bool d_hasPool;
     131                 :            :   /** if non-null, this quantified formula is a function definition for function
     132                 :            :    * d_fundef_f */
     133                 :            :   Node d_fundef_f;
     134                 :            :   /** is this formula marked as a sygus conjecture? */
     135                 :            :   bool d_sygus;
     136                 :            :   /** the oracle, which stores an implementation */
     137                 :            :   Node d_oracle;
     138                 :            :   /** side condition for sygus conjectures */
     139                 :            :   Node d_sygusSideCondition;
     140                 :            :   /** stores the maximum instantiation level allowed for this quantified formula
     141                 :            :    * (-1 means allow any) */
     142                 :            :   int64_t d_qinstLevel;
     143                 :            :   /**
     144                 :            :    * Is this formula marked as preserving structure?
     145                 :            :    * For example, this attribute is marked when computing (partial) quantifier
     146                 :            :    * elimination on a quantified formula, but does not impact the solving method
     147                 :            :    * for it.
     148                 :            :    */
     149                 :            :   bool d_preserveStructure;
     150                 :            :   /**
     151                 :            :    * Is this formula marked for quantifier elimination? This impacts the
     152                 :            :    * strategy used for instantiating it, e.g. we always use CEGQI.
     153                 :            :    */
     154                 :            :   bool d_quant_elim;
     155                 :            :   /**
     156                 :            :    * Is this formula marked for partial quantifier elimination? This impacts the
     157                 :            :    * strategy used for instantiating it, e.g. we only invoke a single
     158                 :            :    * instantiation for it.
     159                 :            :    */
     160                 :            :   bool d_quant_elim_partial;
     161                 :            :   /** Is this formula internally generated and belonging to bounded integers? */
     162                 :            :   bool d_isQuantBounded;
     163                 :            :   /** the instantiation pattern list for this quantified formula (its 3rd child)
     164                 :            :    */
     165                 :            :   Node d_ipl;
     166                 :            :   /** The name of this quantified formula, used for :qid */
     167                 :            :   Node d_name;
     168                 :            :   /** The (internal) quantifier id associated with this formula */
     169                 :            :   Node d_qid_num;
     170                 :            :   /** is this quantified formula a function definition? */
     171                 :    3458630 :   bool isFunDef() const { return !d_fundef_f.isNull(); }
     172                 :            :   /** is this quantified formula an oracle interface quantifier? */
     173                 :    3369530 :   bool isOracleInterface() const { return !d_oracle.isNull(); }
     174                 :            :   /**
     175                 :            :    * Is this a standard quantifier? A standard quantifier is one that we can
     176                 :            :    * perform destructive updates (variable elimination, miniscoping, etc).
     177                 :            :    *
     178                 :            :    * A quantified formula is not standard if it is sygus, one for which
     179                 :            :    * we are performing quantifier elimination, or is a function definition.
     180                 :            :    */
     181                 :            :   bool isStandard() const;
     182                 :            : };
     183                 :            : 
     184                 :            : /** This class caches information about attributes of quantified formulas
     185                 :            : *
     186                 :            : * It also has static utility functions used for determining attributes and
     187                 :            : * information about
     188                 :            : * quantified formulas.
     189                 :            : */
     190                 :            : class QuantAttributes
     191                 :            : {
     192                 :            :  public:
     193                 :            :   QuantAttributes();
     194                 :      49516 :   ~QuantAttributes(){}
     195                 :            :   /** set user attribute
     196                 :            :    * This function applies an attribute
     197                 :            :    * This can be called when we mark expressions with attributes, e.g. (! q
     198                 :            :    * :attribute attr [nodeValues]),
     199                 :            :    * It can also be called internally in various ways (for SyGus, quantifier
     200                 :            :    * elimination, etc.)
     201                 :            :    */
     202                 :            :   static void setUserAttribute(const std::string& attr,
     203                 :            :                                TNode q,
     204                 :            :                                const std::vector<Node>& nodeValues);
     205                 :            : 
     206                 :            :   /** compute quantifier attributes */
     207                 :            :   static void computeQuantAttributes(Node q, QAttributes& qa);
     208                 :            :   /** compute the attributes for q */
     209                 :            :   void computeAttributes(Node q);
     210                 :            : 
     211                 :            :   /** is sygus conjecture */
     212                 :            :   static bool checkSygusConjecture( Node q );
     213                 :            :   /** is sygus conjecture */
     214                 :            :   static bool checkSygusConjectureAnnotation( Node ipl );
     215                 :            :   /** get fun def body */
     216                 :            :   static Node getFunDefHead( Node q );
     217                 :            :   /** get fun def body */
     218                 :            :   static Node getFunDefBody(Node q);
     219                 :            :   /** does q have a user-provided pattern? */
     220                 :            :   static bool hasPattern(Node q);
     221                 :            : 
     222                 :            :   /** is function definition */
     223                 :            :   bool isFunDef( Node q );
     224                 :            :   /** is sygus conjecture */
     225                 :            :   bool isSygus( Node q );
     226                 :            :   /** is oracle interface */
     227                 :            :   bool isOracleInterface(Node q);
     228                 :            :   /** get instantiation level */
     229                 :            :   int64_t getQuantInstLevel(Node q);
     230                 :            :   /** is quant elim partial */
     231                 :            :   bool isQuantElimPartial( Node q );
     232                 :            :   /** is internal quantifier */
     233                 :            :   bool isQuantBounded(Node q) const;
     234                 :            :   /** get quant name, which is used for :qid */
     235                 :            :   Node getQuantName(Node q) const;
     236                 :            :   /** Print quantified formula q, possibly using its name, if it has one */
     237                 :            :   std::string quantToString(Node q) const;
     238                 :            :   /** get (internal) quant id num */
     239                 :            :   int getQuantIdNum( Node q );
     240                 :            :   /** get (internal)quant id num */
     241                 :            :   Node getQuantIdNumNode( Node q );
     242                 :            : 
     243                 :            :   /** Make the instantiation attribute that marks "quantifier elimination" */
     244                 :            :   static Node mkAttrQuantifierElimination();
     245                 :            :   /** Make the instantiation attribute that marks to perserve its structure */
     246                 :            :   static Node mkAttrPreserveStructure();
     247                 :            :   /**
     248                 :            :    * Set instantiation level attribute for all subterms without an instantiation
     249                 :            :    * level in n to level.
     250                 :            :    */
     251                 :            :   static void setInstantiationLevelAttr(Node n, uint64_t level);
     252                 :            :   /**
     253                 :            :    * Get "instantiation level" for term n, if applicable. If n has an
     254                 :            :    * instantiation level, we return true and set level to its instantiation
     255                 :            :    * level.
     256                 :            :    *
     257                 :            :    * The instantiation level is an approximate measure of how many
     258                 :            :    * instantiations were required for generating term n. In particular,
     259                 :            :    * all new terms generated by an instantiation { x1 -> t1 ... xn -> tn } are
     260                 :            :    * assigned an instantiation level that is 1 + max(level(t1)...level(tn)),
     261                 :            :    * where all terms in the input formula have level 0.
     262                 :            :    */
     263                 :            :   static bool getInstantiationLevel(const Node& n, uint64_t& level);
     264                 :            : 
     265                 :            :  private:
     266                 :            :   /** An identifier for the method below */
     267                 :            :   enum class AttrType
     268                 :            :   {
     269                 :            :     ATTR_PRESERVE_STRUCTURE,
     270                 :            :     ATTR_QUANT_ELIM
     271                 :            :   };
     272                 :            :   /** Make attribute internal, helper for mkAttrX methods above. */
     273                 :            :   static Node mkAttrInternal(AttrType at);
     274                 :            :   /** cache of attributes */
     275                 :            :   std::map< Node, QAttributes > d_qattr;
     276                 :            :   /** function definitions */
     277                 :            :   std::map< Node, bool > d_fun_defs;
     278                 :            : };
     279                 :            : 
     280                 :            : /**
     281                 :            :  * Make a named quantified formula. This is a quantified formula that will
     282                 :            :  * print like:
     283                 :            :  *   (<k> <bvl> (! <body> :qid name))
     284                 :            :  */
     285                 :            : Node mkNamedQuant(Kind k, Node bvl, Node body, const std::string& name);
     286                 :            : }
     287                 :            : }
     288                 :            : }  // namespace cvc5::internal
     289                 :            : 
     290                 :            : #endif

Generated by: LCOV version 1.14