A solver for the symbolic heap fragment of SL with compositional ID. It also supports linear integer arithmetics.
Required libraries:
-
The tool is built using CMake, so install z3 by CMake is necessary.
-
Boost
Then, you can build ComSpen by CMake, like
mkdir build
cd build
cmake ..
make
sudo make installNotes: If z3 can be found by CMake, "-DZ3_DIR" can be ignored, otherwise you should tell cmake how to find z3 configuration. In my system, the path to configuration folder is "/usr/local/lib/cmake/z3/".
The tool receive smt formula and return sat or unsat for the satisfiability problems and entailment problems.
- sat: true for satisfiability problems.
- unsat: true for entailment problems.
The command is
./ComSpen <input_file>For example,
./ComSpen ../samples/qf_shls_sat/spaguetti-10-e01.tptp.smt2
file: ../samples/qf_shls_sat/spaguetti-10-e01.tptp.smt2
THEORY path: ../logic_def/Theories/Core.smt2
THEORY path: ../logic_def/Theories/Ints.smt2
THEORY path: ../logic_def/Theories/SepLogicTyped.smt2
logic: QF_SLID_INT
Heap:
RefSll_t -> Sll_t
predicate:
pars:
in out
base: (and (= in out))
rec: (exists ((u RefSll_t))
(! (and (sep (pto in (c_Sll_t u)) (ls u out))) :weight 0))
pto: (pto in (c_Sll_t (:var 0)))
recursive app: (ls (:var 0) out)
data formula: and
phi: (and (= nil nil)
(distinct x1 x6)
(distinct x1 x7)
(distinct x1 x10)
(distinct x4 x8)
(distinct x4 x7)
(distinct x4 x9)
(distinct x3 x8)
(distinct x7 x10)
(distinct x2 x6)
(distinct x2 x3)
(distinct x2 x7)
(sep (ls x5 x7)
(ls x2 x5)
(ls x2 x10)
(ls x2 x1)
(ls x9 x1)
(ls x7 x6)
(ls x3 x10)
(ls x6 x9)))
psi: null
result: unsatIf you want to use our solvers, you can just include API header in you source files and use find_package to include .so file. See examples.