Handle private predicates in specification

src/commands/verify_program.rs

@@ -39,8 +39,18 @@ where
 
 	if let Err(error) = problem.check_consistency(proof_direction)
 	{
-		log::error!("{}", error);
+		match error.kind
-		std::process::exit(1)
+		{
+			// In forward proofs, it’s okay to use private predicates in the specification, but
+			// issue a warning regardless
+			crate::error::Kind::PrivatePredicateInSpecification(_)
+				if !proof_direction.requires_backward_proof() => log::warn!("{}", error),
+			_ =>
+			{
+				log::error!("{}", error);
+				std::process::exit(1)
+			},
+		}
 	}
 
 	if !no_simplify

src/error.rs

@@ -26,6 +26,7 @@ pub enum Kind
 	VariableNameNotAllowed(String),
 	FormulaNotClosed(std::rc::Rc<crate::VariableDeclarations>),
 	PrivatePredicateCycle(std::rc::Rc<crate::PredicateDeclaration>),
+	PrivatePredicateInSpecification(std::rc::Rc<crate::PredicateDeclaration>),
 	RunVampire,
 	// TODO: rename to something Vampire-specific
 	ProveProgram(Option<i32>, String, String),
@@ -164,6 +165,13 @@ impl Error
 		Self::new(Kind::PrivatePredicateCycle(predicate_declaration))
 	}
 
+	pub(crate) fn new_private_predicate_in_specification(
+		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
+		-> Self
+	{
+		Self::new(Kind::PrivatePredicateInSpecification(predicate_declaration))
+	}
+
 	pub(crate) fn new_run_vampire<S: Into<Source>>(source: S) -> Self
 	{
 		Self::new(Kind::RunVampire).with(source)
@@ -244,6 +252,10 @@ impl std::fmt::Debug for Error
 				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::RunVampire => write!(formatter, "could not run Vampire"),
 			Kind::ProveProgram(exit_code, ref stdout, ref stderr) =>
 			{

src/problem.rs

@@ -74,6 +74,31 @@ impl Problem
 				return Err(crate::Error::new_private_predicate_cycle(
 					std::rc::Rc::clone(&predicate_declaration)));
 			}
+
+			if predicate_declaration.is_public()
+			{
+				continue;
+			}
+
+			for (_, statements) in self.statements.borrow().iter()
+			{
+				for statement in statements
+				{
+					match statement.kind
+					{
+						crate::problem::StatementKind::CompletedDefinition(_)
+						| crate::problem::StatementKind::IntegrityConstraint
+						| crate::problem::StatementKind::Lemma(_) => continue,
+						_ => (),
+					}
+
+					if crate::formula_contains_predicate(&statement.formula, predicate_declaration)
+					{
+						return Err(crate::Error::new_private_predicate_in_specification(
+							std::rc::Rc::clone(predicate_declaration)));
+					}
+				}
+			}
 		}
 
 		Ok(())

src/utils.rs

@@ -3,6 +3,7 @@ mod autoname_variables;
 mod closures;
 mod collect_predicate_declarations;
 mod copy_formula;
+mod formula_contains_predicate;
 mod variables_in_terms;
 
 pub(crate) use autoname_variables::*;
@@ -10,6 +11,7 @@ pub(crate) use arithmetic_terms::*;
 pub(crate) use closures::*;
 pub(crate) use collect_predicate_declarations::*;
 pub(crate) use copy_formula::*;
+pub(crate) use formula_contains_predicate::*;
 pub(crate) use variables_in_terms::*;
 
 #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]

src/utils/formula_contains_predicate.rs

@@ -0,0 +1,25 @@
+pub(crate) fn formula_contains_predicate(formula: &crate::Formula,
+	predicate_declaration: &crate::PredicateDeclaration)
+	-> bool
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+			arguments.iter().any(
+				|argument| formula_contains_predicate(argument, predicate_declaration)),
+		Formula::Boolean(_)
+		| Formula::Compare(_) => false,
+		Formula::Exists(quantified_expression)
+		| Formula::ForAll(quantified_expression) =>
+			formula_contains_predicate(&quantified_expression.argument, predicate_declaration),
+		Formula::Implies(implies) =>
+			formula_contains_predicate(&implies.antecedent, predicate_declaration)
+			|| formula_contains_predicate(&implies.implication, predicate_declaration),
+		Formula::Not(argument) => formula_contains_predicate(argument, predicate_declaration),
+		Formula::Predicate(predicate) => &*predicate.declaration == predicate_declaration,
+	}
+}

src/utils/output_predicates.rs

@@ -1,140 +0,0 @@
-pub(crate) fn formula_contains_predicate(formula: &crate::Formula,
-	predicate_declaration: &crate::PredicateDeclaration)
-	-> bool
-{
-	use crate::Formula;
-
-	match formula
-	{
-		Formula::And(arguments)
-		| Formula::IfAndOnlyIf(arguments)
-		| Formula::Or(arguments) =>
-			arguments.iter().any(
-				|argument| formula_contains_predicate(argument, predicate_declaration)),
-		Formula::Boolean(_)
-		| Formula::Compare(_) => false,
-		Formula::Exists(quantified_expression)
-		| Formula::ForAll(quantified_expression) =>
-			formula_contains_predicate(&quantified_expression.argument, predicate_declaration),
-		Formula::Implies(implies) =>
-			formula_contains_predicate(&implies.antecedent, predicate_declaration)
-			|| formula_contains_predicate(&implies.implication, predicate_declaration),
-		Formula::Not(argument) => formula_contains_predicate(argument, predicate_declaration),
-		Formula::Predicate(predicate) => &*predicate.declaration == predicate_declaration,
-	}
-}
-
-fn replace_predicate_in_formula(formula: &mut crate::Formula,
-	predicate_to_replace: &crate::Predicate, replacement_formula: &crate::Formula)
-{
-	use crate::{Formula, Term};
-
-	match formula
-	{
-		Formula::And(arguments)
-		| Formula::IfAndOnlyIf(arguments)
-		| Formula::Or(arguments) =>
-			for mut argument in arguments
-			{
-				replace_predicate_in_formula(&mut argument, predicate_to_replace,
-					replacement_formula);
-			},
-		Formula::Boolean(_)
-		| Formula::Compare(_) => (),
-		Formula::Exists(quantified_expression)
-		| Formula::ForAll(quantified_expression) =>
-			replace_predicate_in_formula(&mut quantified_expression.argument, predicate_to_replace,
-				replacement_formula),
-		Formula::Implies(implies) =>
-		{
-			replace_predicate_in_formula(&mut implies.antecedent, predicate_to_replace,
-				replacement_formula);
-			replace_predicate_in_formula(&mut implies.implication, predicate_to_replace,
-				replacement_formula);
-		},
-		Formula::Not(argument) =>
-			replace_predicate_in_formula(argument, predicate_to_replace, replacement_formula),
-		Formula::Predicate(predicate) =>
-			if predicate.declaration == predicate_to_replace.declaration
-			{
-				let mut replacement_formula = crate::utils::copy_formula(replacement_formula);
-
-				for (index, argument) in predicate.arguments.iter().enumerate()
-				{
-					let variable_declaration = match &predicate_to_replace.arguments[index]
-					{
-						Term::Variable(variable) => &variable.declaration,
-						_ => panic!("invalid completed definition"),
-					};
-
-					crate::utils::replace_variable_in_formula_with_term(&mut replacement_formula,
-						&variable_declaration, argument);
-				}
-
-				*formula = replacement_formula;
-			},
-	}
-}
-
-pub(crate) fn replace_predicate_in_formula_with_completed_definition(
-	formula: &mut crate::Formula, completed_definition: &crate::Formula)
-	-> Result<(), crate::Error>
-{
-	use crate::Formula;
-
-	let false_ = crate::Formula::false_();
-
-	// TODO: refactor
-	let (completed_definition_predicate, completed_definition) = match completed_definition
-	{
-		Formula::ForAll(quantified_expression) => match *quantified_expression.argument
-		{
-			Formula::IfAndOnlyIf(ref arguments) =>
-			{
-				assert_eq!(arguments.len(), 2, "invalid completed definition");
-
-				match arguments[0]
-				{
-					Formula::Predicate(ref predicate) => (predicate, &arguments[1]),
-					_ => panic!("invalid completed definition"),
-				}
-			},
-			Formula::Not(ref argument) => match **argument
-			{
-				Formula::Predicate(ref predicate) => (predicate, &false_),
-				_ => panic!("invalid completed definition"),
-			},
-			_ => panic!("invalid completed definition"),
-		},
-		Formula::IfAndOnlyIf(ref arguments) =>
-		{
-			assert_eq!(arguments.len(), 2, "invalid completed definition");
-
-			match arguments[0]
-			{
-				Formula::Predicate(ref predicate) => (predicate, &arguments[1]),
-				_ => panic!("invalid completed definition"),
-			}
-		},
-		Formula::Not(ref argument) => match **argument
-		{
-			Formula::Predicate(ref predicate) => (predicate, &false_),
-			_ => panic!("invalid completed definition"),
-		},
-		_ => panic!("invalid completed definition"),
-	};
-
-	// Predicates can only be substituted by their completed definitions if there is no cycle.
-	// For example, if the completed definition of p/1 references q/1 and vice versa, neither can
-	// be replaced with the completed definition of the other
-	if formula_contains_predicate(completed_definition, &completed_definition_predicate.declaration)
-		&& formula_contains_predicate(formula, &completed_definition_predicate.declaration)
-	{
-		return Err(crate::Error::new_cannot_hide_predicate(
-			std::rc::Rc::clone(&completed_definition_predicate.declaration)));
-	}
-
-	replace_predicate_in_formula(formula, completed_definition_predicate, completed_definition);
-
-	Ok(())
-}