patrick
/
anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Restructure project

This commit is contained in:
Patrick Lühne 2020-02-04 16:45:06 +01:00
parent 87a3517bfb
commit 3dbe11be61
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
7 changed files with 292 additions and 474 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/lib.rs
View File

@ -3,5 +3,7 @@
pub mod error;
pub mod output;
pub mod translate;
mod utils;
pub use error::Error;
pub(crate) use utils::*;

4
src/output/human_readable.rs
View File

@ -137,8 +137,8 @@ where
let prefix = match domain
{
crate::translate::common::Domain::Integer => "N",
crate::translate::common::Domain::Program => "X",
crate::Domain::Integer => "N",
crate::Domain::Program => "X",
};
write!(format, "{}{}", prefix, id + 1)

12
src/output/tptp.rs
View File

@ -1,9 +1,9 @@
pub(crate) struct DomainDisplay
{
domain: crate::translate::common::Domain,
domain: crate::Domain,
}
pub(crate) fn display_domain(domain: crate::translate::common::Domain) -> DomainDisplay
pub(crate) fn display_domain(domain: crate::Domain) -> DomainDisplay
{
DomainDisplay
{
@ -17,8 +17,8 @@ impl std::fmt::Debug for DomainDisplay
{
let domain_name = match self.domain
{
crate::translate::common::Domain::Integer => "$int",
crate::translate::common::Domain::Program => "object",
crate::Domain::Integer => "$int",
crate::Domain::Program => "object",
};
write!(format, "{}", domain_name)
@ -107,8 +107,8 @@ where
let prefix = match domain
{
crate::translate::common::Domain::Integer => "N",
crate::translate::common::Domain::Program => "X",
crate::Domain::Integer => "N",
crate::Domain::Program => "X",
};
write!(format, "{}{}", prefix, id + 1)

278
src/translate/common.rs
View File

@ -1,20 +1,17 @@
#[derive(Clone, Copy, Debug, PartialEq)]
pub(crate) enum Domain
{
Program,
Integer,
}
mod choose_value_in_term;
pub(crate) use choose_value_in_term::*;
pub(crate) trait AssignVariableDeclarationDomain
{
fn assign_variable_declaration_domain(&self,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>, domain: Domain);
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>, domain: crate::Domain);
}
pub(crate) trait VariableDeclarationDomain
{
fn variable_declaration_domain(&self,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>) -> Option<Domain>;
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>) -> Option<crate::Domain>;
}
pub(crate) trait VariableDeclarationID
@ -84,268 +81,3 @@ pub(crate) fn translate_comparison_operator(comparison_operator: clingo::ast::Co
=> foliage::ComparisonOperator::Equal,
}
}
pub(crate) fn choose_value_in_primitive(term: Box<foliage::Term>,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-> foliage::Formula
{
let variable = foliage::Term::variable(variable_declaration);
foliage::Formula::equal(Box::new(variable), term)
}
pub(crate) fn choose_value_in_term<C>(term: &clingo::ast::Term,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>, context: &C)
-> Result<foliage::Formula, crate::Error>
where
C: crate::translate::common::GetOrCreateFunctionDeclaration
+ crate::translate::common::GetOrCreateVariableDeclaration
+ crate::translate::common::AssignVariableDeclarationDomain
{
match term.term_type()
{
clingo::ast::TermType::Symbol(symbol) => match symbol.symbol_type()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
{
clingo::SymbolType::Number => Ok(choose_value_in_primitive(
Box::new(foliage::Term::integer(symbol.number()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?)),
variable_declaration)),
clingo::SymbolType::Infimum => Ok(choose_value_in_primitive(
Box::new(foliage::Term::infimum()), variable_declaration)),
clingo::SymbolType::Supremum => Ok(choose_value_in_primitive(
Box::new(foliage::Term::supremum()), variable_declaration)),
clingo::SymbolType::String => Ok(choose_value_in_primitive(
Box::new(foliage::Term::string(symbol.string()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
.to_string())),
variable_declaration)),
clingo::SymbolType::Function =>
{
let arguments = symbol.arguments()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?;
// Functions with arguments are represented as clingo::ast::Function by the parser.
// At this point, we only have to handle (0-ary) constants
if !arguments.is_empty()
{
return Err(crate::Error::new_logic("unexpected arguments, expected (0-ary) constant symbol"));
}
let constant_name = symbol.name()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?;
let constant_declaration = context.get_or_create_function_declaration(constant_name, 0);
let function = foliage::Term::function(&constant_declaration, vec![]);
Ok(choose_value_in_primitive(Box::new(function), variable_declaration))
}
},
clingo::ast::TermType::Variable(variable_name) =>
{
let other_variable_declaration = context.get_or_create_variable_declaration(
variable_name);
context.assign_variable_declaration_domain(&other_variable_declaration,
Domain::Program);
let other_variable = foliage::Term::variable(&other_variable_declaration);
Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration))
},
clingo::ast::TermType::BinaryOperation(binary_operation) =>
{
let operator = crate::translate::common::translate_binary_operator(
binary_operation.binary_operator())?;
match operator
{
foliage::BinaryOperator::Add
| foliage::BinaryOperator::Subtract
| foliage::BinaryOperator::Multiply
=>
{
let parameters = (0..2).map(|_|
{
let variable_declaration = std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string()));
context.assign_variable_declaration_domain(&variable_declaration,
Domain::Integer);
variable_declaration
})
.collect::<foliage::VariableDeclarations>();
let parameters = std::rc::Rc::new(parameters);
let parameter_1 = &parameters[0];
let parameter_2 = &parameters[1];
let translated_binary_operation = foliage::Term::binary_operation(operator,
Box::new(foliage::Term::variable(&parameter_1)),
Box::new(foliage::Term::variable(&parameter_2)));
let equals = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(translated_binary_operation));
let choose_value_from_left_argument = choose_value_in_term(
binary_operation.left(), &parameter_1, context)?;
let choose_value_from_right_argument = choose_value_in_term(
binary_operation.right(), &parameter_2, context)?;
let and = foliage::Formula::And(vec![Box::new(equals),
Box::new(choose_value_from_left_argument),
Box::new(choose_value_from_right_argument)]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
foliage::BinaryOperator::Divide
| foliage::BinaryOperator::Modulo
=>
{
let parameters = (0..4).map(|_|
{
let variable_declaration = std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string()));
context.assign_variable_declaration_domain(&variable_declaration,
Domain::Integer);
variable_declaration
})
.collect::<foliage::VariableDeclarations>();
let parameters = std::rc::Rc::new(parameters);
let parameter_i = &parameters[0];
let parameter_j = &parameters[1];
let parameter_q = &parameters[2];
let parameter_r = &parameters[3];
let j_times_q = foliage::Term::multiply(
Box::new(foliage::Term::variable(parameter_j)),
Box::new(foliage::Term::variable(parameter_q)));
let j_times_q_plus_r = foliage::Term::add(Box::new(j_times_q),
Box::new(foliage::Term::variable(parameter_r)));
let i_equals_j_times_q_plus_r = foliage::Formula::equal(
Box::new(foliage::Term::variable(parameter_j)), Box::new(j_times_q_plus_r));
let choose_i_in_t1 = choose_value_in_term(binary_operation.left(), parameter_i,
context)?;
let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), parameter_j,
context)?;
let j_not_equal_to_0 = foliage::Formula::not_equal(
Box::new(foliage::Term::variable(parameter_j)),
Box::new(foliage::Term::integer(0)));
let r_greater_or_equal_to_0 = foliage::Formula::greater_or_equal(
Box::new(foliage::Term::variable(parameter_r)),
Box::new(foliage::Term::integer(0)));
let r_less_than_q = foliage::Formula::less(
Box::new(foliage::Term::variable(parameter_r)),
Box::new(foliage::Term::variable(parameter_q)));
let z_equal_to_q = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(foliage::Term::variable(parameter_q)));
let z_equal_to_r = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(foliage::Term::variable(parameter_r)));
let last_argument = match operator
{
foliage::BinaryOperator::Divide => z_equal_to_q,
foliage::BinaryOperator::Modulo => z_equal_to_r,
_ => return Err(crate::Error::new_logic("unreachable code")),
};
let and = foliage::Formula::and(vec![Box::new(i_equals_j_times_q_plus_r),
Box::new(choose_i_in_t1), Box::new(choose_i_in_t2),
Box::new(j_not_equal_to_0), Box::new(r_greater_or_equal_to_0),
Box::new(r_less_than_q), Box::new(last_argument)]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
foliage::BinaryOperator::Exponentiate =>
Err(crate::Error::new_unsupported_language_feature("exponentiation")),
}
},
clingo::ast::TermType::UnaryOperation(unary_operation) =>
{
match unary_operation.unary_operator()
{
clingo::ast::UnaryOperator::Absolute =>
return Err(crate::Error::new_unsupported_language_feature("absolute value")),
clingo::ast::UnaryOperator::Minus =>
{
let parameter_z_prime = std::rc::Rc::new(foliage::VariableDeclaration::new(
"<anonymous>".to_string()));
context.assign_variable_declaration_domain(&parameter_z_prime, Domain::Integer);
let negative_z_prime = foliage::Term::negative(Box::new(
foliage::Term::variable(&parameter_z_prime)));
let equals = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(negative_z_prime));
let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(),
&parameter_z_prime, context)?;
let and = foliage::Formula::and(vec![Box::new(equals),
Box::new(choose_z_prime_in_t_prime)]);
let parameters = std::rc::Rc::new(vec![parameter_z_prime]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
_ => Err(crate::Error::new_not_yet_implemented("todo")),
}
},
clingo::ast::TermType::Interval(interval) =>
{
let parameters = (0..3).map(|_|
{
let variable_declaration = std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string()));
context.assign_variable_declaration_domain(&variable_declaration,
Domain::Integer);
variable_declaration
})
.collect::<foliage::VariableDeclarations>();
let parameters = std::rc::Rc::new(parameters);
let parameter_i = &parameters[0];
let parameter_j = &parameters[1];
let parameter_k = &parameters[2];
let choose_i_in_t_1 = choose_value_in_term(interval.left(), parameter_i, context)?;
let choose_j_in_t_2 = choose_value_in_term(interval.right(), parameter_j, context)?;
let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal(
Box::new(foliage::Term::variable(parameter_i)),
Box::new(foliage::Term::variable(parameter_k)));
let k_less_than_or_equal_to_j = foliage::Formula::less_or_equal(
Box::new(foliage::Term::variable(parameter_k)),
Box::new(foliage::Term::variable(parameter_j)));
let z_equals_k = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(foliage::Term::variable(parameter_k)));
let and = foliage::Formula::and(vec![Box::new(choose_i_in_t_1),
Box::new(choose_j_in_t_2), Box::new(i_less_than_or_equal_to_k),
Box::new(k_less_than_or_equal_to_j), Box::new(z_equals_k)]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
clingo::ast::TermType::Function(_) =>
Err(crate::Error::new_unsupported_language_feature("symbolic functions")),
clingo::ast::TermType::Pool(_) =>
Err(crate::Error::new_unsupported_language_feature("pools")),
clingo::ast::TermType::ExternalFunction(_) =>
Err(crate::Error::new_unsupported_language_feature("external functions")),
}
}

265
src/translate/common/choose_value_in_term.rs Normal file
View File

@ -0,0 +1,265 @@
pub(crate) fn choose_value_in_primitive(term: Box<foliage::Term>,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-> foliage::Formula
{
let variable = foliage::Term::variable(variable_declaration);
foliage::Formula::equal(Box::new(variable), term)
}
pub(crate) fn choose_value_in_term<C>(term: &clingo::ast::Term,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>, context: &C)
-> Result<foliage::Formula, crate::Error>
where
C: crate::translate::common::GetOrCreateFunctionDeclaration
+ crate::translate::common::GetOrCreateVariableDeclaration
+ crate::translate::common::AssignVariableDeclarationDomain
{
match term.term_type()
{
clingo::ast::TermType::Symbol(symbol) => match symbol.symbol_type()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
{
clingo::SymbolType::Number => Ok(choose_value_in_primitive(
Box::new(foliage::Term::integer(symbol.number()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?)),
variable_declaration)),
clingo::SymbolType::Infimum => Ok(choose_value_in_primitive(
Box::new(foliage::Term::infimum()), variable_declaration)),
clingo::SymbolType::Supremum => Ok(choose_value_in_primitive(
Box::new(foliage::Term::supremum()), variable_declaration)),
clingo::SymbolType::String => Ok(choose_value_in_primitive(
Box::new(foliage::Term::string(symbol.string()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
.to_string())),
variable_declaration)),
clingo::SymbolType::Function =>
{
let arguments = symbol.arguments()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?;
// Functions with arguments are represented as clingo::ast::Function by the parser.
// At this point, we only have to handle (0-ary) constants
if !arguments.is_empty()
{
return Err(crate::Error::new_logic("unexpected arguments, expected (0-ary) constant symbol"));
}
let constant_name = symbol.name()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?;
let constant_declaration = context.get_or_create_function_declaration(constant_name, 0);
let function = foliage::Term::function(&constant_declaration, vec![]);
Ok(choose_value_in_primitive(Box::new(function), variable_declaration))
}
},
clingo::ast::TermType::Variable(variable_name) =>
{
let other_variable_declaration = context.get_or_create_variable_declaration(
variable_name);
context.assign_variable_declaration_domain(&other_variable_declaration,
crate::Domain::Program);
let other_variable = foliage::Term::variable(&other_variable_declaration);
Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration))
},
clingo::ast::TermType::BinaryOperation(binary_operation) =>
{
let operator = crate::translate::common::translate_binary_operator(
binary_operation.binary_operator())?;
match operator
{
foliage::BinaryOperator::Add
| foliage::BinaryOperator::Subtract
| foliage::BinaryOperator::Multiply
=>
{
let parameters = (0..2).map(|_|
{
let variable_declaration = std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string()));
context.assign_variable_declaration_domain(&variable_declaration,
crate::Domain::Integer);
variable_declaration
})
.collect::<foliage::VariableDeclarations>();
let parameters = std::rc::Rc::new(parameters);
let parameter_1 = &parameters[0];
let parameter_2 = &parameters[1];
let translated_binary_operation = foliage::Term::binary_operation(operator,
Box::new(foliage::Term::variable(&parameter_1)),
Box::new(foliage::Term::variable(&parameter_2)));
let equals = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(translated_binary_operation));
let choose_value_from_left_argument = choose_value_in_term(
binary_operation.left(), &parameter_1, context)?;
let choose_value_from_right_argument = choose_value_in_term(
binary_operation.right(), &parameter_2, context)?;
let and = foliage::Formula::And(vec![Box::new(equals),
Box::new(choose_value_from_left_argument),
Box::new(choose_value_from_right_argument)]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
foliage::BinaryOperator::Divide
| foliage::BinaryOperator::Modulo
=>
{
let parameters = (0..4).map(|_|
{
let variable_declaration = std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string()));
context.assign_variable_declaration_domain(&variable_declaration,
crate::Domain::Integer);
variable_declaration
})
.collect::<foliage::VariableDeclarations>();
let parameters = std::rc::Rc::new(parameters);
let parameter_i = &parameters[0];
let parameter_j = &parameters[1];
let parameter_q = &parameters[2];
let parameter_r = &parameters[3];
let j_times_q = foliage::Term::multiply(
Box::new(foliage::Term::variable(parameter_j)),
Box::new(foliage::Term::variable(parameter_q)));
let j_times_q_plus_r = foliage::Term::add(Box::new(j_times_q),
Box::new(foliage::Term::variable(parameter_r)));
let i_equals_j_times_q_plus_r = foliage::Formula::equal(
Box::new(foliage::Term::variable(parameter_j)), Box::new(j_times_q_plus_r));
let choose_i_in_t1 = choose_value_in_term(binary_operation.left(), parameter_i,
context)?;
let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), parameter_j,
context)?;
let j_not_equal_to_0 = foliage::Formula::not_equal(
Box::new(foliage::Term::variable(parameter_j)),
Box::new(foliage::Term::integer(0)));
let r_greater_or_equal_to_0 = foliage::Formula::greater_or_equal(
Box::new(foliage::Term::variable(parameter_r)),
Box::new(foliage::Term::integer(0)));
let r_less_than_q = foliage::Formula::less(
Box::new(foliage::Term::variable(parameter_r)),
Box::new(foliage::Term::variable(parameter_q)));
let z_equal_to_q = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(foliage::Term::variable(parameter_q)));
let z_equal_to_r = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(foliage::Term::variable(parameter_r)));
let last_argument = match operator
{
foliage::BinaryOperator::Divide => z_equal_to_q,
foliage::BinaryOperator::Modulo => z_equal_to_r,
_ => return Err(crate::Error::new_logic("unreachable code")),
};
let and = foliage::Formula::and(vec![Box::new(i_equals_j_times_q_plus_r),
Box::new(choose_i_in_t1), Box::new(choose_i_in_t2),
Box::new(j_not_equal_to_0), Box::new(r_greater_or_equal_to_0),
Box::new(r_less_than_q), Box::new(last_argument)]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
foliage::BinaryOperator::Exponentiate =>
Err(crate::Error::new_unsupported_language_feature("exponentiation")),
}
},
clingo::ast::TermType::UnaryOperation(unary_operation) =>
{
match unary_operation.unary_operator()
{
clingo::ast::UnaryOperator::Absolute =>
return Err(crate::Error::new_unsupported_language_feature("absolute value")),
clingo::ast::UnaryOperator::Minus =>
{
let parameter_z_prime = std::rc::Rc::new(foliage::VariableDeclaration::new(
"<anonymous>".to_string()));
context.assign_variable_declaration_domain(&parameter_z_prime,
crate::Domain::Integer);
let negative_z_prime = foliage::Term::negative(Box::new(
foliage::Term::variable(&parameter_z_prime)));
let equals = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(negative_z_prime));
let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(),
&parameter_z_prime, context)?;
let and = foliage::Formula::and(vec![Box::new(equals),
Box::new(choose_z_prime_in_t_prime)]);
let parameters = std::rc::Rc::new(vec![parameter_z_prime]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
_ => Err(crate::Error::new_not_yet_implemented("todo")),
}
},
clingo::ast::TermType::Interval(interval) =>
{
let parameters = (0..3).map(|_|
{
let variable_declaration = std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string()));
context.assign_variable_declaration_domain(&variable_declaration,
crate::Domain::Integer);
variable_declaration
})
.collect::<foliage::VariableDeclarations>();
let parameters = std::rc::Rc::new(parameters);
let parameter_i = &parameters[0];
let parameter_j = &parameters[1];
let parameter_k = &parameters[2];
let choose_i_in_t_1 = choose_value_in_term(interval.left(), parameter_i, context)?;
let choose_j_in_t_2 = choose_value_in_term(interval.right(), parameter_j, context)?;
let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal(
Box::new(foliage::Term::variable(parameter_i)),
Box::new(foliage::Term::variable(parameter_k)));
let k_less_than_or_equal_to_j = foliage::Formula::less_or_equal(
Box::new(foliage::Term::variable(parameter_k)),
Box::new(foliage::Term::variable(parameter_j)));
let z_equals_k = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(foliage::Term::variable(parameter_k)));
let and = foliage::Formula::and(vec![Box::new(choose_i_in_t_1),
Box::new(choose_j_in_t_2), Box::new(i_less_than_or_equal_to_k),
Box::new(k_less_than_or_equal_to_j), Box::new(z_equals_k)]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
clingo::ast::TermType::Function(_) =>
Err(crate::Error::new_unsupported_language_feature("symbolic functions")),
clingo::ast::TermType::Pool(_) =>
Err(crate::Error::new_unsupported_language_feature("pools")),
clingo::ast::TermType::ExternalFunction(_) =>
Err(crate::Error::new_unsupported_language_feature("external functions")),
}
}

201
src/translate/verify_properties.rs
View File

@ -1,193 +1,12 @@
mod context;
mod head_type;
mod translate_body;
use context::*;
use head_type::*;
use translate_body::*;
use crate::translate::common::AssignVariableDeclarationDomain as _;
struct ScopedFormula
{
free_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>,
formula: Box<foliage::Formula>,
}
struct Definitions
{
head_atom_parameters: std::rc::Rc<foliage::VariableDeclarations>,
definitions: Vec<ScopedFormula>,
}
type VariableDeclarationDomains
= std::collections::BTreeMap<std::rc::Rc<foliage::VariableDeclaration>,
crate::translate::common::Domain>;
type VariableDeclarationIDs
= std::collections::BTreeMap::<std::rc::Rc<foliage::VariableDeclaration>, usize>;
struct Context
{
pub definitions: std::cell::RefCell<std::collections::BTreeMap::<std::rc::Rc<foliage::PredicateDeclaration>,
Definitions>>,
pub integrity_constraints: std::cell::RefCell<foliage::Formulas>,
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>,
pub variable_declaration_domains: std::cell::RefCell<VariableDeclarationDomains>,
pub variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
}
impl Context
{
fn new() -> Self
{
Self
{
definitions: std::cell::RefCell::new(std::collections::BTreeMap::<_, _>::new()),
integrity_constraints: std::cell::RefCell::new(vec![]),
function_declarations: std::cell::RefCell::new(foliage::FunctionDeclarations::new()),
predicate_declarations: std::cell::RefCell::new(foliage::PredicateDeclarations::new()),
variable_declaration_stack: std::cell::RefCell::new(foliage::VariableDeclarationStack::new()),
variable_declaration_domains: std::cell::RefCell::new(VariableDeclarationDomains::new()),
variable_declaration_ids: std::cell::RefCell::new(VariableDeclarationIDs::new()),
}
}
}
impl crate::translate::common::GetOrCreateFunctionDeclaration for Context
{
fn get_or_create_function_declaration(&self, name: &str, arity: usize)
-> std::rc::Rc<foliage::FunctionDeclaration>
{
let mut function_declarations = self.function_declarations.borrow_mut();
match function_declarations.iter()
.find(|x| x.name == name && x.arity == arity)
{
Some(value) => std::rc::Rc::clone(value),
None =>
{
let declaration = std::rc::Rc::new(foliage::FunctionDeclaration::new(
name.to_string(), arity));
function_declarations.insert(std::rc::Rc::clone(&declaration));
log::debug!("new function declaration: {}/{}", name, arity);
declaration
},
}
}
}
impl crate::translate::common::GetOrCreatePredicateDeclaration for Context
{
fn get_or_create_predicate_declaration(&self, name: &str, arity: usize)
-> std::rc::Rc<foliage::PredicateDeclaration>
{
let mut predicate_declarations = self.predicate_declarations.borrow_mut();
match predicate_declarations.iter()
.find(|x| x.name == name && x.arity == arity)
{
Some(value) => std::rc::Rc::clone(value),
None =>
{
let declaration = std::rc::Rc::new(foliage::PredicateDeclaration::new(
name.to_string(), arity));
predicate_declarations.insert(std::rc::Rc::clone(&declaration));
log::debug!("new predicate declaration: {}/{}", name, arity);
declaration
},
}
}
}
impl crate::translate::common::GetOrCreateVariableDeclaration for Context
{
fn get_or_create_variable_declaration(&self, name: &str)
-> std::rc::Rc<foliage::VariableDeclaration>
{
let mut variable_declaration_stack = self.variable_declaration_stack.borrow_mut();
// TODO: check correctness
if name == "_"
{
let variable_declaration = std::rc::Rc::new(foliage::VariableDeclaration::new(
"_".to_owned()));
variable_declaration_stack.free_variable_declarations.push(
std::rc::Rc::clone(&variable_declaration));
return variable_declaration;
}
variable_declaration_stack.find_or_create(name)
}
}
impl crate::translate::common::AssignVariableDeclarationDomain for Context
{
fn assign_variable_declaration_domain(&self,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>,
domain: crate::translate::common::Domain)
{
let mut variable_declaration_domains = self.variable_declaration_domains.borrow_mut();
match variable_declaration_domains.get(variable_declaration)
{
Some(current_domain) => assert_eq!(*current_domain, domain,
"inconsistent variable declaration domain"),
None =>
{
variable_declaration_domains
.insert(std::rc::Rc::clone(variable_declaration).into(), domain);
},
}
}
}
impl crate::translate::common::VariableDeclarationDomain for Context
{
fn variable_declaration_domain(&self,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-> Option<crate::translate::common::Domain>
{
let variable_declaration_domains = self.variable_declaration_domains.borrow();
variable_declaration_domains.get(variable_declaration)
.map(|x| *x)
}
}
impl crate::translate::common::VariableDeclarationID for Context
{
fn variable_declaration_id(&self,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-> usize
{
let mut variable_declaration_ids = self.variable_declaration_ids.borrow_mut();
match variable_declaration_ids.get(variable_declaration)
{
Some(id) =>
{
*id
}
None =>
{
let id = variable_declaration_ids.len();
variable_declaration_ids.insert(std::rc::Rc::clone(variable_declaration).into(), id);
id
},
}
}
}
struct StatementHandler
{
context: Context,
@ -284,7 +103,7 @@ where
let completed_definition = foliage::Formula::if_and_only_if(
Box::new(head_predicate), Box::new(or));
let scoped_formula = ScopedFormula
let scoped_formula = crate::ScopedFormula
{
free_variable_declarations: definitions.head_atom_parameters,
formula: Box::new(completed_definition),
@ -301,7 +120,7 @@ where
let variable_declaration = std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string()));
context.assign_variable_declaration_domain(&variable_declaration,
crate::translate::common::Domain::Program);
crate::Domain::Program);
variable_declaration
})
.collect::<Vec<_>>());
@ -315,7 +134,7 @@ where
let not = foliage::Formula::not(Box::new(head_predicate));
let scoped_formula = ScopedFormula
let scoped_formula = crate::ScopedFormula
{
free_variable_declarations: head_atom_parameters,
formula: Box::new(not),
@ -414,7 +233,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
let variable_declaration = std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string()));
context.assign_variable_declaration_domain(&variable_declaration,
crate::translate::common::Domain::Program);
crate::Domain::Program);
variable_declaration
})
.collect());
@ -475,7 +294,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
_ => Box::new(foliage::Formula::and(definition_arguments)),
};
let definition = ScopedFormula
let definition = crate::ScopedFormula
{
free_variable_declarations: std::rc::Rc::new(free_variable_declarations),
formula: definition,
@ -501,7 +320,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
_ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))),
};
let scoped_formula = ScopedFormula
let scoped_formula = crate::ScopedFormula
{
free_variable_declarations: std::rc::Rc::new(free_variable_declarations),
formula: Box::new(formula),
@ -521,7 +340,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
Ok(())
}
fn existential_closure(scoped_formula: ScopedFormula) -> Box<foliage::Formula>
fn existential_closure(scoped_formula: crate::ScopedFormula) -> Box<foliage::Formula>
{
match scoped_formula.free_variable_declarations.is_empty()
{
@ -531,7 +350,7 @@ fn existential_closure(scoped_formula: ScopedFormula) -> Box<foliage::Formula>
}
}
fn universal_closure(scoped_formula: ScopedFormula) -> Box<foliage::Formula>
fn universal_closure(scoped_formula: crate::ScopedFormula) -> Box<foliage::Formula>
{
match scoped_formula.free_variable_declarations.is_empty()
{

4
src/translate/verify_properties/translate_body.rs
View File

@ -23,7 +23,7 @@ where
let variable_declaration = std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string()));
context.assign_variable_declaration_domain(&variable_declaration,
crate::translate::common::Domain::Program);
crate::Domain::Program);
variable_declaration
})
.collect::<foliage::VariableDeclarations>();
@ -109,7 +109,7 @@ where
let variable_declaration = std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string()));
context.assign_variable_declaration_domain(&variable_declaration,
crate::translate::common::Domain::Program);
crate::Domain::Program);
variable_declaration
})
.collect::<foliage::VariableDeclarations>();