From: Andrew Reynolds Date: Tue, 17 Jan 2012 18:15:03 +0000 (+0000) Subject: updates to smt2 parser to support datatypes, minor updates to datatypes theory/rewrit... X-Git-Tag: cvc5-1.0.0~8352 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b0ac192fd4e8b1ff707e0e3cc9df92ab385f1fd4;p=cvc5.git updates to smt2 parser to support datatypes, minor updates to datatypes theory/rewriter to support datatypes with non-datatype subdata --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a093aa1ef..791e550b9 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -212,7 +212,7 @@ command returns [CVC4::Command* cmd = NULL] sorts.push_back(PARSER_STATE->mkSort(*i)); } } - sortSymbol[t] + sortSymbol[t,CHECK_DECLARED] { PARSER_STATE->popScope(); // Do NOT call mkSort, since that creates a new sort! // This name is not its own distinct sort, it's an alias. @@ -222,7 +222,7 @@ command returns [CVC4::Command* cmd = NULL] | /* function declaration */ DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortList[sorts] RPAREN_TOK - sortSymbol[t] + sortSymbol[t,CHECK_DECLARED] { Debug("parser") << "declare fun: '" << name << "'" << std::endl; if( sorts.size() > 0 ) { t = EXPR_MANAGER->mkFunctionType(sorts, t); @@ -232,7 +232,7 @@ command returns [CVC4::Command* cmd = NULL] | /* function definition */ DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - sortSymbol[t] + sortSymbol[t,CHECK_DECLARED] { /* add variables to parser state before parsing term */ Debug("parser") << "define fun: '" << name << "'" << std::endl; if( sortedVarNames.size() > 0 ) { @@ -462,7 +462,16 @@ term[CVC4::Expr& expr] kind = CVC4::kind::APPLY; } else { expr = PARSER_STATE->getVariable(name); - kind = CVC4::kind::APPLY_UF; + Type t = expr.getType(); + if( t.isConstructor() ){ + kind = CVC4::kind::APPLY_CONSTRUCTOR; + }else if( t.isSelector() ){ + kind = CVC4::kind::APPLY_SELECTOR; + }else if( t.isTester() ){ + kind = CVC4::kind::APPLY_TESTER; + }else{ + kind = CVC4::kind::APPLY_UF; + } } args.push_back(expr); } @@ -495,6 +504,11 @@ term[CVC4::Expr& expr] PARSER_STATE->getFunction(name)); } else { expr = PARSER_STATE->getVariable(name); + Type t = PARSER_STATE->getType(name); + if(t.isConstructor() && ConstructorType(t).getArity() == 0) { + // don't require parentheses, immediately turn it into an apply + expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr); + } } } @@ -688,7 +702,7 @@ sortList[std::vector& sorts] @declarations { Type t; } - : ( sortSymbol[t] { sorts.push_back(t); } )* + : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )* ; /** @@ -700,7 +714,7 @@ sortedVarList[std::vector >& sortedVars] std::string name; Type t; } - : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t] RPAREN_TOK + : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] RPAREN_TOK { sortedVars.push_back(make_pair(name, t)); } )* ; @@ -713,14 +727,20 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check] : symbol[name,check,SYM_SORT] ; -sortSymbol[CVC4::Type& t] +sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] @declarations { std::string name; std::vector args; std::vector numerals; } : sortName[name,CHECK_NONE] - { t = PARSER_STATE->getSort(name); } + { + if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ){ + t = PARSER_STATE->getSort(name); + }else{ + t = PARSER_STATE->mkUnresolvedType(name); + } + } | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK { if( name == "BitVec" ) { @@ -846,7 +866,7 @@ selector[CVC4::DatatypeConstructor& ctor] std::string id; Type t, t2; } - : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t] + : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE] { ctor.addArg(id, t); Debug("parser-idt") << "selector: " << id.c_str() << std::endl; } diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 23768545d..124e6870d 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -75,11 +75,11 @@ public: << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); } else { - TNode gt = in.getType().mkGroundTerm(); + Node gt = in.getType().mkGroundTerm(); TypeNode gtt = gt.getType(); - Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); + //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); if( !gtt.isInstantiatedDatatype() ){ - gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); } Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 75980993b..174513c72 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -43,7 +43,7 @@ Node TheoryDatatypes::getConstructorForSelector( Node sel ) size_t selIndex = Datatype::indexOf( sel.toExpr() ); const Datatype& dt = ((DatatypeType)((sel.getType()[0]).toType())).getDatatype(); for( unsigned i = 0; iselIndex && + if( dt[i].getNumArgs()>selIndex && Node::fromExpr( dt[i][selIndex].getSelector() )==sel ){ return Node::fromExpr( dt[i].getConstructor() ); } @@ -87,7 +87,7 @@ void TheoryDatatypes::addSharedTerm(TNode t) { void TheoryDatatypes::notifyEq(TNode lhs, TNode rhs) { Debug("datatypes") << "TheoryDatatypes::notifyEq(): " << lhs << " = " << rhs << endl; - + } void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) { @@ -99,7 +99,7 @@ void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) { Debug("datatypes-debug") << "TheoryDatatypes::notifyCongruent(): done." << endl; } -void TheoryDatatypes::preRegisterTerm(TNode n) { +void TheoryDatatypes::preRegisterTerm(TNode n) { Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl; } @@ -216,13 +216,13 @@ void TheoryDatatypes::check(Effort e) { } //Debug("datatypes-conflict") << d_cc << std::endl; Node conflict = d_em.getConflict(); - if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || + if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") || Debug.isOn("datatypes-conflict") ){ cout << "Conflict constructed : " << conflict << endl; } - //if( conflict.getKind()!=kind::AND ){ - // conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict); - //} + if( conflict.getKind()!=kind::AND ){ + conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict); + } d_out->conflict(conflict); return; } @@ -316,6 +316,7 @@ bool TheoryDatatypes::checkTester( Node assertion, Node& conflict, unsigned& r ) //check if empty label (no possible constructors for term) for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { Node leqn = (*i); + Debug("datatypes-debug") << "checking " << leqn << std::endl; if( leqn.getKind() == kind::NOT ) { if( leqn[0].getOperator() == tassertion.getOperator() ) { if( assertion.getKind() != NOT ) { @@ -484,7 +485,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) Debug("datatypes-gt") << "constructor is " << dtc << std::endl; Type tspec = dtc.getSpecializedConstructorType(te.getType().toType()); Debug("datatypes-gt") << "tpec is " << tspec << std::endl; - selectorVals[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + selectorVals[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, NodeManager::currentNM()->mkConst(AscriptionType(tspec)), cons); val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals ); } @@ -532,7 +533,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) bool TheoryDatatypes::collapseSelector( Node t ) { if( !hasConflict() && t.getKind() == APPLY_SELECTOR ) { //collapse constructor - TypeNode retTyp = t.getType(); + TypeNode retTyp = t.getType(); TypeNode typ = t[0].getType(); Node sel = t.getOperator(); TypeNode selType = sel.getType(); @@ -683,13 +684,13 @@ void TheoryDatatypes::merge(TNode a, TNode b) { //check for clash NodeBuilder<> explanation(kind::AND); - if( a.getKind() == kind::APPLY_CONSTRUCTOR && b.getKind() == kind::APPLY_CONSTRUCTOR + if( a.getKind() == kind::APPLY_CONSTRUCTOR && b.getKind() == kind::APPLY_CONSTRUCTOR && a.getOperator()!=b.getOperator() ){ Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, a, b ); d_em.addNode( ccEq, &d_cce ); d_em.addNodeConflict( ccEq, Reason::idt_clash ); Debug("datatypes") << "Clash " << a << " " << b << endl; - return; + return; } Debug("datatypes-debug") << "Done clash" << endl; @@ -854,8 +855,8 @@ void TheoryDatatypes::merge(TNode a, TNode b) { } void TheoryDatatypes::addTermToLabels( Node t ) { - if( ( t.getKind() == VARIABLE || t.getKind() == APPLY_SELECTOR ) && - t.getType().isDatatype() ) { + if( t.getType().isDatatype() ) { + Debug("datatypes-debug") << "Add term to labels " << t << std::endl; Node tmp = find( t ); if( tmp == t ) { //add to labels @@ -923,7 +924,7 @@ void TheoryDatatypes::collectTerms( Node n, bool recurse ) { addTermToLabels( n ); } } - + void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) { Debug("datatypes") << "appending " << eq << endl << " to diseq list of " << of << endl; @@ -961,8 +962,8 @@ void TheoryDatatypes::addEquality(TNode eq) { //record which nodes are waiting to be merged vector< pair< Node, Node > > mp; - mp.insert( mp.begin(), - d_merge_pending[d_merge_pending.size()-1].begin(), + mp.insert( mp.begin(), + d_merge_pending[d_merge_pending.size()-1].begin(), d_merge_pending[d_merge_pending.size()-1].end() ); d_merge_pending.pop_back();