Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Utils for counterexample-guided quantifier instantiation.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__THEORY__QUANTIFIERS__CEG_UTILS_H
      16                 :            : #define CVC5__THEORY__QUANTIFIERS__CEG_UTILS_H
      17                 :            : 
      18                 :            : #include <vector>
      19                 :            : 
      20                 :            : #include "expr/node.h"
      21                 :            : #include "smt/env_obj.h"
      22                 :            : #include "theory/inference_id.h"
      23                 :            : #include "util/statistics_stats.h"
      24                 :            : 
      25                 :            : namespace cvc5::internal {
      26                 :            : namespace theory {
      27                 :            : namespace quantifiers {
      28                 :            : 
      29                 :            : /**
      30                 :            :  * Descriptions of the types of constraints that a term was solved for in.
      31                 :            :  */
      32                 :            : enum CegTermType
      33                 :            : {
      34                 :            :   // invalid
      35                 :            :   CEG_TT_INVALID,
      36                 :            :   // term was the result of solving an equality
      37                 :            :   CEG_TT_EQUAL,
      38                 :            :   // term was the result of solving a non-strict lower bound x >= t
      39                 :            :   CEG_TT_LOWER,
      40                 :            :   // term was the result of solving a strict lower bound x > t
      41                 :            :   CEG_TT_LOWER_STRICT,
      42                 :            :   // term was the result of solving a non-strict upper bound x <= t
      43                 :            :   CEG_TT_UPPER,
      44                 :            :   // term was the result of solving a strict upper bound x < t
      45                 :            :   CEG_TT_UPPER_STRICT,
      46                 :            : };
      47                 :            : /** make (non-strict term type) c a strict term type */
      48                 :            : CegTermType mkStrictCTT(CegTermType c);
      49                 :            : /** negate c (lower/upper bounds are swapped) */
      50                 :            : CegTermType mkNegateCTT(CegTermType c);
      51                 :            : /** is c a strict term type? */
      52                 :            : bool isStrictCTT(CegTermType c);
      53                 :            : /** is c a lower bound? */
      54                 :            : bool isLowerBoundCTT(CegTermType c);
      55                 :            : /** is c an upper bound? */
      56                 :            : bool isUpperBoundCTT(CegTermType c);
      57                 :            : 
      58                 :            : /** Term Properties
      59                 :            :  *
      60                 :            :  * Stores properties for a variable to solve for in counterexample-guided
      61                 :            :  * instantiation.
      62                 :            :  *
      63                 :            :  * For LIA, this includes the coefficient of the variable, and the bound type
      64                 :            :  * for the variable.
      65                 :            :  */
      66                 :            : class TermProperties
      67                 :            : {
      68                 :            :  public:
      69                 :    1932454 :   TermProperties() : d_type(CEG_TT_EQUAL) {}
      70                 :    6847059 :   virtual ~TermProperties() {}
      71                 :            : 
      72                 :            :   /**
      73                 :            :    * Type for the solution term. For arithmetic this corresponds to bound type
      74                 :            :    * of the constraint that the constraint the term was solved for in.
      75                 :            :    */
      76                 :            :   CegTermType d_type;
      77                 :            :   // for arithmetic
      78                 :            :   Node d_coeff;
      79                 :            :   // get cache node
      80                 :            :   // we consider terms + TermProperties that are unique up to their cache node
      81                 :            :   // (see constructInstantiationInc)
      82                 :      88333 :   Node getCacheNode() const { return d_coeff; }
      83                 :            :   // is non-basic
      84                 :     257487 :   bool isBasic() const { return d_coeff.isNull(); }
      85                 :            :   // get modified term
      86                 :      10182 :   Node getModifiedTerm(Node pv) const
      87                 :            :   {
      88         [ +  + ]:      10182 :     if (!d_coeff.isNull())
      89                 :            :     {
      90                 :        739 :       return NodeManager::mkNode(Kind::MULT, d_coeff, pv);
      91                 :            :     }
      92                 :            :     else
      93                 :            :     {
      94                 :       9443 :       return pv;
      95                 :            :     }
      96                 :            :   }
      97                 :            :   // compose property, should be such that:
      98                 :            :   //   p.getModifiedTerm( this.getModifiedTerm( x ) ) =
      99                 :            :   //   this_updated.getModifiedTerm( x )
     100                 :            :   void composeProperty(TermProperties& p);
     101                 :            : };
     102                 :            : 
     103                 :            : /** Solved form
     104                 :            :  *  This specifies a substitution:
     105                 :            :  *  { d_props[i].getModifiedTerm(d_vars[i]) -> d_subs[i] | i = 0...|d_vars| }
     106                 :            :  */
     107                 :            : class SolvedForm
     108                 :            : {
     109                 :            :  public:
     110                 :            :   // list of variables
     111                 :            :   std::vector<Node> d_vars;
     112                 :            :   // list of terms that they are substituted to
     113                 :            :   std::vector<Node> d_subs;
     114                 :            :   // properties for each variable
     115                 :            :   std::vector<TermProperties> d_props;
     116                 :            :   // the variables that have non-basic information regarding how they are
     117                 :            :   // substituted
     118                 :            :   //   an example is for linear arithmetic, we store "substitution with
     119                 :            :   //   coefficients".
     120                 :            :   std::vector<Node> d_non_basic;
     121                 :            :   // push the substitution pv_prop.getModifiedTerm(pv) -> n
     122                 :            :   void push_back(Node pv, Node n, TermProperties& pv_prop);
     123                 :            :   // pop the substitution pv_prop.getModifiedTerm(pv) -> n
     124                 :            :   void pop_back(TermProperties& pv_prop);
     125                 :            :   // is this solved form empty?
     126                 :       1742 :   bool empty() { return d_vars.empty(); }
     127                 :            : 
     128                 :            :  public:
     129                 :            :   // theta values (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017)
     130                 :            :   std::vector<Node> d_theta;
     131                 :            :   // get the current value for theta (for LIA, see Section 4 of
     132                 :            :   // Reynolds/King/Kuncak FMSD 2017)
     133                 :      55521 :   Node getTheta()
     134                 :            :   {
     135         [ +  + ]:      55521 :     if (d_theta.empty())
     136                 :            :     {
     137                 :      55036 :       return Node::null();
     138                 :            :     }
     139                 :            :     else
     140                 :            :     {
     141                 :        485 :       return d_theta[d_theta.size() - 1];
     142                 :            :     }
     143                 :            :   }
     144                 :            : };
     145                 :            : 
     146                 :            : /** instantiation effort levels
     147                 :            :  *
     148                 :            :  * This effort is used to stratify the construction of
     149                 :            :  * instantiations for some theories that may result to
     150                 :            :  * using model value instantiations.
     151                 :            :  */
     152                 :            : enum CegInstEffort
     153                 :            : {
     154                 :            :   // uninitialized
     155                 :            :   CEG_INST_EFFORT_NONE,
     156                 :            :   // standard effort level
     157                 :            :   CEG_INST_EFFORT_STANDARD,
     158                 :            :   // standard effort level, but we have used model values
     159                 :            :   CEG_INST_EFFORT_STANDARD_MV,
     160                 :            :   // full effort level
     161                 :            :   CEG_INST_EFFORT_FULL
     162                 :            : };
     163                 :            : 
     164                 :            : std::ostream& operator<<(std::ostream& os, CegInstEffort e);
     165                 :            : 
     166                 :            : /** instantiation phase for variables
     167                 :            :  *
     168                 :            :  * This indicates the phase in which we constructed
     169                 :            :  * a substitution for individual variables.
     170                 :            :  */
     171                 :            : enum CegInstPhase
     172                 :            : {
     173                 :            :   // uninitialized
     174                 :            :   CEG_INST_PHASE_NONE,
     175                 :            :   // instantiation constructed during traversal of equivalence classes
     176                 :            :   CEG_INST_PHASE_EQC,
     177                 :            :   // instantiation constructed during solving equalities
     178                 :            :   CEG_INST_PHASE_EQUAL,
     179                 :            :   // instantiation constructed by looking at theory assertions
     180                 :            :   CEG_INST_PHASE_ASSERTION,
     181                 :            :   // instantiation constructed by querying model value
     182                 :            :   CEG_INST_PHASE_MVALUE,
     183                 :            : };
     184                 :            : 
     185                 :            : std::ostream& operator<<(std::ostream& os, CegInstPhase phase);
     186                 :            : 
     187                 :            : /**
     188                 :            :  * The handled status of a sort/term/quantified formula, indicating whether
     189                 :            :  * counterexample-guided instantiation handles it.
     190                 :            :  */
     191                 :            : enum CegHandledStatus
     192                 :            : {
     193                 :            :   // the sort/term/quantified formula is unhandled by cegqi
     194                 :            :   CEG_UNHANDLED,
     195                 :            :   // the sort/term/quantified formula is partially handled by cegqi
     196                 :            :   CEG_PARTIALLY_HANDLED,
     197                 :            :   // the sort/term/quantified formula is handled by cegqi
     198                 :            :   CEG_HANDLED,
     199                 :            :   // the sort/term/quantified formula is handled by cegqi, regardless of
     200                 :            :   // additional factors
     201                 :            :   CEG_HANDLED_UNCONDITIONAL,
     202                 :            : };
     203                 :            : std::ostream& operator<<(std::ostream& os, CegHandledStatus status);
     204                 :            : 
     205                 :            : }  // namespace quantifiers
     206                 :            : }  // namespace theory
     207                 :            : }  // namespace cvc5::internal
     208                 :            : 
     209                 :            : #endif