ConstraintSpecialisation specialises a set of Constrainted Horn clauses with repect to a goal (at the moment "false").
ConstraintSpecialisation is written in Ciao prolog (32 bit version) and is interfaced with Parma polyhedra libray for handling constraints. Any library interfaced with Ciao should also be in 32 bit. ConstraintSpecialisation uses several reusable components such as Convex polyhedra analyser, Query-answer tranformer etc. tied together using a shell script.
- Ciao prolog
- Parma polyhedra libray
Input and output:
Input: a set of Horn clauses. They are written using Prolog notation: e.g. h(X):- C, b1(X1),...,bn(Xn).
Output: A specialised set of Horn clauses.
How to run:
- cd src
- ciaoc thresholds; ciaoc cpascc; ciaoc qa; ciaoc insertProps; ciaoc stripSuffix
- sh specialiseConstraints.sh <File containing a set of Horn clauses> <Output file for storing a set of specialised Horn clauses>
Please edit specialiseConstraints.sh before running the program.
Constraint specialisation in Horn clause verification by Bishoksan Kafle and John P. Gallagher in PEPM 2015 (http://dl.acm.org/citation.cfm?id=2682544).