// Operators #[derive(Clone, Copy, Eq, PartialEq)] pub enum BinaryOperator { Add, Subtract, Multiply, Divide, Modulo, Exponentiate, } #[derive(Clone, Copy, Eq, PartialEq)] pub enum ComparisonOperator { Greater, Less, LessOrEqual, GreaterOrEqual, NotEqual, Equal, } #[derive(Clone, Copy, Eq, PartialEq)] pub enum UnaryOperator { AbsoluteValue, Negative, } // ImplicationDirection #[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)] pub enum ImplicationDirection { LeftToRight, RightToLeft, } // 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>; pub struct VariableDeclaration { pub name: String, } impl std::cmp::PartialEq for VariableDeclaration { #[inline(always)] fn eq(&self, other: &VariableDeclaration) -> bool { let l = self as *const VariableDeclaration; let r = other as *const VariableDeclaration; l.eq(&r) } } impl std::cmp::Eq for VariableDeclaration { } impl std::cmp::PartialOrd for VariableDeclaration { #[inline(always)] fn partial_cmp(&self, other: &VariableDeclaration) -> Option { let l = self as *const VariableDeclaration; let r = other as *const VariableDeclaration; l.partial_cmp(&r) } } impl std::cmp::Ord for VariableDeclaration { #[inline(always)] fn cmp(&self, other: &VariableDeclaration) -> std::cmp::Ordering { let l = self as *const VariableDeclaration; let r = other as *const VariableDeclaration; l.cmp(&r) } } impl VariableDeclaration { pub fn new(name: String) -> Self { Self { name, } } } pub type VariableDeclarations = Vec>; // 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 { assert_eq!(declaration.arity, arguments.len(), "function has a different number of arguments then declared"); Self { declaration: std::rc::Rc::clone(declaration), arguments, } } } #[derive(Clone, Copy, Eq, PartialEq)] 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 direction: ImplicationDirection, pub antecedent: Box, pub implication: Box, } impl Implies { pub fn new(direction: ImplicationDirection, antecedent: Box, implication: Box) -> Self { Self { direction, 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 { assert_eq!(declaration.arity, arguments.len(), "predicate has a different number of arguments then declared"); 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(direction: ImplicationDirection, antecedent: Box, consequent: Box) -> Self { Self::Implies(Implies::new(direction, 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) } }