adding missing rules, renaming

HanielB · Feb 12, 2024 · 0df2e55 · 0df2e55
1 parent be6f3eb
commit 0df2e55
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 15 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -37,7 +37,10 @@ namespace cvc5::internal {
 namespace proof {
 
 std::unordered_map<Kind, AletheRule> s_bvKindToAletheRule = {
+  {Kind::BITVECTOR_COMP, AletheRule::BV_BITBLAST_STEP_BVCOMP},
   {Kind::BITVECTOR_ULT, AletheRule::BV_BITBLAST_STEP_BVULT},
+  {Kind::BITVECTOR_ULE, AletheRule::BV_BITBLAST_STEP_BVULE},
+  {Kind::BITVECTOR_SLT, AletheRule::BV_BITBLAST_STEP_BVSLT},
   {Kind::BITVECTOR_AND, AletheRule::BV_BITBLAST_STEP_BVAND},
   {Kind::BITVECTOR_OR, AletheRule::BV_BITBLAST_STEP_BVOR},
   {Kind::BITVECTOR_XOR, AletheRule::BV_BITBLAST_STEP_BVXOR},
@@ -49,6 +52,7 @@ std::unordered_map<Kind, AletheRule> s_bvKindToAletheRule = {
   {Kind::BITVECTOR_CONCAT, AletheRule::BV_BITBLAST_STEP_CONCAT},
   {Kind::CONST_BITVECTOR, AletheRule::BV_BITBLAST_STEP_CONST},
   {Kind::BITVECTOR_EXTRACT, AletheRule::BV_BITBLAST_STEP_EXTRACT},
+  {Kind::BITVECTOR_SIGN_EXTEND, AletheRule::BV_BITBLAST_STEP_SIGN_EXTEND},
   {Kind::EQUAL, AletheRule::BV_BITBLAST_STEP_BVEQUAL},
   // TODO add support
   {Kind::BITVECTOR_UDIV, AletheRule::HOLE},

diff --git a/src/proof/alethe/alethe_proof_rule.cpp b/src/proof/alethe/alethe_proof_rule.cpp
@@ -125,23 +125,27 @@ const char* aletheRuleToString(AletheRule id)
     case AletheRule::SYMM: return "symm";
     case AletheRule::NOT_SYMM: return "not_symm";
     case AletheRule::REORDERING: return "reordering";
-    case AletheRule::BV_BITBLAST_STEP_VAR: return "bv_bitblast_step_var";
-    case AletheRule::BV_BITBLAST_STEP_BVAND: return "bv_bitblast_step_bvand";
-    case AletheRule::BV_BITBLAST_STEP_BVOR: return "bv_bitblast_step_bvor";
-    case AletheRule::BV_BITBLAST_STEP_BVXOR: return "bv_bitblast_step_bvxor";
-    case AletheRule::BV_BITBLAST_STEP_BVXNOR: return "bv_bitblast_step_bvxnor";
-    case AletheRule::BV_BITBLAST_STEP_BVNOT: return "bv_bitblast_step_bvnot";
-    case AletheRule::BV_BITBLAST_STEP_BVADD: return "bv_bitblast_step_bvadd";
-    case AletheRule::BV_BITBLAST_STEP_BVNEG: return "bv_bitblast_step_bvneg";
-    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_VAR: return "bitblast_var";
+    case AletheRule::BV_BITBLAST_STEP_BVAND: return "bitblast_bvand";
+    case AletheRule::BV_BITBLAST_STEP_BVOR: return "bitblast_bvor";
+    case AletheRule::BV_BITBLAST_STEP_BVXOR: return "bitblast_bvxor";
+    case AletheRule::BV_BITBLAST_STEP_BVXNOR: return "bitblast_bvxnor";
+    case AletheRule::BV_BITBLAST_STEP_BVNOT: return "bitblast_bvnot";
+    case AletheRule::BV_BITBLAST_STEP_BVADD: return "bitblast_bvadd";
+    case AletheRule::BV_BITBLAST_STEP_BVNEG: return "bitblast_bvneg";
+    case AletheRule::BV_BITBLAST_STEP_BVMULT: return "bitblast_bvmult";
+    case AletheRule::BV_BITBLAST_STEP_BVULE: return "bitblast_bvule";
+    case AletheRule::BV_BITBLAST_STEP_BVULT: return "bitblast_bvult";
+    case AletheRule::BV_BITBLAST_STEP_BVSLT: return "bitblast_bvslt";
+    case AletheRule::BV_BITBLAST_STEP_BVCOMP: return "bitblast_bvcomp";
     case AletheRule::BV_BITBLAST_STEP_EXTRACT:
-      return "bv_bitblast_step_extract";
+      return "bitblast_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";
+      return "bitblast_equal";
+    case AletheRule::BV_BITBLAST_STEP_CONCAT: return "bitblast_concat";
+    case AletheRule::BV_BITBLAST_STEP_CONST: return "bitblast_const";
+    case AletheRule::BV_BITBLAST_STEP_SIGN_EXTEND: return "bitblast_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
@@ -442,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,