projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f70804a) | patch
Change default option to --inst-when=full-last-call (interleave instantiation and...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 21 Nov 2014 08:42:07 +0000 (09:42 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 21 Nov 2014 08:42:07 +0000 (09:42 +0100)
commit32b0aba2c2c27ad038d34c8554a4bae76e8dd363
treee6e737d10b53c0c13dfba072cdec6d1f9b5449a2tree
parentf70804a7159390fcb01d8c1ec208fbfd8e544fbacommit | diff
Change default option to --inst-when=full-last-call (interleave instantiation and theory combination).  Fix inefficiency in NNF, enable by default.  Set best defaults for --mbqi=abs.
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/options_handlers.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
test/regress/regress0/quantifiers/burns4.smt2 diff | blob | history