projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f7c6707) | patch
Updates to E-matching to avoid entailed instantiations earlier. Minor updates to...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 30 Mar 2016 19:06:27 +0000 (14:06 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 30 Mar 2016 19:06:34 +0000 (14:06 -0500)
commit2abcda1cfcb0c6388c00d65f8a6b3e63de9d96df
tree6c72c3145cef49e76b1f8e5577947d441e14f938tree
parentf7c6707fa38a850d6798c747b3c45ef10769fa7ccommit | diff
Updates to E-matching to avoid entailed instantiations earlier. Minor updates to datatypes lemmas, other minor changes.
14 files changed:
src/options/quantifiers_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.cpp 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_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.h diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.h diff | blob | history
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history