Commit Graph

5 Commits

Author SHA1 Message Date
Patrick Lühne ae3925c72b
Fix function formatting
By mistake, a function’s name was printed two consecutive times if the
function had more than one argument.
2020-03-30 05:39:20 +02:00
Patrick Lühne 6183ae22b5
Minor refactoring for clarity 2020-03-30 05:38:42 +02:00
Patrick Lühne a7e07380ff
Support formatting special integers separately
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.
2020-03-30 05:32:26 +02:00
Patrick Lühne 14abd73110
Remove unneeded lifetime specifiers 2020-03-30 05:19:01 +02:00
Patrick Lühne a446aed011
Initial commit
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)
2020-02-05 03:23:11 +01:00