projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 03cc40c) | patch
Refactor theory model (#1236)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 27 Oct 2017 16:20:50 +0000 (11:20 -0500)
committerGitHub <noreply@github.com>
Fri, 27 Oct 2017 16:20:50 +0000 (11:20 -0500)
commit079ed9540d498bcbb58f2f0fbe87bdae28101d1e
tree8c3ba1818dc515c1714b23555460a3a39192acc5tree
parent03cc40cc070df0bc11c1556cef3016f784a95d23commit | diff
Refactor theory model (#1236)

* Refactor theory model, working on making RepSet references const.

* Encapsulation of members of rep set.

* More documentation on rep set.

* Swap names

* Reference issues.

* Minor

* Minor

* New clang format.
15 files changed:
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/quantifiers/ambqi_builder.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/equality_query.cpp diff | blob | history
src/theory/quantifiers/full_model_check.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_engine.cpp diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/rep_set.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history
src/theory/uf/theory_uf_model.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history