Rename or_intro rule to weakening

This is because it doesn't actually use the `or` operator. Instead it operates directly on the clause. See the conversation here: https://gitlab.uliege.be/verit/alethe/-/issues/45
ufmg-smite · Aug 8, 2024 · 45d9fd5 · 45d9fd5
1 parent 6a670a8
commit 45d9fd5
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 11 deletions.
diff --git a/carcara/src/checker/mod.rs b/carcara/src/checker/mod.rs
@@ -538,7 +538,7 @@ impl<'c> ProofChecker<'c> {
             "symm" => extras::symm,
             "not_symm" => extras::not_symm,
             "eq_symmetric" => extras::eq_symmetric,
-            "or_intro" => extras::or_intro,
+            "weakening" => extras::weakening,
             "bind_let" => extras::bind_let,
             "la_mult_pos" => extras::la_mult_pos,
             "la_mult_neg" => extras::la_mult_neg,

diff --git a/carcara/src/checker/parallel/scheduler.rs b/carcara/src/checker/parallel/scheduler.rs
@@ -400,7 +400,7 @@ pub fn get_step_weight(step: &ProofCommand) -> u64 {
                 "symm" => 682,
                 "not_symm" => 0, //-1
                 "eq_symmetric" => 673,
-                "or_intro" => 508,
+                "weakening" => 508,
                 "bind_let" => 2324,
                 "la_mult_pos" => 1446,
                 "la_mult_neg" => 1447,

diff --git a/carcara/src/checker/rules/extras.rs b/carcara/src/checker/rules/extras.rs
@@ -54,7 +54,7 @@ pub fn eq_symmetric(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
     assert_eq(u_1, u_2)
 }
 
-pub fn or_intro(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
+pub fn weakening(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
     assert_num_premises(premises, 1)?;
     let premise = premises[0].clause;
     assert_clause_len(conclusion, premise.len()..)?;
@@ -289,7 +289,7 @@ mod tests {
     }
 
     #[test]
-    fn or_intro() {
+    fn weakening() {
         test_cases! {
             definitions = "
                 (declare-fun a () Bool)
@@ -298,17 +298,17 @@ mod tests {
             ",
             "Simple working examples" {
                 "(step t1 (cl a b) :rule hole)
-                (step t2 (cl a b c) :rule or_intro :premises (t1))": true,
+                (step t2 (cl a b c) :rule weakening :premises (t1))": true,
 
                 "(step t1 (cl) :rule hole)
-                (step t2 (cl a b) :rule or_intro :premises (t1))": true,
+                (step t2 (cl a b) :rule weakening :premises (t1))": true,
             }
             "Failing examples" {
                 "(step t1 (cl a b) :rule hole)
-                (step t2 (cl a c b) :rule or_intro :premises (t1))": false,
+                (step t2 (cl a c b) :rule weakening :premises (t1))": false,
 
                 "(step t1 (cl a b c) :rule hole)
-                (step t2 (cl a b) :rule or_intro :premises (t1))": false,
+                (step t2 (cl a b) :rule weakening :premises (t1))": false,
             }
         }
     }

diff --git a/carcara/src/checker/rules/transitivity.rs b/carcara/src/checker/rules/transitivity.rs
@@ -181,15 +181,15 @@ pub fn elaborate_eq_transitive(
     if !not_needed.is_empty() {
         let mut clause = latest_clause;
         clause.extend(not_needed);
-        let or_intro_step = ProofStep {
+        let weakening_step = ProofStep {
             id: elaborator.get_new_id(&command_id),
             clause,
-            rule: "or_intro".to_owned(),
+            rule: "weakening".to_owned(),
             premises: vec![latest_step_index],
             args: Vec::new(),
             discharge: Vec::new(),
         };
-        latest_step_index = elaborator.add_new_step(or_intro_step);
+        latest_step_index = elaborator.add_new_step(weakening_step);
     }
 
     elaborator.push_elaborated_step(ProofStep {