Fix sygus datatype parsing in sygus v1 format (#3113)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index af374274b5e4da588ab9d9838a5c1b2947383256..278f2bdfd1d529805970a17f96124a247d9939d6 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1088,7 +1088,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
         }
       }
       Kind sk = sop.getKind() != kind::BUILTIN
-                    ? kind::APPLY_UF
+                    ? getKindForFunction(sop)
                     : getExprManager()->operatorToKind(sop);
       Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
       Expr e = getExprManager()->mkExpr( sk, children );

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 29f31960c0d409378b051ce50128b07733f972b4..659071fc36cdda0bf1fe07b0a99baead7ad12692 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -879,6 +879,7 @@ set(regress_0_tests
   regress0/sygus/check-generic-red.sy
   regress0/sygus/const-var-test.sy
   regress0/sygus/dt-no-syntax.sy
+  regress0/sygus/dt-sel-parse1.sy
   regress0/sygus/hd-05-d1-prog-nogrammar.sy
   regress0/sygus/inv-different-var-order.sy
   regress0/sygus/let-ringer.sy

diff --git a/test/regress/regress0/sygus/dt-sel-parse1.sy b/test/regress/regress0/sygus/dt-sel-parse1.sy
new file mode 100644 (file)
index 0000000..52edb32
--- /dev/null
+++ b/test/regress/regress0/sygus/dt-sel-parse1.sy
@@ -0,0 +1,48 @@
+; COMMAND-LINE: --sygus-out=status
+; EXPECT: unsat
+(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 max ((x Int) (y Int)) Int
+ (ite (>= x y) x y)
+)
+
+(define-fun min ((x Int) (y Int)) Int
+ (ite (<= x y) x y)
+)
+
+; provide synthesis template 
+(synth-fun f ((secret Ship) (prior ShipRange) (response Bool)) ShipRange
+(
+     (Start ShipRange ((ite B SR SR)))
+     (B Bool (response))
+     (SR ShipRange ((ShipRange IR LR) prior))
+     (IR IntRange ((IntRange I I) (shipCapacityD SR)))
+     (LR LocRange ((LocRange IR IR) (shipLocD SR)))
+     (I Int ((lower IR) (upper IR) 
+             (max I (lower (shipCapacityD SR))) 
+             (min I I) 50 51))
+ )    
+)
+
+(declare-var secret Ship)
+(declare-var prior ShipRange)
+(declare-var response Bool)
+
+(constraint true)
+
+(check-synth)