The interval operator has a lower precedence than, for example, binary
operations. This was unexpected and incorrectly implemented in the
output functions. For now, this is fixed by enclosing intervals in
parentheses to avoid misinterpretations.
The existing unit tests are adjusted to the updated output format.
The code responsible for completing formulas made the assumption that
all head variables could be safely removed from the list of free
variables of each formula. This is only correct given the current
limitation that only rules with singleton heads are supported.
Because of this assumption, code with multiple elements in the head were
completed to an incorrect result instead of issuing an error that such
rules aren’t supported yet.
This commit improves the code by excluding only variables that are
actually replaced from the list of free variables and not all head
variables. Still, other places will need to be adjusted for full support
of rules with multiple elements in the head. For this reason, this also
adds an error message indicating that only rules with singleton heads
are supported as of now.
Finally, multiple test cases are added to check that the supported
features related to the issues outlined above are translated without
exceptions, while errors are returned when attempting to use unsupported
The equality check is used within a simplification rule that turns
biconditionals into simple implications in special cases. This adds some
unit tests that cover this simplification rule as well as the equality
Multiplication and addition are commutative binary operations, where the
equality between the operands has to be also checked in switched order.
By mistake, the operands were not compared with the other binary
operation, which is fixed by this commit.
This adds support for detecting integer variables in formulas.
The idea is to iteratively assume variables to be noninteger and to
prove that this would lead to a false or erroneous result. If the proof
is successful, the variable is integer as a consequence.
The implementation consists of two parts. The first one is a visitor
class that recursively searches for all declared variables in a formula
and applies the second part, a custom check. Three such checks are
The first one tests whether a predicate definition is falsified by
making a variable noninteger, in which case it can be concluded that the
variable in question is integer. The second one checks whether bound
variables in a quantified formula turn the quantified part false, again
to conclude that variables are integer. The third check consists in
testing if making a variable noninteger turns the entire formula
obtained from completion true. In this case, the statement can be
dropped and the variable is concluded to be integer as well.
This provides a new function that can be used to evaluate formulas under
partial knowledge about the individual variables’ assignments.
This will be useful for testing whether formulas or subformulas become
trivial under specific interpretations.
This implements a function for retrieving the return type of terms, that
is, both the domain to which the expression evaluates to as well as
whether it’s an empty, unit, or general set with multiple values.
With this change, the domain of variable declarations can be specified.
Variables can have the integer domain, in which case additional integer-
specific simplification rules apply. Aside from that, the noninteger
domain represents precomputed values. An additional “unknown” domain is
introduced to flag variable domains prior to determining whether they
are integer or not.
This replaces the SimplificationResult enum class with OperationResult.
The rationale is that this type, which just reports whether or not an
operation actually changed the input data, is not simplification-
specific and will be used for integer variable detection as well.
The unary modulus operation does not require extra parentheses to be
printed in cases like “|X + Y|”. This adds a new option to the printing
routine to omit parentheses in cases where the parent expression already
defines a parenthesis-like scope (currently only with unary operations).