Before larger refactoring
This commit is contained in:
parent
1a497254a8
commit
d1ab7963b1
GPG Key ID:
05F3611E97A70ABF
|
|
@ -10,19 +10,21 @@ impl super::Precedence for crate::Formula
|
|||
| Self::Boolean(_)
|
||||
| Self::Compare(_)
|
||||
=> 0,
|
||||
Self::Exists(_)
|
||||
/*Self::And(formulas)
|
||||
| Self::Or(formulas) if formulas.len() == 1
|
||||
=> 0,*/
|
||||
Self::Not(_)
|
||||
| Self::Exists(_)
|
||||
| Self::ForAll(_)
|
||||
=> 1,
|
||||
Self::Not(_)
|
||||
=> 2,
|
||||
Self::And(_)
|
||||
=> 3,
|
||||
=> 2,
|
||||
Self::Or(_)
|
||||
=> 4,
|
||||
=> 3,
|
||||
Self::Implies(_)
|
||||
=> 5,
|
||||
=> 4,
|
||||
Self::IfAndOnlyIf(_)
|
||||
=> 6,
|
||||
=> 5,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -609,6 +611,13 @@ mod tests
|
|||
let term_3 = || exponentiate(constant("a"), exponentiate(constant("b"), constant("c")));
|
||||
let term_4 = || negative(function("f", vec![integer(5), add(variable("X"), integer(3))]));
|
||||
|
||||
assert_eq!(format(not(greater(term_1(), term_2()))), "not (a + b) * c > |d - e|");
|
||||
assert_eq!(format(not(less(term_1(), term_2()))), "not (a + b) * c < |d - e|");
|
||||
assert_eq!(format(not(less_or_equal(term_1(), term_2()))), "not (a + b) * c <= |d - e|");
|
||||
assert_eq!(format(not(greater_or_equal(term_1(), term_2()))), "not (a + b) * c >= |d - e|");
|
||||
assert_eq!(format(not(equal(term_1(), term_2()))), "not (a + b) * c = |d - e|");
|
||||
assert_eq!(format(not(not_equal(term_1(), term_2()))), "not (a + b) * c != |d - e|");
|
||||
|
||||
assert_eq!(format(
|
||||
exists(vec![variable_declaration("X")], greater(term_1(), term_2()))),
|
||||
"exists X (a + b) * c > |d - e|");
|
||||
|
|
@ -646,13 +655,6 @@ mod tests
|
|||
for_all(vec![variable_declaration("X")], not_equal(term_1(), term_2()))),
|
||||
"forall X (a + b) * c != |d - e|");
|
||||
|
||||
assert_eq!(format(not(greater(term_1(), term_2()))), "not (a + b) * c > |d - e|");
|
||||
assert_eq!(format(not(less(term_1(), term_2()))), "not (a + b) * c < |d - e|");
|
||||
assert_eq!(format(not(less_or_equal(term_1(), term_2()))), "not (a + b) * c <= |d - e|");
|
||||
assert_eq!(format(not(greater_or_equal(term_1(), term_2()))), "not (a + b) * c >= |d - e|");
|
||||
assert_eq!(format(not(equal(term_1(), term_2()))), "not (a + b) * c = |d - e|");
|
||||
assert_eq!(format(not(not_equal(term_1(), term_2()))), "not (a + b) * c != |d - e|");
|
||||
|
||||
assert_eq!(format(
|
||||
and(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
|
||||
greater(term_2(), term_4())])),
|
||||
|
|
@ -777,4 +779,71 @@ mod tests
|
|||
not_equal(term_2(), term_4())])),
|
||||
"(a + b) * c != |d - e| <-> a ** b ** c != -f(5, X + 3) <-> |d - e| != -f(5, X + 3)");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn format_combination_not_and_lower()
|
||||
{
|
||||
assert_eq!(format(not(not(predicate("p", vec![])))), "not not p");
|
||||
|
||||
assert_eq!(format(
|
||||
not(exists(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||
variable_declaration("Z")], predicate("p", vec![])))),
|
||||
"not exists X, Y, Z p");
|
||||
assert_eq!(format(
|
||||
exists(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||
variable_declaration("Z")], not(predicate("p", vec![])))),
|
||||
"exists X, Y, Z not p");
|
||||
assert_eq!(format(
|
||||
not(for_all(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||
variable_declaration("Z")], predicate("p", vec![])))),
|
||||
"not forall X, Y, Z p");
|
||||
assert_eq!(format(
|
||||
for_all(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||
variable_declaration("Z")], not(predicate("p", vec![])))),
|
||||
"forall X, Y, Z not p");
|
||||
|
||||
assert_eq!(format(
|
||||
not(and(vec![predicate("p", vec![])]))),
|
||||
"not p");
|
||||
assert_eq!(format(
|
||||
not(and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
|
||||
"not (p and q and r)");
|
||||
|
||||
assert_eq!(format(
|
||||
or(vec![predicate("p", vec![]), or(vec![or(vec![predicate("q", vec![]), predicate("r", vec![])])])])),
|
||||
"p or q or r");
|
||||
|
||||
assert_eq!(format(
|
||||
and(vec![predicate("p", vec![]), or(vec![or(vec![predicate("q", vec![]), predicate("r", vec![])])])])),
|
||||
"p and (q or r)");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn format_combination_quantifiers_and_lower()
|
||||
{
|
||||
assert_eq!(format(
|
||||
exists(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||
variable_declaration("Z")], exists(vec![variable_declaration("A"),
|
||||
variable_declaration("B"), variable_declaration("C")],
|
||||
predicate("p", vec![])))),
|
||||
"exists X, Y, Z exists A, B, C p");
|
||||
assert_eq!(format(
|
||||
exists(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||
variable_declaration("Z")], for_all(vec![variable_declaration("A"),
|
||||
variable_declaration("B"), variable_declaration("C")],
|
||||
predicate("p", vec![])))),
|
||||
"exists X, Y, Z forall A, B, C p");
|
||||
assert_eq!(format(
|
||||
for_all(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||
variable_declaration("Z")], exists(vec![variable_declaration("A"),
|
||||
variable_declaration("B"), variable_declaration("C")],
|
||||
predicate("p", vec![])))),
|
||||
"forall X, Y, Z exists A, B, C p");
|
||||
assert_eq!(format(
|
||||
for_all(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||
variable_declaration("Z")], for_all(vec![variable_declaration("A"),
|
||||
variable_declaration("B"), variable_declaration("C")],
|
||||
predicate("p", vec![])))),
|
||||
"forall X, Y, Z forall A, B, C p");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue