Show all predicates used in specification by default

src/ast.rs

@@ -137,9 +137,64 @@ impl PredicateDependencySign
 pub type PredicateDependencies =
 	std::collections::BTreeMap<std::rc::Rc<PredicateDeclaration>, PredicateDependencySign>;
 
+#[derive(Clone, Copy, Eq, PartialEq)]
+pub enum PredicateDeclarationSource
+{
+	Program,
+	Specification,
+	ProgramAndSpecification,
+}
+
+impl PredicateDeclarationSource
+{
+	pub fn and(self, other: Self) -> Self
+	{
+		match (self, other)
+		{
+			(Self::ProgramAndSpecification, _)
+			| (_, Self::ProgramAndSpecification) => Self::ProgramAndSpecification,
+			(Self::Program, Self::Program) => Self::Program,
+			(Self::Specification, Self::Specification) => Self::Specification,
+			(Self::Program, Self::Specification)
+			| (Self::Specification, Self::Program) => Self::ProgramAndSpecification,
+		}
+	}
+
+	pub fn and_specification(self) -> Self
+	{
+		match self
+		{
+			Self::Program
+			| Self::ProgramAndSpecification => Self::ProgramAndSpecification,
+			Self::Specification => Self::Specification,
+		}
+	}
+
+	pub fn is_program(&self) -> bool
+	{
+		match self
+		{
+			Self::Program
+			| Self::ProgramAndSpecification => true,
+			Self::Specification => false,
+		}
+	}
+
+	pub fn is_specification(&self) -> bool
+	{
+		match self
+		{
+			Self::Program => false,
+			Self::Specification
+			| Self::ProgramAndSpecification => true,
+		}
+	}
+}
+
 pub struct PredicateDeclaration
 {
 	pub declaration: foliage::PredicateDeclaration,
+	pub source: std::cell::RefCell<PredicateDeclarationSource>,
 	pub dependencies: std::cell::RefCell<Option<PredicateDependencies>>,
 	pub is_input: std::cell::RefCell<bool>,
 	pub is_output: std::cell::RefCell<bool>,
@@ -290,6 +345,7 @@ impl foliage::flavor::PredicateDeclaration for PredicateDeclaration
 		Self
 		{
 			declaration: foliage::PredicateDeclaration::new(name, arity),
+			source: std::cell::RefCell::new(PredicateDeclarationSource::Specification),
 			dependencies: std::cell::RefCell::new(None),
 			is_input: std::cell::RefCell::new(false),
 			is_output: std::cell::RefCell::new(false),

src/commands/verify_program.rs

@@ -27,6 +27,8 @@ where
 
 	log::info!("read specification “{}”", specification_path.as_ref().display());
 
+	problem.process_output_predicates();
+
 	log::info!("reading input program “{}”", program_path.as_ref().display());
 
 	// TODO: make consistent with specification call (path vs. content)

src/input/specification.rs

@@ -166,10 +166,9 @@ fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
 		{
 			input = remaining_input;
 
-			use foliage::FindOrCreatePredicateDeclaration as _;
-
 			let predicate_declaration =
-				problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity);
+				problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity,
+					crate::PredicateDeclarationSource::Specification);
 
 			*predicate_declaration.is_input.borrow_mut() = true;
 		}
@@ -236,10 +235,9 @@ fn output_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
 		{
 			input = remaining_input;
 
-			use foliage::FindOrCreatePredicateDeclaration as _;
-
 			let predicate_declaration =
-				problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity);
+				problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity,
+					crate::PredicateDeclarationSource::Specification);
 
 			*predicate_declaration.is_output.borrow_mut() = true;
 		}

src/problem.rs

@@ -49,6 +49,28 @@ impl Problem
 		section.push(statement);
 	}
 
+	pub(crate) fn process_output_predicates(&self)
+	{
+		let are_any_output_predicates_declared =
+			self.predicate_declarations.borrow().iter().find(|x| *x.is_output.borrow()).is_some();
+
+		if are_any_output_predicates_declared
+		{
+			return;
+		}
+
+		for predicate_declaration in self.predicate_declarations.borrow().iter()
+		{
+			if predicate_declaration.source.borrow().is_specification()
+				&& !*predicate_declaration.is_input.borrow()
+			{
+				log::info!("assuming {} to be an output predicate",
+					predicate_declaration.declaration);
+				*predicate_declaration.is_output.borrow_mut() = true;
+			}
+		}
+	}
+
 	pub(crate) fn check_consistency(&self, proof_direction: ProofDirection)
 		-> Result<(), crate::Error>
 	{
@@ -429,6 +451,35 @@ impl Problem
 	{
 		ProblemTPTPDisplay(self)
 	}
+
+	pub(crate) fn find_or_create_predicate_declaration(&self, name: &str, arity: usize,
+		source: crate::PredicateDeclarationSource)
+		-> std::rc::Rc<crate::PredicateDeclaration>
+	{
+		let mut predicate_declarations = self.predicate_declarations.borrow_mut();
+
+		match predicate_declarations.iter().find(|x| x.matches_signature(name, arity))
+		{
+			Some(declaration) =>
+			{
+				let mut existing_source = declaration.source.borrow_mut();
+				*existing_source = existing_source.and(source);
+
+				std::rc::Rc::clone(&declaration)
+			},
+			None =>
+			{
+				let declaration = crate::PredicateDeclaration::new(name.to_string(), arity);
+				let declaration = std::rc::Rc::new(declaration);
+
+				predicate_declarations.insert(std::rc::Rc::clone(&declaration));
+
+				log::debug!("new predicate declaration: {}/{}", name, arity);
+
+				declaration
+			},
+		}
+	}
 }
 
 struct ProblemTPTPDisplay<'p>(&'p Problem);
@@ -625,23 +676,8 @@ impl foliage::FindOrCreatePredicateDeclaration<crate::FoliageFlavor> for Problem
 	fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
 		-> std::rc::Rc<crate::PredicateDeclaration>
 	{
-		let mut predicate_declarations = self.predicate_declarations.borrow_mut();
+		(self as &Problem).find_or_create_predicate_declaration(name, arity,
-
+			crate::PredicateDeclarationSource::Specification)
-		match predicate_declarations.iter().find(|x| x.matches_signature(name, arity))
-		{
-			Some(declaration) => std::rc::Rc::clone(&declaration),
-			None =>
-			{
-				let declaration = crate::PredicateDeclaration::new(name.to_string(), arity);
-				let declaration = std::rc::Rc::new(declaration);
-
-				predicate_declarations.insert(std::rc::Rc::clone(&declaration));
-
-				log::debug!("new predicate declaration: {}/{}", name, arity);
-
-				declaration
-			},
-		}
 	}
 }