projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a9bf7fc) | patch
Refactoring of model engine to separate individual implementations of model builder...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 25 Jun 2013 17:18:05 +0000 (12:18 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 25 Jun 2013 17:18:14 +0000 (12:18 -0500)
commitd8de492163b90974709a16918cb615515a536afc
tree8241c94be9a610149b40af0fc0932ee05094b2aatree
parenta9bf7fc500daba46ed86ca744c1346059880e6f4commit | diff
Refactoring of model engine to separate individual implementations of model builder.  Begin work on interval models for integers.  Other minor cleanup.
14 files changed:
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/first_order_model.cpp diff | blob | history
src/theory/quantifiers/first_order_model.h diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/full_model_check.h 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/model_engine.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/rep_set.h diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history