From: Andrew Reynolds Date: Fri, 14 Feb 2020 05:31:13 +0000 (-0600) Subject: Update sygus v1 parser to use ParseOp utility (#3756) X-Git-Tag: cvc5-1.0.0~3648 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08289dd911aff28110baf0fd815fd912f8b76fd3;p=cvc5.git Update sygus v1 parser to use ParseOp utility (#3756) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 81328831a..975dd26f6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -924,6 +924,7 @@ install(FILES parser/parser.h parser/parser_builder.h parser/parser_exception.h + parser/parse_op.h DESTINATION ${INCLUDE_INSTALL_DIR}/cvc4/parser) install(FILES diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index 508a74532..3cd6a7e51 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -151,6 +151,7 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java ${CMAKE_CURRENT_BINARY_DIR}/Options.java ${CMAKE_CURRENT_BINARY_DIR}/OutputLanguage.java + ${CMAKE_CURRENT_BINARY_DIR}/ParseOp.java ${CMAKE_CURRENT_BINARY_DIR}/Parser.java ${CMAKE_CURRENT_BINARY_DIR}/ParserBuilder.java ${CMAKE_CURRENT_BINARY_DIR}/ParserEndOfFileException.java diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 7e5fb6d7d..4d2467f84 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -252,7 +252,18 @@ void Datatype::addSygusConstructor(Expr op, } addConstructor(c); } - + +void Datatype::addSygusConstructor(Kind k, + const std::string& cname, + const std::vector& cargs, + std::shared_ptr spc, + int weight) +{ + ExprManagerScope ems(*d_em); + Expr op = d_em->operatorOf(k); + addSygusConstructor(op, cname, cargs, spc, weight); +} + void Datatype::setTuple() { PrettyCheckArgument( !isResolved(), this, "cannot set tuple to a finalized Datatype"); diff --git a/src/expr/datatype.h b/src/expr/datatype.h index dccda5ad4..1ae59f00c 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -630,6 +630,14 @@ class CVC4_PUBLIC Datatype { const std::vector& cargs, std::shared_ptr spc = nullptr, int weight = -1); + /** + * Same as above, with builtin kind k. + */ + void addSygusConstructor(Kind k, + const std::string& cname, + const std::vector& cargs, + std::shared_ptr spc = nullptr, + int weight = -1); /** set that this datatype is a tuple */ void setTuple(); diff --git a/src/expr/datatype.i b/src/expr/datatype.i index 6bd5eb82c..83e21793c 100644 --- a/src/expr/datatype.i +++ b/src/expr/datatype.i @@ -9,6 +9,8 @@ #endif /* SWIGJAVA */ %} +%include "expr/kind.i" + %extend std::vector< CVC4::Datatype > { /* These member functions have slightly different signatures in * different swig language packages. The underlying issue is that diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index f2c1a6ef4..77a9ba053 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -32,12 +32,12 @@ set(libcvc4parser_src_files line_buffer.h memory_mapped_input_buffer.cpp memory_mapped_input_buffer.h + parse_op.h parser.cpp parser.h parser_builder.cpp parser_builder.h parser_exception.h - smt2/parse_op.h smt2/smt2.cpp smt2/smt2.h smt2/smt2_input.cpp diff --git a/src/parser/cvc4parser.i b/src/parser/cvc4parser.i index 2ad3bf01d..accb4826c 100644 --- a/src/parser/cvc4parser.i +++ b/src/parser/cvc4parser.i @@ -9,7 +9,8 @@ namespace CVC4 {} using namespace CVC4; %} -%include "parser/parser_exception.i" %include "parser/input.i" +%include "parser/parse_op.i" %include "parser/parser.i" %include "parser/parser_builder.i" +%include "parser/parser_exception.i" diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h new file mode 100644 index 000000000..2465bf324 --- /dev/null +++ b/src/parser/parse_op.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file parse_op.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Definitions of parsed operators. + **/ + +#include "cvc4parser_public.h" + +#ifndef CVC4__PARSER__PARSE_OP_H +#define CVC4__PARSER__PARSE_OP_H + +#include + +#include "expr/expr.h" +#include "expr/kind.h" + +namespace CVC4 { + +/** A parsed operator + * + * The purpose of this struct is to store information regarding a parsed term + * that might not be ready to associate with an expression. + * + * While parsing terms in smt2, we may store a combination of one or more of + * the following to track how to process this term: + * (1) A kind. + * (2) A string name. + * (3) An expression expr. + * (4) A type t. + * + * Examples: + * + * - For declared functions f that we have not yet looked up in a symbol table, + * we store (2). We may store a name in a state if f is overloaded and we have + * not yet parsed its arguments to know how to disambiguate f. + * - For tuple selectors (_ tupSel n), we store (1) and (3). Kind is set to + * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the + * caller as the n^th generic tuple selector. We do this since there is no + * AST expression representing generic tuple select, and we do not have enough + * type information at this point to know the type of the tuple we will be + * selecting from. + * - For array constant specifications prior to type ascription e.g. when we + * have parsed "const", we store (1), setting the kind to STORE_ALL. + * - For array constant specifications (as const (Array T1 T2)), we store (1) + * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2). + * When parsing this as an operator e.g. ((as const (Array T1 T2)) t), we + * interpret this operator by converting the next parsed constant of type T2 to + * an Array of type (Array T1 T2) over that constant. + */ +struct CVC4_PUBLIC ParseOp +{ + ParseOp() : d_kind(kind::NULL_EXPR) {} + /** The kind associated with the parsed operator, if it exists */ + Kind d_kind; + /** The name associated with the parsed operator, if it exists */ + std::string d_name; + /** The expression associated with the parsed operator, if it exists */ + Expr d_expr; + /** The type associated with the parsed operator, if it exists */ + Type d_type; + + /* Return true if this is equal to 'p'. */ + bool operator==(const ParseOp& p) const + { + return d_kind == p.d_kind && d_name == p.d_name && d_expr == p.d_expr + && d_type == p.d_type; + } +}; + +inline std::ostream& operator<<(std::ostream& os, const ParseOp& p) +{ + if (!p.d_expr.isNull()) + { + return os << p.d_expr; + } + else if (p.d_kind != kind::NULL_EXPR) + { + return os << p.d_kind; + } + return os << "ParseOp::unknown"; +} + +} // namespace CVC4 + +#endif /* CVC4__PARSER__PARSE_OP_H */ diff --git a/src/parser/parse_op.i b/src/parser/parse_op.i new file mode 100644 index 000000000..37c3bd30f --- /dev/null +++ b/src/parser/parse_op.i @@ -0,0 +1,5 @@ +%{ +#include "parser/parse_op.h" +%} + +%include "parser/parse_op.h" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 9829b70d9..af193c04b 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -138,6 +138,11 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { } Kind Parser::getKindForFunction(Expr fun) { + Kind k = getExprManager()->operatorToKind(fun); + if (k != UNDEFINED_KIND) + { + return k; + } Type t = fun.getType(); if (t.isFunction()) { @@ -155,11 +160,7 @@ Kind Parser::getKindForFunction(Expr fun) { { return APPLY_TESTER; } - else - { - parseError("internal error: unhandled function application kind"); - return UNDEFINED_KIND; - } + return UNDEFINED_KIND; } Type Parser::getSort(const std::string& name) { diff --git a/src/parser/parser.h b/src/parser/parser.h index 642b81fb0..b0ef2328f 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -29,6 +29,7 @@ #include "expr/kind.h" #include "expr/symbol_table.h" #include "parser/input.h" +#include "parser/parse_op.h" #include "parser/parser_exception.h" #include "util/unsafe_interrupt_exception.h" @@ -58,7 +59,8 @@ public: gterm_ignore, }; Type d_type; - Expr d_expr; + /** The parsed operator */ + ParseOp d_op; std::vector< Expr > d_let_vars; unsigned d_gterm_type; std::string d_name; @@ -367,11 +369,12 @@ public: virtual Expr getExpressionForNameAndType(const std::string& name, Type t); /** - * Returns the kind that should be used for applications of expression fun, where - * fun has "function-like" type, i.e. where checkFunctionLike(fun) returns true. - * Returns a parse error if fun does not have function-like type. + * Returns the kind that should be used for applications of expression fun. + * This is a generalization of ExprManager::operatorToKind that also + * handles variables whose types are "function-like", i.e. where + * checkFunctionLike(fun) returns true. * - * For example, this function returns + * For examples of the latter, this function returns * APPLY_UF if fun has function type, * APPLY_CONSTRUCTOR if fun has constructor type. */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 30239dc2f..aed62f94c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -81,7 +81,7 @@ using namespace CVC4::parser; #include "parser/antlr_tracing.h" #include "parser/parser.h" -#include "parser/smt2/parse_op.h" +#include "parser/parse_op.h" #include "smt/command.h" namespace CVC4 { @@ -662,7 +662,7 @@ sygusGrammarV1[CVC4::Type & ret, std::vector> sgts; std::vector datatypes; std::vector sorts; - std::vector> ops; + std::vector> ops; std::vector> cnames; std::vector>> cargs; std::vector allow_const; @@ -837,7 +837,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] k = PARSER_STATE->getOperatorKind(name); sgt.d_name = kind::kindToString(k); sgt.d_gterm_type = SygusGTerm::gterm_op; - sgt.d_expr = EXPR_MANAGER->operatorOf(k); + sgt.d_op.d_kind = k; }else{ // what is this sygus term trying to accomplish here, if the // symbol isn't yet declared?! probably the following line will @@ -853,7 +853,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] } sgt.d_name = name; sgt.d_gterm_type = SygusGTerm::gterm_op; - sgt.d_expr = PARSER_STATE->getVariable(name) ; + sgt.d_op.d_expr = PARSER_STATE->getVariable(name) ; } } ) @@ -878,7 +878,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] << "expression " << atomTerm << std::endl; std::stringstream ss; ss << atomTerm; - sgt.d_expr = atomTerm.getExpr(); + sgt.d_op.d_expr = atomTerm.getExpr(); sgt.d_name = ss.str(); sgt.d_gterm_type = SygusGTerm::gterm_op; } @@ -888,13 +888,13 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl; - sgt.d_expr = MK_CONST(Rational(name)); + sgt.d_op.d_expr = MK_CONST(Rational(name)); sgt.d_name = name; sgt.d_gterm_type = SygusGTerm::gterm_op; }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){ Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl; - sgt.d_expr = PARSER_STATE->getExpressionForName(name); + sgt.d_op.d_expr = PARSER_STATE->getExpressionForName(name); sgt.d_name = name; sgt.d_gterm_type = SygusGTerm::gterm_op; }else{ diff --git a/src/parser/smt2/parse_op.h b/src/parser/smt2/parse_op.h deleted file mode 100644 index 40b42d0bb..000000000 --- a/src/parser/smt2/parse_op.h +++ /dev/null @@ -1,74 +0,0 @@ -/********************* */ -/*! \file parse_op.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Definitions of parsed operators in smt2. - **/ - -#include "cvc4parser_private.h" - -#ifndef CVC4__PARSER__SMT2__PARSE_OP_H -#define CVC4__PARSER__SMT2__PARSE_OP_H - -#include - -#include "expr/expr.h" -#include "expr/kind.h" - -namespace CVC4 { - -/** A parsed operator - * - * The purpose of this struct is to store information regarding a parsed term - * in the smt2 language that might not be ready to associate with an - * expression. - * - * While parsing terms in smt2, we may store a combination of one or more of - * the following to track how to process this term: - * (1) A kind. - * (2) A string name. - * (3) An expression expr. - * (4) A type t. - * - * Examples: - * - * - For declared functions f that we have not yet looked up in a symbol table, - * we store (2). We may store a name in a state if f is overloaded and we have - * not yet parsed its arguments to know how to disambiguate f. - * - For tuple selectors (_ tupSel n), we store (1) and (3). Kind is set to - * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the - * caller as the n^th generic tuple selector. We do this since there is no - * AST expression representing generic tuple select, and we do not have enough - * type information at this point to know the type of the tuple we will be - * selecting from. - * - For array constant specifications prior to type ascription e.g. when we - * have parsed "const", we store (1), setting the kind to STORE_ALL. - * - For array constant specifications (as const (Array T1 T2)), we store (1) - * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2). - * When parsing this as an operator e.g. ((as const (Array T1 T2)) t), we - * interpret this operator by converting the next parsed constant of type T2 to - * an Array of type (Array T1 T2) over that constant. - */ -struct ParseOp -{ - ParseOp() : d_kind(kind::NULL_EXPR) {} - /** The kind associated with the parsed operator, if it exists */ - Kind d_kind; - /** The name associated with the parsed operator, if it exists */ - std::string d_name; - /** The expression associated with the parsed operator, if it exists */ - Expr d_expr; - /** The type associated with the parsed operator, if it exists */ - Type d_type; -}; - -} // namespace CVC4 - -#endif /* CVC4__PARSER__SMT2__PARSE_OP_H */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 291885278..3ab3c0eb1 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -975,7 +975,7 @@ void Smt2::processSygusGTerm( int index, std::vector& datatypes, std::vector& sorts, - std::vector>& ops, + std::vector>& ops, std::vector>& cnames, std::vector>>& cargs, std::vector& allow_const, @@ -988,19 +988,20 @@ void Smt2::processSygusGTerm( { if (sgt.d_gterm_type == SygusGTerm::gterm_op) { - Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index - << std::endl; + Debug("parser-sygus") << "Add " << sgt.d_op << " to datatype " + << index << std::endl; Kind oldKind; Kind newKind = kind::UNDEFINED_KIND; //convert to UMINUS if one child of MINUS - if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){ + if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == kind::MINUS) + { oldKind = kind::MINUS; newKind = kind::UMINUS; } if( newKind!=kind::UNDEFINED_KIND ){ - Expr newExpr = getExprManager()->operatorOf(newKind); - Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl; - sgt.d_expr = newExpr; + Debug("parser-sygus") + << "Replace " << sgt.d_op.d_kind << " with " << newKind << std::endl; + sgt.d_op.d_kind = newKind; std::string oldName = kind::kindToString(oldKind); std::string newName = kind::kindToString(newKind); size_t pos = 0; @@ -1008,7 +1009,7 @@ void Smt2::processSygusGTerm( sgt.d_name.replace(pos, oldName.length(), newName); } } - ops[index].push_back( sgt.d_expr ); + ops[index].push_back(sgt.d_op); cnames[index].push_back( sgt.d_name ); cargs[index].push_back( std::vector< CVC4::Type >() ); for( unsigned i=0; i() ); } @@ -1059,7 +1062,9 @@ void Smt2::processSygusGTerm( std::stringstream ss; ss << sygus_vars[i]; Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; - ops[index].push_back( sygus_vars[i] ); + ParseOp varOp; + varOp.d_expr = sygus_vars[i]; + ops[index].push_back(varOp); cnames[index].push_back( ss.str() ); cargs[index].push_back( std::vector< CVC4::Type >() ); } @@ -1091,17 +1096,20 @@ void Smt2::processSygusGTerm( } } -bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname, - std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector >& ops, - std::vector< std::vector >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector< bool >& allow_const, - std::vector< std::vector< std::string > >& unresolved_gterm_sym ){ +bool Smt2::pushSygusDatatypeDef( + Type t, + std::string& dname, + std::vector& datatypes, + std::vector& sorts, + std::vector>& ops, + std::vector>& cnames, + std::vector>>& cargs, + std::vector& allow_const, + std::vector>& unresolved_gterm_sym) +{ sorts.push_back(t); datatypes.push_back(Datatype(getExprManager(), dname)); - ops.push_back(std::vector()); + ops.push_back(std::vector()); cnames.push_back(std::vector()); cargs.push_back(std::vector >()); allow_const.push_back(false); @@ -1109,13 +1117,15 @@ bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname, return true; } -bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector >& ops, - std::vector< std::vector >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector< bool >& allow_const, - std::vector< std::vector< std::string > >& unresolved_gterm_sym ){ +bool Smt2::popSygusDatatypeDef( + std::vector& datatypes, + std::vector& sorts, + std::vector>& ops, + std::vector>& cnames, + std::vector>>& cargs, + std::vector& allow_const, + std::vector>& unresolved_gterm_sym) +{ sorts.pop_back(); datatypes.pop_back(); ops.pop_back(); @@ -1126,15 +1136,20 @@ bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, return true; } -Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector >& ops, - std::vector< std::vector >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector< bool >& allow_const, - std::vector< std::vector< std::string > >& unresolved_gterm_sym, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, - std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) { +Type Smt2::processSygusNestedGTerm( + int sub_dt_index, + std::string& sub_dname, + std::vector& datatypes, + std::vector& sorts, + std::vector>& ops, + std::vector>& cnames, + std::vector>>& cargs, + std::vector& allow_const, + std::vector>& unresolved_gterm_sym, + std::map& sygus_to_builtin, + std::map& sygus_to_builtin_expr, + Type sub_ret) +{ Type t = sub_ret; Debug("parser-sygus") << "Argument is "; if( t.isNull() ){ @@ -1145,9 +1160,12 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st if( cargs[sub_dt_index].empty() ){ parseError(std::string("Internal error : datatype for nested gterm does not have a constructor.")); } - Expr sop = ops[sub_dt_index][0]; + ParseOp op = ops[sub_dt_index][0]; Type curr_t; - if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){ + if (!op.d_expr.isNull() + && (op.d_expr.isConst() || cargs[sub_dt_index][0].empty())) + { + Expr sop = op.d_expr; curr_t = sop.getType(); Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl; // only cache if it is a singleton datatype (has unique expr) @@ -1160,11 +1178,10 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st d_sygus_bound_var_type[sop] = t; } } - }else{ + } + else + { std::vector< Expr > children; - if( sop.getKind() != kind::BUILTIN ){ - children.push_back( sop ); - } for( unsigned i=0; i::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] ); if( it==sygus_to_builtin_expr.end() ){ @@ -1189,11 +1206,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st children.push_back( it->second ); } } - Kind sk = sop.getKind() != kind::BUILTIN - ? getKindForFunction(sop) - : getExprManager()->operatorToKind(sop); - Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl; - Expr e = getExprManager()->mkExpr( sk, children ); + Expr e = applyParseOp(op, children); Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl; curr_t = e.getType(); sygus_to_builtin_expr[t] = e; @@ -1214,12 +1227,12 @@ void Smt2::setSygusStartIndex(const std::string& fun, int startIndex, std::vector& datatypes, std::vector& sorts, - std::vector>& ops) + std::vector>& ops) { if( startIndex>0 ){ CVC4::Datatype tmp_dt = datatypes[0]; Type tmp_sort = sorts[0]; - std::vector< Expr > tmp_ops; + std::vector tmp_ops; tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() ); datatypes[0] = datatypes[startIndex]; sorts[0] = sorts[startIndex]; @@ -1236,10 +1249,13 @@ void Smt2::setSygusStartIndex(const std::string& fun, } } -void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, - std::vector& cnames, std::vector< std::vector< CVC4::Type > >& cargs, - std::vector& unresolved_gterm_sym, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) { +void Smt2::mkSygusDatatype(CVC4::Datatype& dt, + std::vector& ops, + std::vector& cnames, + std::vector>& cargs, + std::vector& unresolved_gterm_sym, + std::map& sygus_to_builtin) +{ Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; @@ -1293,27 +1309,21 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); // make the let_body - std::vector children; - if (ops[i].getKind() != kind::BUILTIN) - { - children.push_back(ops[i]); - } - children.insert(children.end(), largs.begin(), largs.end()); - Kind sk = ops[i].getKind() != kind::BUILTIN - ? getKindForFunction(ops[i]) - : getExprManager()->operatorToKind(ops[i]); - Expr body = getExprManager()->mkExpr(sk, children); + Expr body = applyParseOp(ops[i], largs); // replace by lambda - ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + ParseOp pLam; + pLam.d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + ops[i] = pLam; Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; // callback prints as the expression spc = std::make_shared(body, largs); } else { - if (ops[i].getType().isBitVector() && ops[i].isConst()) + Expr sop = ops[i].d_expr; + if (!sop.isNull() && sop.getType().isBitVector() && sop.isConst()) { - Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " (" + Debug("parser-sygus") << "--> Bit-vector constant " << sop << " (" << cnames[i] << ")" << std::endl; // Since there are multiple output formats for bit-vectors and // we are required by sygus standards to print in the exact input @@ -1321,22 +1331,22 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, // the given name. spc = std::make_shared(cnames[i]); } - else if (ops[i].getKind() == kind::VARIABLE) + else if (!sop.isNull() && sop.getKind() == kind::VARIABLE) { Debug("parser-sygus") << "--> Defined function " << ops[i] << std::endl; // turn f into (lammbda (x) (f x)) // in a degenerate case, ops[i] may be a defined constant, // in which case we do not replace by a lambda. - if (ops[i].getType().isFunction()) + if (sop.getType().isFunction()) { std::vector ftypes = - static_cast(ops[i].getType()).getArgTypes(); + static_cast(sop.getType()).getArgTypes(); std::vector largs; Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); - largs.insert(largs.begin(), ops[i]); + largs.insert(largs.begin(), sop); Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs); - ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + ops[i].d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; } @@ -1359,8 +1369,22 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, cnames[i] = ss.str(); Debug("parser-sygus") << " construct the datatype " << cnames[i] << "..." << std::endl; - // add the sygus constructor - dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc); + // Add the sygus constructor, either using the expression operator of + // ops[i], or the kind. + if (!ops[i].d_expr.isNull()) + { + dt.addSygusConstructor(ops[i].d_expr, cnames[i], cargs[i], spc); + } + else if (ops[i].d_kind != kind::NULL_EXPR) + { + dt.addSygusConstructor(ops[i].d_kind, cnames[i], cargs[i], spc); + } + else + { + std::stringstream ss; + ss << "unexpected parse operator for sygus constructor" << ops[i]; + parseError(ss.str()); + } Debug("parser-sygus") << " finished constructing the datatype" << std::endl; } @@ -1400,7 +1424,9 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc); //add to operators - ops.push_back( id_op ); + ParseOp idOp; + idOp.d_expr = id_op; + ops.push_back(idOp); } }else{ std::stringstream ss; @@ -1711,11 +1737,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) { // An explicit operator, e.g. an indexed symbol. args.insert(args.begin(), p.d_expr); - if (p.d_expr.getType().isTester()) + Kind fkind = getKindForFunction(p.d_expr); + if (fkind != kind::UNDEFINED_KIND) { + // Some operators may require a specific kind. // Testers are handled differently than other indexed operators, // since they require a kind. - kind = kind::APPLY_TESTER; + kind = fkind; } } else @@ -1767,7 +1795,7 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) // Second phase: apply the arguments to the parse op ExprManager* em = getExprManager(); // handle special cases - if (p.d_kind == kind::STORE_ALL) + if (p.d_kind == kind::STORE_ALL && !p.d_type.isNull()) { if (args.size() != 1) { @@ -1812,12 +1840,8 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) } return em->mkConst(ArrayStoreAll(p.d_type, constVal)); } - else if (p.d_kind == kind::APPLY_SELECTOR) + else if (p.d_kind == kind::APPLY_SELECTOR && !p.d_expr.isNull()) { - if (p.d_expr.isNull()) - { - parseError("Could not process parsed tuple selector."); - } // tuple selector case Integer x = p.d_expr.getConst().getNumerator(); if (!x.fitsUnsignedInt()) @@ -1846,9 +1870,15 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) } else if (p.d_kind != kind::NULL_EXPR) { - std::stringstream ss; - ss << "Could not process parsed qualified identifier kind " << p.d_kind; - parseError(ss.str()); + // it should not have an expression or type specified at this point + if (!p.d_expr.isNull() || !p.d_type.isNull()) + { + std::stringstream ss; + ss << "Could not process parsed qualified identifier kind " << p.d_kind; + parseError(ss.str()); + } + // otherwise it is a simple application + kind = p.d_kind; } else if (isBuiltinOperator) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 4f0935916..6c1275115 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -26,8 +26,8 @@ #include #include "api/cvc4cpp.h" +#include "parser/parse_op.h" #include "parser/parser.h" -#include "parser/smt2/parse_op.h" #include "smt/command.h" #include "theory/logic_info.h" #include "util/abstract_value.h" @@ -372,7 +372,7 @@ class Smt2 : public Parser int index, std::vector& datatypes, std::vector& sorts, - std::vector>& ops, + std::vector>& ops, std::vector>& cnames, std::vector>>& cargs, std::vector& allow_const, @@ -388,7 +388,7 @@ class Smt2 : public Parser std::string& dname, std::vector& datatypes, std::vector& sorts, - std::vector>& ops, + std::vector>& ops, std::vector>& cnames, std::vector>>& cargs, std::vector& allow_const, @@ -397,7 +397,7 @@ class Smt2 : public Parser bool popSygusDatatypeDef( std::vector& datatypes, std::vector& sorts, - std::vector>& ops, + std::vector>& ops, std::vector>& cnames, std::vector>>& cargs, std::vector& allow_const, @@ -407,12 +407,14 @@ class Smt2 : public Parser int startIndex, std::vector& datatypes, std::vector& sorts, - std::vector>& ops); + std::vector>& ops); - void mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, - std::vector& cnames, std::vector< std::vector< CVC4::Type > >& cargs, - std::vector& unresolved_gterm_sym, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ); + void mkSygusDatatype(CVC4::Datatype& dt, + std::vector& ops, + std::vector& cnames, + std::vector>& cargs, + std::vector& unresolved_gterm_sym, + std::map& sygus_to_builtin); /** * Adds a constructor to sygus datatype dt whose sygus operator is term. @@ -584,15 +586,19 @@ class Smt2 : public Parser private: std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type; - Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector >& ops, - std::vector< std::vector >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector< bool >& allow_const, - std::vector< std::vector< std::string > >& unresolved_gterm_sym, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, - std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ); + Type processSygusNestedGTerm( + int sub_dt_index, + std::string& sub_dname, + std::vector& datatypes, + std::vector& sorts, + std::vector>& ops, + std::vector>& cnames, + std::vector>>& cargs, + std::vector& allow_const, + std::vector>& unresolved_gterm_sym, + std::map& sygus_to_builtin, + std::map& sygus_to_builtin_expr, + Type sub_ret); /** make sygus bound var list *