projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e8bbee7) | patch
Remove arrays lazy rintro option (#4806)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 28 Jul 2020 21:02:41 +0000 (16:02 -0500)
committerGitHub <noreply@github.com>
Tue, 28 Jul 2020 21:02:41 +0000 (16:02 -0500)
commitc323481d737d82b4b4b2906afec3200fe223707f
tree636834eedc604f26799a7d54c69550e416c291f8tree
parente8bbee7afb039834955aee96d181b499550a28fecommit | diff
Remove arrays lazy rintro option (#4806)

This option has model soundness issues (#4771) and moreover is overall worse performance on SMT-LIB {QF_ABV QF_ABVFP QF_ABVFPLRA QF_ALIA QF_ANIA QF_AUFBV QF_AUFLIA QF_AUFNIA QF_AX}:

                           Configuration  #unsat      time    #sat      time #solved    #total
                         CVC4-072720_def    9428   9405.46   24932   16631.6     34360     35399
                       CVC4-072720_nalr1    9446   9536.41   24924   16146.3     34370     35399
where def = default, nalr1 = --no-arrays-lazy-rintro1.

Fixes #4771.

FYI @barrettcw
src/options/arrays_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history