projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eb7f6bf) | patch
Generalize CandidateRewriteDatabase to ExprMiner (#2340)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 14 Sep 2018 02:48:25 +0000 (21:48 -0500)
committerGitHub <noreply@github.com>
Fri, 14 Sep 2018 02:48:25 +0000 (21:48 -0500)
commit4a9a0dcb8b06e3fc917b642426140b044a64facd
treeaf90c7520f3dce3046f2d5fcd597fe8de76f41f0tree
parenteb7f6bf4eb7a84ce0e9c2f6578ce76ecab88d020commit | diff
Generalize CandidateRewriteDatabase to ExprMiner (#2340)
src/Makefile.am diff | blob | history
src/options/quantifiers_options.toml diff | blob | history
src/theory/quantifiers/candidate_rewrite_database.cpp diff | blob | history
src/theory/quantifiers/candidate_rewrite_database.h diff | blob | history
src/theory/quantifiers/expr_miner.cpp [new file with mode: 0644] blob
src/theory/quantifiers/expr_miner.h [new file with mode: 0644] blob
src/theory/quantifiers/expr_miner_manager.cpp [new file with mode: 0644] blob
src/theory/quantifiers/expr_miner_manager.h [new file with mode: 0644] blob
src/theory/quantifiers/sygus/ce_guided_conjecture.cpp diff | blob | history
src/theory/quantifiers/sygus/ce_guided_conjecture.h diff | blob | history
test/regress/regress1/rr-verify/bv-term.sy diff | blob | history