projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 75d3b08) | patch
Add new method for checking candidate models, --fmf-fmc. Add infrastructure for...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 9 May 2013 01:02:10 +0000 (20:02 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 9 May 2013 01:02:22 +0000 (20:02 -0500)
commit85377f73a331b334437aa0d50d15c81e905869c1
treebb98f8ec511f9314731fe4545b6e9b8f64d18b33tree
parent75d3b086d2cbcb4508446e405e0599788a3a25a5commit | diff
Add new method for checking candidate models, --fmf-fmc.  Add infrastructure for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp).  Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model.  Add option for relational triggers such as x = f(y), --relational-trigger.
26 files changed:
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/Makefile.am diff | blob | history
src/theory/quantifiers/bounded_integers.cpp [new file with mode: 0755] blob
src/theory/quantifiers/bounded_integers.h [new file with mode: 0755] blob
src/theory/quantifiers/full_model_check.cpp [new file with mode: 0755] blob
src/theory/quantifiers/full_model_check.h [new file with mode: 0755] blob
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/model_engine.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quant_util.cpp 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/trigger.cpp diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/uf/options diff | blob | history
src/theory/uf/theory_uf_model.cpp diff | blob | history
src/theory/uf/theory_uf_model.h diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history