From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 24 Apr 2017 15:14:19 +0000 (-0500)
Subject: Fix parsing selectors for nullary constructors in smtlib 2.6 format.
X-Git-Tag: cvc5-1.0.0~5818
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bcfe5eed9c79e7bd3c32b5ce8e96a54bcff4099f;p=cvc5.git

Fix parsing selectors for nullary constructors in smtlib 2.6 format.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 740e35ba4..d73a60ed1 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2538,6 +2538,10 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind]
     | FP_TO_SBV_TOK m=INTEGER_LITERAL
       { op = MK_CONST(FloatingPointToSBV(AntlrInput::tokenToUnsigned($m))); }
     | TESTER_TOK term[expr, expr2] { 
+        if( expr.getKind()==kind::APPLY_CONSTRUCTOR ){
+          //for nullary constructors, must get the operator
+          expr = expr.getOperator();
+        }
         if( !expr.getType().isConstructor() ){
           PARSER_STATE->parseError("Bad syntax for test (_ is X), X must be a constructor.");
         }
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index caf1fc61c..b437f1878 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -80,7 +80,8 @@ TESTS =	\
 	dt-param-2.6.smt2 \
 	dt-color-2.6.smt2 \
 	dt-match-pat-param-2.6.smt2 \
-	tuple-no-clash.cvc
+	tuple-no-clash.cvc \
+	jsat-2.6.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/jsat-2.6.smt2 b/test/regress/regress0/datatypes/jsat-2.6.smt2
new file mode 100644
index 000000000..7e7fe4f49
--- /dev/null
+++ b/test/regress/regress0/datatypes/jsat-2.6.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --lang=smt2.6
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))
+((cons (car tree) (cdr list)) (null))
+((node (children list)) (leaf (data nat)))
+))
+(declare-fun x1 () nat)
+(declare-fun x2 () nat)
+(declare-fun x3 () nat)
+(declare-fun x4 () nat)
+(declare-fun x5 () nat)
+(declare-fun x6 () list)
+(declare-fun x7 () list)
+(declare-fun x8 () list)
+(declare-fun x9 () list)
+(declare-fun x10 () list)
+(declare-fun x11 () tree)
+(declare-fun x12 () tree)
+(declare-fun x13 () tree)
+(declare-fun x14 () tree)
+(declare-fun x15 () tree)
+
+(assert (and (and (= x9 x7) ((_ is node) x11)) (not ((_ is zero) x5))))
+(check-sat)
+
+