projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5fae5ff) | patch
Better combination of UF with cbqi, refactor quantifiers intialization.
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 4 Nov 2015 09:41:49 +0000 (10:41 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 4 Nov 2015 09:42:01 +0000 (10:42 +0100)
commitf9e109b0ac12ffbfd167a19dcd60f16241a0542c
tree07547a834d60cbbbd75c91e1695c5518774c813etree
parent5fae5ff49bfc9c96c03c52f5e2a5caa52ac40d03commit | diff
Better combination of UF with cbqi, refactor quantifiers intialization.
16 files changed:
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h 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/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/krs-sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/ari056.smt2 [new file with mode: 0644] blob