projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 675e82e) | patch
Document term db (#1220)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 28 Oct 2017 14:13:13 +0000 (09:13 -0500)
committerGitHub <noreply@github.com>
Sat, 28 Oct 2017 14:13:13 +0000 (09:13 -0500)
commit34e84a25a044e3af192bb69089467c2125911900
tree924a3ae0894bfec136f91949a1bf55e19c4125datree
parent675e82e32a34911163f9de0e6389eb107be5b0f1commit | diff
Document term db (#1220)

* Document TermDb and related classes. Minor changes to quantifiers utils and their interface.  Address some comments left over from PR 1206.

* Minor

* Minor

* Change namespace style.

* Address review

* Fix incorrectly merged portion that led to regression failures.

* New clang format, fully document relevant domain.

* Clang format again.

* Minor
15 files changed:
src/theory/quantifiers/equality_query.cpp diff | blob | history
src/theory/quantifiers/equality_query.h diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/inst_propagator.h diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/quantifiers_attributes.cpp diff | blob | history
src/theory/quantifiers/quantifiers_attributes.h diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.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/term_util.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/theory.h diff | blob | history