Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Hanna Lachnitt, Haniel Barbosa
       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                 :            :  * Implementation of Alethe proof rules
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "proof/alethe/alethe_proof_rule.h"
      17                 :            : 
      18                 :            : #include <iostream>
      19                 :            : 
      20                 :            : #include "proof/proof_checker.h"
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : 
      24                 :            : namespace proof {
      25                 :            : 
      26                 :      23424 : const char* aletheRuleToString(AletheRule id)
      27                 :            : {
      28 [ -  + ][ -  - ]:      23424 :   switch (id)
         [ -  - ][ -  - ]
         [ +  + ][ -  + ]
         [ -  - ][ -  - ]
         [ -  + ][ +  - ]
         [ +  - ][ -  - ]
         [ -  - ][ -  - ]
         [ -  - ][ -  - ]
         [ -  + ][ -  + ]
         [ -  - ][ -  - ]
         [ -  - ][ -  - ]
         [ +  - ][ +  + ]
         [ +  - ][ -  - ]
         [ -  + ][ +  - ]
         [ -  - ][ -  + ]
         [ -  - ][ +  - ]
         [ -  - ][ -  - ]
         [ -  - ][ -  + ]
         [ -  - ][ -  - ]
         [ -  - ][ +  + ]
         [ -  - ][ -  - ]
         [ -  - ][ -  - ]
         [ -  - ][ -  - ]
         [ -  - ][ +  + ]
         [ -  + ][ -  - ]
         [ -  - ][ -  - ]
         [ -  - ][ -  - ]
         [ -  - ][ -  - ]
         [ -  - ][ -  - ]
            [ +  - ][ - ]
      29                 :            :   {
      30                 :          0 :     case AletheRule::ASSUME: return "assume";
      31                 :        366 :     case AletheRule::ANCHOR_SUBPROOF: return "subproof";
      32                 :          0 :     case AletheRule::ANCHOR_BIND: return "bind";
      33                 :          0 :     case AletheRule::ANCHOR_SKO_FORALL: return "sko_forall";
      34                 :          0 :     case AletheRule::ANCHOR_SKO_EX: return "sko_ex";
      35                 :          0 :     case AletheRule::TRUE: return "true";
      36                 :          0 :     case AletheRule::FALSE: return "false";
      37                 :          0 :     case AletheRule::NOT_NOT: return "not_not";
      38                 :        549 :     case AletheRule::AND_POS: return "and_pos";
      39                 :        183 :     case AletheRule::AND_NEG: return "and_neg";
      40                 :          0 :     case AletheRule::OR_POS: return "or_pos";
      41                 :        549 :     case AletheRule::OR_NEG: return "or_neg";
      42                 :          0 :     case AletheRule::XOR_POS1: return "xor_pos1";
      43                 :          0 :     case AletheRule::XOR_POS2: return "xor_pos2";
      44                 :          0 :     case AletheRule::XOR_NEG1: return "xor_neg1";
      45                 :          0 :     case AletheRule::XOR_NEG2: return "xor_neg2";
      46                 :          0 :     case AletheRule::IMPLIES_POS: return "implies_pos";
      47                 :        366 :     case AletheRule::IMPLIES_NEG1: return "implies_neg1";
      48                 :        366 :     case AletheRule::IMPLIES_NEG2: return "implies_neg2";
      49                 :          0 :     case AletheRule::EQUIV_POS1: return "equiv_pos1";
      50                 :       2379 :     case AletheRule::EQUIV_POS2: return "equiv_pos2";
      51                 :          0 :     case AletheRule::EQUIV_NEG1: return "equiv_neg1";
      52                 :          0 :     case AletheRule::EQUIV_NEG2: return "equiv_neg2";
      53                 :          0 :     case AletheRule::ITE_POS1: return "ite_pos1";
      54                 :          0 :     case AletheRule::ITE_POS2: return "ite_pos2";
      55                 :          0 :     case AletheRule::ITE_NEG1: return "ite_neg1";
      56                 :          0 :     case AletheRule::ITE_NEG2: return "ite_neg2";
      57                 :          0 :     case AletheRule::EQ_REFLEXIVE: return "eq_reflexive";
      58                 :          0 :     case AletheRule::EQ_TRANSITIVE: return "eq_transitive";
      59                 :          0 :     case AletheRule::EQ_CONGRUENT: return "eq_congruent";
      60                 :          0 :     case AletheRule::EQ_CONGRUENT_PRED: return "eq_congruent_pred";
      61                 :          0 :     case AletheRule::DISTINCT_ELIM: return "distinct_elim";
      62                 :          0 :     case AletheRule::LA_RW_EQ: return "la_rw_eq";
      63                 :        183 :     case AletheRule::LA_GENERIC: return "la_generic";
      64                 :          0 :     case AletheRule::LA_MULT_POS: return "la_mult_pos";
      65                 :        183 :     case AletheRule::LA_MULT_NEG: return "la_mult_neg";
      66                 :          0 :     case AletheRule::LIA_GENERIC: return "lia_generic";
      67                 :          0 :     case AletheRule::LA_DISEQUALITY: return "la_disequality";
      68                 :          0 :     case AletheRule::LA_TOTALITY: return "la_totality";
      69                 :          0 :     case AletheRule::LA_TAUTOLOGY: return "la_tautology";
      70                 :          0 :     case AletheRule::FORALL_INST: return "forall_inst";
      71                 :          0 :     case AletheRule::QNT_JOIN: return "qnt_join";
      72                 :          0 :     case AletheRule::QNT_RM_UNUSED: return "qnt_rm_unused";
      73                 :          0 :     case AletheRule::TH_RESOLUTION: return "th_resolution";
      74                 :       5124 :     case AletheRule::RESOLUTION: return "resolution";
      75                 :          0 :     case AletheRule::RESOLUTION_OR: return "resolution";
      76                 :        732 :     case AletheRule::REFL: return "refl";
      77                 :       2379 :     case AletheRule::TRANS: return "trans";
      78                 :       2013 :     case AletheRule::CONG: return "cong";
      79                 :          0 :     case AletheRule::HO_CONG: return "ho_cong";
      80                 :          0 :     case AletheRule::AND: return "and";
      81                 :          0 :     case AletheRule::TAUTOLOGIC_CLAUSE: return "tautologic_clause";
      82                 :          0 :     case AletheRule::NOT_OR: return "not_or";
      83                 :        183 :     case AletheRule::OR: return "or";
      84                 :        183 :     case AletheRule::NOT_AND: return "not_and";
      85                 :          0 :     case AletheRule::XOR1: return "xor1";
      86                 :          0 :     case AletheRule::XOR2: return "xor2";
      87                 :          0 :     case AletheRule::NOT_XOR1: return "not_xor1";
      88                 :          0 :     case AletheRule::NOT_XOR2: return "not_xor2";
      89                 :        183 :     case AletheRule::IMPLIES: return "implies";
      90                 :          0 :     case AletheRule::NOT_IMPLIES1: return "not_implies1";
      91                 :          0 :     case AletheRule::NOT_IMPLIES2: return "not_implies2";
      92                 :        549 :     case AletheRule::EQUIV1: return "equiv1";
      93                 :          0 :     case AletheRule::EQUIV2: return "equiv2";
      94                 :          0 :     case AletheRule::NOT_EQUIV1: return "not_equiv1";
      95                 :          0 :     case AletheRule::NOT_EQUIV2: return "not_equiv2";
      96                 :          0 :     case AletheRule::ITE1: return "ite1";
      97                 :          0 :     case AletheRule::ITE2: return "ite2";
      98                 :          0 :     case AletheRule::NOT_ITE1: return "not_ite1";
      99                 :          0 :     case AletheRule::NOT_ITE2: return "not_ite2";
     100                 :          0 :     case AletheRule::ITE_INTRO: return "ite_intro";
     101                 :        732 :     case AletheRule::CONTRACTION: return "contraction";
     102                 :          0 :     case AletheRule::CONNECTIVE_DEF: return "connective_def";
     103                 :          0 :     case AletheRule::ITE_SIMPLIFY: return "ite_simplify";
     104                 :          0 :     case AletheRule::EQ_SIMPLIFY: return "eq_simplify";
     105                 :          0 :     case AletheRule::AND_SIMPLIFY: return "and_simplify";
     106                 :          0 :     case AletheRule::OR_SIMPLIFY: return "or_simplify";
     107                 :          0 :     case AletheRule::NOT_SIMPLIFY: return "not_simplify";
     108                 :        366 :     case AletheRule::IMPLIES_SIMPLIFY: return "implies_simplify";
     109                 :        183 :     case AletheRule::EQUIV_SIMPLIFY: return "equiv_simplify";
     110                 :          0 :     case AletheRule::BOOL_SIMPLIFY: return "bool_simplify";
     111                 :          0 :     case AletheRule::QUANTIFIER_SIMPLIFY: return "qnt_simplify";
     112                 :          0 :     case AletheRule::DIV_SIMPLIFY: return "div_simplify";
     113                 :          0 :     case AletheRule::PROD_SIMPLIFY: return "prod_simplify";
     114                 :          0 :     case AletheRule::UNARY_MINUS_SIMPLIFY: return "unary_minus_simplify";
     115                 :          0 :     case AletheRule::MINUS_SIMPLIFY: return "minus_simplify";
     116                 :          0 :     case AletheRule::SUM_SIMPLIFY: return "sum_simplify";
     117                 :          0 :     case AletheRule::COMP_SIMPLIFY: return "comp_simplify";
     118                 :          0 :     case AletheRule::NARY_ELIM: return "nary_elim";
     119                 :          0 :     case AletheRule::LET: return "let";
     120                 :          0 :     case AletheRule::QNT_SIMPLIFY: return "qnt_simplify";
     121                 :          0 :     case AletheRule::SKO_EX: return "sko_ex";
     122                 :          0 :     case AletheRule::SKO_FORALL: return "sko_forall";
     123                 :          0 :     case AletheRule::ALL_SIMPLIFY: return "all_simplify";
     124                 :        183 :     case AletheRule::RARE_REWRITE: return "rare_rewrite";
     125                 :        549 :     case AletheRule::SYMM: return "symm";
     126                 :          0 :     case AletheRule::NOT_SYMM: return "not_symm";
     127                 :        183 :     case AletheRule::REORDERING: return "reordering";
     128                 :          0 :     case AletheRule::BV_BITBLAST_STEP_VAR: return "bv_bitblast_step_var";
     129                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVAND: return "bv_bitblast_step_bvand";
     130                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVOR: return "bv_bitblast_step_bvor";
     131                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVXOR: return "bv_bitblast_step_bvxor";
     132                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVXNOR: return "bv_bitblast_step_bvxnor";
     133                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVNOT: return "bv_bitblast_step_bvnot";
     134                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVADD: return "bv_bitblast_step_bvadd";
     135                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVNEG: return "bv_bitblast_step_bvneg";
     136                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVMULT: return "bv_bitblast_step_bvmult";
     137                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVULE: return "bv_bitblast_step_bvule";
     138                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVULT: return "bv_bitblast_step_bvult";
     139                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVSLT: return "bv_bitblast_step_bvslt";
     140                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVCOMP: return "bv_bitblast_step_bvcomp";
     141                 :          0 :     case AletheRule::BV_BITBLAST_STEP_EXTRACT:
     142                 :          0 :       return "bv_bitblast_step_extract";
     143                 :          0 :     case AletheRule::BV_BITBLAST_STEP_BVEQUAL:
     144                 :          0 :       return "bv_bitblast_step_bvequal";
     145                 :          0 :     case AletheRule::BV_BITBLAST_STEP_CONCAT: return "bv_bitblast_step_concat";
     146                 :          0 :     case AletheRule::BV_BITBLAST_STEP_CONST: return "bv_bitblast_step_const";
     147                 :          0 :     case AletheRule::BV_BITBLAST_STEP_SIGN_EXTEND:
     148                 :          0 :       return "bv_bitblast_step_sign_extend";
     149                 :            :     //================================================= Hole
     150                 :       4758 :     case AletheRule::HOLE: return "hole";
     151                 :            :     //================================================= Undefined rule
     152                 :          0 :     case AletheRule::UNDEFINED: return "undefined";
     153                 :          0 :     default: return "?";
     154                 :            :   }
     155                 :            : }
     156                 :            : 
     157                 :      23424 : std::ostream& operator<<(std::ostream& out, AletheRule id)
     158                 :            : {
     159                 :      23424 :   out << aletheRuleToString(id);
     160                 :      23424 :   return out;
     161                 :            : }
     162                 :            : 
     163                 :      50142 : AletheRule getAletheRule(Node n)
     164                 :            : {
     165                 :            :   uint32_t id;
     166         [ +  + ]:      50142 :   if (ProofRuleChecker::getUInt32(n, id))
     167                 :            :   {
     168                 :      49227 :     return static_cast<AletheRule>(id);
     169                 :            :   }
     170                 :        915 :   return AletheRule::UNDEFINED;
     171                 :            : }
     172                 :            : 
     173                 :            : }  // namespace proof
     174                 :            : 
     175                 :            : }  // namespace cvc5::internal