projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1ec95c5) | patch
Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 24 Aug 2015 16:34:25 +0000 (18:34 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 24 Aug 2015 16:34:25 +0000 (18:34 +0200)
commitd7dc7c2b3038b862af5ea55e7cf6b1fc4e1fe684
treed6c229a2659bfcb3cdf7c7c786414ecc1e59e61ctree
parent1ec95c559074ed7575a0165deb16fcee45920e9fcommit | diff
Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.
16 files changed:
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.h diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h 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_util.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/theory_quantifiers.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
test/regress/regress0/quantifiers/ARI176e1.smt2 diff | blob | history