Commit Graph

120 Commits

Author SHA1 Message Date
504f7da4c3
Add unknown variable domain
Before being able to tell whether a variable’s domain is general or
integer, it is necessary to flag it as “unknown.”
2018-04-20 16:37:48 +02:00
d2b48f9679
Move Tristate class to separate header
The Tristate class (representing truth values that are either true,
false, or unknown) is used at multiple ends. This moves it to a separate
header for reusing it properly.
2018-04-20 16:37:48 +02:00
2372eb24c4
Refactor predicate representation
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-20 16:37:47 +02:00
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