projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a236ade) | patch
Synthesize candidate-rewrites from standard inputs (#1918)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 27 Jun 2018 19:12:17 +0000 (14:12 -0500)
committerGitHub <noreply@github.com>
Wed, 27 Jun 2018 19:12:17 +0000 (14:12 -0500)
commitd6c7967cfc7a9f8530f0de50f12f99bfc5f93da7
tree2741c23c2cc42c065dc2aa573e0983e8f10823c1tree
parenta236ade3242599d4916fd9ee676c2c68c7c004b1commit | diff
Synthesize candidate-rewrites from standard inputs (#1918)
14 files changed:
src/Makefile.am diff | blob | history
src/options/smt_options.toml diff | blob | history
src/preprocessing/passes/synth_rew_rules.cpp [new file with mode: 0644] blob
src/preprocessing/passes/synth_rew_rules.h [new file with mode: 0644] blob
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/candidate_rewrite_database.cpp diff | blob | history
src/theory/quantifiers/candidate_rewrite_database.h diff | blob | history
src/theory/quantifiers/dynamic_rewrite.cpp diff | blob | history
src/theory/quantifiers/dynamic_rewrite.h diff | blob | history
src/theory/quantifiers/sygus/ce_guided_conjecture.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.h diff | blob | history
src/theory/quantifiers/sygus_sampler.cpp diff | blob | history
src/theory/quantifiers/sygus_sampler.h diff | blob | history