projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: decde5b) | patch
Minor improvements for alpha equivalence and partial quantifier elimination in increm...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 13 Apr 2016 20:02:31 +0000 (15:02 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 13 Apr 2016 20:02:31 +0000 (15:02 -0500)
commit199cf857baa106545196503cc4029e2b7771d1af
treee51f45c941ef6bf8995cbfcc02494784b76b26f1tree
parentdecde5be0b6409b9c1b84f40c8383bb8483e4566commit | diff
Minor improvements for alpha equivalence and partial quantifier elimination in incremental mode. Change defaults to addInstantiation method.
17 files changed:
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/alpha_equivalence.cpp diff | blob | history
src/theory/quantifiers/alpha_equivalence.h diff | blob | history
src/theory/quantifiers/ambqi_builder.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/full_model_check.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_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/model_engine.cpp 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_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history