From 0dbf30bb1bbb169a891d6012815da103954015b0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Wed, 13 May 2020 02:24:13 +0200
Subject: [PATCH] Work in progress

---
 src/problem.rs                     | 19 +++++++-----
 src/translate/verify_properties.rs | 49 ++++++++++++++++++++++++------
 2 files changed, 51 insertions(+), 17 deletions(-)

diff --git a/src/problem.rs b/src/problem.rs
index 2260841..e9263c7 100644
--- a/src/problem.rs
+++ b/src/problem.rs
@@ -4,11 +4,12 @@ mod section_kind;
 pub use proof_direction::ProofDirection;
 pub use section_kind::SectionKind;
 
-#[derive(Copy, Clone, Eq, PartialEq)]
+#[derive(Eq, PartialEq)]
 pub enum StatementKind
 {
 	Axiom,
-	Program,
+	CompletedDefinition(std::rc::Rc<foliage::PredicateDeclaration>),
+	IntegrityConstraint,
 	Assumption,
 	Lemma(ProofDirection),
 	Assertion,
@@ -155,7 +156,7 @@ impl Problem
 		{
 			self.print_step_title("Started",
 				termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green)));
-			self.shell.borrow_mut().println(&"verification of assertions from completed definitions",
+			self.shell.borrow_mut().println(&"verification of assertions from translated program",
 				&termcolor::ColorSpec::new());
 
 			let mut statements = self.statements.borrow_mut();
@@ -169,7 +170,8 @@ impl Problem
 					{
 						StatementKind::Axiom
 						| StatementKind::Assumption
-						| StatementKind::Program =>
+						| StatementKind::CompletedDefinition(_)
+						| StatementKind::IntegrityConstraint =>
 							statement.proof_status = ProofStatus::AssumedProven,
 						StatementKind::Lemma(ProofDirection::Backward) =>
 							statement.proof_status = ProofStatus::Ignored,
@@ -193,7 +195,7 @@ impl Problem
 			};
 
 			self.print_step_title("Finished", &step_title_color);
-			println!("verification of assertions from completed definitions");
+			println!("verification of assertions from translated program");
 		}
 
 		if proof_direction == ProofDirection::Both
@@ -206,7 +208,7 @@ impl Problem
 		{
 			self.print_step_title("Started",
 				termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green)));
-			self.shell.borrow_mut().println(&"verification of completed definitions from assertions",
+			self.shell.borrow_mut().println(&"verification of translated program from assertions",
 				&termcolor::ColorSpec::new());
 
 			let mut statements = self.statements.borrow_mut();
@@ -244,7 +246,7 @@ impl Problem
 			};
 
 			self.print_step_title("Finished", &step_title_color);
-			println!("verification of completed definitions from assertions");
+			println!("verification of translated program from assertions");
 		}
 
 		Ok(())
@@ -313,7 +315,8 @@ impl Problem
 
 			match statement.kind
 			{
-				StatementKind::Program =>
+				StatementKind::CompletedDefinition(_)
+				| StatementKind::IntegrityConstraint =>
 					print!("{}",
 						foliage::format::display_formula(&statement.formula, format_context)),
 				_ =>
diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs
index 772dac0..b03426e 100644
--- a/src/translate/verify_properties.rs
+++ b/src/translate/verify_properties.rs
@@ -141,19 +141,50 @@ impl<'p> Translator<'p>
 			}
 		};
 
-		for predicate_declaration in self.problem.predicate_declarations.borrow().iter()
+		// TODO: refactor
+		let predicate_declarations = self.problem.predicate_declarations.borrow();
+		let input_predicate_declarations = self.problem.input_predicate_declarations.borrow();
+		let mut definitions = &mut self.definitions;
+		let problem = &self.problem;
+
+		let completed_definitions = predicate_declarations.iter()
+			.filter_map(
+				|predicate_declaration|
+				{
+					// Don’t perform completion for input predicates
+					if input_predicate_declarations.contains(predicate_declaration)
+					{
+						return None;
+					}
+
+					let completed_definition = completed_definition(predicate_declaration,
+						&mut definitions, problem);
+
+					Some((std::rc::Rc::clone(predicate_declaration), completed_definition))
+				})
+			.collect::<std::collections::BTreeMap<_, _>>();
+
+		// Replace occurrences of hidden predicates with their completed definitions
+		let output_predicate_declarations = self.problem.output_predicate_declarations.borrow();
+
+		// If no output statements are present, don’t hide any predicates by default
+		if !output_predicate_declarations.is_empty()
 		{
-			// Don’t perform completion for input predicates
-			if self.problem.input_predicate_declarations.borrow().contains(predicate_declaration)
+			let hidden_predicate_declarations =
+				predicate_declarations.difference(&output_predicate_declarations);
+
+			for hidden_predicate_declaration in hidden_predicate_declarations
 			{
-				continue;
+				log::debug!("hidden: {}", hidden_predicate_declaration);
 			}
+		}
 
-			let completed_definition =
-				completed_definition(predicate_declaration, &mut self.definitions, self.problem);
+		for (predicate_declaration, completed_definition) in completed_definitions.into_iter()
+		{
+			let statement_kind = crate::problem::StatementKind::CompletedDefinition(
+				std::rc::Rc::clone(&predicate_declaration));
 
-			let statement = crate::problem::Statement::new(
-				crate::problem::StatementKind::Program, completed_definition)
+			let statement = crate::problem::Statement::new(statement_kind, completed_definition)
 				.with_name(format!("completed_definition_{}_{}", predicate_declaration.name,
 					predicate_declaration.arity))
 				.with_description(format!("completed definition of {}/{}",
@@ -295,7 +326,7 @@ impl<'p> Translator<'p>
 				let integrity_constraint = crate::universal_closure(open_formula);
 
 				let statement = crate::problem::Statement::new(
-					crate::problem::StatementKind::Program, integrity_constraint)
+					crate::problem::StatementKind::IntegrityConstraint, integrity_constraint)
 					.with_name("integrity_constraint".to_string())
 					.with_description("integrity constraint".to_string());