Argument Relevance for Synthesis Conjectures (#1311)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 13 Nov 2017 17:53:33 +0000 (11:53 -0600)
committerGitHub <noreply@github.com>
Mon, 13 Nov 2017 17:53:33 +0000 (11:53 -0600)
commit8c04e55f16faebbe552752e2ff76ffda5a9fb21f
tree41fd1d9844b0d88bd9c4da15dbb5fdd6c6165628
parent6e9f70f5bc59a57cbfdcf0f149265652461fcf2e
Argument Relevance for Synthesis Conjectures (#1311)

* Initial work on conjecture-specific symmetry breaking.

* More infrastructure, working on process term.

* Flattening.

* Process defs

* More setup

* Fixes.

* Sketching

* Generalize to inference of argument definitions.

* More, separate conjunct processing per synth function.

* Single occurrence variables.

* Assign relevance.

* Document, connecting.

* Connecting to grammar construction.

* Enabled, add regressions.

* Fix regressions.

* Clang format.

* Add regress1, minor.

* Fix

* Two passes.

* Fix

* Note

* Improve check match, make single var occurrence more conservative.

* Add regression.

* Clang format

* Minor comments

* Update regression to new option.

* Undo grammar cons changes.

* Enable irrelevant args.

* Improvements.

* Format

* Minor
12 files changed:
src/theory/quantifiers/ce_guided_conjecture.cpp
src/theory/quantifiers/ce_guided_conjecture.h
src/theory/quantifiers/ce_guided_pbe.h
src/theory/quantifiers/sygus_grammar_cons.cpp
src/theory/quantifiers/sygus_process_conj.cpp
src/theory/quantifiers/sygus_process_conj.h
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/inv-unused.sy [new file with mode: 0644]
test/regress/regress0/sygus/process-10-vars-2fun.sy [new file with mode: 0644]
test/regress/regress0/sygus/process-10-vars.sy [new file with mode: 0644]
test/regress/regress1/sygus/Makefile.am
test/regress/regress1/sygus/process-arg-invariance.sy [new file with mode: 0644]