Commit Graph

122 Commits

Author SHA1 Message Date
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
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
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
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
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
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
cbe87d8cb7 Fixed issue with simplifying binary operations in arguments. 2017-06-09 22:00:00 +02:00
9d1a1249d3 Removed obsolete to-do. 2017-06-09 20:19:46 +02:00
bbbd0b65a4 Added new option --parentheses=full to make parsing the output easier. 2017-06-06 02:02:26 +02:00
0285c1cbbb Renamed internal variables for clarity. 2017-06-06 01:44:44 +02:00
14abc37116 Implemented #show statements for completed output. 2017-06-05 03:02:22 +02:00
b4c8ce3dc4 Extended AST visitors with optional return type. 2017-06-04 21:59:19 +02:00
4ed4458f1b Fixed typos in error messages. 2017-06-04 04:43:07 +02:00
64bd1c17e3 Improved debug output. 2017-06-02 14:59:13 +02:00
2bc60d3eea Started implementing support for #show statements. 2017-06-01 04:05:11 +02:00
663c59c470 Removed unused function. 2017-06-01 03:43:18 +02:00
85614296e2 Improved debug message. 2017-06-01 03:32:19 +02:00
cdcee897ec Added missing error message when input file does not exist. 2017-06-01 03:29:09 +02:00
4baed6fbc6 Added back completion support. 2017-06-01 02:37:45 +02:00
c47bd3c934 Noted to-do. 2017-06-01 02:32:45 +02:00
b918da3c49 Minor formatting. 2017-06-01 00:19:09 +02:00
e998c5b7be Removed unused variable. 2017-06-01 00:16:02 +02:00
957457939c Minor formatting. 2017-06-01 00:15:48 +02:00
4f003a8730 Noted to-do. 2017-05-31 18:12:24 +02:00
830b8846d6 Added more constructor options for exceptions. 2017-05-31 18:10:55 +02:00
193b7f5c91 Noted to-do. 2017-05-31 18:07:27 +02:00
0d8b1e94da Refactored error handling. 2017-05-31 18:03:19 +02:00
1de0486989 Removed unnecessary namespace identifiers. 2017-05-30 18:13:31 +02:00
664a57ec68 Fixed issue with multi-layer variable stacks. 2017-05-30 18:09:33 +02:00
7aad8380d1 Refactored logging interface. 2017-05-30 17:19:26 +02:00
59fbc473df Dropping now unused head variable names. 2017-05-30 16:40:56 +02:00
2964dd1309 Restricting variable stack look-up to user-defined variables. 2017-05-30 16:39:44 +02:00
f78c0e4da5 Reordered constructor parameters of VariableDeclaration. 2017-05-30 16:27:45 +02:00
9a3c85dc83 Dropping now unused body variable names. 2017-05-30 16:20:57 +02:00
1c925d661b Major refactoring to uniquely link variables to their declarations (breaks simplification and completion). 2017-05-30 03:56:35 +02:00
ce159c7bf0 Added missing assertion. 2017-05-23 15:25:55 +02:00
d056fabb8b Fixes lost signs with negated 0-ary predicates. 2017-05-04 15:44:37 +02:00
108c51cf28 Fixed Variant move semantic issue with older compilers. 2017-04-11 16:59:58 +02:00
d999415c3d Enforcing move semantics on all AST elements explicitly. 2017-04-11 15:55:31 +02:00
5948d30e5c Refactored implementation of completion. 2017-04-10 16:32:12 +02:00
37526bcc8e Fixed incorrect handling of implications with Booleans. 2017-04-08 20:17:01 +02:00
8210adea7c Added support for completion of integrity constraints. 2017-04-08 18:25:59 +02:00
a716da4af1 Finished implementing completion (unit tests to follow). 2017-04-08 16:21:24 +02:00