projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3a3a575) | patch
Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 7 Nov 2014 16:38:53 +0000 (17:38 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 7 Nov 2014 16:38:59 +0000 (17:38 +0100)
commit4ad0191e20e4d812d9a5dc3a733153cb10f6d728
treef25fa219a0d464ca7a30b40d27fa45b05ff33638tree
parent3a3a57583fd8bd4af5c3b99b0047c9b20de38bb1commit | diff
Enable --quant-cf by default.  Fix bug in qcf for mixed Int/Real.  Minor improvement to performance of E-matching.
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.h diff | blob | history
src/theory/quantifiers/options 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_engine.cpp diff | blob | history