projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e4cff69) | patch
Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default...
authorajreynol <andrew.j.reynolds@gmail.com>
Sat, 27 Jun 2015 07:30:06 +0000 (09:30 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Sat, 27 Jun 2015 07:30:06 +0000 (09:30 +0200)
commit65c2e1688d83dfeb913b689c10d9b43c5dc89cc0
treef552414624cd7259e638b6edc0c7a710a4215138tree
parente4cff69e3b565e928dbf04960249477ce2c9ef6bcommit | diff
Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.
18 files changed:
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/model_builder.h diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quant_util.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
src/theory/rep_set.cpp diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history
src/util/sort_inference.cpp diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/syn002-si-real-int.smt2 [new file with mode: 0755] blob