Skip to content

Commit

Permalink
Restrict and, or and xor to 2 or more arguments
Browse files Browse the repository at this point in the history 
Previously, Carcara allowed these operators to be called with just one
argument, which goes against the SMT-LIB and Alethe specifications.
  • Loading branch information
@bpandreotti
bpandreotti committed Nov 8, 2023
1 parent d869277 commit c537c75
Show file tree
Hide file tree
Showing 4 changed files with 1 addition and 37 deletions.
1 change: 0 additions & 1 deletion carcara/src/checker/rules/clausification.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -844,7 +844,6 @@ mod tests {
",
"Chainable operators" {
"(step t1 (cl (= (= a b c d) (and (= a b) (= b c) (= c d)))) :rule nary_elim)": true,
"(step t1 (cl (= (= a b) (and (= a b)))) :rule nary_elim)": true,
"(step t1 (cl (= (= a b c) (and (= b c) (= a b)))) :rule nary_elim)": false,
"(step t1 (cl (= (= a b c d) (and (= a b) (= c d)))) :rule nary_elim)": false,
}
Expand Down
30 changes: 0 additions & 30 deletions carcara/src/checker/rules/simplification.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,16 +190,6 @@ fn generic_and_or_simplify(
_ => std::slice::from_ref(result_term),
};

// Sometimes, the `and_simplify` and `or_simplify` rules are used on a nested application of
// the rule operator, where the outer operation only has one argument, e.g. `(and (and p q r))`.
// If we encounter this, we remove the outer application
if phis.len() == 1 {
match phis[0].as_ref() {
Term::Op(op, args) if *op == rule_kind => phis = args.clone(),
_ => (),
}
}

// First, we remove all "skip term"s from the arguments. If at this point we already found the
// result, we return true. While doing this before the main loop requires an additional
// allocation for the `phis` vector, it allows us to exit early in some cases, which overall
Expand Down Expand Up @@ -836,8 +826,6 @@ mod tests {
",
"Transformation #1" {
"(step t1 (cl (= (and true true true) true)) :rule and_simplify)": true,
"(step t1 (cl (= (and true true true) (and true))) :rule and_simplify)": true,
"(step t1 (cl (= (and true) true)) :rule and_simplify)": true,

"(step t1 (cl (= (and true p true) true)) :rule and_simplify)": false,
"(step t1 (cl (= (and true true) false)) :rule and_simplify)": false,
Expand All @@ -846,30 +834,26 @@ mod tests {
"(step t1 (cl (= (and p true q) (and p q))) :rule and_simplify)": true,
"(step t1 (cl (= (and p true q r true true) (and p q r))) :rule and_simplify)": true,
"(step t1 (cl (= (and true q true true) q)) :rule and_simplify)": true,
"(step t1 (cl (= (and true q true true) (and q))) :rule and_simplify)": true,

"(step t1 (cl (= (and p true q true) (and p true q))) :rule and_simplify)": false,
"(step t1 (cl (= (and p true q r true true) (and p r))) :rule and_simplify)": false,
}
"Transformation #3" {
"(step t1 (cl (= (and p p q q q r) (and p q r))) :rule and_simplify)": true,
"(step t1 (cl (= (and p p) (and p))) :rule and_simplify)": true,
"(step t1 (cl (= (and p p) p)) :rule and_simplify)": true,

"(step t1 (cl (= (and p p q q q r) (and p q q r))) :rule and_simplify)": false,
"(step t1 (cl (= (and p p q q q) (and p q r))) :rule and_simplify)": false,
}
"Transformation #4" {
"(step t1 (cl (= (and p q false r) false)) :rule and_simplify)": true,
"(step t1 (cl (= (and p q false r) (and false))) :rule and_simplify)": true,
"(step t1 (cl (= (and false true) false)) :rule and_simplify)": true,

"(step t1 (cl (= (and p q false r) (and p q r))) :rule and_simplify)": false,
"(step t1 (cl (= (and p q false r) true)) :rule and_simplify)": false,
}
"Transformation #5" {
"(step t1 (cl (= (and p q (not q) r) false)) :rule and_simplify)": true,
"(step t1 (cl (= (and p q (not q) r) (and false))) :rule and_simplify)": true,
"(step t1 (cl (= (and p (not (not q)) (not q) r) false)) :rule and_simplify)": true,
"(step t1 (cl (= (and p (not (not (not p))) (not p)) false))
:rule and_simplify)": true,
Expand All @@ -885,10 +869,6 @@ mod tests {
"(step t1 (cl (= (and p false p (not p) q true q r) false))
:rule and_simplify)": true,
}
"Nested \"and\" term" {
"(step t1 (cl (= (and (and p p true q q true q r)) (and p q r)))
:rule and_simplify)": true,
}
}
}

Expand All @@ -902,8 +882,6 @@ mod tests {
",
"Transformation #1" {
"(step t1 (cl (= (or false false false) false)) :rule or_simplify)": true,
"(step t1 (cl (= (or false false false) (or false))) :rule or_simplify)": true,
"(step t1 (cl (= (or false) false)) :rule or_simplify)": true,

"(step t1 (cl (= (or false p false) false)) :rule or_simplify)": false,
"(step t1 (cl (= (or false false) true)) :rule or_simplify)": false,
Expand All @@ -912,30 +890,26 @@ mod tests {
"(step t1 (cl (= (or p false q) (or p q))) :rule or_simplify)": true,
"(step t1 (cl (= (or p false q r false false) (or p q r))) :rule or_simplify)": true,
"(step t1 (cl (= (or false q false false) q)) :rule or_simplify)": true,
"(step t1 (cl (= (or false q false false) (or q))) :rule or_simplify)": true,

"(step t1 (cl (= (or p false q false) (or p false q))) :rule or_simplify)": false,
"(step t1 (cl (= (or p false q r false false) (or p r))) :rule or_simplify)": false,
}
"Transformation #3" {
"(step t1 (cl (= (or p p q q q r) (or p q r))) :rule or_simplify)": true,
"(step t1 (cl (= (or p p) (or p))) :rule or_simplify)": true,
"(step t1 (cl (= (or p p) p)) :rule or_simplify)": true,

"(step t1 (cl (= (or p p q q q r) (or p q q r))) :rule or_simplify)": false,
"(step t1 (cl (= (or p p q q q) (or p q r))) :rule or_simplify)": false,
}
"Transformation #4" {
"(step t1 (cl (= (or p q true r) true)) :rule or_simplify)": true,
"(step t1 (cl (= (or p q true r) (or true))) :rule or_simplify)": true,
"(step t1 (cl (= (or true false) true)) :rule or_simplify)": true,

"(step t1 (cl (= (or p q true r) (or p q r))) :rule or_simplify)": false,
"(step t1 (cl (= (or p q true r) false)) :rule or_simplify)": false,
}
"Transformation #5" {
"(step t1 (cl (= (or p q (not q) r) true)) :rule or_simplify)": true,
"(step t1 (cl (= (or p q (not q) r) (or true))) :rule or_simplify)": true,
"(step t1 (cl (= (or p (not (not q)) (not q) r) true)) :rule or_simplify)": true,
"(step t1 (cl (= (or p (not (not (not p))) (not p)) true)) :rule or_simplify)": true,

Expand All @@ -948,10 +922,6 @@ mod tests {
"(step t1 (cl (= (or p p (not p) q q false q r) true)) :rule or_simplify)": true,
"(step t1 (cl (= (or p true p (not p) q false q r) true)) :rule or_simplify)": true,
}
"Nested \"or\" term" {
"(step t1 (cl (= (or (or p p false q q false q r)) (or p q r)))
:rule or_simplify)": true,
}
}
}

Expand Down
3 changes: 1 addition & 2 deletions carcara/src/parser/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -183,8 +183,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
}
}
Operator::Or | Operator::And | Operator::Xor => {
// These operators can be called with only one argument
assert_num_args(&args, 1..)?;
assert_num_args(&args, 2..)?;
for s in sorts {
SortError::assert_eq(&Sort::Bool, s.as_sort().unwrap())?;
}
Expand Down
4 changes: 0 additions & 4 deletions carcara/src/parser/tests.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,10 +162,6 @@ fn test_logic_ops() {
vec![p.bool_true(), p.bool_true(), p.bool_false()],
)),
),
(
"(and true)",
p.add(Term::Op(Operator::And, vec![p.bool_true()])),
),
("(or true (and false false))", {
let false_and_false = p.add(Term::Op(
Operator::And,
Expand Down

0 comments on commit c537c75

Please sign in to comment.