projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3092004) | patch
Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring of term...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 25 Sep 2015 15:58:56 +0000 (17:58 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 25 Sep 2015 15:58:56 +0000 (17:58 +0200)
commit773963f4342bb860fe4deb1d3c65d801b6acd72f
treec5cf5b0685df6311226f7f823f61c7bb3ff14241tree
parent30920046fd6992b6e2c12c33ba888df5c1caf8decommit | diff
Clear term caches for quantifiers + incremental, fixes bug 674.  Refactoring of term database, other refactoring. Bug fixes for cbqi+datatypes.
16 files changed:
src/theory/quantifiers/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.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/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/rewrite_engine.cpp diff | blob | history
src/theory/quantifiers/rewrite_engine.h 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/theory_engine.cpp diff | blob | history
test/regress/regress0/push-pop/Makefile.am diff | blob | history
test/regress/regress0/push-pop/bug674.smt2 [new file with mode: 0644] blob