From 84031c483b3ac2279a20ed0c56123170248c0f70 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 13 May 2020 03:27:47 +0200 Subject: [PATCH] Revert logic for building completed definitions --- src/translate/verify_properties.rs | 43 +++++------------------------- 1 file changed, 7 insertions(+), 36 deletions(-) diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 25d74a8..d00a465 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -141,49 +141,20 @@ impl<'p> Translator<'p> } }; - // 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::>(); - - // 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() + for predicate_declaration in self.problem.predicate_declarations.borrow().iter() { - let hidden_predicate_declarations = - predicate_declarations.difference(&output_predicate_declarations); - - for hidden_predicate_declaration in hidden_predicate_declarations + // Don’t perform completion for input predicates + if self.problem.input_predicate_declarations.borrow().contains(predicate_declaration) { - log::debug!("hidden: {}", hidden_predicate_declaration); + continue; } - } - for (predicate_declaration, completed_definition) in completed_definitions.into_iter() - { let statement_kind = crate::problem::StatementKind::CompletedDefinition( std::rc::Rc::clone(&predicate_declaration)); + let completed_definition = completed_definition(predicate_declaration, + &mut self.definitions, self.problem); + let statement = crate::problem::Statement::new(statement_kind, completed_definition) .with_name(format!("completed_definition_{}_{}", predicate_declaration.name, predicate_declaration.arity));