Compare commits

...

73 Commits

Author SHA1 Message Date
Patrick Lühne e0aa3497ee
Version bump after release 0.1.9 2018-05-04 17:24:36 +02:00
Patrick Lühne 64bab69a36
Version bump for release 0.1.9 2018-05-04 17:06:28 +02:00
Patrick Lühne 9566629237
Document new default options in readme
By default, completion, simplification, and integer variable detection
are now turned on by default. This updates the readme accordingly.
2018-05-04 17:06:28 +02:00
Patrick Lühne c199f609bd
Enable all processing steps by default
This enables completion, simplification, and integer variable detection
by default, because these options are be used more often than not.

The change log is updated according to this change.
2018-05-04 17:06:28 +02:00
Patrick Lühne 1570432ee0
Add interval precedence fix to change log 2018-05-04 17:06:28 +02:00
Patrick Lühne 0ce4e54d1a
Fix precedence of interval operator
The interval operator has a lower precedence than, for example, binary
operations. This was unexpected and incorrectly implemented in the
output functions. For now, this is fixed by enclosing intervals in
parentheses to avoid misinterpretations.

The existing unit tests are adjusted to the updated output format.
2018-05-04 17:06:28 +02:00
Patrick Lühne fa3ed31eca
Add fix related to choice rules to change log
This adds the fix concerning the incorrect translation generated for
choice rules with multiple elements to the change log.
2018-05-04 17:06:25 +02:00
Patrick Lühne e85807accb
Fix handling of rules with multielement head
The code responsible for completing formulas made the assumption that
all head variables could be safely removed from the list of free
variables of each formula. This is only correct given the current
limitation that only rules with singleton heads are supported.

Because of this assumption, code with multiple elements in the head were
completed to an incorrect result instead of issuing an error that such
rules aren’t supported yet.

This commit improves the code by excluding only variables that are
actually replaced from the list of free variables and not all head
variables. Still, other places will need to be adjusted for full support
of rules with multiple elements in the head. For this reason, this also
adds an error message indicating that only rules with singleton heads
are supported as of now.

Finally, multiple test cases are added to check that the supported
features related to the issues outlined above are translated without
exceptions, while errors are returned when attempting to use unsupported
features.
2018-05-04 15:13:36 +02:00
Patrick Lühne 3393f84a4a
Add unit tests covering equality checks
The equality check is used within a simplification rule that turns
biconditionals into simple implications in special cases. This adds some
unit tests that cover this simplification rule as well as the equality
check implementation.
2018-05-03 16:57:19 +02:00
Patrick Lühne 7013b9ea54
Fix equality check for binary operations
Multiplication and addition are commutative binary operations, where the
equality between the operands has to be also checked in switched order.
By mistake, the operands were not compared with the other binary
operation, which is fixed by this commit.
2018-05-03 16:52:29 +02:00
Patrick Lühne c84ae51ff2
Add unit tests covering integer variable detection
This adds a series of unit tests that cover the recently introduced
support for integer variable detection as well as the corresponding
simplification rule.
2018-05-02 18:37:07 +02:00
Patrick Lühne d60e2a736b
Update examples
This updates the examples to showcase the scope of anthem’s feature set.
New examples are added concerning placeholders, hiding predicates, and
simplifications related to integer variables.
2018-04-29 22:39:44 +02:00
Patrick Lühne bb9013e7c5
Add integer extensions to change log
This adds the recent integer extensions to the change log, namely,
integer variable detection, simplifications concerning integer
variables, and support for explicitly declaring functions integer.
2018-04-29 22:39:36 +02:00
Patrick Lühne 69688d1d39
Add integer simplification rule
This adds the rule “(F in G) === (F = G) if F and G are integer
variables” to the simplification rule tableau
2018-04-29 22:28:42 +02:00
Patrick Lühne a70b1fb726
Print typing formulas for integer parameters
For every integer parameter of the visible predicates, this prints a
formula to the output that makes the integer type of that parameter
explicit.
2018-04-29 22:28:42 +02:00
Patrick Lühne a2c4d87852
Prefix integer variables with “N”
This prefixes integer variables with “N” to distinguish them from
general variables in the output in analogy to common mathematical
notations.
2018-04-29 22:28:42 +02:00
Patrick Lühne b60c65a810
Add option to turn on integer variable detection 2018-04-29 22:28:42 +02:00
Patrick Lühne 19e1e16e45
Implement integer variable detection
This adds support for detecting integer variables in formulas.

The idea is to iteratively assume variables to be noninteger and to
prove that this would lead to a false or erroneous result. If the proof
is successful, the variable is integer as a consequence.

The implementation consists of two parts. The first one is a visitor
class that recursively searches for all declared variables in a formula
and applies the second part, a custom check. Three such checks are
implemented.

The first one tests whether a predicate definition is falsified by
making a variable noninteger, in which case it can be concluded that the
variable in question is integer. The second one checks whether bound
variables in a quantified formula turn the quantified part false, again
to conclude that variables are integer. The third check consists in
testing if making a variable noninteger turns the entire formula
obtained from completion true. In this case, the statement can be
dropped and the variable is concluded to be integer as well.
2018-04-29 22:28:42 +02:00
Patrick Lühne 63f39e5162
Provide function for evaluating formulas
This provides a new function that can be used to evaluate formulas under
partial knowledge about the individual variables’ assignments.

This will be useful for testing whether formulas or subformulas become
trivial under specific interpretations.
2018-04-29 21:27:31 +02:00
Patrick Lühne 811523e580
Provide term type deduction function
This implements a function for retrieving the return type of terms, that
is, both the domain to which the expression evaluates to as well as
whether it’s an empty, unit, or general set with multiple values.
2018-04-29 21:20:29 +02:00
Patrick Lühne 09ef64a0e1
Support declaring functions as integer
This adds a new syntax for declaring functions integer:

    #external integer(<function name>(<arity)).

If a function is declared integer, it may enable some variables to be
detected as integer as well.
2018-04-28 01:48:39 +02:00
Patrick Lühne 43d2c153c7
Represent predicate parameters explicitly
This adds a vector of Parameter structs to PredicateDeclaration. In this
way, the domain of each parameter can be tracked individually.
2018-04-28 01:48:39 +02:00
Patrick Lühne 541cb3fb47
Add domain specifier to variable declarations
With this change, the domain of variable declarations can be specified.
Variables can have the integer domain, in which case additional integer-
specific simplification rules apply. Aside from that, the noninteger
domain represents precomputed values. An additional “unknown” domain is
introduced to flag variable domains prior to determining whether they
are integer or not.
2018-04-28 01:48:39 +02:00
Patrick Lühne 921d5ed4f0
Remove unnecessary include directives 2018-04-28 00:16:55 +02:00
Patrick Lühne e0509f725a
Replace SimplificationResult with OperationResult
This replaces the SimplificationResult enum class with OperationResult.
The rationale is that this type, which just reports whether or not an
operation actually changed the input data, is not simplification-
specific and will be used for integer variable detection as well.
2018-04-27 23:37:13 +02:00
Patrick Lühne 48cf8ee3e0
Minor refactoring
Reorders some include directives lexicographically.
2018-04-27 23:35:43 +02:00
Patrick Lühne f7d99c82fa
Move Tristate class to Utils header
The Tristate class (representing truth values that are either true,
false, or unknown) will be used at multiple ends. This moves it to a
separate header in order to reuse it properly.
2018-04-27 23:19:42 +02:00
Patrick Lühne 618189368c
Split functions from their declarations
This splits occurrences of functions from their declaration. This is
necessary to flag integer functions consistently and not just single
occurrences.
2018-04-27 17:59:10 +02:00
Patrick Lühne d0debc6ad1
Split predicates from their declarations
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-27 17:55:59 +02:00
Patrick Lühne 3ba80e8c9d
Minor refactoring 2018-04-27 17:38:29 +02:00
Patrick Lühne d66d3557c1
Minor refactoring 2018-04-27 17:25:43 +02:00
Patrick Lühne e15a6b2e88
Remove Constant class
Constants are not a construct present in Clingo’s AST and were
unintentionally made part of anthem’s AST. This removes the unused
classes for clarity.
2018-04-27 17:08:41 +02:00
Patrick Lühne 9a59ac17f5
Version bump after release 0.1.8 2018-04-20 16:37:03 +02:00
Patrick Lühne 250942643c
Version bump for release 0.1.8 2018-04-20 16:35:35 +02:00
Patrick Lühne 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
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 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
Patrick Lühne 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
Patrick Lühne a01e78a467
Add example program for prime number detection 2018-04-11 21:42:08 +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 b63ef21849
Add example program generating permutations 2018-04-11 21:35:29 +02:00
Patrick Lühne cc3c9b642c
Minor formatting in graph coloring example 2018-04-11 21:35:04 +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 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
Patrick Lühne 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
Patrick Lühne 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
Patrick Lühne 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
Patrick Lühne 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
Patrick Lühne 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
Patrick Lühne 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
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 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
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
54 changed files with 3061 additions and 605 deletions

View File

@ -0,0 +1,9 @@
FROM archimg/base-devel:latest
ARG toolchain
RUN pacman -Sy
RUN pacman -S --noconfirm cmake git ninja re2c
RUN if [ "${toolchain}" = "clang" ]; then pacman -S --noconfirm clang; fi
VOLUME /app

View File

@ -0,0 +1,10 @@
FROM ubuntu:18.04
ARG toolchain
RUN apt-get update
RUN apt-get install -y bison cmake git ninja-build re2c
RUN if [ "${toolchain}" = "gcc" ]; then apt-get install -y g++; fi
RUN if [ "${toolchain}" = "clang" ]; then apt-get install -y clang; fi
VOLUME /app

17
.ci/ci.sh Executable file
View File

@ -0,0 +1,17 @@
#!/bin/bash
if [ "$1" = "gcc" ]
then
cxx=g++
cc=gcc
elif [ "$1" = "clang" ]
then
cxx=clang++
cc=clang
fi
git submodule update --init --recursive
mkdir -p build/debug
cd build/debug
cmake ../.. -GNinja -DANTHEM_BUILD_TESTS=ON -DCMAKE_CXX_COMPILER=${cxx} -DCMAKE_C_COMPILER=${cc}
ninja anthem-app && ninja run-tests

5
.gitmodules vendored
View File

@ -3,4 +3,7 @@
url = https://github.com/potassco/clingo
[submodule "lib/catch"]
path = lib/catch
url = https://github.com/philsquared/Catch
url = https://github.com/catchorg/Catch2
[submodule "lib/cxxopts"]
path = lib/cxxopts
url = https://github.com/jarro2783/cxxopts

View File

@ -1,47 +1,25 @@
# Use container-based distribution
sudo: false
language: c++
addons:
apt:
sources: &default_sources
- ubuntu-toolchain-r-test
- boost-latest
packages: &default_packages
- libboost-program-options1.55-dev
- libboost-iostreams1.55-dev
- libboost-system1.55-dev
- libboost-filesystem1.55-dev
- re2c
sudo: required
services:
- docker
matrix:
include:
- env: COMPILER_NAME=g++ _CXX=g++-5 _CC=gcc-5
- env: distribution=arch-latest toolchain=gcc
os: linux
language: cpp
addons:
apt:
sources:
- *default_sources
packages:
- *default_packages
- g++-5
- env: COMPILER_NAME=g++ _CXX=g++-6 _CC=gcc-6
- env: distribution=arch-latest toolchain=clang
os: linux
language: cpp
addons:
apt:
sources:
- *default_sources
packages:
- *default_packages
- g++-6
- env: distribution=ubuntu-18.04 toolchain=gcc
os: linux
language: cpp
- env: distribution=ubuntu-18.04 toolchain=clang
os: linux
language: cpp
before_install:
- docker build --build-arg toolchain=${toolchain} -t ${distribution} - < .ci/Dockerfile-${distribution}
script:
- if [[ "${TRAVIS_OS_NAME}" == "linux" ]]; then
CMAKE_URL="http://www.cmake.org/files/v3.7/cmake-3.7.0-Linux-x86_64.tar.gz";
mkdir cmake-bin && wget --quiet --no-check-certificate -O - ${CMAKE_URL} | tar --strip-components=1 -xz -C cmake-bin;
export PATH=${PWD}/cmake-bin/bin:${PATH};
fi
- git submodule update --init --recursive
- mkdir -p build/debug
- cd build/debug
- cmake ../.. -DCMAKE_BUILD_TYPE=Debug -DCMAKE_CXX_COMPILER=$_CXX -DCMAKE_C_COMPILER=$_CC -DANTHEM_BUILD_TESTS=ON
- make -j3 anthem-app && make -j3 run-tests
- docker run --mount source=$(pwd),target=/app,type=bind -w /app ${distribution} /bin/bash -c ".ci/ci.sh ${toolchain}"

View File

@ -2,9 +2,45 @@
## (unreleased)
## 0.1.9 (2018-05-04)
### Changes
* turns on completion and simplification by default, which can now be switched off with `--no-complete` and `--no-simplify`
### Features
* detection of integer variables and integer predicate parameters
* command-line option `--no-detect-integers` to disable integer variable detection
* new simplification rule applying to integer variables
* support for declaring functions integer with the `#external` directive
### Bug Fixes
* fixes incorrect translation of unsupported choice rules with multiple elements by returning an error instead
* fixes precedence of intervals by enclosing them in parentheses
## 0.1.8 (2018-04-20)
### Features
* more and advanced simplification rules
* adds support for exponentiation (power) and modulus (absolute value)
* new examples: prime numbers, permutation generator, and graph coloring (extended)
## 0.1.7 (2018-04-08)
### Features
* support for declaring placeholders with the `#external` directive
### Internal
* drops Boost dependency in favor of the header-only command-line option library [cxxopts](https://github.com/jarro2783/cxxopts)
## 0.1.6 (2017-06-12)
Features:
### Features
* unique IDs for all variables (user-defined variables are renamed)
* support for hiding predicates from completed output by using `#show` statements
@ -12,7 +48,7 @@ Features:
* command-line option `--parentheses` to fully parenthesize the output
* adds multiple example instances for experimenting
Bug Fixes:
### Bug Fixes
* adds missing error message when attempting to read inaccessible file
* removes unnecessary parentheses after simplification
@ -20,52 +56,52 @@ Bug Fixes:
## 0.1.5 (2017-05-04)
Bug Fixes:
### Bug Fixes
* fixes lost signs with negated 0-ary predicates
## 0.1.4 (2017-04-12)
Features:
### Features
* completion of input programs (optional)
* command-line option `--complete` to turn on completion
## 0.1.3 (2017-03-30)
Features:
### Features
* support for anonymous variables
Bug Fixes:
### Bug Fixes
* fixes incorrectly simplified rules with comparisons
* fixes misleading error message concerning negated, unsupported body literals
## 0.1.2 (2017-03-23)
Features:
### Features
* simplification of output formulas (optional)
* command-line option `--simplify` to turn on simplification
Bug Fixes:
### Bug Fixes
* fixes incorrectly translated choice rules with multiple elements in the head aggregate
Internal:
### Internal
* explicit syntax tree representation for first-order formulas
## 0.1.1 (2017-03-06)
Features:
### Features
* support for choice rules (without guards)
## 0.1.0 (2016-11-24)
Features:
### Features
* initial support for translating rules in *Essential Gringo* (excluding aggregates) to first-order logic formulas
* command-line option `--color` to autodetect, enable, or disable color output

View File

@ -7,7 +7,7 @@ option(ANTHEM_BUILD_STATIC "Build static binaries" OFF)
set(CMAKE_CXX_FLAGS "-Wall -Wextra -Wpedantic ${CMAKE_CXX_FLAGS}")
set(CMAKE_CXX_FLAGS_DEBUG "-g ${CMAKE_CXX_FLAGS_DEBUG}")
set(CMAKE_CXX_STANDARD 14)
set(CMAKE_CXX_STANDARD 17)
set(CMAKE_CXX_STANDARD_REQUIRED ON)
set(CMAKE_CXX_EXTENSIONS OFF)

View File

@ -1,6 +1,6 @@
# The MIT License (MIT)
Copyright © 20162017 Patrick Lühne
Copyright © 20162018 Patrick Lühne
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal

View File

@ -9,15 +9,17 @@
## Usage
```bash
$ anthem [--simplify] file...
$ anthem [--no-complete] [--no-simplify] [--no-detect-integers] file...
```
With the option `--simplify`, output formulas are simplified by applying several basic transformation rules.
By default, `anthem` performs Clarks completion on the translated formulas, detects which variables are integer, and simplifies the output by applying several basic transformation rules.
These processing steps can be turned off with the options `--no-complete`, `--no-simplify`, and `--no-detect-integers`.
## Building
`anthem` requires [CMake](https://cmake.org/) and [Boost](http://www.boost.org/) for building.
After installing the dependencies, `anthem` is built with a C++14 compiler (GCC ≥ 6.1 or clang ≥ 3.8).
`anthem` requires [CMake](https://cmake.org/) for building.
After installing the dependencies, `anthem` is built with a C++17 compiler (GCC ≥ 7.3 or clang ≥ 5.0).
```bash
$ git clone https://github.com/potassco/anthem.git

View File

@ -1,7 +1,5 @@
set(target anthem-app)
find_package(Boost 1.55.0 COMPONENTS program_options system filesystem REQUIRED)
file(GLOB core_sources "*.cpp")
file(GLOB core_headers "*.h")
@ -11,11 +9,10 @@ set(sources
)
set(includes
${Boost_INCLUDE_DIRS}
${PROJECT_SOURCE_DIR}/lib/cxxopts/include
)
set(libraries
${Boost_LIBRARIES}
anthem
)

View File

@ -1,6 +1,6 @@
#include <iostream>
#include <boost/program_options.hpp>
#include <cxxopts.hpp>
#include <anthem/AST.h>
#include <anthem/Context.h>
@ -10,63 +10,72 @@ int main(int argc, char **argv)
{
anthem::Context context;
namespace po = boost::program_options;
cxxopts::Options options("anthem", "Translate ASP programs to the language of first-order theorem provers.");
po::options_description description("Allowed options");
description.add_options()
("help,h", "Display this help message")
("version,v", "Display version information")
("input,i", po::value<std::vector<std::string>>(), "Input files")
("simplify,s", po::bool_switch(&context.performSimplification), "Simplify the output")
("complete,c", po::bool_switch(&context.performCompletion), "Perform completion")
("color", po::value<std::string>()->default_value("auto"), "Colorize output (always, never, auto)")
("parentheses", po::value<std::string>()->default_value("normal"), "Parenthesis style (normal, full)")
("log-priority,p", po::value<std::string>()->default_value("warning"), "Log messages starting from this priority (debug, info, warning, error)");
options.add_options()
("h,help", "Display this help message")
("v,version", "Display version information")
("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
("no-simplify", "Do not simplify the output")
("no-complete", "Do not perform completion")
("no-detect-integers", "Do not detect integer variables")
("color", "Colorize output (always, never, auto)", cxxopts::value<std::string>()->default_value("auto"))
("parentheses", "Parenthesis style (normal, full)", cxxopts::value<std::string>()->default_value("normal"))
("p,log-priority", "Log messages starting from this priority (debug, info, warning, error)", cxxopts::value<std::string>()->default_value("info"));
po::positional_options_description positionalOptionsDescription;
positionalOptionsDescription.add("input", -1);
po::variables_map variablesMap;
options.parse_positional("input");
options.positional_help("[<input file...>]");
const auto printHelp =
[&]()
{
std::cout
<< "Usage: anthem [options] file..." << std::endl
<< "Translate ASP programs to the language of first-order theorem provers." << std::endl << std::endl
<< description;
std::cout << options.help();
};
bool help;
bool version;
std::vector<std::string> inputFiles;
std::string colorPolicyString;
std::string parenthesisStyleString;
std::string logPriorityString;
try
{
po::store(po::command_line_parser(argc, argv)
.options(description)
.positional(positionalOptionsDescription)
.run(),
variablesMap);
po::notify(variablesMap);
const auto parseResult = options.parse(argc, argv);
help = (parseResult.count("help") > 0);
version = (parseResult.count("version") > 0);
if (parseResult.count("input") > 0)
inputFiles = parseResult["input"].as<std::vector<std::string>>();
context.performSimplification = (parseResult.count("no-simplify") == 0);
context.performCompletion = (parseResult.count("no-complete") == 0);
context.performIntegerDetection = (parseResult.count("no-detect-integers") == 0);
colorPolicyString = parseResult["color"].as<std::string>();
parenthesisStyleString = parseResult["parentheses"].as<std::string>();
logPriorityString = parseResult["log-priority"].as<std::string>();
}
catch (const po::error &e)
catch (const std::exception &exception)
{
context.logger.log(anthem::output::Priority::Error) << e.what();
context.logger.log(anthem::output::Priority::Error) << exception.what();
context.logger.errorStream() << std::endl;
printHelp();
return EXIT_FAILURE;
}
if (variablesMap.count("help"))
if (help)
{
printHelp();
return EXIT_SUCCESS;
}
if (variablesMap.count("version"))
if (version)
{
std::cout << "anthem version 0.1.7-git" << std::endl;
std::cout << "anthem version 0.1.9+git" << std::endl;
return EXIT_SUCCESS;
}
const auto colorPolicyString = variablesMap["color"].as<std::string>();
if (colorPolicyString == "auto")
context.logger.setColorPolicy(anthem::output::ColorStream::ColorPolicy::Auto);
else if (colorPolicyString == "never")
@ -81,22 +90,18 @@ int main(int argc, char **argv)
return EXIT_FAILURE;
}
const auto parenthesisStyle = variablesMap["parentheses"].as<std::string>();
if (parenthesisStyle == "normal")
if (parenthesisStyleString == "normal")
context.parenthesisStyle = anthem::ast::ParenthesisStyle::Normal;
else if (parenthesisStyle == "full")
else if (parenthesisStyleString == "full")
context.parenthesisStyle = anthem::ast::ParenthesisStyle::Full;
else
{
context.logger.log(anthem::output::Priority::Error) << "unknown parenthesis style “" << parenthesisStyle << "";
context.logger.log(anthem::output::Priority::Error) << "unknown parenthesis style “" << parenthesisStyleString << "";
context.logger.errorStream() << std::endl;
printHelp();
return EXIT_FAILURE;
}
const auto logPriorityString = variablesMap["log-priority"].as<std::string>();
try
{
const auto logPriority = anthem::output::priorityFromName(logPriorityString.c_str());
@ -112,11 +117,8 @@ int main(int argc, char **argv)
try
{
if (variablesMap.count("input"))
{
const auto &inputFiles = variablesMap["input"].as<std::vector<std::string>>();
if (!inputFiles.empty())
anthem::translate(inputFiles, context);
}
else
anthem::translate("std::cin", std::cin, context);
}

2
examples/choice-rules.lp Normal file
View File

@ -0,0 +1,2 @@
p(a).
{q(a)}.

View File

@ -1,12 +1,18 @@
colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).
colored(V, green) :- vertex(V), not colored(V, red), not colored(V, blue).
colored(V, blue) :- vertex(V), not colored(V, red), not colored(V, green).
% assign a set of colors to each vertex
{color(V, C)} :- vertex(V), color(C).
:- edge(V1, V2), colored(V1, C), colored(V2, C).
% at most one color per vertex
:- color(V, C1), color(V, C2), C1 != C2.
vertex(a).
vertex(b).
vertex(c).
% at least one color per vertex
covered(V) :- color(V, _).
:- vertex(V), not covered(V).
edge(a, b).
edge(a, c).
% adjacent vertices dont share the same color
:- color(V1, C), color(V2, C), edge(V1, V2).
#show color/2.
#external vertex(1).
#external edge(2).
#external color(1).

11
examples/letters.lp Normal file
View File

@ -0,0 +1,11 @@
letter(a).
letter(b).
letter(c).
{p(1..3, Y)} :- letter(Y).
:- p(X1, Y), p(X2, Y), X1 != X2.
q(X) :- p(X, _).
:- X = 1..3, not q(X).
#show p/2.

12
examples/permutations.lp Normal file
View File

@ -0,0 +1,12 @@
#show p/2.
{p(1..n, 1..n)}.
:- p(X, Y1), p(X, Y2), Y1 != Y2.
:- p(X1, Y), p(X2, Y), X1 != X2.
q1(X) :- p(X, _).
q2(Y) :- p(_, Y).
:- not q1(X), X = 1..n.
:- not q2(Y), Y = 1..n.

4
examples/prime.lp Normal file
View File

@ -0,0 +1,4 @@
#show prime/1.
composite(I * J) :- I = 2..n, J = 2..n.
prime(N) :- N = 2..n, not composite(N).

View File

@ -1,3 +1,5 @@
#show in/2.
{in(1..n, 1..r)}.
covered(I) :- in(I, S).

View File

@ -0,0 +1,9 @@
s(X) :- p(X).
s(X) :- q(X).
u(X) :- r(X), not s(X).
#show u/1.
#external p(1).
#external q(1).
#external r(1).

View File

@ -0,0 +1,5 @@
s(X) :- p(X).
s(X) :- q(X).
#external p(1).
#external q(1).

View File

@ -2,6 +2,7 @@
#define __ANTHEM__AST_H
#include <anthem/ASTForward.h>
#include <anthem/Utils.h>
namespace anthem
{
@ -32,7 +33,8 @@ struct BinaryOperation
Minus,
Multiplication,
Division,
Modulo
Modulo,
Power
};
explicit BinaryOperation(Operator operator_, Term &&left, Term &&right)
@ -102,32 +104,15 @@ struct Comparison
////////////////////////////////////////////////////////////////////////////////////////////////////
struct Constant
{
explicit Constant(std::string &&name)
: name{std::move(name)}
{
}
Constant(const Constant &other) = delete;
Constant &operator=(const Constant &other) = delete;
Constant(Constant &&other) = default;
Constant &operator=(Constant &&other) = default;
std::string name;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct Function
{
explicit Function(std::string &&name)
: name{std::move(name)}
explicit Function(FunctionDeclaration *declaration)
: declaration{declaration}
{
}
explicit Function(std::string &&name, std::vector<Term> &&arguments)
: name{std::move(name)},
explicit Function(FunctionDeclaration *declaration, std::vector<Term> &&arguments)
: declaration{declaration},
arguments{std::move(arguments)}
{
}
@ -137,12 +122,37 @@ struct Function
Function(Function &&other) noexcept = default;
Function &operator=(Function &&other) noexcept = default;
std::string name;
FunctionDeclaration *declaration;
std::vector<Term> arguments;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct FunctionDeclaration
{
explicit FunctionDeclaration(std::string &&name)
: name{std::move(name)}
{
}
explicit FunctionDeclaration(std::string &&name, size_t arity)
: name{std::move(name)},
arity{arity}
{
}
FunctionDeclaration(const FunctionDeclaration &other) = delete;
FunctionDeclaration &operator=(const FunctionDeclaration &other) = delete;
FunctionDeclaration(FunctionDeclaration &&other) noexcept = default;
FunctionDeclaration &operator=(FunctionDeclaration &&other) noexcept = default;
std::string name;
size_t arity;
Domain domain{Domain::Noninteger};
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// TODO: refactor (limit element type to primitive terms)
struct In
{
@ -203,13 +213,13 @@ struct Interval
struct Predicate
{
explicit Predicate(std::string &&name)
: name{std::move(name)}
explicit Predicate(PredicateDeclaration *declaration)
: declaration{declaration}
{
}
explicit Predicate(std::string &&name, std::vector<Term> &&arguments)
: name{std::move(name)},
explicit Predicate(PredicateDeclaration *declaration, std::vector<Term> &&arguments)
: declaration{declaration},
arguments{std::move(arguments)}
{
}
@ -219,35 +229,47 @@ struct Predicate
Predicate(Predicate &&other) noexcept = default;
Predicate &operator=(Predicate &&other) noexcept = default;
std::size_t arity() const
{
return arguments.size();
}
std::string name;
PredicateDeclaration *declaration{nullptr};
std::vector<Term> arguments;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// TODO: make more use of this class
struct PredicateSignature
struct PredicateDeclaration
{
explicit PredicateSignature(std::string &&name, size_t arity)
enum class Visibility
{
Default,
Visible,
Hidden
};
struct Parameter
{
Domain domain{Domain::Unknown};
};
explicit PredicateDeclaration(std::string &&name, size_t arity)
: name{std::move(name)},
arity{arity}
parameters{std::vector<Parameter>(arity)}
{
}
PredicateSignature(const PredicateSignature &other) = delete;
PredicateSignature &operator=(const PredicateSignature &other) = delete;
// TODO: make noexcept again
// GCC versions before 7 dont declare moving std::string noexcept and would complain here
PredicateSignature(PredicateSignature &&other) = default;
PredicateSignature &operator=(PredicateSignature &&other) = default;
PredicateDeclaration(const PredicateDeclaration &other) = delete;
PredicateDeclaration &operator=(const PredicateDeclaration &other) = delete;
PredicateDeclaration(PredicateDeclaration &&other) noexcept = default;
PredicateDeclaration &operator=(PredicateDeclaration &&other) noexcept = default;
size_t arity() const noexcept
{
return parameters.size();
}
std::string name;
size_t arity;
std::vector<Parameter> parameters;
bool isUsed{false};
bool isExternal{false};
Visibility visibility{Visibility::Default};
};
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -292,6 +314,30 @@ struct String
////////////////////////////////////////////////////////////////////////////////////////////////////
struct UnaryOperation
{
enum class Operator
{
Absolute
};
explicit UnaryOperation(Operator operator_, Term &&argument)
: operator_{operator_},
argument{std::move(argument)}
{
}
UnaryOperation(const UnaryOperation &other) = delete;
UnaryOperation &operator=(const UnaryOperation &other) = delete;
UnaryOperation(UnaryOperation &&other) noexcept = default;
UnaryOperation &operator=(UnaryOperation &&other) noexcept = default;
Operator operator_;
Term argument;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct Variable
{
explicit Variable(VariableDeclaration *declaration)
@ -335,6 +381,7 @@ struct VariableDeclaration
VariableDeclaration &operator=(VariableDeclaration &&other) = default;
Type type;
Domain domain{Domain::Unknown};
std::string name;
};

View File

@ -22,7 +22,6 @@ namespace ast
BinaryOperation prepareCopy(const BinaryOperation &other);
Boolean prepareCopy(const Boolean &other);
Comparison prepareCopy(const Comparison &other);
Constant prepareCopy(const Constant &other);
Function prepareCopy(const Function &other);
In prepareCopy(const In &other);
Integer prepareCopy(const Integer &other);

View File

@ -24,10 +24,10 @@ struct BinaryOperation;
struct Biconditional;
struct Boolean;
struct Comparison;
struct Constant;
struct Exists;
struct ForAll;
struct Function;
struct FunctionDeclaration;
struct Implies;
struct In;
struct Integer;
@ -35,8 +35,10 @@ struct Interval;
struct Not;
struct Or;
struct Predicate;
struct PredicateDeclaration;
struct SpecialInteger;
struct String;
struct UnaryOperation;
struct Variable;
struct VariableDeclaration;
using VariableDeclarationPointer = std::unique_ptr<VariableDeclaration>;
@ -62,12 +64,12 @@ using Formula = Clingo::Variant<
using Term = Clingo::Variant<
BinaryOperation,
Boolean,
Constant,
Function,
Integer,
Interval,
SpecialInteger,
String,
UnaryOperation,
Variable>;
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -1,10 +1,11 @@
#ifndef __ANTHEM__AST_UTILS_H
#define __ANTHEM__AST_UTILS_H
#include <experimental/optional>
#include <optional>
#include <anthem/AST.h>
#include <anthem/ASTVisitors.h>
#include <anthem/Context.h>
namespace anthem
{
@ -28,19 +29,13 @@ class VariableStack
void push(Layer layer);
void pop();
std::experimental::optional<VariableDeclaration *> findUserVariableDeclaration(const char *variableName) const;
std::optional<VariableDeclaration *> findUserVariableDeclaration(const char *variableName) const;
bool contains(const VariableDeclaration &variableDeclaration) const;
private:
std::vector<Layer> m_layers;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
bool matches(const Predicate &lhs, const Predicate &rhs);
bool matches(const Predicate &predicate, const PredicateSignature &signature);
bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs);
void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures);
////////////////////////////////////////////////////////////////////////////////////////////////////
// Replacing Variables
@ -95,6 +90,21 @@ struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor<ReplaceV
////////////////////////////////////////////////////////////////////////////////////////////////////
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// Accessing Variable Domains
////////////////////////////////////////////////////////////////////////////////////////////////////
struct DefaultVariableDomainAccessor
{
Domain operator()(const ast::Variable &variable)
{
return variable.declaration->domain;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
}
#endif

View File

@ -123,12 +123,6 @@ struct RecursiveTermVisitor
return T::accept(boolean, term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
ReturnType visit(Constant &constant, Term &term, Arguments &&... arguments)
{
return T::accept(constant, term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
ReturnType visit(Function &function, Term &term, Arguments &&... arguments)
{
@ -165,6 +159,14 @@ struct RecursiveTermVisitor
return T::accept(string, term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
ReturnType visit(UnaryOperation &unaryOperation, Term &term, Arguments &&... arguments)
{
unaryOperation.argument.accept(*this, unaryOperation.argument, std::forward<Arguments>(arguments)...);
return T::accept(unaryOperation, term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
ReturnType visit(Variable &variable, Term &term, Arguments &&... arguments)
{

View File

@ -43,19 +43,22 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp
struct BodyTermTranslateVisitor
{
// TODO: refactor
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, ast::VariableStack &variableStack)
std::optional<ast::Formula> visit(const Clingo::AST::Function &function,
const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext,
Context &context, ast::VariableStack &variableStack)
{
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
throw TranslationException(literal.location, "double-negated literals currently unsupported");
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size());
predicateDeclaration->isUsed = true;
if (function.arguments.empty())
{
auto predicate = ast::Formula::make<ast::Predicate>(std::string(function.name));
if (literal.sign == Clingo::AST::Sign::None)
return std::move(predicate);
return ast::Predicate(predicateDeclaration);
else if (literal.sign == Clingo::AST::Sign::Negation)
return ast::Formula::make<ast::Not>(std::move(predicate));
return ast::Formula::make<ast::Not>(ast::Predicate(predicateDeclaration));
}
// Create new body variable declarations
@ -73,12 +76,12 @@ struct BodyTermTranslateVisitor
for (size_t i = 0; i < function.arguments.size(); i++)
{
auto &argument = function.arguments[i];
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, variableStack)));
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, context, variableStack)));
}
variableStack.pop();
ast::Predicate predicate(std::string(function.name));
ast::Predicate predicate(predicateDeclaration);
predicate.arguments.reserve(function.arguments.size());
for (size_t i = 0; i < function.arguments.size(); i++)
@ -93,12 +96,13 @@ struct BodyTermTranslateVisitor
}
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &,
const Clingo::AST::Term &term, RuleContext &, Context &, ast::VariableStack &)
{
assert(!term.data.is<Clingo::AST::Function>());
throw TranslationException(term.location, "term currently unsupported in this context, expected function");
return std::experimental::nullopt;
return std::nullopt;
}
};
@ -106,18 +110,18 @@ struct BodyTermTranslateVisitor
struct BodyLiteralTranslateVisitor
{
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &)
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, ast::VariableStack &)
{
return ast::Formula::make<ast::Boolean>(boolean.value);
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
{
return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, variableStack);
return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, context, variableStack);
}
// TODO: refactor
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
{
// Comparisons should never have a sign, because these are converted to positive comparisons by clingo
if (literal.sign != Clingo::AST::Sign::None)
@ -132,18 +136,18 @@ struct BodyLiteralTranslateVisitor
ast::And conjunction;
conjunction.arguments.reserve(3);
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[0].get()), translate(comparison.left, ruleContext, variableStack)));
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[1].get()), translate(comparison.right, ruleContext, variableStack)));
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[0].get()), translate(comparison.left, ruleContext, context, variableStack)));
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[1].get()), translate(comparison.right, ruleContext, context, variableStack)));
conjunction.arguments.emplace_back(ast::Formula::make<ast::Comparison>(operator_, ast::Variable(parameters[0].get()), ast::Variable(parameters[1].get())));
return ast::Formula::make<ast::Exists>(std::move(parameters), std::move(conjunction));
}
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, ast::VariableStack &)
{
throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term");
return std::experimental::nullopt;
return std::nullopt;
}
};
@ -151,19 +155,19 @@ struct BodyLiteralTranslateVisitor
struct BodyBodyLiteralTranslateVisitor
{
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack)
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
{
if (bodyLiteral.sign != Clingo::AST::Sign::None)
throw TranslationException(bodyLiteral.location, "only positive body literals supported currently");
return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, variableStack);
return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, context, variableStack);
}
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, Context &, ast::VariableStack &)
{
throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal");
return std::experimental::nullopt;
return std::nullopt;
}
};

View File

@ -1,7 +1,7 @@
#ifndef __ANTHEM__CONTEXT_H
#define __ANTHEM__CONTEXT_H
#include <experimental/optional>
#include <optional>
#include <anthem/AST.h>
#include <anthem/output/Logger.h>
@ -16,6 +16,14 @@ namespace anthem
//
////////////////////////////////////////////////////////////////////////////////////////////////////
struct PredicateDeclarationMeta
{
ast::PredicateDeclaration *declaration;
bool used{false};
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct Context
{
Context() = default;
@ -25,12 +33,59 @@ struct Context
{
}
ast::PredicateDeclaration *findOrCreatePredicateDeclaration(const char *name, size_t arity)
{
const auto matchesExistingPredicateDeclaration =
[&](const auto &predicateDeclaration)
{
return (predicateDeclaration->arity() == arity
&& strcmp(predicateDeclaration->name.c_str(), name) == 0);
};
auto matchingPredicateDeclaration = std::find_if(predicateDeclarations.begin(),
predicateDeclarations.end(), matchesExistingPredicateDeclaration);
if (matchingPredicateDeclaration != predicateDeclarations.end())
return matchingPredicateDeclaration->get();
predicateDeclarations.emplace_back(std::make_unique<ast::PredicateDeclaration>(name, arity));
return predicateDeclarations.back().get();
}
ast::FunctionDeclaration *findOrCreateFunctionDeclaration(const char *name, size_t arity)
{
const auto matchesExistingFunctionDeclaration =
[&](const auto &functionDeclarations)
{
return (functionDeclarations->arity == arity
&& strcmp(functionDeclarations->name.c_str(), name) == 0);
};
auto matchingFunctionDeclaration = std::find_if(functionDeclarations.begin(),
functionDeclarations.end(), matchesExistingFunctionDeclaration);
if (matchingFunctionDeclaration != functionDeclarations.end())
return matchingFunctionDeclaration->get();
functionDeclarations.emplace_back(std::make_unique<ast::FunctionDeclaration>(name, arity));
return functionDeclarations.back().get();
}
output::Logger logger;
bool performSimplification = false;
bool performCompletion = false;
bool performSimplification{false};
bool performCompletion{false};
bool performIntegerDetection{false};
std::experimental::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations;
ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible};
std::vector<std::unique_ptr<ast::FunctionDeclaration>> functionDeclarations;
bool externalStatementsUsed{false};
bool showStatementsUsed{false};
ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
};

409
include/anthem/Equality.h Normal file
View File

@ -0,0 +1,409 @@
#ifndef __ANTHEM__EQUALITY_H
#define __ANTHEM__EQUALITY_H
#include <anthem/AST.h>
#include <anthem/ASTUtils.h>
#include <anthem/Utils.h>
namespace anthem
{
namespace ast
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Equality
//
////////////////////////////////////////////////////////////////////////////////////////////////////
Tristate equal(const Formula &lhs, const Formula &rhs);
Tristate equal(const Term &lhs, const Term &rhs);
////////////////////////////////////////////////////////////////////////////////////////////////////
struct FormulaEqualityVisitor
{
Tristate visit(const And &and_, const Formula &otherFormula)
{
if (!otherFormula.is<And>())
return Tristate::Unknown;
const auto &otherAnd = otherFormula.get<And>();
for (const auto &argument : and_.arguments)
{
const auto match = std::find_if(
otherAnd.arguments.cbegin(), otherAnd.arguments.cend(),
[&](const auto &otherArgument)
{
return equal(argument, otherArgument) == Tristate::True;
});
if (match == otherAnd.arguments.cend())
return Tristate::Unknown;
}
for (const auto &otherArgument : otherAnd.arguments)
{
const auto match = std::find_if(
and_.arguments.cbegin(), and_.arguments.cend(),
[&](const auto &argument)
{
return equal(otherArgument, argument) == Tristate::True;
});
if (match == and_.arguments.cend())
return Tristate::Unknown;
}
return Tristate::True;
}
Tristate visit(const Biconditional &biconditional, const Formula &otherFormula)
{
if (!otherFormula.is<Biconditional>())
return Tristate::Unknown;
const auto &otherBiconditional = otherFormula.get<Biconditional>();
if (equal(biconditional.left, otherBiconditional.left) == Tristate::True
&& equal(biconditional.right, otherBiconditional.right) == Tristate::True)
{
return Tristate::True;
}
if (equal(biconditional.left, otherBiconditional.right) == Tristate::True
&& equal(biconditional.right, otherBiconditional.left) == Tristate::True)
{
return Tristate::True;
}
return Tristate::Unknown;
}
Tristate visit(const Boolean &boolean, const Formula &otherFormula)
{
if (!otherFormula.is<Boolean>())
return Tristate::Unknown;
const auto &otherBoolean = otherFormula.get<Boolean>();
return (boolean.value == otherBoolean.value)
? Tristate::True
: Tristate::False;
}
Tristate visit(const Comparison &comparison, const Formula &otherFormula)
{
if (!otherFormula.is<Comparison>())
return Tristate::Unknown;
const auto &otherComparison = otherFormula.get<Comparison>();
if (comparison.operator_ != otherComparison.operator_)
return Tristate::Unknown;
if (equal(comparison.left, otherComparison.left) == Tristate::True
&& equal(comparison.right, otherComparison.right) == Tristate::True)
{
return Tristate::True;
}
// Only = and != are commutative operators, all others dont need to be checked with exchanged arguments
if (comparison.operator_ != Comparison::Operator::Equal
&& comparison.operator_ != Comparison::Operator::NotEqual)
{
return Tristate::Unknown;
}
if (equal(comparison.left, otherComparison.right) == Tristate::True
&& equal(comparison.right, otherComparison.left) == Tristate::True)
{
return Tristate::True;
}
return Tristate::Unknown;
}
Tristate visit(const Exists &, const Formula &otherFormula)
{
if (!otherFormula.is<Exists>())
return Tristate::Unknown;
// TODO: implement stronger check
return Tristate::Unknown;
}
Tristate visit(const ForAll &, const Formula &otherFormula)
{
if (!otherFormula.is<ForAll>())
return Tristate::Unknown;
// TODO: implement stronger check
return Tristate::Unknown;
}
Tristate visit(const Implies &implies, const Formula &otherFormula)
{
if (!otherFormula.is<Implies>())
return Tristate::Unknown;
const auto &otherImplies = otherFormula.get<Implies>();
if (equal(implies.antecedent, otherImplies.antecedent) == Tristate::True
&& equal(implies.consequent, otherImplies.consequent) == Tristate::True)
{
return Tristate::True;
}
return Tristate::Unknown;
}
Tristate visit(const In &in, const Formula &otherFormula)
{
if (!otherFormula.is<In>())
return Tristate::Unknown;
const auto &otherIn = otherFormula.get<In>();
if (equal(in.element, otherIn.element) == Tristate::True
&& equal(in.set, otherIn.set) == Tristate::True)
{
return Tristate::True;
}
return Tristate::Unknown;
}
Tristate visit(const Not &not_, const Formula &otherFormula)
{
if (!otherFormula.is<Not>())
return Tristate::Unknown;
const auto &otherNot = otherFormula.get<Not>();
return equal(not_.argument, otherNot.argument);
}
Tristate visit(const Or &or_, const Formula &otherFormula)
{
if (!otherFormula.is<Or>())
return Tristate::Unknown;
const auto &otherOr = otherFormula.get<Or>();
for (const auto &argument : or_.arguments)
{
const auto match = std::find_if(
otherOr.arguments.cbegin(), otherOr.arguments.cend(),
[&](const auto &otherArgument)
{
return equal(argument, otherArgument) == Tristate::True;
});
if (match == otherOr.arguments.cend())
return Tristate::Unknown;
}
for (const auto &otherArgument : otherOr.arguments)
{
const auto match = std::find_if(
or_.arguments.cbegin(), or_.arguments.cend(),
[&](const auto &argument)
{
return equal(otherArgument, argument) == Tristate::True;
});
if (match == or_.arguments.cend())
return Tristate::Unknown;
}
return Tristate::True;
}
Tristate visit(const Predicate &predicate, const Formula &otherFormula)
{
if (!otherFormula.is<Predicate>())
return Tristate::Unknown;
const auto &otherPredicate = otherFormula.get<Predicate>();
if (predicate.declaration != otherPredicate.declaration)
return Tristate::False;
assert(predicate.arguments.size() == otherPredicate.arguments.size());
for (size_t i = 0; i < predicate.arguments.size(); i++)
if (equal(predicate.arguments[i], otherPredicate.arguments[i]) != Tristate::True)
return Tristate::Unknown;
return Tristate::True;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct TermEqualityVisitor
{
Tristate visit(const BinaryOperation &binaryOperation, const Term &otherTerm)
{
if (!otherTerm.is<BinaryOperation>())
return Tristate::Unknown;
const auto &otherBinaryOperation = otherTerm.get<BinaryOperation>();
if (binaryOperation.operator_ != otherBinaryOperation.operator_)
return Tristate::Unknown;
if (equal(binaryOperation.left, otherBinaryOperation.left) == Tristate::True
&& equal(binaryOperation.right, otherBinaryOperation.right) == Tristate::True)
{
return Tristate::True;
}
// Only + and * are commutative operators, all others dont need to be checked with exchanged arguments
if (binaryOperation.operator_ != BinaryOperation::Operator::Plus
&& binaryOperation.operator_ != BinaryOperation::Operator::Multiplication)
{
return Tristate::Unknown;
}
if (equal(binaryOperation.left, otherBinaryOperation.right) == Tristate::True
&& equal(binaryOperation.right, otherBinaryOperation.left) == Tristate::True)
{
return Tristate::True;
}
return Tristate::Unknown;
}
Tristate visit(const Boolean &boolean, const Term &otherTerm)
{
if (!otherTerm.is<Boolean>())
return Tristate::Unknown;
const auto &otherBoolean = otherTerm.get<Boolean>();
return (boolean.value == otherBoolean.value)
? Tristate::True
: Tristate::False;
}
Tristate visit(const Function &function, const Term &otherTerm)
{
if (!otherTerm.is<Function>())
return Tristate::Unknown;
const auto &otherFunction = otherTerm.get<Function>();
if (function.declaration != otherFunction.declaration)
return Tristate::False;
if (function.arguments.size() != otherFunction.arguments.size())
return Tristate::False;
for (size_t i = 0; i < function.arguments.size(); i++)
if (equal(function.arguments[i], otherFunction.arguments[i]) != Tristate::True)
return Tristate::Unknown;
return Tristate::True;
}
Tristate visit(const Integer &integer, const Term &otherTerm)
{
if (!otherTerm.is<Integer>())
return Tristate::Unknown;
const auto &otherInteger = otherTerm.get<Integer>();
return (integer.value == otherInteger.value)
? Tristate::True
: Tristate::False;
}
Tristate visit(const Interval &interval, const Term &otherTerm)
{
if (!otherTerm.is<Interval>())
return Tristate::Unknown;
const auto &otherInterval = otherTerm.get<Interval>();
if (equal(interval.from, otherInterval.from) != Tristate::True)
return Tristate::Unknown;
if (equal(interval.to, otherInterval.to) != Tristate::True)
return Tristate::Unknown;
return Tristate::True;
}
Tristate visit(const SpecialInteger &specialInteger, const Term &otherTerm)
{
if (!otherTerm.is<SpecialInteger>())
return Tristate::Unknown;
const auto &otherSpecialInteger = otherTerm.get<SpecialInteger>();
return (specialInteger.type == otherSpecialInteger.type)
? Tristate::True
: Tristate::False;
}
Tristate visit(const String &string, const Term &otherTerm)
{
if (!otherTerm.is<String>())
return Tristate::Unknown;
const auto &otherString = otherTerm.get<String>();
return (string.text == otherString.text)
? Tristate::True
: Tristate::False;
}
Tristate visit(const UnaryOperation &unaryOperation, const Term &otherTerm)
{
if (!otherTerm.is<UnaryOperation>())
return Tristate::Unknown;
const auto &otherUnaryOperation = otherTerm.get<UnaryOperation>();
if (unaryOperation.operator_ != otherUnaryOperation.operator_)
return Tristate::Unknown;
return equal(unaryOperation.argument, otherUnaryOperation.argument);
}
Tristate visit(const Variable &variable, const Term &otherTerm)
{
if (!otherTerm.is<Variable>())
return Tristate::Unknown;
const auto &otherVariable = otherTerm.get<Variable>();
return (variable.declaration == otherVariable.declaration)
? Tristate::True
: Tristate::False;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
Tristate equal(const Formula &lhs, const Formula &rhs)
{
return lhs.accept(FormulaEqualityVisitor(), rhs);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
Tristate equal(const Term &lhs, const Term &rhs)
{
return lhs.accept(TermEqualityVisitor(), rhs);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}
}
#endif

244
include/anthem/Evaluation.h Normal file
View File

@ -0,0 +1,244 @@
#ifndef __ANTHEM__EVALUATION_H
#define __ANTHEM__EVALUATION_H
#include <anthem/AST.h>
#include <anthem/ASTUtils.h>
#include <anthem/Utils.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Evaluation
//
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class VariableDomainAccessor = DefaultVariableDomainAccessor>
struct EvaluateFormulaVisitor
{
template <class... Arguments>
static EvaluationResult visit(const ast::And &and_, Arguments &&... arguments)
{
bool someFalse = false;
bool someUnknown = false;
for (const auto &argument : and_.arguments)
{
const auto result = evaluate(argument, std::forward<Arguments>(arguments)...);
switch (result)
{
case EvaluationResult::Error:
return EvaluationResult::Error;
case EvaluationResult::True:
break;
case EvaluationResult::False:
someFalse = true;
break;
case EvaluationResult::Unknown:
someUnknown = true;
break;
}
}
if (someFalse)
return EvaluationResult::False;
if (someUnknown)
return EvaluationResult::Unknown;
return EvaluationResult::True;
}
template <class... Arguments>
static EvaluationResult visit(const ast::Biconditional &biconditional, Arguments &&... arguments)
{
const auto leftResult = evaluate(biconditional.left, std::forward<Arguments>(arguments)...);
const auto rightResult = evaluate(biconditional.right, std::forward<Arguments>(arguments)...);
if (leftResult == EvaluationResult::Error || rightResult == EvaluationResult::Error)
return EvaluationResult::Error;
if (leftResult == EvaluationResult::Unknown || rightResult == EvaluationResult::Unknown)
return EvaluationResult::Unknown;
return (leftResult == rightResult ? EvaluationResult::True : EvaluationResult::False);
}
template <class... Arguments>
static EvaluationResult visit(const ast::Boolean &boolean, Arguments &&...)
{
return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False);
}
template <class... Arguments>
static EvaluationResult visit(const ast::Comparison &comparison, Arguments &&... arguments)
{
const auto leftType = type(comparison.left, std::forward<Arguments>(arguments)...);
const auto rightType = type(comparison.right, std::forward<Arguments>(arguments)...);
// Comparisons with empty sets always return false
if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
return EvaluationResult::False;
// If either side has an unknown domain, the result is unknown
if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
return EvaluationResult::Unknown;
// If both sides have the same domain, the result is unknown
if (leftType.domain == rightType.domain)
return EvaluationResult::Unknown;
// If one side is integer, but the other one isnt, they are not equal
switch (comparison.operator_)
{
case ast::Comparison::Operator::Equal:
return EvaluationResult::False;
case ast::Comparison::Operator::NotEqual:
return EvaluationResult::True;
default:
// TODO: implement more cases
return EvaluationResult::Unknown;
}
}
template <class... Arguments>
static EvaluationResult visit(const ast::Exists &exists, Arguments &&... arguments)
{
return evaluate(exists.argument, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
static EvaluationResult visit(const ast::ForAll &forAll, Arguments &&... arguments)
{
return evaluate(forAll.argument, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
static EvaluationResult visit(const ast::Implies &implies, Arguments &&... arguments)
{
const auto antecedentResult = evaluate(implies.antecedent, std::forward<Arguments>(arguments)...);
const auto consequentResult = evaluate(implies.consequent, std::forward<Arguments>(arguments)...);
if (antecedentResult == EvaluationResult::Error || consequentResult == EvaluationResult::Error)
return EvaluationResult::Error;
if (antecedentResult == EvaluationResult::False)
return EvaluationResult::True;
if (consequentResult == EvaluationResult::True)
return EvaluationResult::True;
if (antecedentResult == EvaluationResult::True && consequentResult == EvaluationResult::False)
return EvaluationResult::False;
return EvaluationResult::Unknown;
}
template <class... Arguments>
static EvaluationResult visit(const ast::In &in, Arguments &&... arguments)
{
const auto elementType = type(in.element, std::forward<Arguments>(arguments)...);
const auto setType = type(in.set, std::forward<Arguments>(arguments)...);
// The element to test shouldnt be empty or a proper set by itself
assert(elementType.setSize != SetSize::Empty && elementType.setSize != SetSize::Multi);
// If the set is empty, no element can be selected
if (setType.setSize == SetSize::Empty)
return EvaluationResult::False;
// If one of the sides has an unknown type, the result is unknown
if (elementType.domain == Domain::Unknown || setType.domain == Domain::Unknown)
return EvaluationResult::Unknown;
// If both sides have the same domain, the result is unknown
if (elementType.domain == setType.domain)
return EvaluationResult::Unknown;
// If one side is integer, but the other one isnt, set inclusion is never satisfied
return EvaluationResult::False;
}
template <class... Arguments>
static EvaluationResult visit(const ast::Not &not_, Arguments &&... arguments)
{
const auto result = evaluate(not_.argument, std::forward<Arguments>(arguments)...);
if (result == EvaluationResult::Error || result == EvaluationResult::Unknown)
return result;
return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True);
}
template <class... Arguments>
static EvaluationResult visit(const ast::Or &or_, Arguments &&... arguments)
{
bool someTrue = false;
bool someUnknown = false;
for (const auto &argument : or_.arguments)
{
const auto result = evaluate(argument, std::forward<Arguments>(arguments)...);
switch (result)
{
case EvaluationResult::Error:
return EvaluationResult::Error;
case EvaluationResult::True:
someTrue = true;
break;
case EvaluationResult::False:
break;
case EvaluationResult::Unknown:
someUnknown = true;
break;
}
}
if (someTrue)
return EvaluationResult::True;
if (someUnknown)
return EvaluationResult::Unknown;
return EvaluationResult::False;
}
template <class... Arguments>
static EvaluationResult visit(const ast::Predicate &predicate, Arguments &&... arguments)
{
assert(predicate.arguments.size() == predicate.declaration->arity());
for (size_t i = 0; i < predicate.arguments.size(); i++)
{
const auto &argument = predicate.arguments[i];
const auto &parameter = predicate.declaration->parameters[i];
if (parameter.domain != Domain::Integer)
continue;
const auto argumentType = type(argument, std::forward<Arguments>(arguments)...);
if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
return EvaluationResult::Error;
}
return EvaluationResult::Unknown;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
EvaluationResult evaluate(const ast::Formula &formula, Arguments &&... arguments)
{
return formula.accept(EvaluateFormulaVisitor<VariableDomainAccessor>(), std::forward<Arguments>(arguments)...);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}
#endif

View File

@ -2,7 +2,7 @@
#define __ANTHEM__HEAD_H
#include <algorithm>
#include <experimental/optional>
#include <optional>
#include <anthem/AST.h>
#include <anthem/Exception.h>
@ -118,8 +118,7 @@ struct HeadLiteralCollectFunctionTermsVisitor
struct FunctionTermTranslateVisitor
{
// TODO: check correctness
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex)
std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
{
if (function.external)
throw TranslationException(term.location, "external functions currently unsupported");
@ -130,14 +129,17 @@ struct FunctionTermTranslateVisitor
for (size_t i = 0; i < function.arguments.size(); i++)
arguments.emplace_back(ast::Variable(ruleContext.freeVariables[headVariableIndex++].get()));
return ast::Formula::make<ast::Predicate>(function.name, std::move(arguments));
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size());
predicateDeclaration->isUsed = true;
return ast::Predicate(predicateDeclaration, std::move(arguments));
}
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, Context &, size_t &)
{
throw TranslationException(term.location, "term currently unsupported in this context, function expected");
return std::experimental::nullopt;
return std::nullopt;
}
};
@ -145,21 +147,21 @@ struct FunctionTermTranslateVisitor
struct LiteralTranslateVisitor
{
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &)
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, size_t &)
{
return ast::Formula::make<ast::Boolean>(boolean.value);
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, size_t &headVariableIndex)
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
{
return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, headVariableIndex);
return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, context, headVariableIndex);
}
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, size_t &)
{
throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals");
return std::experimental::nullopt;
return std::nullopt;
}
};
@ -167,23 +169,23 @@ struct LiteralTranslateVisitor
struct HeadLiteralTranslateToConsequentVisitor
{
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex)
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
{
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
throw TranslationException(literal.location, "double-negated head literals currently unsupported");
auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, headVariableIndex);
auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, context, headVariableIndex);
if (literal.sign == Clingo::AST::Sign::None)
return translatedLiteral;
if (!translatedLiteral)
return std::experimental::nullopt;
return std::nullopt;
return ast::Formula::make<ast::Not>(std::move(translatedLiteral.value()));
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
std::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
{
std::vector<ast::Formula> arguments;
arguments.reserve(disjunction.elements.size());
@ -193,7 +195,7 @@ struct HeadLiteralTranslateToConsequentVisitor
if (!conditionalLiteral.condition.empty())
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
if (!argument)
throw TranslationException(headLiteral.location, "could not parse argument");
@ -204,7 +206,7 @@ struct HeadLiteralTranslateToConsequentVisitor
return ast::Formula::make<ast::Or>(std::move(arguments));
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
std::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
{
if (aggregate.left_guard || aggregate.right_guard)
throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported");
@ -215,7 +217,7 @@ struct HeadLiteralTranslateToConsequentVisitor
if (!conditionalLiteral.condition.empty())
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
};
if (aggregate.elements.size() == 1)
@ -238,10 +240,10 @@ struct HeadLiteralTranslateToConsequentVisitor
}
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, Context &, size_t &)
{
throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate");
return std::experimental::nullopt;
return std::nullopt;
}
};

View File

@ -13,7 +13,7 @@ namespace anthem
//
////////////////////////////////////////////////////////////////////////////////////////////////////
void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context);
void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context);
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -0,0 +1,22 @@
#ifndef __ANTHEM__INTEGER_VARIABLE_DETECTION_H
#define __ANTHEM__INTEGER_VARIABLE_DETECTION_H
#include <anthem/AST.h>
#include <anthem/Context.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// IntegerVariableDetection
//
////////////////////////////////////////////////////////////////////////////////////////////////////
void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas);
////////////////////////////////////////////////////////////////////////////////////////////////////
}
#endif

View File

@ -0,0 +1,193 @@
#ifndef __ANTHEM__SIMPLIFICATION_VISITORS_H
#define __ANTHEM__SIMPLIFICATION_VISITORS_H
#include <anthem/AST.h>
#include <anthem/Simplification.h>
#include <anthem/Utils.h>
namespace anthem
{
namespace ast
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Simplification Visitor
//
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class T>
struct FormulaSimplificationVisitor
{
template <class... Arguments>
OperationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
{
for (auto &argument : and_.arguments)
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
{
if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
{
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
{
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
{
if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
{
if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
{
if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(In &, Formula &formula, Arguments &&... arguments)
{
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Not &not_, Formula &formula, Arguments &&... arguments)
{
if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
{
for (auto &argument : or_.arguments)
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
{
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class T, class OperationResult = void>
struct TermSimplificationVisitor
{
template <class... Arguments>
OperationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
{
if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Boolean &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Function &function, Term &term, Arguments &&... arguments)
{
for (auto &argument : function.arguments)
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Integer &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
{
if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(String &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Variable &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
}
}
#endif

View File

@ -73,7 +73,7 @@ struct StatementVisitor
// Compute consequent
auto headVariableIndex = ruleContext.headVariablesStartIndex;
auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, headVariableIndex);
auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, context, headVariableIndex);
assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex);
@ -87,7 +87,7 @@ struct StatementVisitor
const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin();
auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get());
auto set = translate(headTerm, ruleContext, variableStack);
auto set = translate(headTerm, ruleContext, context, variableStack);
auto in = ast::In(std::move(element), std::move(set));
antecedent.arguments.emplace_back(std::move(in));
@ -98,7 +98,7 @@ struct StatementVisitor
{
const auto &bodyLiteral = *i;
auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, variableStack);
auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, context, variableStack);
if (!argument)
throw TranslationException(bodyLiteral.location, "could not translate body literal");
@ -165,8 +165,8 @@ struct StatementVisitor
if (signature.negative())
throw LogicException(statement.location, "negative #show atom signatures are currently unsupported");
if (!context.visiblePredicateSignatures)
context.visiblePredicateSignatures.emplace();
context.showStatementsUsed = true;
context.defaultPredicateVisibility = ast::PredicateDeclaration::Visibility::Hidden;
if (std::strlen(signature.name()) == 0)
{
@ -176,7 +176,8 @@ struct StatementVisitor
context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "";
context.visiblePredicateSignatures.value().emplace_back(std::string(signature.name()), signature.arity());
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(signature.name(), signature.arity());
predicateDeclaration->visibility = ast::PredicateDeclaration::Visibility::Visible;
}
void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
@ -184,6 +185,84 @@ struct StatementVisitor
throw LogicException(statement.location, "only #show statements for atoms (not terms) are supported currently");
}
void visit(const Clingo::AST::External &external, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &context)
{
const auto fail =
[&]()
{
throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>). or #external integer(<function name>(<arity>)). supported");
};
if (!external.body.empty())
fail();
if (!external.atom.data.is<Clingo::AST::Function>())
fail();
const auto &predicate = external.atom.data.get<Clingo::AST::Function>();
if (predicate.arguments.size() != 1)
fail();
const auto handleIntegerDeclaration =
[&]()
{
// Integer function declarations are treated separately if applicable
if (strcmp(predicate.name, "integer") != 0)
return false;
if (predicate.arguments.size() != 1)
return false;
const auto &functionArgument = predicate.arguments.front();
if (!functionArgument.data.is<Clingo::AST::Function>())
return false;
const auto &function = functionArgument.data.get<Clingo::AST::Function>();
if (function.arguments.size() != 1)
return false;
const auto &arityArgument = function.arguments.front();
if (!arityArgument.data.is<Clingo::Symbol>())
return false;
const auto &aritySymbol = arityArgument.data.get<Clingo::Symbol>();
if (aritySymbol.type() != Clingo::SymbolType::Number)
return false;
const size_t arity = aritySymbol.number();
auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, arity);
functionDeclaration->domain = Domain::Integer;
return true;
};
if (handleIntegerDeclaration())
return;
const auto &arityArgument = predicate.arguments.front();
if (!arityArgument.data.is<Clingo::Symbol>())
fail();
const auto &aritySymbol = arityArgument.data.get<Clingo::Symbol>();
if (aritySymbol.type() != Clingo::SymbolType::Number)
fail();
context.externalStatementsUsed = true;
const size_t arity = aritySymbol.number();
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(predicate.name, arity);
predicateDeclaration->isExternal = true;
}
template<class T>
void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
{

View File

@ -23,6 +23,12 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
{
switch (binaryOperator)
{
case Clingo::AST::BinaryOperator::XOr:
throw TranslationException(term.location, "binary operation “xor” currently unsupported");
case Clingo::AST::BinaryOperator::Or:
throw TranslationException(term.location, "binary operation “or” currently unsupported");
case Clingo::AST::BinaryOperator::And:
throw TranslationException(term.location, "binary operation “and” currently unsupported");
case Clingo::AST::BinaryOperator::Plus:
return ast::BinaryOperation::Operator::Plus;
case Clingo::AST::BinaryOperator::Minus:
@ -33,22 +39,39 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
return ast::BinaryOperation::Operator::Division;
case Clingo::AST::BinaryOperator::Modulo:
return ast::BinaryOperation::Operator::Modulo;
default:
throw TranslationException(term.location, "“binary operation” terms currently unsupported");
case Clingo::AST::BinaryOperator::Power:
return ast::BinaryOperation::Operator::Power;
}
return ast::BinaryOperation::Operator::Plus;
throw TranslationException(term.location, "unknown binary operation");
}
////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack);
ast::UnaryOperation::Operator translate(Clingo::AST::UnaryOperator unaryOperator, const Clingo::AST::Term &term)
{
switch (unaryOperator)
{
case Clingo::AST::UnaryOperator::Absolute:
return ast::UnaryOperation::Operator::Absolute;
case Clingo::AST::UnaryOperator::Minus:
throw TranslationException(term.location, "binary operation “minus” currently unsupported");
case Clingo::AST::UnaryOperator::Negation:
throw TranslationException(term.location, "binary operation “negation” currently unsupported");
}
throw TranslationException(term.location, "unknown unary operation");
}
////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack);
////////////////////////////////////////////////////////////////////////////////////////////////////
struct TermTranslateVisitor
{
std::experimental::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{
switch (symbol.type())
{
@ -62,29 +85,29 @@ struct TermTranslateVisitor
return ast::Term::make<ast::String>(std::string(symbol.string()));
case Clingo::SymbolType::Function:
{
auto function = ast::Term::make<ast::Function>(symbol.name());
// TODO: remove workaround
auto &functionRaw = function.get<ast::Function>();
functionRaw.arguments.reserve(symbol.arguments().size());
auto functionDeclaration = context.findOrCreateFunctionDeclaration(symbol.name(), symbol.arguments().size());
auto function = ast::Function(functionDeclaration);
function.arguments.reserve(symbol.arguments().size());
for (const auto &argument : symbol.arguments())
{
auto translatedArgument = visit(argument, term, ruleContext, variableStack);
auto translatedArgument = visit(argument, term, ruleContext, context, variableStack);
if (!translatedArgument)
throw TranslationException(term.location, "could not translate argument");
functionRaw.arguments.emplace_back(std::move(translatedArgument.value()));
function.arguments.emplace_back(std::move(translatedArgument.value()));
}
return std::move(function);
}
}
return std::experimental::nullopt;
return std::nullopt;
}
std::experimental::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, Context &, const ast::VariableStack &variableStack)
{
const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name);
const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0);
@ -97,33 +120,36 @@ struct TermTranslateVisitor
auto variableDeclaration = std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::UserDefined, std::string(variable.name));
ruleContext.freeVariables.emplace_back(std::move(variableDeclaration));
// TODO: ast::Term::make is unnecessary and can be removed
return ast::Term::make<ast::Variable>(ruleContext.freeVariables.back().get());
}
std::experimental::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
{
throw TranslationException(term.location, "“unary operation” terms currently unsupported");
return std::experimental::nullopt;
}
std::experimental::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{
const auto operator_ = translate(binaryOperation.binary_operator, term);
auto left = translate(binaryOperation.left, ruleContext, variableStack);
auto right = translate(binaryOperation.right, ruleContext, variableStack);
auto left = translate(binaryOperation.left, ruleContext, context, variableStack);
auto right = translate(binaryOperation.right, ruleContext, context, variableStack);
return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
}
std::experimental::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{
auto left = translate(interval.left, ruleContext, variableStack);
auto right = translate(interval.right, ruleContext, variableStack);
const auto operator_ = translate(unaryOperation.unary_operator, term);
auto argument = translate(unaryOperation.argument, ruleContext, context, variableStack);
return ast::Term::make<ast::UnaryOperation>(operator_, std::move(argument));
}
std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{
auto left = translate(interval.left, ruleContext, context, variableStack);
auto right = translate(interval.right, ruleContext, context, variableStack);
return ast::Term::make<ast::Interval>(std::move(left), std::move(right));
}
std::experimental::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{
if (function.external)
throw TranslationException(term.location, "external functions currently unsupported");
@ -132,23 +158,25 @@ struct TermTranslateVisitor
arguments.reserve(function.arguments.size());
for (const auto &argument : function.arguments)
arguments.emplace_back(translate(argument, ruleContext, variableStack));
arguments.emplace_back(translate(argument, ruleContext, context, variableStack));
return ast::Term::make<ast::Function>(function.name, std::move(arguments));
auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, function.arguments.size());
return ast::Term::make<ast::Function>(functionDeclaration, std::move(arguments));
}
std::experimental::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, Context &, const ast::VariableStack &)
{
throw TranslationException(term.location, "“pool” terms currently unsupported");
return std::experimental::nullopt;
return std::nullopt;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{
auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, variableStack);
auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, context, variableStack);
if (!translatedTerm)
throw TranslationException(term.location, "could not translate term");

157
include/anthem/Type.h Normal file
View File

@ -0,0 +1,157 @@
#ifndef __ANTHEM__TYPE_H
#define __ANTHEM__TYPE_H
#include <anthem/AST.h>
#include <anthem/ASTUtils.h>
#include <anthem/Utils.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Type
//
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
Type type(const ast::Term &term, Arguments &&... arguments);
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class VariableDomainAccessor = DefaultVariableDomainAccessor>
struct TermTypeVisitor
{
template <class... Arguments>
static Type visit(const ast::BinaryOperation &binaryOperation, Arguments &&... arguments)
{
const auto leftType = type<VariableDomainAccessor>(binaryOperation.left, std::forward<Arguments>(arguments)...);
const auto rightType = type<VariableDomainAccessor>(binaryOperation.right, std::forward<Arguments>(arguments)...);
// Binary operations on empty sets return an empty set (also with division)
if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
return {Domain::Unknown, SetSize::Empty};
// Binary operations on nonintegers return an empty set (also with division)
if (leftType.domain == Domain::Noninteger || rightType.domain == Domain::Noninteger)
return {Domain::Unknown, SetSize::Empty};
// Binary operations on unknown types return an unknown set
if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
return {Domain::Unknown, SetSize::Unknown};
// Divisions return an unknown set
if (binaryOperation.operator_ == ast::BinaryOperation::Operator::Division)
return {Domain::Integer, SetSize::Unknown};
// Binary operations on integer sets of unknown size return an integer set of unknown size
if (leftType.setSize == SetSize::Unknown || rightType.setSize == SetSize::Unknown)
return {Domain::Integer, SetSize::Unknown};
// Binary operations on integer sets with multiple elements return an integer set with multiple elements
if (leftType.setSize == SetSize::Multi || rightType.setSize == SetSize::Multi)
return {Domain::Integer, SetSize::Multi};
// Binary operations on plain integers return a plain integer
return {Domain::Integer, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::Boolean &, Arguments &&...)
{
return {Domain::Noninteger, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::Function &function, Arguments &&...)
{
// TODO: check that functions cannot return sets
return {function.declaration->domain, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::Integer &, Arguments &&...)
{
return {Domain::Integer, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::Interval &interval, Arguments &&... arguments)
{
const auto fromType = type<VariableDomainAccessor>(interval.from, std::forward<Arguments>(arguments)...);
const auto toType = type<VariableDomainAccessor>(interval.to, std::forward<Arguments>(arguments)...);
// Intervals with empty sets return an empty set
if (fromType.setSize == SetSize::Empty || toType.setSize == SetSize::Empty)
return {Domain::Unknown, SetSize::Empty};
// Intervals with nonintegers return an empty set
if (fromType.domain == Domain::Noninteger || toType.domain == Domain::Noninteger)
return {Domain::Unknown, SetSize::Empty};
// Intervals with unknown types return an unknown set
if (fromType.domain == Domain::Unknown || toType.domain == Domain::Unknown)
return {Domain::Unknown, SetSize::Unknown};
// Intervals with integers generally return integer sets
// TODO: handle 1-element intervals such as 1..1 and empty intervals such as 2..1
return {Domain::Integer, SetSize::Unknown};
}
template <class... Arguments>
static Type visit(const ast::SpecialInteger &, Arguments &&...)
{
return {Domain::Noninteger, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::String &, Arguments &&...)
{
return {Domain::Noninteger, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::UnaryOperation &unaryOperation, Arguments &&... arguments)
{
assert(unaryOperation.operator_ == ast::UnaryOperation::Operator::Absolute);
const auto argumentType = type<VariableDomainAccessor>(unaryOperation.argument, std::forward<Arguments>(arguments)...);
// Absolute value of an empty set returns an empty set
if (argumentType.setSize == SetSize::Empty)
return {Domain::Unknown, SetSize::Empty};
// Absolute value of nonintegers returns an empty set
if (argumentType.domain == Domain::Noninteger)
return {Domain::Unknown, SetSize::Empty};
// Absolute value of integers returns the same type
if (argumentType.domain == Domain::Integer)
return argumentType;
return {Domain::Unknown, SetSize::Unknown};
}
template <class... Arguments>
static Type visit(const ast::Variable &variable, Arguments &&... arguments)
{
const auto domain = VariableDomainAccessor()(variable, std::forward<Arguments>(arguments)...);
return {domain, SetSize::Unit};
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class VariableDomainAccessor, class... Arguments>
Type type(const ast::Term &term, Arguments &&... arguments)
{
return term.accept(TermTypeVisitor<VariableDomainAccessor>(), std::forward<Arguments>(arguments)...);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}
#endif

View File

@ -1,13 +1,6 @@
#ifndef __ANTHEM__UTILS_H
#define __ANTHEM__UTILS_H
#include <iostream>
#include <clingo.hh>
#include <anthem/Context.h>
#include <anthem/Location.h>
namespace anthem
{
@ -20,6 +13,61 @@ namespace anthem
constexpr const auto HeadVariablePrefix = "V";
constexpr const auto BodyVariablePrefix = "X";
constexpr const auto UserVariablePrefix = "U";
constexpr const auto IntegerVariablePrefix = "N";
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class Tristate
{
True,
False,
Unknown,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class OperationResult
{
Unchanged,
Changed,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class EvaluationResult
{
True,
False,
Unknown,
Error,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class Domain
{
Noninteger,
Integer,
Unknown,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class SetSize
{
Empty,
Unit,
Multi,
Unknown,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct Type
{
Domain domain{Domain::Unknown};
SetSize setSize{SetSize::Unknown};
};
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -35,43 +35,46 @@ struct PrintContext
std::map<const VariableDeclaration *, size_t> userVariableIDs;
std::map<const VariableDeclaration *, size_t> headVariableIDs;
std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
std::map<const VariableDeclaration *, size_t> integerVariableIDs;
const Context &context;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext);
output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext, bool omitParentheses = false);
////////////////////////////////////////////////////////////////////////////////////////////////////
// Primitives
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &)
inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &, bool)
{
switch (operator_)
{
@ -85,6 +88,8 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::
return (stream << output::Operator("/"));
case BinaryOperation::Operator::Modulo:
return (stream << output::Operator("%"));
case BinaryOperation::Operator::Power:
return (stream << output::Operator("**"));
}
return stream;
@ -92,22 +97,26 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses)
{
stream << "(";
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
print(stream, binaryOperation.left, printContext);
stream << " ";
print(stream, binaryOperation.operator_, printContext);
stream << " ";
print(stream, binaryOperation.right, printContext);
stream << ")";
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &)
inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &, bool)
{
if (boolean.value)
return (stream << output::Boolean("#true"));
@ -117,7 +126,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Boolean &bo
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &)
inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &, bool)
{
switch (operator_)
{
@ -140,7 +149,7 @@ inline output::ColorStream &print(output::ColorStream &stream, Comparison::Opera
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
@ -159,16 +168,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Comparison
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &)
inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool)
{
return (stream << constant.name);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext)
{
stream << function.name;
stream << function.declaration->name;
if (function.arguments.empty())
return stream;
@ -183,7 +185,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
print(stream, *i, printContext);
}
if (function.name.empty() && function.arguments.size() == 1)
if (function.declaration->name.empty() && function.arguments.size() == 1)
stream << ",";
stream << ")";
@ -193,7 +195,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
@ -210,23 +212,23 @@ inline output::ColorStream &print(output::ColorStream &stream, const In &in, Pri
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &)
inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &, bool)
{
return (stream << output::Number<int>(integer.value));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
print(stream, interval.from, printContext);
stream << "..";
print(stream, interval.to, printContext);
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
@ -234,9 +236,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Interval &i
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool)
{
stream << predicate.name;
stream << predicate.declaration->name;
if (predicate.arguments.empty())
return stream;
@ -258,7 +260,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const Predicate &
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &)
inline output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &, bool)
{
return (stream << predicateDeclaration.name << "/" << predicateDeclaration.arity());
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &, bool)
{
switch (specialInteger.type)
{
@ -273,14 +282,37 @@ inline output::ColorStream &print(output::ColorStream &stream, const SpecialInte
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &)
inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &, bool)
{
return (stream << output::String(string.text.c_str()));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool)
{
switch (unaryOperation.operator_)
{
case UnaryOperation::Operator::Absolute:
stream << "|";
break;
}
print(stream, unaryOperation.argument, printContext, true);
switch (unaryOperation.operator_)
{
case UnaryOperation::Operator::Absolute:
stream << "|";
break;
}
return stream;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext, bool)
{
assert(variable.declaration != nullptr);
@ -289,7 +321,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Variable &v
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool)
{
const auto printVariableDeclaration =
[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
@ -308,6 +340,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
return (stream << output::Variable(variableName.c_str()));
};
if (variableDeclaration.domain == Domain::Integer)
return printVariableDeclaration(IntegerVariablePrefix, printContext.integerVariableIDs);
switch (variableDeclaration.type)
{
case VariableDeclaration::Type::UserDefined:
@ -325,9 +360,10 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
// Expressions
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses)
{
stream << "(";
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
for (auto i = and_.arguments.cbegin(); i != and_.arguments.cend(); i++)
{
@ -337,27 +373,32 @@ inline output::ColorStream &print(output::ColorStream &stream, const And &and_,
print(stream, *i, printContext);
}
stream << ")";
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses)
{
stream << "(";
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
print(stream, biconditional.left, printContext);
stream << " <-> ";
print(stream, biconditional.right, printContext);
stream << ")";
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
@ -383,7 +424,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Exists &exi
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
@ -409,20 +450,24 @@ inline output::ColorStream &print(output::ColorStream &stream, const ForAll &for
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses)
{
stream << "(";
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
print(stream, implies.antecedent, printContext);
stream << " -> ";
print(stream, implies.consequent, printContext);
stream << ")";
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext, bool)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
@ -438,9 +483,10 @@ inline output::ColorStream &print(output::ColorStream &stream, const Not &not_,
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses)
{
stream << "(";
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
for (auto i = or_.arguments.cbegin(); i != or_.arguments.cend(); i++)
{
@ -450,7 +496,8 @@ inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, Pr
print(stream, *i, printContext);
}
stream << ")";
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}
@ -463,24 +510,24 @@ template<class Variant>
struct VariantPrintVisitor
{
template<class T>
output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext)
output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext, bool omitParentheses)
{
return print(stream, x, printContext);
return print(stream, x, printContext, omitParentheses);
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext, bool omitParentheses)
{
return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext);
return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext, omitParentheses);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext)
inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext, bool omitParentheses)
{
return term.accept(VariantPrintVisitor<Term>(), stream, printContext);
return term.accept(VariantPrintVisitor<Term>(), stream, printContext, omitParentheses);
}
////////////////////////////////////////////////////////////////////////////////////////////////////

@ -1 +1 @@
Subproject commit 017a63da62ba7ffce1e1b005e6adc846412c575b
Subproject commit d2d8455b571b6c66c4b7003500a77f9a93ecdc28

@ -1 +1 @@
Subproject commit cc83b3b231ae9626ff5402a5424b0e9e6b4aa180
Subproject commit 969ce8f618c4cdf78d5c430ba827217075b88460

1
lib/cxxopts Submodule

@ -0,0 +1 @@
Subproject commit ca6e9f70eb6b5fab44504daf57d92a9412ab301c

View File

@ -103,16 +103,9 @@ Comparison prepareCopy(const Comparison &other)
////////////////////////////////////////////////////////////////////////////////////////////////////
Constant prepareCopy(const Constant &other)
{
return Constant(std::string(other.name));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
Function prepareCopy(const Function &other)
{
return Function(std::string(other.name), prepareCopy(other.arguments));
return Function(other.declaration, prepareCopy(other.arguments));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -140,7 +133,7 @@ Interval prepareCopy(const Interval &other)
Predicate prepareCopy(const Predicate &other)
{
return Predicate(std::string(other.name), prepareCopy(other.arguments));
return Predicate(other.declaration, prepareCopy(other.arguments));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -159,6 +152,13 @@ String prepareCopy(const String &other)
////////////////////////////////////////////////////////////////////////////////////////////////////
UnaryOperation prepareCopy(const UnaryOperation &other)
{
return UnaryOperation(other.operator_, prepareCopy(other.argument));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
Variable prepareCopy(const Variable &other)
{
return Variable(other.declaration);
@ -286,11 +286,6 @@ struct FixDanglingVariablesInTermVisitor
{
}
template <class... Arguments>
void visit(Constant &, Arguments &&...)
{
}
template <class... Arguments>
void visit(Function &function, Arguments &&... arguments)
{
@ -320,6 +315,12 @@ struct FixDanglingVariablesInTermVisitor
{
}
template <class... Arguments>
void visit(UnaryOperation &unaryOperation, Arguments &&... arguments)
{
unaryOperation.argument.accept(*this, std::forward<Arguments>(arguments)...);
}
void visit(Variable &variable, ScopedFormula &scopedFormula, VariableStack &variableStack,
std::map<VariableDeclaration *, VariableDeclaration *> &replacements)
{

View File

@ -27,7 +27,7 @@ void VariableStack::pop()
////////////////////////////////////////////////////////////////////////////////////////////////////
std::experimental::optional<VariableDeclaration *> VariableStack::findUserVariableDeclaration(const char *variableName) const
std::optional<VariableDeclaration *> VariableStack::findUserVariableDeclaration(const char *variableName) const
{
const auto variableDeclarationMatches =
[&variableName](const auto &variableDeclaration)
@ -45,7 +45,7 @@ std::experimental::optional<VariableDeclaration *> VariableStack::findUserVariab
return matchingVariableDeclaration->get();
}
return std::experimental::nullopt;
return std::nullopt;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -59,7 +59,7 @@ bool VariableStack::contains(const VariableDeclaration &variableDeclaration) con
};
const auto layerContainsVariableDeclaration =
[&variableDeclaration, &variableDeclarationMatches](const auto &layer)
[&variableDeclarationMatches](const auto &layer)
{
return (std::find_if(layer->cbegin(), layer->cend(), variableDeclarationMatches) != layer->cend());
};
@ -150,10 +150,6 @@ struct CollectFreeVariablesVisitor
binaryOperation.right.accept(*this, variableStack, freeVariables);
}
void visit(Constant &, VariableStack &, std::vector<VariableDeclaration *> &)
{
}
void visit(Function &function, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{
for (auto &argument : function.arguments)
@ -178,6 +174,11 @@ struct CollectFreeVariablesVisitor
{
}
void visit(UnaryOperation &unaryOperation, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{
unaryOperation.argument.accept(*this, variableStack, freeVariables);
}
void visit(Variable &variable, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{
if (variableStack.contains(*variable.declaration))
@ -192,61 +193,5 @@ struct CollectFreeVariablesVisitor
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
{
static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures)
{
const auto predicateSignatureMatches =
[&predicate](const auto &predicateSignature)
{
return matches(predicate, predicateSignature);
};
if (std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), predicateSignatureMatches) != predicateSignatures.cend())
return;
// TODO: avoid copies
predicateSignatures.emplace_back(std::string(predicate.name), predicate.arity());
}
// Ignore all other types of expressions
template<class T>
static void accept(const T &, const Formula &, std::vector<PredicateSignature> &)
{
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
bool matches(const Predicate &lhs, const Predicate &rhs)
{
return (lhs.name == rhs.name && lhs.arity() == rhs.arity());
}
////////////////////////////////////////////////////////////////////////////////////////////////////
bool matches(const Predicate &predicate, const PredicateSignature &signature)
{
return (predicate.name == signature.name && predicate.arity() == signature.arity);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs)
{
return (lhs.name == rhs.name && lhs.arity == rhs.arity);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// TODO: remove const_cast
void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures)
{
auto &formulaMutable = const_cast<Formula &>(formula);
formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}
}

View File

@ -35,13 +35,41 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
if (!ast::matches(predicate, otherPredicate))
if (predicate.declaration != otherPredicate.declaration)
continue;
assert(otherPredicate.arguments.size() == parameters.size());
auto &freeVariables = scopedFormula.freeVariables;
// Each formula with the predicate as its consequent currently has its own copy of the predicates parameters
// These need to be linked to the new, unique set of parameters
// First, remove the free variables whose occurrences will be relinked, which is why they are no longer needed
const auto isFreeVariableUnneeded =
[&](const auto &freeVariable)
{
const auto matchesVariableToBeReplaced = std::find_if(otherPredicate.arguments.cbegin(), otherPredicate.arguments.cend(),
[&](const ast::Term &argument)
{
assert(argument.is<ast::Variable>());
const auto &otherVariable = argument.get<ast::Variable>();
return (freeVariable.get() == otherVariable.declaration);
});
return (matchesVariableToBeReplaced != otherPredicate.arguments.cend());
};
freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isFreeVariableUnneeded), freeVariables.end());
// Currently, only rules with singleton heads are supported
// Rules with multiple elements in the head are not yet handled correctly by the head variable detection mechanism
for (const auto &freeVariable : freeVariables)
if (freeVariable->type == ast::VariableDeclaration::Type::Head)
throw CompletionException("cannot perform completion, only singleton rule heads supported currently");
// Second, link all occurrences of the deleted free variable to the new, unique parameter
for (size_t i = 0; i < parameters.size(); i++)
{
assert(otherPredicate.arguments[i].is<ast::Variable>());
@ -50,16 +78,6 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
scopedFormula.formula.accept(ast::ReplaceVariableInFormulaVisitor(), scopedFormula.formula, otherVariable.declaration, parameters[i].get());
}
// Remove all the head variables, because they are not free variables after completion
const auto isHeadVariable =
[](const auto &variableDeclaration)
{
return variableDeclaration->type == ast::VariableDeclaration::Type::Head;
};
auto &freeVariables = scopedFormula.freeVariables;
freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isHeadVariable), freeVariables.end());
if (freeVariables.empty())
disjunction.get<ast::Or>().arguments.emplace_back(std::move(implies.antecedent));
else
@ -100,22 +118,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector<ast::ScopedFormula> &scopedFormulas)
ast::Formula completePredicate(ast::PredicateDeclaration &predicateDeclaration, std::vector<ast::ScopedFormula> &scopedFormulas)
{
// Create new set of parameters for the completed definition for the predicate
ast::VariableDeclarationPointers parameters;
parameters.reserve(predicateSignature.arity);
parameters.reserve(predicateDeclaration.arity());
std::vector<ast::Term> arguments;
arguments.reserve(predicateSignature.arity);
arguments.reserve(predicateDeclaration.arity());
for (size_t i = 0; i < predicateSignature.arity; i++)
for (size_t i = 0; i < predicateDeclaration.arity(); i++)
{
parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Head));
arguments.emplace_back(ast::Term::make<ast::Variable>(parameters.back().get()));
}
ast::Predicate predicateCopy(std::string(predicateSignature.name), std::move(arguments));
ast::Predicate predicateCopy(&predicateDeclaration, std::move(arguments));
auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
@ -161,28 +179,27 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
}
std::vector<ast::PredicateSignature> predicateSignatures;
// Get a list of all predicates
for (const auto &scopedFormula : scopedFormulas)
ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures);
std::sort(predicateSignatures.begin(), predicateSignatures.end(),
std::sort(context.predicateDeclarations.begin(), context.predicateDeclarations.end(),
[](const auto &lhs, const auto &rhs)
{
const auto order = std::strcmp(lhs.name.c_str(), rhs.name.c_str());
const auto order = std::strcmp(lhs->name.c_str(), rhs->name.c_str());
if (order != 0)
return (order < 0);
return lhs.arity < rhs.arity;
return lhs->arity() < rhs->arity();
});
std::vector<ast::Formula> completedFormulas;
// Complete predicates
for (const auto &predicateSignature : predicateSignatures)
completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
for (auto &predicateDeclaration : context.predicateDeclarations)
{
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
continue;
completedFormulas.emplace_back(completePredicate(*predicateDeclaration, scopedFormulas));
}
// Complete integrity constraints
for (auto &scopedFormula : scopedFormulas)
@ -202,7 +219,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
}
// Eliminate all predicates that should not be visible in the output
eliminateHiddenPredicates(predicateSignatures, completedFormulas, context);
eliminateHiddenPredicates(completedFormulas, context);
return completedFormulas;
}

View File

@ -78,7 +78,7 @@ struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor<Re
{
static void accept(ast::Predicate &predicate, ast::Formula &formula, const PredicateReplacement &predicateReplacement)
{
if (!ast::matches(predicate, predicateReplacement.predicate))
if (predicate.declaration != predicateReplacement.predicate.declaration)
return;
auto formulaReplacement = ast::prepareCopy(predicateReplacement.replacement);
@ -109,15 +109,15 @@ struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor<Re
// Detect whether a formula contains a circular dependency on a given predicate
struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<DetectCircularDependcyVisitor>
{
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateSignature &predicateSignature, bool &hasCircularDependency)
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateDeclaration &predicateDeclaration, bool &hasCircularDependency)
{
if (ast::matches(predicate, predicateSignature))
if (predicate.declaration == &predicateDeclaration)
hasCircularDependency = true;
}
// Ignore all other types of expressions
template<class T>
static void accept(T &, ast::Formula &, const ast::PredicateSignature &, bool &)
static void accept(T &, ast::Formula &, const ast::PredicateDeclaration &, bool &)
{
}
};
@ -125,12 +125,12 @@ struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<Detec
////////////////////////////////////////////////////////////////////////////////////////////////////
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> q(X1, ..., Xn)”
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Predicate &predicate)
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Predicate &predicate)
{
// Declare variable used, only used in debug mode
(void)(predicateSignature);
(void)(predicateDeclaration);
assert(ast::matches(predicate, predicateSignature));
assert(predicate.declaration == &predicateDeclaration);
// Replace with “#true”
return {predicate, ast::Formula::make<ast::Boolean>(true)};
@ -139,13 +139,13 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
////////////////////////////////////////////////////////////////////////////////////////////////////
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> not q(X1, ..., Xn)”
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Not &not_)
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Not &not_)
{
// Declare variable used, only used in debug mode
(void)(predicateSignature);
(void)(predicateDeclaration);
assert(not_.argument.is<ast::Predicate>());
assert(ast::matches(not_.argument.get<ast::Predicate>(), predicateSignature));
assert(not_.argument.get<ast::Predicate>().declaration == &predicateDeclaration);
// Replace with “#false”
return {not_.argument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(false)};
@ -154,13 +154,13 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
////////////////////////////////////////////////////////////////////////////////////////////////////
// Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)”
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Biconditional &biconditional)
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Biconditional &biconditional)
{
// Declare variable used, only used in debug mode
(void)(predicateSignature);
(void)(predicateDeclaration);
assert(biconditional.left.is<ast::Predicate>());
assert(ast::matches(biconditional.left.get<ast::Predicate>(), predicateSignature));
assert(biconditional.left.get<ast::Predicate>().declaration == &predicateDeclaration);
// TODO: avoid copy
return {biconditional.left.get<ast::Predicate>(), ast::prepareCopy(biconditional.right)};
@ -169,78 +169,65 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
////////////////////////////////////////////////////////////////////////////////////////////////////
// Finds a replacement for a predicate that should be hidden
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Formula &completedPredicateDefinition)
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Formula &completedPredicateDefinition)
{
// TODO: refactor
if (completedPredicateDefinition.is<ast::ForAll>())
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::ForAll>().argument);
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::ForAll>().argument);
else if (completedPredicateDefinition.is<ast::Biconditional>())
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Biconditional>());
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Biconditional>());
else if (completedPredicateDefinition.is<ast::Predicate>())
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Predicate>());
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Predicate>());
else if (completedPredicateDefinition.is<ast::Not>())
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Not>());
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Not>());
throw CompletionException("unsupported completed definition for predicate “" + predicateSignature.name + "/" + std::to_string(predicateSignature.arity) + "” for hiding predicates");
throw CompletionException("unsupported completed definition for predicate “" + predicateDeclaration.name + "/" + std::to_string(predicateDeclaration.arity()) + "” for hiding predicates");
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context)
void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context)
{
if (!context.visiblePredicateSignatures)
if (context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible)
{
context.logger.log(output::Priority::Debug) << "no predicates to be eliminated";
return;
}
const auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
assert(context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Hidden);
// Check for undeclared predicates that are requested to be shown
for (const auto &visiblePredicateSignature : visiblePredicateSignatures)
{
const auto matchesPredicateSignature =
[&](const auto &predicateSignature)
{
return ast::matches(predicateSignature, visiblePredicateSignature);
};
const auto matchingPredicateSignature =
std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature);
if (matchingPredicateSignature == predicateSignatures.cend())
context.logger.log(output::Priority::Warning) << "cannot show undeclared predicate “" << visiblePredicateSignature.name << "/" << visiblePredicateSignature.arity <<"";
}
// TODO: get rid of index-wise matching of completed formulas and predicate declarations
size_t i = -1;
// Replace all occurrences of hidden predicates
for (size_t i = 0; i < predicateSignatures.size(); i++)
for (auto &predicateDeclaration : context.predicateDeclarations)
{
auto &predicateSignature = predicateSignatures[i];
const auto matchesVisiblePredicateSignature =
[&](const auto &visiblePredicateSignature)
{
return ast::matches(predicateSignature, visiblePredicateSignature);
};
const auto matchingPredicateSignature =
std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesVisiblePredicateSignature);
// If the predicate ought to be visible, dont eliminate it
if (matchingPredicateSignature != visiblePredicateSignatures.cend())
// Check that the predicate is used and not declared #external
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
continue;
context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "";
i++;
const auto isPredicateVisible =
(predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Visible)
|| (predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Default
&& context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible);
// If the predicate ought to be visible, dont eliminate it
if (isPredicateVisible)
continue;
context.logger.log(output::Priority::Debug) << "eliminating “" << predicateDeclaration->name << "/" << predicateDeclaration->arity() << "";
const auto &completedPredicateDefinition = completedFormulas[i];
auto replacement = findReplacement(predicateSignature, completedPredicateDefinition);
auto replacement = findReplacement(*predicateDeclaration, completedPredicateDefinition);
bool hasCircularDependency = false;
replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, predicateSignature, hasCircularDependency);
replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, *predicateDeclaration, hasCircularDependency);
if (hasCircularDependency)
{
context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateSignature.name << "/" << predicateSignature.arity << "” due to circular dependency";
context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateDeclaration->name << "/" << predicateDeclaration->arity() << "” due to circular dependency";
continue;
}

View File

@ -0,0 +1,332 @@
#include <anthem/IntegerVariableDetection.h>
#include <anthem/ASTCopy.h>
#include <anthem/ASTUtils.h>
#include <anthem/ASTVisitors.h>
#include <anthem/Evaluation.h>
#include <anthem/Exception.h>
#include <anthem/Simplification.h>
#include <anthem/Type.h>
#include <anthem/Utils.h>
#include <anthem/output/AST.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// IntegerVariableDetection
//
////////////////////////////////////////////////////////////////////////////////////////////////////
using VariableDomainMap = std::map<const ast::VariableDeclaration *, Domain>;
////////////////////////////////////////////////////////////////////////////////////////////////////
Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
{
if (variable.declaration->domain != Domain::Unknown)
return variable.declaration->domain;
const auto match = variableDomainMap.find(variable.declaration);
if (match == variableDomainMap.end())
return Domain::Unknown;
return match->second;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
{
for (auto &variableDeclaration : variableDomainMap)
variableDeclaration.second = Domain::Unknown;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
struct VariableDomainMapAccessor
{
Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
{
return domain(variable, variableDomainMap);
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
Type type(const ast::Term &term, VariableDomainMap &variableDomainMap)
{
return type<VariableDomainMapAccessor>(term, variableDomainMap);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap)
{
return evaluate<VariableDomainMap>(formula, variableDomainMap);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class Functor>
struct ForEachVariableDeclarationVisitor
{
template <class... Arguments>
static OperationResult visit(ast::And &and_, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
for (auto &argument : and_.arguments)
if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::Biconditional &biconditional, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
if (biconditional.left.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
if (biconditional.right.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::Boolean &, Arguments &&...)
{
return OperationResult::Unchanged;
}
template <class... Arguments>
static OperationResult visit(ast::Comparison &, Arguments &&...)
{
return OperationResult::Unchanged;
}
template <class... Arguments>
static OperationResult visit(ast::Exists &exists, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
if (exists.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
for (auto &variableDeclaration : exists.variables)
if (Functor()(*variableDeclaration, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::ForAll &forAll, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
if (forAll.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
for (auto &variableDeclaration : forAll.variables)
if (Functor()(*variableDeclaration, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::Implies &implies, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
if (implies.antecedent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
if (implies.consequent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::In &, Arguments &&...)
{
return OperationResult::Unchanged;
}
template <class... Arguments>
static OperationResult visit(ast::Not &not_, Arguments &&... arguments)
{
return not_.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
static OperationResult visit(ast::Or &or_, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
for (auto &argument : or_.arguments)
if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::Predicate &, Arguments &&...)
{
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CheckIfDefinitionFalseFunctor
{
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
// As a hypothesis, make the parameters domain noninteger
variableDomainMap[&variableDeclaration] = Domain::Noninteger;
const auto result = evaluate(definition, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, its proven to be integer
variableDeclaration.domain = Domain::Integer;
return OperationResult::Changed;
}
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CheckIfQuantifiedFormulaFalseFunctor
{
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
// As a hypothesis, make the parameters domain noninteger
variableDomainMap[&variableDeclaration] = Domain::Noninteger;
const auto result = evaluate(quantifiedFormula, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, its proven to be integer
variableDeclaration.domain = Domain::Integer;
return OperationResult::Changed;
}
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CheckIfCompletedFormulaTrueFunctor
{
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
// As a hypothesis, make the parameters domain noninteger
variableDomainMap[&variableDeclaration] = Domain::Noninteger;
const auto result = evaluate(completedFormula, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::True)
{
// If making the variable noninteger leads to a false or erroneous result, its proven to be integer
variableDeclaration.domain = Domain::Integer;
return OperationResult::Changed;
}
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// Assumes the completed formulas to be in translated but not simplified form.
// That is, completed formulas are either variable-free or universally quantified
void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
{
VariableDomainMap variableDomainMap;
auto operationResult = OperationResult::Changed;
while (operationResult == OperationResult::Changed)
{
operationResult = OperationResult::Unchanged;
for (auto &completedFormula : completedFormulas)
{
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfQuantifiedFormulaFalseFunctor>(), variableDomainMap) == OperationResult::Changed)
operationResult = OperationResult::Changed;
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfCompletedFormulaTrueFunctor>(), completedFormula, variableDomainMap) == OperationResult::Changed)
operationResult = OperationResult::Changed;
if (!completedFormula.is<ast::ForAll>())
continue;
auto &forAll = completedFormula.get<ast::ForAll>();
if (!forAll.argument.is<ast::Biconditional>())
continue;
auto &biconditional = forAll.argument.get<ast::Biconditional>();
if (!biconditional.left.is<ast::Predicate>())
continue;
auto &predicate = biconditional.left.get<ast::Predicate>();
auto &definition = biconditional.right;
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfDefinitionFalseFunctor>(), definition, variableDomainMap) == OperationResult::Changed)
operationResult = OperationResult::Changed;
assert(predicate.arguments.size() == predicate.declaration->arity());
for (size_t i = 0; i < predicate.arguments.size(); i++)
{
auto &variableArgument = predicate.arguments[i];
auto &parameter = predicate.declaration->parameters[i];
assert(variableArgument.is<ast::Variable>());
auto &variable = variableArgument.get<ast::Variable>();
parameter.domain = variable.declaration->domain;
}
}
}
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}

View File

@ -1,9 +1,12 @@
#include <anthem/Simplification.h>
#include <experimental/optional>
#include <optional>
#include <anthem/ASTCopy.h>
#include <anthem/ASTVisitors.h>
#include <anthem/Equality.h>
#include <anthem/SimplificationVisitors.h>
#include <anthem/Type.h>
#include <anthem/output/AST.h>
namespace anthem
{
@ -27,15 +30,15 @@ bool matchesVariableDeclaration(const ast::Term &term, const ast::VariableDeclar
// Extracts the term t if the given formula is of the form “X = t” and X matches the given variable
// The input formula is no longer usable after this call if a term is returned
std::experimental::optional<ast::Term> extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration)
std::optional<ast::Term> extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration)
{
if (!formula.is<ast::Comparison>())
return std::experimental::nullopt;
return std::nullopt;
auto &comparison = formula.get<ast::Comparison>();
if (comparison.operator_ != ast::Comparison::Operator::Equal)
return std::experimental::nullopt;
return std::nullopt;
if (matchesVariableDeclaration(comparison.left, variableDeclaration))
return std::move(comparison.right);
@ -43,7 +46,7 @@ std::experimental::optional<ast::Term> extractAssignedTerm(ast::Formula &formula
if (matchesVariableDeclaration(comparison.right, variableDeclaration))
return std::move(comparison.left);
return std::experimental::nullopt;
return std::nullopt;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -97,18 +100,65 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
////////////////////////////////////////////////////////////////////////////////////////////////////
// Simplifies exists statements by using the equivalence “exists X (X = t and F(X))” == “F(t)”
// The exists statement has to be of the form “exists <variables> <conjunction>”
void simplify(ast::Exists &exists, ast::Formula &formula)
template<class SimplificationRule>
OperationResult simplify(ast::Formula &formula)
{
// Simplify formulas like “exists X (X = Y)” to “#true”
// TODO: check that this covers all cases
if (exists.argument.is<ast::Comparison>())
return SimplificationRule::apply(formula);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
OperationResult simplify(ast::Formula &formula)
{
if (simplify<FirstSimplificationRule>(formula) == OperationResult::Changed)
return OperationResult::Changed;
return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleExistsWithoutQuantifiedVariables
{
static constexpr const auto Description = "exists () (F) === F";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Exists>())
return OperationResult::Unchanged;
auto &exists = formula.get<ast::Exists>();
if (!exists.variables.empty())
return OperationResult::Unchanged;
formula = std::move(exists.argument);
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleTrivialAssignmentInExists
{
static constexpr const auto Description = "exists X (X = Y) === #true";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Exists>())
return OperationResult::Unchanged;
const auto &exists = formula.get<ast::Exists>();
if (!exists.argument.is<ast::Comparison>())
return OperationResult::Unchanged;
const auto &comparison = exists.argument.get<ast::Comparison>();
if (comparison.operator_ != ast::Comparison::Operator::Equal)
return;
return OperationResult::Unchanged;
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
[&](const auto &variableDeclaration)
@ -117,107 +167,407 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
});
if (matchingAssignment != exists.variables.cend())
formula = ast::Formula::make<ast::Boolean>(true);
if (matchingAssignment == exists.variables.cend())
return OperationResult::Unchanged;
return;
formula = ast::Formula::make<ast::Boolean>(true);
return OperationResult::Changed;
}
};
if (!exists.argument.is<ast::And>())
return;
////////////////////////////////////////////////////////////////////////////////////////////////////
auto &conjunction = exists.argument.get<ast::And>();
auto &arguments = conjunction.arguments;
struct SimplificationRuleAssignmentInExists
{
static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
// Simplify formulas of type “exists X (X = t and F(X))” to “F(t)”
for (auto i = exists.variables.begin(); i != exists.variables.end();)
static OperationResult apply(ast::Formula &formula)
{
const auto &variableDeclaration = **i;
if (!formula.is<ast::Exists>())
return OperationResult::Unchanged;
bool wasVariableReplaced = false;
auto &exists = formula.get<ast::Exists>();
// TODO: refactor
for (auto j = arguments.begin(); j != arguments.end(); j++)
if (!exists.argument.is<ast::And>())
return OperationResult::Unchanged;
auto &and_ = exists.argument.get<ast::And>();
auto &arguments = and_.arguments;
auto simplificationResult = OperationResult::Unchanged;
for (auto i = exists.variables.begin(); i != exists.variables.end();)
{
auto &argument = *j;
// Find term that is equivalent to the given variable
auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
const auto &variableDeclaration = **i;
if (!assignedTerm)
continue;
bool wasVariableReplaced = false;
// Replace all occurrences of the variable with the equivalent term
for (auto k = arguments.begin(); k != arguments.end(); k++)
// TODO: refactor
for (auto j = arguments.begin(); j != arguments.end(); j++)
{
if (k == j)
auto &argument = *j;
// Find term that is equivalent to the given variable
auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
if (!assignedTerm)
continue;
auto &otherArgument = *k;
otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
// Replace all occurrences of the variable with the equivalent term
for (auto k = arguments.begin(); k != arguments.end(); k++)
{
if (k == j)
continue;
auto &otherArgument = *k;
otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
}
arguments.erase(j);
wasVariableReplaced = true;
simplificationResult = OperationResult::Changed;
break;
}
arguments.erase(j);
wasVariableReplaced = true;
break;
if (wasVariableReplaced)
{
i = exists.variables.erase(i);
continue;
}
i++;
}
if (wasVariableReplaced)
{
i = exists.variables.erase(i);
continue;
}
i++;
return simplificationResult;
}
};
// If there are no arguments left, we had a formula of the form “exists X1, ..., Xn (X1 = Y1 and ... and Xn = Yn)”
// Such exists statements are useless and can be safely replaced with “#true”
if (arguments.empty())
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleEmptyConjunction
{
static constexpr const auto Description = "[empty conjunction] === #true";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::And>())
return OperationResult::Unchanged;
auto &and_ = formula.get<ast::And>();
if (!and_.arguments.empty())
return OperationResult::Unchanged;
formula = ast::Formula::make<ast::Boolean>(true);
return;
return OperationResult::Changed;
}
};
// If the argument now is a conjunction with just one element, directly replace the input formula with the argument
if (arguments.size() == 1)
exists.argument = std::move(arguments.front());
////////////////////////////////////////////////////////////////////////////////////////////////////
// If there are still remaining variables, simplification is over
if (!exists.variables.empty())
return;
struct SimplificationRuleOneElementConjunction
{
static constexpr const auto Description = "[conjunction of only F] === F";
assert(!arguments.empty());
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::And>())
return OperationResult::Unchanged;
// If there is more than one element in the conjunction, replace the input formula with the conjunction
formula = std::move(exists.argument);
}
auto &and_ = formula.get<ast::And>();
if (and_.arguments.size() != 1)
return OperationResult::Unchanged;
formula = std::move(and_.arguments.front());
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleTrivialExists
{
static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Exists>())
return OperationResult::Unchanged;
auto &exists = formula.get<ast::Exists>();
if (!exists.argument.is<ast::Boolean>())
return OperationResult::Unchanged;
formula = std::move(exists.argument);
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleInWithPrimitiveArguments
{
static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::In>())
return OperationResult::Unchanged;
auto &in = formula.get<ast::In>();
assert(ast::isPrimitive(in.element));
if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
return OperationResult::Unchanged;
formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleSubsumptionInBiconditionals
{
static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Biconditional>())
return OperationResult::Unchanged;
auto &biconditional = formula.get<ast::Biconditional>();
const auto leftIsPredicate = biconditional.left.is<ast::Predicate>();
const auto rightIsPredicate = biconditional.right.is<ast::Predicate>();
const auto leftIsAnd = biconditional.left.is<ast::And>();
const auto rightIsAnd = biconditional.right.is<ast::And>();
if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
return OperationResult::Unchanged;
auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
auto &and_ = andSide.get<ast::And>();
const auto matchingPredicate =
std::find_if(and_.arguments.cbegin(), and_.arguments.cend(),
[&](const auto &argument)
{
return (ast::equal(predicateSide, argument) == Tristate::True);
});
if (matchingPredicate == and_.arguments.cend())
return OperationResult::Unchanged;
and_.arguments.erase(matchingPredicate);
formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide));
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleDoubleNegation
{
static constexpr const auto Description = "not not F === F";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Not>())
return OperationResult::Unchanged;
auto &not_ = formula.get<ast::Not>();
if (!not_.argument.is<ast::Not>())
return OperationResult::Unchanged;
auto &notNot = not_.argument.get<ast::Not>();
formula = std::move(notNot.argument);
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleDeMorganForConjunctions
{
static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Not>())
return OperationResult::Unchanged;
auto &not_ = formula.get<ast::Not>();
if (!not_.argument.is<ast::And>())
return OperationResult::Unchanged;
auto &and_ = not_.argument.get<ast::And>();
for (auto &argument : and_.arguments)
argument = ast::Formula::make<ast::Not>(std::move(argument));
formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleImplicationFromDisjunction
{
static constexpr const auto Description = "(not F or G) === (F -> G)";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Or>())
return OperationResult::Unchanged;
auto &or_ = formula.get<ast::Or>();
if (or_.arguments.size() != 2)
return OperationResult::Unchanged;
const auto leftIsNot = or_.arguments[0].is<ast::Not>();
const auto rightIsNot = or_.arguments[1].is<ast::Not>();
if (leftIsNot == rightIsNot)
return OperationResult::Unchanged;
auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
assert(negativeSide.is<ast::Not>());
assert(!positiveSide.is<ast::Not>());
auto &negativeSideArgument = negativeSide.get<ast::Not>().argument;
formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleNegatedComparison
{
static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Not>())
return OperationResult::Unchanged;
auto &not_ = formula.get<ast::Not>();
if (!not_.argument.is<ast::Comparison>())
return OperationResult::Unchanged;
auto &comparison = not_.argument.get<ast::Comparison>();
switch (comparison.operator_)
{
case ast::Comparison::Operator::GreaterThan:
comparison.operator_ = ast::Comparison::Operator::LessEqual;
break;
case ast::Comparison::Operator::LessThan:
comparison.operator_ = ast::Comparison::Operator::GreaterEqual;
break;
case ast::Comparison::Operator::LessEqual:
comparison.operator_ = ast::Comparison::Operator::GreaterThan;
break;
case ast::Comparison::Operator::GreaterEqual:
comparison.operator_ = ast::Comparison::Operator::LessThan;
break;
case ast::Comparison::Operator::NotEqual:
comparison.operator_ = ast::Comparison::Operator::Equal;
break;
case ast::Comparison::Operator::Equal:
comparison.operator_ = ast::Comparison::Operator::NotEqual;
break;
}
formula = std::move(comparison);
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleIntegerSetInclusion
{
static constexpr const auto Description = "(F in G) === (F = G) if F and G are integer variables";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::In>())
return OperationResult::Unchanged;
auto &in = formula.get<ast::In>();
const auto elementType = type(in.element);
const auto setType = type(in.set);
if (elementType.domain != Domain::Integer || setType.domain != Domain::Integer
|| elementType.setSize != SetSize::Unit || setType.setSize != SetSize::Unit)
{
return OperationResult::Unchanged;
}
formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
const auto simplifyWithDefaultRules =
simplify
<
SimplificationRuleDoubleNegation,
SimplificationRuleTrivialAssignmentInExists,
SimplificationRuleAssignmentInExists,
SimplificationRuleEmptyConjunction,
SimplificationRuleTrivialExists,
SimplificationRuleOneElementConjunction,
SimplificationRuleExistsWithoutQuantifiedVariables,
SimplificationRuleInWithPrimitiveArguments,
SimplificationRuleSubsumptionInBiconditionals,
SimplificationRuleDeMorganForConjunctions,
SimplificationRuleImplicationFromDisjunction,
SimplificationRuleNegatedComparison,
SimplificationRuleIntegerSetInclusion
>;
////////////////////////////////////////////////////////////////////////////////////////////////////
// Performs the different simplification techniques
struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyFormulaVisitor>
struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
{
// Forward exists statements to the dedicated simplification function
static void accept(ast::Exists &exists, ast::Formula &formula)
{
simplify(exists, formula);
}
// Simplify formulas of type “A in B” to “A = B” if A and B are primitive
static void accept(ast::In &in, ast::Formula &formula)
{
assert(ast::isPrimitive(in.element));
if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
return;
formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
}
// Do nothing for all other types of expressions
template<class T>
static void accept(T &, ast::Formula &)
static OperationResult accept(ast::Formula &formula)
{
return simplifyWithDefaultRules(formula);
}
};
@ -225,7 +575,7 @@ struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyForm
void simplify(ast::Formula &formula)
{
formula.accept(SimplifyFormulaVisitor(), formula);
while (formula.accept(SimplifyFormulaVisitor(), formula) == OperationResult::Changed);
}
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -8,6 +8,7 @@
#include <anthem/Completion.h>
#include <anthem/Context.h>
#include <anthem/IntegerVariableDetection.h>
#include <anthem/Simplification.h>
#include <anthem/StatementVisitor.h>
#include <anthem/output/AST.h>
@ -67,9 +68,12 @@ void translate(const char *fileName, std::istream &stream, Context &context)
for (auto &scopedFormula : scopedFormulas)
simplify(scopedFormula.formula);
if (context.visiblePredicateSignatures)
if (context.showStatementsUsed)
context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";
if (context.externalStatementsUsed)
context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled";
for (const auto &scopedFormula : scopedFormulas)
{
ast::print(context.logger.outputStream(), scopedFormula.formula, printContext);
@ -82,6 +86,34 @@ void translate(const char *fileName, std::istream &stream, Context &context)
// Perform completion
auto completedFormulas = complete(std::move(scopedFormulas), context);
for (const auto &predicateDeclaration : context.predicateDeclarations)
{
if (predicateDeclaration->isUsed)
continue;
// Check for #show statements with undeclared predicates
if (predicateDeclaration->visibility != ast::PredicateDeclaration::Visibility::Default)
context.logger.log(output::Priority::Warning)
<< "#show declaration of “"
<< predicateDeclaration->name
<< "/"
<< predicateDeclaration->arity()
<< "” does not match any declared predicate";
// Check for #external statements with undeclared predicates
if (predicateDeclaration->isExternal && !predicateDeclaration->isUsed)
context.logger.log(output::Priority::Warning)
<< "#external declaration of “"
<< predicateDeclaration->name
<< "/"
<< predicateDeclaration->arity()
<< "” does not match any declared predicate";
}
// Detect integer variables
if (context.performIntegerDetection)
detectIntegerVariables(completedFormulas);
// Simplify output if specified
if (context.performSimplification)
for (auto &completedFormula : completedFormulas)
@ -94,6 +126,38 @@ void translate(const char *fileName, std::istream &stream, Context &context)
ast::print(context.logger.outputStream(), completedFormula, printContext);
context.logger.outputStream() << std::endl;
}
// Print specifiers for integer predicate parameters
for (auto &predicateDeclaration : context.predicateDeclarations)
{
// Check that the predicate is used and not declared #external
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
continue;
const auto isPredicateVisible =
(predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Visible)
|| (predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Default
&& context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible);
// If the predicate ought to be visible, dont eliminate it
if (!isPredicateVisible)
continue;
for (size_t i = 0; i < predicateDeclaration->parameters.size(); i++)
{
auto &parameter = predicateDeclaration->parameters[i];
if (parameter.domain != Domain::Integer)
continue;
context.logger.outputStream()
<< output::Keyword("int")
<< "(" << predicateDeclaration->name
<< "/" << output::Number(predicateDeclaration->arity())
<< "@" << output::Number(i + 1)
<< ")" << std::endl;
}
}
}
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -123,7 +123,7 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1 (f(V1) <-> (exists U1 (V1 = f(f(f(f(U1)))) and f(U1)) or V1 in 1..5))\n");
"forall V1 (f(V1) <-> (exists U1 (V1 = f(f(f(f(U1)))) and f(U1)) or V1 in (1..5)))\n");
}
SECTION("useless implications")
@ -152,9 +152,9 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
CHECK(output.str() ==
"forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n"
"forall V2, V3 (in(V2, V3) <-> (V2 in 1..n and V3 in 1..r and in(V2, V3)))\n"
"forall U2 not (U2 in 1..n and not covered(U2))\n"
"forall U3, U4, U5 not (in(U3, U4) and in(U5, U4) and exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
"forall V2, V3 (in(V2, V3) -> (V2 in (1..n) and V3 in (1..r)))\n"
"forall U2 (U2 in (1..n) -> covered(U2))\n"
"forall U3, U4, U5 (not in(U3, U4) or not in(U5, U4) or not exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
}
SECTION("binary operations with multiple variables")
@ -176,4 +176,20 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
CHECK(output.str() ==
"forall V1, V2, V3 (p(V1, V2, V3) <-> #true)\n");
}
SECTION("negated comparisons")
{
input << ":- color(V, C1), color(V, C2), C1 != C2.";
anthem::translate("input", input, context);
CHECK(output.str() == "forall V1, V2 not color(V1, V2)\nforall U1, U2, U3 (not color(U1, U2) or not color(U1, U3) or U2 = U3)\n");
}
SECTION("absolute value operation")
{
input << "adj(X, Y) :- X = 1..n, Y = 1..n, |X - Y| = 1.";
anthem::translate("input", input, context);
CHECK(output.str() == "forall V1, V2 (adj(V1, V2) <-> (V1 in (1..n) and V2 in (1..n) and |V1 - V2| = 1))\n");
}
}

View File

@ -103,9 +103,10 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
"#show a/1.";
anthem::translate("input", input, context);
// TODO: simplify further
CHECK(output.str() ==
"forall V1 (a(V1) <-> not d(V1))\n"
"forall V2 (d(V2) <-> not not d(V2))\n"
"forall V2 (d(V2) <-> d(V2))\n"
"forall V3 (e(V3) <-> e(V3))\n");
}
@ -149,7 +150,7 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
// TODO: simplify further
CHECK(output.str() ==
"forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in 1..4))\n");
"forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in (1..4)))\n");
}
SECTION("simple propositions are hidden correctly")
@ -164,12 +165,11 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
"#show t/0.";
anthem::translate("input", input, context);
// TODO: simplify further
CHECK(output.str() ==
"(s <-> (not #false and s))\n"
"(t <-> (not #false and t))\n"
"not (s and not t)\n"
"not (not #false and not #false and #false)\n");
"(s -> not #false)\n"
"(t -> not #false)\n"
"(s -> t)\n"
"(#false or #false or not #false)\n");
}
SECTION("predicate with more than one argument is hidden correctly")

View File

@ -0,0 +1,117 @@
#include <catch.hpp>
#include <sstream>
#include <anthem/AST.h>
#include <anthem/Context.h>
#include <anthem/Translation.h>
////////////////////////////////////////////////////////////////////////////////////////////////////
TEST_CASE("[integer detection] Integer variables are correctly detected", "[integer detection]")
{
std::stringstream input;
std::stringstream output;
std::stringstream errors;
anthem::output::Logger logger(output, errors);
anthem::Context context(std::move(logger));
context.performSimplification = true;
context.performCompletion = true;
context.performIntegerDetection = true;
SECTION("simple-to-detect integer parameter")
{
input << "p(X) :- X = 1..5.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in (1..5))\n"
"int(p/1@1)\n");
}
SECTION("simple noninteger parameter")
{
input <<
"p(X) :- X = 1..5.\n"
"p(X) :- X = error.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1 (p(V1) <-> (V1 in (1..5) or V1 = error))\n");
}
SECTION("integer parameter with arithmetics")
{
input << "p(X) :- X = (2 + (1..5)) * 2.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in ((2 + (1..5)) * 2))\n"
"int(p/1@1)\n");
}
SECTION("integer parameter with arithmetics depending on another integer parameter")
{
input
<< "p(X) :- X = 1..5."
<< "q(X) :- p(Y), X = (Y + 5) / 3.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in (1..5))\n"
"forall N2 (q(N2) <-> exists N3 (p(N3) and N2 in ((N3 + 5) / 3)))\n"
"int(p/1@1)\n"
"int(q/1@1)\n");
}
SECTION("multiple mixed parameters")
{
input
<< "p(X) :- X = 1..5."
<< "q(X) :- X = error."
<< "r(A, B, C) :- p(X), A = X ** 2, q(B), p(C).";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in (1..5))\n"
"forall V1 (q(V1) <-> V1 = error)\n"
"forall N2, V2, N3 (r(N2, V2, N3) <-> exists N4 (p(N4) and N2 = (N4 ** 2) and q(V2) and p(N3)))\n"
"int(p/1@1)\n"
"int(r/3@1)\n"
"int(r/3@3)\n");
}
SECTION("integer parameter despite usage of constant symbol")
{
input
<< "p(X) :- X = 2..n.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in (2..n))\n"
"int(p/1@1)\n");
}
SECTION("integer arithmetics are correctly simplified for operators other than division")
{
input
<< "p(X) :- X = 5 + 9 ** 2.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 = (5 + (9 ** 2)))\n"
"int(p/1@1)\n");
}
SECTION("integer arithmetics are not simplified with the division operator")
{
input
<< "p(X) :- X = 5 + 9 / 0.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in (5 + (9 / 0)))\n"
"int(p/1@1)\n");
}
}

View File

@ -0,0 +1,62 @@
#include <catch.hpp>
#include <sstream>
#include <anthem/AST.h>
#include <anthem/Context.h>
#include <anthem/Translation.h>
////////////////////////////////////////////////////////////////////////////////////////////////////
TEST_CASE("[placeholders] Programs with placeholders are correctly completed", "[placeholders]")
{
std::stringstream input;
std::stringstream output;
std::stringstream errors;
anthem::output::Logger logger(output, errors);
anthem::Context context(std::move(logger));
context.performSimplification = true;
context.performCompletion = true;
SECTION("no placeholders")
{
input <<
"colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n"
"forall V3 not vertex(V3)\n");
}
SECTION("single placeholder")
{
input <<
"#external vertex(1).\n"
"colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n");
}
SECTION("complex example: graph coloring")
{
input <<
"#external color(1).\n"
"#external edge(2).\n"
"#external vertex(1).\n"
"#show color/2.\n"
"{color(V, C)} :- vertex(V), color(C).\n"
"covered(V) :- color(V, _).\n"
":- vertex(V), not covered(V).\n"
":- color(V1, C), color(V2, C), edge(V1, V2).";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1, V2 (color(V1, V2) -> (vertex(V1) and color(V2)))\n"
"forall U1 (vertex(U1) -> exists U2 color(U1, U2))\n"
"forall U3, U4, U5 (not color(U3, U4) or not color(U5, U4) or not edge(U3, U5))\n");
}
}

View File

@ -40,7 +40,7 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]")
input << ":- not covered(I), I = 1..n.";
anthem::translate("input", input, context);
CHECK(output.str() == "((not covered(U1) and U1 in 1..n) -> #false)\n");
CHECK(output.str() == "((not covered(U1) and U1 in (1..n)) -> #false)\n");
}
SECTION("comparisons")
@ -50,4 +50,34 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]")
CHECK(output.str() == "(U1 > U2 -> #false)\n");
}
SECTION("biconditionals are replaced with implifactions with choice rules")
{
context.performCompletion = true;
input << "{p(a)}.";
anthem::translate("input", input, context);
CHECK(output.str() == "forall V1 (p(V1) -> V1 = a)\n");
}
SECTION("biconditionals are replaced with implifactions with complicated choice rules")
{
context.performCompletion = true;
input << "{p(n + 5)}.";
anthem::translate("input", input, context);
CHECK(output.str() == "forall V1 (p(V1) -> V1 in (n + 5))\n");
}
SECTION("biconditionals are not replaced with implifactions with nonchoice rules")
{
context.performCompletion = true;
input << "p(a).";
anthem::translate("input", input, context);
CHECK(output.str() == "forall V1 (p(V1) <-> V1 = a)\n");
}
}

View File

@ -24,7 +24,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "p(1..5).";
anthem::translate("input", input, context);
CHECK(output.str() == "(V1 in 1..5 -> p(V1))\n");
CHECK(output.str() == "(V1 in (1..5) -> p(V1))\n");
}
SECTION("simple example 2")
@ -32,7 +32,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "p(N) :- N = 1..5.";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> p(V1))\n");
CHECK(output.str() == "((V1 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> p(V1))\n");
}
SECTION("simple example 3")
@ -48,7 +48,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "p(N, 1, 2) :- N = 1..5.";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> p(V1, V2, V3))\n");
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> p(V1, V2, V3))\n");
}
SECTION("disjunctive head")
@ -57,7 +57,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "q(3, N); p(N, 1, 2) :- N = 1..5.";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
}
SECTION("disjunctive head (alternative syntax)")
@ -66,7 +66,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "q(3, N), p(N, 1, 2) :- N = 1..5.";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
}
SECTION("escaping conflicting variable names")
@ -98,7 +98,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << ":- not p(I), I = 1..n.";
anthem::translate("input", input, context);
CHECK(output.str() == "((exists X1 (X1 in U1 and not p(X1)) and exists X2, X3 (X2 in U1 and X3 in 1..n and X2 = X3)) -> #false)\n");
CHECK(output.str() == "((exists X1 (X1 in U1 and not p(X1)) and exists X2, X3 (X2 in U1 and X3 in (1..n) and X2 = X3)) -> #false)\n");
}
SECTION("disjunctive fact (no arguments)")
@ -178,7 +178,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "p(X, 1..10) :- q(X, 6..12).";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and V2 in 1..10 and exists X1, X2 (X1 in U1 and X2 in 6..12 and q(X1, X2))) -> p(V1, V2))\n");
CHECK(output.str() == "((V1 in U1 and V2 in (1..10) and exists X1, X2 (X1 in U1 and X2 in (6..12) and q(X1, X2))) -> p(V1, V2))\n");
}
SECTION("intervals with variable")
@ -186,7 +186,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << ":- q(N), 1 = 1..N.";
anthem::translate("input", input, context);
CHECK(output.str() == "((exists X1 (X1 in U1 and q(X1)) and exists X2, X3 (X2 in 1 and X3 in 1..U1 and X2 = X3)) -> #false)\n");
CHECK(output.str() == "((exists X1 (X1 in U1 and q(X1)) and exists X2, X3 (X2 in 1 and X3 in (1..U1) and X2 = X3)) -> #false)\n");
}
SECTION("intervals with two variables")
@ -194,7 +194,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << ":- q(M, N), M = 1..N.";
anthem::translate("input", input, context);
CHECK(output.str() == "((exists X1, X2 (X1 in U1 and X2 in U2 and q(X1, X2)) and exists X3, X4 (X3 in U1 and X4 in 1..U2 and X3 = X4)) -> #false)\n");
CHECK(output.str() == "((exists X1, X2 (X1 in U1 and X2 in U2 and q(X1, X2)) and exists X3, X4 (X3 in U1 and X4 in (1..U2) and X3 = X4)) -> #false)\n");
}
SECTION("comparisons")
@ -262,7 +262,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
anthem::translate("input", input, context);
// TODO: eliminate V5: not needed
CHECK(output.str() == "((V1 in 1..3 and V2 in U1 and V3 in 2..4 and p(V1, V2)) -> p(V1, V2))\n((V4 in 1..3 and V5 in U2 and V6 in 2..4 and q(V6)) -> q(V6))\n");
CHECK(output.str() == "((V1 in (1..3) and V2 in U1 and V3 in (2..4) and p(V1, V2)) -> p(V1, V2))\n((V4 in (1..3) and V5 in U2 and V6 in (2..4) and q(V6)) -> q(V6))\n");
}
SECTION("choice rule with body")
@ -296,4 +296,12 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
CHECK(output.str() == "((V1 in U1 and V2 in U2 and exists X1, X2 (X1 in U3 and X2 in U4 and q(X1, X2))) -> p(V1, V2))\n");
}
SECTION("exponentiation operator")
{
input << "p(N, N ** N) :- N = 1..n.";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and V2 in (U1 ** U1) and exists X1, X2 (X1 in U1 and X2 in (1..n) and X1 = X2)) -> p(V1, V2))\n");
}
}

73
tests/TestUnsupported.cpp Normal file
View File

@ -0,0 +1,73 @@
#include <catch.hpp>
#include <sstream>
#include <anthem/AST.h>
#include <anthem/Context.h>
#include <anthem/Translation.h>
////////////////////////////////////////////////////////////////////////////////////////////////////
TEST_CASE("[unsupported] Errors are correctly issued when using unsupported features", "[unsupported]")
{
std::stringstream input;
std::stringstream output;
std::stringstream errors;
anthem::output::Logger logger(output, errors);
anthem::Context context(std::move(logger));
SECTION("rules with disjunctive head are unsupported")
{
context.performCompletion = true;
input << "a; b.";
CHECK_THROWS(anthem::translate("input", input, context));
}
SECTION("rules with disjunctive head containing elements with arguments are unsupported")
{
context.performCompletion = true;
input << "p(a); p(b).";
CHECK_THROWS(anthem::translate("input", input, context));
}
SECTION("singleton choice rules are supported")
{
context.performCompletion = true;
input << "{a}.";
CHECK_NOTHROW(anthem::translate("input", input, context));
}
SECTION("singleton choice rules containing an element with arguments are supported")
{
context.performCompletion = true;
input << "{p(a)}.";
CHECK_NOTHROW(anthem::translate("input", input, context));
}
SECTION("choice rules with multiple simple elements are supported")
{
context.performCompletion = true;
input << "{a; b}.";
CHECK_NOTHROW(anthem::translate("input", input, context));
}
SECTION("choice rules with multiple elements with arguments are unsupported")
{
context.performCompletion = true;
input << "{p(a); p(b)}.";
CHECK_THROWS(anthem::translate("input", input, context));
}
}