projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5b8b6ac) | patch
first draft of new inst gen method (still with bugs), some cleanup of quantifiers...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 16 Oct 2012 17:10:47 +0000 (17:10 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 16 Oct 2012 17:10:47 +0000 (17:10 +0000)
commitbbcfb5208c6c0f343d1a63b129c54914f66b2701
treef2369b3cc07121645ef0c8c3a415f243f5a4fcb9tree
parent5b8b6acd9091e2afec654ebed1332d6755bbb7d9commit | diff
first draft of new inst gen method (still with bugs), some cleanup of quantifiers code
18 files changed:
src/theory/quantifiers/Makefile.am diff | blob | history
src/theory/quantifiers/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/candidate_generator.h diff | blob | history
src/theory/quantifiers/inst_gen.cpp [new file with mode: 0755] blob
src/theory/quantifiers/inst_gen.h [new file with mode: 0755] blob
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.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.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/rewriterules/theory_rewriterules.cpp diff | blob | history
src/theory/uf/theory_uf_model.cpp diff | blob | history