Commit Graph

117 Commits

Author SHA1 Message Date
87dcd6ee93 Add domain specifier to variable declarations
With this change, the domain of variable declarations can be specified.
While the default is the general domain of all precomputed value, this
adds support for integer variables, for which advanced simplification
rules apply.
2018-04-20 16:37:47 +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
811eb3054c Partly implemented completion. 2017-04-06 17:46:16 +02:00
c3351206b9 Removed unused code. 2017-04-06 17:19:32 +02:00
27b46ceee1 Added scaffold for implementing completion. 2017-04-05 18:21:38 +02:00
838a68e230 Refactoring to prepare for implementing completion. 2017-04-05 18:15:42 +02:00
5940fc4a3b Removed workarounds thanks to a fix in clingo. 2017-04-01 03:13:52 +02:00