// Operators pub enum BinaryOperator { Add, Subtract, Multiply, Divide, Modulo, Exponentiate, } pub enum ComparisonOperator { Greater, Less, LessOrEqual, GreaterOrEqual, NotEqual, Equal, } pub enum UnaryOperator { AbsoluteValue, Negative, } // Primitives #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct FunctionDeclaration { pub name: String, pub arity: usize, } impl FunctionDeclaration { pub fn new(name: String, arity: usize) -> Self { Self { name, arity, } } } pub type FunctionDeclarations = std::collections::BTreeSet>; #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct PredicateDeclaration { pub name: String, pub arity: usize, } impl PredicateDeclaration { pub fn new(name: String, arity: usize) -> Self { Self { name, arity, } } } pub type PredicateDeclarations = std::collections::BTreeSet>; #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct VariableDeclaration { pub name: String, } impl VariableDeclaration { pub fn new(name: String) -> Self { Self { name, } } } pub type VariableDeclarations = Vec>; pub struct VariableDeclarationStack { pub free_variable_declarations: VariableDeclarations, bound_variable_declaration_stack: Vec>, } impl VariableDeclarationStack { pub fn new() -> Self { Self { free_variable_declarations: VariableDeclarations::new(), bound_variable_declaration_stack: vec![], } } pub fn find(&self, variable_name: &str) -> Option> { for variable_declarations in self.bound_variable_declaration_stack.iter().rev() { if let Some(variable_declaration) = variable_declarations.iter().find(|x| x.name == variable_name) { return Some(std::rc::Rc::clone(&variable_declaration)); } } if let Some(variable_declaration) = self.free_variable_declarations.iter().find(|x| x.name == variable_name) { return Some(std::rc::Rc::clone(&variable_declaration)); } None } pub fn find_or_create(&mut self, variable_name: &str) -> std::rc::Rc { if let Some(variable_declaration) = self.find(variable_name) { return variable_declaration; } let variable_declaration = VariableDeclaration { name: variable_name.to_owned(), }; let variable_declaration = std::rc::Rc::new(variable_declaration); self.free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration)); variable_declaration } pub fn push(&mut self, bound_variable_declarations: std::rc::Rc) { self.bound_variable_declaration_stack.push(bound_variable_declarations); } pub fn pop(&mut self) { // TODO: return error instead self.bound_variable_declaration_stack.pop().expect("bound variable is empty, cannot pop last element"); } } // Terms pub struct BinaryOperation { pub operator: BinaryOperator, pub left: Box, pub right: Box, } impl BinaryOperation { pub fn new(operator: BinaryOperator, left: Box, right: Box) -> Self { Self { operator, left, right, } } } pub struct Function { pub declaration: std::rc::Rc, pub arguments: Vec>, } impl Function { pub fn new(declaration: &std::rc::Rc, arguments: Vec>) -> Self { Self { declaration: std::rc::Rc::clone(declaration), arguments, } } } pub enum SpecialInteger { Infimum, Supremum, } pub struct UnaryOperation { pub operator: UnaryOperator, pub argument: Box, } impl UnaryOperation { pub fn new(operator: UnaryOperator, argument: Box) -> Self { Self { operator, argument, } } } pub struct Variable { pub declaration: std::rc::Rc, } impl Variable { pub fn new(declaration: &std::rc::Rc) -> Self { Self { declaration: std::rc::Rc::clone(declaration), } } } // Formulas pub struct Compare { pub operator: ComparisonOperator, pub left: Box, pub right: Box, } impl Compare { pub fn new(operator: ComparisonOperator, left: Box, right: Box) -> Self { Self { operator, left, right, } } } pub struct Exists { pub parameters: std::rc::Rc, pub argument: Box, } impl Exists { pub fn new(parameters: std::rc::Rc, argument: Box) -> Self { Self { parameters, argument, } } } pub struct ForAll { pub parameters: std::rc::Rc, pub argument: Box, } impl ForAll { pub fn new(parameters: std::rc::Rc, argument: Box) -> Self { Self { parameters, argument, } } } pub struct IfAndOnlyIf { pub left: Box, pub right: Box, } impl IfAndOnlyIf { pub fn new(left: Box, right: Box) -> Self { Self { left, right, } } } pub struct Implies { pub antecedent: Box, pub implication: Box, } impl Implies { pub fn new(antecedent: Box, implication: Box) -> Self { Self { antecedent, implication, } } } pub struct Predicate { pub declaration: std::rc::Rc, pub arguments: Vec>, } impl Predicate { pub fn new(declaration: &std::rc::Rc, arguments: Vec>) -> Self { Self { declaration: std::rc::Rc::clone(declaration), arguments, } } } // Variants pub enum Term { BinaryOperation(BinaryOperation), Boolean(bool), Function(Function), Integer(i32), SpecialInteger(SpecialInteger), String(String), UnaryOperation(UnaryOperation), Variable(Variable), } pub type Terms = Vec>; impl Term { pub fn absolute_value(argument: Box) -> Self { Self::unary_operation(UnaryOperator::AbsoluteValue, argument) } pub fn add(left: Box, right: Box) -> Self { Self::binary_operation(BinaryOperator::Add, left, right) } pub fn binary_operation(operator: BinaryOperator, left: Box, right: Box) -> Self { Self::BinaryOperation(BinaryOperation::new(operator, left, right)) } pub fn boolean(value: bool) -> Self { Self::Boolean(value) } pub fn divide(left: Box, right: Box) -> Self { Self::binary_operation(BinaryOperator::Divide, left, right) } pub fn exponentiate(left: Box, right: Box) -> Self { Self::binary_operation(BinaryOperator::Exponentiate, left, right) } pub fn false_() -> Self { Self::boolean(false) } pub fn function(declaration: &std::rc::Rc, arguments: Vec>) -> Self { Self::Function(Function::new(declaration, arguments)) } pub fn infimum() -> Self { Self::special_integer(SpecialInteger::Infimum) } pub fn integer(value: i32) -> Self { Self::Integer(value) } pub fn modulo(left: Box, right: Box) -> Self { Self::binary_operation(BinaryOperator::Modulo, left, right) } pub fn multiply(left: Box, right: Box) -> Self { Self::binary_operation(BinaryOperator::Multiply, left, right) } pub fn negative(argument: Box) -> Self { Self::unary_operation(UnaryOperator::Negative, argument) } pub fn special_integer(value: SpecialInteger) -> Self { Self::SpecialInteger(value) } pub fn string(value: String) -> Self { Self::String(value) } pub fn subtract(left: Box, right: Box) -> Self { Self::binary_operation(BinaryOperator::Subtract, left, right) } pub fn supremum() -> Self { Self::special_integer(SpecialInteger::Supremum) } pub fn true_() -> Self { Self::boolean(true) } pub fn unary_operation(operator: UnaryOperator, argument: Box) -> Self { Self::UnaryOperation(UnaryOperation::new(operator, argument)) } pub fn variable(declaration: &std::rc::Rc) -> Self { Self::Variable(Variable::new(declaration)) } } pub enum Formula { And(Formulas), Boolean(bool), Compare(Compare), Exists(Exists), ForAll(ForAll), IfAndOnlyIf(IfAndOnlyIf), Implies(Implies), Not(Box), Or(Formulas), Predicate(Predicate), } pub type Formulas = Vec>; impl Formula { pub fn and(arguments: Formulas) -> Self { assert!(!arguments.is_empty()); Self::And(arguments) } pub fn boolean(value: bool) -> Self { Self::Boolean(value) } pub fn compare(operator: ComparisonOperator, left: Box, right: Box) -> Self { Self::Compare(Compare::new(operator, left, right)) } pub fn exists(parameters: std::rc::Rc, argument: Box) -> Self { assert!(!parameters.is_empty()); Self::Exists(Exists::new(parameters, argument)) } pub fn equal(left: Box, right: Box) -> Self { Self::compare(ComparisonOperator::Equal, left, right) } pub fn false_() -> Self { Self::boolean(false) } pub fn for_all(parameters: std::rc::Rc, argument: Box) -> Self { assert!(!parameters.is_empty()); Self::ForAll(ForAll::new(parameters, argument)) } pub fn greater(left: Box, right: Box) -> Self { Self::compare(ComparisonOperator::Greater, left, right) } pub fn greater_or_equal(left: Box, right: Box) -> Self { Self::compare(ComparisonOperator::GreaterOrEqual, left, right) } pub fn if_and_only_if(left: Box, right: Box) -> Self { Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right)) } pub fn implies(antecedent: Box, consequent: Box) -> Self { Self::Implies(Implies::new(antecedent, consequent)) } pub fn less(left: Box, right: Box) -> Self { Self::compare(ComparisonOperator::Less, left, right) } pub fn less_or_equal(left: Box, right: Box) -> Self { Self::compare(ComparisonOperator::LessOrEqual, left, right) } pub fn not(argument: Box) -> Self { Self::Not(argument) } pub fn not_equal(left: Box, right: Box) -> Self { Self::compare(ComparisonOperator::NotEqual, left, right) } pub fn or(arguments: Formulas) -> Self { assert!(!arguments.is_empty()); Self::Or(arguments) } pub fn predicate(declaration: &std::rc::Rc, arguments: Vec>) -> Self { Self::Predicate(Predicate::new(declaration, arguments)) } pub fn true_() -> Self { Self::boolean(true) } }