Compare commits

...

64 Commits

Author SHA1 Message Date
Patrick Lühne 79d6643598
Remove unneeded trait methods 2 years ago
Patrick Lühne c6f2cdc6e1
Improve public interface 2 years ago
Patrick Lühne 66b5499005
Experimental refactoring 2 years ago
Patrick Lühne 742379934f
Remove unused trait implementations 3 years ago
Patrick Lühne a0fefe9b6a
Improve interface for declaration types 3 years ago
Patrick Lühne 036544d3c7
Minor refactoring 3 years ago
Patrick Lühne c7d79e7b07
Make inner types customizable 3 years ago
Patrick Lühne 170cde6a82
Fix parsing right-to-left implication 3 years ago
Patrick Lühne 0216f90929
Add support for comments 3 years ago
Patrick Lühne ae46634d67
Rename ClosedFormula to OpenFormula 3 years ago
Patrick Lühne 75e97a5c07
Use log crate rather than println 3 years ago
Patrick Lühne dd208ffeeb
Expose number parser 3 years ago
Patrick Lühne bdd5d0e583
Expose identifier parser 3 years ago
Patrick Lühne 82e98e5ec0
Look up functions 3 years ago
Patrick Lühne 1b4c400bfb
Look up variables 3 years ago
Patrick Lühne f8918628fa
Pass declarations to term parser 3 years ago
Patrick Lühne 555f983285
Look up predicates 3 years ago
Patrick Lühne 56885dc290
Pass declarations to formula parser 3 years ago
Patrick Lühne 30c28c2bc4
Fix unit tests 3 years ago
Patrick Lühne 8d474fa489
Finish dirty first pass over parser 3 years ago
Patrick Lühne 66ac57c5b8
Work in progress 3 years ago
Patrick Lühne 0fb2be4897
Minor refactoring 3 years ago
Patrick Lühne 80aafb2359
Implement right-to-left implication 3 years ago
Patrick Lühne a2268ab85b
Minor renaming 3 years ago
Patrick Lühne 451b887019
Minor renaming 3 years ago
Patrick Lühne a12acae633
Refactoring 3 years ago
Patrick Lühne 35937d7930
Clean-up 3 years ago
Patrick Lühne 31805fa9d8
Clean-up 3 years ago
Patrick Lühne a6edd2e9cc
Clean-up 3 years ago
Patrick Lühne 834194d40a
Work in progress 3 years ago
Patrick Lühne 15d0d2b76c
Work in progress 3 years ago
Patrick Lühne ff17c60cd1
Start rewriting parser 3 years ago
Patrick Lühne b516396977
Fix parsing nested quantified formulas 3 years ago
Patrick Lühne 987e02f478
Allow period character as word boundary 3 years ago
Patrick Lühne ba385868cb
Fix parsing precedence of left implication vs. less-than comparison 3 years ago
Patrick Lühne 04e2d61583
Fix order of operators 3 years ago
Patrick Lühne 395c029ca9
Expose function/predicate name parser 3 years ago
Patrick Lühne c927fe4628
Expose Declarations type 3 years ago
Patrick Lühne 2b3add562f
Update nom to 6.0.0-alpha1 3 years ago
Patrick Lühne 0d5971cad7
Retrieve declarations using traits and not objects 3 years ago
Patrick Lühne 0e78e4ea57
Minor refactoring 3 years ago
Patrick Lühne 63c1931e30
Expose functions to access free and manipulate variable declarations 3 years ago
Patrick Lühne 8a9a7b9132
Remove unneeded indirection 3 years ago
Patrick Lühne abbc047dda
Replace variable declaration stack with recursive layer implementation 3 years ago
Patrick Lühne 62b9e2da04
Make variable declaration stack safer with guards 3 years ago
Patrick Lühne fa6f27beb4
Start reimplementing parser 3 years ago
Patrick Lühne 1e34d726e1
Export formatting implementation functionality 3 years ago
Patrick Lühne 1e610a77fe
Make variable formatting customizable 3 years ago
Patrick Lühne 9216bbbe31
Rename formatter variables 3 years ago
Patrick Lühne d67e530fec
Rewrite formula and term formatting 3 years ago
Patrick Lühne 8e32b58c99
Remove unneeded indirection from vector types 3 years ago
Patrick Lühne 2fa592576b
Take reference-counted arguments by value 3 years ago
Patrick Lühne 7d22e47ba1
Represent quantified formulas consistently 3 years ago
Patrick Lühne 7566fdaa29
Support n-ary biconditionals 3 years ago
Patrick Lühne 855fd9abcf
Support right-to-left implications 3 years ago
Patrick Lühne 5bbb09eef8
Split formatting utils into separate files 3 years ago
Patrick Lühne fd6ba4a005
Test crate with GitHub Actions 3 years ago
Patrick Lühne 153f77621e
Fix precedence of absolute value operation 3 years ago
Patrick Lühne 551c35ed75
Fix formatting of binary operations 3 years ago
Patrick Lühne 549f127729
Derive simple enums from basic traits 3 years ago
Patrick Lühne a304ec9a75
Fix output of Booleans in formulas 3 years ago
Patrick Lühne a82b4080c8
Fix function formatting 3 years ago
Patrick Lühne 90f7be2f33
Minor refactoring for clarity 3 years ago
Patrick Lühne a127a053b2
Support formatting special integers separately 3 years ago
  1. 32
      .github/workflows/main.yml
  2. 3
      Cargo.toml
  3. 340
      src/ast.rs
  4. 85
      src/flavor.rs
  5. 433
      src/format.rs
  6. 1275
      src/format/formulas.rs
  7. 1090
      src/format/terms.rs
  8. 9
      src/lib.rs
  9. 142
      src/parse.rs
  10. 182
      src/parse/error.rs
  11. 564
      src/parse/formulas.rs
  12. 651
      src/parse/terms.rs
  13. 641
      src/parse/tokens.rs
  14. 102
      src/utils.rs

@ -0,0 +1,32 @@
name: Rust
on:
push:
branches: [master]
pull_request:
branches: [master]
jobs:
test:
name: Test
runs-on: ubuntu-latest
strategy:
matrix:
build: [stable, beta, nightly]
include:
- build: stable
rust: stable
- build: beta
rust: beta
- build: nightly
rust: nightly
steps:
- uses: actions/checkout@v2
- name: Install Rust (rustup)
run: rustup update ${{ matrix.rust }} --no-self-update && rustup default ${{ matrix.rust }}
shell: bash
- name: Build
run: cargo build --verbose
- name: Run tests
run: cargo test --verbose

@ -11,3 +11,6 @@ keywords = ["logic"]
categories = ["data-structures", "science"]
license = "MIT"
edition = "2018"
[dependencies]
log = "0.4"

@ -1,5 +1,8 @@
use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _};
// Operators
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum BinaryOperator
{
Add,
@ -10,6 +13,7 @@ pub enum BinaryOperator
Exponentiate,
}
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum ComparisonOperator
{
Greater,
@ -20,12 +24,22 @@ pub enum ComparisonOperator
Equal,
}
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
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)]
@ -47,7 +61,8 @@ impl FunctionDeclaration
}
}
pub type FunctionDeclarations = std::collections::BTreeSet<std::rc::Rc<FunctionDeclaration>>;
pub type FunctionDeclarations<F> =
std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::FunctionDeclaration>>;
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct PredicateDeclaration
@ -68,7 +83,8 @@ impl PredicateDeclaration
}
}
pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>;
pub type PredicateDeclarations<F> =
std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::PredicateDeclaration>>;
pub struct VariableDeclaration
{
@ -78,10 +94,10 @@ pub struct VariableDeclaration
impl std::cmp::PartialEq for VariableDeclaration
{
#[inline(always)]
fn eq(&self, other: &VariableDeclaration) -> bool
fn eq(&self, other: &Self) -> bool
{
let l = self as *const VariableDeclaration;
let r = other as *const VariableDeclaration;
let l = self as *const Self;
let r = other as *const Self;
l.eq(&r)
}
@ -115,6 +131,17 @@ impl std::cmp::Ord for VariableDeclaration
}
}
impl std::hash::Hash for VariableDeclaration
{
#[inline(always)]
fn hash<H: std::hash::Hasher>(&self, state: &mut H)
{
let p = self as *const VariableDeclaration;
p.hash(state);
}
}
impl VariableDeclaration
{
pub fn new(name: String) -> Self
@ -126,20 +153,26 @@ impl VariableDeclaration
}
}
pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
pub type VariableDeclarations<F> =
Vec<std::rc::Rc<<F as crate::flavor::Flavor>::VariableDeclaration>>;
// Terms
pub struct BinaryOperation
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct BinaryOperation<F>
where
F: crate::flavor::Flavor,
{
pub operator: BinaryOperator,
pub left: Box<Term>,
pub right: Box<Term>,
pub left: Box<Term<F>>,
pub right: Box<Term<F>>,
}
impl BinaryOperation
impl<F> BinaryOperation<F>
where
F: crate::flavor::Flavor,
{
pub fn new(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
pub fn new(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self
{
@ -150,42 +183,53 @@ impl BinaryOperation
}
}
pub struct Function
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Function<F>
where
F: crate::flavor::Flavor,
{
pub declaration: std::rc::Rc<FunctionDeclaration>,
pub arguments: Vec<Box<Term>>,
pub declaration: std::rc::Rc<F::FunctionDeclaration>,
pub arguments: Terms<F>,
}
impl Function
impl<F> Function<F>
where
F: crate::flavor::Flavor,
{
pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
pub fn new(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> Self
{
assert_eq!(declaration.arity, arguments.len(),
"function has a different number of arguments then declared");
assert_eq!(declaration.arity(), arguments.len(),
"function has a different number of arguments than declared");
Self
{
declaration: std::rc::Rc::clone(declaration),
declaration,
arguments,
}
}
}
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum SpecialInteger
{
Infimum,
Supremum,
}
pub struct UnaryOperation
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct UnaryOperation<F>
where
F: crate::flavor::Flavor,
{
pub operator: UnaryOperator,
pub argument: Box<Term>,
pub argument: Box<Term<F>>,
}
impl UnaryOperation
impl<F> UnaryOperation<F>
where
F: crate::flavor::Flavor,
{
pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self
pub fn new(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
{
Self
{
@ -195,34 +239,44 @@ impl UnaryOperation
}
}
pub struct Variable
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Variable<F>
where
F: crate::flavor::Flavor,
{
pub declaration: std::rc::Rc<VariableDeclaration>,
pub declaration: std::rc::Rc<F::VariableDeclaration>,
}
impl Variable
impl<F> Variable<F>
where
F: crate::flavor::Flavor,
{
pub fn new(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
pub fn new(declaration: std::rc::Rc<F::VariableDeclaration>) -> Self
{
Self
{
declaration: std::rc::Rc::clone(declaration),
declaration,
}
}
}
// Formulas
pub struct Compare
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Compare<F>
where
F: crate::flavor::Flavor,
{
pub operator: ComparisonOperator,
pub left: Box<Term>,
pub right: Box<Term>,
pub left: Box<Term<F>>,
pub right: Box<Term<F>>,
}
impl Compare
impl<F> Compare<F>
where
F: crate::flavor::Flavor,
{
pub fn new(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
pub fn new(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self
{
@ -233,33 +287,20 @@ impl Compare
}
}
pub struct Exists
{
pub parameters: std::rc::Rc<VariableDeclarations>,
pub argument: Box<Formula>,
}
impl Exists
{
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
{
Self
{
parameters,
argument,
}
}
}
pub struct ForAll
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct QuantifiedFormula<F>
where
F: crate::flavor::Flavor,
{
pub parameters: std::rc::Rc<VariableDeclarations>,
pub argument: Box<Formula>,
pub parameters: std::rc::Rc<VariableDeclarations<F>>,
pub argument: Box<Formula<F>>,
}
impl ForAll
impl<F> QuantifiedFormula<F>
where
F: crate::flavor::Flavor,
{
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
pub fn new(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
{
Self
{
@ -269,58 +310,54 @@ impl ForAll
}
}
pub struct IfAndOnlyIf
{
pub left: Box<Formula>,
pub right: Box<Formula>,
}
impl IfAndOnlyIf
{
pub fn new(left: Box<Formula>, right: Box<Formula>) -> Self
{
Self
{
left,
right,
}
}
}
pub struct Implies
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Implies<F>
where
F: crate::flavor::Flavor,
{
pub antecedent: Box<Formula>,
pub implication: Box<Formula>,
pub direction: ImplicationDirection,
pub antecedent: Box<Formula<F>>,
pub implication: Box<Formula<F>>,
}
impl Implies
impl<F> Implies<F>
where
F: crate::flavor::Flavor,
{
pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
pub fn new(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
implication: Box<Formula<F>>)
-> Self
{
Self
{
direction,
antecedent,
implication,
}
}
}
pub struct Predicate
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Predicate<F>
where
F: crate::flavor::Flavor,
{
pub declaration: std::rc::Rc<PredicateDeclaration>,
pub arguments: Vec<Box<Term>>,
pub declaration: std::rc::Rc<F::PredicateDeclaration>,
pub arguments: Terms<F>,
}
impl Predicate
impl<F> Predicate<F>
where
F: crate::flavor::Flavor,
{
pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
pub fn new(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
{
assert_eq!(declaration.arity, arguments.len(),
"predicate has a different number of arguments then declared");
assert_eq!(declaration.arity(), arguments.len(),
"predicate has a different number of arguments than declared");
Self
{
declaration: std::rc::Rc::clone(declaration),
declaration,
arguments,
}
}
@ -328,33 +365,38 @@ impl Predicate
// Variants
pub enum Term
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum Term<F>
where
F: crate::flavor::Flavor,
{
BinaryOperation(BinaryOperation),
BinaryOperation(BinaryOperation<F>),
Boolean(bool),
Function(Function),
Function(Function<F>),
Integer(i32),
SpecialInteger(SpecialInteger),
String(String),
UnaryOperation(UnaryOperation),
Variable(Variable),
UnaryOperation(UnaryOperation<F>),
Variable(Variable<F>),
}
pub type Terms = Vec<Box<Term>>;
pub type Terms<F> = Vec<Term<F>>;
impl Term
impl<F> Term<F>
where
F: crate::flavor::Flavor,
{
pub fn absolute_value(argument: Box<Term>) -> Self
pub fn absolute_value(argument: Box<Term<F>>) -> Self
{
Self::unary_operation(UnaryOperator::AbsoluteValue, argument)
}
pub fn add(left: Box<Term>, right: Box<Term>) -> Self
pub fn add(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Add, left, right)
}
pub fn binary_operation(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
pub fn binary_operation(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::BinaryOperation(BinaryOperation::new(operator, left, right))
}
@ -364,12 +406,12 @@ impl Term
Self::Boolean(value)
}
pub fn divide(left: Box<Term>, right: Box<Term>) -> Self
pub fn divide(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Divide, left, right)
}
pub fn exponentiate(left: Box<Term>, right: Box<Term>) -> Self
pub fn exponentiate(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Exponentiate, left, right)
}
@ -379,8 +421,7 @@ impl Term
Self::boolean(false)
}
pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
-> Self
pub fn function(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> Self
{
Self::Function(Function::new(declaration, arguments))
}
@ -395,17 +436,17 @@ impl Term
Self::Integer(value)
}
pub fn modulo(left: Box<Term>, right: Box<Term>) -> Self
pub fn modulo(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Modulo, left, right)
}
pub fn multiply(left: Box<Term>, right: Box<Term>) -> Self
pub fn multiply(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Multiply, left, right)
}
pub fn negative(argument: Box<Term>) -> Self
pub fn negative(argument: Box<Term<F>>) -> Self
{
Self::unary_operation(UnaryOperator::Negative, argument)
}
@ -420,7 +461,7 @@ impl Term
Self::String(value)
}
pub fn subtract(left: Box<Term>, right: Box<Term>) -> Self
pub fn subtract(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Subtract, left, right)
}
@ -435,39 +476,42 @@ impl Term
Self::boolean(true)
}
pub fn unary_operation(operator: UnaryOperator, argument: Box<Term>) -> Self
pub fn unary_operation(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
{
Self::UnaryOperation(UnaryOperation::new(operator, argument))
}
pub fn variable(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
pub fn variable(declaration: std::rc::Rc<F::VariableDeclaration>) -> Self
{
Self::Variable(Variable::new(declaration))
}
}
pub enum Formula
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum Formula<F>
where
F: crate::flavor::Flavor,
{
And(Formulas),
And(Formulas<F>),
Boolean(bool),
Compare(Compare),
Exists(Exists),
ForAll(ForAll),
IfAndOnlyIf(IfAndOnlyIf),
Implies(Implies),
Not(Box<Formula>),
Or(Formulas),
Predicate(Predicate),
Compare(Compare<F>),
Exists(QuantifiedFormula<F>),
ForAll(QuantifiedFormula<F>),
IfAndOnlyIf(Formulas<F>),
Implies(Implies<F>),
Not(Box<Formula<F>>),
Or(Formulas<F>),
Predicate(Predicate<F>),
}
pub type Formulas = Vec<Box<Formula>>;
pub type Formulas<F> = Vec<Formula<F>>;
impl Formula
impl<F> Formula<F>
where
F: crate::flavor::Flavor,
{
pub fn and(arguments: Formulas) -> Self
pub fn and(arguments: Formulas<F>) -> Self
{
assert!(!arguments.is_empty());
Self::And(arguments)
}
@ -476,19 +520,17 @@ impl Formula
Self::Boolean(value)
}
pub fn compare(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
pub fn compare(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::Compare(Compare::new(operator, left, right))
}
pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
pub fn exists(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
{
assert!(!parameters.is_empty());
Self::Exists(Exists::new(parameters, argument))
Self::Exists(QuantifiedFormula::new(parameters, argument))
}
pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
pub fn equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::Equal, left, right)
}
@ -498,62 +540,58 @@ impl Formula
Self::boolean(false)
}
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
{
assert!(!parameters.is_empty());
Self::ForAll(ForAll::new(parameters, argument))
Self::ForAll(QuantifiedFormula::new(parameters, argument))
}
pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
pub fn greater(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::Greater, left, right)
}
pub fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Self
pub fn greater_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
}
pub fn if_and_only_if(left: Box<Formula>, right: Box<Formula>) -> Self
pub fn if_and_only_if(arguments: Formulas<F>) -> Self
{
Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
Self::IfAndOnlyIf(arguments)
}
pub fn implies(antecedent: Box<Formula>, consequent: Box<Formula>) -> Self
pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
consequent: Box<Formula<F>>) -> Self
{
Self::Implies(Implies::new(antecedent, consequent))
Self::Implies(Implies::new(direction, antecedent, consequent))
}
pub fn less(left: Box<Term>, right: Box<Term>) -> Self
pub fn less(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::Less, left, right)
}
pub fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Self
pub fn less_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::LessOrEqual, left, right)
}
pub fn not(argument: Box<Formula>) -> Self
pub fn not(argument: Box<Formula<F>>) -> Self
{
Self::Not(argument)
}
pub fn not_equal(left: Box<Term>, right: Box<Term>) -> Self
pub fn not_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::NotEqual, left, right)
}
pub fn or(arguments: Formulas) -> Self
pub fn or(arguments: Formulas<F>) -> Self
{
assert!(!arguments.is_empty());
Self::Or(arguments)
}
pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
-> Self
pub fn predicate(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
{
Self::Predicate(Predicate::new(declaration, arguments))
}
@ -563,3 +601,11 @@ impl Formula
Self::boolean(true)
}
}
pub struct OpenFormula<F>
where
F: crate::flavor::Flavor,
{
pub free_variable_declarations: std::rc::Rc<VariableDeclarations<F>>,
pub formula: Formula<F>,
}

@ -0,0 +1,85 @@
pub trait FunctionDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
fn arity(&self) -> usize;
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
}
impl FunctionDeclaration for crate::FunctionDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", self.name)
}
fn arity(&self) -> usize
{
self.arity
}
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
{
self.name == other_name && self.arity == other_arity
}
}
pub trait PredicateDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
fn arity(&self) -> usize;
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
}
impl PredicateDeclaration for crate::PredicateDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", self.name)
}
fn arity(&self) -> usize
{
self.arity
}
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
{
self.name == other_name && self.arity == other_arity
}
}
pub trait VariableDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
fn matches_name(&self, other_name: &str) -> bool;
}
impl VariableDeclaration for crate::VariableDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", self.name)
}
fn matches_name(&self, other_name: &str) -> bool
{
self.name == other_name
}
}
pub trait Flavor
{
type FunctionDeclaration: FunctionDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
type PredicateDeclaration:
PredicateDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
type VariableDeclaration: VariableDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
}
pub struct DefaultFlavor;
impl Flavor for DefaultFlavor
{
type FunctionDeclaration = crate::FunctionDeclaration;
type PredicateDeclaration = crate::PredicateDeclaration;
type VariableDeclaration = crate::VariableDeclaration;
}

@ -1,431 +1,2 @@
trait Precedence
{
fn precedence(&self) -> i32;
}
impl Precedence for crate::Term
{
fn precedence(&self) -> i32
{
match &self
{
Self::Boolean(_)
| Self::Function(_)
| Self::SpecialInteger(_)
| Self::Integer(_)
| Self::String(_)
| Self::Variable(_)
=> 0,
Self::UnaryOperation(
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
=> 1,
Self::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
=> 2,
Self::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
| Self::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
| Self::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
=> 3,
Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, ..})
| Self::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
=> 4,
Self::UnaryOperation(
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
=> 5,
}
}
}
impl Precedence for crate::Formula
{
fn precedence(&self) -> i32
{
match &self
{
Self::Predicate(_)
| Self::Boolean(_)
| Self::Compare(_)
=> 0,
Self::Exists(_)
| Self::ForAll(_)
=> 1,
Self::Not(_)
=> 2,
Self::And(_)
=> 3,
Self::Or(_)
=> 4,
Self::Implies(_)
=> 5,
Self::IfAndOnlyIf(_)
=> 6,
}
}
}
impl std::fmt::Debug for crate::FunctionDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{}/{}", &self.name, self.arity)
}
}
impl std::fmt::Display for crate::FunctionDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", &self)
}
}
impl std::fmt::Debug for crate::PredicateDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{}/{}", &self.name, self.arity)
}
}
impl std::fmt::Display for crate::PredicateDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", &self)
}
}
impl std::fmt::Debug for crate::VariableDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{}", &self.name)
}
}
impl std::fmt::Display for crate::VariableDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", &self)
}
}
struct TermDisplay<'term>
{
parent_precedence: Option<i32>,
term: &'term crate::Term,
}
fn display_term(term: &crate::Term, parent_precedence: Option<i32>) -> TermDisplay
{
TermDisplay
{
parent_precedence,
term,
}
}
impl<'term> std::fmt::Debug for TermDisplay<'term>
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
let precedence = self.term.precedence();
let requires_parentheses = match self.parent_precedence
{
Some(parent_precedence) => precedence > parent_precedence,
None => false,
};
let precedence = Some(precedence);
if requires_parentheses
{
write!(format, "(")?;
}
match &self.term
{
crate::Term::Boolean(true) => write!(format, "true"),
crate::Term::Boolean(false) => write!(format, "false"),
crate::Term::SpecialInteger(crate::SpecialInteger::Infimum) => write!(format, "#inf"),
crate::Term::SpecialInteger(crate::SpecialInteger::Supremum) => write!(format, "#sup"),
crate::Term::Integer(value) => write!(format, "{}", value),
crate::Term::String(value) => write!(format, "\"{}\"", value),
crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
crate::Term::Function(function) =>
{
write!(format, "{}", function.declaration.name)?;
assert!(function.declaration.arity == function.arguments.len(),
"number of function arguments differs from declaration (expected {}, got {})",
function.declaration.arity, function.arguments.len());
if function.arguments.len() > 0
{
write!(format, "{}(", function.declaration.name)?;
let mut separator = "";
for argument in &function.arguments
{
write!(format, "{}{:?}", separator, display_term(&argument, None))?;
separator = ", ";
}
write!(format, ")")?;
}
Ok(())
},
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
=> write!(format, "{:?} + {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
=> write!(format, "{:?} - {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
=> write!(format, "{:?} * {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
=> write!(format, "{:?} / {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
=> write!(format, "{:?} % {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
=> write!(format, "{:?} ** {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::UnaryOperation(
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
=> write!(format, "-{:?}", display_term(argument, precedence)),
crate::Term::UnaryOperation(
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
=> write!(format, "|{:?}|", display_term(argument, precedence)),
}?;
if requires_parentheses
{
write!(format, ")")?;
}
Ok(())
}
}
impl<'term> std::fmt::Display for TermDisplay<'term>
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", self)
}
}
struct FormulaDisplay<'formula>
{
parent_precedence: Option<i32>,
formula: &'formula crate::Formula,
}
fn display_formula(formula: &crate::Formula, parent_precedence: Option<i32>) -> FormulaDisplay
{
FormulaDisplay
{
parent_precedence,
formula,
}
}
impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
let precedence = self.formula.precedence();
let requires_parentheses = match self.parent_precedence
{
Some(parent_precedence) => precedence > parent_precedence,
None => false,
};
let precedence = Some(precedence);
if requires_parentheses
{
write!(format, "(")?;
}
match &self.formula
{
crate::Formula::Exists(exists) =>
{
assert!(!exists.parameters.is_empty());
write!(format, "exists")?;
let mut separator = " ";
for parameter in exists.parameters.iter()
{
write!(format, "{}{:?}", separator, parameter)?;
separator = ", "
}