projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ae7434f) | patch
Print only instantiations that are in the unsat core when --proof is enabled. Add...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 20 Jul 2016 16:52:37 +0000 (11:52 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 20 Jul 2016 16:52:37 +0000 (11:52 -0500)
commitdaf2eca9a4bb32680cbf35945bb09cfd13be76a7
treefd387c71b6d1bd03e79e4e3403041c12a906a98atree
parentae7434f94a1bc66ee12474414985249a71881b6ccommit | diff
Print only instantiations that are in the unsat core when --proof is enabled.  Add option to minimize sygus solutions based on unsat core (disabled by default).
src/options/quantifiers_options diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history