[rules] [clausification, tautologies] Support for arguments (#48)

* [rules] [clausification, tautologies] Support for arguments

The semantics of the rules `and`, `not_or`, `and_pos`, and `or_neg` changed so
that now they expect an argument as to the position in which the concluding
element is from an n-ary application of the operators `and` or `or`.

* address

* fix

carcara/src/ast/term.rs

@@ -808,6 +808,16 @@ impl Rc<Term> {
             .ok_or_else(|| CheckerError::ExpectedAnyInteger(self.clone()))
     }
 
+    /// Similar to `Term::as_integer_err`, but also checks if non-negative.
+    pub fn as_usize_err(&self) -> Result<usize, CheckerError> {
+        if let Some(i) = self.as_integer() {
+            if i >= 0 {
+                return Ok(i.to_usize().unwrap());
+            }
+        }
+        Err(CheckerError::ExpectedNonnegInteger(self.clone()))
+    }
+
     /// Similar to `Term::as_signed_number`, but returns a `CheckerError` on failure.
     pub fn as_signed_number_err(&self) -> Result<Rational, CheckerError> {
         self.as_signed_number()

carcara/src/checker/error.rs

@@ -71,6 +71,9 @@ pub enum CheckerError {
     #[error("cannot evaluate the fixed length of the term '{0}'")]
     LengthCannotBeEvaluated(Rc<Term>),
 
+    #[error("No {0}-th child in term {1}")]
+    NoIthChildInTerm(usize, Rc<Term>),
+
     // General errors
     #[error("expected {0} premises, got {1}")]
     WrongNumberOfPremises(Range, usize),
@@ -117,6 +120,9 @@ pub enum CheckerError {
     #[error("expected term '{0}' to be an integer constant")]
     ExpectedAnyInteger(Rc<Term>),
 
+    #[error("expected term '{0}' to be an non-negative integer constant")]
+    ExpectedNonnegInteger(Rc<Term>),
+
     #[error("expected operation term, got '{0}'")]
     ExpectedOperationTerm(Rc<Term>),
 

carcara/src/checker/rules/clausification.rs

@@ -1,6 +1,7 @@
 use super::{
-    assert_clause_len, assert_eq, assert_is_expected, assert_num_premises, assert_operation_len,
-    assert_polyeq_expected, get_premise_term, CheckerError, EqualityError, RuleArgs, RuleResult,
+    assert_clause_len, assert_eq, assert_is_expected, assert_num_args, assert_num_premises,
+    assert_operation_len, assert_polyeq_expected, get_premise_term, CheckerError, EqualityError,
+    RuleArgs, RuleResult,
 };
 use crate::ast::*;
 use indexmap::IndexMap;
@@ -59,37 +60,37 @@ pub fn distinct_elim(RuleArgs { conclusion, pool, .. }: RuleArgs) -> RuleResult
     }
 }
 
-pub fn and(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
+pub fn and(RuleArgs { conclusion, premises, args, .. }: RuleArgs) -> RuleResult {
     assert_num_premises(premises, 1)?;
+    assert_num_args(args, 1)?;
     assert_clause_len(conclusion, 1)?;
 
     let and_term = get_premise_term(&premises[0])?;
     let and_contents = match_term_err!((and ...) = and_term)?;
+    let i = args[0].as_usize_err()?;
 
-    if !and_contents.contains(&conclusion[0]) {
-        return Err(CheckerError::TermDoesntApperInOp(
-            Operator::And,
-            conclusion[0].clone(),
-        ));
+    if i >= and_contents.len() {
+        return Err(CheckerError::NoIthChildInTerm(i, and_term.clone()));
     }
-    Ok(())
+
+    assert_eq(&conclusion[0], &and_contents[i])
 }
 
-pub fn not_or(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
+pub fn not_or(RuleArgs { conclusion, premises, args, .. }: RuleArgs) -> RuleResult {
     assert_num_premises(premises, 1)?;
+    assert_num_args(args, 1)?;
     assert_clause_len(conclusion, 1)?;
 
     let or_term = get_premise_term(&premises[0])?;
     let or_contents = match_term_err!((not (or ...)) = or_term)?;
     let conclusion = conclusion[0].remove_negation_err()?;
+    let i = args[0].as_usize_err()?;
 
-    if !or_contents.contains(conclusion) {
-        return Err(CheckerError::TermDoesntApperInOp(
-            Operator::Or,
-            conclusion.clone(),
-        ));
+    if i >= or_contents.len() {
+        return Err(CheckerError::NoIthChildInTerm(i, or_term.clone()));
     }
-    Ok(())
+
+    assert_eq(conclusion, &or_contents[i])
 }
 
 pub fn or(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
@@ -464,13 +465,13 @@ mod tests {
             ",
             "Simple working examples" {
                 "(assume h1 (and p q))
-                (step t2 (cl q) :rule and :premises (h1))": true,
+                (step t2 (cl q) :rule and :premises (h1) :args (1))": true,
 
                 "(assume h1 (and p q r s))
-                (step t2 (cl p) :rule and :premises (h1))": true,
+                (step t2 (cl p) :rule and :premises (h1) :args (0))": true,
 
                 "(assume h1 (and p q r s))
-                (step t2 (cl s) :rule and :premises (h1))": true,
+                (step t2 (cl s) :rule and :premises (h1) :args (3))": true,
             }
             "Number of premises != 1" {
                 "(step t1 (cl p) :rule and)": false,
@@ -481,22 +482,22 @@ mod tests {
             }
             "Premise clause has more than one term" {
                 "(step t1 (cl (and p q) (and r s)) :rule hole)
-                (step t2 (cl p) :rule and :premises (t1))": false,
+                (step t2 (cl p) :rule and :premises (t1) :args (0))": false,
             }
             "Conclusion clause does not have exactly one term" {
                 "(assume h1 (and p q r s))
-                (step t2 (cl q s) :rule and :premises (h1))": false,
+                (step t2 (cl q s) :rule and :premises (h1) :args (1))": false,
 
                 "(assume h1 (and p q))
-                (step t2 (cl) :rule and :premises (h1))": false,
+                (step t2 (cl) :rule and :premises (h1) :args (0))": false,
             }
             "Premise is not an \"and\" operation" {
                 "(assume h1 (or p q r s))
-                (step t2 (cl r) :rule and :premises (h1))": false,
+                (step t2 (cl r) :rule and :premises (h1) :args (0))": false,
             }
             "Conclusion term is not in premise" {
                 "(assume h1 (and p q r))
-                (step t2 (cl s) :rule and :premises (h1))": false,
+                (step t2 (cl s) :rule and :premises (h1) :args (0))": false,
             }
         }
     }
@@ -512,28 +513,28 @@ mod tests {
             ",
             "Simple working examples" {
                 "(assume h1 (not (or p q)))
-                (step t2 (cl (not q)) :rule not_or :premises (h1))": true,
+                (step t2 (cl (not q)) :rule not_or :premises (h1) :args (1))": true,
 
                 "(assume h1 (not (or p q r s)))
-                (step t2 (cl (not p)) :rule not_or :premises (h1))": true,
+                (step t2 (cl (not p)) :rule not_or :premises (h1) :args (0))": true,
             }
             "Conclusion clause is of the wrong form" {
                 "(assume h1 (not (or p q r s)))
-                (step t2 (cl (not q) (not s)) :rule not_or :premises (h1))": false,
+                (step t2 (cl (not q) (not s)) :rule not_or :premises (h1) :args (1))": false,
 
                 "(assume h1 (not (or p q)))
-                (step t2 (cl q) :rule not_or :premises (h1))": false,
+                (step t2 (cl q) :rule not_or :premises (h1) :args (1))": false,
             }
             "Premise is of the wrong form" {
                 "(assume h1 (not (and p q r s)))
-                (step t2 (cl (not r)) :rule not_or :premises (h1))": false,
+                (step t2 (cl (not r)) :rule not_or :premises (h1) :args (2))": false,
 
                 "(assume h1 (or p q r s))
-                (step t2 (cl (not r)) :rule not_or :premises (h1))": false,
+                (step t2 (cl (not r)) :rule not_or :premises (h1) :args (2))": false,
             }
             "Conclusion term is not in premise" {
                 "(assume h1 (not (or p q r)))
-                (step t2 (cl (not s)) :rule not_or :premises (h1))": false,
+                (step t2 (cl (not s)) :rule not_or :premises (h1) :args (0))": false,
             }
         }
     }

carcara/src/checker/rules/tautology.rs

@@ -1,6 +1,6 @@
 use super::{
-    assert_clause_len, assert_eq, assert_num_premises, assert_polyeq, get_premise_term,
-    CheckerError, RuleArgs, RuleResult,
+    assert_clause_len, assert_eq, assert_num_args, assert_num_premises, assert_polyeq,
+    get_premise_term, CheckerError, RuleArgs, RuleResult,
 };
 use crate::{ast::*, checker::rules::assert_operation_len};
 
@@ -31,17 +31,18 @@ pub fn not_not(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
     assert_eq(p, &conclusion[1])
 }
 
-pub fn and_pos(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
+pub fn and_pos(RuleArgs { conclusion, args, .. }: RuleArgs) -> RuleResult {
     assert_clause_len(conclusion, 2)?;
+    assert_num_args(args, 1)?;
 
     let and_contents = match_term_err!((not (and ...)) = &conclusion[0])?;
-    if !and_contents.contains(&conclusion[1]) {
-        return Err(CheckerError::TermDoesntApperInOp(
-            Operator::And,
-            conclusion[1].clone(),
-        ));
+    let i = args[0].as_usize_err()?;
+
+    if i >= and_contents.len() {
+        return Err(CheckerError::NoIthChildInTerm(i, conclusion[0].clone()));
     }
-    Ok(())
+
+    assert_eq(&conclusion[1], &and_contents[i])
 }
 
 pub fn and_neg(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
@@ -69,18 +70,19 @@ pub fn or_pos(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
     Ok(())
 }
 
-pub fn or_neg(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
+pub fn or_neg(RuleArgs { conclusion, args, .. }: RuleArgs) -> RuleResult {
     assert_clause_len(conclusion, 2)?;
+    assert_num_args(args, 1)?;
+
     let or_contents = match_term_err!((or ...) = &conclusion[0])?;
     let other = conclusion[1].remove_negation_err()?;
+    let i = args[0].as_usize_err()?;
 
-    if !or_contents.contains(other) {
-        return Err(CheckerError::TermDoesntApperInOp(
-            Operator::Or,
-            other.clone(),
-        ));
+    if i >= or_contents.len() {
+        return Err(CheckerError::NoIthChildInTerm(i, conclusion[0].clone()));
     }
-    Ok(())
+
+    assert_eq(other, &or_contents[i])
 }
 
 pub fn xor_pos1(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
@@ -420,8 +422,8 @@ mod tests {
                 (declare-fun s () Bool)
             ",
             "Simple working examples" {
-                "(step t1 (cl (not (and p q r)) r) :rule and_pos)": true,
-                "(step t1 (cl (not (and (or (not r) p) q)) (or (not r) p)) :rule and_pos)": true,
+                "(step t1 (cl (not (and p q r)) r) :rule and_pos :args (2))": true,
+                "(step t1 (cl (not (and (or (not r) p) q)) (or (not r) p)) :rule and_pos :args (0))": true,
             }
             "First term in clause is not of the correct form" {
                 "(step t1 (cl (and p q r) r) :rule and_pos)": false,
@@ -502,7 +504,7 @@ mod tests {
                 (declare-fun s () Bool)
             ",
             "Simple working examples" {
-                "(step t1 (cl (or p q r) (not r)) :rule or_neg)": true,
+                "(step t1 (cl (or p q r) (not r)) :rule or_neg :args (2))": true,
             }
             "First term in clause is not of the correct form" {
                 "(step t1 (cl (and p q r) (not r)) :rule or_neg)": false,