Commit Graph

315 Commits

Author SHA1 Message Date
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
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
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
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
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
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
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
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
b60c65a810
Add option to turn on integer variable detection 2018-04-29 22:28:42 +02:00
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
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
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
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
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
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
921d5ed4f0
Remove unnecessary include directives 2018-04-28 00:16:55 +02:00
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
48cf8ee3e0
Minor refactoring
Reorders some include directives lexicographically.
2018-04-27 23:35:43 +02:00
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
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
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
3ba80e8c9d
Minor refactoring 2018-04-27 17:38:29 +02:00
d66d3557c1
Minor refactoring 2018-04-27 17:25:43 +02:00
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
9a59ac17f5
Version bump after release 0.1.8 2018-04-20 16:37:03 +02:00
250942643c
Version bump for release 0.1.8 2018-04-20 16:35:35 +02:00
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
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
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
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
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
a01e78a467
Add example program for prime number detection 2018-04-11 21:42:08 +02:00
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
b63ef21849
Add example program generating permutations 2018-04-11 21:35:29 +02:00
cc3c9b642c
Minor formatting in graph coloring example 2018-04-11 21:35:04 +02:00
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
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
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
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
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
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
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
827d6e40fe
Move simplification rule to tableau
This moves the rule “[conjunction of only F] === F” to the
simplification rule tableau.
2018-04-10 22:34:47 +02:00
4a85fc4b23
Move simplification rule to tableau
This moves the rule “exists ... ([#true/#false]) === [#true/#false]” to
the simplification rule tableau along with “[empty conjunction] ===
2018-04-10 22:34:46 +02:00
7e3fc007c8
Move simplification rule to tableau
This moves the rule “exists X (X = t and F(X)) === exists () (F(t))” to
the simplification rule tableau.
2018-04-10 22:34:46 +02:00
5c5411c0ff
Implement simplification rule tableau
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.
2018-04-10 22:34:46 +02:00
eaabeb0c55
Support exponentiation operator
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.
2018-04-10 22:29:55 +02:00
7b6729acaa
Add missing dependency to Ubuntu image
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.
2018-04-10 22:29:55 +02:00
92fddd6665
Version bump after release 0.1.7 2018-04-08 21:03:20 +02:00
582b6ade6d
Version bump for release 0.1.7 2018-04-08 20:44:43 +02:00