projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1b2e6c8) | patch
Optimizations for QCF to check relevant domain of variable argument positions eagerly...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 12 Apr 2016 15:13:45 +0000 (10:13 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 12 Apr 2016 15:13:45 +0000 (10:13 -0500)
commit4ff2946e1338d3f500b7e6bababee50fadad68d6
tree6f1306e4476e3f7496d7a4e045e63d942802a392tree
parent1b2e6c81be2a8ab0656ff2ee3938ef4587e24e25commit | diff
Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.
25 files changed:
src/options/options_handler.cpp diff | blob | history
src/options/quantifiers_modes.h diff | blob | history
src/theory/quantifiers/anti_skolem.cpp diff | blob | history
src/theory/quantifiers/candidate_generator.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/first_order_model.cpp diff | blob | history
src/theory/quantifiers/first_order_model.h diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/inst_propagator.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/instantiation_engine.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/quant_conflict_find.h diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/rewrite_engine.cpp 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
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 [new file with mode: 0644] blob