projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d4a7b0c) | patch
Do ITE term bookkeeping when solving Sygus inputs. Add missing script from Sygus...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 27 Aug 2015 15:27:57 +0000 (17:27 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 27 Aug 2015 15:27:57 +0000 (17:27 +0200)
commit0ddf1b9c74f2b2a78e0960b710c2edbdc5f8d02d
tree523a7c7ec9bfefd4297c5d8f56ef0ff474045d73tree
parentd4a7b0cf0500e971c9c01e7628f3c1b567715059commit | diff
Do ITE term bookkeeping when solving Sygus inputs.  Add missing script from Sygus comp 2015. Fix bug 665 regarding strings rewriter for contains.
contrib/run-script-syguscomp2015 [new file with mode: 0644] blob
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history