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 Alethe proof rules
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "proof/alethe/alethe_proof_rule.h"
      14                 :            : 
      15                 :            : #include <iostream>
      16                 :            : 
      17                 :            : #include "proof/proof_checker.h"
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : 
      21                 :            : namespace proof {
      22                 :            : 
      23                 :    2622552 : const char* aletheRuleToString(AletheRule id)
      24                 :            : {
      25 [ -  + ][ +  + ]:    2622552 :   switch (id)
         [ -  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ -  - ][ -  - ]
         [ +  - ][ +  + ]
         [ +  - ][ +  - ]
         [ -  + ][ +  + ]
         [ -  + ][ -  + ]
         [ +  + ][ +  + ]
         [ -  + ][ +  + ]
         [ +  + ][ -  - ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  - ][ -  - ]
         [ +  - ][ +  + ]
         [ -  - ][ -  - ]
         [ -  - ][ -  + ]
         [ +  - ][ -  - ]
         [ -  - ][ -  - ]
         [ +  - ][ -  - ]
         [ -  - ][ -  + ]
         [ +  - ][ +  + ]
         [ +  + ][ -  - ]
         [ -  + ][ -  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  - ]
         [ +  + ][ +  + ]
         [ -  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  - ][ -  + ]
            [ +  - ][ - ]
      26                 :            :   {
      27                 :          0 :     case AletheRule::ASSUME: return "assume";
      28                 :      38350 :     case AletheRule::ANCHOR_SUBPROOF: return "subproof";
      29                 :      13367 :     case AletheRule::ANCHOR_BIND: return "bind";
      30                 :        136 :     case AletheRule::ANCHOR_SKO_FORALL: return "sko_forall";
      31                 :          0 :     case AletheRule::ANCHOR_SKO_EX: return "sko_ex";
      32                 :          2 :     case AletheRule::ANCHOR_ONEPOINT: return "onepoint";
      33                 :       1384 :     case AletheRule::TRUE: return "true";
      34                 :        431 :     case AletheRule::FALSE: return "false";
      35                 :       2284 :     case AletheRule::NOT_NOT: return "not_not";
      36                 :     209643 :     case AletheRule::AND_POS: return "and_pos";
      37                 :      11166 :     case AletheRule::AND_NEG: return "and_neg";
      38                 :       3178 :     case AletheRule::OR_POS: return "or_pos";
      39                 :      66815 :     case AletheRule::OR_NEG: return "or_neg";
      40                 :       1272 :     case AletheRule::XOR_POS1: return "xor_pos1";
      41                 :        584 :     case AletheRule::XOR_POS2: return "xor_pos2";
      42                 :        750 :     case AletheRule::XOR_NEG1: return "xor_neg1";
      43                 :        885 :     case AletheRule::XOR_NEG2: return "xor_neg2";
      44                 :         59 :     case AletheRule::IMPLIES_POS: return "implies_pos";
      45                 :      38477 :     case AletheRule::IMPLIES_NEG1: return "implies_neg1";
      46                 :      38669 :     case AletheRule::IMPLIES_NEG2: return "implies_neg2";
      47                 :       1627 :     case AletheRule::EQUIV_POS1: return "equiv_pos1";
      48                 :      67129 :     case AletheRule::EQUIV_POS2: return "equiv_pos2";
      49                 :        820 :     case AletheRule::EQUIV_NEG1: return "equiv_neg1";
      50                 :        886 :     case AletheRule::EQUIV_NEG2: return "equiv_neg2";
      51                 :       1158 :     case AletheRule::ITE_POS1: return "ite_pos1";
      52                 :       1109 :     case AletheRule::ITE_POS2: return "ite_pos2";
      53                 :        465 :     case AletheRule::ITE_NEG1: return "ite_neg1";
      54                 :        369 :     case AletheRule::ITE_NEG2: return "ite_neg2";
      55                 :          0 :     case AletheRule::EQ_REFLEXIVE: return "eq_reflexive";
      56                 :          0 :     case AletheRule::EQ_TRANSITIVE: return "eq_transitive";
      57                 :          0 :     case AletheRule::EQ_CONGRUENT: return "eq_congruent";
      58                 :          0 :     case AletheRule::EQ_CONGRUENT_PRED: return "eq_congruent_pred";
      59                 :          1 :     case AletheRule::DISTINCT_ELIM: return "distinct_elim";
      60                 :          0 :     case AletheRule::LA_RW_EQ: return "la_rw_eq";
      61                 :       8287 :     case AletheRule::LA_GENERIC: return "la_generic";
      62                 :       1394 :     case AletheRule::LA_MULT_POS: return "la_mult_pos";
      63                 :      16735 :     case AletheRule::LA_MULT_NEG: return "la_mult_neg";
      64                 :          0 :     case AletheRule::LIA_GENERIC: return "lia_generic";
      65                 :       1073 :     case AletheRule::LA_DISEQUALITY: return "la_disequality";
      66                 :          0 :     case AletheRule::LA_TOTALITY: return "la_totality";
      67                 :          0 :     case AletheRule::LA_TAUTOLOGY: return "la_tautology";
      68                 :       1285 :     case AletheRule::FORALL_INST: return "forall_inst";
      69                 :          2 :     case AletheRule::QNT_JOIN: return "qnt_join";
      70                 :         10 :     case AletheRule::QNT_RM_UNUSED: return "qnt_rm_unused";
      71                 :          0 :     case AletheRule::TH_RESOLUTION: return "th_resolution";
      72                 :     324953 :     case AletheRule::RESOLUTION: return "resolution";
      73                 :          0 :     case AletheRule::RESOLUTION_OR: return "resolution";
      74                 :      75055 :     case AletheRule::REFL: return "refl";
      75                 :     250082 :     case AletheRule::TRANS: return "trans";
      76                 :     467607 :     case AletheRule::CONG: return "cong";
      77                 :        149 :     case AletheRule::HO_CONG: return "ho_cong";
      78                 :      13422 :     case AletheRule::AND: return "and";
      79                 :          0 :     case AletheRule::TAUTOLOGIC_CLAUSE: return "tautologic_clause";
      80                 :        173 :     case AletheRule::NOT_OR: return "not_or";
      81                 :     255851 :     case AletheRule::OR: return "or";
      82                 :       8235 :     case AletheRule::NOT_AND: return "not_and";
      83                 :          5 :     case AletheRule::XOR1: return "xor1";
      84                 :          3 :     case AletheRule::XOR2: return "xor2";
      85                 :          0 :     case AletheRule::NOT_XOR1: return "not_xor1";
      86                 :          0 :     case AletheRule::NOT_XOR2: return "not_xor2";
      87                 :      47207 :     case AletheRule::IMPLIES: return "implies";
      88                 :        618 :     case AletheRule::NOT_IMPLIES1: return "not_implies1";
      89                 :        452 :     case AletheRule::NOT_IMPLIES2: return "not_implies2";
      90                 :      25170 :     case AletheRule::EQUIV1: return "equiv1";
      91                 :       5178 :     case AletheRule::EQUIV2: return "equiv2";
      92                 :         39 :     case AletheRule::NOT_EQUIV1: return "not_equiv1";
      93                 :         39 :     case AletheRule::NOT_EQUIV2: return "not_equiv2";
      94                 :       1381 :     case AletheRule::ITE1: return "ite1";
      95                 :        713 :     case AletheRule::ITE2: return "ite2";
      96                 :          0 :     case AletheRule::NOT_ITE1: return "not_ite1";
      97                 :          0 :     case AletheRule::NOT_ITE2: return "not_ite2";
      98                 :          0 :     case AletheRule::ITE_INTRO: return "ite_intro";
      99                 :        173 :     case AletheRule::DIV_INTRO: return "div_intro";
     100                 :          0 :     case AletheRule::LOG2_INTRO: return "log2_intro";
     101                 :         12 :     case AletheRule::TO_INT_INTRO: return "to_int_intro";
     102                 :      81120 :     case AletheRule::CONTRACTION: return "contraction";
     103                 :          0 :     case AletheRule::CONNECTIVE_DEF: return "connective_def";
     104                 :          0 :     case AletheRule::AC_SIMP: return "ac_simp";
     105                 :          0 :     case AletheRule::ITE_SIMPLIFY: return "ite_simplify";
     106                 :          0 :     case AletheRule::EQ_SIMPLIFY: return "eq_simplify";
     107                 :          0 :     case AletheRule::AND_SIMPLIFY: return "and_simplify";
     108                 :          0 :     case AletheRule::OR_SIMPLIFY: return "or_simplify";
     109                 :          0 :     case AletheRule::NOT_SIMPLIFY: return "not_simplify";
     110                 :       9115 :     case AletheRule::IMPLIES_SIMPLIFY: return "implies_simplify";
     111                 :      17835 :     case AletheRule::EQUIV_SIMPLIFY: return "equiv_simplify";
     112                 :          0 :     case AletheRule::BOOL_SIMPLIFY: return "bool_simplify";
     113                 :          0 :     case AletheRule::QUANTIFIER_SIMPLIFY: return "qnt_simplify";
     114                 :          0 :     case AletheRule::DIV_SIMPLIFY: return "div_simplify";
     115                 :          0 :     case AletheRule::PROD_SIMPLIFY: return "prod_simplify";
     116                 :          0 :     case AletheRule::UNARY_MINUS_SIMPLIFY: return "unary_minus_simplify";
     117                 :          0 :     case AletheRule::MINUS_SIMPLIFY: return "minus_simplify";
     118                 :          0 :     case AletheRule::SUM_SIMPLIFY: return "sum_simplify";
     119                 :       1324 :     case AletheRule::COMP_SIMPLIFY: return "comp_simplify";
     120                 :          0 :     case AletheRule::NARY_ELIM: return "nary_elim";
     121                 :          0 :     case AletheRule::LET: return "let";
     122                 :          0 :     case AletheRule::QNT_SIMPLIFY: return "qnt_simplify";
     123                 :          0 :     case AletheRule::SKO_EX: return "sko_ex";
     124                 :          0 :     case AletheRule::SKO_FORALL: return "sko_forall";
     125                 :          0 :     case AletheRule::ALL_SIMPLIFY: return "all_simplify";
     126                 :          4 :     case AletheRule::ACI_SIMP: return "aci_simp";
     127                 :        428 :     case AletheRule::POLY_SIMP: return "poly_simp";
     128                 :          0 :     case AletheRule::POLY_SIMP_REL: return "poly_simp_rel";
     129                 :      12247 :     case AletheRule::EVALUATE: return "evaluate";
     130                 :       7071 :     case AletheRule::RARE_REWRITE: return "rare_rewrite";
     131                 :      79896 :     case AletheRule::SYMM: return "symm";
     132                 :        217 :     case AletheRule::NOT_SYMM: return "not_symm";
     133                 :          0 :     case AletheRule::MINISCOPE_DISTRIBUTE: return "miniscope_distribute";
     134                 :          0 :     case AletheRule::MINISCOPE_SPLIT: return "miniscope_split";
     135                 :          0 :     case AletheRule::MINISCOPE_ITE: return "miniscope_ite";
     136                 :      85088 :     case AletheRule::REORDERING: return "reordering";
     137                 :          0 :     case AletheRule::BETA_EQUIVALENCE: return "beta_equiv";
     138                 :        768 :     case AletheRule::ARRAYS_IDX: return "arrays_idx";
     139                 :        599 :     case AletheRule::ARRAYS_ROW: return "arrays_row";
     140                 :          1 :     case AletheRule::ARRAYS_ROW_CONTRA: return "arrays_row_contra";
     141                 :         31 :     case AletheRule::ARRAYS_EXT: return "arrays_ext";
     142                 :        763 :     case AletheRule::BV_BITBLAST_STEP_VAR: return "bv_bitblast_step_var";
     143                 :        104 :     case AletheRule::BV_BITBLAST_STEP_BVAND: return "bv_bitblast_step_bvand";
     144                 :         68 :     case AletheRule::BV_BITBLAST_STEP_BVOR: return "bv_bitblast_step_bvor";
     145                 :         65 :     case AletheRule::BV_BITBLAST_STEP_BVXOR: return "bv_bitblast_step_bvxor";
     146                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVXNOR: return "bv_bitblast_step_bvxnor";
     147                 :        216 :     case AletheRule::BV_BITBLAST_STEP_BVNOT: return "bv_bitblast_step_bvnot";
     148                 :        119 :     case AletheRule::BV_BITBLAST_STEP_BVADD: return "bv_bitblast_step_bvadd";
     149                 :         99 :     case AletheRule::BV_BITBLAST_STEP_BVNEG: return "bv_bitblast_step_bvneg";
     150                 :         46 :     case AletheRule::BV_BITBLAST_STEP_BVMULT: return "bv_bitblast_step_bvmult";
     151                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVULE: return "bv_bitblast_step_bvule";
     152                 :        288 :     case AletheRule::BV_BITBLAST_STEP_BVULT: return "bv_bitblast_step_bvult";
     153                 :        306 :     case AletheRule::BV_BITBLAST_STEP_BVSLT: return "bv_bitblast_step_bvslt";
     154                 :        293 :     case AletheRule::BV_BITBLAST_STEP_BVCOMP: return "bv_bitblast_step_bvcomp";
     155                 :        510 :     case AletheRule::BV_BITBLAST_STEP_EXTRACT:
     156                 :        510 :       return "bv_bitblast_step_extract";
     157                 :       1282 :     case AletheRule::BV_BITBLAST_STEP_BVEQUAL:
     158                 :       1282 :       return "bv_bitblast_step_bvequal";
     159                 :        601 :     case AletheRule::BV_BITBLAST_STEP_CONCAT: return "bv_bitblast_step_concat";
     160                 :        647 :     case AletheRule::BV_BITBLAST_STEP_CONST: return "bv_bitblast_step_const";
     161                 :        362 :     case AletheRule::BV_BITBLAST_STEP_SIGN_EXTEND:
     162                 :        362 :       return "bv_bitblast_step_sign_extend";
     163                 :            :     //================================================= Temporary
     164                 :          0 :     case AletheRule::BV_BITWISE_SLICING: return "bv_bitwise_slicing";
     165                 :          0 :     case AletheRule::BV_REPEAT_ELIM: return "bv_repeat_elim";
     166                 :            :     //================================================= Hole
     167                 :     281161 :     case AletheRule::HOLE: return "hole";
     168                 :      33559 :     case AletheRule::AND_INTRO: return "and_intro";
     169                 :            :     //================================================= Undefined rule
     170                 :          0 :     case AletheRule::UNDEFINED: return "undefined";
     171                 :          0 :     default: return "?";
     172                 :            :   }
     173                 :            : }
     174                 :            : 
     175                 :    2622552 : std::ostream& operator<<(std::ostream& out, AletheRule id)
     176                 :            : {
     177                 :    2622552 :   out << aletheRuleToString(id);
     178                 :    2622552 :   return out;
     179                 :            : }
     180                 :            : 
     181                 :    4789910 : AletheRule getAletheRule(Node n)
     182                 :            : {
     183                 :            :   uint32_t id;
     184         [ +  + ]:    4789910 :   if (ProofRuleChecker::getUInt32(n, id))
     185                 :            :   {
     186                 :    4651647 :     return static_cast<AletheRule>(id);
     187                 :            :   }
     188                 :     138263 :   return AletheRule::UNDEFINED;
     189                 :            : }
     190                 :            : 
     191                 :            : }  // namespace proof
     192                 :            : 
     193                 :            : }  // namespace cvc5::internal