projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d9c22c3) | patch
Minor improvements to cbqi, fix bug in solving with vts symbols, round up for integer...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 26 Aug 2015 13:49:23 +0000 (15:49 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 26 Aug 2015 13:49:23 +0000 (15:49 +0200)
commit7c3790db478c4f06e65ef0f777317a4c6a803059
tree89f95e1e0db42a580980b34f58ee1315b73004dbtree
parentd9c22c34d122a34d8a8a914936d9186be9a638fecommit | diff
Minor improvements to cbqi, fix bug in solving with vts symbols, round up for integer lower bounds.  Add presolve infrastructure to quantifiers engine, modify --cbqi-prereg-inst.
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp 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/theory_quantifiers.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history