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 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)
