What can be downloaded from this page ?
- A research report containing a complete description of our instantiation schema (with detailed proofs and examples).
- A prolog program implementing the completeness criteria.
- An input file containing some theories of interest in the SMT community.
We have developed an instantiation
schema which reduces (in some cases) the satisfiability
problem for a set S
1 of first-order clauses to a satisfiability problem
for a (finite) set S
0 of ground instances of the clauses in S
1. The latter problem is
well-known to be decidable, whereas the former is only sem-decidable.
This instantiation schema is
flat in the sense that every clause in S
0 is obtained from a clause in S
1 by replacing all the variables in it by constant symbols.
This instantiation schema is intented to be used for solving
Satisfiability Modulo Theories problems.
It is (trivially) sound, i.e. if the obtained clause set S
0 is
unsatisfiable then so is the original one S
1. The converse (refutationally
completeness) holds only for some particular clause sets, called
controllable. Details can be found in the following
research report.
Determining whether a given clause set is controllable or not is a
decidable problem, but it is not straigtforward since it requires
checking many different conditions involving fixpoint computations.
Moreover several parameters have to be set properly. Thus we have
developed a small
program to automatise the process. Here is an
example of an input file, containing the main theories that are useful in program verification (lists, arrays etc.).
The program is written in Prolog. It should run easily on any Prolog system (tested only on
SWI-Prolog).
The instantiation schema itself is not yet implemented (we hope to be
able to do this soon...). The program uses a straightforward
implementation of the conditions defined in the above report, without
any optimisation. It is not intended to be efficient, and will probably
not work if the clause set is very large, but it is meant to be easily
modifiable and extensible and as clear as possible.
Disclaimer: this program is a highly.
experimental software. It has been developed for facilitating on-going
researches and is delivered as it is, for research purpose only,
without any guarantee. See here for details.
For further information, please contact
N. Peltier or
M. Echenim
Laboratory of Informatics of Grenoble, CAPP Team