Compare commits
No commits in common. "master" and "pre-0.1.0" have entirely different histories.
2
.gitignore
vendored
2
.gitignore
vendored
@ -1,3 +1,3 @@
|
||||
/Cargo.lock
|
||||
/target
|
||||
**/*.rs.bk
|
||||
Cargo.lock
|
||||
|
||||
11
Cargo.toml
11
Cargo.toml
@ -2,12 +2,7 @@
|
||||
name = "foliage"
|
||||
version = "0.1.0"
|
||||
authors = ["Patrick Lühne <patrick@luehne.de>"]
|
||||
description = "Abstract syntax tree for first-order logic with integer arithmetics"
|
||||
documentation = "https://github.com/potassco/foliage"
|
||||
homepage = "https://github.com/potassco/foliage"
|
||||
repository = "https://github.com/potassco/foliage"
|
||||
readme = "README.md"
|
||||
keywords = ["logic"]
|
||||
categories = ["data-structures", "science"]
|
||||
license = "MIT"
|
||||
edition = "2018"
|
||||
|
||||
[dependencies]
|
||||
nom = "5.0"
|
||||
|
||||
21
LICENSE.md
21
LICENSE.md
@ -1,21 +0,0 @@
|
||||
# The MIT License (MIT)
|
||||
|
||||
Copyright © 2020 Patrick Lühne
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
of this software and associated documentation files (the "Software"), to deal
|
||||
in the Software without restriction, including without limitation the rights
|
||||
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all
|
||||
copies or substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
|
||||
SOFTWARE.
|
||||
26
README.md
26
README.md
@ -1,26 +0,0 @@
|
||||
# foliage [](https://crates.io/crates/foliage)
|
||||
|
||||
> First-order logic with integer arithmetics in Rust
|
||||
|
||||
This Rust crate provides an abstract syntax tree for first-order formulas with integer arithmetics.
|
||||
|
||||
## Supported Formulas
|
||||
|
||||
- Booleans values (`true` and `false`)
|
||||
- predicates
|
||||
- negated formulas
|
||||
- comparisons of terms (<, ≤, >, ≥, =, ≠)
|
||||
- implications and biconditionals
|
||||
- conjunctions and disjunctions of formulas
|
||||
- existentially and universally quantified formulas
|
||||
|
||||
## Supported Terms
|
||||
|
||||
- Boolean values (`true` and `false`)
|
||||
- integers
|
||||
- strings
|
||||
- special integers (infimum and supremum)
|
||||
- symbolic functions
|
||||
- variables
|
||||
- binary operations (addition, subtraction, multiplication, division, modulo, exponentiation)
|
||||
- unary operations (absolute value, numeric negation)
|
||||
20
benches/test.rs
Normal file
20
benches/test.rs
Normal file
@ -0,0 +1,20 @@
|
||||
#![feature(test)]
|
||||
|
||||
extern crate test;
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests
|
||||
{
|
||||
#[bench]
|
||||
fn anthem_example_2(b: &mut test::Bencher)
|
||||
{
|
||||
let formulas = "forall XV1 (p(XV1) <-> (exists XU1 (exists X1, X2 (X1 = XU1 and exists N1, N2, N3 (N1 = 0 and N2 = n and N1 <= N3 and N3 <= N2 and X2 = N3) and X1 = X2) and exists X3, X4 (exists N4, N5 (X3 = (N4 * N5) and N4 = XU1 and N5 = XU1) and X4 = n and X3 <= X4) and XV1 = XU1)))
|
||||
forall XV2 (q(XV2) <-> (exists XU2 (exists X5 (X5 = XU2 and p(X5)) and exists X6 (exists N6, N7 (X6 = (N6 + N7) and N6 = XU2 and N7 = 1) and not p(X6)) and XV2 = XU2)))";
|
||||
|
||||
b.iter(||
|
||||
{
|
||||
let (i, _) = foliage::formulas(formulas).unwrap();
|
||||
assert_eq!(i, "");
|
||||
});
|
||||
}
|
||||
}
|
||||
26
examples/test.rs
Normal file
26
examples/test.rs
Normal file
@ -0,0 +1,26 @@
|
||||
fn main() -> Result<(), Box<dyn std::error::Error>>
|
||||
{
|
||||
let formulas = "forall XV1 (p(XV1) <-> (exists XU1 (exists X1, X2 (X1 = XU1 and exists N1, N2, N3 (N1 = 0 and N2 = n and N1 <= N3 and N3 <= N2 and X2 = N3) and X1 = X2) and exists X3, X4 (exists N4, N5 (X3 = (N4 * N5) and N4 = XU1 and N5 = XU1) and X4 = n and X3 <= X4) and XV1 = XU1)))
|
||||
forall XV2 (q(XV2) <-> (exists XU2 (exists X5 (X5 = XU2 and p(X5)) and exists X6 (exists N6, N7 (X6 = (N6 + N7) and N6 = XU2 and N7 = 1) and not p(X6)) and XV2 = XU2)))";
|
||||
|
||||
let (i, formulas) = foliage::formulas(formulas).unwrap();
|
||||
assert_eq!(i, "");
|
||||
|
||||
for formula in formulas
|
||||
{
|
||||
println!("{}", formula);
|
||||
}
|
||||
|
||||
let formulas = "forall XV1 (p(XV1) <-> exists XU1 (exists X1, X2 (X1 = XU1 and exists N1, N2, N3 (N1 = 0 and N2 = n and N1 <= N3 and N3 <= N2 and X2 = N3) and X1 = X2) and exists X3, X4 (exists N4, N5 (X3 = N4 * N5 and N4 = XU1 and N5 = XU1) and X4 = n and X3 <= X4) and XV1 = XU1))
|
||||
forall XV2 (q(XV2) <-> exists XU2 (exists X5 (X5 = XU2 and p(X5)) and exists X6 (exists N6, N7 (X6 = N6 + N7 and N6 = XU2 and N7 = 1) and not p(X6)) and XV2 = XU2))";
|
||||
|
||||
let (i, formulas) = foliage::formulas(formulas).unwrap();
|
||||
assert_eq!(i, "");
|
||||
|
||||
for formula in formulas
|
||||
{
|
||||
println!("{}", formula);
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
590
src/ast.rs
590
src/ast.rs
@ -1,565 +1,83 @@
|
||||
// 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<std::rc::Rc<FunctionDeclaration>>;
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
#[derive(Eq, Hash, PartialEq)]
|
||||
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<std::rc::Rc<PredicateDeclaration>>;
|
||||
|
||||
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<std::cmp::Ordering>
|
||||
{
|
||||
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<std::rc::Rc<VariableDeclaration>>;
|
||||
|
||||
// Terms
|
||||
|
||||
pub struct BinaryOperation
|
||||
{
|
||||
pub operator: BinaryOperator,
|
||||
pub left: Box<Term>,
|
||||
pub right: Box<Term>,
|
||||
}
|
||||
|
||||
impl BinaryOperation
|
||||
{
|
||||
pub fn new(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
operator,
|
||||
left,
|
||||
right,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub struct Function
|
||||
{
|
||||
pub declaration: std::rc::Rc<FunctionDeclaration>,
|
||||
pub arguments: Vec<Box<Term>>,
|
||||
}
|
||||
|
||||
impl Function
|
||||
{
|
||||
pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
|
||||
{
|
||||
assert_eq!(declaration.arity, arguments.len(),
|
||||
"function has a different number of arguments then declared");
|
||||
|
||||
Self
|
||||
{
|
||||
declaration: std::rc::Rc::clone(declaration),
|
||||
arguments,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub enum SpecialInteger
|
||||
{
|
||||
Infimum,
|
||||
Supremum,
|
||||
}
|
||||
|
||||
pub struct UnaryOperation
|
||||
{
|
||||
pub operator: UnaryOperator,
|
||||
pub argument: Box<Term>,
|
||||
}
|
||||
|
||||
impl UnaryOperation
|
||||
{
|
||||
pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
operator,
|
||||
argument,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub struct Variable
|
||||
{
|
||||
pub declaration: std::rc::Rc<VariableDeclaration>,
|
||||
}
|
||||
|
||||
impl Variable
|
||||
{
|
||||
pub fn new(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
declaration: std::rc::Rc::clone(declaration),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Formulas
|
||||
|
||||
pub struct Compare
|
||||
{
|
||||
pub operator: ComparisonOperator,
|
||||
pub left: Box<Term>,
|
||||
pub right: Box<Term>,
|
||||
}
|
||||
|
||||
impl Compare
|
||||
{
|
||||
pub fn new(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
operator,
|
||||
left,
|
||||
right,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
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
|
||||
{
|
||||
pub parameters: std::rc::Rc<VariableDeclarations>,
|
||||
pub argument: Box<Formula>,
|
||||
}
|
||||
|
||||
impl ForAll
|
||||
{
|
||||
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
parameters,
|
||||
argument,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
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
|
||||
{
|
||||
pub antecedent: Box<Formula>,
|
||||
pub implication: Box<Formula>,
|
||||
}
|
||||
|
||||
impl Implies
|
||||
{
|
||||
pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
antecedent,
|
||||
implication,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(PartialEq)]
|
||||
pub struct Predicate
|
||||
{
|
||||
pub declaration: std::rc::Rc<PredicateDeclaration>,
|
||||
pub arguments: Vec<Box<Term>>,
|
||||
pub declaration: PredicateDeclaration,
|
||||
pub arguments: Vec<Term>,
|
||||
}
|
||||
|
||||
impl Predicate
|
||||
#[derive(PartialEq)]
|
||||
pub struct Exists
|
||||
{
|
||||
pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
|
||||
{
|
||||
assert_eq!(declaration.arity, arguments.len(),
|
||||
"predicate has a different number of arguments then declared");
|
||||
|
||||
Self
|
||||
{
|
||||
declaration: std::rc::Rc::clone(declaration),
|
||||
arguments,
|
||||
}
|
||||
}
|
||||
pub parameters: Vec<VariableDeclaration>,
|
||||
pub argument: Box<Formula>,
|
||||
}
|
||||
|
||||
// Variants
|
||||
|
||||
pub enum Term
|
||||
#[derive(PartialEq)]
|
||||
pub struct ForAll
|
||||
{
|
||||
BinaryOperation(BinaryOperation),
|
||||
Boolean(bool),
|
||||
Function(Function),
|
||||
Integer(i32),
|
||||
SpecialInteger(SpecialInteger),
|
||||
String(String),
|
||||
UnaryOperation(UnaryOperation),
|
||||
Variable(Variable),
|
||||
pub parameters: Vec<VariableDeclaration>,
|
||||
pub argument: Box<Formula>,
|
||||
}
|
||||
|
||||
pub type Terms = Vec<Box<Term>>;
|
||||
|
||||
impl Term
|
||||
#[derive(PartialEq)]
|
||||
pub enum ImplicationDirection
|
||||
{
|
||||
pub fn absolute_value(argument: Box<Term>) -> Self
|
||||
{
|
||||
Self::unary_operation(UnaryOperator::AbsoluteValue, argument)
|
||||
}
|
||||
|
||||
pub fn add(left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::binary_operation(BinaryOperator::Add, left, right)
|
||||
}
|
||||
|
||||
pub fn binary_operation(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::BinaryOperation(BinaryOperation::new(operator, left, right))
|
||||
}
|
||||
|
||||
pub fn boolean(value: bool) -> Self
|
||||
{
|
||||
Self::Boolean(value)
|
||||
}
|
||||
|
||||
pub fn divide(left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::binary_operation(BinaryOperator::Divide, left, right)
|
||||
}
|
||||
|
||||
pub fn exponentiate(left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::binary_operation(BinaryOperator::Exponentiate, left, right)
|
||||
}
|
||||
|
||||
pub fn false_() -> Self
|
||||
{
|
||||
Self::boolean(false)
|
||||
}
|
||||
|
||||
pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
|
||||
-> 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<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::binary_operation(BinaryOperator::Modulo, left, right)
|
||||
}
|
||||
|
||||
pub fn multiply(left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::binary_operation(BinaryOperator::Multiply, left, right)
|
||||
}
|
||||
|
||||
pub fn negative(argument: Box<Term>) -> 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<Term>, right: Box<Term>) -> 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<Term>) -> Self
|
||||
{
|
||||
Self::UnaryOperation(UnaryOperation::new(operator, argument))
|
||||
}
|
||||
|
||||
pub fn variable(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
|
||||
{
|
||||
Self::Variable(Variable::new(declaration))
|
||||
}
|
||||
LeftToRight,
|
||||
RightToLeft,
|
||||
}
|
||||
|
||||
#[derive(PartialEq)]
|
||||
pub enum Formula
|
||||
{
|
||||
And(Formulas),
|
||||
Boolean(bool),
|
||||
Compare(Compare),
|
||||
Exists(Exists),
|
||||
ForAll(ForAll),
|
||||
IfAndOnlyIf(IfAndOnlyIf),
|
||||
Implies(Implies),
|
||||
Not(Box<Formula>),
|
||||
Or(Formulas),
|
||||
And(Vec<Box<Formula>>),
|
||||
Or(Vec<Box<Formula>>),
|
||||
Implies(Box<Formula>, Box<Formula>, ImplicationDirection),
|
||||
Biconditional(Box<Formula>, Box<Formula>),
|
||||
Less(Term, Term),
|
||||
LessOrEqual(Term, Term),
|
||||
Greater(Term, Term),
|
||||
GreaterOrEqual(Term, Term),
|
||||
Equal(Term, Term),
|
||||
NotEqual(Term, Term),
|
||||
Boolean(bool),
|
||||
Predicate(Predicate),
|
||||
}
|
||||
|
||||
pub type Formulas = Vec<Box<Formula>>;
|
||||
|
||||
impl Formula
|
||||
#[derive(Eq, Hash, PartialEq)]
|
||||
pub enum Domain
|
||||
{
|
||||
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<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::Compare(Compare::new(operator, left, right))
|
||||
}
|
||||
|
||||
pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
||||
{
|
||||
assert!(!parameters.is_empty());
|
||||
|
||||
Self::Exists(Exists::new(parameters, argument))
|
||||
}
|
||||
|
||||
pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::compare(ComparisonOperator::Equal, left, right)
|
||||
}
|
||||
|
||||
pub fn false_() -> Self
|
||||
{
|
||||
Self::boolean(false)
|
||||
}
|
||||
|
||||
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
||||
{
|
||||
assert!(!parameters.is_empty());
|
||||
|
||||
Self::ForAll(ForAll::new(parameters, argument))
|
||||
}
|
||||
|
||||
pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::compare(ComparisonOperator::Greater, left, right)
|
||||
}
|
||||
|
||||
pub fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
|
||||
}
|
||||
|
||||
pub fn if_and_only_if(left: Box<Formula>, right: Box<Formula>) -> Self
|
||||
{
|
||||
Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
|
||||
}
|
||||
|
||||
pub fn implies(antecedent: Box<Formula>, consequent: Box<Formula>) -> Self
|
||||
{
|
||||
Self::Implies(Implies::new(antecedent, consequent))
|
||||
}
|
||||
|
||||
pub fn less(left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::compare(ComparisonOperator::Less, left, right)
|
||||
}
|
||||
|
||||
pub fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Self
|
||||
{
|
||||
Self::compare(ComparisonOperator::LessOrEqual, left, right)
|
||||
}
|
||||
|
||||
pub fn not(argument: Box<Formula>) -> Self
|
||||
{
|
||||
Self::Not(argument)
|
||||
}
|
||||
|
||||
pub fn not_equal(left: Box<Term>, right: Box<Term>) -> 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<PredicateDeclaration>, arguments: Vec<Box<Term>>)
|
||||
-> Self
|
||||
{
|
||||
Self::Predicate(Predicate::new(declaration, arguments))
|
||||
}
|
||||
|
||||
pub fn true_() -> Self
|
||||
{
|
||||
Self::boolean(true)
|
||||
}
|
||||
Program,
|
||||
Integer,
|
||||
}
|
||||
|
||||
#[derive(PartialEq)]
|
||||
pub struct VariableDeclaration
|
||||
{
|
||||
pub name: String,
|
||||
pub domain: Domain,
|
||||
}
|
||||
|
||||
#[derive(PartialEq)]
|
||||
pub enum Term
|
||||
{
|
||||
Infimum,
|
||||
Supremum,
|
||||
Integer(i64),
|
||||
Symbolic(String),
|
||||
String(String),
|
||||
Variable(VariableDeclaration),
|
||||
Add(Box<Term>, Box<Term>),
|
||||
Subtract(Box<Term>, Box<Term>),
|
||||
Multiply(Box<Term>, Box<Term>),
|
||||
Negative(Box<Term>),
|
||||
}
|
||||
|
||||
397
src/format.rs
397
src/format.rs
@ -1,121 +1,107 @@
|
||||
trait Precedence
|
||||
struct TermDisplay<'parent>
|
||||
{
|
||||
fn precedence(&self) -> i32;
|
||||
parent: Option<&'parent crate::Term>,
|
||||
term: &'parent crate::Term,
|
||||
}
|
||||
|
||||
impl Precedence for crate::Term
|
||||
struct FormulaDisplay<'parent>
|
||||
{
|
||||
fn precedence(&self) -> i32
|
||||
parent: Option<&'parent crate::Formula>,
|
||||
formula: &'parent crate::Formula,
|
||||
}
|
||||
|
||||
fn display_term<'parent>(term: &'parent crate::Term, parent: Option<&'parent crate::Term>) -> TermDisplay<'parent>
|
||||
{
|
||||
TermDisplay
|
||||
{
|
||||
match &self
|
||||
parent,
|
||||
term,
|
||||
}
|
||||
}
|
||||
|
||||
fn display_formula<'parent>(formula: &'parent crate::Formula, parent: Option<&'parent crate::Formula>)
|
||||
-> FormulaDisplay<'parent>
|
||||
{
|
||||
FormulaDisplay
|
||||
{
|
||||
parent,
|
||||
formula,
|
||||
}
|
||||
}
|
||||
|
||||
fn term_precedence(term: &crate::Term) -> u64
|
||||
{
|
||||
match term
|
||||
{
|
||||
crate::Term::Infimum | crate::Term::Supremum | crate::Term::Integer(_) | crate::Term::Symbolic(_) | crate::Term::String(_) | crate::Term::Variable(_) => 0,
|
||||
crate::Term::Negative(_) => 1,
|
||||
crate::Term::Multiply(_, _) => 2,
|
||||
crate::Term::Add(_, _) | crate::Term::Subtract(_, _) => 3,
|
||||
}
|
||||
}
|
||||
|
||||
fn term_requires_parentheses(child: &crate::Term, parent: Option<&crate::Term>) -> bool
|
||||
{
|
||||
match parent
|
||||
{
|
||||
None => false,
|
||||
Some(parent) =>
|
||||
{
|
||||
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,
|
||||
}
|
||||
let child_precedence = term_precedence(child);
|
||||
let parent_precedence = term_precedence(parent);
|
||||
|
||||
if child_precedence != parent_precedence
|
||||
{
|
||||
return child_precedence > parent_precedence;
|
||||
}
|
||||
|
||||
// Subtraction isn’t associative, so handle them separately
|
||||
// TODO: only do this for right-hand side of subtractions
|
||||
match parent
|
||||
{
|
||||
crate::Term::Subtract(_, _) => true,
|
||||
_ => false,
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
|
||||
impl Precedence for crate::Formula
|
||||
fn formula_precedence(formula: &crate::Formula) -> u64
|
||||
{
|
||||
fn precedence(&self) -> i32
|
||||
match formula
|
||||
{
|
||||
match &self
|
||||
crate::Formula::Predicate(_) | crate::Formula::Boolean(_) | crate::Formula::Less(_, _) | crate::Formula::LessOrEqual(_, _) | crate::Formula::Greater(_, _) | crate::Formula::GreaterOrEqual(_, _) | crate::Formula::Equal(_, _) | crate::Formula::NotEqual(_, _) => 0,
|
||||
crate::Formula::Exists(_) | crate::Formula::ForAll(_) => 1,
|
||||
crate::Formula::Not(_) => 2,
|
||||
crate::Formula::And(_) => 3,
|
||||
crate::Formula::Or(_) => 4,
|
||||
crate::Formula::Implies(_, _, _) => 5,
|
||||
crate::Formula::Biconditional(_, _) => 6,
|
||||
}
|
||||
}
|
||||
|
||||
fn formula_requires_parentheses(child: &crate::Formula, parent: Option<&crate::Formula>) -> bool
|
||||
{
|
||||
match parent
|
||||
{
|
||||
None => false,
|
||||
Some(parent) =>
|
||||
{
|
||||
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,
|
||||
}
|
||||
}
|
||||
}
|
||||
let child_precedence = formula_precedence(child);
|
||||
let parent_precedence = formula_precedence(parent);
|
||||
|
||||
impl std::fmt::Debug for crate::SpecialInteger
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
match &self
|
||||
{
|
||||
crate::SpecialInteger::Infimum => write!(format, "#inf"),
|
||||
crate::SpecialInteger::Supremum => write!(format, "#sup"),
|
||||
}
|
||||
}
|
||||
}
|
||||
if child_precedence != parent_precedence
|
||||
{
|
||||
return child_precedence > parent_precedence;
|
||||
}
|
||||
|
||||
impl std::fmt::Display for crate::SpecialInteger
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", &self)
|
||||
}
|
||||
}
|
||||
|
||||
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)
|
||||
// Implications aren’t associative, so handle them separately
|
||||
match parent
|
||||
{
|
||||
crate::Formula::Implies(_, _, _) => true,
|
||||
_ => false,
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
|
||||
@ -135,102 +121,29 @@ impl std::fmt::Display for crate::VariableDeclaration
|
||||
}
|
||||
}
|
||||
|
||||
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);
|
||||
let requires_parentheses = term_requires_parentheses(self.term, self.parent);
|
||||
|
||||
if requires_parentheses
|
||||
{
|
||||
write!(format, "(")?;
|
||||
}
|
||||
|
||||
match &self.term
|
||||
match self.term
|
||||
{
|
||||
crate::Term::Boolean(true) => write!(format, "true"),
|
||||
crate::Term::Boolean(false) => write!(format, "false"),
|
||||
crate::Term::SpecialInteger(value) => write!(format, "{:?}", value),
|
||||
crate::Term::Infimum => write!(format, "#inf"),
|
||||
crate::Term::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.is_empty()
|
||||
{
|
||||
write!(format, "(")?;
|
||||
|
||||
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)),
|
||||
crate::Term::Symbolic(ref value) => write!(format, "{}", value),
|
||||
crate::Term::String(ref value) => write!(format, "\"{}\"", value),
|
||||
crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration),
|
||||
crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
|
||||
crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
|
||||
crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
|
||||
crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, Some(self.term))),
|
||||
}?;
|
||||
|
||||
if requires_parentheses
|
||||
@ -250,135 +163,91 @@ impl<'term> std::fmt::Display for TermDisplay<'term>
|
||||
}
|
||||
}
|
||||
|
||||
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);
|
||||
let requires_parentheses = formula_requires_parentheses(self.formula, self.parent);
|
||||
|
||||
if requires_parentheses
|
||||
{
|
||||
write!(format, "(")?;
|
||||
}
|
||||
|
||||
match &self.formula
|
||||
match self.formula
|
||||
{
|
||||
crate::Formula::Exists(exists) =>
|
||||
crate::Formula::Exists(ref exists) =>
|
||||
{
|
||||
assert!(!exists.parameters.is_empty());
|
||||
|
||||
write!(format, "exists")?;
|
||||
|
||||
let mut separator = " ";
|
||||
|
||||
for parameter in exists.parameters.iter()
|
||||
for parameter in &exists.parameters
|
||||
{
|
||||
write!(format, "{}{:?}", separator, parameter)?;
|
||||
|
||||
separator = ", "
|
||||
}
|
||||
|
||||
write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
|
||||
write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula)))?;
|
||||
},
|
||||
crate::Formula::ForAll(for_all) =>
|
||||
crate::Formula::ForAll(ref for_all) =>
|
||||
{
|
||||
assert!(!for_all.parameters.is_empty());
|
||||
|
||||
write!(format, "forall")?;
|
||||
|
||||
let mut separator = " ";
|
||||
|
||||
for parameter in for_all.parameters.iter()
|
||||
for parameter in &for_all.parameters
|
||||
{
|
||||
write!(format, "{}{:?}", separator, parameter)?;
|
||||
|
||||
separator = ", "
|
||||
}
|
||||
|
||||
write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
|
||||
write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula)))?;
|
||||
},
|
||||
crate::Formula::Not(argument) => write!(format, "not {:?}",
|
||||
display_formula(argument, precedence))?,
|
||||
crate::Formula::And(arguments) =>
|
||||
crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, Some(self.formula)))?,
|
||||
crate::Formula::And(ref arguments) =>
|
||||
{
|
||||
let mut separator = "";
|
||||
|
||||
assert!(!arguments.is_empty());
|
||||
|
||||
for argument in arguments
|
||||
{
|
||||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
||||
write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
|
||||
|
||||
separator = " and "
|
||||
}
|
||||
},
|
||||
crate::Formula::Or(arguments) =>
|
||||
crate::Formula::Or(ref arguments) =>
|
||||
{
|
||||
let mut separator = "";
|
||||
|
||||
assert!(!arguments.is_empty());
|
||||
|
||||
for argument in arguments
|
||||
{
|
||||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
||||
write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
|
||||
|
||||
separator = " or "
|
||||
}
|
||||
},
|
||||
crate::Formula::Implies(crate::Implies{antecedent, implication})
|
||||
=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence),
|
||||
display_formula(implication, precedence))?,
|
||||
crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right})
|
||||
=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence),
|
||||
display_formula(right, precedence))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
|
||||
=> write!(format, "{:?} < {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
|
||||
=> write!(format, "{:?} <= {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
|
||||
=> write!(format, "{:?} > {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
|
||||
=> write!(format, "{:?} >= {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
|
||||
=> write!(format, "{:?} = {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
|
||||
=> write!(format, "{:?} != {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Boolean(true) => write!(format, "#true")?,
|
||||
crate::Formula::Boolean(false) => write!(format, "#false")?,
|
||||
crate::Formula::Predicate(predicate) =>
|
||||
crate::Formula::Implies(ref left, ref right, implication_direction) => match implication_direction
|
||||
{
|
||||
crate::ImplicationDirection::LeftToRight => write!(format, "{:?} -> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
|
||||
crate::ImplicationDirection::RightToLeft => write!(format, "{:?} <- {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
|
||||
},
|
||||
crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
|
||||
crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Boolean(value) =>
|
||||
match value
|
||||
{
|
||||
true => write!(format, "#true")?,
|
||||
false => write!(format, "#false")?,
|
||||
},
|
||||
crate::Formula::Predicate(ref predicate) =>
|
||||
{
|
||||
write!(format, "{}", predicate.declaration.name)?;
|
||||
|
||||
|
||||
@ -1,4 +1,6 @@
|
||||
mod ast;
|
||||
pub mod format;
|
||||
pub mod parse;
|
||||
|
||||
pub use ast::*;
|
||||
pub use ast::{Domain, Exists, Formula, ForAll, ImplicationDirection, Predicate, PredicateDeclaration, VariableDeclaration, Term};
|
||||
pub use parse::{formula, formulas, term};
|
||||
|
||||
1131
src/parse.rs
Normal file
1131
src/parse.rs
Normal file
File diff suppressed because it is too large
Load Diff
Loading…
Reference in New Issue
Block a user