projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5031c6d) | patch
CBQI BV quick heuristics (#1239)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 13 Oct 2017 05:12:02 +0000 (00:12 -0500)
committerMathias Preiner <mathias.preiner@gmail.com>
Fri, 13 Oct 2017 05:12:02 +0000 (22:12 -0700)
commit39a85cc99f3b9f3d203490f5918ebe56bd916d64
tree1962850621944d07af786ff491463e043aefcff1tree
parent5031c6d9a08c84a6e8fe5019c6e278b8b2d7a238commit | diff
CBQI BV quick heuristics (#1239)

Adds two heuristics for cbqi-bv, both disabled by default.

The first optimistically solves for boundary points of inequalities.
The second randomly interleaves inversion and value instantiations.
Adds some newly solved regressions from SMT LIB.
src/options/quantifiers_options diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.cpp diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/intersection-example-onelane.proof-node22337.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/nested9_true-unreach-call.i_575.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/small-pipeline-fixpoint-3.smt2 [new file with mode: 0644] blob