Version bump for release v0.4.0-beta.3

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "anthem"
-version = "0.4.0-beta.2"
+version = "0.4.0-beta.3"
 authors = ["Patrick Lühne <patrick@luehne.de>"]
 edition = "2018"
 

examples/example-2.lemmas

@@ -1,10 +1,6 @@
-# Multiplication with positive numbers preserves the order of integers
-axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
-
 # Induction principle instantiated for p.
 # This axiom is necessary because we use Vampire without higher-order reasoning
-axiom: forall N1 (p(N1) and forall N2 (N2 >= N1 and not p(N2) -> not p(N2 + 1)) -> forall N2 (N2 >= N1 -> p(N2))).
-#axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)) -> forall N p(N).
+axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)) -> forall N (N >= 0 -> p(N)).
 
 lemma(forward): forall X (p(X) <-> exists N (X = N and N >= 0 and N * N <= n)).
 lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n)).
@@ -14,7 +10,9 @@ lemma(forward): not p(n + 1).
 lemma(forward): forall N1, N2 (q(N1) and N2 > N1 -> not q(N2)).
 lemma(forward): forall N (N >= 0 and not p(N + 1) -> (N + 1) * (N + 1) > n).
 
-lemma(backward): forall N1, N2 (q(N1) and q(N2) -> N1 = N2).
-axiom: forall N1, N2 (p(N1) and not p(N1 + 1) and p(N2) and not p(N2 + 1) -> N1 = N2).
-
-lemma(backward): forall X1 (q(X1) -> p(X1) and exists X2 (exists N (X2 = N + 1 and N = X1) and not p(X2))).
+lemma(backward): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 * N1 <= N2 * N2 -> N1 <= N2).
+lemma(backward): forall N (p(N) <-> 0 <= N and N <= n and N * N <= n).
+lemma(backward): forall N (not p(N) and N >= 0 -> N * N > n).
+lemma(backward): forall N (N >= 0 -> N * N < (N + 1) * (N + 1)).
+lemma(backward): forall N1, N2 (p(N1) and not p(N2) and N2 >= 0 -> N1 < N2).
+lemma(backward): forall N1, N2 (p(N1) and not p(N1 + 1) and p(N2) and not p(N2 + 1) -> N1 = N2).

examples/example-exact-cover.lp

@@ -1,5 +1,5 @@
-{in(1..n)}.
+{in_cover(1..n)}.
 
-:- I != J, in(I), in(J), s(X, I), s(X, J).
-covered(X) :- in(I), s(X, I).
+:- I != J, in_cover(I), in_cover(J), s(X, I), s(X, J).
+covered(X) :- in_cover(I), s(X, I).
 :- s(X, I), not covered(X).

examples/example-exact-cover.spec

@@ -8,15 +8,15 @@ input: s/2.
 
 # Only the in/1 predicate is an actual output, s/2 is an input and covered/1 and is_int/1 are
 # auxiliary
-output: in/1.
+output: in_cover/1.
 
 # Perform the proofs under the assumption that the second parameter of s/2 (the number of the set)
 # is always an integer
-assume: forall Y (exists X s(X, Y) -> exists N (Y = N and N >= 1 and N <= n)).
+assume: forall Y (exists X s(X, Y) -> exists I (Y = I and I >= 1 and I <= n)).
 
 # Only valid sets can be included in the solution
-spec: forall Y (in(Y) -> exists N (Y = N and N >= 1 and N <= n)).
+spec: forall Y (in_cover(Y) -> exists I (Y = I and I >= 1 and I <= n)).
 # If an element is contained in an input set, it must be covered by all solutions
-spec: forall X (exists Y s(X, Y) -> exists Y (in(Y) and s(X, Y))).
+spec: forall X (exists Y s(X, Y) -> exists Y (s(X, Y) and in_cover(Y))).
 # Elements may not be covered by two input sets
-spec: forall Y, Z (exists X (s(X, Y) and s(X, Z)) and in(Y) and in(Z) -> Y = Z).
+spec: forall Y, Z (exists X (s(X, Y) and s(X, Z)) and in_cover(Y) and in_cover(Z) -> Y = Z).

src/ast.rs

@@ -422,7 +422,10 @@ impl VariableDeclaration
 						| Some('L')
 						| Some('M')
 						| Some('N') => return Ok(crate::Domain::Integer),
-						Some('X')
+						Some('U')
+						| Some('V')
+						| Some('W')
+						| Some('X')
 						| Some('Y')
 						| Some('Z') => return Ok(crate::Domain::Program),
 						Some('_') => continue,

src/problem.rs

@@ -326,7 +326,7 @@ impl Problem
 		{
 			let step_title = match statement.proof_status
 			{
-				ProofStatus::AssumedProven => format!("Added"),
+				ProofStatus::AssumedProven => format!("Presupposed"),
 				ProofStatus::Proven => format!("Verified"),
 				ProofStatus::NotProven
 				| ProofStatus::Disproven

src/simplify.rs

@@ -196,6 +196,90 @@ fn simplify_quantified_formulas_without_parameters(formula: &mut crate::Formula)
 	}
 }
 
+fn join_nested_quantified_formulas_of_same_type(formula: &mut crate::Formula)
+	-> SimplificationResult
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+		{
+			let mut simplification_result = SimplificationResult::NotSimplified;
+
+			for mut argument in arguments
+			{
+				simplification_result = simplification_result.or(
+					join_nested_quantified_formulas_of_same_type(&mut argument));
+			}
+
+			simplification_result
+		},
+		Formula::Boolean(_)
+		| Formula::Compare(_)
+		| Formula::Predicate(_) => SimplificationResult::NotSimplified,
+		Formula::Exists(ref mut quantified_formula) =>
+		{
+			let mut simplification_result =
+				join_nested_quantified_formulas_of_same_type(&mut quantified_formula.argument);
+
+			if let Formula::Exists(ref mut nested_quantified_formula) = *quantified_formula.argument
+			{
+				// TODO: remove workaround
+				let mut argument = crate::Formula::false_();
+				std::mem::swap(&mut argument, &mut nested_quantified_formula.argument);
+
+				let joined_parameters =
+					[&quantified_formula.parameters[..], &nested_quantified_formula.parameters[..]]
+					.concat()
+					.iter()
+					.map(|x| std::rc::Rc::clone(x))
+					.collect::<Vec<_>>();
+
+				quantified_formula.parameters = std::rc::Rc::new(joined_parameters);
+				*quantified_formula.argument = argument;
+
+				simplification_result = SimplificationResult::Simplified;
+			}
+
+			simplification_result
+		},
+		Formula::ForAll(ref mut quantified_formula) =>
+		{
+			let mut simplification_result =
+				join_nested_quantified_formulas_of_same_type(&mut quantified_formula.argument);
+
+			if let Formula::ForAll(ref mut nested_quantified_formula) = *quantified_formula.argument
+			{
+				// TODO: remove workaround
+				let mut argument = crate::Formula::false_();
+				std::mem::swap(&mut argument, &mut nested_quantified_formula.argument);
+
+				let joined_parameters =
+					[&quantified_formula.parameters[..], &nested_quantified_formula.parameters[..]]
+					.concat()
+					.iter()
+					.map(|x| std::rc::Rc::clone(x))
+					.collect::<Vec<_>>();
+
+				quantified_formula.parameters = std::rc::Rc::new(joined_parameters);
+				*quantified_formula.argument = argument;
+
+				simplification_result = SimplificationResult::Simplified;
+			}
+
+			simplification_result
+		},
+		Formula::Implies(ref mut implies) =>
+			join_nested_quantified_formulas_of_same_type(&mut implies.antecedent)
+				.or(join_nested_quantified_formulas_of_same_type(&mut implies.implication)),
+		Formula::Not(ref mut argument) =>
+			join_nested_quantified_formulas_of_same_type(argument),
+	}
+}
+
 fn simplify_trivial_n_ary_formulas(formula: &mut crate::Formula) -> SimplificationResult
 {
 	use crate::Formula;
@@ -257,6 +341,8 @@ pub(crate) fn simplify(formula: &mut crate::Formula) -> Result<(), crate::Error>
 		if remove_unnecessary_exists_parameters(formula)? == SimplificationResult::Simplified
 			|| simplify_quantified_formulas_without_parameters(formula)
 				== SimplificationResult::Simplified
+			|| join_nested_quantified_formulas_of_same_type(formula)
+				== SimplificationResult::Simplified
 			|| simplify_trivial_n_ary_formulas(formula) == SimplificationResult::Simplified
 		{
 			continue;