About
On this page we provide source code and logs for our paper
Constructing Cycles in the Simplex Method for DPLL(T).
Constructing Cycles using Linear Real Arithmetic
- simplex-dpll.hs
- This Haskell program is the generator we used for constructing cycling
examples using linear real arithmetic.
- r8-yices.sh
- Shell code for finding nice cycles of length 8 using Yices 2.5.2
- r8-yices.log
- sample log
- r8-yices.smt
- sample satisfiable SMT problem
- r8-yices.sol
- output by Yices
- r8-z3.sh
- Shell code for finding nice cycles of length 8 using Z3 4.5.0
- r8-z3.log
- sample log
- r8-z3.smt
- sample satisfiable SMT problem
- r8-z3.sol
- output by Z3
Constructing Cycles using Nonlinear Real Arithmetic
- standard-simplex.smt
- naive encoding of a cycle in the standard simplex (neither Yices nor Z3 produced any solution in 600s)
- standard-simplex-zoernig-simp.smt
- encoding of cycle of length 6 with 2 constraints using Zörnig's encoding
- standard-simplex-zoernig-simp.sol
- corresponding output (by Yices; Z3 didn't produce a solution in 600s)
- standard-simplex-zoernig-simp-tweak.smt
- the same encoding with some values fixed (obtained by trial and error, rounding values from previously obtained solutions)
- standard-simplex-zoernig-simp.sol
- corresponding output
Links