Commit Graph

289 Commits

Author SHA1 Message Date
815bcda367
Update cxxopts to 2.1.0+1+gcc4914f
cxxopts 2.1.0 has a bug preventing it from being used with standard main
signatures. This updates cxxopts to the commit after release 2.1.0,
where this issue was addressed.
2018-04-13 14:03:30 +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
0608748349
Describe --complete option in readme
The readme was missing information on the --complete option. This adds a
brief mention of Clark’s completion to the readme.
2018-04-11 23:21:56 +02:00
31d4a20491
Update change log with recent additions
This updates the change log with the advanced simplification rules,
support for the exponentation operator, and the newly added examples.
2018-04-11 21:50:15 +02:00
a01e78a467
Add example program for prime number detection 2018-04-11 21:42:08 +02:00
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
b63ef21849
Add example program generating permutations 2018-04-11 21:35:29 +02:00
cc3c9b642c
Minor formatting in graph coloring example 2018-04-11 21:35:04 +02:00
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
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
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
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
c4c3156e77
Move simplification rule to tableau
This moves the rule “[primitive A] in [primitive B] === A = B” to the
simplification rule tableau.
2018-04-10 22:34:47 +02:00
107dae7287
Move simplification rule to tableau
This moves the rule “exists () (F) === F” to the simplification rule
tableau.
2018-04-10 22:34:47 +02:00
827d6e40fe
Move simplification rule to tableau
This moves the rule “[conjunction of only F] === F” to the
simplification rule tableau.
2018-04-10 22:34:47 +02:00
4a85fc4b23
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-10 22:34:46 +02:00
7e3fc007c8
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-10 22:34:46 +02:00
5c5411c0ff
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-10 22:34:46 +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
7b6729acaa
Add missing dependency to Ubuntu image
For some reason, Bison is not implicitly installed along with the other
dependencies in the Ubuntu 18.04 image used for continuous integration.
This adds Bison explicitly.
2018-04-10 22:29:55 +02:00
92fddd6665
Version bump after release 0.1.7 2018-04-08 21:03:20 +02:00
582b6ade6d
Version bump for release 0.1.7 2018-04-08 20:44:43 +02:00
e64b2e70de
Remove unused captured lambda reference 2018-04-08 20:44:43 +02:00
d7e4af98d7
Update copyright year in license file 2018-04-08 20:35:03 +02:00
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
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
c91cbaf58b
Update Catch to 2.2.2 2018-04-07 00:22:01 +02:00
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
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
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
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
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
fde2af5841
Add clang to Travis configurations
This adds the clang compiler to the tested Travis configurations.
2018-03-24 18:53:51 +01: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
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
6b1cf6735e
Update clingo to 5.2.2 2018-03-21 16:41:08 +01:00
addc65e3c5
Update Catch to 2.2.1 2018-03-21 16:35:54 +01:00
427e5705c7
Fixed order of CMake options. 2017-06-20 02:05:12 +02:00
bda57b2fe7
Fixed incorrect handling of CMake options. 2017-06-18 15:04:45 +02:00
b7cd875f0e
Updated Catch. 2017-06-15 15:27:51 +02:00
be19a5f66b
Version bump after release 0.1.6. 2017-06-13 00:14:16 +02:00
675a3e2eb7
Version bump for release 0.1.6. 2017-06-12 18:38:36 +02:00
4f399a594a
Updated change log with new examples for experimenting. 2017-06-12 18:35:06 +02:00
5f8c144628
Fixed regression in simplifying predicates with more than one argument. 2017-06-12 18:27:39 +02:00
64c9a741c4
Added example with simple propositions. 2017-06-12 15:42:23 +02:00
1f1006ea96
Corrected hiding predicates that are simple propositions. 2017-06-12 15:40:02 +02:00
7665cb7bf1
Added unit test for the completion of predicates with nested arguments. 2017-06-12 15:32:05 +02:00
d7641aa410
Added example with nested predicate arguments. 2017-06-12 03:05:21 +02:00