From bcfe5eed9c79e7bd3c32b5ce8e96a54bcff4099f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 24 Apr 2017 10:14:19 -0500 Subject: [PATCH] Fix parsing selectors for nullary constructors in smtlib 2.6 format. --- src/parser/smt2/Smt2.g | 4 +++ test/regress/regress0/datatypes/Makefile.am | 3 +- test/regress/regress0/datatypes/jsat-2.6.smt2 | 28 +++++++++++++++++++ 3 files changed, 34 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/datatypes/jsat-2.6.smt2 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) + + -- 2.30.2