Do not regress explanations of datatype lemmas (#5376)

This modifies datatypes to not regress explanations for lemmas. This avoids segfaults in some corner cases of sygus (see attached) and leads to slightly better performance on Facebook verification benchmarks.

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index df0f38c0b357167ee908ec0e7a4ea85d6ad6a82e..ddff9728353684c1a74bfae6018633169c37abd1 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -88,13 +88,17 @@ bool InferenceManager::processDtInference(Node conc,
                           << std::endl;
   if (asLemma)
   {
-    // send it as an (explained) lemma
-    std::vector<Node> expv;
+    // send it as a lemma
+    Node lem;
     if (!exp.isNull() && !exp.isConst())
     {
-      expv.push_back(exp);
+      lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc);
     }
-    if (!lemmaExp(conc, expv, {}))
+    else
+    {
+      lem = conc;
+    }
+    if (!lemma(lem))
     {
       Trace("dt-lemma-debug") << "...duplicate lemma" << std::endl;
       return false;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c6c55d8478b13c3ed4ca505407105d1e19de7529..58a43895e082b94137b2bd0fc95d6ac9ac2c7b16 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2201,6 +2201,7 @@ set(regress_2_tests
   regress2/sygus/nia-max-square.sy
   regress2/sygus/no-syntax-test-no-si.sy
   regress2/sygus/pbe_bvurem.sy
+  regress2/sygus/policyM.sy
   regress2/sygus/process-10-vars-2fun.sy
   regress2/sygus/process-arg-invariance.sy
   regress2/sygus/real-grammar-neg.sy

diff --git a/test/regress/regress2/sygus/policyM.sy b/test/regress/regress2/sygus/policyM.sy
new file mode 100644 (file)
index 0000000..0e9b331
--- /dev/null
+++ b/test/regress/regress2/sygus/policyM.sy
@@ -0,0 +1,41 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
+(set-logic ALL)
+
+(declare-datatype Pair ((pair (pmin Int) (pmax Int))))
+
+(define-fun wf ((p Pair)) Bool
+  (<= (pmin p) (pmax p)))
+(define-fun a ((p Pair) (q Pair)) Bool
+  (< (pmax p) (pmin q)))
+(define-fun intMax ((x Int) (y Int)) Int
+  (ite (>= x y) x y))
+(define-fun intMin ((x Int) (y Int)) Int
+  (ite (>= x y) y x))
+(define-fun midpoint ((x Int) (y Int)) Int
+  (div (+ x y) 2))
+
+(synth-fun pW ((p Pair) (q Pair)) Pair
+  ((StartPair Pair) (StartInt Int)) (
+  (StartPair Pair ((pair StartInt StartInt)))
+  (StartInt Int ((pmin p) (pmax p) (pmin q) (pmax q) (intMax StartInt StartInt) (intMin StartInt StartInt) (midpoint StartInt StartInt)))
+))
+(synth-fun pL ((p Pair) (q Pair)) Pair
+  ((StartPair Pair) (StartInt Int)) (
+  (StartPair Pair ((pair StartInt StartInt)))
+  (StartInt Int ((+ StartInt StartInt) 0 1 (pmin p) (pmax p) (pmin q) (pmax q) (intMax StartInt StartInt) (intMin StartInt StartInt) (midpoint StartInt StartInt)))
+))
+
+(declare-var p Pair)
+(declare-var q Pair)
+(declare-var r Pair)
+
+(constraint (=> (and (wf p) (wf q)) (wf (pW p q))))
+(constraint (=> (and (wf p) (wf q)) (wf (pL p q))))
+
+(constraint (=> (and (wf p) (wf q) (wf r) (a p r)) (a (pW p q) r)))
+(constraint (=> (and (wf p) (wf q) (wf r) (a p r)) (a p (pL r q))))
+
+(constraint (=> (and (wf p) (wf q)) (not (a (pL q p) (pW p q)))))
+
+(check-synth)