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
features.
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 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.
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.
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.
With C++17, optionals, an experimental language feature, were moved to
the “std” namespace. This makes C++17 mandatory and drops the now
obsolete “experimental” namespace.
Patrick Lühne