[alethe] Update new proof rules

HanielB · Apr 20, 2024 · 5b8876c · 5b8876c
1 parent 517bdd1
commit 5b8876c
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 0 deletions.
diff --git a/src/proof/alethe/alethe_proof_rule.cpp b/src/proof/alethe/alethe_proof_rule.cpp
@@ -76,6 +76,7 @@ const char* aletheRuleToString(AletheRule id)
     case AletheRule::REFL: return "refl";
     case AletheRule::TRANS: return "trans";
     case AletheRule::CONG: return "cong";
+    case AletheRule::HO_CONG: return "ho_cong";
     case AletheRule::AND: return "and";
     case AletheRule::TAUTOLOGIC_CLAUSE: return "tautologic_clause";
     case AletheRule::NOT_OR: return "not_or";
@@ -120,6 +121,7 @@ const char* aletheRuleToString(AletheRule id)
     case AletheRule::SKO_EX: return "sko_ex";
     case AletheRule::SKO_FORALL: return "sko_forall";
     case AletheRule::ALL_SIMPLIFY: return "all_simplify";
+    case AletheRule::RARE_REWRITE: return "rare_rewrite";
     case AletheRule::SYMM: return "symm";
     case AletheRule::NOT_SYMM: return "not_symm";
     case AletheRule::REORDERING: return "reordering";
@@ -134,12 +136,16 @@ const char* aletheRuleToString(AletheRule id)
     case AletheRule::BV_BITBLAST_STEP_BVMULT: return "bv_bitblast_step_bvmult";
     case AletheRule::BV_BITBLAST_STEP_BVULE: return "bv_bitblast_step_bvule";
     case AletheRule::BV_BITBLAST_STEP_BVULT: return "bv_bitblast_step_bvult";
+    case AletheRule::BV_BITBLAST_STEP_BVSLT: return "bv_bitblast_step_bvslt";
+    case AletheRule::BV_BITBLAST_STEP_BVCOMP: return "bv_bitblast_step_bvcomp";
     case AletheRule::BV_BITBLAST_STEP_EXTRACT:
       return "bv_bitblast_step_extract";
     case AletheRule::BV_BITBLAST_STEP_BVEQUAL:
       return "bv_bitblast_step_bvequal";
     case AletheRule::BV_BITBLAST_STEP_CONCAT: return "bv_bitblast_step_concat";
     case AletheRule::BV_BITBLAST_STEP_CONST: return "bv_bitblast_step_const";
+    case AletheRule::BV_BITBLAST_STEP_SIGN_EXTEND:
+      return "bv_bitblast_step_sign_extend";
     //================================================= Hole
     case AletheRule::HOLE: return "hole";
     //================================================= Undefined rule

diff --git a/src/proof/alethe/alethe_proof_rule.h b/src/proof/alethe/alethe_proof_rule.h
@@ -245,6 +245,15 @@ enum class AletheRule : uint32_t
   // G > j. (= (f F1 ... Fn) (f G1 ... Gn))
   // where f is an n-ary function symbol.
   CONG,
+  // ======== ho_cong
+  // G > i0. (= f g)
+  // G > i1. (= F1 G1)
+  // ...
+  // G > in. (= Fn Gn)
+  // ...
+  // G > j. (= (f F1 ... Fn) (g G1 ... Gn))
+  // where f and g are n-ary function symbols.
+  HO_CONG,
   // ======== and
   // > i. (and F1 ... Fn)
   // ...
@@ -387,6 +396,7 @@ enum class AletheRule : uint32_t
   NARY_ELIM,
   QNT_SIMPLIFY,
   ALL_SIMPLIFY,
+  RARE_REWRITE,
   // ======== let
   // G,x1->F1,...,xn->Fn > j. (= G G')
   // ---------------------------------
@@ -432,10 +442,13 @@ enum class AletheRule : uint32_t
   BV_BITBLAST_STEP_BVMULT,
   BV_BITBLAST_STEP_BVULE,
   BV_BITBLAST_STEP_BVULT,
+  BV_BITBLAST_STEP_BVSLT,
+  BV_BITBLAST_STEP_BVCOMP,
   BV_BITBLAST_STEP_EXTRACT,
   BV_BITBLAST_STEP_BVEQUAL,
   BV_BITBLAST_STEP_CONCAT,
   BV_BITBLAST_STEP_CONST,
+  BV_BITBLAST_STEP_SIGN_EXTEND,
   // ======== hole
   // Used for unjustified steps
   HOLE,