Fix sygus quantifier elimination preprocess for multiple functions (#5130)

The option --sygus-qe-preproc performs quantifier elimination to coerce certain synthesis conjectures to be single invocation. This technique was broken when multiple synthesis functions were present. This fixes the issue and adds a regression where --sygus-qe-preproc enables a benchmark to be quickly solved.

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 95f1acb25679dd11ff73d0f0072426f214b13b9f..5358a0aff80a99b0b4fd04b7e0dc3305c37f2192 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -184,13 +184,19 @@ void SynthEngine::assignConjecture(Node q)
       for (unsigned i = 0, size = all_vars.size(); i < size; i++)
       {
         Node v = all_vars[i];
-        if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
+        if (std::find(funcs0.begin(), funcs0.end(), v) != funcs0.end())
+        {
+          Trace("cegqi-qep") << "- fun var: " << v << std::endl;
+        }
+        else if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
         {
           qe_vars.push_back(v);
+          Trace("cegqi-qep") << "- qe var: " << v << std::endl;
         }
         else
         {
           nqe_vars.push_back(v);
+          Trace("cegqi-qep") << "- non qe var: " << v << std::endl;
         }
       }
       std::vector<Node> orig;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8273eb30540f6cac9c39e9a588fed4b7722965d0..a5ed6dd09fca3245fa29a2d42f503a92773db605 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2023,6 +2023,7 @@ set(regress_1_tests
   regress1/sygus/rec-fun-while-infinite.sy
   regress1/sygus/re-concat.sy
   regress1/sygus/repair-const-rl.sy
+  regress1/sygus/replicate-mod.sy
   regress1/sygus/rex-strings-alarm.sy
   regress1/sygus/sets-pred-test.sy
   regress1/sygus/simple-regexp.sy

diff --git a/test/regress/regress1/sygus/replicate-mod.sy b/test/regress/regress1/sygus/replicate-mod.sy
new file mode 100644 (file)
index 0000000..fbe3b7d
--- /dev/null
+++ b/test/regress/regress1/sygus/replicate-mod.sy
@@ -0,0 +1,181 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-qe-preproc --sygus-si=all  --sygus-out=status
+(set-logic LIA)
+(synth-fun fr0 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr1 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr10 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr11 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr12 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr13 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr14 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr15 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr16 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr17 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr18 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr19 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr2 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr20 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr21 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr22 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr23 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr24 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr25 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr26 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr27 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr28 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr29 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr3 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr30 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr31 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr32 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr33 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr34 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr35 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr36 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr4 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr5 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr6 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr7 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr8 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr9 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m0 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m1 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m10 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m11 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m12 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m13 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m14 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m15 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m16 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m17 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m2 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m3 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m4 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m5 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m6 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m7 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m8 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m9 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun p0 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p1 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p2 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p3 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p4 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p5 ((_v Int) (n Int) (x Int)) Int)
+(declare-var n Int)
+(declare-var x Int)
+(declare-var x10 Int)
+(declare-var x11 Int)
+(declare-var x14 Int)
+(declare-var x15 Int)
+(declare-var x2 Int)
+(declare-var x3 Int)
+(declare-var x6 Int)
+(declare-var x7 Int)
+(declare-var _v Int)
+(constraint (=> (>= n 0) (and (and (and (>= (m2 _v n x) 0) (>= (m4 _v n x) 0)) (>= (m5 _v n x) 0)) (= (m2 _v n x) (+ (m4 _v n x) (m5 _v n x))))))
+(constraint (=> (>= n 0) (and (and (and (>= (fr7 _v n x) 0) (>= (fr9 _v n x) 0)) (>= (fr10 _v n x) 0)) (= (fr7 _v n x) (+ (fr9 _v n x) (fr10 _v n x))))))
+(constraint (=> (>= n 0) (and (and (and (>= (fr5 _v n x) 0) (>= (fr7 _v n x) 0)) (>= (fr8 _v n x) 0)) (= (fr5 _v n x) (+ (fr7 _v n x) (fr8 _v n x))))))
+(constraint (=> (>= n 0) (and (and (and (>= (m0 _v n x) 0) (>= (m2 _v n x) 0)) (>= (m3 _v n x) 0)) (= (m0 _v n x) (+ (m2 _v n x) (m3 _v n x))))))
+(constraint (=> (>= n 0) (and (and (and (>= (fr3 _v n x) 0) (>= (fr5 _v n x) 0)) (>= (fr6 _v n x) 0)) (= (fr3 _v n x) (+ (fr5 _v n x) (fr6 _v n x))))))
+(constraint (=> (>= n 0) (and (and (and (>= (fr2 _v n x) 0) (>= (fr3 _v n x) 0)) (>= (fr4 _v n x) 0)) (= (fr2 _v n x) (+ (fr3 _v n x) (fr4 _v n x))))))
+(constraint (=> (>= n 0) (and (and (and (and (and (and (= (+ (+ (+ 0 (p0 _v n x)) (fr0 _v n x)) 0) (+ (+ (+ 0 0) (fr2 _v n x)) 0)) (>= (fr0 _v n x) 0)) (>= (fr2 _v n x) 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)) (>= 0 0))))
+(constraint (=> (>= n 0) (and (and (and (>= 1 0) (>= (m0 _v n x) 0)) (>= (m1 _v n x) 0)) (= 1 (+ (m0 _v n x) (m1 _v n x))))))
+(constraint (=> (and (= _v x) (>= n 0)) (and (and (and (>= n 0) (>= (p0 _v n x) 0)) (>= (p1 _v n x) 0)) (= n (+ (p0 _v n x) (p1 _v n x))))))
+(constraint (=> (>= n 0) (and (and (and (>= 0 0) (>= (fr0 _v n x) 0)) (>= (fr1 _v n x) 0)) (= 0 (+ (fr0 _v n x) (fr1 _v n x))))))
+(constraint (=> (and (= _v n) (>= n 0)) (>= 0 (+ (p2 _v n x) (- (+ (fr8 _v n x) 0))))))
+(constraint (=> (>= n 0) (>= (p2 _v n x) 0)))
+(constraint (=> (and (= _v 0) (>= n 0)) (>= 0 (+ (p2 _v n x) (- (+ (fr4 _v n x) 0))))))
+(constraint (=> (and (= true (<= n 0)) (>= n 0)) (>= (p3 _v n x) 0)))
+(constraint (=> (and (= true (<= n 0)) (>= n 0)) (and (and (and (and (and (and (= (+ (+ (+ 0 (p1 _v n x)) (fr1 _v n x)) 0) (+ (+ (+ 0 0) (fr11 _v n x)) 0)) (>= (fr1 _v n x) 0)) (>= (fr11 _v n x) 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)) (>= 0 0))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (>= (p4 _v n x) 0)))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (m6 _v n x) 0) (>= (m8 _v n x) 0)) (>= (m9 _v n x) 0)) (= (m6 _v n x) (+ (m8 _v n x) (m9 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr17 _v n x) 0) (>= (fr19 _v n x) 0)) (>= (fr20 _v n x) 0)) (= (fr17 _v n x) (+ (fr19 _v n x) (fr20 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr15 _v n x) 0) (>= (fr17 _v n x) 0)) (>= (fr18 _v n x) 0)) (= (fr15 _v n x) (+ (fr17 _v n x) (fr18 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (m1 _v n x) 0) (>= (m6 _v n x) 0)) (>= (m7 _v n x) 0)) (= (m1 _v n x) (+ (m6 _v n x) (m7 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr13 _v n x) 0) (>= (fr15 _v n x) 0)) (>= (fr16 _v n x) 0)) (= (fr13 _v n x) (+ (fr15 _v n x) (fr16 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr12 _v n x) 0) (>= (fr13 _v n x) 0)) (>= (fr14 _v n x) 0)) (= (fr12 _v n x) (+ (fr13 _v n x) (fr14 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (and (and (and (= (+ (+ (+ 0 (p1 _v n x)) (fr1 _v n x)) 0) (+ (+ (+ 0 0) (fr12 _v n x)) 0)) (>= (fr1 _v n x) 0)) (>= (fr12 _v n x) 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)) (>= 0 0))))
+(constraint (=> (and (and (= false (<= n 0)) (= _v x)) (>= n 0)) (>= 0 (+ (p4 _v n x) (- (+ (fr18 _v n x) 0))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (>= 0 (- (+ (fr14 _v n x) 0)))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (>= (p5 _v n x) (p4 _v n x))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (>= (p5 _v n x) 0)))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (m10 _v n x) 0) (>= (m12 _v n x) 0)) (>= (m13 _v n x) 0)) (= (m10 _v n x) (+ (m12 _v n x) (m13 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr25 _v n x) 0) (>= (fr27 _v n x) 0)) (>= (fr28 _v n x) 0)) (= (fr25 _v n x) (+ (fr27 _v n x) (fr28 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr23 _v n x) 0) (>= (fr25 _v n x) 0)) (>= (fr26 _v n x) 0)) (= (fr23 _v n x) (+ (fr25 _v n x) (fr26 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (m7 _v n x) 0) (>= (m10 _v n x) 0)) (>= (m11 _v n x) 0)) (= (m7 _v n x) (+ (m10 _v n x) (m11 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr21 _v n x) 0) (>= (fr23 _v n x) 0)) (>= (fr24 _v n x) 0)) (= (fr21 _v n x) (+ (fr23 _v n x) (fr24 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (- (fr16 _v n x) 1) 0) (>= (fr21 _v n x) 0)) (>= (fr22 _v n x) 0)) (= (- (fr16 _v n x) 1) (+ (fr21 _v n x) (fr22 _v n x))))))
+(constraint (=> false (>= 0 (- (+ (fr26 _v n x) 0)))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (m14 _v n x) 0) (>= (m16 _v n x) 0)) (>= (m17 _v n x) 0)) (= (m14 _v n x) (+ (m16 _v n x) (m17 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr33 _v n x) 0) (>= (fr35 _v n x) 0)) (>= (fr36 _v n x) 0)) (= (fr33 _v n x) (+ (fr35 _v n x) (fr36 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr31 _v n x) 0) (>= (fr33 _v n x) 0)) (>= (fr34 _v n x) 0)) (= (fr31 _v n x) (+ (fr33 _v n x) (fr34 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (m13 _v n x) 0) (>= (m14 _v n x) 0)) (>= (m15 _v n x) 0)) (= (m13 _v n x) (+ (m14 _v n x) (m15 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr29 _v n x) 0) (>= (fr31 _v n x) 0)) (>= (fr32 _v n x) 0)) (= (fr29 _v n x) (+ (fr31 _v n x) (fr32 _v n x))))))
+(constraint (=> (and (= false (<= n 0)) (>= n 0)) (and (and (and (>= (fr28 _v n x) 0) (>= (fr29 _v n x) 0)) (>= (fr30 _v n x) 0)) (= (fr28 _v n x) (+ (fr29 _v n x) (fr30 _v n x))))))
+(constraint (=> (and (and (= false (<= n 0)) (= _v n)) (>= n 0)) (>= 0 (- (+ (fr34 _v n x) 0)))))
+(constraint (=> false (>= 0 (- (+ (fr26 _v n x) 0)))))
+(constraint (=> (and (and (= false (<= n 0)) (= _v 1)) (>= n 0)) (>= 0 (- (+ (fr30 _v n x) 0)))))
+(constraint (=> (and (and (= false (<= n 0)) (= _v (- n 1))) (>= n 0)) (>= 0 (- (+ (fr26 _v n x) 0)))))
+(constraint (=> (and (and (= false (<= n 0)) (= x10 (- n 1))) (>= n 0)) (>= 0 (- (+ (fr14 _v n x) 0)))))
+(constraint (=> (and (and (= false (<= n 0)) (= x10 (- n 1))) (>= n 0)) (>= (p5 _v n x) (p4 _v n x))))
+(constraint (=> (and (and (and (= false (<= n 0)) (= x10 (- n 1))) (= _v x)) (>= n 0)) (>= 0 (+ (p5 _v n x) (+ x10 (- (+ (fr22 _v n x) 0)))))))
+(constraint (=> (and (and (= false (<= n 0)) (= x10 (- n 1))) (>= n 0)) (>= 0 (- (+ (fr14 _v n x) 0)))))
+(constraint (=> (and (and (= false (<= n 0)) (= x10 (- n 1))) (>= n 0)) (>= (p5 _v n x) (p4 _v n x))))
+(constraint (=> true (and (and (and (>= 0 0) (>= 0 0)) (>= 0 0)) (= 0 (+ 0 0)))))
+(check-synth)