projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0e956da) | patch
Refactoring, generalization of bounded inference module. Simplification of rep set...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 7 Dec 2016 18:43:15 +0000 (12:43 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 7 Dec 2016 18:43:31 +0000 (12:43 -0600)
commite8c09abb9165278b13491c83bdcbe17ae535126e
tree1101d3e878bcfd9e12cd64aaad3017aa320c896btree
parent0e956da9b32ce8a8fcf20ec65e5a2820b4e31324commit | diff
Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
16 files changed:
src/options/quantifiers_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.h diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/quant_split.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/rep_set.h diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/bounded_sets.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/fmf-bound-2dim.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/fmf-strange-bounds-2.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/fmf-strange-bounds.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/memory_model-R_cpp-dd.cvc [new file with mode: 0644] blob