projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f58c881) | patch
Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 16 May 2016 22:30:59 +0000 (17:30 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 16 May 2016 22:30:59 +0000 (17:30 -0500)
commit246fffffafba07aaeadd0d0c99a2e1c4b589a63c
tree5d2b41e264fc2039da115556befa7fe487a12bb7tree
parentf58c881034d3b0193dfee8fabf451cc0e9ea20abcommit | diff
Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean structure.  Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.
13 files changed:
src/options/quantifiers_options diff | blob | history
src/theory/bv/bitblaster_template.h diff | blob | history
src/theory/bv/eager_bitblaster.cpp diff | blob | history
src/theory/bv/lazy_bitblaster.cpp diff | blob | history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h diff | blob | history
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.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
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/hd-sdiv.sy [new file with mode: 0644] blob