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
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
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
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
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
Patrick Lühne
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
Patrick Lühne
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
Patrick Lühne
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
Patrick Lühne
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
Patrick Lühne
e64b2e70de
Remove unused captured lambda reference
2018-04-08 20:44:43 +02:00
Patrick Lühne
c294a29cb2
Support placeholders with #external declarations
...
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.
2018-04-08 20:28:57 +02:00
Patrick Lühne
22238bb398
Switch to C++17
...
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.
2018-03-24 16:09:52 +01:00
Patrick Lühne
5f8c144628
Fixed regression in simplifying predicates with more than one argument.
2017-06-12 18:27:39 +02:00
Patrick Lühne
1f1006ea96
Corrected hiding predicates that are simple propositions.
2017-06-12 15:40:02 +02:00
Patrick Lühne
a4cd133ba7
Correctly implemented hiding predicates with nested arguments.
2017-06-12 02:25:04 +02:00
Patrick Lühne
bbbd0b65a4
Added new option --parentheses=full to make parsing the output easier.
2017-06-06 02:02:26 +02:00
Patrick Lühne
0285c1cbbb
Renamed internal variables for clarity.
2017-06-06 01:44:44 +02:00
Patrick Lühne
95984f0447
Added warning when attempting to use #show statements without completion.
2017-06-05 04:24:00 +02:00
Patrick Lühne
7ae0a1f289
Removed unnecessary parentheses after simplification.
2017-06-05 03:58:39 +02:00
Patrick Lühne
3b26580815
Minor formatting.
2017-06-05 03:54:17 +02:00
Patrick Lühne
14abc37116
Implemented #show statements for completed output.
2017-06-05 03:02:22 +02:00
Patrick Lühne
4fd143ef64
Added simplification rule “exists X (X = Y)” → “#true.”
2017-06-05 02:41:17 +02:00
Patrick Lühne
7bf5d3867d
Minor clarification on side effects of a function.
2017-06-05 00:19:43 +02:00
Patrick Lühne
ab71e8eb0a
Minor refactoring.
2017-06-04 20:55:25 +02:00
Patrick Lühne
dcc504ebc0
Added another simplification step after completion.
2017-06-04 20:55:24 +02:00
Patrick Lühne
381d55b6ed
Minor formatting fix.
2017-06-01 16:16:06 +02:00
Patrick Lühne
2bc60d3eea
Started implementing support for #show statements.
2017-06-01 04:05:11 +02:00
Patrick Lühne
cdcee897ec
Added missing error message when input file does not exist.
2017-06-01 03:29:09 +02:00
Patrick Lühne
4baed6fbc6
Added back completion support.
2017-06-01 02:37:45 +02:00
Patrick Lühne
0d8b1e94da
Refactored error handling.
2017-05-31 18:03:19 +02:00
Patrick Lühne
1de0486989
Removed unnecessary namespace identifiers.
2017-05-30 18:13:31 +02:00
Patrick Lühne
664a57ec68
Fixed issue with multi-layer variable stacks.
2017-05-30 18:09:33 +02:00
Patrick Lühne
7aad8380d1
Refactored logging interface.
2017-05-30 17:19:26 +02:00
Patrick Lühne
8214d7837a
Fixed incorrect variable declaration look-up in variable stack.
2017-05-30 16:40:14 +02:00
Patrick Lühne
2964dd1309
Restricting variable stack look-up to user-defined variables.
2017-05-30 16:39:44 +02:00
Patrick Lühne
f78c0e4da5
Reordered constructor parameters of VariableDeclaration.
2017-05-30 16:27:45 +02:00
Patrick Lühne
1917f18b6a
Added back simplification support.
2017-05-30 04:06:56 +02:00
Patrick Lühne
1c925d661b
Major refactoring to uniquely link variables to their declarations (breaks simplification and completion).
2017-05-30 03:56:35 +02:00
Patrick Lühne
c2f8762dc1
Removed unnecessary CMake directive.
2017-05-08 14:41:02 +02:00
Patrick Lühne
6e7abb283e
Fixed minor incorrect variable references.
2017-04-10 17:50:19 +02:00