projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 18d2fd5) | patch
Work on new approach for sygus involving conditional solutions. Refactoring of sygus...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 22 Mar 2017 13:52:42 +0000 (08:52 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 22 Mar 2017 14:00:56 +0000 (09:00 -0500)
commit620ebbaf88f07abc36399499cfa6dfef8c3369d9
treefe18fdae38b0fcd64ea9d3014a3dd7846b6c7202tree
parent18d2fd549d5058a6ea3ee782568bbc3ce00189eacommit | diff
Work on new approach for sygus involving conditional solutions. Refactoring of sygus solver. Bug fix for sygus solution reconstruction.
src/expr/datatype.cpp diff | blob | history
src/expr/datatype.h diff | blob | history
src/options/quantifiers_options diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.h diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv_sol.cpp diff | blob | history