Commit Graph

323 Commits

Author SHA1 Message Date
Patrick Lühne e0aa3497ee
Version bump after release 0.1.9 2018-05-04 17:24:36 +02:00
Patrick Lühne 64bab69a36
Version bump for release 0.1.9 2018-05-04 17:06:28 +02:00
Patrick Lühne 9566629237
Document new default options in readme
By default, completion, simplification, and integer variable detection
are now turned on by default. This updates the readme accordingly.
2018-05-04 17:06:28 +02:00
Patrick Lühne c199f609bd
Enable all processing steps by default
This enables completion, simplification, and integer variable detection
by default, because these options are be used more often than not.

The change log is updated according to this change.
2018-05-04 17:06:28 +02:00
Patrick Lühne 1570432ee0
Add interval precedence fix to change log 2018-05-04 17:06:28 +02:00
Patrick Lühne 0ce4e54d1a
Fix precedence of interval operator
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.
2018-05-04 17:06:28 +02:00
Patrick Lühne fa3ed31eca
Add fix related to choice rules to change log
This adds the fix concerning the incorrect translation generated for
choice rules with multiple elements to the change log.
2018-05-04 17:06:25 +02:00
Patrick Lühne e85807accb
Fix handling of rules with multielement head
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.
2018-05-04 15:13:36 +02:00
Patrick Lühne 3393f84a4a
Add unit tests covering equality checks
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
check implementation.
2018-05-03 16:57:19 +02:00
Patrick Lühne 7013b9ea54
Fix equality check for binary operations
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.
2018-05-03 16:52:29 +02:00
Patrick Lühne c84ae51ff2
Add unit tests covering integer variable detection
This adds a series of unit tests that cover the recently introduced
support for integer variable detection as well as the corresponding
simplification rule.
2018-05-02 18:37:07 +02:00
Patrick Lühne d60e2a736b
Update examples
This updates the examples to showcase the scope of anthem’s feature set.
New examples are added concerning placeholders, hiding predicates, and
simplifications related to integer variables.
2018-04-29 22:39:44 +02:00
Patrick Lühne bb9013e7c5
Add integer extensions to change log
This adds the recent integer extensions to the change log, namely,
integer variable detection, simplifications concerning integer
variables, and support for explicitly declaring functions integer.
2018-04-29 22:39:36 +02:00
Patrick Lühne 69688d1d39
Add integer simplification rule
This adds the rule “(F in G) === (F = G) if F and G are integer
variables” to the simplification rule tableau
2018-04-29 22:28:42 +02:00
Patrick Lühne a70b1fb726
Print typing formulas for integer parameters
For every integer parameter of the visible predicates, this prints a
formula to the output that makes the integer type of that parameter
explicit.
2018-04-29 22:28:42 +02:00
Patrick Lühne a2c4d87852
Prefix integer variables with “N”
This prefixes integer variables with “N” to distinguish them from
general variables in the output in analogy to common mathematical
notations.
2018-04-29 22:28:42 +02:00
Patrick Lühne b60c65a810
Add option to turn on integer variable detection 2018-04-29 22:28:42 +02:00
Patrick Lühne 19e1e16e45
Implement integer variable detection
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.
2018-04-29 22:28:42 +02:00
Patrick Lühne 63f39e5162
Provide function for evaluating formulas
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.
2018-04-29 21:27:31 +02:00
Patrick Lühne 811523e580
Provide term type deduction function
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.
2018-04-29 21:20:29 +02:00
Patrick Lühne 09ef64a0e1
Support declaring functions as integer
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.
2018-04-28 01:48:39 +02:00
Patrick Lühne 43d2c153c7
Represent predicate parameters explicitly
This adds a vector of Parameter structs to PredicateDeclaration. In this
way, the domain of each parameter can be tracked individually.
2018-04-28 01:48:39 +02:00
Patrick Lühne 541cb3fb47
Add domain specifier to variable declarations
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.
2018-04-28 01:48:39 +02:00
Patrick Lühne 921d5ed4f0
Remove unnecessary include directives 2018-04-28 00:16:55 +02:00
Patrick Lühne e0509f725a
Replace SimplificationResult with OperationResult
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.
2018-04-27 23:37:13 +02:00
Patrick Lühne 48cf8ee3e0
Minor refactoring
Reorders some include directives lexicographically.
2018-04-27 23:35:43 +02:00
Patrick Lühne f7d99c82fa
Move Tristate class to Utils header
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.
2018-04-27 23:19:42 +02:00
Patrick Lühne 618189368c
Split functions from their declarations
This splits occurrences of functions from their declaration. This is
necessary to flag integer functions consistently and not just single
occurrences.
2018-04-27 17:59:10 +02:00
Patrick Lühne d0debc6ad1
Split predicates from their declarations
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.
2018-04-27 17:55:59 +02:00
Patrick Lühne 3ba80e8c9d
Minor refactoring 2018-04-27 17:38:29 +02:00
Patrick Lühne d66d3557c1
Minor refactoring 2018-04-27 17:25:43 +02:00
Patrick Lühne e15a6b2e88
Remove Constant class
Constants are not a construct present in Clingo’s AST and were
unintentionally made part of anthem’s AST. This removes the unused
classes for clarity.
2018-04-27 17:08:41 +02:00
Patrick Lühne 9a59ac17f5
Version bump after release 0.1.8 2018-04-20 16:37:03 +02:00
Patrick Lühne 250942643c
Version bump for release 0.1.8 2018-04-20 16:35:35 +02:00
Patrick Lühne 815bcda367
Update cxxopts to 2.1.0+1+gcc4914f
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.
2018-04-13 14:03:30 +02:00
Patrick Lühne 04094eee23
Remove unnecessary parentheses
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).
2018-04-12 00:59:03 +02:00
Patrick Lühne 8c250f5c59
Support modulus operation (absolute value)
This adds support for computing the absolute value of a term along with
an according unit test.
2018-04-12 00:38:48 +02:00
Patrick Lühne 0608748349
Describe --complete option in readme
The readme was missing information on the --complete option. This adds a
brief mention of Clark’s completion to the readme.
2018-04-11 23:21:56 +02:00
Patrick Lühne 31d4a20491
Update change log with recent additions
This updates the change log with the advanced simplification rules,
support for the exponentation operator, and the newly added examples.
2018-04-11 21:50:15 +02:00
Patrick Lühne a01e78a467
Add example program for prime number detection 2018-04-11 21:42:08 +02:00
Patrick Lühne 797660d6de
Add new simplification rule
This adds the rule “(not F [comparison] G) === (F [negated comparison]
G)” to the simplification rule tableau.
2018-04-11 21:39:27 +02:00
Patrick Lühne b63ef21849
Add example program generating permutations 2018-04-11 21:35:29 +02:00
Patrick Lühne cc3c9b642c
Minor formatting in graph coloring example 2018-04-11 21:35:04 +02:00
Patrick Lühne 40ddee8444
Add new simplification rule
This adds the rule “(not F or G) === (F -> G)” to the simplification
rule tableau.
2018-04-10 22:34:47 +02:00
Patrick Lühne 6f7b021712
Add new simplification rule
This adds the rule “(not (F and G)) === (not F or not G)” to the
simplification rule tableau.
2018-04-10 22:34:47 +02:00
Patrick Lühne 23624007ec
Add new simplification rule
This adds the rule “not not F === F” to the simplification rule tableau.
2018-04-10 22:34:47 +02:00
Patrick Lühne 6d7b91c391
Add new simplification rule
This adds the rule “(F <-> (F and G)) === (F -> G)” to the
simplification rule tableau.
2018-04-10 22:34:47 +02:00
Patrick Lühne b88393655a
Iteratively apply simplification tableau rules
With this change, the tableau rules for simplifying formula are applied
iteratively until a fixpoint is reached.
2018-04-10 22:34:47 +02:00
Patrick Lühne c4c3156e77
Move simplification rule to tableau
This moves the rule “[primitive A] in [primitive B] === A = B” to the
simplification rule tableau.
2018-04-10 22:34:47 +02:00
Patrick Lühne 107dae7287
Move simplification rule to tableau
This moves the rule “exists () (F) === F” to the simplification rule
tableau.
2018-04-10 22:34:47 +02:00