projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9b9864d) | patch
Implementation of model-based projection in cbqi, cleanup, add regressions.
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 19 Aug 2015 07:35:17 +0000 (09:35 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 19 Aug 2015 07:35:24 +0000 (09:35 +0200)
commit331ec1abc311a6be85eb5adc0ca70f4e3c0c79a2
treed6f74f6513d00a91ef0b0cfbedc9e1333de687a9tree
parent9b9864d639ccf474dedd66c5691c93ca17b670e9commit | diff
Implementation of model-based projection in cbqi, cleanup, add regressions.
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/RND-small.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/clock-10.smt2 [new file with mode: 0644] blob