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

4 files changed, 68 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
 
 
diff --git a/test/regress/regress0/sygus/inv-unused.sy b/test/regress/regress0/sygus/inv-unused.sy
new file mode 100644
index 000000000..91ba95d39
--- /dev/null
+++ b/test/regress/regress0/sygus/inv-unused.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+(synth-inv inv-f ((x Int) (y Int) (b Bool)))
+(declare-primed-var x Int)
+(declare-primed-var y Int)
+(declare-primed-var b Bool)
+(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (>= x 5) (<= x 9)))
+(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (= x! (+ x 1)))
+(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (> x 0))
+(inv-constraint inv-f pre-f trans-f post-f)
+; invariant does not depend on arguments y and b
+(check-synth)
diff --git a/test/regress/regress0/sygus/process-10-vars-2fun.sy b/test/regress/regress0/sygus/process-10-vars-2fun.sy
new file mode 100644
index 000000000..00340030f
--- /dev/null
+++ b/test/regress/regress0/sygus/process-10-vars-2fun.sy
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+; EXPECT: unsat
+(set-logic LIA)
+
+(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int)
+
+(synth-fun g ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int)
+
+(declare-var x1 Int)
+(declare-var x2 Int)
+(declare-var x3 Int)
+(declare-var x4 Int)
+(declare-var x5 Int)
+(declare-var x6 Int)
+(declare-var x7 Int)
+(declare-var x8 Int)
+(declare-var x9 Int)
+(declare-var x10 Int)
+
+; should be able to determine that arguments 1...6, 8...10 are irrelevant for f
+; and arguments 1...3, 5...10 are irrelevant for g
+
+(constraint (>= (f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x7 x7 x7)))
+
+(constraint (>= (g x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x4 x4 x4)))
+
+(check-synth)
+
diff --git a/test/regress/regress0/sygus/process-10-vars.sy b/test/regress/regress0/sygus/process-10-vars.sy
new file mode 100644
index 000000000..523abd70d
--- /dev/null
+++ b/test/regress/regress0/sygus/process-10-vars.sy
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+; EXPECT: unsat
+(set-logic LIA)
+
+(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int)
+
+
+(declare-var x1 Int)
+(declare-var x2 Int)
+(declare-var x3 Int)
+(declare-var x4 Int)
+(declare-var x5 Int)
+(declare-var x6 Int)
+(declare-var x7 Int)
+(declare-var x8 Int)
+(declare-var x9 Int)
+(declare-var x10 Int)
+
+; should be able to determine that arguments 1...6, 8...10 are irrelevant for f
+
+(constraint (>= (f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x7 x7 x7)))
+
+(check-synth)
+