Extending SMT solvers to Higher-Order Logic

Solvers

The tarballs containing the binaries of the solvers used in our experiments: CVC4, veriT, Ehoh, Leo-III, Satallax

To enable individual configurations of CVC4:

• Configuration @cvc is enabled by: --uf-ho --full-saturate-quant --ho-elim --no-ho-elim-partial --no-ho-elim-store-ax
• Configuration @cvc-sax is enabled by: --uf-ho --full-saturate-quant --ho-elim --no-ho-elim-partial
• Configuration @cvc-ui is enabled by: --uf-ho --full-saturate-quant --fs-interleave --ho-elim --no-ho-elim-partial --no-ho-elim-store-ax
• Configuration @cvc-ui-sax is enabled by: --uf-ho --full-saturate-quant --fs-interleave --ho-elim --no-ho-elim-partial
• Configuration cvc is enabled by: --uf-ho --ho-flatten-total --full-saturate-quant --no-ho-matching
• Configuration cvc-sax is enabled by: --uf-ho --ho-flatten-total --full-saturate-quant --no-ho-matching --ho-elim-store-ax
• Configuration cvc-ui is enabled by: --uf-ho --ho-flatten-total --full-saturate-quant --fs-interleave --no-ho-matching
• Configuration cvc-ui-sax is enabled by: --uf-ho --ho-flatten-total --full-saturate-quant --fs-interleave --no-ho-matching --ho-elim-store-ax
• Configuration @cvc-fmf-sax is enabled by: --uf-ho --finite-model-find --ho-elim --no-ho-elim-partial
• Configuration cvc-fmf is enabled by: --uf-ho --finite-model-find

• Configuration @vt is enabled by: --prune-cnf-off --full-app --disable-print-success --disable-ackermann --disable-unit-subst-simp --ccfv-breadth
• Configuration vt is enabled by: --prune-cnf-off --extentionality --ho-matching --lfree --disable-print-success --disable-ackermann --disable-unit-subst-simp --ccfv-breadth

• Configuration a is enabled by: --delete-bad-limit=2000000000 --definitional-cnf=24 -s --free-numbers --auto
• Configuration as is enabled by: --delete-bad-limit=2000000000 --definitional-cnf=24 -s --free-numbers --auto-schedule --cpu-limit=60
• Configuration b is enabled by: solver options: --delete-bad-limit=2000000000 --definitional-cnf=24 -s --free-numbers --simul-paramod --forward-context-sr --strong-destructive-er --destructive-er-aggressive --destructive-er --presat-simplify -tKBO6 -winvfreqrank -c1 -Ginvfreq -F1 -WSelectMaxLComplexAvoidPosPred -H(1.ConjectureRelativeSymbolWeight(SimulateSOS,0.5,100,100,100,100,1.5,1.5,1,1),4.ConjectureRelativeSymbolWeight(ConstPrio,0.1,100,100,100,100,1.5,1.5,1.5,1),1.FIFOWeight(PreferProcessed),1.ConjectureRelativeSymbolWeight(PreferNonGoals,0.5,100,100,100,100,1.5,1.5,1,1),4.Refinedweight(SimulateSOS,3,2,2,1.5,2,1))
• Configuration hb is enabled by: solver options: --delete-bad-limit=2000000000 --definitional-cnf=24 -s --free-numbers --simul-paramod --forward-context-sr --strong-destructive-er --destructive-er-aggressive --destructive-er --presat-simplify -tKBO6 -winvtypefreqrank -c1 -Ginvtypefreq -F1 -WSelectMaxLComplexAvoidPosPred -H(1.ConjectureRelativeSymbolWeight(SimulateSOS,0.5,100,100,100,100,1.5,1.5,1,1.41),4.ConjectureRelativeTypeSymbolWeight(ConstPrio,0.1,100,100,100,100,1.5,1.5,1.5,1.41),1.FIFOWeight(PreferProcessed),1.ConjectureRelativeSymbolWeight(PreferNonGoals,0.5,100,100,100,100,1.5,1.5,1,1.41),4.Refinedweight(SimulateSOS,3,2,2,1.5,2,1.41))

Benchmarks

• TH0: th0-lf-ehoh.txt
• oTH0: th0-lf-boolsubterm.txt
• λoTH0: th0-lamb.txt

• JD³²: sh_32.tar.gz
• JD⁵¹²: sh_512.tar.gz
• λoSH¹⁰²⁴: benzmueller.tar.gz

• hosmt-th0-lf-ehoh.tar.gz
• hosmt-th0-lf-boolsubterm.tar.gz
• hosmt-sh.tar.gz

Results

According to the naming conventions of the benchmark sets as per the tarballs and problem lists above and with the solver configurations being identified in the CSVs according to the mapping:

• results-tptp.csv
• results-sh.csv
• results-benzmueller.csv