Skip to content

Commit

Permalink
[rules] [clausification, tautologies] Support for arguments
Browse files Browse the repository at this point in the history 
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`.
  • Loading branch information
@HanielB
HanielB committed Nov 22, 2024
1 parent ae844d1 commit d5dd816
Show file tree
Hide file tree
Showing 2 changed files with 49 additions and 54 deletions.
63 changes: 30 additions & 33 deletions carcara/src/checker/rules/clausification.rs
View file
Original file line number Diff line number Diff line change
@@ -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;
Expand Down Expand Up @@ -59,37 +60,33 @@ 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)?;

if !and_contents.contains(&conclusion[0]) {
return Err(CheckerError::TermDoesntApperInOp(
Operator::And,
conclusion[0].clone(),
));
}
Ok(())
assert_eq(
&conclusion[0],
&and_contents[args[0].as_integer().unwrap().to_usize().unwrap()],
)
}

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()?;

if !or_contents.contains(conclusion) {
return Err(CheckerError::TermDoesntApperInOp(
Operator::Or,
conclusion.clone(),
));
}
Ok(())
assert_eq(
conclusion,
&or_contents[args[0].as_integer().unwrap().to_usize().unwrap()],
)
}

pub fn or(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
Expand Down Expand Up @@ -464,13 +461,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,
Expand All @@ -481,22 +478,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,
}
}
}
Expand All @@ -512,28 +509,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,
}
}
}
Expand Down
40 changes: 19 additions & 21 deletions carcara/src/checker/rules/tautology.rs
View file
Original file line number Diff line number Diff line change
@@ -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};

Expand Down Expand Up @@ -31,17 +31,16 @@ 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(),
));
}
Ok(())

assert_eq(
&conclusion[1],
&and_contents[args[0].as_integer().unwrap().to_usize().unwrap()],
)
}

pub fn and_neg(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
Expand Down Expand Up @@ -69,18 +68,17 @@ 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()?;

if !or_contents.contains(other) {
return Err(CheckerError::TermDoesntApperInOp(
Operator::Or,
other.clone(),
));
}
Ok(())
assert_eq(
other,
&or_contents[args[0].as_integer().unwrap().to_usize().unwrap()],
)
}

pub fn xor_pos1(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
Expand Down Expand Up @@ -420,8 +418,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,
Expand Down Expand Up @@ -502,7 +500,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,
Expand Down

0 comments on commit d5dd816

Please sign in to comment.