patrick
/
anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity
328 Commits 2 Branches 21 Tags 2.8 MiB
Commit Graph

67 Commits

Author SHA1 Message Date
Patrick Lühne 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
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 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
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 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 7665cb7bf1
Added unit test for the completion of predicates with nested arguments. 2017-06-12 15:32:05 +02:00
Patrick Lühne a4cd133ba7
Correctly implemented hiding predicates with nested arguments. 2017-06-12 02:25:04 +02:00
Patrick Lühne 649489a1eb
Renamed unit test for clarity. 2017-06-09 22:10:43 +02:00
Patrick Lühne cbe87d8cb7
Fixed issue with simplifying binary operations in arguments. 2017-06-09 22:00:00 +02:00
Patrick Lühne 0285c1cbbb
Renamed internal variables for clarity. 2017-06-06 01:44:44 +02:00
Patrick Lühne 19ede968ed
Added unit test that predicate arity is respected by #show statements. 2017-06-05 04:00:09 +02:00
Patrick Lühne 7ae0a1f289
Removed unnecessary parentheses after simplification. 2017-06-05 03:58:39 +02:00
Patrick Lühne b272a91888
Extended unit test for circular dependencies and #show. 2017-06-05 03:40:41 +02:00
Patrick Lühne b91e55dfc4
Added unit test for recognizing Booleans when hiding statements. 2017-06-05 03:39:10 +02:00
Patrick Lühne 7904b41e60
Added unit test covering circular dependencies with #show statements. 2017-06-05 03:34:13 +02:00
Patrick Lühne adabe1bf1a
Added simple unit tests for #show statements. 2017-06-05 03:26:09 +02:00
Patrick Lühne dcc504ebc0
Added another simplification step after completion. 2017-06-04 20:55:24 +02:00
Patrick Lühne 0930e062c4
Enforcing color output when testing for convenience. 2017-06-01 03:08:05 +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 664a57ec68
Fixed issue with multi-layer variable stacks. 2017-05-30 18:09:33 +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 48271cea88
Removed obsolete to-do. 2017-05-05 13:51:07 +02:00
Patrick Lühne d056fabb8b
Fixes lost signs with negated 0-ary predicates. 2017-05-04 15:44:37 +02:00
Patrick Lühne 5948d30e5c
Refactored implementation of completion. 2017-04-10 16:32:12 +02:00
Patrick Lühne d4ce0d54e8
Fixed typo. 2017-04-10 14:30:35 +02:00
Patrick Lühne b0388b9b28
Added example from the completion paper as unit test. 2017-04-08 20:22:50 +02:00
Patrick Lühne 37526bcc8e
Fixed incorrect handling of implications with Booleans. 2017-04-08 20:17:01 +02:00
Patrick Lühne 2ef3ef24a1
Fixed typos in unit test case. 2017-04-08 20:02:20 +02:00
Patrick Lühne 2ae5cfbfa6
Enforcing unit tests not to throw exceptions. 2017-04-08 19:59:59 +02:00
Patrick Lühne a1648e27c9
Added tests covering completion of integrity constraints and facts. 2017-04-08 18:50:42 +02:00
Patrick Lühne 350f31d0fd
Added simple unit tests for completion. 2017-04-08 18:47:06 +02:00
Patrick Lühne ac7a0f6d4c
Fixed typo. 2017-04-08 18:42:36 +02:00
Patrick Lühne 8ddf068eeb
Removed unnecessary include directive. 2017-04-08 18:38:37 +02:00
Patrick Lühne f28873617d
Implemented translation of anonymous variables. 2017-03-29 21:28:46 +02:00
Patrick Lühne c8cd6fec48
Added test case for incorrectly simplified rules with comparison. 2017-03-28 17:10:38 +02:00
Patrick Lühne 32e6301b5e
Added some unit tests for the simplification procedure. 2017-03-23 15:14:32 +01:00
Patrick Lühne 09c2674148
Fixed incorrectly translated choice rules with multiple elements in the aggregate. 2017-03-23 02:06:19 +01:00
Patrick Lühne 73f67f5c17
Added back support for function symbols. 2017-03-15 17:01:09 +01:00
Patrick Lühne 9e6d135781
Implemented explicit syntax tree representation for first-order formulas. 2017-03-15 16:00:43 +01:00
Patrick Lühne c294aa1337
Added test covering choice rules with bodies. 2017-03-06 15:55:00 +01:00
Patrick Lühne 2a0b7ef3b5
Added tests covering simple choice rules. 2017-03-06 15:49:40 +01:00
Patrick Lühne a653556d77
Resolved minor warnings. 2016-11-29 02:29:54 +01:00