From 46857bda6c6bb6db3481514c8cdee3ecbadb3301 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 16 Mar 2017 13:24:31 -0500 Subject: [PATCH] Support for SMT LIB 2.6 syntax declare-datatype and match. --- src/parser/smt2/Smt2.g | 134 +++++++++++++++++- test/regress/regress0/datatypes/Makefile.am | 3 +- .../regress0/datatypes/dt-color-2.6.smt2 | 15 ++ 3 files changed, 149 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/datatypes/dt-color-2.6.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4d884d894..bb7ac9fb8 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1359,6 +1359,8 @@ extendedCommand[CVC4::PtrCloser* cmd] * --smtlib2 compliance mode. */ : DECLARE_DATATYPES_2_5_TOK datatypes_2_5_DefCommand[false, cmd] | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd] + | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd] + | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd] | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | rewriterulesCommand[cmd] @@ -1526,10 +1528,24 @@ datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser* cmd] } ; +datatypeDefCommand[bool isCo, CVC4::PtrCloser* cmd] +@declarations { + std::vector dts; + std::string name; +} + : { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_UNDECLARED,SYM_SORT] LPAREN_TOK + { std::vector params; + dts.push_back(Datatype(name,params,isCo)); + } + ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+ + RPAREN_TOK + { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); } + ; + datatypesDefCommand[bool isCo, CVC4::PtrCloser* cmd] @declarations { std::vector dts; - std::vector types; std::string name; std::vector dnames; std::vector arities; @@ -1545,8 +1561,8 @@ datatypesDefCommand[bool isCo, CVC4::PtrCloser* cmd] //} else { // type = PARSER_STATE->mkSortConstructor(name, arity); //} - Debug("parser-dt") << "Datatype : " << name << ", arity = " << arity << std::endl; //types.push_back(type); + Debug("parser-dt") << "Datatype : " << name << ", arity = " << arity << std::endl; dnames.push_back(name); arities.push_back( arity ); } @@ -1793,12 +1809,15 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] std::string attr; Expr attexpr; std::vector patexprs; + std::vector patconds; std::hash_set names; std::vector< std::pair > binders; Type type; std::string s; bool isBuiltinOperator = false; bool readLetSort = false; + int match_vindex = -1; + std::vector match_ptypes; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -2029,6 +2048,115 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] term[expr, f2] RPAREN_TOK { PARSER_STATE->popScope(); } + | /* match expression */ + LPAREN_TOK MATCH_TOK term[expr, f2] { + if( !expr.getType().isDatatype() ){ + PARSER_STATE->parseError("Cannot match on non-datatype term."); + } + } + LPAREN_TOK + ( + /* match cases */ + LPAREN_TOK INDEX_TOK term[f, f2] { + if( match_vindex==-1 ){ + match_vindex = (int)patexprs.size(); + } + patexprs.push_back( f ); + patconds.push_back(MK_CONST(bool(true))); + } + RPAREN_TOK + | LPAREN_TOK LPAREN_TOK term[f, f2] { + args.clear(); + PARSER_STATE->pushScope(true); + //f should be a constructor + type = f.getType(); + Debug("parser-dt") << "Pattern head : " << f << " " << f.getType() << std::endl; + if( !type.isConstructor() ){ + PARSER_STATE->parseError("Pattern must be application of a constructor or a variable."); + } + //TODO + //if( Datatype::datatypeOf(f).isParametric() ){ + // type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType()); + //} + match_ptypes = ((ConstructorType)type).getArgTypes(); + } + //arguments + ( symbol[name,CHECK_NONE,SYM_VARIABLE] { + if( args.size()>=match_ptypes.size() ){ + PARSER_STATE->parseError("Too many arguments for pattern."); + } + //make of proper type + Expr arg = PARSER_STATE->mkBoundVar(name, match_ptypes[args.size()]); + args.push_back( arg ); + } + )* + RPAREN_TOK + term[f3, f2] { + const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)]; + if( args.size()!=dtc.getNumArgs() ){ + PARSER_STATE->parseError("Bad number of arguments for application of constructor in pattern."); + } + // build a lambda + std::vector largs; + largs.push_back( MK_EXPR( CVC4::Kind::BOUND_VAR_LIST, args ) ); + largs.push_back( f3 ); + std::vector< Expr > aargs; + aargs.push_back( MK_EXPR( CVC4::Kind::LAMBDA, largs ) ); + for( unsigned i=0; ipopScope(); } + | LPAREN_TOK symbol[name,CHECK_DECLARED,SYM_VARIABLE] { + f = PARSER_STATE->getVariable(name); + type = f.getType(); + if( !type.isConstructor() || !((ConstructorType)type).getArgTypes().empty() ){ + PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern."); + } + } + term[f3, f2] { + const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)]; + patexprs.push_back( f3 ); + patconds.push_back( MK_EXPR( CVC4::Kind::APPLY_TESTER, dtc.getTester(), expr ) ); + } + RPAREN_TOK + )+ + RPAREN_TOK RPAREN_TOK { + if( match_vindex==-1 ){ + const Datatype& dt = ((DatatypeType)expr.getType()).getDatatype(); + std::map< unsigned, bool > processed; + unsigned count = 0; + //ensure that all datatype constructors are matched (to ensure exhaustiveness) + for( unsigned i=0; i=dt.getNumConstructors() ){ + PARSER_STATE->parseError("Pattern is not legal for the head of a match."); + } + if( processed.find( curr_index )==processed.end() ){ + processed[curr_index] = true; + count++; + } + } + if( count!=dt.getNumConstructors() ){ + PARSER_STATE->parseError("Patterns are not exhaustive in a match construct."); + } + } + //now, make the ITE + int end_index = match_vindex==-1 ? patexprs.size()-1 : match_vindex; + bool first_time = true; + for( int index = end_index; index>=0; index-- ){ + if( first_time ){ + expr = patexprs[index]; + first_time = false; + }else{ + expr = MK_EXPR( CVC4::Kind::ITE, patconds[index], patexprs[index], expr ); + } + } + } | symbol[name,CHECK_NONE,SYM_VARIABLE] SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { std::string cname = name + "__Enum__" + name2; @@ -2900,6 +3028,7 @@ AS_TOK : 'as'; CONST_TOK : 'const'; // extended commands +DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() }? 'declare-codatatype'; DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() }? 'declare-datatype'; DECLARE_DATATYPES_2_5_TOK : { !PARSER_STATE->v2_6() }?'declare-datatypes'; DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() }?'declare-datatypes'; @@ -2907,6 +3036,7 @@ DECLARE_CODATATYPES_2_5_TOK : { !PARSER_STATE->v2_6() }?'declare-codatatypes'; DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() }?'declare-codatatypes'; PAR_TOK : { PARSER_STATE->v2_6() }?'par'; TESTER_TOK : { PARSER_STATE->v2_6() }?'is'; +MATCH_TOK : { PARSER_STATE->v2_6() }?'match'; GET_MODEL_TOK : 'get-model'; ECHO_TOK : 'echo'; REWRITE_RULE_TOK : 'assert-rewrite'; diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 90d6b4716..24c289650 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -77,7 +77,8 @@ TESTS = \ example-dailler-min.smt2 \ dt-2.6.smt2 \ dt-sel-2.6.smt2 \ - dt-param-2.6.smt2 + dt-param-2.6.smt2 \ + dt-color-2.6.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/dt-color-2.6.smt2 b/test/regress/regress0/datatypes/dt-color-2.6.smt2 new file mode 100644 index 000000000..a44219954 --- /dev/null +++ b/test/regress/regress0/datatypes/dt-color-2.6.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --lang=smt2.6 +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatype Color ( ( red ) ( green ) ( blue ) )) + +(declare-fun a () Color) +(declare-fun b () Color) +(declare-fun c () Color) +(declare-fun d () Color) + +(assert (or (distinct a b c d) + (< (match a ((red 5) (green 3) (blue 2))) 0))) + +(check-sat) -- 2.30.2