projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 83c0e6c) | patch
Add term db mode. Minor changes to quantifiers rewriter: split ITE's where equality...
authorajreynol <andrew.j.reynolds@gmail.com>
Sun, 16 Nov 2014 15:38:50 +0000 (16:38 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Sun, 16 Nov 2014 15:38:50 +0000 (16:38 +0100)
commitd8da3b13bc9df7750723cf3da38edc8cb6f67d3d
tree5eaf5af8346b95c84d41c0feb1e14864c02bf035tree
parent83c0e6c14955e04b3dca56037508e4ceb6691f10commit | diff
Add term db mode.  Minor changes to quantifiers rewriter: split ITE's where equality resolution is possible on condition, pull nested quantifiers from ITE branches.  Minor cleanup.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/modes.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/options_handlers.h diff | blob | history
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history