Add option for input predicates

src/error.rs

@@ -8,6 +8,7 @@ pub enum Kind
 	DecodeIdentifier,
 	Translate,
 	ReadFile(std::path::PathBuf),
+	ParsePredicateDeclaration,
 }
 
 pub struct Error
@@ -62,6 +63,11 @@ impl Error
 	{
 		Self::new(Kind::ReadFile(path)).with(source)
 	}
+
+	pub(crate) fn new_parse_predicate_declaration() -> Self
+	{
+		Self::new(Kind::ParsePredicateDeclaration)
+	}
 }
 
 impl std::fmt::Debug for Error
@@ -79,6 +85,8 @@ impl std::fmt::Debug for Error
 			Kind::DecodeIdentifier => write!(formatter, "could not decode identifier"),
 			Kind::Translate => write!(formatter, "could not translate input program"),
 			Kind::ReadFile(path) => write!(formatter, "could not read file “{}”", path.display()),
+			Kind::ParsePredicateDeclaration => write!(formatter,
+				"could not parse predicate declaration"),
 		}?;
 
 		if let Some(source) = &self.source

src/lib.rs

@@ -8,3 +8,4 @@ mod utils;
 
 pub use error::Error;
 pub(crate) use utils::*;
+pub use utils::parse_predicate_declaration;

src/main.rs

@@ -14,6 +14,10 @@ enum Command
 		/// Output format (human-readable, tptp)
 		#[structopt(long, default_value = "human-readable")]
 		output_format: anthem::output::Format,
+
+		/// Input predicates (examples: p/0, q/2)
+		#[structopt(long, parse(try_from_str = anthem::parse_predicate_declaration))]
+		input_predicates: Vec<std::rc::Rc<foliage::PredicateDeclaration>>,
 	}
 }
 
@@ -29,10 +33,12 @@ fn main()
 		{
 			input,
 			output_format,
+			input_predicates,
 		}
 			=>
 		{
 			if let Err(error) = anthem::translate::verify_properties::translate(&input,
+				input_predicates.into_iter().collect::<foliage::PredicateDeclarations>(),
 				output_format)
 			{
 				log::error!("could not translate input program: {}", error);

src/output.rs

@@ -1,7 +1,7 @@
 pub(crate) mod human_readable;
 pub(crate) mod tptp;
 
-#[derive(Debug)]
+#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
 pub enum Format
 {
 	HumanReadable,

src/translate/verify_properties.rs

@@ -54,13 +54,21 @@ impl clingo::Logger for Logger
 	}
 }
 
-pub fn translate<P>(program_paths: &[P], output_format: crate::output::Format)
+pub fn translate<P>(program_paths: &[P],
+	input_predicate_declarations: foliage::PredicateDeclarations,
+	output_format: crate::output::Format)
 	-> Result<(), crate::Error>
 where
 	P: AsRef<std::path::Path>
 {
 	let mut statement_handler = StatementHandler::new();
 
+	*statement_handler.context.input_predicate_declarations.borrow_mut()
+		= input_predicate_declarations.clone();
+	*statement_handler.context.predicate_declarations.borrow_mut()
+		= input_predicate_declarations;
+
+	// Read all input programs
 	for program_path in program_paths
 	{
 		let program = std::fs::read_to_string(program_path.as_ref())
@@ -68,6 +76,8 @@ where
 
 		clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX)
 			.map_err(|error| crate::Error::new_translate(error))?;
+
+		log::info!("read input program “{}”", program_path.as_ref().display());
 	}
 
 	let context = statement_handler.context;
@@ -147,69 +157,76 @@ where
 
 	let predicate_declarations = context.predicate_declarations.borrow();
 	let completed_definitions = predicate_declarations.iter()
+		// Don’t perform completion for any input predicate
+		.filter(|x| !context.input_predicate_declarations.borrow().contains(*x))
 		.map(|x| (std::rc::Rc::clone(x), completed_definition(x)));
 
 	// Earlier log messages may have assigned IDs to the variable declarations, so reset them
 	context.variable_declaration_ids.borrow_mut().clear();
 
-	match output_format
+	let print_formula = |formula: &foliage::Formula|
 	{
-		crate::output::Format::HumanReadable =>
+		match output_format
 		{
-			let mut section_separator = "";
+			crate::output::Format::HumanReadable => print!("{}",
+				crate::output::human_readable::display_formula(formula, None, &context)),
+			crate::output::Format::TPTP => print!("{}",
+				crate::output::tptp::display_formula(formula, &context)),
+		}
+	};
 
-			if !predicate_declarations.is_empty()
+	let mut section_separator = "";
-			{
-				println!("{}% completed definitions", section_separator);
-				section_separator = "\n";
-			}
 
-			for (predicate_declaration, completed_definition) in completed_definitions
+	for (i, (predicate_declaration, completed_definition)) in completed_definitions.enumerate()
-			{
+	{
-				println!("%% completed definition of {}/{}\n{}", predicate_declaration.name,
+		if i == 0
-					predicate_declaration.arity, crate::output::human_readable::display_formula(
-						&completed_definition, None, &context));
-			}
-
-			if !context.integrity_constraints.borrow().is_empty()
-			{
-				println!("{}% integrity constraints", section_separator);
-			}
-
-			for integrity_constraint in context.integrity_constraints.borrow().iter()
-			{
-				println!("{}", crate::output::human_readable::display_formula(
-					&integrity_constraint, None, &context));
-			}
-		},
-		crate::output::Format::TPTP =>
 		{
-			let mut section_separator = "";
+			println!("{}% completed definitions", section_separator);
+		}
 
-			if !predicate_declarations.is_empty()
+		println!("%% completed definition of {}/{}", predicate_declaration.name,
-			{
+			predicate_declaration.arity);
-				println!("{}% completed definitions", section_separator);
-				section_separator = "\n";
-			}
 
-			for (predicate_declaration, completed_definition) in completed_definitions
+		if output_format == crate::output::Format::TPTP
-			{
+		{
-				println!("tff(completion_{}_{}, axiom, {}).", predicate_declaration.name,
+			print!("tff(completion_{}_{}, axiom, ", predicate_declaration.name,
-					predicate_declaration.arity, crate::output::tptp::display_formula(
+				predicate_declaration.arity);
-						&completed_definition, &context));
+		}
-			}
 
-			if !context.integrity_constraints.borrow().is_empty()
+		print_formula(&completed_definition);
-			{
-				println!("{}% integrity constraints", section_separator);
-			}
 
-			for integrity_constraint in context.integrity_constraints.borrow().iter()
+		if output_format == crate::output::Format::TPTP
-			{
+		{
-				println!("tff(integrity_constraint, axiom, {}).",
+			print!(").");
-					crate::output::tptp::display_formula(&integrity_constraint, &context));
+		}
-			}
+
-		},
+		println!("");
+
+		section_separator = "\n";
+	}
+
+	for (i, integrity_constraint) in context.integrity_constraints.borrow().iter().enumerate()
+	{
+		if i == 0
+		{
+			println!("{}% integrity constraints", section_separator);
+		}
+
+		if output_format == crate::output::Format::TPTP
+		{
+			print!("tff(integrity_constraint, axiom, ");
+		}
+
+		print_formula(&integrity_constraint);
+
+		if output_format == crate::output::Format::TPTP
+		{
+			print!(").");
+		}
+
+		println!("");
+
+		section_separator = "\n";
 	}
 
 	Ok(())

src/translate/verify_properties/context.rs

@@ -20,6 +20,8 @@ pub(crate) struct Context
 	pub integrity_constraints: std::cell::RefCell<foliage::Formulas>,
 
 	pub input_constant_declaration_domains: std::cell::RefCell<InputConstantDeclarationDomains>,
+	pub input_predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
+
 	pub function_declarations: std::cell::RefCell<foliage::FunctionDeclarations>,
 	pub predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
 	pub variable_declaration_stack: std::cell::RefCell<foliage::VariableDeclarationStack>,
@@ -38,6 +40,9 @@ impl Context
 
 			input_constant_declaration_domains:
 				std::cell::RefCell::new(InputConstantDeclarationDomains::new()),
+			input_predicate_declarations:
+				std::cell::RefCell::new(foliage::PredicateDeclarations::new()),
+
 			function_declarations: std::cell::RefCell::new(foliage::FunctionDeclarations::new()),
 			predicate_declarations: std::cell::RefCell::new(foliage::PredicateDeclarations::new()),
 			variable_declaration_stack:

src/utils.rs

@@ -21,3 +21,35 @@ pub(crate) struct ScopedFormula
 	pub free_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>,
 	pub formula: Box<foliage::Formula>,
 }
+
+pub fn parse_predicate_declaration(input: &str)
+	-> Result<std::rc::Rc<foliage::PredicateDeclaration>, crate::Error>
+{
+	let mut parts = input.split("/");
+
+	let name = match parts.next()
+	{
+		Some(name) => name.to_string(),
+		None => return Err(crate::Error::new_parse_predicate_declaration()),
+	};
+
+	use std::str::FromStr;
+
+	let arity = match parts.next()
+	{
+		Some(arity)
+			=> usize::from_str(arity).map_err(|_| crate::Error::new_parse_predicate_declaration())?,
+		None => return Err(crate::Error::new_parse_predicate_declaration()),
+	};
+
+	if parts.next().is_some()
+	{
+		return Err(crate::Error::new_parse_predicate_declaration());
+	}
+
+	Ok(std::rc::Rc::new(foliage::PredicateDeclaration
+	{
+		name,
+		arity,
+	}))
+}