Always miniscope nested quantifiers. Disable miniscoping when cegqi enabled. Simpli...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 27 Jan 2015 17:17:27 +0000 (18:17 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 27 Jan 2015 17:17:27 +0000 (18:17 +0100)
commit3d82de01011931ee352715ac4f45c7bbc66f2201
tree27009ced9e0af2cc1706053ffed6913ac7344447
parentb2334221c88ba8ae6adbd27b0802aa2b02641378
Always miniscope nested quantifiers.  Disable miniscoping when cegqi enabled.  Simplify option names.
src/smt/smt_engine.cpp
src/theory/quantifiers/ce_guided_instantiation.cpp
src/theory/quantifiers/options
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h