projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e9fb730) | patch
Work on conjecture generator : do not generalize subterms with concrete values, filte...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 3 Sep 2014 10:35:00 +0000 (12:35 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 3 Sep 2014 10:35:00 +0000 (12:35 +0200)
commit83f91b92090ef0231156560f337affc6e5c2a33f
treed0fe321ce4a6d29742688b9e8a5eaec859bd60edtree
parente9fb730333b2719cddaa0a9209aa7953d7f30b0bcommit | diff
Work on conjecture generator : do not generalize subterms with concrete values, filter conjectures with ground substitutions whose equality is unknown, simplify generalization depth calculation.  Print --dump-instantiations on sat/unknown.
src/main/command_executor.cpp diff | blob | history
src/main/command_executor_portfolio.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.h diff | blob | history
src/theory/quantifiers/options diff | blob | history