summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/Makefile.am
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-11-13 11:53:33 -0600
committerGitHub <noreply@github.com>2017-11-13 11:53:33 -0600
commit8c04e55f16faebbe552752e2ff76ffda5a9fb21f (patch)
tree41fd1d9844b0d88bd9c4da15dbb5fdd6c6165628 /test/regress/regress0/sygus/Makefile.am
parent6e9f70f5bc59a57cbfdcf0f149265652461fcf2e (diff)
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
Diffstat (limited to 'test/regress/regress0/sygus/Makefile.am')
-rw-r--r--test/regress/regress0/sygus/Makefile.am3
1 files changed, 3 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 3c118a007..b40ee845f 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -67,6 +67,9 @@ TESTS = commutative.sy \
triv-type-mismatch-si.sy \
nia-max-square-ns.sy \
strings-concat-3-args.sy \
+ process-10-vars.sy \
+ process-10-vars-2fun.sy \
+ inv-unused.sy \
ccp16.lus.sy
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback