From: Andrew Reynolds Date: Tue, 30 Apr 2019 01:27:20 +0000 (-0500) Subject: Eliminate APPLY kind (#2976) X-Git-Tag: cvc5-1.0.0~4160 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=19a93d5e0f924c70e7f77719e0310c730c8fbc61;p=cvc5.git Eliminate APPLY kind (#2976) --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 4cd9f4923..ab34e62b4 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -52,8 +52,6 @@ const static std::unordered_map s_kinds{ /* Builtin ------------------------------------------------------------- */ {UNINTERPRETED_CONSTANT, CVC4::Kind::UNINTERPRETED_CONSTANT}, {ABSTRACT_VALUE, CVC4::Kind::ABSTRACT_VALUE}, - {FUNCTION, CVC4::Kind::FUNCTION}, - {APPLY, CVC4::Kind::APPLY}, {EQUAL, CVC4::Kind::EQUAL}, {DISTINCT, CVC4::Kind::DISTINCT}, {CONSTANT, CVC4::Kind::VARIABLE}, @@ -300,8 +298,6 @@ const static std::unordered_map /* Builtin --------------------------------------------------------- */ {CVC4::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT}, {CVC4::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE}, - {CVC4::Kind::FUNCTION, FUNCTION}, - {CVC4::Kind::APPLY, APPLY}, {CVC4::Kind::EQUAL, EQUAL}, {CVC4::Kind::DISTINCT, DISTINCT}, {CVC4::Kind::VARIABLE, CONSTANT}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index d4f6880f9..7d9ec28c6 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -78,31 +78,6 @@ enum CVC4_PUBLIC Kind : int32_t /* Built-in operator */ BUILTIN, #endif - /** - * Defined function. - * Parameters: 3 (4) - * See defineFun(). - * Create with: - * defineFun(const std::string& symbol, - * const std::vector& bound_vars, - * Sort sort, - * Term term) - * defineFun(Term fun, - * const std::vector& bound_vars, - * Term term) - */ - FUNCTION, - /** - * Application of a defined function. - * Parameters: n > 1 - * -[1]..[n]: Function argument instantiation Terms - * Create with: - * mkTerm(Kind kind, Term child) - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector& children) - */ - APPLY, /** * Equality. * Parameters: 2 diff --git a/src/expr/node.h b/src/expr/node.h index 935cde308..768d7b948 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -489,7 +489,7 @@ public: /** * Returns a node representing the operator of this expression. - * If this is an APPLY, then the operator will be a functional term. + * If this is an APPLY_UF, then the operator will be a functional term. * Otherwise, it will be a node with kind BUILTIN. */ NodeTemplate getOperator() const; @@ -1273,7 +1273,7 @@ NodeTemplate::printAst(std::ostream& out, int indent) const { /** * Returns a node representing the operator of this expression. - * If this is an APPLY, then the operator will be a functional term. + * If this is an APPLY_UF, then the operator will be a functional term. * Otherwise, it will be a node with kind BUILTIN. */ template diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index bc88166d3..28489154a 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -128,23 +128,18 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { } // now, post-process the expression assert( !expr.isNull() ); - if(isDefinedFunction(expr)) { - // defined functions/constants are wrapped in an APPLY so that they are - // expanded into their definition, e.g. during SmtEnginePrivate::expandDefinitions - expr = getExprManager()->mkExpr(CVC4::kind::APPLY, expr); - }else{ - Type te = expr.getType(); - if(te.isConstructor() && ConstructorType(te).getArity() == 0) { - // nullary constructors have APPLY_CONSTRUCTOR kind with no children - expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr); - } + Type te = expr.getType(); + if (te.isConstructor() && ConstructorType(te).getArity() == 0) + { + // nullary constructors have APPLY_CONSTRUCTOR kind with no children + expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr); } return expr; } Kind Parser::getKindForFunction(Expr fun) { if(isDefinedFunction(fun)) { - return APPLY; + return APPLY_UF; } Type t = fun.getType(); if(t.isConstructor()) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 75df38637..9ba7f4b2e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2091,7 +2091,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] // however, we need to apply partial version since we don't have the internal selector available aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR, dtc[i].getSelector(), expr ) ); } - patexprs.push_back( MK_EXPR( CVC4::kind::APPLY, aargs ) ); + patexprs.push_back( MK_EXPR( CVC4::kind::APPLY_UF, aargs ) ); patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) ); } RPAREN_TOK diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 47da10f42..71ba81124 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -859,7 +859,9 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st children.push_back( it->second ); } } - Kind sk = sop.getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(sop); + Kind sk = sop.getKind() != kind::BUILTIN + ? kind::APPLY_UF + : getExprManager()->operatorToKind(sop); Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl; Expr e = getExprManager()->mkExpr( sk, children ); Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl; @@ -1072,7 +1074,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, } children.insert(children.end(), largs.begin(), largs.end()); Kind sk = ops[i].getKind() != kind::BUILTIN - ? kind::APPLY + ? kind::APPLY_UF : getExprManager()->operatorToKind(ops[i]); Expr body = getExprManager()->mkExpr(sk, children); // replace by lambda @@ -1131,14 +1133,13 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, std::vector largs; Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); largs.insert(largs.begin(), ops[i]); - Expr body = getExprManager()->mkExpr(kind::APPLY, largs); + Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs); ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; } else { - ops[i] = getExprManager()->mkExpr(kind::APPLY, ops[i]); Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index c95ff5781..630d8bdd7 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -280,9 +280,6 @@ void CvcPrinter::toStream( out << ")"; return; break; - case kind::APPLY: - toStream(op, n.getOperator(), depth, types, true); - break; case kind::CHAIN: case kind::DISTINCT: // chain and distinct not supported directly in CVC4, blast them away with the rewriter toStream(out, theory::Rewriter::rewrite(n), depth, types, true); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 7ea7765d8..5311f1bec 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -475,7 +475,6 @@ void Smt2Printer::toStream(std::ostream& out, } switch(Kind k = n.getKind()) { // builtin theory - case kind::APPLY: break; case kind::EQUAL: case kind::DISTINCT: out << smtKindString(k, d_variant) << " "; @@ -965,7 +964,6 @@ static string smtKindString(Kind k, Variant v) { switch(k) { // builtin theory - case kind::APPLY: break; case kind::EQUAL: return "="; case kind::DISTINCT: return "distinct"; case kind::CHAIN: break; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index ecd3c6f16..b1936d8cc 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1358,8 +1358,7 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) this->DefineFunctionCommand::invoke(smtEngine); if (!d_func.isNull() && d_func.getType().isBoolean()) { - smtEngine->addToAssignment( - d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); + smtEngine->addToAssignment(d_func); } d_commandStatus = CommandSuccess::instance(); } @@ -1751,14 +1750,7 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine) for (const auto& p : assignments) { vector v; - if (p.first.getKind() == kind::APPLY) - { - v.emplace_back(SExpr::Keyword(p.first.getOperator().toString())); - } - else - { - v.emplace_back(SExpr::Keyword(p.first.toString())); - } + v.emplace_back(SExpr::Keyword(p.first.toString())); v.emplace_back(SExpr::Keyword(p.second.toString())); sexprs.emplace_back(v); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d035f88c1..66198946f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2734,13 +2734,20 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_mapfind(n); if(i != d_smt.d_definedFunctions->end()) { + Node f = (*i).second.getFormula(); + // must expand its definition + Node fe = expandDefinitions(f, cache, expandOnly); // replacement must be closed if((*i).second.getFormals().size() > 0) { - result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula())); + result.push(d_smt.d_nodeManager->mkNode( + kind::LAMBDA, + d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, + (*i).second.getFormals()), + fe)); continue; } // don't bother putting in the cache - result.push((*i).second.getFormula()); + result.push(fe); continue; } // don't bother putting in the cache @@ -2758,11 +2765,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_mapmkNode(i == 0 ? kind::APPLY_UF : kind::APPLY, children); + terms[i] = d_nodeManager->mkNode(kind::APPLY_UF, children); // make application of Inv on primed variables if (i == 0) { @@ -4218,15 +4219,15 @@ bool SmtEngine::addToAssignment(const Expr& ex) { "expected Boolean-typed variable or function application " "in addToAssignment()" ); Node n = e.getNode(); - // must be an APPLY of a zero-ary defined function, or a variable + // must be a defined constant, or a variable PrettyCheckArgument( - ( ( n.getKind() == kind::APPLY && - ( d_definedFunctions->find(n.getOperator()) != - d_definedFunctions->end() ) && - n.getNumChildren() == 0 ) || - n.isVar() ), e, + (((d_definedFunctions->find(n) != d_definedFunctions->end()) + && n.getNumChildren() == 0) + || n.isVar()), + e, "expected variable or defined-function application " - "in addToAssignment(),\ngot %s", e.toString().c_str() ); + "in addToAssignment(),\ngot %s", + e.toString().c_str()); if(!options::produceAssignments()) { return false; } @@ -4295,8 +4296,7 @@ vector> SmtEngine::getAssignment() // ensure it's a constant Assert(resultNode.isConst()); - Assert(as.getKind() == kind::APPLY || as.isVar()); - Assert(as.getKind() != kind::APPLY || as.getNumChildren() == 0); + Assert(as.isVar()); res.emplace_back(as.toExpr(), resultNode.toExpr()); } } diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 3313a684f..15891dfad 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -289,9 +289,6 @@ constant BUILTIN \ "expr/kind.h" \ "the kind of expressions representing built-in operators" -variable FUNCTION "a defined function" -parameterized APPLY FUNCTION 0: "application of a defined function" - operator EQUAL 2 "equality (two parameters only, sorts must match)" operator DISTINCT 2: "disequality (N-ary, sorts must match)" variable VARIABLE "a variable (not permitted in bindings)" @@ -332,7 +329,6 @@ well-founded SEXPR_TYPE \ "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 2c726d12f..db427d21e 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -31,44 +31,6 @@ namespace CVC4 { namespace theory { namespace builtin { -class ApplyTypeRule { - public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - TNode f = n.getOperator(); - TypeNode fType = f.getType(check); - if( !fType.isFunction() && n.getNumChildren() > 0 ) { - throw TypeCheckingExceptionPrivate(n, "operator does not have function type"); - } - if( check ) { - if(fType.isFunction()) { - if(n.getNumChildren() != fType.getNumChildren() - 1) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); - } - TNode::iterator argument_it = n.begin(); - TNode::iterator argument_it_end = n.end(); - TypeNode::iterator argument_type_it = fType.begin(); - for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) { - if(!(*argument_it).getType().isComparableTo(*argument_type_it)) { - std::stringstream ss; - ss << "argument types do not match the function type:\n" - << "argument: " << *argument_it << "\n" - << "has type: " << (*argument_it).getType() << "\n" - << "not equal: " << *argument_type_it; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - } else { - if( n.getNumChildren() > 0 ) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); - } - } - } - return fType.isFunction() ? fType.getRangeType() : fType; - } -};/* class ApplyTypeRule */ - - class EqualityTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 5d3a92cdc..be87b7e8d 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -191,8 +191,6 @@ Kind DatatypesRewriter::getOperatorKindForSygusBuiltin(Node op) Assert(op.getKind() != BUILTIN); if (op.getKind() == LAMBDA) { - // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF - // does beta-reduction but does not for APPLY return APPLY_UF; } TypeNode tn = op.getType(); @@ -247,7 +245,16 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt, Kind ok = NodeManager::operatorToKind(op); if (ok != UNDEFINED_KIND) { - ret = NodeManager::currentNM()->mkNode(ok, schildren); + if (ok == APPLY_UF && schildren.size() == 1) + { + // This case is triggered for defined constant symbols. In this case, + // we return the operator itself instead of an APPLY_UF node. + ret = schildren[0]; + } + else + { + ret = NodeManager::currentNM()->mkNode(ok, schildren); + } Trace("dt-sygus-util") << "...return (op) " << ret << std::endl; return ret; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 25c0e92aa..c9514dd76 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -414,6 +414,7 @@ set(regress_0_tests regress0/decision/wchains010ue.delta02.smt regress0/declare-fun-is-match.smt2 regress0/declare-funs.smt2 + regress0/define-fun-model.smt2 regress0/distinct.smt regress0/expect/scrub.01.smt regress0/expect/scrub.02.smt diff --git a/test/regress/regress0/define-fun-model.smt2 b/test/regress/regress0/define-fun-model.smt2 new file mode 100644 index 000000000..c6ca206fc --- /dev/null +++ b/test/regress/regress0/define-fun-model.smt2 @@ -0,0 +1,16 @@ +; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/' +; EXPECT: sat +; EXPECT: (((f 4) 7)) +; EXPECT: ((g (lambda ((BOUND_VARIABLE Int)) 7))) +; EXPECT: ((f (lambda ((BOUND_VARIABLE Int)) 7))) +(set-logic UFLIA) +(set-option :produce-models true) +(define-fun f ((x Int)) Int 7) +(declare-fun g (Int) Int) + +(assert (= (g 5) (f 5))) + +(check-sat) +(get-value ((f 4))) +(get-value (g)) +(get-value (f))