projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9aaa7ca) | patch
Miniscope top level conjunctions for prenex normal form, allow one level miniscoping...
authorajreynol <andrew.j.reynolds@gmail.com>
Sat, 3 Sep 2016 22:40:18 +0000 (17:40 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Sat, 3 Sep 2016 22:40:18 +0000 (17:40 -0500)
commitce883ca9296c872affb47547304a9ecc0ec5224d
tree2e797668f07fa045bde9f1b690e8402fb8238f97tree
parent9aaa7ca741199f73e70149f8309cd7cd9a12e69fcommit | diff
Miniscope top level conjunctions for prenex normal form, allow one level miniscoping in prenex normal form.
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history