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
implemented.
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.
This adds a new syntax for declaring functions integer:
#external integer(<function name>(<arity)).
If a function is declared integer, it may enable some variables to be
detected as integer as well.
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 Tristate class (representing truth values that are either true,
false, or unknown) will be used at multiple ends. This moves it to a
separate header in order to reuse it properly.
This refactoring separates predicates from their declarations. The
purpose of this is to avoid duplicating properties specific to the
predicate declaration and not its occurrences in the program.
cxxopts 2.1.0 has a bug preventing it from being used with standard main
signatures. This updates cxxopts to the commit after release 2.1.0,
where this issue was addressed.
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).
This implements a tableau containing simplification rules that can be
iteratively applied to input formulas until they remain unchanged.
First, this moves the rule “exists X (X = Y) === #true” to the tableau
as a reference implementation.
Because of a bug in the Clingo API, the exponentation operator was not
properly exposed to anthem. This updates Clingo to a version with a
fixed API and adds proper support for exponentation within anthem along
with a matching unit test.
For some reason, Bison is not implicitly installed along with the other
dependencies in the Ubuntu 18.04 image used for continuous integration.
This adds Bison explicitly.
This adds support for declaring predicates as placeholders through the
“#external” directive in the input language of clingo.
Placeholders are not subject to completion. This prevents predicates
that represent instance-specific facts from being assumed as universally
false by default negation when translating an encoding.
This stretches clingo’s usual syntax a bit to make the implementation
lightweight. In order to declare a predicate with a specific arity as a
placeholder, the following statement needs to be added to the program:
#external <predicate name>(<arity>).
Multiple unit tests cover cases where placeholders are used or not as
well as a more complex graph coloring example.
