Implement name parsing
Start parsing terms
Implement word boundaries
Implement strings
Add pipe character to allowed word boundaries
Implement booleans
Require word boundaries around names
Implement variable parsing
Finish implementing term parsing
Add term parsing test
Test associativity of multiplication
Make parse feature the default
Fix term parsing and finish tests
Start parsing formulas
Continue parsing formulas
Finish implementing formula parsing
Move boolean parser to separate module
Move integer parser to separate module
Move special integer parser to separate module
Move string parser to separate module
Address warnings
Fix negation parser
Refactor term parser tests
Address clippy warning
Disallow reserved keywords as names
Add missing word boundary character
Check that names don’t start with special characters
Minor refactoring
Add note
Test conjunction parser
Test disjunction parser
Parentheses for stronger checks
Add note
Fix implication parser and output
Split formatting functionality into two files
Test term formatting
Add unit test for function declaration formatting
Work in progress
Fix implication formatting
Refactor precedence rules
Start testing formula formatter
Minor formatting
Test remaining formula types
Add unit tests for precedence-0 formulas and lower
Before larger refactoring
Refactor precedence rules for formulas
Remove ChildPosition enum
Fix
Address warnings
Remove unneeded precedence implementation
Test negation
Test quantified formulas
Clean up tests
Clean up tests
Test conjunction
Test disjunction
Start testing implications
Refactor parenthesis requirement check
Fix precedence of implication
Continue testing implication
Test biconditionals
Experimental method for testing all permutations
Rewrite tests for clarity
Rewrite tests for clarity
Add type annotations
Rewrite tests for clarity
Reorganize tests
Finish testing biconditionals
Support empty n-aries
Support quantified expressions with 0 parameters
Rewrite term formatting tests for clarity
Reorganize term formatter tests
Refactor parenthesis rules for terms
Remove unneeded parentheses enum
Refactoring
Refactoring
Minor clean-up
Minor clean-up
Simplify representation of quantified formulas
Remove redundant indirection
Remove redundant indirection
This introduces a Format trait, which can be implemented to customize
the appearance of variable declarations right now. The Format trait will
be extended with further customization options in the future.
The rules for determining required parentheses as opposed to parentheses
that can be omitted are more complicated than just showing parentheses
whenever a child expression has lower precedence than its parent. This
necessitated a rewrite.
This new implementation determines whether an expression requires to be
parenthesized with individual rules for each type of expression, which
may or may not depend on the type of the parent expression and the
position of a child within its parent expression. For example,
implication is defined to be right-associative, which means that the
parentheses in the formula
(F -> G) -> H
cannot be ommitted. When determining whether the subformula (F -> G)
needs to be parenthesized, the new algorithm notices that the subformula
is contained as the antecedent of another implication and concludes that
parentheses are required.
Furthermore, this adds extensive unit tests for both formula and term
formatting. The general idea is to test all types of expressions
individually and, in addition to that, all combinations of parent and
child expression types.
Unit testing made it clear that the formatting of empty and 1-ary
conjunctions, disjunctions, and biconditionals needs to be well-defined
even though these types of formulas may be unconventional. The same
applies to existentially and universally quantified formulas where the
list of parameters is empty. Now, empty conjunctions and biconditionals
are rendered like true Booleans, empty disjunctions like false Booleans,
and 1-ary conjunctions, disjunctions, biconditionals, as well as
quantified expressions with empty parameter lists as their singleton
argument.
The latter formulas can be considered neutral intermediates. That is,
they should not affect whether their singleton arguments are
parenthesized or not. To account for that, all unit tests covering
combinations of formulas are tested with any of those five neutral
intermediates additionally.
The type aliases for vectors of formulas and terms were defined as
vectors of boxed formulas and terms, respectively. This is an
unnecessary indirection, so store the formulas and terms directly.
These reference-counted arguments were taken by reference, which made it
necessary to clone them. If a reference-counted object is created for the
sole purpose of being passed to one of these methods, it would be cloned
unnecessarily. This changes the signatures to take these arguments by
value, shifting the responsibility of cloning the reference-counted
objects to the users of these methods.
Existential and universal quantification used redundant data
representations, while they actually share the same structure. This
unifies both into a single QuantifiedFormula type.
For convenience, support biconditionals with more than one argument.
An n-ary “if and only if” statement
F_1 <-> F_2 <-> ... <-> F_n
is to be interpreted as
F_1 <-> F_2 and F2 <-> F3 and ... and F_(n - 1) <-> F_n
As the absolute value operation has its own type of parentheses, it
never needs to take precedence over other terms in order to be displayed
correctly. To avoid extraneous parentheses around absolute value
operations, set its precedence level to 0.
The precedence rules of binary operations are a bit trickier than
expected. The fact that a parent and a child term have the same
precedence level doesn’t automatically mean that parentheses can be
omitted. This is the case, for example, with
a - (b + c)
While addition and subtraction have the same precedence level, the
parenthesis cannot be omitted. In general, this happens on the right-
hand side of the subtraction, division, and modulo operators if the
right-hand side has the same precedence level.
This patch fixes the output of binary operations accordingly.
Booleans are supposed to be formatted without a leading hash sign in
both terms and formulas. By mistake, the formula formatter added leading
hash signs though.
This adds Debug and Display trait implementations for the SpecialInteger
enum to make it possible to format its values without having to wrap it
in a Term variant.
Provided that the latest version of this crate is always published on
crates.io and tagged as a release on GitHub.com, the crates.io and the
GitHub.com release badges will always show the same version.
Consequently, remove the GitHub.com release badge to avoid redundancy.
This provides an abstract syntax tree for first-order logic with integer
arithmetics. Initially, the following types of formulas are supported:
- Booleans values (true and false)
- predicates
- negated formulas
- comparisons of terms (<, ≤, >, ≥, =, ≠)
- implications and biconditionals
- conjunctions and disjunctions of formulas
- existentially and universally quantified formulas
In addition, these types of terms are provided:
- 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)
Patrick Lühne