From 1b827edd45d801cf630ab2f59595e45853a7d3d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 28 May 2020 04:58:24 +0200 Subject: [PATCH] Clean-up --- src/error.rs | 22 ---------------------- src/utils/copy_formula.rs | 1 + 2 files changed, 1 insertion(+), 22 deletions(-) diff --git a/src/error.rs b/src/error.rs index 4669f8b..35a2ed1 100644 --- a/src/error.rs +++ b/src/error.rs @@ -25,9 +25,7 @@ pub enum Kind UnknownColorChoice(String), VariableNameNotAllowed(String), FormulaNotClosed(std::rc::Rc), - NoCompletedDefinitionFound(std::rc::Rc), PrivatePredicateCycle(std::rc::Rc), - PrivatePredicateInSpecification(std::rc::Rc), PrivatePredicateDependingOnPublicPredicate(std::rc::Rc, std::rc::Rc), RunVampire, @@ -161,13 +159,6 @@ impl Error Self::new(Kind::FormulaNotClosed(free_variables)) } - pub(crate) fn new_no_completed_definition_found( - predicate_declaration: std::rc::Rc) - -> Self - { - Self::new(Kind::NoCompletedDefinitionFound(predicate_declaration)) - } - pub(crate) fn new_private_predicate_cycle( predicate_declaration: std::rc::Rc) -> Self @@ -175,13 +166,6 @@ impl Error Self::new(Kind::PrivatePredicateCycle(predicate_declaration)) } - pub(crate) fn new_private_predicate_in_specification( - predicate_declaration: std::rc::Rc) - -> Self - { - Self::new(Kind::PrivatePredicateInSpecification(predicate_declaration)) - } - pub(crate) fn new_private_predicate_depending_on_public_predicate( private_predicate_declaration: std::rc::Rc, public_predicate_declaration: std::rc::Rc) @@ -267,16 +251,10 @@ impl std::fmt::Debug for Error write!(formatter, ")") }, - Kind::NoCompletedDefinitionFound(ref predicate_declaration) => - write!(formatter, "no completed definition found for {}", predicate_declaration.declaration), Kind::PrivatePredicateCycle(ref predicate_declaration) => write!(formatter, "program is not supertight (private predicate {} transitively depends on itself)", predicate_declaration.declaration), - Kind::PrivatePredicateInSpecification(ref predicate_declaration) => - write!(formatter, - "private predicate {} should not occur in specification (consider declaring it an input or output predicate)", - predicate_declaration.declaration), Kind::PrivatePredicateDependingOnPublicPredicate(ref private_predicate_declaration, ref public_predicate_declaration) => write!(formatter, diff --git a/src/utils/copy_formula.rs b/src/utils/copy_formula.rs index a24f7f2..4e48d2e 100644 --- a/src/utils/copy_formula.rs +++ b/src/utils/copy_formula.rs @@ -212,6 +212,7 @@ fn copy_quantified_formula(quantified_expression: &crate::QuantifiedFormula) crate::QuantifiedFormula::new(copy_parameters, Box::new(copy_argument)) } +#[allow(dead_code)] pub(crate) fn copy_formula(formula: &crate::Formula) -> crate::Formula { use crate::Formula;