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                 :            :  * Implementation of utils for counterexample-guided quantifier instantiation.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/cegqi/ceg_utils.h"
      14                 :            : 
      15                 :            : #include "theory/arith/arith_utilities.h"
      16                 :            : 
      17                 :            : using namespace std;
      18                 :            : using namespace cvc5::internal::kind;
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : namespace theory {
      22                 :            : namespace quantifiers {
      23                 :            : 
      24                 :        921 : CegTermType mkStrictCTT(CegTermType c)
      25                 :            : {
      26 [ -  + ][ -  + ]:        921 :   Assert(!isStrictCTT(c));
                 [ -  - ]
      27         [ +  + ]:        921 :   if (c == CEG_TT_LOWER)
      28                 :            :   {
      29                 :        521 :     return CEG_TT_LOWER_STRICT;
      30                 :            :   }
      31         [ +  - ]:        400 :   else if (c == CEG_TT_UPPER)
      32                 :            :   {
      33                 :        400 :     return CEG_TT_UPPER_STRICT;
      34                 :            :   }
      35                 :          0 :   return c;
      36                 :            : }
      37                 :            : 
      38                 :       7593 : CegTermType mkNegateCTT(CegTermType c)
      39                 :            : {
      40         [ +  + ]:       7593 :   if (c == CEG_TT_LOWER)
      41                 :            :   {
      42                 :       2955 :     return CEG_TT_UPPER;
      43                 :            :   }
      44         [ +  - ]:       4638 :   else if (c == CEG_TT_UPPER)
      45                 :            :   {
      46                 :       4638 :     return CEG_TT_LOWER;
      47                 :            :   }
      48         [ -  - ]:          0 :   else if (c == CEG_TT_LOWER_STRICT)
      49                 :            :   {
      50                 :          0 :     return CEG_TT_UPPER_STRICT;
      51                 :            :   }
      52         [ -  - ]:          0 :   else if (c == CEG_TT_UPPER_STRICT)
      53                 :            :   {
      54                 :          0 :     return CEG_TT_LOWER_STRICT;
      55                 :            :   }
      56                 :          0 :   return c;
      57                 :            : }
      58                 :        921 : bool isStrictCTT(CegTermType c)
      59                 :            : {
      60 [ +  - ][ -  + ]:        921 :   return c == CEG_TT_LOWER_STRICT || c == CEG_TT_UPPER_STRICT;
      61                 :            : }
      62                 :          0 : bool isLowerBoundCTT(CegTermType c)
      63                 :            : {
      64 [ -  - ][ -  - ]:          0 :   return c == CEG_TT_LOWER || c == CEG_TT_LOWER_STRICT;
      65                 :            : }
      66                 :      40483 : bool isUpperBoundCTT(CegTermType c)
      67                 :            : {
      68 [ +  + ][ +  + ]:      40483 :   return c == CEG_TT_UPPER || c == CEG_TT_UPPER_STRICT;
      69                 :            : }
      70                 :            : 
      71                 :          0 : std::ostream& operator<<(std::ostream& os, CegInstEffort e)
      72                 :            : {
      73 [ -  - ][ -  - ]:          0 :   switch (e)
                    [ - ]
      74                 :            :   {
      75                 :          0 :     case CEG_INST_EFFORT_NONE: os << "?"; break;
      76                 :          0 :     case CEG_INST_EFFORT_STANDARD: os << "STANDARD"; break;
      77                 :          0 :     case CEG_INST_EFFORT_STANDARD_MV: os << "STANDARD_MV"; break;
      78                 :          0 :     case CEG_INST_EFFORT_FULL: os << "FULL"; break;
      79                 :          0 :     default: Unreachable();
      80                 :            :   }
      81                 :          0 :   return os;
      82                 :            : }
      83                 :            : 
      84                 :          0 : std::ostream& operator<<(std::ostream& os, CegInstPhase phase)
      85                 :            : {
      86 [ -  - ][ -  - ]:          0 :   switch (phase)
                 [ -  - ]
      87                 :            :   {
      88                 :          0 :     case CEG_INST_PHASE_NONE: os << "?"; break;
      89                 :          0 :     case CEG_INST_PHASE_EQC: os << "eqc"; break;
      90                 :          0 :     case CEG_INST_PHASE_EQUAL: os << "eq"; break;
      91                 :          0 :     case CEG_INST_PHASE_ASSERTION: os << "as"; break;
      92                 :          0 :     case CEG_INST_PHASE_MVALUE: os << "mv"; break;
      93                 :          0 :     default: Unreachable();
      94                 :            :   }
      95                 :          0 :   return os;
      96                 :            : }
      97                 :          0 : std::ostream& operator<<(std::ostream& os, CegHandledStatus status)
      98                 :            : {
      99 [ -  - ][ -  - ]:          0 :   switch (status)
                    [ - ]
     100                 :            :   {
     101                 :          0 :     case CEG_UNHANDLED: os << "unhandled"; break;
     102                 :          0 :     case CEG_PARTIALLY_HANDLED: os << "partially_handled"; break;
     103                 :          0 :     case CEG_HANDLED: os << "handled"; break;
     104                 :          0 :     case CEG_HANDLED_UNCONDITIONAL: os << "handled_unc"; break;
     105                 :          0 :     default: Unreachable();
     106                 :            :   }
     107                 :          0 :   return os;
     108                 :            : }
     109                 :            : 
     110                 :         91 : void TermProperties::composeProperty(TermProperties& p)
     111                 :            : {
     112         [ -  + ]:         91 :   if (p.d_coeff.isNull())
     113                 :            :   {
     114                 :          0 :     return;
     115                 :            :   }
     116         [ +  + ]:         91 :   if (d_coeff.isNull())
     117                 :            :   {
     118                 :         84 :     d_coeff = p.d_coeff;
     119                 :            :   }
     120                 :            :   else
     121                 :            :   {
     122                 :          7 :     d_coeff = arith::multConstants(d_coeff, p.d_coeff);
     123                 :            :   }
     124                 :            : }
     125                 :            : 
     126                 :            : // push the substitution pv_prop.getModifiedTerm(pv) -> n
     127                 :      86255 : void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop)
     128                 :            : {
     129 [ -  + ][ -  + ]:     258765 :   AssertEqual(n.getType(), pv.getType());
                 [ -  - ]
     130                 :      86255 :   d_vars.push_back(pv);
     131                 :      86255 :   d_subs.push_back(n);
     132                 :      86255 :   d_props.push_back(pv_prop);
     133         [ +  + ]:      86255 :   if (pv_prop.isBasic())
     134                 :            :   {
     135                 :      85907 :     return;
     136                 :            :   }
     137                 :        348 :   d_non_basic.push_back(pv);
     138                 :            :   // update theta value
     139                 :        348 :   Node new_theta = getTheta();
     140         [ +  + ]:        348 :   if (new_theta.isNull())
     141                 :            :   {
     142                 :        233 :     new_theta = pv_prop.d_coeff;
     143                 :            :   }
     144                 :            :   else
     145                 :            :   {
     146                 :        115 :     new_theta = arith::multConstants(new_theta, pv_prop.d_coeff);
     147                 :            :   }
     148                 :        348 :   d_theta.push_back(new_theta);
     149                 :        348 : }
     150                 :            : // pop the substitution pv_prop.getModifiedTerm(pv) -> n
     151                 :       7184 : void SolvedForm::pop_back(TermProperties& pv_prop)
     152                 :            : {
     153                 :       7184 :   d_vars.pop_back();
     154                 :       7184 :   d_subs.pop_back();
     155                 :       7184 :   d_props.pop_back();
     156         [ +  + ]:       7184 :   if (pv_prop.isBasic())
     157                 :            :   {
     158                 :       7182 :     return;
     159                 :            :   }
     160                 :          2 :   d_non_basic.pop_back();
     161                 :            :   // update theta value
     162                 :          2 :   d_theta.pop_back();
     163                 :            : }
     164                 :            : 
     165                 :            : }  // namespace quantifiers
     166                 :            : }  // namespace theory
     167                 :            : }  // namespace cvc5::internal