Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
+69 −50
Open

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

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d5dd816
[rules] [clausification, tautologies] Support for arguments
HanielB Nov 22, 2024
a08adf9
address
HanielB Nov 27, 2024
c94775b
fix
HanielB Nov 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
63 changes: 30 additions & 33 deletions carcara/src/checker/rules/clausification.rs
View file
Open in desktop
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()],
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

By calling .as_integer().unwrap() here, we will panic if the argument is not an integer term. It would be better to return an error, with .as_integer_err()?:

Suggested change
&and_contents[args[0].as_integer().unwrap().to_usize().unwrap()],
&and_contents[args[0].as_integer_err()?.to_usize().unwrap()],

Also, since we are simply accessing and_contents with [], this code will also panic if the index is out-of-bounds. It would be better to check that the argument value is in bounds, and return a nice error otherwise.

(The same thing applies to the other rules changed)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good points, thanks! I'll fix.

)
}

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
Open in desktop
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
Loading