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

279 Commits

Author SHA1 Message Date
Patrick Lühne 285fa08e5a
Version bump for release 0.1.8 RC 1 2018-04-10 00:19:55 +02:00
Patrick Lühne dfffdcfce6
Add new simplification rule 
This adds the rule “(not F or G) === (F -> G)” to the simplification
rule tableau.
 2018-04-09 23:48:04 +02:00
Patrick Lühne 4967576b6c
Add new simplification rule 
This adds the rule “(not (F and G)) === (not F or not G)” to the
simplification rule tableau.
 2018-04-09 23:39:29 +02:00
Patrick Lühne 1c5851441d
Add new simplification rule 
This adds the rule “not not F === F” to the simplification rule tableau.
 2018-04-09 23:36:16 +02:00
Patrick Lühne b18ddcc575
Add new simplification rule 
This adds the rule “(F <-> (F and G)) === (F -> G)” to the
simplification rule tableau.
 2018-04-09 23:27:38 +02:00
Patrick Lühne 00ab975c2d
Iteratively apply simplification tableau rules 
With this change, the tableau rules for simplifying formula are applied
iteratively until a fixpoint is reached.
 2018-04-08 22:24:14 +02:00
Patrick Lühne e01b5dc561
Move simplification rule to tableau 
This moves the rule “[primitive A] in [primitive B] === A = B” to the
simplification rule tableau.
 2018-04-08 22:24:14 +02:00
Patrick Lühne 91529b84aa
Move simplification rule to tableau 
This moves the rule “exists () (F) === F” to the simplification rule
tableau.
 2018-04-08 22:24:14 +02:00
Patrick Lühne 1cbfd335a1
Move simplification rule to tableau 
This moves the rule “[conjunction of only F] === F” to the
simplification rule tableau.
 2018-04-08 22:24:14 +02:00
Patrick Lühne a86e978a5a
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-08 22:24:14 +02:00
Patrick Lühne 5eb3ed5681
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-08 22:24:14 +02:00
Patrick Lühne 3d0266136c
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-08 22:24:10 +02:00
Patrick Lühne 92fddd6665
Version bump after release 0.1.7 2018-04-08 21:03:20 +02:00
Patrick Lühne 582b6ade6d
Version bump for release 0.1.7 2018-04-08 20:44:43 +02:00
Patrick Lühne e64b2e70de
Remove unused captured lambda reference 2018-04-08 20:44:43 +02:00
Patrick Lühne d7e4af98d7
Update copyright year in license file 2018-04-08 20:35:03 +02:00
Patrick Lühne a406cb43bd
Update graph coloring example with placeholders 
This replaces the former graph coloring example with a new formulation
that makes use of the newly supported placeholders.
 2018-04-08 20:28:57 +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 c91cbaf58b
Update Catch to 2.2.2 2018-04-07 00:22:01 +02:00
Patrick Lühne 2a2fec0eac
Update change log with dependency change 
This adds the dependency change from Boost (for program options) to
cxxopts to the change log.
 2018-04-06 23:08:57 +02:00
Patrick Lühne 09e56c3bce
Format change log sections with proper headings 
This makes the change log sections have proper headings, which were just
normal text before.
 2018-04-06 22:53:59 +02:00
Patrick Lühne e2c0d6b705
Update cxxopts to 2.0.0+3+gabe9ebd 
With cxxopts 2.0.0, positional arguments weren’t recognized when other
command-line options were passed before. This has been fixed in the
meantime, but there is no release with the bug fix yet.

This updates cxxopts to a newer commit to ship anthem with this fix.
 2018-04-06 22:44:14 +02:00
Patrick Lühne e01506f9ff
Drop Boost dependency 
Boost was only used for program option parsing. To avoid this huge
dependency, this commit replaces boost::program_options with cxxopts,
a header-only library with the same functionality.

cxxopts is added as a submodule, and Boost is removed from the
dependencies in the code and Travis configuration.
 2018-03-25 17:24:06 +02:00
Patrick Lühne 50ebf3c6de
Install g++ package explicitly on Ubuntu 
Apparently, g++ is only installed because of the Boost dependency.
Make the g++ dependency explicit to avoid future package errors.
 2018-03-25 17:23:33 +02:00
Patrick Lühne fde2af5841
Add clang to Travis configurations 
This adds the clang compiler to the tested Travis configurations.
 2018-03-24 18:53:51 +01: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 c7d1026a31
Switch Travis to Docker 
As Travis only provides outdated packages (compilers in particular),
this changes the Travis configuration to use Docker images to build and
test the code. This also has the benefit that multiple distributions can
be tested and not just Ubuntu.

For the time being, Arch Linux and Ubuntu 18.04 are added as supported
platforms.
 2018-03-24 15:51:20 +01:00
Patrick Lühne 6b1cf6735e
Update clingo to 5.2.2 2018-03-21 16:41:08 +01:00
Patrick Lühne addc65e3c5
Update Catch to 2.2.1 2018-03-21 16:35:54 +01:00
Patrick Lühne 427e5705c7
Fixed order of CMake options. 2017-06-20 02:05:12 +02:00
Patrick Lühne bda57b2fe7
Fixed incorrect handling of CMake options. 2017-06-18 15:04:45 +02:00
Patrick Lühne b7cd875f0e
Updated Catch. 2017-06-15 15:27:51 +02:00
Patrick Lühne be19a5f66b
Version bump after release 0.1.6. 2017-06-13 00:14:16 +02:00
Patrick Lühne 675a3e2eb7
Version bump for release 0.1.6. 2017-06-12 18:38:36 +02:00
Patrick Lühne 4f399a594a
Updated change log with new examples for experimenting. 2017-06-12 18:35:06 +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 64c9a741c4
Added example with simple propositions. 2017-06-12 15:42:23 +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 d7641aa410
Added example with nested predicate arguments. 2017-06-12 03:05:21 +02:00
Patrick Lühne eb730b9f8b
Added example for attempting to hide a circular predicate dependency. 2017-06-12 03:01:30 +02:00
Patrick Lühne ecdefa9221
Added graph coloring example. 2017-06-12 02:53:02 +02:00
Patrick Lühne c1899a6347
Added Schur numbers example. 2017-06-12 02:27:57 +02:00
Patrick Lühne a4cd133ba7
Correctly implemented hiding predicates with nested arguments. 2017-06-12 02:25:04 +02:00
Patrick Lühne 1d172589f5
Rephrased change log entry for clarity. 2017-06-09 22:13:05 +02:00
Patrick Lühne 649489a1eb
Renamed unit test for clarity. 2017-06-09 22:10:43 +02:00
Patrick Lühne fd40bd1a5b
Added bug fix to change log. 2017-06-09 22:02:02 +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 9d1a1249d3
Removed obsolete to-do. 2017-06-09 20:19:46 +02:00
Patrick Lühne 0d5fb00286
Updated clingo. 2017-06-06 19:26:33 +02:00