projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8011f27) | patch
Simplify representation of inversion Skolems for bv cegqi (#1164)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 29 Sep 2017 19:28:52 +0000 (14:28 -0500)
committerGitHub <noreply@github.com>
Fri, 29 Sep 2017 19:28:52 +0000 (14:28 -0500)
commitb48120e1c224208eaef28f86e77830f211852f9b
tree28d9329c1cc13d5e99e8ac38212efb88c20c7ffatree
parent8011f2715fa6ba312fd766cab5249648598310d4commit | diff
Simplify representation of inversion Skolems for bv cegqi (#1164)

* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression.

* Enable other regression
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.h diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 diff | blob | history