Implement bv_poly_simp_eq

Author: bpandreotti

carcara/src/checker/rules/polynomial.rs

@@ -1,8 +1,10 @@
 use super::{assert_clause_len, assert_eq, RuleArgs, RuleResult};
 use crate::{
     ast::{Operator, Rc, Sort, Term},
-    checker::error::PolynomialError,
-    checker::rules::{assert_num_premises, get_premise_term},
+    checker::{
+        error::PolynomialError,
+        rules::{assert_is_expected, assert_num_premises, get_premise_term},
+    },
 };
 use indexmap::{map::Entry, IndexMap};
 use rug::{ops::NegAssign, Integer, Rational};
@@ -231,3 +233,27 @@ pub fn poly_simp_rel(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleRes
         ((op1, _), (op2, _)) => Err(PolynomialError::InvalidOperators(op1, op2).into()),
     }
 }
+
+pub fn bv_poly_simp_eq(RuleArgs { conclusion, premises, pool, .. }: RuleArgs) -> RuleResult {
+    assert_num_premises(premises, 1)?;
+    assert_clause_len(conclusion, 1)?;
+
+    let ((c1, (x1, x2)), (c2, (y1, y2))) =
+        match_term_err!((= (* c1 (- x1 x2)) (* c2 (- y1 y2))) = get_premise_term(&premises[0])?)?;
+
+    let sort = pool.sort(c1);
+    let Sort::BitVec(width) = sort.as_sort().unwrap() else {
+        unreachable!() // The parser ensures that the sort is a bitvector sort
+    };
+    let one = pool.add(Term::new_bv(Integer::from(1), *width));
+    assert_is_expected(c1, one.clone())?;
+    assert_is_expected(c2, one)?;
+
+    let ((l1, l2), (r1, r2)) = match_term_err!((= (= x1 x2) (= y1 y2)) = &conclusion[0])?;
+
+    assert_eq(l1, x1)?;
+    assert_eq(l2, x2)?;
+    assert_eq(r1, y1)?;
+    assert_eq(r2, y2)?;
+    Ok(())
+}

carcara/src/checker/shared.rs

@@ -205,6 +205,7 @@ pub fn get_rule_shared(rule_name: &str, elaborated: bool) -> Option<crate::check
         "poly_simp" => polynomial::poly_simp,
         "bv_poly_simp" => polynomial::bv_poly_simp,
         "poly_simp_rel" => polynomial::poly_simp_rel,
+        "bv_poly_simp_eq" => polynomial::bv_poly_simp_eq,
         "forall_inst" => quantifier::forall_inst,
         "qnt_join" => quantifier::qnt_join,
         "qnt_rm_unused" => quantifier::qnt_rm_unused,