From 6cb2e5743bd886115124256c2a3ad689a5b822a2 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 9 Nov 2020 07:42:03 -0600
Subject: [PATCH] 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.
---
 src/theory/datatypes/inference_manager.cpp | 12 ++++---
 test/regress/CMakeLists.txt                |  1 +
 test/regress/regress2/sygus/policyM.sy     | 41 ++++++++++++++++++++++
 3 files changed, 50 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress2/sygus/policyM.sy

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index df0f38c0b..ddff97283 100644
--- 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 c6c55d847..58a43895e 100644
--- 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
index 000000000..0e9b33148
--- /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)
-- 
2.30.2