From 7de5f26ca35f6b3b11dc8a7465f7a15e5d0d2e50 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 19 Jul 2019 12:39:07 -0400
Subject: [PATCH] Fixes for sygus with datatypes (#3103)

---
 src/printer/smt2/smt2_printer.cpp             | 17 ++---
 .../quantifiers/sygus/term_database_sygus.cpp |  7 +-
 test/regress/CMakeLists.txt                   |  1 +
 test/regress/regress1/sygus/error1-dt.sy      | 71 +++++++++++++++++++
 4 files changed, 85 insertions(+), 11 deletions(-)
 create mode 100644 test/regress/regress1/sygus/error1-dt.sy

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9b34b1d7c..163c8acad 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1476,18 +1476,15 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
       return;
     }
   }
+  Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
+  if (!p.isNull())
+  {
+    out << p;
+  }
   else
   {
-    Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
-    if (!p.isNull())
-    {
-      out << p;
-    }
-    else
-    {
-      // cannot convert term to analog, print original
-      out << n;
-    }
+    // cannot convert term to analog, print original
+    out << n;
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 01d08dad8..af8c93e45 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -874,8 +874,13 @@ void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, un
       // do not recurse to non-datatype types
       return;
     }
+    const Datatype& dt = tn.getDatatype();
+    if( !dt.isSygus() )
+    {
+      // do not recurse to non-sygus datatype types
+      return;
+    }
     d_min_type_depth[root_tn][tn] = type_depth;
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
     //compute for connected types
     for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
       for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index af6a9b839..29f31960c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1641,6 +1641,7 @@ set(regress_1_tests
   regress1/sygus/double.sy
   regress1/sygus/dt-test-ns.sy
   regress1/sygus/dup-op.sy
+  regress1/sygus/error1-dt.sy
   regress1/sygus/extract.sy
   regress1/sygus/fg_polynomial3.sy
   regress1/sygus/find_sc_bvult_bvnot.sy
diff --git a/test/regress/regress1/sygus/error1-dt.sy b/test/regress/regress1/sygus/error1-dt.sy
new file mode 100644
index 000000000..67f73aded
--- /dev/null
+++ b/test/regress/regress1/sygus/error1-dt.sy
@@ -0,0 +1,71 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --cegqi-si=none --sygus-active-gen=enum
+
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes ((IntRange 0)) 
+   (((IntRange (lower Int) (upper Int)))))
+
+(declare-datatypes ((Loc 0)) 
+   (((Loc (x Int) (y Int)))))
+
+(declare-datatypes ((LocRange 0)) 
+   (((LocRange (xD IntRange) (yD IntRange)))))
+
+(declare-datatypes ((Ship 0)) 
+   (((Ship (shipCapacity Int) (shipLoc Loc)))))
+
+(declare-datatypes ((ShipRange 0)) 
+   (((ShipRange (shipCapacityD IntRange) (shipLocD LocRange)))))
+
+(define-fun betweenInt ((x Int) (r IntRange)) Bool
+    (and (< (lower r) x) (< x (upper r)))
+)
+
+(define-fun betweenLoc ((l Loc) (lr LocRange)) Bool
+    (and (betweenInt (x l) (xD lr)) (betweenInt (y l) (yD lr)))
+)
+
+(define-fun subsetInt ((r1 IntRange) (r2 IntRange)) Bool
+    (and (>= (lower r1) (lower r2)) (<= (upper r1) (upper r2)))
+)
+
+(define-fun betweenShip ((s Ship) (sr ShipRange)) Bool
+    (and (betweenInt (shipCapacity s) (shipCapacityD sr)) (betweenLoc (shipLoc s) (shipLocD sr)))
+)
+
+(define-fun atLeast ((s Ship)) Bool
+    (> (shipCapacity s) 50)
+)
+
+(define-fun subsetLoc ((s1 LocRange) (s2 LocRange)) Bool
+    (and (subsetInt (xD s1) (xD s2)) (subsetInt (yD s1) (yD s2)))
+)
+
+(define-fun subsetShip ((s1 ShipRange) (s2 ShipRange)) Bool
+    (and (subsetInt (shipCapacityD s1) (shipCapacityD s2)) (subsetLoc (shipLocD s1) (shipLocD s2)))
+)
+
+(define-fun max ((x Int) (y Int)) Int
+ (ite (>= x y) x y)
+)
+
+(define-fun min ((x Int) (y Int)) Int
+ (ite (<= x y) x y)
+)
+
+
+(synth-fun f ((secret Ship) (prior ShipRange) (response Bool)) ShipRange)
+
+(declare-var secret Ship)
+(declare-var prior ShipRange)
+(declare-var response Bool)
+
+(constraint 
+  (=> (betweenShip secret (f secret prior response)) 
+          (= response 
+             (and (atLeast secret) 
+                  (subsetShip (f secret prior response) prior))))
+)
+
+(check-synth)
-- 
2.30.2