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 740e35ba4f818469b397223f8a7b409a39c474fd..d73a60ed1289d3f41354d8b9fb31d24592024ae3 100644 (file)
--- 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 caf1fc61c8dfeb7da97aed605b02dabad0c6cf40..b437f1878f7f9a9412f32edfefee83c8a78cf30f 100644 (file)
--- 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 (file)
index 0000000..7e7fe4f
--- /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)
+
+