Compare commits
No commits in common. "develop" and "v0.1.6" have entirely different histories.
|
@ -1,9 +0,0 @@
|
||||||
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
|
|
|
@ -1,10 +0,0 @@
|
||||||
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
17
.ci/ci.sh
|
@ -1,17 +0,0 @@
|
||||||
#!/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
|
|
|
@ -3,7 +3,4 @@
|
||||||
url = https://github.com/potassco/clingo
|
url = https://github.com/potassco/clingo
|
||||||
[submodule "lib/catch"]
|
[submodule "lib/catch"]
|
||||||
path = lib/catch
|
path = lib/catch
|
||||||
url = https://github.com/catchorg/Catch2
|
url = https://github.com/philsquared/Catch
|
||||||
[submodule "lib/cxxopts"]
|
|
||||||
path = lib/cxxopts
|
|
||||||
url = https://github.com/jarro2783/cxxopts
|
|
||||||
|
|
58
.travis.yml
58
.travis.yml
|
@ -1,25 +1,47 @@
|
||||||
sudo: required
|
# Use container-based distribution
|
||||||
|
sudo: false
|
||||||
services:
|
language: c++
|
||||||
- docker
|
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
|
||||||
matrix:
|
matrix:
|
||||||
include:
|
include:
|
||||||
- env: distribution=arch-latest toolchain=gcc
|
- env: COMPILER_NAME=g++ _CXX=g++-5 _CC=gcc-5
|
||||||
os: linux
|
os: linux
|
||||||
language: cpp
|
language: cpp
|
||||||
- env: distribution=arch-latest toolchain=clang
|
addons:
|
||||||
|
apt:
|
||||||
|
sources:
|
||||||
|
- *default_sources
|
||||||
|
packages:
|
||||||
|
- *default_packages
|
||||||
|
- g++-5
|
||||||
|
- env: COMPILER_NAME=g++ _CXX=g++-6 _CC=gcc-6
|
||||||
os: linux
|
os: linux
|
||||||
language: cpp
|
language: cpp
|
||||||
- env: distribution=ubuntu-18.04 toolchain=gcc
|
addons:
|
||||||
os: linux
|
apt:
|
||||||
language: cpp
|
sources:
|
||||||
- env: distribution=ubuntu-18.04 toolchain=clang
|
- *default_sources
|
||||||
os: linux
|
packages:
|
||||||
language: cpp
|
- *default_packages
|
||||||
|
- g++-6
|
||||||
before_install:
|
|
||||||
- docker build --build-arg toolchain=${toolchain} -t ${distribution} - < .ci/Dockerfile-${distribution}
|
|
||||||
|
|
||||||
script:
|
script:
|
||||||
- docker run --mount source=$(pwd),target=/app,type=bind -w /app ${distribution} /bin/bash -c ".ci/ci.sh ${toolchain}"
|
- 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
|
||||||
|
|
58
CHANGELOG.md
58
CHANGELOG.md
|
@ -2,45 +2,9 @@
|
||||||
|
|
||||||
## (unreleased)
|
## (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)
|
## 0.1.6 (2017-06-12)
|
||||||
|
|
||||||
### Features
|
Features:
|
||||||
|
|
||||||
* unique IDs for all variables (user-defined variables are renamed)
|
* unique IDs for all variables (user-defined variables are renamed)
|
||||||
* support for hiding predicates from completed output by using `#show` statements
|
* support for hiding predicates from completed output by using `#show` statements
|
||||||
|
@ -48,7 +12,7 @@
|
||||||
* command-line option `--parentheses` to fully parenthesize the output
|
* command-line option `--parentheses` to fully parenthesize the output
|
||||||
* adds multiple example instances for experimenting
|
* adds multiple example instances for experimenting
|
||||||
|
|
||||||
### Bug Fixes
|
Bug Fixes:
|
||||||
|
|
||||||
* adds missing error message when attempting to read inaccessible file
|
* adds missing error message when attempting to read inaccessible file
|
||||||
* removes unnecessary parentheses after simplification
|
* removes unnecessary parentheses after simplification
|
||||||
|
@ -56,52 +20,52 @@
|
||||||
|
|
||||||
## 0.1.5 (2017-05-04)
|
## 0.1.5 (2017-05-04)
|
||||||
|
|
||||||
### Bug Fixes
|
Bug Fixes:
|
||||||
|
|
||||||
* fixes lost signs with negated 0-ary predicates
|
* fixes lost signs with negated 0-ary predicates
|
||||||
|
|
||||||
## 0.1.4 (2017-04-12)
|
## 0.1.4 (2017-04-12)
|
||||||
|
|
||||||
### Features
|
Features:
|
||||||
|
|
||||||
* completion of input programs (optional)
|
* completion of input programs (optional)
|
||||||
* command-line option `--complete` to turn on completion
|
* command-line option `--complete` to turn on completion
|
||||||
|
|
||||||
## 0.1.3 (2017-03-30)
|
## 0.1.3 (2017-03-30)
|
||||||
|
|
||||||
### Features
|
Features:
|
||||||
|
|
||||||
* support for anonymous variables
|
* support for anonymous variables
|
||||||
|
|
||||||
### Bug Fixes
|
Bug Fixes:
|
||||||
|
|
||||||
* fixes incorrectly simplified rules with comparisons
|
* fixes incorrectly simplified rules with comparisons
|
||||||
* fixes misleading error message concerning negated, unsupported body literals
|
* fixes misleading error message concerning negated, unsupported body literals
|
||||||
|
|
||||||
## 0.1.2 (2017-03-23)
|
## 0.1.2 (2017-03-23)
|
||||||
|
|
||||||
### Features
|
Features:
|
||||||
|
|
||||||
* simplification of output formulas (optional)
|
* simplification of output formulas (optional)
|
||||||
* command-line option `--simplify` to turn on simplification
|
* command-line option `--simplify` to turn on simplification
|
||||||
|
|
||||||
### Bug Fixes
|
Bug Fixes:
|
||||||
|
|
||||||
* fixes incorrectly translated choice rules with multiple elements in the head aggregate
|
* fixes incorrectly translated choice rules with multiple elements in the head aggregate
|
||||||
|
|
||||||
### Internal
|
Internal:
|
||||||
|
|
||||||
* explicit syntax tree representation for first-order formulas
|
* explicit syntax tree representation for first-order formulas
|
||||||
|
|
||||||
## 0.1.1 (2017-03-06)
|
## 0.1.1 (2017-03-06)
|
||||||
|
|
||||||
### Features
|
Features:
|
||||||
|
|
||||||
* support for choice rules (without guards)
|
* support for choice rules (without guards)
|
||||||
|
|
||||||
## 0.1.0 (2016-11-24)
|
## 0.1.0 (2016-11-24)
|
||||||
|
|
||||||
### Features
|
Features:
|
||||||
|
|
||||||
* initial support for translating rules in *Essential Gringo* (excluding aggregates) to first-order logic formulas
|
* 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
|
* command-line option `--color` to autodetect, enable, or disable color output
|
||||||
|
|
|
@ -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 "-Wall -Wextra -Wpedantic ${CMAKE_CXX_FLAGS}")
|
||||||
set(CMAKE_CXX_FLAGS_DEBUG "-g ${CMAKE_CXX_FLAGS_DEBUG}")
|
set(CMAKE_CXX_FLAGS_DEBUG "-g ${CMAKE_CXX_FLAGS_DEBUG}")
|
||||||
|
|
||||||
set(CMAKE_CXX_STANDARD 17)
|
set(CMAKE_CXX_STANDARD 14)
|
||||||
set(CMAKE_CXX_STANDARD_REQUIRED ON)
|
set(CMAKE_CXX_STANDARD_REQUIRED ON)
|
||||||
set(CMAKE_CXX_EXTENSIONS OFF)
|
set(CMAKE_CXX_EXTENSIONS OFF)
|
||||||
|
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
# The MIT License (MIT)
|
# The MIT License (MIT)
|
||||||
|
|
||||||
Copyright © 2016–2018 Patrick Lühne
|
Copyright © 2016–2017 Patrick Lühne
|
||||||
|
|
||||||
Permission is hereby granted, free of charge, to any person obtaining a copy
|
Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||||
of this software and associated documentation files (the "Software"), to deal
|
of this software and associated documentation files (the "Software"), to deal
|
||||||
|
|
10
README.md
10
README.md
|
@ -9,17 +9,15 @@
|
||||||
## Usage
|
## Usage
|
||||||
|
|
||||||
```bash
|
```bash
|
||||||
$ anthem [--no-complete] [--no-simplify] [--no-detect-integers] file...
|
$ anthem [--simplify] file...
|
||||||
```
|
```
|
||||||
|
|
||||||
By default, `anthem` performs Clark’s completion on the translated formulas, detects which variables are integer, and simplifies the output by applying several basic transformation rules.
|
With the option `--simplify`, output formulas are simplified 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
|
## Building
|
||||||
|
|
||||||
`anthem` requires [CMake](https://cmake.org/) for 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++17 compiler (GCC ≥ 7.3 or clang ≥ 5.0).
|
After installing the dependencies, `anthem` is built with a C++14 compiler (GCC ≥ 6.1 or clang ≥ 3.8).
|
||||||
|
|
||||||
```bash
|
```bash
|
||||||
$ git clone https://github.com/potassco/anthem.git
|
$ git clone https://github.com/potassco/anthem.git
|
||||||
|
|
|
@ -1,5 +1,7 @@
|
||||||
set(target anthem-app)
|
set(target anthem-app)
|
||||||
|
|
||||||
|
find_package(Boost 1.55.0 COMPONENTS program_options system filesystem REQUIRED)
|
||||||
|
|
||||||
file(GLOB core_sources "*.cpp")
|
file(GLOB core_sources "*.cpp")
|
||||||
file(GLOB core_headers "*.h")
|
file(GLOB core_headers "*.h")
|
||||||
|
|
||||||
|
@ -9,10 +11,11 @@ set(sources
|
||||||
)
|
)
|
||||||
|
|
||||||
set(includes
|
set(includes
|
||||||
${PROJECT_SOURCE_DIR}/lib/cxxopts/include
|
${Boost_INCLUDE_DIRS}
|
||||||
)
|
)
|
||||||
|
|
||||||
set(libraries
|
set(libraries
|
||||||
|
${Boost_LIBRARIES}
|
||||||
anthem
|
anthem
|
||||||
)
|
)
|
||||||
|
|
||||||
|
|
90
app/main.cpp
90
app/main.cpp
|
@ -1,6 +1,6 @@
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
|
|
||||||
#include <cxxopts.hpp>
|
#include <boost/program_options.hpp>
|
||||||
|
|
||||||
#include <anthem/AST.h>
|
#include <anthem/AST.h>
|
||||||
#include <anthem/Context.h>
|
#include <anthem/Context.h>
|
||||||
|
@ -10,72 +10,63 @@ int main(int argc, char **argv)
|
||||||
{
|
{
|
||||||
anthem::Context context;
|
anthem::Context context;
|
||||||
|
|
||||||
cxxopts::Options options("anthem", "Translate ASP programs to the language of first-order theorem provers.");
|
namespace po = boost::program_options;
|
||||||
|
|
||||||
options.add_options()
|
po::options_description description("Allowed options");
|
||||||
("h,help", "Display this help message")
|
description.add_options()
|
||||||
("v,version", "Display version information")
|
("help,h", "Display this help message")
|
||||||
("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
|
("version,v", "Display version information")
|
||||||
("no-simplify", "Do not simplify the output")
|
("input,i", po::value<std::vector<std::string>>(), "Input files")
|
||||||
("no-complete", "Do not perform completion")
|
("simplify,s", po::bool_switch(&context.performSimplification), "Simplify the output")
|
||||||
("no-detect-integers", "Do not detect integer variables")
|
("complete,c", po::bool_switch(&context.performCompletion), "Perform completion")
|
||||||
("color", "Colorize output (always, never, auto)", cxxopts::value<std::string>()->default_value("auto"))
|
("color", po::value<std::string>()->default_value("auto"), "Colorize output (always, never, auto)")
|
||||||
("parentheses", "Parenthesis style (normal, full)", cxxopts::value<std::string>()->default_value("normal"))
|
("parentheses", po::value<std::string>()->default_value("normal"), "Parenthesis style (normal, full)")
|
||||||
("p,log-priority", "Log messages starting from this priority (debug, info, warning, error)", cxxopts::value<std::string>()->default_value("info"));
|
("log-priority,p", po::value<std::string>()->default_value("warning"), "Log messages starting from this priority (debug, info, warning, error)");
|
||||||
|
|
||||||
options.parse_positional("input");
|
po::positional_options_description positionalOptionsDescription;
|
||||||
options.positional_help("[<input file...>]");
|
positionalOptionsDescription.add("input", -1);
|
||||||
|
|
||||||
|
po::variables_map variablesMap;
|
||||||
|
|
||||||
const auto printHelp =
|
const auto printHelp =
|
||||||
[&]()
|
[&]()
|
||||||
{
|
{
|
||||||
std::cout << options.help();
|
std::cout
|
||||||
|
<< "Usage: anthem [options] file..." << std::endl
|
||||||
|
<< "Translate ASP programs to the language of first-order theorem provers." << std::endl << std::endl
|
||||||
|
<< description;
|
||||||
};
|
};
|
||||||
|
|
||||||
bool help;
|
|
||||||
bool version;
|
|
||||||
std::vector<std::string> inputFiles;
|
|
||||||
std::string colorPolicyString;
|
|
||||||
std::string parenthesisStyleString;
|
|
||||||
std::string logPriorityString;
|
|
||||||
|
|
||||||
try
|
try
|
||||||
{
|
{
|
||||||
const auto parseResult = options.parse(argc, argv);
|
po::store(po::command_line_parser(argc, argv)
|
||||||
|
.options(description)
|
||||||
help = (parseResult.count("help") > 0);
|
.positional(positionalOptionsDescription)
|
||||||
version = (parseResult.count("version") > 0);
|
.run(),
|
||||||
|
variablesMap);
|
||||||
if (parseResult.count("input") > 0)
|
po::notify(variablesMap);
|
||||||
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 std::exception &exception)
|
catch (const po::error &e)
|
||||||
{
|
{
|
||||||
context.logger.log(anthem::output::Priority::Error) << exception.what();
|
context.logger.log(anthem::output::Priority::Error) << e.what();
|
||||||
context.logger.errorStream() << std::endl;
|
|
||||||
printHelp();
|
printHelp();
|
||||||
return EXIT_FAILURE;
|
return EXIT_FAILURE;
|
||||||
}
|
}
|
||||||
|
|
||||||
if (help)
|
if (variablesMap.count("help"))
|
||||||
{
|
{
|
||||||
printHelp();
|
printHelp();
|
||||||
return EXIT_SUCCESS;
|
return EXIT_SUCCESS;
|
||||||
}
|
}
|
||||||
|
|
||||||
if (version)
|
if (variablesMap.count("version"))
|
||||||
{
|
{
|
||||||
std::cout << "anthem version 0.1.9+git" << std::endl;
|
std::cout << "anthem version 0.1.7-git" << std::endl;
|
||||||
return EXIT_SUCCESS;
|
return EXIT_SUCCESS;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
const auto colorPolicyString = variablesMap["color"].as<std::string>();
|
||||||
|
|
||||||
if (colorPolicyString == "auto")
|
if (colorPolicyString == "auto")
|
||||||
context.logger.setColorPolicy(anthem::output::ColorStream::ColorPolicy::Auto);
|
context.logger.setColorPolicy(anthem::output::ColorStream::ColorPolicy::Auto);
|
||||||
else if (colorPolicyString == "never")
|
else if (colorPolicyString == "never")
|
||||||
|
@ -90,18 +81,22 @@ int main(int argc, char **argv)
|
||||||
return EXIT_FAILURE;
|
return EXIT_FAILURE;
|
||||||
}
|
}
|
||||||
|
|
||||||
if (parenthesisStyleString == "normal")
|
const auto parenthesisStyle = variablesMap["parentheses"].as<std::string>();
|
||||||
|
|
||||||
|
if (parenthesisStyle == "normal")
|
||||||
context.parenthesisStyle = anthem::ast::ParenthesisStyle::Normal;
|
context.parenthesisStyle = anthem::ast::ParenthesisStyle::Normal;
|
||||||
else if (parenthesisStyleString == "full")
|
else if (parenthesisStyle == "full")
|
||||||
context.parenthesisStyle = anthem::ast::ParenthesisStyle::Full;
|
context.parenthesisStyle = anthem::ast::ParenthesisStyle::Full;
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
context.logger.log(anthem::output::Priority::Error) << "unknown parenthesis style “" << parenthesisStyleString << "”";
|
context.logger.log(anthem::output::Priority::Error) << "unknown parenthesis style “" << parenthesisStyle << "”";
|
||||||
context.logger.errorStream() << std::endl;
|
context.logger.errorStream() << std::endl;
|
||||||
printHelp();
|
printHelp();
|
||||||
return EXIT_FAILURE;
|
return EXIT_FAILURE;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
const auto logPriorityString = variablesMap["log-priority"].as<std::string>();
|
||||||
|
|
||||||
try
|
try
|
||||||
{
|
{
|
||||||
const auto logPriority = anthem::output::priorityFromName(logPriorityString.c_str());
|
const auto logPriority = anthem::output::priorityFromName(logPriorityString.c_str());
|
||||||
|
@ -117,8 +112,11 @@ int main(int argc, char **argv)
|
||||||
|
|
||||||
try
|
try
|
||||||
{
|
{
|
||||||
if (!inputFiles.empty())
|
if (variablesMap.count("input"))
|
||||||
|
{
|
||||||
|
const auto &inputFiles = variablesMap["input"].as<std::vector<std::string>>();
|
||||||
anthem::translate(inputFiles, context);
|
anthem::translate(inputFiles, context);
|
||||||
|
}
|
||||||
else
|
else
|
||||||
anthem::translate("std::cin", std::cin, context);
|
anthem::translate("std::cin", std::cin, context);
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,2 +0,0 @@
|
||||||
p(a).
|
|
||||||
{q(a)}.
|
|
|
@ -1,18 +1,12 @@
|
||||||
% assign a set of colors to each vertex
|
colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).
|
||||||
{color(V, C)} :- vertex(V), color(C).
|
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).
|
||||||
|
|
||||||
% at most one color per vertex
|
:- edge(V1, V2), colored(V1, C), colored(V2, C).
|
||||||
:- color(V, C1), color(V, C2), C1 != C2.
|
|
||||||
|
|
||||||
% at least one color per vertex
|
vertex(a).
|
||||||
covered(V) :- color(V, _).
|
vertex(b).
|
||||||
:- vertex(V), not covered(V).
|
vertex(c).
|
||||||
|
|
||||||
% adjacent vertices don’t share the same color
|
edge(a, b).
|
||||||
:- color(V1, C), color(V2, C), edge(V1, V2).
|
edge(a, c).
|
||||||
|
|
||||||
#show color/2.
|
|
||||||
|
|
||||||
#external vertex(1).
|
|
||||||
#external edge(2).
|
|
||||||
#external color(1).
|
|
||||||
|
|
|
@ -1,11 +0,0 @@
|
||||||
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.
|
|
|
@ -1,12 +0,0 @@
|
||||||
#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.
|
|
|
@ -1,4 +0,0 @@
|
||||||
#show prime/1.
|
|
||||||
|
|
||||||
composite(I * J) :- I = 2..n, J = 2..n.
|
|
||||||
prime(N) :- N = 2..n, not composite(N).
|
|
|
@ -1,5 +1,3 @@
|
||||||
#show in/2.
|
|
||||||
|
|
||||||
{in(1..n, 1..r)}.
|
{in(1..n, 1..r)}.
|
||||||
covered(I) :- in(I, S).
|
covered(I) :- in(I, S).
|
||||||
|
|
||||||
|
|
|
@ -1,9 +0,0 @@
|
||||||
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).
|
|
|
@ -1,5 +0,0 @@
|
||||||
s(X) :- p(X).
|
|
||||||
s(X) :- q(X).
|
|
||||||
|
|
||||||
#external p(1).
|
|
||||||
#external q(1).
|
|
|
@ -2,7 +2,6 @@
|
||||||
#define __ANTHEM__AST_H
|
#define __ANTHEM__AST_H
|
||||||
|
|
||||||
#include <anthem/ASTForward.h>
|
#include <anthem/ASTForward.h>
|
||||||
#include <anthem/Utils.h>
|
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
|
@ -33,8 +32,7 @@ struct BinaryOperation
|
||||||
Minus,
|
Minus,
|
||||||
Multiplication,
|
Multiplication,
|
||||||
Division,
|
Division,
|
||||||
Modulo,
|
Modulo
|
||||||
Power
|
|
||||||
};
|
};
|
||||||
|
|
||||||
explicit BinaryOperation(Operator operator_, Term &&left, Term &&right)
|
explicit BinaryOperation(Operator operator_, Term &&left, Term &&right)
|
||||||
|
@ -104,15 +102,32 @@ struct Comparison
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
struct Function
|
struct Constant
|
||||||
{
|
{
|
||||||
explicit Function(FunctionDeclaration *declaration)
|
explicit Constant(std::string &&name)
|
||||||
: declaration{declaration}
|
: name{std::move(name)}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
explicit Function(FunctionDeclaration *declaration, std::vector<Term> &&arguments)
|
Constant(const Constant &other) = delete;
|
||||||
: declaration{declaration},
|
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(std::string &&name, std::vector<Term> &&arguments)
|
||||||
|
: name{std::move(name)},
|
||||||
arguments{std::move(arguments)}
|
arguments{std::move(arguments)}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
@ -122,33 +137,8 @@ struct Function
|
||||||
Function(Function &&other) noexcept = default;
|
Function(Function &&other) noexcept = default;
|
||||||
Function &operator=(Function &&other) noexcept = default;
|
Function &operator=(Function &&other) noexcept = default;
|
||||||
|
|
||||||
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;
|
std::string name;
|
||||||
size_t arity;
|
std::vector<Term> arguments;
|
||||||
Domain domain{Domain::Noninteger};
|
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
@ -213,13 +203,13 @@ struct Interval
|
||||||
|
|
||||||
struct Predicate
|
struct Predicate
|
||||||
{
|
{
|
||||||
explicit Predicate(PredicateDeclaration *declaration)
|
explicit Predicate(std::string &&name)
|
||||||
: declaration{declaration}
|
: name{std::move(name)}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
explicit Predicate(PredicateDeclaration *declaration, std::vector<Term> &&arguments)
|
explicit Predicate(std::string &&name, std::vector<Term> &&arguments)
|
||||||
: declaration{declaration},
|
: name{std::move(name)},
|
||||||
arguments{std::move(arguments)}
|
arguments{std::move(arguments)}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
@ -229,47 +219,35 @@ struct Predicate
|
||||||
Predicate(Predicate &&other) noexcept = default;
|
Predicate(Predicate &&other) noexcept = default;
|
||||||
Predicate &operator=(Predicate &&other) noexcept = default;
|
Predicate &operator=(Predicate &&other) noexcept = default;
|
||||||
|
|
||||||
PredicateDeclaration *declaration{nullptr};
|
std::size_t arity() const
|
||||||
|
{
|
||||||
|
return arguments.size();
|
||||||
|
}
|
||||||
|
|
||||||
|
std::string name;
|
||||||
std::vector<Term> arguments;
|
std::vector<Term> arguments;
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
struct PredicateDeclaration
|
// TODO: make more use of this class
|
||||||
|
struct PredicateSignature
|
||||||
{
|
{
|
||||||
enum class Visibility
|
explicit PredicateSignature(std::string &&name, size_t arity)
|
||||||
{
|
|
||||||
Default,
|
|
||||||
Visible,
|
|
||||||
Hidden
|
|
||||||
};
|
|
||||||
|
|
||||||
struct Parameter
|
|
||||||
{
|
|
||||||
Domain domain{Domain::Unknown};
|
|
||||||
};
|
|
||||||
|
|
||||||
explicit PredicateDeclaration(std::string &&name, size_t arity)
|
|
||||||
: name{std::move(name)},
|
: name{std::move(name)},
|
||||||
parameters{std::vector<Parameter>(arity)}
|
arity{arity}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
PredicateDeclaration(const PredicateDeclaration &other) = delete;
|
PredicateSignature(const PredicateSignature &other) = delete;
|
||||||
PredicateDeclaration &operator=(const PredicateDeclaration &other) = delete;
|
PredicateSignature &operator=(const PredicateSignature &other) = delete;
|
||||||
PredicateDeclaration(PredicateDeclaration &&other) noexcept = default;
|
// TODO: make noexcept again
|
||||||
PredicateDeclaration &operator=(PredicateDeclaration &&other) noexcept = default;
|
// GCC versions before 7 don’t declare moving std::string noexcept and would complain here
|
||||||
|
PredicateSignature(PredicateSignature &&other) = default;
|
||||||
size_t arity() const noexcept
|
PredicateSignature &operator=(PredicateSignature &&other) = default;
|
||||||
{
|
|
||||||
return parameters.size();
|
|
||||||
}
|
|
||||||
|
|
||||||
std::string name;
|
std::string name;
|
||||||
std::vector<Parameter> parameters;
|
size_t arity;
|
||||||
bool isUsed{false};
|
|
||||||
bool isExternal{false};
|
|
||||||
Visibility visibility{Visibility::Default};
|
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
@ -314,30 +292,6 @@ 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
|
struct Variable
|
||||||
{
|
{
|
||||||
explicit Variable(VariableDeclaration *declaration)
|
explicit Variable(VariableDeclaration *declaration)
|
||||||
|
@ -381,7 +335,6 @@ struct VariableDeclaration
|
||||||
VariableDeclaration &operator=(VariableDeclaration &&other) = default;
|
VariableDeclaration &operator=(VariableDeclaration &&other) = default;
|
||||||
|
|
||||||
Type type;
|
Type type;
|
||||||
Domain domain{Domain::Unknown};
|
|
||||||
std::string name;
|
std::string name;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
@ -22,6 +22,7 @@ namespace ast
|
||||||
BinaryOperation prepareCopy(const BinaryOperation &other);
|
BinaryOperation prepareCopy(const BinaryOperation &other);
|
||||||
Boolean prepareCopy(const Boolean &other);
|
Boolean prepareCopy(const Boolean &other);
|
||||||
Comparison prepareCopy(const Comparison &other);
|
Comparison prepareCopy(const Comparison &other);
|
||||||
|
Constant prepareCopy(const Constant &other);
|
||||||
Function prepareCopy(const Function &other);
|
Function prepareCopy(const Function &other);
|
||||||
In prepareCopy(const In &other);
|
In prepareCopy(const In &other);
|
||||||
Integer prepareCopy(const Integer &other);
|
Integer prepareCopy(const Integer &other);
|
||||||
|
|
|
@ -24,10 +24,10 @@ struct BinaryOperation;
|
||||||
struct Biconditional;
|
struct Biconditional;
|
||||||
struct Boolean;
|
struct Boolean;
|
||||||
struct Comparison;
|
struct Comparison;
|
||||||
|
struct Constant;
|
||||||
struct Exists;
|
struct Exists;
|
||||||
struct ForAll;
|
struct ForAll;
|
||||||
struct Function;
|
struct Function;
|
||||||
struct FunctionDeclaration;
|
|
||||||
struct Implies;
|
struct Implies;
|
||||||
struct In;
|
struct In;
|
||||||
struct Integer;
|
struct Integer;
|
||||||
|
@ -35,10 +35,8 @@ struct Interval;
|
||||||
struct Not;
|
struct Not;
|
||||||
struct Or;
|
struct Or;
|
||||||
struct Predicate;
|
struct Predicate;
|
||||||
struct PredicateDeclaration;
|
|
||||||
struct SpecialInteger;
|
struct SpecialInteger;
|
||||||
struct String;
|
struct String;
|
||||||
struct UnaryOperation;
|
|
||||||
struct Variable;
|
struct Variable;
|
||||||
struct VariableDeclaration;
|
struct VariableDeclaration;
|
||||||
using VariableDeclarationPointer = std::unique_ptr<VariableDeclaration>;
|
using VariableDeclarationPointer = std::unique_ptr<VariableDeclaration>;
|
||||||
|
@ -64,12 +62,12 @@ using Formula = Clingo::Variant<
|
||||||
using Term = Clingo::Variant<
|
using Term = Clingo::Variant<
|
||||||
BinaryOperation,
|
BinaryOperation,
|
||||||
Boolean,
|
Boolean,
|
||||||
|
Constant,
|
||||||
Function,
|
Function,
|
||||||
Integer,
|
Integer,
|
||||||
Interval,
|
Interval,
|
||||||
SpecialInteger,
|
SpecialInteger,
|
||||||
String,
|
String,
|
||||||
UnaryOperation,
|
|
||||||
Variable>;
|
Variable>;
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
@ -1,11 +1,10 @@
|
||||||
#ifndef __ANTHEM__AST_UTILS_H
|
#ifndef __ANTHEM__AST_UTILS_H
|
||||||
#define __ANTHEM__AST_UTILS_H
|
#define __ANTHEM__AST_UTILS_H
|
||||||
|
|
||||||
#include <optional>
|
#include <experimental/optional>
|
||||||
|
|
||||||
#include <anthem/AST.h>
|
#include <anthem/AST.h>
|
||||||
#include <anthem/ASTVisitors.h>
|
#include <anthem/ASTVisitors.h>
|
||||||
#include <anthem/Context.h>
|
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
|
@ -29,13 +28,19 @@ class VariableStack
|
||||||
void push(Layer layer);
|
void push(Layer layer);
|
||||||
void pop();
|
void pop();
|
||||||
|
|
||||||
std::optional<VariableDeclaration *> findUserVariableDeclaration(const char *variableName) const;
|
std::experimental::optional<VariableDeclaration *> findUserVariableDeclaration(const char *variableName) const;
|
||||||
bool contains(const VariableDeclaration &variableDeclaration) const;
|
bool contains(const VariableDeclaration &variableDeclaration) const;
|
||||||
|
|
||||||
private:
|
private:
|
||||||
std::vector<Layer> m_layers;
|
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
|
// Replacing Variables
|
||||||
|
@ -90,21 +95,6 @@ struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor<ReplaceV
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
// Accessing Variable Domains
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
struct DefaultVariableDomainAccessor
|
|
||||||
{
|
|
||||||
Domain operator()(const ast::Variable &variable)
|
|
||||||
{
|
|
||||||
return variable.declaration->domain;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -123,6 +123,12 @@ struct RecursiveTermVisitor
|
||||||
return T::accept(boolean, term, std::forward<Arguments>(arguments)...);
|
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>
|
template <class... Arguments>
|
||||||
ReturnType visit(Function &function, Term &term, Arguments &&... arguments)
|
ReturnType visit(Function &function, Term &term, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
|
@ -159,14 +165,6 @@ struct RecursiveTermVisitor
|
||||||
return T::accept(string, term, std::forward<Arguments>(arguments)...);
|
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>
|
template <class... Arguments>
|
||||||
ReturnType visit(Variable &variable, Term &term, Arguments &&... arguments)
|
ReturnType visit(Variable &variable, Term &term, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
|
|
|
@ -43,22 +43,19 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp
|
||||||
struct BodyTermTranslateVisitor
|
struct BodyTermTranslateVisitor
|
||||||
{
|
{
|
||||||
// TODO: refactor
|
// TODO: refactor
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Function &function,
|
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)
|
||||||
const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext,
|
|
||||||
Context &context, ast::VariableStack &variableStack)
|
|
||||||
{
|
{
|
||||||
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
|
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
|
||||||
throw TranslationException(literal.location, "double-negated literals currently unsupported");
|
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())
|
if (function.arguments.empty())
|
||||||
{
|
{
|
||||||
|
auto predicate = ast::Formula::make<ast::Predicate>(std::string(function.name));
|
||||||
|
|
||||||
if (literal.sign == Clingo::AST::Sign::None)
|
if (literal.sign == Clingo::AST::Sign::None)
|
||||||
return ast::Predicate(predicateDeclaration);
|
return std::move(predicate);
|
||||||
else if (literal.sign == Clingo::AST::Sign::Negation)
|
else if (literal.sign == Clingo::AST::Sign::Negation)
|
||||||
return ast::Formula::make<ast::Not>(ast::Predicate(predicateDeclaration));
|
return ast::Formula::make<ast::Not>(std::move(predicate));
|
||||||
}
|
}
|
||||||
|
|
||||||
// Create new body variable declarations
|
// Create new body variable declarations
|
||||||
|
@ -76,12 +73,12 @@ struct BodyTermTranslateVisitor
|
||||||
for (size_t i = 0; i < function.arguments.size(); i++)
|
for (size_t i = 0; i < function.arguments.size(); i++)
|
||||||
{
|
{
|
||||||
auto &argument = function.arguments[i];
|
auto &argument = function.arguments[i];
|
||||||
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, context, variableStack)));
|
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, variableStack)));
|
||||||
}
|
}
|
||||||
|
|
||||||
variableStack.pop();
|
variableStack.pop();
|
||||||
|
|
||||||
ast::Predicate predicate(predicateDeclaration);
|
ast::Predicate predicate(std::string(function.name));
|
||||||
predicate.arguments.reserve(function.arguments.size());
|
predicate.arguments.reserve(function.arguments.size());
|
||||||
|
|
||||||
for (size_t i = 0; i < function.arguments.size(); i++)
|
for (size_t i = 0; i < function.arguments.size(); i++)
|
||||||
|
@ -96,13 +93,12 @@ struct BodyTermTranslateVisitor
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &,
|
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &)
|
||||||
const Clingo::AST::Term &term, RuleContext &, Context &, ast::VariableStack &)
|
|
||||||
{
|
{
|
||||||
assert(!term.data.is<Clingo::AST::Function>());
|
assert(!term.data.is<Clingo::AST::Function>());
|
||||||
|
|
||||||
throw TranslationException(term.location, "term currently unsupported in this context, expected function");
|
throw TranslationException(term.location, "term currently unsupported in this context, expected function");
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -110,18 +106,18 @@ struct BodyTermTranslateVisitor
|
||||||
|
|
||||||
struct BodyLiteralTranslateVisitor
|
struct BodyLiteralTranslateVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, ast::VariableStack &)
|
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &)
|
||||||
{
|
{
|
||||||
return ast::Formula::make<ast::Boolean>(boolean.value);
|
return ast::Formula::make<ast::Boolean>(boolean.value);
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
|
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, context, variableStack);
|
return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, variableStack);
|
||||||
}
|
}
|
||||||
|
|
||||||
// TODO: refactor
|
// TODO: refactor
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
|
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
// Comparisons should never have a sign, because these are converted to positive comparisons by clingo
|
// Comparisons should never have a sign, because these are converted to positive comparisons by clingo
|
||||||
if (literal.sign != Clingo::AST::Sign::None)
|
if (literal.sign != Clingo::AST::Sign::None)
|
||||||
|
@ -136,18 +132,18 @@ struct BodyLiteralTranslateVisitor
|
||||||
|
|
||||||
ast::And conjunction;
|
ast::And conjunction;
|
||||||
conjunction.arguments.reserve(3);
|
conjunction.arguments.reserve(3);
|
||||||
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[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, context, 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::Comparison>(operator_, ast::Variable(parameters[0].get()), ast::Variable(parameters[1].get())));
|
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));
|
return ast::Formula::make<ast::Exists>(std::move(parameters), std::move(conjunction));
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, ast::VariableStack &)
|
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &)
|
||||||
{
|
{
|
||||||
throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term");
|
throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term");
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -155,19 +151,19 @@ struct BodyLiteralTranslateVisitor
|
||||||
|
|
||||||
struct BodyBodyLiteralTranslateVisitor
|
struct BodyBodyLiteralTranslateVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
|
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
if (bodyLiteral.sign != Clingo::AST::Sign::None)
|
if (bodyLiteral.sign != Clingo::AST::Sign::None)
|
||||||
throw TranslationException(bodyLiteral.location, "only positive body literals supported currently");
|
throw TranslationException(bodyLiteral.location, "only positive body literals supported currently");
|
||||||
|
|
||||||
return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, context, variableStack);
|
return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, variableStack);
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, Context &, ast::VariableStack &)
|
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &)
|
||||||
{
|
{
|
||||||
throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal");
|
throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal");
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
@ -1,7 +1,7 @@
|
||||||
#ifndef __ANTHEM__CONTEXT_H
|
#ifndef __ANTHEM__CONTEXT_H
|
||||||
#define __ANTHEM__CONTEXT_H
|
#define __ANTHEM__CONTEXT_H
|
||||||
|
|
||||||
#include <optional>
|
#include <experimental/optional>
|
||||||
|
|
||||||
#include <anthem/AST.h>
|
#include <anthem/AST.h>
|
||||||
#include <anthem/output/Logger.h>
|
#include <anthem/output/Logger.h>
|
||||||
|
@ -16,14 +16,6 @@ namespace anthem
|
||||||
//
|
//
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
struct PredicateDeclarationMeta
|
|
||||||
{
|
|
||||||
ast::PredicateDeclaration *declaration;
|
|
||||||
bool used{false};
|
|
||||||
};
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
struct Context
|
struct Context
|
||||||
{
|
{
|
||||||
Context() = default;
|
Context() = default;
|
||||||
|
@ -33,59 +25,12 @@ 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;
|
output::Logger logger;
|
||||||
|
|
||||||
bool performSimplification{false};
|
bool performSimplification = false;
|
||||||
bool performCompletion{false};
|
bool performCompletion = false;
|
||||||
bool performIntegerDetection{false};
|
|
||||||
|
|
||||||
std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations;
|
std::experimental::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
|
||||||
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;
|
ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
|
||||||
};
|
};
|
||||||
|
|
|
@ -1,409 +0,0 @@
|
||||||
#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 don’t 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 ¬_, 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 don’t 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
|
|
|
@ -1,244 +0,0 @@
|
||||||
#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 isn’t, 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 shouldn’t 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 isn’t, set inclusion is never satisfied
|
|
||||||
return EvaluationResult::False;
|
|
||||||
}
|
|
||||||
|
|
||||||
template <class... Arguments>
|
|
||||||
static EvaluationResult visit(const ast::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 ¶meter = 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
|
|
|
@ -2,7 +2,7 @@
|
||||||
#define __ANTHEM__HEAD_H
|
#define __ANTHEM__HEAD_H
|
||||||
|
|
||||||
#include <algorithm>
|
#include <algorithm>
|
||||||
#include <optional>
|
#include <experimental/optional>
|
||||||
|
|
||||||
#include <anthem/AST.h>
|
#include <anthem/AST.h>
|
||||||
#include <anthem/Exception.h>
|
#include <anthem/Exception.h>
|
||||||
|
@ -118,7 +118,8 @@ struct HeadLiteralCollectFunctionTermsVisitor
|
||||||
|
|
||||||
struct FunctionTermTranslateVisitor
|
struct FunctionTermTranslateVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
|
// TODO: check correctness
|
||||||
|
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex)
|
||||||
{
|
{
|
||||||
if (function.external)
|
if (function.external)
|
||||||
throw TranslationException(term.location, "external functions currently unsupported");
|
throw TranslationException(term.location, "external functions currently unsupported");
|
||||||
|
@ -129,17 +130,14 @@ struct FunctionTermTranslateVisitor
|
||||||
for (size_t i = 0; i < function.arguments.size(); i++)
|
for (size_t i = 0; i < function.arguments.size(); i++)
|
||||||
arguments.emplace_back(ast::Variable(ruleContext.freeVariables[headVariableIndex++].get()));
|
arguments.emplace_back(ast::Variable(ruleContext.freeVariables[headVariableIndex++].get()));
|
||||||
|
|
||||||
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size());
|
return ast::Formula::make<ast::Predicate>(function.name, std::move(arguments));
|
||||||
predicateDeclaration->isUsed = true;
|
|
||||||
|
|
||||||
return ast::Predicate(predicateDeclaration, std::move(arguments));
|
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, Context &, size_t &)
|
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &)
|
||||||
{
|
{
|
||||||
throw TranslationException(term.location, "term currently unsupported in this context, function expected");
|
throw TranslationException(term.location, "term currently unsupported in this context, function expected");
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -147,21 +145,21 @@ struct FunctionTermTranslateVisitor
|
||||||
|
|
||||||
struct LiteralTranslateVisitor
|
struct LiteralTranslateVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, size_t &)
|
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &)
|
||||||
{
|
{
|
||||||
return ast::Formula::make<ast::Boolean>(boolean.value);
|
return ast::Formula::make<ast::Boolean>(boolean.value);
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
|
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, size_t &headVariableIndex)
|
||||||
{
|
{
|
||||||
return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, context, headVariableIndex);
|
return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, headVariableIndex);
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, size_t &)
|
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &)
|
||||||
{
|
{
|
||||||
throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals");
|
throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals");
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -169,23 +167,23 @@ struct LiteralTranslateVisitor
|
||||||
|
|
||||||
struct HeadLiteralTranslateToConsequentVisitor
|
struct HeadLiteralTranslateToConsequentVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
|
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex)
|
||||||
{
|
{
|
||||||
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
|
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
|
||||||
throw TranslationException(literal.location, "double-negated head literals currently unsupported");
|
throw TranslationException(literal.location, "double-negated head literals currently unsupported");
|
||||||
|
|
||||||
auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, context, headVariableIndex);
|
auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, headVariableIndex);
|
||||||
|
|
||||||
if (literal.sign == Clingo::AST::Sign::None)
|
if (literal.sign == Clingo::AST::Sign::None)
|
||||||
return translatedLiteral;
|
return translatedLiteral;
|
||||||
|
|
||||||
if (!translatedLiteral)
|
if (!translatedLiteral)
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
|
|
||||||
return ast::Formula::make<ast::Not>(std::move(translatedLiteral.value()));
|
return ast::Formula::make<ast::Not>(std::move(translatedLiteral.value()));
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
|
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
|
||||||
{
|
{
|
||||||
std::vector<ast::Formula> arguments;
|
std::vector<ast::Formula> arguments;
|
||||||
arguments.reserve(disjunction.elements.size());
|
arguments.reserve(disjunction.elements.size());
|
||||||
|
@ -195,7 +193,7 @@ struct HeadLiteralTranslateToConsequentVisitor
|
||||||
if (!conditionalLiteral.condition.empty())
|
if (!conditionalLiteral.condition.empty())
|
||||||
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
|
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
|
||||||
|
|
||||||
auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
|
auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
|
||||||
|
|
||||||
if (!argument)
|
if (!argument)
|
||||||
throw TranslationException(headLiteral.location, "could not parse argument");
|
throw TranslationException(headLiteral.location, "could not parse argument");
|
||||||
|
@ -206,7 +204,7 @@ struct HeadLiteralTranslateToConsequentVisitor
|
||||||
return ast::Formula::make<ast::Or>(std::move(arguments));
|
return ast::Formula::make<ast::Or>(std::move(arguments));
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
|
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
|
||||||
{
|
{
|
||||||
if (aggregate.left_guard || aggregate.right_guard)
|
if (aggregate.left_guard || aggregate.right_guard)
|
||||||
throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported");
|
throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported");
|
||||||
|
@ -217,7 +215,7 @@ struct HeadLiteralTranslateToConsequentVisitor
|
||||||
if (!conditionalLiteral.condition.empty())
|
if (!conditionalLiteral.condition.empty())
|
||||||
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
|
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
|
||||||
|
|
||||||
return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
|
return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
|
||||||
};
|
};
|
||||||
|
|
||||||
if (aggregate.elements.size() == 1)
|
if (aggregate.elements.size() == 1)
|
||||||
|
@ -240,10 +238,10 @@ struct HeadLiteralTranslateToConsequentVisitor
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, Context &, size_t &)
|
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &)
|
||||||
{
|
{
|
||||||
throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate");
|
throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate");
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
@ -13,7 +13,7 @@ namespace anthem
|
||||||
//
|
//
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context);
|
void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context);
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
|
@ -1,22 +0,0 @@
|
||||||
#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
|
|
|
@ -1,193 +0,0 @@
|
||||||
#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 ¬_, 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
|
|
|
@ -73,7 +73,7 @@ struct StatementVisitor
|
||||||
|
|
||||||
// Compute consequent
|
// Compute consequent
|
||||||
auto headVariableIndex = ruleContext.headVariablesStartIndex;
|
auto headVariableIndex = ruleContext.headVariablesStartIndex;
|
||||||
auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, context, headVariableIndex);
|
auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, headVariableIndex);
|
||||||
|
|
||||||
assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex);
|
assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex);
|
||||||
|
|
||||||
|
@ -87,7 +87,7 @@ struct StatementVisitor
|
||||||
|
|
||||||
const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin();
|
const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin();
|
||||||
auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get());
|
auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get());
|
||||||
auto set = translate(headTerm, ruleContext, context, variableStack);
|
auto set = translate(headTerm, ruleContext, variableStack);
|
||||||
auto in = ast::In(std::move(element), std::move(set));
|
auto in = ast::In(std::move(element), std::move(set));
|
||||||
|
|
||||||
antecedent.arguments.emplace_back(std::move(in));
|
antecedent.arguments.emplace_back(std::move(in));
|
||||||
|
@ -98,7 +98,7 @@ struct StatementVisitor
|
||||||
{
|
{
|
||||||
const auto &bodyLiteral = *i;
|
const auto &bodyLiteral = *i;
|
||||||
|
|
||||||
auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, context, variableStack);
|
auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, variableStack);
|
||||||
|
|
||||||
if (!argument)
|
if (!argument)
|
||||||
throw TranslationException(bodyLiteral.location, "could not translate body literal");
|
throw TranslationException(bodyLiteral.location, "could not translate body literal");
|
||||||
|
@ -165,8 +165,8 @@ struct StatementVisitor
|
||||||
if (signature.negative())
|
if (signature.negative())
|
||||||
throw LogicException(statement.location, "negative #show atom signatures are currently unsupported");
|
throw LogicException(statement.location, "negative #show atom signatures are currently unsupported");
|
||||||
|
|
||||||
context.showStatementsUsed = true;
|
if (!context.visiblePredicateSignatures)
|
||||||
context.defaultPredicateVisibility = ast::PredicateDeclaration::Visibility::Hidden;
|
context.visiblePredicateSignatures.emplace();
|
||||||
|
|
||||||
if (std::strlen(signature.name()) == 0)
|
if (std::strlen(signature.name()) == 0)
|
||||||
{
|
{
|
||||||
|
@ -176,8 +176,7 @@ struct StatementVisitor
|
||||||
|
|
||||||
context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”";
|
context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”";
|
||||||
|
|
||||||
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(signature.name(), signature.arity());
|
context.visiblePredicateSignatures.value().emplace_back(std::string(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 &)
|
void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
|
||||||
|
@ -185,84 +184,6 @@ struct StatementVisitor
|
||||||
throw LogicException(statement.location, "only #show statements for atoms (not terms) are supported currently");
|
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>
|
template<class T>
|
||||||
void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
|
void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
|
||||||
{
|
{
|
||||||
|
|
|
@ -23,12 +23,6 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
|
||||||
{
|
{
|
||||||
switch (binaryOperator)
|
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:
|
case Clingo::AST::BinaryOperator::Plus:
|
||||||
return ast::BinaryOperation::Operator::Plus;
|
return ast::BinaryOperation::Operator::Plus;
|
||||||
case Clingo::AST::BinaryOperator::Minus:
|
case Clingo::AST::BinaryOperator::Minus:
|
||||||
|
@ -39,39 +33,22 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
|
||||||
return ast::BinaryOperation::Operator::Division;
|
return ast::BinaryOperation::Operator::Division;
|
||||||
case Clingo::AST::BinaryOperator::Modulo:
|
case Clingo::AST::BinaryOperator::Modulo:
|
||||||
return ast::BinaryOperation::Operator::Modulo;
|
return ast::BinaryOperation::Operator::Modulo;
|
||||||
case Clingo::AST::BinaryOperator::Power:
|
default:
|
||||||
return ast::BinaryOperation::Operator::Power;
|
throw TranslationException(term.location, "“binary operation” terms currently unsupported");
|
||||||
}
|
}
|
||||||
|
|
||||||
throw TranslationException(term.location, "unknown binary operation");
|
return ast::BinaryOperation::Operator::Plus;
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
ast::UnaryOperation::Operator translate(Clingo::AST::UnaryOperator unaryOperator, const Clingo::AST::Term &term)
|
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack);
|
||||||
{
|
|
||||||
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
|
struct TermTranslateVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
std::experimental::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
switch (symbol.type())
|
switch (symbol.type())
|
||||||
{
|
{
|
||||||
|
@ -85,29 +62,29 @@ struct TermTranslateVisitor
|
||||||
return ast::Term::make<ast::String>(std::string(symbol.string()));
|
return ast::Term::make<ast::String>(std::string(symbol.string()));
|
||||||
case Clingo::SymbolType::Function:
|
case Clingo::SymbolType::Function:
|
||||||
{
|
{
|
||||||
auto functionDeclaration = context.findOrCreateFunctionDeclaration(symbol.name(), symbol.arguments().size());
|
auto function = ast::Term::make<ast::Function>(symbol.name());
|
||||||
|
// TODO: remove workaround
|
||||||
auto function = ast::Function(functionDeclaration);
|
auto &functionRaw = function.get<ast::Function>();
|
||||||
function.arguments.reserve(symbol.arguments().size());
|
functionRaw.arguments.reserve(symbol.arguments().size());
|
||||||
|
|
||||||
for (const auto &argument : symbol.arguments())
|
for (const auto &argument : symbol.arguments())
|
||||||
{
|
{
|
||||||
auto translatedArgument = visit(argument, term, ruleContext, context, variableStack);
|
auto translatedArgument = visit(argument, term, ruleContext, variableStack);
|
||||||
|
|
||||||
if (!translatedArgument)
|
if (!translatedArgument)
|
||||||
throw TranslationException(term.location, "could not translate argument");
|
throw TranslationException(term.location, "could not translate argument");
|
||||||
|
|
||||||
function.arguments.emplace_back(std::move(translatedArgument.value()));
|
functionRaw.arguments.emplace_back(std::move(translatedArgument.value()));
|
||||||
}
|
}
|
||||||
|
|
||||||
return std::move(function);
|
return std::move(function);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, Context &, const ast::VariableStack &variableStack)
|
std::experimental::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name);
|
const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name);
|
||||||
const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0);
|
const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0);
|
||||||
|
@ -120,36 +97,33 @@ struct TermTranslateVisitor
|
||||||
auto variableDeclaration = std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::UserDefined, std::string(variable.name));
|
auto variableDeclaration = std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::UserDefined, std::string(variable.name));
|
||||||
ruleContext.freeVariables.emplace_back(std::move(variableDeclaration));
|
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());
|
return ast::Term::make<ast::Variable>(ruleContext.freeVariables.back().get());
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
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)
|
||||||
{
|
{
|
||||||
const auto operator_ = translate(binaryOperation.binary_operator, term);
|
const auto operator_ = translate(binaryOperation.binary_operator, term);
|
||||||
auto left = translate(binaryOperation.left, ruleContext, context, variableStack);
|
auto left = translate(binaryOperation.left, ruleContext, variableStack);
|
||||||
auto right = translate(binaryOperation.right, ruleContext, context, variableStack);
|
auto right = translate(binaryOperation.right, ruleContext, variableStack);
|
||||||
|
|
||||||
return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
|
return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
std::experimental::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
const auto operator_ = translate(unaryOperation.unary_operator, term);
|
auto left = translate(interval.left, ruleContext, variableStack);
|
||||||
auto argument = translate(unaryOperation.argument, ruleContext, context, variableStack);
|
auto right = translate(interval.right, ruleContext, 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));
|
return ast::Term::make<ast::Interval>(std::move(left), std::move(right));
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
std::experimental::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
if (function.external)
|
if (function.external)
|
||||||
throw TranslationException(term.location, "external functions currently unsupported");
|
throw TranslationException(term.location, "external functions currently unsupported");
|
||||||
|
@ -158,25 +132,23 @@ struct TermTranslateVisitor
|
||||||
arguments.reserve(function.arguments.size());
|
arguments.reserve(function.arguments.size());
|
||||||
|
|
||||||
for (const auto &argument : function.arguments)
|
for (const auto &argument : function.arguments)
|
||||||
arguments.emplace_back(translate(argument, ruleContext, context, variableStack));
|
arguments.emplace_back(translate(argument, ruleContext, variableStack));
|
||||||
|
|
||||||
auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, function.arguments.size());
|
return ast::Term::make<ast::Function>(function.name, std::move(arguments));
|
||||||
|
|
||||||
return ast::Term::make<ast::Function>(functionDeclaration, std::move(arguments));
|
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, Context &, const ast::VariableStack &)
|
std::experimental::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
|
||||||
{
|
{
|
||||||
throw TranslationException(term.location, "“pool” terms currently unsupported");
|
throw TranslationException(term.location, "“pool” terms currently unsupported");
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, context, variableStack);
|
auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, variableStack);
|
||||||
|
|
||||||
if (!translatedTerm)
|
if (!translatedTerm)
|
||||||
throw TranslationException(term.location, "could not translate term");
|
throw TranslationException(term.location, "could not translate term");
|
||||||
|
|
|
@ -1,157 +0,0 @@
|
||||||
#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
|
|
|
@ -1,6 +1,13 @@
|
||||||
#ifndef __ANTHEM__UTILS_H
|
#ifndef __ANTHEM__UTILS_H
|
||||||
#define __ANTHEM__UTILS_H
|
#define __ANTHEM__UTILS_H
|
||||||
|
|
||||||
|
#include <iostream>
|
||||||
|
|
||||||
|
#include <clingo.hh>
|
||||||
|
|
||||||
|
#include <anthem/Context.h>
|
||||||
|
#include <anthem/Location.h>
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
|
|
||||||
|
@ -13,61 +20,6 @@ namespace anthem
|
||||||
constexpr const auto HeadVariablePrefix = "V";
|
constexpr const auto HeadVariablePrefix = "V";
|
||||||
constexpr const auto BodyVariablePrefix = "X";
|
constexpr const auto BodyVariablePrefix = "X";
|
||||||
constexpr const auto UserVariablePrefix = "U";
|
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};
|
|
||||||
};
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
|
@ -35,46 +35,43 @@ struct PrintContext
|
||||||
std::map<const VariableDeclaration *, size_t> userVariableIDs;
|
std::map<const VariableDeclaration *, size_t> userVariableIDs;
|
||||||
std::map<const VariableDeclaration *, size_t> headVariableIDs;
|
std::map<const VariableDeclaration *, size_t> headVariableIDs;
|
||||||
std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
|
std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
|
||||||
std::map<const VariableDeclaration *, size_t> integerVariableIDs;
|
|
||||||
|
|
||||||
const Context &context;
|
const Context &context;
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext);
|
||||||
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);
|
||||||
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);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext);
|
||||||
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, 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, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Not ¬_, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Not ¬_, PrintContext &printContext);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext);
|
||||||
|
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Formula &formula, 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, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext);
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
// Primitives
|
// Primitives
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &)
|
||||||
{
|
{
|
||||||
switch (operator_)
|
switch (operator_)
|
||||||
{
|
{
|
||||||
|
@ -88,8 +85,6 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::
|
||||||
return (stream << output::Operator("/"));
|
return (stream << output::Operator("/"));
|
||||||
case BinaryOperation::Operator::Modulo:
|
case BinaryOperation::Operator::Modulo:
|
||||||
return (stream << output::Operator("%"));
|
return (stream << output::Operator("%"));
|
||||||
case BinaryOperation::Operator::Power:
|
|
||||||
return (stream << output::Operator("**"));
|
|
||||||
}
|
}
|
||||||
|
|
||||||
return stream;
|
return stream;
|
||||||
|
@ -97,26 +92,22 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses)
|
inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
stream << "(";
|
||||||
stream << "(";
|
|
||||||
|
|
||||||
print(stream, binaryOperation.left, printContext);
|
print(stream, binaryOperation.left, printContext);
|
||||||
stream << " ";
|
stream << " ";
|
||||||
print(stream, binaryOperation.operator_, printContext);
|
print(stream, binaryOperation.operator_, printContext);
|
||||||
stream << " ";
|
stream << " ";
|
||||||
print(stream, binaryOperation.right, printContext);
|
print(stream, binaryOperation.right, printContext);
|
||||||
|
stream << ")";
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
|
||||||
stream << ")";
|
|
||||||
|
|
||||||
return stream;
|
return stream;
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &)
|
||||||
{
|
{
|
||||||
if (boolean.value)
|
if (boolean.value)
|
||||||
return (stream << output::Boolean("#true"));
|
return (stream << output::Boolean("#true"));
|
||||||
|
@ -126,7 +117,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Boolean &bo
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &)
|
||||||
{
|
{
|
||||||
switch (operator_)
|
switch (operator_)
|
||||||
{
|
{
|
||||||
|
@ -149,7 +140,7 @@ inline output::ColorStream &print(output::ColorStream &stream, Comparison::Opera
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
||||||
stream << "(";
|
stream << "(";
|
||||||
|
@ -168,9 +159,16 @@ inline output::ColorStream &print(output::ColorStream &stream, const Comparison
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &)
|
||||||
{
|
{
|
||||||
stream << function.declaration->name;
|
return (stream << constant.name);
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext)
|
||||||
|
{
|
||||||
|
stream << function.name;
|
||||||
|
|
||||||
if (function.arguments.empty())
|
if (function.arguments.empty())
|
||||||
return stream;
|
return stream;
|
||||||
|
@ -185,7 +183,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
|
||||||
print(stream, *i, printContext);
|
print(stream, *i, printContext);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (function.declaration->name.empty() && function.arguments.size() == 1)
|
if (function.name.empty() && function.arguments.size() == 1)
|
||||||
stream << ",";
|
stream << ",";
|
||||||
|
|
||||||
stream << ")";
|
stream << ")";
|
||||||
|
@ -195,7 +193,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
||||||
stream << "(";
|
stream << "(";
|
||||||
|
@ -212,23 +210,23 @@ inline output::ColorStream &print(output::ColorStream &stream, const In &in, Pri
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &)
|
||||||
{
|
{
|
||||||
return (stream << output::Number<int>(integer.value));
|
return (stream << output::Number<int>(integer.value));
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses)
|
inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
||||||
stream << "(";
|
stream << "(";
|
||||||
|
|
||||||
print(stream, interval.from, printContext);
|
print(stream, interval.from, printContext);
|
||||||
stream << "..";
|
stream << "..";
|
||||||
print(stream, interval.to, printContext);
|
print(stream, interval.to, printContext);
|
||||||
|
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
||||||
stream << ")";
|
stream << ")";
|
||||||
|
|
||||||
return stream;
|
return stream;
|
||||||
|
@ -236,9 +234,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Interval &i
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
stream << predicate.declaration->name;
|
stream << predicate.name;
|
||||||
|
|
||||||
if (predicate.arguments.empty())
|
if (predicate.arguments.empty())
|
||||||
return stream;
|
return stream;
|
||||||
|
@ -260,14 +258,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Predicate &
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &)
|
||||||
{
|
|
||||||
return (stream << predicateDeclaration.name << "/" << predicateDeclaration.arity());
|
|
||||||
}
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &, bool)
|
|
||||||
{
|
{
|
||||||
switch (specialInteger.type)
|
switch (specialInteger.type)
|
||||||
{
|
{
|
||||||
|
@ -282,37 +273,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const SpecialInte
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &)
|
||||||
{
|
{
|
||||||
return (stream << output::String(string.text.c_str()));
|
return (stream << output::String(string.text.c_str()));
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext)
|
||||||
{
|
|
||||||
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);
|
assert(variable.declaration != nullptr);
|
||||||
|
|
||||||
|
@ -321,7 +289,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Variable &v
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
const auto printVariableDeclaration =
|
const auto printVariableDeclaration =
|
||||||
[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
|
[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
|
||||||
|
@ -340,9 +308,6 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
|
||||||
return (stream << output::Variable(variableName.c_str()));
|
return (stream << output::Variable(variableName.c_str()));
|
||||||
};
|
};
|
||||||
|
|
||||||
if (variableDeclaration.domain == Domain::Integer)
|
|
||||||
return printVariableDeclaration(IntegerVariablePrefix, printContext.integerVariableIDs);
|
|
||||||
|
|
||||||
switch (variableDeclaration.type)
|
switch (variableDeclaration.type)
|
||||||
{
|
{
|
||||||
case VariableDeclaration::Type::UserDefined:
|
case VariableDeclaration::Type::UserDefined:
|
||||||
|
@ -360,10 +325,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
|
||||||
// Expressions
|
// Expressions
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses)
|
inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
stream << "(";
|
||||||
stream << "(";
|
|
||||||
|
|
||||||
for (auto i = and_.arguments.cbegin(); i != and_.arguments.cend(); i++)
|
for (auto i = and_.arguments.cbegin(); i != and_.arguments.cend(); i++)
|
||||||
{
|
{
|
||||||
|
@ -373,32 +337,27 @@ inline output::ColorStream &print(output::ColorStream &stream, const And &and_,
|
||||||
print(stream, *i, printContext);
|
print(stream, *i, printContext);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
stream << ")";
|
||||||
stream << ")";
|
|
||||||
|
|
||||||
return stream;
|
return stream;
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses)
|
inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
stream << "(";
|
||||||
stream << "(";
|
|
||||||
|
|
||||||
print(stream, biconditional.left, printContext);
|
print(stream, biconditional.left, printContext);
|
||||||
stream << " <-> ";
|
stream << " <-> ";
|
||||||
print(stream, biconditional.right, printContext);
|
print(stream, biconditional.right, printContext);
|
||||||
|
stream << ")";
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
|
||||||
stream << ")";
|
|
||||||
|
|
||||||
return stream;
|
return stream;
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
||||||
stream << "(";
|
stream << "(";
|
||||||
|
@ -424,7 +383,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Exists &exi
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
||||||
stream << "(";
|
stream << "(";
|
||||||
|
@ -450,24 +409,20 @@ inline output::ColorStream &print(output::ColorStream &stream, const ForAll &for
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses)
|
inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
stream << "(";
|
||||||
stream << "(";
|
|
||||||
|
|
||||||
print(stream, implies.antecedent, printContext);
|
print(stream, implies.antecedent, printContext);
|
||||||
stream << " -> ";
|
stream << " -> ";
|
||||||
print(stream, implies.consequent, printContext);
|
print(stream, implies.consequent, printContext);
|
||||||
|
stream << ")";
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
|
||||||
stream << ")";
|
|
||||||
|
|
||||||
return stream;
|
return stream;
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Not ¬_, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const Not ¬_, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
||||||
stream << "(";
|
stream << "(";
|
||||||
|
@ -483,10 +438,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Not ¬_,
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses)
|
inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
stream << "(";
|
||||||
stream << "(";
|
|
||||||
|
|
||||||
for (auto i = or_.arguments.cbegin(); i != or_.arguments.cend(); i++)
|
for (auto i = or_.arguments.cbegin(); i != or_.arguments.cend(); i++)
|
||||||
{
|
{
|
||||||
|
@ -496,8 +450,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, Pr
|
||||||
print(stream, *i, printContext);
|
print(stream, *i, printContext);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
stream << ")";
|
||||||
stream << ")";
|
|
||||||
|
|
||||||
return stream;
|
return stream;
|
||||||
}
|
}
|
||||||
|
@ -510,24 +463,24 @@ template<class Variant>
|
||||||
struct VariantPrintVisitor
|
struct VariantPrintVisitor
|
||||||
{
|
{
|
||||||
template<class T>
|
template<class T>
|
||||||
output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext, bool omitParentheses)
|
output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
return print(stream, x, printContext, omitParentheses);
|
return print(stream, x, printContext);
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext, bool omitParentheses)
|
inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext, omitParentheses);
|
return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext);
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext, bool omitParentheses)
|
inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
return term.accept(VariantPrintVisitor<Term>(), stream, printContext, omitParentheses);
|
return term.accept(VariantPrintVisitor<Term>(), stream, printContext);
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
@ -1 +1 @@
|
||||||
Subproject commit d2d8455b571b6c66c4b7003500a77f9a93ecdc28
|
Subproject commit 017a63da62ba7ffce1e1b005e6adc846412c575b
|
|
@ -1 +1 @@
|
||||||
Subproject commit 969ce8f618c4cdf78d5c430ba827217075b88460
|
Subproject commit cc83b3b231ae9626ff5402a5424b0e9e6b4aa180
|
|
@ -1 +0,0 @@
|
||||||
Subproject commit ca6e9f70eb6b5fab44504daf57d92a9412ab301c
|
|
|
@ -103,9 +103,16 @@ Comparison prepareCopy(const Comparison &other)
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
Constant prepareCopy(const Constant &other)
|
||||||
|
{
|
||||||
|
return Constant(std::string(other.name));
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
Function prepareCopy(const Function &other)
|
Function prepareCopy(const Function &other)
|
||||||
{
|
{
|
||||||
return Function(other.declaration, prepareCopy(other.arguments));
|
return Function(std::string(other.name), prepareCopy(other.arguments));
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
@ -133,7 +140,7 @@ Interval prepareCopy(const Interval &other)
|
||||||
|
|
||||||
Predicate prepareCopy(const Predicate &other)
|
Predicate prepareCopy(const Predicate &other)
|
||||||
{
|
{
|
||||||
return Predicate(other.declaration, prepareCopy(other.arguments));
|
return Predicate(std::string(other.name), prepareCopy(other.arguments));
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
@ -152,13 +159,6 @@ String prepareCopy(const String &other)
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
UnaryOperation prepareCopy(const UnaryOperation &other)
|
|
||||||
{
|
|
||||||
return UnaryOperation(other.operator_, prepareCopy(other.argument));
|
|
||||||
}
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
Variable prepareCopy(const Variable &other)
|
Variable prepareCopy(const Variable &other)
|
||||||
{
|
{
|
||||||
return Variable(other.declaration);
|
return Variable(other.declaration);
|
||||||
|
@ -286,6 +286,11 @@ struct FixDanglingVariablesInTermVisitor
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
template <class... Arguments>
|
||||||
|
void visit(Constant &, Arguments &&...)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
void visit(Function &function, Arguments &&... arguments)
|
void visit(Function &function, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
|
@ -315,12 +320,6 @@ 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,
|
void visit(Variable &variable, ScopedFormula &scopedFormula, VariableStack &variableStack,
|
||||||
std::map<VariableDeclaration *, VariableDeclaration *> &replacements)
|
std::map<VariableDeclaration *, VariableDeclaration *> &replacements)
|
||||||
{
|
{
|
||||||
|
|
|
@ -27,7 +27,7 @@ void VariableStack::pop()
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
std::optional<VariableDeclaration *> VariableStack::findUserVariableDeclaration(const char *variableName) const
|
std::experimental::optional<VariableDeclaration *> VariableStack::findUserVariableDeclaration(const char *variableName) const
|
||||||
{
|
{
|
||||||
const auto variableDeclarationMatches =
|
const auto variableDeclarationMatches =
|
||||||
[&variableName](const auto &variableDeclaration)
|
[&variableName](const auto &variableDeclaration)
|
||||||
|
@ -45,7 +45,7 @@ std::optional<VariableDeclaration *> VariableStack::findUserVariableDeclaration(
|
||||||
return matchingVariableDeclaration->get();
|
return matchingVariableDeclaration->get();
|
||||||
}
|
}
|
||||||
|
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
@ -59,7 +59,7 @@ bool VariableStack::contains(const VariableDeclaration &variableDeclaration) con
|
||||||
};
|
};
|
||||||
|
|
||||||
const auto layerContainsVariableDeclaration =
|
const auto layerContainsVariableDeclaration =
|
||||||
[&variableDeclarationMatches](const auto &layer)
|
[&variableDeclaration, &variableDeclarationMatches](const auto &layer)
|
||||||
{
|
{
|
||||||
return (std::find_if(layer->cbegin(), layer->cend(), variableDeclarationMatches) != layer->cend());
|
return (std::find_if(layer->cbegin(), layer->cend(), variableDeclarationMatches) != layer->cend());
|
||||||
};
|
};
|
||||||
|
@ -150,6 +150,10 @@ struct CollectFreeVariablesVisitor
|
||||||
binaryOperation.right.accept(*this, variableStack, freeVariables);
|
binaryOperation.right.accept(*this, variableStack, freeVariables);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void visit(Constant &, VariableStack &, std::vector<VariableDeclaration *> &)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
void visit(Function &function, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
|
void visit(Function &function, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
|
||||||
{
|
{
|
||||||
for (auto &argument : function.arguments)
|
for (auto &argument : function.arguments)
|
||||||
|
@ -174,11 +178,6 @@ 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)
|
void visit(Variable &variable, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
|
||||||
{
|
{
|
||||||
if (variableStack.contains(*variable.declaration))
|
if (variableStack.contains(*variable.declaration))
|
||||||
|
@ -193,5 +192,61 @@ 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);
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -35,41 +35,13 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
|
||||||
|
|
||||||
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
|
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
|
||||||
|
|
||||||
if (predicate.declaration != otherPredicate.declaration)
|
if (!ast::matches(predicate, otherPredicate))
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
assert(otherPredicate.arguments.size() == parameters.size());
|
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 predicate’s parameters
|
// Each formula with the predicate as its consequent currently has its own copy of the predicate’s parameters
|
||||||
// These need to be linked to the new, unique set of 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++)
|
for (size_t i = 0; i < parameters.size(); i++)
|
||||||
{
|
{
|
||||||
assert(otherPredicate.arguments[i].is<ast::Variable>());
|
assert(otherPredicate.arguments[i].is<ast::Variable>());
|
||||||
|
@ -78,6 +50,16 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
|
||||||
scopedFormula.formula.accept(ast::ReplaceVariableInFormulaVisitor(), scopedFormula.formula, otherVariable.declaration, parameters[i].get());
|
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())
|
if (freeVariables.empty())
|
||||||
disjunction.get<ast::Or>().arguments.emplace_back(std::move(implies.antecedent));
|
disjunction.get<ast::Or>().arguments.emplace_back(std::move(implies.antecedent));
|
||||||
else
|
else
|
||||||
|
@ -118,22 +100,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
ast::Formula completePredicate(ast::PredicateDeclaration &predicateDeclaration, std::vector<ast::ScopedFormula> &scopedFormulas)
|
ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector<ast::ScopedFormula> &scopedFormulas)
|
||||||
{
|
{
|
||||||
// Create new set of parameters for the completed definition for the predicate
|
// Create new set of parameters for the completed definition for the predicate
|
||||||
ast::VariableDeclarationPointers parameters;
|
ast::VariableDeclarationPointers parameters;
|
||||||
parameters.reserve(predicateDeclaration.arity());
|
parameters.reserve(predicateSignature.arity);
|
||||||
|
|
||||||
std::vector<ast::Term> arguments;
|
std::vector<ast::Term> arguments;
|
||||||
arguments.reserve(predicateDeclaration.arity());
|
arguments.reserve(predicateSignature.arity);
|
||||||
|
|
||||||
for (size_t i = 0; i < predicateDeclaration.arity(); i++)
|
for (size_t i = 0; i < predicateSignature.arity; i++)
|
||||||
{
|
{
|
||||||
parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Head));
|
parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Head));
|
||||||
arguments.emplace_back(ast::Term::make<ast::Variable>(parameters.back().get()));
|
arguments.emplace_back(ast::Term::make<ast::Variable>(parameters.back().get()));
|
||||||
}
|
}
|
||||||
|
|
||||||
ast::Predicate predicateCopy(&predicateDeclaration, std::move(arguments));
|
ast::Predicate predicateCopy(std::string(predicateSignature.name), std::move(arguments));
|
||||||
|
|
||||||
auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
|
auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
|
||||||
auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
|
auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
|
||||||
|
@ -179,27 +161,28 @@ 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");
|
throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
|
||||||
}
|
}
|
||||||
|
|
||||||
std::sort(context.predicateDeclarations.begin(), context.predicateDeclarations.end(),
|
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(),
|
||||||
[](const auto &lhs, const auto &rhs)
|
[](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)
|
if (order != 0)
|
||||||
return (order < 0);
|
return (order < 0);
|
||||||
|
|
||||||
return lhs->arity() < rhs->arity();
|
return lhs.arity < rhs.arity;
|
||||||
});
|
});
|
||||||
|
|
||||||
std::vector<ast::Formula> completedFormulas;
|
std::vector<ast::Formula> completedFormulas;
|
||||||
|
|
||||||
// Complete predicates
|
// Complete predicates
|
||||||
for (auto &predicateDeclaration : context.predicateDeclarations)
|
for (const auto &predicateSignature : predicateSignatures)
|
||||||
{
|
completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
|
||||||
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
completedFormulas.emplace_back(completePredicate(*predicateDeclaration, scopedFormulas));
|
|
||||||
}
|
|
||||||
|
|
||||||
// Complete integrity constraints
|
// Complete integrity constraints
|
||||||
for (auto &scopedFormula : scopedFormulas)
|
for (auto &scopedFormula : scopedFormulas)
|
||||||
|
@ -219,7 +202,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
|
||||||
}
|
}
|
||||||
|
|
||||||
// Eliminate all predicates that should not be visible in the output
|
// Eliminate all predicates that should not be visible in the output
|
||||||
eliminateHiddenPredicates(completedFormulas, context);
|
eliminateHiddenPredicates(predicateSignatures, completedFormulas, context);
|
||||||
|
|
||||||
return completedFormulas;
|
return completedFormulas;
|
||||||
}
|
}
|
||||||
|
|
|
@ -78,7 +78,7 @@ struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor<Re
|
||||||
{
|
{
|
||||||
static void accept(ast::Predicate &predicate, ast::Formula &formula, const PredicateReplacement &predicateReplacement)
|
static void accept(ast::Predicate &predicate, ast::Formula &formula, const PredicateReplacement &predicateReplacement)
|
||||||
{
|
{
|
||||||
if (predicate.declaration != predicateReplacement.predicate.declaration)
|
if (!ast::matches(predicate, predicateReplacement.predicate))
|
||||||
return;
|
return;
|
||||||
|
|
||||||
auto formulaReplacement = ast::prepareCopy(predicateReplacement.replacement);
|
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
|
// Detect whether a formula contains a circular dependency on a given predicate
|
||||||
struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<DetectCircularDependcyVisitor>
|
struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<DetectCircularDependcyVisitor>
|
||||||
{
|
{
|
||||||
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateDeclaration &predicateDeclaration, bool &hasCircularDependency)
|
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateSignature &predicateSignature, bool &hasCircularDependency)
|
||||||
{
|
{
|
||||||
if (predicate.declaration == &predicateDeclaration)
|
if (ast::matches(predicate, predicateSignature))
|
||||||
hasCircularDependency = true;
|
hasCircularDependency = true;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Ignore all other types of expressions
|
// Ignore all other types of expressions
|
||||||
template<class T>
|
template<class T>
|
||||||
static void accept(T &, ast::Formula &, const ast::PredicateDeclaration &, bool &)
|
static void accept(T &, ast::Formula &, const ast::PredicateSignature &, 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)”
|
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> q(X1, ..., Xn)”
|
||||||
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Predicate &predicate)
|
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Predicate &predicate)
|
||||||
{
|
{
|
||||||
// Declare variable used, only used in debug mode
|
// Declare variable used, only used in debug mode
|
||||||
(void)(predicateDeclaration);
|
(void)(predicateSignature);
|
||||||
|
|
||||||
assert(predicate.declaration == &predicateDeclaration);
|
assert(ast::matches(predicate, predicateSignature));
|
||||||
|
|
||||||
// Replace with “#true”
|
// Replace with “#true”
|
||||||
return {predicate, ast::Formula::make<ast::Boolean>(true)};
|
return {predicate, ast::Formula::make<ast::Boolean>(true)};
|
||||||
|
@ -139,13 +139,13 @@ PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateD
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> not q(X1, ..., Xn)”
|
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> not q(X1, ..., Xn)”
|
||||||
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Not ¬_)
|
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Not ¬_)
|
||||||
{
|
{
|
||||||
// Declare variable used, only used in debug mode
|
// Declare variable used, only used in debug mode
|
||||||
(void)(predicateDeclaration);
|
(void)(predicateSignature);
|
||||||
|
|
||||||
assert(not_.argument.is<ast::Predicate>());
|
assert(not_.argument.is<ast::Predicate>());
|
||||||
assert(not_.argument.get<ast::Predicate>().declaration == &predicateDeclaration);
|
assert(ast::matches(not_.argument.get<ast::Predicate>(), predicateSignature));
|
||||||
|
|
||||||
// Replace with “#false”
|
// Replace with “#false”
|
||||||
return {not_.argument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(false)};
|
return {not_.argument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(false)};
|
||||||
|
@ -154,13 +154,13 @@ PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateD
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)”
|
// Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)”
|
||||||
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Biconditional &biconditional)
|
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Biconditional &biconditional)
|
||||||
{
|
{
|
||||||
// Declare variable used, only used in debug mode
|
// Declare variable used, only used in debug mode
|
||||||
(void)(predicateDeclaration);
|
(void)(predicateSignature);
|
||||||
|
|
||||||
assert(biconditional.left.is<ast::Predicate>());
|
assert(biconditional.left.is<ast::Predicate>());
|
||||||
assert(biconditional.left.get<ast::Predicate>().declaration == &predicateDeclaration);
|
assert(ast::matches(biconditional.left.get<ast::Predicate>(), predicateSignature));
|
||||||
|
|
||||||
// TODO: avoid copy
|
// TODO: avoid copy
|
||||||
return {biconditional.left.get<ast::Predicate>(), ast::prepareCopy(biconditional.right)};
|
return {biconditional.left.get<ast::Predicate>(), ast::prepareCopy(biconditional.right)};
|
||||||
|
@ -169,65 +169,78 @@ PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateD
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// Finds a replacement for a predicate that should be hidden
|
// Finds a replacement for a predicate that should be hidden
|
||||||
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Formula &completedPredicateDefinition)
|
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Formula &completedPredicateDefinition)
|
||||||
{
|
{
|
||||||
// TODO: refactor
|
// TODO: refactor
|
||||||
if (completedPredicateDefinition.is<ast::ForAll>())
|
if (completedPredicateDefinition.is<ast::ForAll>())
|
||||||
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::ForAll>().argument);
|
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::ForAll>().argument);
|
||||||
else if (completedPredicateDefinition.is<ast::Biconditional>())
|
else if (completedPredicateDefinition.is<ast::Biconditional>())
|
||||||
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Biconditional>());
|
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Biconditional>());
|
||||||
else if (completedPredicateDefinition.is<ast::Predicate>())
|
else if (completedPredicateDefinition.is<ast::Predicate>())
|
||||||
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Predicate>());
|
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Predicate>());
|
||||||
else if (completedPredicateDefinition.is<ast::Not>())
|
else if (completedPredicateDefinition.is<ast::Not>())
|
||||||
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Not>());
|
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Not>());
|
||||||
|
|
||||||
throw CompletionException("unsupported completed definition for predicate “" + predicateDeclaration.name + "/" + std::to_string(predicateDeclaration.arity()) + "” for hiding predicates");
|
throw CompletionException("unsupported completed definition for predicate “" + predicateSignature.name + "/" + std::to_string(predicateSignature.arity) + "” for hiding predicates");
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context)
|
void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context)
|
||||||
{
|
{
|
||||||
if (context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible)
|
if (!context.visiblePredicateSignatures)
|
||||||
{
|
{
|
||||||
context.logger.log(output::Priority::Debug) << "no predicates to be eliminated";
|
context.logger.log(output::Priority::Debug) << "no predicates to be eliminated";
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
assert(context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Hidden);
|
const auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
|
||||||
|
|
||||||
// TODO: get rid of index-wise matching of completed formulas and predicate declarations
|
// Check for undeclared predicates that are requested to be shown
|
||||||
size_t i = -1;
|
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 <<"”";
|
||||||
|
}
|
||||||
|
|
||||||
// Replace all occurrences of hidden predicates
|
// Replace all occurrences of hidden predicates
|
||||||
for (auto &predicateDeclaration : context.predicateDeclarations)
|
for (size_t i = 0; i < predicateSignatures.size(); i++)
|
||||||
{
|
{
|
||||||
// Check that the predicate is used and not declared #external
|
auto &predicateSignature = predicateSignatures[i];
|
||||||
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
i++;
|
const auto matchesVisiblePredicateSignature =
|
||||||
|
[&](const auto &visiblePredicateSignature)
|
||||||
|
{
|
||||||
|
return ast::matches(predicateSignature, visiblePredicateSignature);
|
||||||
|
};
|
||||||
|
|
||||||
const auto isPredicateVisible =
|
const auto matchingPredicateSignature =
|
||||||
(predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Visible)
|
std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesVisiblePredicateSignature);
|
||||||
|| (predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Default
|
|
||||||
&& context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible);
|
|
||||||
|
|
||||||
// If the predicate ought to be visible, don’t eliminate it
|
// If the predicate ought to be visible, don’t eliminate it
|
||||||
if (isPredicateVisible)
|
if (matchingPredicateSignature != visiblePredicateSignatures.cend())
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
context.logger.log(output::Priority::Debug) << "eliminating “" << predicateDeclaration->name << "/" << predicateDeclaration->arity() << "”";
|
context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "”";
|
||||||
|
|
||||||
const auto &completedPredicateDefinition = completedFormulas[i];
|
const auto &completedPredicateDefinition = completedFormulas[i];
|
||||||
auto replacement = findReplacement(*predicateDeclaration, completedPredicateDefinition);
|
auto replacement = findReplacement(predicateSignature, completedPredicateDefinition);
|
||||||
|
|
||||||
bool hasCircularDependency = false;
|
bool hasCircularDependency = false;
|
||||||
replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, *predicateDeclaration, hasCircularDependency);
|
replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, predicateSignature, hasCircularDependency);
|
||||||
|
|
||||||
if (hasCircularDependency)
|
if (hasCircularDependency)
|
||||||
{
|
{
|
||||||
context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateDeclaration->name << "/" << predicateDeclaration->arity() << "” due to circular dependency";
|
context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateSignature.name << "/" << predicateSignature.arity << "” due to circular dependency";
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -1,332 +0,0 @@
|
||||||
#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 ¬_, 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 parameter’s 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, it’s 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 parameter’s 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, it’s 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 parameter’s 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, it’s 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 ¶meter = predicate.declaration->parameters[i];
|
|
||||||
|
|
||||||
assert(variableArgument.is<ast::Variable>());
|
|
||||||
|
|
||||||
auto &variable = variableArgument.get<ast::Variable>();
|
|
||||||
|
|
||||||
parameter.domain = variable.declaration->domain;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
}
|
|
|
@ -1,12 +1,9 @@
|
||||||
#include <anthem/Simplification.h>
|
#include <anthem/Simplification.h>
|
||||||
|
|
||||||
#include <optional>
|
#include <experimental/optional>
|
||||||
|
|
||||||
#include <anthem/ASTCopy.h>
|
#include <anthem/ASTCopy.h>
|
||||||
#include <anthem/Equality.h>
|
#include <anthem/ASTVisitors.h>
|
||||||
#include <anthem/SimplificationVisitors.h>
|
|
||||||
#include <anthem/Type.h>
|
|
||||||
#include <anthem/output/AST.h>
|
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
|
@ -30,15 +27,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
|
// 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
|
// The input formula is no longer usable after this call if a term is returned
|
||||||
std::optional<ast::Term> extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration)
|
std::experimental::optional<ast::Term> extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Comparison>())
|
if (!formula.is<ast::Comparison>())
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
|
|
||||||
auto &comparison = formula.get<ast::Comparison>();
|
auto &comparison = formula.get<ast::Comparison>();
|
||||||
|
|
||||||
if (comparison.operator_ != ast::Comparison::Operator::Equal)
|
if (comparison.operator_ != ast::Comparison::Operator::Equal)
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
|
|
||||||
if (matchesVariableDeclaration(comparison.left, variableDeclaration))
|
if (matchesVariableDeclaration(comparison.left, variableDeclaration))
|
||||||
return std::move(comparison.right);
|
return std::move(comparison.right);
|
||||||
|
@ -46,7 +43,7 @@ std::optional<ast::Term> extractAssignedTerm(ast::Formula &formula, const ast::V
|
||||||
if (matchesVariableDeclaration(comparison.right, variableDeclaration))
|
if (matchesVariableDeclaration(comparison.right, variableDeclaration))
|
||||||
return std::move(comparison.left);
|
return std::move(comparison.left);
|
||||||
|
|
||||||
return std::nullopt;
|
return std::experimental::nullopt;
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
@ -100,65 +97,18 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
template<class SimplificationRule>
|
// Simplifies exists statements by using the equivalence “exists X (X = t and F(X))” == “F(t)”
|
||||||
OperationResult simplify(ast::Formula &formula)
|
// The exists statement has to be of the form “exists <variables> <conjunction>”
|
||||||
|
void simplify(ast::Exists &exists, ast::Formula &formula)
|
||||||
{
|
{
|
||||||
return SimplificationRule::apply(formula);
|
// Simplify formulas like “exists X (X = Y)” to “#true”
|
||||||
}
|
// TODO: check that this covers all cases
|
||||||
|
if (exists.argument.is<ast::Comparison>())
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
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>();
|
const auto &comparison = exists.argument.get<ast::Comparison>();
|
||||||
|
|
||||||
if (comparison.operator_ != ast::Comparison::Operator::Equal)
|
if (comparison.operator_ != ast::Comparison::Operator::Equal)
|
||||||
return OperationResult::Unchanged;
|
return;
|
||||||
|
|
||||||
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
|
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
|
||||||
[&](const auto &variableDeclaration)
|
[&](const auto &variableDeclaration)
|
||||||
|
@ -167,407 +117,107 @@ struct SimplificationRuleTrivialAssignmentInExists
|
||||||
|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
|
|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
|
||||||
});
|
});
|
||||||
|
|
||||||
if (matchingAssignment == exists.variables.cend())
|
if (matchingAssignment != exists.variables.cend())
|
||||||
return OperationResult::Unchanged;
|
formula = ast::Formula::make<ast::Boolean>(true);
|
||||||
|
|
||||||
formula = ast::Formula::make<ast::Boolean>(true);
|
return;
|
||||||
|
|
||||||
return OperationResult::Changed;
|
|
||||||
}
|
}
|
||||||
};
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
if (!exists.argument.is<ast::And>())
|
||||||
|
return;
|
||||||
|
|
||||||
struct SimplificationRuleAssignmentInExists
|
auto &conjunction = exists.argument.get<ast::And>();
|
||||||
{
|
auto &arguments = conjunction.arguments;
|
||||||
static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
|
|
||||||
|
|
||||||
static OperationResult apply(ast::Formula &formula)
|
// Simplify formulas of type “exists X (X = t and F(X))” to “F(t)”
|
||||||
|
for (auto i = exists.variables.begin(); i != exists.variables.end();)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Exists>())
|
const auto &variableDeclaration = **i;
|
||||||
return OperationResult::Unchanged;
|
|
||||||
|
|
||||||
auto &exists = formula.get<ast::Exists>();
|
bool wasVariableReplaced = false;
|
||||||
|
|
||||||
if (!exists.argument.is<ast::And>())
|
// TODO: refactor
|
||||||
return OperationResult::Unchanged;
|
for (auto j = arguments.begin(); j != arguments.end(); j++)
|
||||||
|
|
||||||
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();)
|
|
||||||
{
|
{
|
||||||
const auto &variableDeclaration = **i;
|
auto &argument = *j;
|
||||||
|
// Find term that is equivalent to the given variable
|
||||||
|
auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
|
||||||
|
|
||||||
bool wasVariableReplaced = false;
|
if (!assignedTerm)
|
||||||
|
continue;
|
||||||
|
|
||||||
// TODO: refactor
|
// Replace all occurrences of the variable with the equivalent term
|
||||||
for (auto j = arguments.begin(); j != arguments.end(); j++)
|
for (auto k = arguments.begin(); k != arguments.end(); k++)
|
||||||
{
|
{
|
||||||
auto &argument = *j;
|
if (k == j)
|
||||||
// Find term that is equivalent to the given variable
|
|
||||||
auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
|
|
||||||
|
|
||||||
if (!assignedTerm)
|
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
// Replace all occurrences of the variable with the equivalent term
|
auto &otherArgument = *k;
|
||||||
for (auto k = arguments.begin(); k != arguments.end(); k++)
|
otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
|
||||||
{
|
|
||||||
if (k == j)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
auto &otherArgument = *k;
|
|
||||||
otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
|
|
||||||
}
|
|
||||||
|
|
||||||
arguments.erase(j);
|
|
||||||
|
|
||||||
wasVariableReplaced = true;
|
|
||||||
simplificationResult = OperationResult::Changed;
|
|
||||||
|
|
||||||
break;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
if (wasVariableReplaced)
|
arguments.erase(j);
|
||||||
{
|
wasVariableReplaced = true;
|
||||||
i = exists.variables.erase(i);
|
break;
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
i++;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
return simplificationResult;
|
if (wasVariableReplaced)
|
||||||
|
{
|
||||||
|
i = exists.variables.erase(i);
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
|
||||||
|
i++;
|
||||||
}
|
}
|
||||||
};
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
// 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”
|
||||||
struct SimplificationRuleEmptyConjunction
|
if (arguments.empty())
|
||||||
{
|
|
||||||
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);
|
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());
|
||||||
|
|
||||||
struct SimplificationRuleOneElementConjunction
|
// If there are still remaining variables, simplification is over
|
||||||
{
|
if (!exists.variables.empty())
|
||||||
static constexpr const auto Description = "[conjunction of only F] === F";
|
return;
|
||||||
|
|
||||||
static OperationResult apply(ast::Formula &formula)
|
assert(!arguments.empty());
|
||||||
{
|
|
||||||
if (!formula.is<ast::And>())
|
|
||||||
return OperationResult::Unchanged;
|
|
||||||
|
|
||||||
auto &and_ = formula.get<ast::And>();
|
// If there is more than one element in the conjunction, replace the input formula with the conjunction
|
||||||
|
formula = std::move(exists.argument);
|
||||||
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 ¬_ = formula.get<ast::Not>();
|
|
||||||
|
|
||||||
if (!not_.argument.is<ast::Not>())
|
|
||||||
return OperationResult::Unchanged;
|
|
||||||
|
|
||||||
auto ¬Not = 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 ¬_ = 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 ¬_ = 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
|
// Performs the different simplification techniques
|
||||||
struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
|
struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyFormulaVisitor>
|
||||||
{
|
{
|
||||||
// Do nothing for all other types of expressions
|
// Forward exists statements to the dedicated simplification function
|
||||||
static OperationResult accept(ast::Formula &formula)
|
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 &)
|
||||||
{
|
{
|
||||||
return simplifyWithDefaultRules(formula);
|
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -575,7 +225,7 @@ struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<Simplif
|
||||||
|
|
||||||
void simplify(ast::Formula &formula)
|
void simplify(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
while (formula.accept(SimplifyFormulaVisitor(), formula) == OperationResult::Changed);
|
formula.accept(SimplifyFormulaVisitor(), formula);
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
@ -8,7 +8,6 @@
|
||||||
|
|
||||||
#include <anthem/Completion.h>
|
#include <anthem/Completion.h>
|
||||||
#include <anthem/Context.h>
|
#include <anthem/Context.h>
|
||||||
#include <anthem/IntegerVariableDetection.h>
|
|
||||||
#include <anthem/Simplification.h>
|
#include <anthem/Simplification.h>
|
||||||
#include <anthem/StatementVisitor.h>
|
#include <anthem/StatementVisitor.h>
|
||||||
#include <anthem/output/AST.h>
|
#include <anthem/output/AST.h>
|
||||||
|
@ -68,12 +67,9 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
||||||
for (auto &scopedFormula : scopedFormulas)
|
for (auto &scopedFormula : scopedFormulas)
|
||||||
simplify(scopedFormula.formula);
|
simplify(scopedFormula.formula);
|
||||||
|
|
||||||
if (context.showStatementsUsed)
|
if (context.visiblePredicateSignatures)
|
||||||
context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";
|
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)
|
for (const auto &scopedFormula : scopedFormulas)
|
||||||
{
|
{
|
||||||
ast::print(context.logger.outputStream(), scopedFormula.formula, printContext);
|
ast::print(context.logger.outputStream(), scopedFormula.formula, printContext);
|
||||||
|
@ -86,34 +82,6 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
||||||
// Perform completion
|
// Perform completion
|
||||||
auto completedFormulas = complete(std::move(scopedFormulas), context);
|
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
|
// Simplify output if specified
|
||||||
if (context.performSimplification)
|
if (context.performSimplification)
|
||||||
for (auto &completedFormula : completedFormulas)
|
for (auto &completedFormula : completedFormulas)
|
||||||
|
@ -126,38 +94,6 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
||||||
ast::print(context.logger.outputStream(), completedFormula, printContext);
|
ast::print(context.logger.outputStream(), completedFormula, printContext);
|
||||||
context.logger.outputStream() << std::endl;
|
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, don’t eliminate it
|
|
||||||
if (!isPredicateVisible)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
for (size_t i = 0; i < predicateDeclaration->parameters.size(); i++)
|
|
||||||
{
|
|
||||||
auto ¶meter = 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;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
@ -123,7 +123,7 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
|
||||||
anthem::translate("input", input, context);
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
CHECK(output.str() ==
|
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")
|
SECTION("useless implications")
|
||||||
|
@ -152,9 +152,9 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
|
||||||
|
|
||||||
CHECK(output.str() ==
|
CHECK(output.str() ==
|
||||||
"forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n"
|
"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)))\n"
|
"forall V2, V3 (in(V2, V3) <-> (V2 in 1..n and V3 in 1..r and in(V2, V3)))\n"
|
||||||
"forall U2 (U2 in (1..n) -> covered(U2))\n"
|
"forall U2 not (U2 in 1..n and not 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");
|
"forall U3, U4, U5 not (in(U3, U4) and in(U5, U4) and exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
SECTION("binary operations with multiple variables")
|
SECTION("binary operations with multiple variables")
|
||||||
|
@ -176,20 +176,4 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
|
||||||
CHECK(output.str() ==
|
CHECK(output.str() ==
|
||||||
"forall V1, V2, V3 (p(V1, V2, V3) <-> #true)\n");
|
"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");
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
|
@ -103,10 +103,9 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
|
||||||
"#show a/1.";
|
"#show a/1.";
|
||||||
anthem::translate("input", input, context);
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
// TODO: simplify further
|
|
||||||
CHECK(output.str() ==
|
CHECK(output.str() ==
|
||||||
"forall V1 (a(V1) <-> not d(V1))\n"
|
"forall V1 (a(V1) <-> not d(V1))\n"
|
||||||
"forall V2 (d(V2) <-> d(V2))\n"
|
"forall V2 (d(V2) <-> not not d(V2))\n"
|
||||||
"forall V3 (e(V3) <-> e(V3))\n");
|
"forall V3 (e(V3) <-> e(V3))\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -150,7 +149,7 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
|
||||||
|
|
||||||
// TODO: simplify further
|
// TODO: simplify further
|
||||||
CHECK(output.str() ==
|
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")
|
SECTION("simple propositions are hidden correctly")
|
||||||
|
@ -165,11 +164,12 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
|
||||||
"#show t/0.";
|
"#show t/0.";
|
||||||
anthem::translate("input", input, context);
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
|
// TODO: simplify further
|
||||||
CHECK(output.str() ==
|
CHECK(output.str() ==
|
||||||
"(s -> not #false)\n"
|
"(s <-> (not #false and s))\n"
|
||||||
"(t -> not #false)\n"
|
"(t <-> (not #false and t))\n"
|
||||||
"(s -> t)\n"
|
"not (s and not t)\n"
|
||||||
"(#false or #false or not #false)\n");
|
"not (not #false and not #false and #false)\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
SECTION("predicate with more than one argument is hidden correctly")
|
SECTION("predicate with more than one argument is hidden correctly")
|
||||||
|
|
|
@ -1,117 +0,0 @@
|
||||||
#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");
|
|
||||||
}
|
|
||||||
}
|
|
|
@ -1,62 +0,0 @@
|
||||||
#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");
|
|
||||||
}
|
|
||||||
}
|
|
|
@ -40,7 +40,7 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]")
|
||||||
input << ":- not covered(I), I = 1..n.";
|
input << ":- not covered(I), I = 1..n.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("comparisons")
|
||||||
|
@ -50,34 +50,4 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]")
|
||||||
|
|
||||||
CHECK(output.str() == "(U1 > U2 -> #false)\n");
|
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");
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
|
@ -24,7 +24,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
||||||
input << "p(1..5).";
|
input << "p(1..5).";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("simple example 2")
|
||||||
|
@ -32,7 +32,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
||||||
input << "p(N) :- N = 1..5.";
|
input << "p(N) :- N = 1..5.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("simple example 3")
|
||||||
|
@ -48,7 +48,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
||||||
input << "p(N, 1, 2) :- N = 1..5.";
|
input << "p(N, 1, 2) :- N = 1..5.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
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.";
|
input << "q(3, N); p(N, 1, 2) :- N = 1..5.";
|
||||||
anthem::translate("input", input, context);
|
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)")
|
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.";
|
input << "q(3, N), p(N, 1, 2) :- N = 1..5.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("escaping conflicting variable names")
|
||||||
|
@ -98,7 +98,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
||||||
input << ":- not p(I), I = 1..n.";
|
input << ":- not p(I), I = 1..n.";
|
||||||
anthem::translate("input", input, context);
|
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)")
|
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).";
|
input << "p(X, 1..10) :- q(X, 6..12).";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("intervals with variable")
|
||||||
|
@ -186,7 +186,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
||||||
input << ":- q(N), 1 = 1..N.";
|
input << ":- q(N), 1 = 1..N.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("intervals with two variables")
|
||||||
|
@ -194,7 +194,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
||||||
input << ":- q(M, N), M = 1..N.";
|
input << ":- q(M, N), M = 1..N.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("comparisons")
|
||||||
|
@ -262,7 +262,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
||||||
anthem::translate("input", input, context);
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
// TODO: eliminate V5: not needed
|
// 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")
|
SECTION("choice rule with body")
|
||||||
|
@ -296,12 +296,4 @@ 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");
|
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");
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,73 +0,0 @@
|
||||||
#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));
|
|
||||||
}
|
|
||||||
}
|
|
Loading…
Reference in New Issue