projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2e4eba4) | patch
Use sygus to synthesize/verify rewrite rules (#1547)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 1 Feb 2018 18:13:54 +0000 (12:13 -0600)
committerGitHub <noreply@github.com>
Thu, 1 Feb 2018 18:13:54 +0000 (12:13 -0600)
commitdbd1797f64216ba9eb598579de27cc45814e1db4
treeda47015c59c728ada2b7034900267609a00ecb12tree
parent2e4eba43ffa4dd938b7e1153cc42216a42e8ce04commit | diff
Use sygus to synthesize/verify rewrite rules (#1547)
src/Makefile.am diff | blob | history
src/options/quantifiers_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.h diff | blob | history
src/theory/quantifiers/ce_guided_conjecture.cpp diff | blob | history
src/theory/quantifiers/ce_guided_conjecture.h diff | blob | history
src/theory/quantifiers/sygus_sampler.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus_sampler.h [new file with mode: 0644] blob