projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 10f6aae) | patch
Moving methods from quantifiers engine to quantifiers state (#5881)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 13 Feb 2021 14:42:36 +0000 (08:42 -0600)
committerGitHub <noreply@github.com>
Sat, 13 Feb 2021 14:42:36 +0000 (08:42 -0600)
commit0ff53d70b3e0a11e4ae5c1c8f612d809dca2d004
tree212f4f751615c5dbe4173c74ba52e60f708dfd3btree
parent10f6aae991a550e2b970c6234ebdd75742d078ddcommit | diff
Moving methods from quantifiers engine to quantifiers state (#5881)

Towards eliminating dependencies on quantifiers engine.
13 files changed:
src/CMakeLists.txt diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy.cpp [new file with mode: 0644] blob
src/theory/quantifiers/ematching/inst_strategy.h diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h diff | blob | history
src/theory/quantifiers/ematching/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_enumerative.cpp diff | blob | history
src/theory/quantifiers/quantifiers_state.cpp diff | blob | history
src/theory/quantifiers/quantifiers_state.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history