Merge release 'v0.2.0'

.gitignore

@@ -102,3 +102,6 @@ venv.bak/
 
 # mypy
 .mypy_cache/
+
+# VSCode
+.vscode/

.travis.yml

@@ -1,28 +1,26 @@
 language: python
 
 
-include:
+python: 
+  - "3.6"
 
-  - python: 3.6
+os:
+  - linux
 
 before_install:
-
-  - wget http://repo.continuum.io/miniconda/Miniconda-latest-Linux-x86_64.sh -O miniconda.sh
+  - wget https://repo.continuum.io/miniconda/Miniconda3-latest-Linux-x86_64.sh -O miniconda.sh
   - chmod +x miniconda.sh
-  - ./miniconda.sh -b
-  - export PATH=/home/travis/miniconda2/bin:$PATH
-  - conda update --yes conda
+  - bash miniconda.sh -b -p $HOME/miniconda
+  - source "$HOME/miniconda/etc/profile.d/conda.sh"
+  - hash -r
+  - conda config --set always_yes yes --set changeps1 no
+  - conda update -q conda
 
 install:
-
-  - conda create --yes -n test python=$TRAVIS_PYTHON_VERSION
-  - source activate test
-
-  - conda install --yes -c potassco clingo
-  - conda install --yes -c anaconda pylint
-  - conda install --yes -c anaconda pytest 
+  - conda env create -f environment.yml
+  - conda activate eclingo
+  - python3 -m pip install .
 
 script:
-
-  - pylint -E eclingo.py src/parser/parser.py src/solver/solver.py test/test_main.py test/support/support.py
-  - python3 -m pytest
+  - pylama
+  - python3 -m pytest --durations=5 -vv

MANIFEST.in

@@ -0,0 +1 @@
+include LICENSE README.md

README.md

@@ -1 +1,176 @@
-# eclingo
+# eclingo
+
+> A solver for Epistemic Logic Programs.
+
+![Travis](https://travis-ci.com/potassco/eclingo.svg?token=UsJRkwzSfzyEzdaYoHPd&branch=master&status=passed)
+![GitHub](https://img.shields.io/github/license/potassco/eclingo?color=blue)
+![GitHub release (latest by date)](https://img.shields.io/github/v/release/potassco/eclingo)
+
+---
+
+## Description
+`eclingo` is a solver for epistemic logic programs built upon the ASP system [`clingo`](https://github.com/potassco/clingo).  
+Currently, `eclingo` can compute world views under the following semantics:
+- Gelfond 1991; Gelfond and Przymusinska 1993; Gelfond 1994 (G94) [[1, 2, 3]](#references)
+- Kahl et al. 2015 (K15) [[4]](#references)
+
+## Dependencies
+
+- `python 3.6`
+- `clingo 5.4.0` Python module.
+
+## Installation
+
+### Clone
+
+Clone this repo:
+```
+git clone https://github.com/potassco/eclingo.git
+```
+
+### Setup
+
+Change your directory and install `eclingo`:
+```
+cd eclingo/
+pip install .
+```
+
+## Usage
+
+```
+$ eclingo --help
+eclingo version 0.2.0
+usage: eclingo [-h] [-n MODELS] [-k] [-op OPTIMIZATION] [-c CONST]
+               input_files [input_files ...]
+
+positional arguments:
+  input_files           path to input files
+
+optional arguments:
+  -h, --help            show this help message and exit
+  -n MODELS, --models MODELS
+                        maximum number of models to compute (0 computes all
+                        models)
+  -k, --k15             computes world views under K15 semantics
+  -op OPTIMIZATION, --optimization OPTIMIZATION
+                        number of optimization to use (0 for no optimizations)
+  -c CONST, --const CONST
+                        adds a constant to the program (using '<name>=<term>'
+                        format)
+```
+
+### Input language
+
+`eclingo`'s syntax considers three types of statements:
+- [Rules](#rules)
+- [Show statements](#show-statements)
+- [Constant definitions](#constant-definitions)
+
+#### Rules
+
+`eclingo` accepts rules with the same structure as `clingo` does. Additionally, `eclingo` allows these rules to include subjective literals in their body. These subjective literals are represented using the modal operator **K**, which is represented as `&k{}`. The expression inside the curly braces can be an explicit literal (that is, an atom `A` or its explicit negation `-A`) possibly preceded by default negation, that is represented inside the braces as `~`.
+
+> Modal operator **M** is not directly supported but `M A` can be replaced by the construction `not &k{ ~ A}`.
+
+For example, the epistemic logic program:
+```
+p <- M q.
+```
+is written under `eclingo`'s syntax as:
+```
+p :- not &k{ ~ q }.
+```
+
+#### Show statements
+Show statements follow `clingo`'s syntax but, in eclingo, they refer to *subjective atoms*.
+
+For example, the show statement:
+```
+#show p/1.
+```
+refers to the subjective atom `&k{p/1}`.
+
+
+#### Constant definitions
+
+`eclingo` accepts constant definitions in the same way as `clingo` does.
+For example, to declare the constant `length` with value `2`, the following statement is written:
+```
+#const length=2.
+```
+
+### Examples
+
+This repo contains a set of example scenarios inside the `test` folder.
+
+- The `prog` folder, includes some basic programs.
+- The `eligible` folder, includes the knowledge base and a set of 25 instances of the *Scholarship Eligibility Problem*.
+- The `yale` folder, includes the knowledge base and a set of 12 instances of the *Yale Shooting Problem*.
+- The `ground_yale` folder, includes a set of 12 instances of a ground version of the *Yale Shooting Problem*.
+- The `paths` folder, includes the knowledge base and a set of 5 instances of a custom search problem that involves directed graphs.
+
+
+#### Simple example
+
+Run `eclingo` passing the input files paths as arguments.
+
+```
+$ eclingo test/eligible/eligible.lp test/eligible/input/eligible10.lp
+eclingo version 0.2.0
+Solving...
+Answer: 1
+&k{ -eligible(van) } &k{ eligible(mary) } &k{ eligible(nancy) } &k{ eligible(paul) } &k{ eligible(sam) } &k{ eligible(tim) }
+SATISFIABLE
+
+Elapsed time: 0.008156 s
+```
+> Note that you can provide several paths to split the problem encoding from its instances.
+
+#### Computing `n` models
+
+The `-n` flag allows the user to select the maximum number of models to compute (0 for all models).
+
+```
+$ eclingo test/prog/input/prog02.lp -n 0
+eclingo version 0.2.0
+Solving...
+Answer: 1
+&k{ a }
+Answer: 2
+&k{ b }
+SATISFIABLE
+
+Elapsed time: 0.005810 s
+```
+> By default, `eclingo` computes just one model.
+
+#### Solving a conformant planning problem
+We can use the `-c` flag to declare a constant.
+In the case of a planning problem, this is useful to indicate the length of the path:
+```
+$ eclingo test/yale/yale.lp test/yale/input/yale04.lp -c length=4
+eclingo version 0.2.0
+Solving...
+Answer: 1
+&k{ occurs(load, 0) } &k{ occurs(load, 2) } &k{ occurs(pull_trigger, 1) } &k{ occurs(pull_trigger, 3) }
+SATISFIABLE
+
+Elapsed time: 0.014135 s
+```
+
+## License
+
+- **[MIT license](https://github.com/potassco/eclingo/blob/master/LICENSE)**
+
+---
+
+## References
+
+[1] Gelfond, M. 1991. Strong introspection. In Proceedings of the Ninth National Conference on Artificial Intelligence (AAAI’91), T. Dean and K. McKeown, Eds. AAAI Press / The MIT Press, 386–391.
+
+[2] Gelfond, M. and Przymusinska, H. 1993. Reasoning on open domains. In Logic Programming and Non-monotonic Reasoning, Proceedings of the Second International Workshop, Lisbon, Portugal, June 1993, L. Moniz Pereira and A. Nerode, Eds. MIT Press, 397–413.
+
+[3] Gelfond, M. 1994. Logic programming and reasoning with incomplete information. Annals of Mathematics and Artificial Intelligence 12, 1-2, 89–116.
+
+[4] Kahl, P., Watson, R., Balai, E., Gelfond, M., and Zhang, Y. 2015. The language of epistemic specifications (refined) including a prototype solver. Journal of Logic and Computation.

eclingo/__main__.py

@@ -0,0 +1,49 @@
+import argparse
+from time import perf_counter as timer
+import eclingo.main as eclingo
+
+
+def main():
+    print(f'eclingo version {eclingo.__version__}')
+
+    argparser = argparse.ArgumentParser(prog='eclingo')
+    argparser.add_argument('-n', '--models', type=int,
+                           help='maximum number of models to compute (0 computes all models)',
+                           default=1)
+    argparser.add_argument('-k', '--k15', action='store_true',
+                           help='computes world views under K15 semantics')
+    argparser.add_argument('-op', '--optimization', type=int,
+                           help='number of optimization to use (0 for no optimizations)',
+                           default=eclingo.__optimization__)
+    argparser.add_argument('-c', '--const', action='append',
+                           help='adds a constant to the program (using \'<name>=<term>\' format)')
+    argparser.add_argument('input_files', nargs='+', type=str, help='path to input files')
+    args = argparser.parse_args()
+
+    start = timer()
+
+    eclingo_control = eclingo.Control(max_models=args.models,
+                                      semantics=args.k15,
+                                      optimization=args.optimization)
+
+    for file_path in args.input_files:
+        eclingo_control.load(file_path)
+    if args.const:
+        for constant in args.const:
+            name, term = constant.split('=')
+            eclingo_control.add_const(name, term)
+
+    eclingo_control.parse()
+    print('Solving...')
+    for model in eclingo_control.solve():
+        print(f'Answer: {eclingo_control.models}\n{model}')
+
+    end = timer()
+
+    print('SATISFIABLE\n') if eclingo_control.models else print('UNSATISFIABLE\n')
+
+    print(f'Elapsed time: {(end-start):.6f} s')
+
+
+if __name__ == "__main__":
+    main()

eclingo/main.py

@@ -0,0 +1,66 @@
+import clingo
+from eclingo.preprocessor.preprocessor import G94Preprocessor, K15Preprocessor
+from eclingo.parser.parser import Parser
+from eclingo.solver.solver import Solver
+from eclingo.postprocessor.postprocessor import Postprocessor
+from eclingo.utils.logger import logger, silent_logger
+
+
+__version__ = '0.2.0'
+__optimization__ = 3
+
+
+class Control:
+
+    def __init__(self, max_models=1, semantics=False, optimization=__optimization__):
+        self.models = 0
+        self.max_models = max_models
+        self.semantics = semantics
+        self.optimization = optimization
+        self._candidates_gen = clingo.Control(['0', '--project'], logger=silent_logger)
+        self._candidates_test = clingo.Control(['0'], logger=logger)
+        self._epistemic_atoms = {}
+        self._predicates = []
+        self._show_signatures = set()
+
+    def add(self, program):
+        if self.semantics:
+            preprocessor = K15Preprocessor(self._candidates_gen, self._candidates_test,
+                                           self.optimization)
+        else:
+            preprocessor = G94Preprocessor(self._candidates_gen, self._candidates_test,
+                                           self.optimization)
+
+        preprocessor.preprocess(program)
+        self._predicates.extend(preprocessor.predicates)
+        self._show_signatures.update(preprocessor.show_signatures)
+
+        del preprocessor
+
+    def add_const(self, name, value):
+        self.add(f'#const {name}={value}.')
+
+    def load(self, input_path):
+        with open(input_path, 'r') as program:
+            self.add(program.read())
+
+    def parse(self):
+        parser = Parser(self._candidates_gen, self._candidates_test,
+                        self._predicates, self.optimization)
+
+        parser.parse()
+        self._epistemic_atoms.update(parser.epistemic_atoms)
+
+        del parser
+
+    def solve(self):
+        solver = Solver(self._candidates_gen, self._candidates_test,
+                        self._epistemic_atoms, self.max_models)
+        postprocessor = Postprocessor(self._candidates_test, self._show_signatures)
+
+        for model, assumptions in solver.solve():
+            self.models += 1
+            yield postprocessor.postprocess(model, assumptions)
+
+        del solver
+        del postprocessor