Add option for input constants

src/error.rs

@@ -9,6 +9,7 @@ pub enum Kind
 	Translate,
 	ReadFile(std::path::PathBuf),
 	ParsePredicateDeclaration,
+	ParseConstantDeclaration,
 }
 
 pub struct Error
@@ -68,6 +69,11 @@ impl Error
 	{
 		Self::new(Kind::ParsePredicateDeclaration)
 	}
+
+	pub(crate) fn new_parse_constant_declaration() -> Self
+	{
+		Self::new(Kind::ParseConstantDeclaration)
+	}
 }
 
 impl std::fmt::Debug for Error
@@ -87,6 +93,8 @@ impl std::fmt::Debug for Error
 			Kind::ReadFile(path) => write!(formatter, "could not read file “{}”", path.display()),
 			Kind::ParsePredicateDeclaration => write!(formatter,
 				"could not parse predicate declaration"),
+			Kind::ParseConstantDeclaration => write!(formatter,
+				"could not parse constant declaration"),
 		}?;
 
 		if let Some(source) = &self.source

src/lib.rs

@@ -8,4 +8,5 @@ mod utils;
 
 pub use error::Error;
 pub(crate) use utils::*;
-pub use utils::parse_predicate_declaration;
+pub use utils::{Domain, InputConstantDeclarationDomains, parse_predicate_declaration,
+	parse_constant_declaration};

src/main.rs

@@ -18,6 +18,11 @@ enum Command
 		/// 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>>,
+
+		/// Input constants (example: c, integer(n))
+		#[structopt(long, parse(try_from_str = anthem::parse_constant_declaration))]
+		input_constants: Vec<
+			(std::rc::Rc<foliage::FunctionDeclaration>, anthem::Domain)>,
 	}
 }
 
@@ -34,11 +39,13 @@ fn main()
 			input,
 			output_format,
 			input_predicates,
+			input_constants,
 		}
 			=>
 		{
 			if let Err(error) = anthem::translate::verify_properties::translate(&input,
 				input_predicates.into_iter().collect::<foliage::PredicateDeclarations>(),
+				input_constants.into_iter().collect::<std::collections::BTreeMap<_, _>>(),
 				output_format)
 			{
 				log::error!("could not translate input program: {}", error);

src/translate/verify_properties.rs

@@ -56,6 +56,7 @@ impl clingo::Logger for Logger
 
 pub fn translate<P>(program_paths: &[P],
 	input_predicate_declarations: foliage::PredicateDeclarations,
+	input_constant_declaration_domains: crate::InputConstantDeclarationDomains,
 	output_format: crate::output::Format)
 	-> Result<(), crate::Error>
 where
@@ -67,6 +68,23 @@ where
 		= input_predicate_declarations.clone();
 	*statement_handler.context.predicate_declarations.borrow_mut()
 		= input_predicate_declarations;
+	*statement_handler.context.function_declarations.borrow_mut()
+		= input_constant_declaration_domains.keys().map(std::rc::Rc::clone).collect();
+	*statement_handler.context.input_constant_declaration_domains.borrow_mut()
+		= input_constant_declaration_domains;
+
+	for input_predicate_declaration in statement_handler.context.input_predicate_declarations
+		.borrow().iter()
+	{
+		log::info!("input predicate: {}/{}", input_predicate_declaration.name,
+			input_predicate_declaration.arity);
+	}
+
+	for (input_constant_declaration, domain) in statement_handler.context
+		.input_constant_declaration_domains.borrow().iter()
+	{
+		log::info!("input constant: {} (domain: {:?})", input_constant_declaration.name, domain);
+	}
 
 	// Read all input programs
 	for program_path in program_paths

src/translate/verify_properties/context.rs

@@ -4,9 +4,6 @@ pub(crate) struct Definitions
 	pub definitions: Vec<crate::ScopedFormula>,
 }
 
-type InputConstantDeclarationDomains
-	= std::collections::BTreeMap<std::rc::Rc<foliage::FunctionDeclaration>, crate::Domain>;
-
 type VariableDeclarationDomains
 	= std::collections::BTreeMap<std::rc::Rc<foliage::VariableDeclaration>, crate::Domain>;
 
@@ -19,7 +16,8 @@ pub(crate) struct Context
 		std::rc::Rc<foliage::PredicateDeclaration>, Definitions>>,
 	pub integrity_constraints: std::cell::RefCell<foliage::Formulas>,
 
-	pub input_constant_declaration_domains: std::cell::RefCell<InputConstantDeclarationDomains>,
+	pub input_constant_declaration_domains: std::cell::RefCell<
+		crate::InputConstantDeclarationDomains>,
 	pub input_predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
 
 	pub function_declarations: std::cell::RefCell<foliage::FunctionDeclarations>,
@@ -40,7 +38,7 @@ impl Context
 			integrity_constraints: std::cell::RefCell::new(vec![]),
 
 			input_constant_declaration_domains:
-				std::cell::RefCell::new(InputConstantDeclarationDomains::new()),
+				std::cell::RefCell::new(crate::InputConstantDeclarationDomains::new()),
 			input_predicate_declarations:
 				std::cell::RefCell::new(foliage::PredicateDeclarations::new()),
 

src/utils.rs

@@ -11,19 +11,42 @@ pub(crate) enum OperatorNotation
 	Infix,
 }
 
-#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
+#[derive(Clone, Copy, Eq, Ord, PartialEq, PartialOrd)]
-pub(crate) enum Domain
+pub enum Domain
 {
 	Program,
 	Integer,
 }
 
+impl std::fmt::Debug for Domain
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match self
+		{
+			Domain::Program => write!(formatter, "program"),
+			Domain::Integer => write!(formatter, "integer"),
+		}
+	}
+}
+
+impl std::fmt::Display for Domain
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(formatter, "{:?}", self)
+	}
+}
+
 pub(crate) struct ScopedFormula
 {
 	pub free_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>,
 	pub formula: Box<foliage::Formula>,
 }
 
+pub type InputConstantDeclarationDomains
+	= std::collections::BTreeMap<std::rc::Rc<foliage::FunctionDeclaration>, Domain>;
+
 pub fn parse_predicate_declaration(input: &str)
 	-> Result<std::rc::Rc<foliage::PredicateDeclaration>, crate::Error>
 {
@@ -55,3 +78,35 @@ pub fn parse_predicate_declaration(input: &str)
 		arity,
 	}))
 }
+
+pub fn parse_constant_declaration(input: &str)
+	-> Result<(std::rc::Rc<foliage::FunctionDeclaration>, crate::Domain), crate::Error>
+{
+	let mut parts = input.split(":");
+
+	let name = parts.next().ok_or(crate::Error::new_parse_constant_declaration())?.trim();
+
+	let domain = match parts.next()
+	{
+		None => crate::Domain::Program,
+		Some(value) => match value.trim()
+		{
+			"program" => crate::Domain::Program,
+			"integer" => crate::Domain::Integer,
+			_ => return Err(crate::Error::new_parse_constant_declaration()),
+		},
+	};
+
+	if parts.next().is_some()
+	{
+		return Err(crate::Error::new_parse_constant_declaration());
+	}
+
+	let constant_declaration = std::rc::Rc::new(foliage::FunctionDeclaration
+	{
+		name: name.to_string(),
+		arity: 0,
+	});
+
+	Ok((constant_declaration, domain))
+}