projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 519cdc2) | patch
Move equality query utility into quantifiers model (#6186)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 22 Mar 2021 18:42:46 +0000 (13:42 -0500)
committerGitHub <noreply@github.com>
Mon, 22 Mar 2021 18:42:46 +0000 (18:42 +0000)
commit134985065820077d2628023b9b72f78471392968
tree544c433dbc20f3022f964f582d0395817ccb72abtree
parent519cdc2d4b44a9785ee68d181e2682d74890e89acommit | diff
Move equality query utility into quantifiers model (#6186)

This simplifies the initialization of quantifiers engine.

This PR also makes general improvements to EqualityQuery.
src/theory/quantifiers/ematching/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/equality_query.cpp diff | blob | history
src/theory/quantifiers/equality_query.h 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/fmf/first_order_model_fmc.cpp diff | blob | history
src/theory/quantifiers/fmf/model_engine.cpp diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history