Solver for Array Folds Logic
C++ SMT Other
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
benchmarks
experiments
tinyxml
.gitignore
LICENSE
Makefile
README.md
afolder.cc
automata.cc
automata.h
cm.cc
cm.h
common.cc
common.h
dp.cc
emptiness.cc
emptiness.h
folds.cc
folds.h
graph.cc
graph.h
parikh.cc
parikh.h
pda.cc
pda.h
run_benchmarks.sh
run_experiments.sh
scm.cc
scm.h
semptiness.cc
semptiness.h
semptinessaux.cc
semptinessaux.h

README.md

AFolder - Solver for Array Folds Logic.

0. License

Copyright (c) 2016 Przemyslaw Daca. This software is distributed under the MIT Licences. This software is based on TinyXML library (http://www.grinninglizard.com/tinyxml/)

1. Requirements

AFolder requires the Z3 theorem prover to be installed (https://github.com/Z3Prover/z3).

2. Compilation

Type 'make' to compile.

3. Usage example

./afolder benchmarks/markdown2.smt benchmarks/markdown2.xml -model

The input is an SMT formula, and an XML formula that is a functional description of folds.

4. Running benchmarks

To run all benchmarks execute './run_benchmarks.sh'