diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-06-04 15:19:18 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-04 15:19:18 -0700 |
commit | c5e74835268abbade41524a0584d3b58e3b000f7 (patch) | |
tree | f9c4d9b0bfda35d0fea98690849db61c902248be /src/parser | |
parent | e7e9b3587f82bb57c25bc52fdb229687cded5e22 (diff) | |
parent | 6c608754e8058098e410e208d0b6cc0f586b79ca (diff) |
Merge branch 'master' into fixJavaTestsfixJavaTests
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 38 | ||||
-rw-r--r-- | src/parser/parser.cpp | 55 | ||||
-rw-r--r-- | src/parser/parser.h | 12 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 33 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 19 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 7 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 4 |
7 files changed, 101 insertions, 67 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 8e4152e2e..e604c7769 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1159,7 +1159,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t, PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); api::Term func = PARSER_STATE->mkVar( *i, - t.getType(), + api::Sort(SOLVER, t.getType()), ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED); PARSER_STATE->defineVar(*i, f); Command* decl = @@ -1654,7 +1654,7 @@ tupleStore[CVC4::api::Term& f] } const Datatype & dt = ((DatatypeType)t.getType()).getDatatype(); f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, api::Term(dt[0][k].getSelector()), f); + api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][k].getSelector()), f); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1687,7 +1687,7 @@ recordStore[CVC4::api::Term& f] } const Datatype & dt = ((DatatypeType)t.getType()).getDatatype(); f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, api::Term(dt[0][id].getSelector()), f); + api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][id].getSelector()), f); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1831,7 +1831,9 @@ postfixTerm[CVC4::api::Term& f] PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } const Datatype & dt = ((DatatypeType)type.getType()).getDatatype(); - f = SOLVER->mkTerm(api::APPLY_SELECTOR,api::Term(dt[0][id].getSelector()), f); + f = SOLVER->mkTerm(api::APPLY_SELECTOR, + api::Term(SOLVER, dt[0][id].getSelector()), + f); } | k=numeral { @@ -1846,7 +1848,9 @@ postfixTerm[CVC4::api::Term& f] PARSER_STATE->parseError(ss.str()); } const Datatype & dt = ((DatatypeType)type.getType()).getDatatype(); - f = SOLVER->mkTerm(api::APPLY_SELECTOR,api::Term(dt[0][k].getSelector()), f); + f = SOLVER->mkTerm(api::APPLY_SELECTOR, + api::Term(SOLVER, dt[0][k].getSelector()), + f); } ) )* @@ -1857,7 +1861,7 @@ postfixTerm[CVC4::api::Term& f] | ABS_TOK LPAREN formula[f] RPAREN { f = MK_TERM(CVC4::api::ABS, f); } | DIVISIBLE_TOK LPAREN formula[f] COMMA n=numeral RPAREN - { f = MK_TERM(SOLVER->mkOp(CVC4::api::DIVISIBLE,n), f); } + { f = MK_TERM(SOLVER->mkOp(CVC4::api::DIVISIBLE, n), f); } | DISTINCT_TOK LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f] { args.push_back(f); } )* RPAREN @@ -1868,7 +1872,7 @@ postfixTerm[CVC4::api::Term& f] ) ( typeAscription[f, t] { - f = PARSER_STATE->applyTypeAscription(f,t).getExpr(); + f = PARSER_STATE->applyTypeAscription(f,t); } )? ; @@ -1885,8 +1889,8 @@ relationTerm[CVC4::api::Term& f] args.push_back(f); types.push_back(f.getSort()); api::Sort t = SOLVER->mkTupleSort(types); - const Datatype& dt = ((DatatypeType)t.getType()).getDatatype(); - args.insert( args.begin(), api::Term(dt[0].getConstructor()) ); + const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype()); + args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } | IDEN_TOK LPAREN formula[f] RPAREN @@ -2136,7 +2140,7 @@ simpleTerm[CVC4::api::Term& f] } api::Sort dtype = SOLVER->mkTupleSort(types); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - args.insert( args.begin(), dt[0].getConstructor() ); + args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } } @@ -2146,7 +2150,9 @@ simpleTerm[CVC4::api::Term& f] { std::vector<api::Sort> types; api::Sort dtype = SOLVER->mkTupleSort(types); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - f = MK_TERM(api::APPLY_CONSTRUCTOR, api::Term(dt[0].getConstructor())); } + f = MK_TERM(api::APPLY_CONSTRUCTOR, + api::Term(SOLVER, dt[0].getConstructor())); + } /* empty record literal */ | PARENHASH HASHPAREN @@ -2154,7 +2160,8 @@ simpleTerm[CVC4::api::Term& f] api::Sort dtype = SOLVER->mkRecordSort( std::vector<std::pair<std::string, api::Sort>>()); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - f = MK_TERM(api::APPLY_CONSTRUCTOR, api::Term(dt[0].getConstructor())); + f = MK_TERM(api::APPLY_CONSTRUCTOR, + api::Term(SOLVER, dt[0].getConstructor())); } /* empty set literal */ | LBRACE RBRACE @@ -2252,7 +2259,7 @@ simpleTerm[CVC4::api::Term& f] } api::Sort dtype = SOLVER->mkRecordSort(typeIds); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - args.insert( args.begin(), dt[0].getConstructor() ); + args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } @@ -2360,8 +2367,9 @@ constructorDef[CVC4::api::DatatypeDecl& type] std::unique_ptr<CVC4::api::DatatypeConstructorDecl> ctor; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] - { - ctor.reset(new CVC4::api::DatatypeConstructorDecl(id)); + { + ctor.reset(new CVC4::api::DatatypeConstructorDecl( + SOLVER->mkDatatypeConstructorDecl(id))); } ( LPAREN selector[&ctor] diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c860d14c7..b24f9ae9d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -82,14 +82,9 @@ api::Term Parser::getSymbol(const std::string& name, SymbolType type) { checkDeclaration(name, CHECK_DECLARED, type); assert(isDeclared(name, type)); - - if (type == SYM_VARIABLE) { - // Functions share var namespace - return d_symtab->lookup(name); - } - - assert(false); // Unhandled(type); - return Expr(); + assert(type == SYM_VARIABLE); + // Functions share var namespace + return api::Term(d_solver, d_symtab->lookup(name)); } api::Term Parser::getVariable(const std::string& name) @@ -166,7 +161,7 @@ api::Sort Parser::getSort(const std::string& name) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); assert(isDeclared(name, SYM_SORT)); - api::Sort t = api::Sort(d_symtab->lookupType(name)); + api::Sort t = api::Sort(d_solver, d_symtab->lookupType(name)); return t; } @@ -175,8 +170,8 @@ api::Sort Parser::getSort(const std::string& name, { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); assert(isDeclared(name, SYM_SORT)); - api::Sort t = - api::Sort(d_symtab->lookupType(name, api::sortVectorToTypes(params))); + api::Sort t = api::Sort( + d_solver, d_symtab->lookupType(name, api::sortVectorToTypes(params))); return t; } @@ -237,7 +232,8 @@ std::vector<api::Term> Parser::bindBoundVars( std::vector<api::Term> vars; for (std::pair<std::string, api::Sort>& i : sortedVarNames) { - vars.push_back(bindBoundVar(i.first, i.second.getType())); + vars.push_back( + bindBoundVar(i.first, api::Sort(d_solver, i.second.getType()))); } return vars; } @@ -251,7 +247,7 @@ api::Term Parser::mkAnonymousFunction(const std::string& prefix, } stringstream name; name << prefix << "_anon_" << ++d_anonymousFunctionCount; - return mkVar(name.str(), type.getType(), flags); + return mkVar(name.str(), api::Sort(d_solver, type.getType()), flags); } std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names, @@ -334,7 +330,8 @@ void Parser::defineParameterizedType(const std::string& name, api::Sort Parser::mkSort(const std::string& name, uint32_t flags) { Debug("parser") << "newSort(" << name << ")" << std::endl; - api::Sort type = d_solver->getExprManager()->mkSort(name, flags); + api::Sort type = + api::Sort(d_solver, d_solver->getExprManager()->mkSort(name, flags)); defineType( name, type, @@ -348,8 +345,9 @@ api::Sort Parser::mkSortConstructor(const std::string& name, { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - api::Sort type = - d_solver->getExprManager()->mkSortConstructor(name, arity, flags); + api::Sort type = api::Sort( + d_solver, + d_solver->getExprManager()->mkSortConstructor(name, arity, flags)); defineType( name, vector<api::Sort>(arity), @@ -379,8 +377,10 @@ api::Sort Parser::mkUnresolvedTypeConstructor( { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - api::Sort unresolved = d_solver->getExprManager()->mkSortConstructor( - name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER); + api::Sort unresolved = + api::Sort(d_solver, + d_solver->getExprManager()->mkSortConstructor( + name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER)); defineType(name, params, unresolved); api::Sort t = getSort(name, params); d_unresolved.insert(unresolved); @@ -588,11 +588,12 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) Expr e = t.getExpr(); const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; - t = api::Term(em->mkExpr( - kind::APPLY_TYPE_ASCRIPTION, - em->mkConst( - AscriptionType(dtc.getSpecializedConstructorType(s.getType()))), - e)); + t = api::Term( + d_solver, + em->mkExpr(kind::APPLY_TYPE_ASCRIPTION, + em->mkConst(AscriptionType( + dtc.getSpecializedConstructorType(s.getType()))), + e)); } // the type of t does not match the sort s by design (constructor type // vs datatype type), thus we use an alternative check here. @@ -624,7 +625,7 @@ api::Term Parser::mkVar(const std::string& name, uint32_t flags) { return api::Term( - d_solver->getExprManager()->mkVar(name, type.getType(), flags)); + d_solver, d_solver->getExprManager()->mkVar(name, type.getType(), flags)); } //!!!!!!!!!!! temporary @@ -892,16 +893,16 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) return str; } -Expr Parser::mkStringConstant(const std::string& s) +api::Term Parser::mkStringConstant(const std::string& s) { ExprManager* em = d_solver->getExprManager(); if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage())) { - return d_solver->mkString(s, true).getExpr(); + return api::Term(d_solver, d_solver->mkString(s, true).getExpr()); } // otherwise, we must process ad-hoc escape sequences std::vector<unsigned> str = processAdHocStringEsc(s); - return d_solver->mkString(str).getExpr(); + return api::Term(d_solver, d_solver->mkString(str).getExpr()); } } /* CVC4::parser namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 7941cfdd5..b5dc83902 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -808,7 +808,7 @@ public: inline SymbolTable* getSymbolTable() const { return d_symtab; } - + //------------------------ operator overloading /** is this function overloaded? */ bool isOverloadedFunction(api::Term fun) @@ -822,7 +822,8 @@ public: */ api::Term getOverloadedConstantForType(const std::string& name, api::Sort t) { - return d_symtab->getOverloadedConstantForType(name, t.getType()); + return api::Term(d_solver, + d_symtab->getOverloadedConstantForType(name, t.getType())); } /** @@ -833,8 +834,9 @@ public: api::Term getOverloadedFunctionForTypes(const std::string& name, std::vector<api::Sort>& argTypes) { - return d_symtab->getOverloadedFunctionForTypes( - name, api::sortVectorToTypes(argTypes)); + return api::Term(d_solver, + d_symtab->getOverloadedFunctionForTypes( + name, api::sortVectorToTypes(argTypes))); } //------------------------ end operator overloading /** @@ -845,7 +847,7 @@ public: * SMT-LIB 2.6 or higher), or otherwise calling the solver to construct * the string. */ - Expr mkStringConstant(const std::string& s); + api::Term mkStringConstant(const std::string& s); private: /** ad-hoc string escaping diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d591c29de..62bf7e974 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -101,7 +101,7 @@ namespace CVC4 { struct myExpr : public CVC4::api::Term { myExpr() : CVC4::api::Term() {} myExpr(void*) : CVC4::api::Term() {} - myExpr(const Expr& e) : CVC4::api::Term(e) {} + myExpr(const Expr& e) : CVC4::api::Term(d_solver, e) {} myExpr(const myExpr& e) : CVC4::api::Term(e) {} };/* struct myExpr */ }/* CVC4::parser::smt2 namespace */ @@ -286,7 +286,7 @@ command [std::unique_ptr<CVC4::Command>* cmd] { 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. - PARSER_STATE->defineParameterizedType(name, sorts, t.getType()); + PARSER_STATE->defineParameterizedType(name, sorts, t); cmd->reset(new DefineTypeCommand( name, api::sortVectorToTypes(sorts), t.getType())); } @@ -800,7 +800,7 @@ sygusGrammarV1[CVC4::api::Sort & ret, PARSER_STATE->getUnresolvedSorts().clear(); - ret = datatypeTypes[0]; + ret = api::Sort(SOLVER, datatypeTypes[0]); }; // SyGuS grammar term. @@ -893,7 +893,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] << "expression " << atomTerm << std::endl; std::stringstream ss; ss << atomTerm; - sgt.d_op.d_expr = atomTerm.getExpr(); + sgt.d_op.d_expr = atomTerm; sgt.d_name = ss.str(); sgt.d_gterm_type = SygusGTerm::gterm_op; } @@ -1692,7 +1692,13 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] std::vector<api::Sort> argTypes; } : LPAREN_TOK quantOp[kind] - { PARSER_STATE->pushScope(true); } + { + if (!PARSER_STATE->isTheoryEnabled(theory::THEORY_QUANTIFIERS)) + { + PARSER_STATE->parseError("Quantifier used in non-quantified logic."); + } + PARSER_STATE->pushScope(true); + } boundVarList[bvl] term[f, f2] RPAREN_TOK { @@ -1791,8 +1797,10 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] Expr ef = f.getExpr(); if (Datatype::datatypeOf(ef).isParametric()) { - type = Datatype::datatypeOf(ef)[Datatype::indexOf(ef)] - .getSpecializedConstructorType(expr.getSort().getType()); + type = api::Sort( + SOLVER, + Datatype::datatypeOf(ef)[Datatype::indexOf(ef)] + .getSpecializedConstructorType(expr.getSort().getType())); } argTypes = type.getConstructorDomainSorts(); } @@ -1914,10 +1922,10 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] sorts.emplace_back(arg.getSort()); terms.emplace_back(arg); } - expr = SOLVER->mkTuple(sorts, terms).getExpr(); + expr = SOLVER->mkTuple(sorts, terms); } | /* an atomic term (a term with no subterms) */ - termAtomic[atomTerm] { expr = atomTerm.getExpr(); } + termAtomic[atomTerm] { expr = atomTerm; } ; @@ -2513,7 +2521,8 @@ constructorDef[CVC4::api::DatatypeDecl& type] } : symbol[id,CHECK_NONE,SYM_VARIABLE] { - ctor = new api::DatatypeConstructorDecl(id); + ctor = new api::DatatypeConstructorDecl( + SOLVER->mkDatatypeConstructorDecl(id)); } ( LPAREN_TOK selector[*ctor] RPAREN_TOK )* { // make the constructor @@ -2630,8 +2639,8 @@ CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple'; TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel'; -HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->'; -HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda'; +HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->'; +HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda'; /** * A sequence of printable ASCII characters (except backslash) that starts diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 91260d1db..608e47a6b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -315,6 +315,12 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const return d_logic.isTheoryEnabled(theory); } +bool Smt2::isHoEnabled() const +{ + return getLogic().isHigherOrder() + && d_solver->getExprManager()->getOptions().getUfHo(); +} + bool Smt2::logicIsSet() { return d_logicSet; } @@ -1371,7 +1377,7 @@ void Smt2::mkSygusDatatype(api::DatatypeDecl& dt, if( std::find( types.begin(), types.end(), t )==types.end() ){ types.push_back( t ); //identity element - api::Sort bt = dt.getDatatype().getSygusType(); + api::Sort bt = api::Sort(d_solver, dt.getDatatype().getSygusType()); Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl; std::stringstream ss; @@ -1475,7 +1481,7 @@ api::Term Smt2::purifySygusGTerm(api::Term term, api::Term ret = d_solver->mkVar(term.getSort()); Trace("parser-sygus2-debug") << "...unresolved non-terminal, intro " << ret << std::endl; - args.push_back(ret.getExpr()); + args.push_back(api::Term(d_solver, ret.getExpr())); cargs.push_back(itn->second); return ret; } @@ -1565,8 +1571,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort(); Trace("parser-qid") << std::endl; // otherwise, we process the type ascription - p.d_expr = - applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr(); + p.d_expr = applyTypeAscription(p.d_expr, type); } api::Term Smt2::parseOpToExpr(ParseOp& p) @@ -1770,8 +1775,10 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) parseError(ss.str()); } const Datatype& dt = ((DatatypeType)t.getType()).getDatatype(); - api::Term ret = d_solver->mkTerm( - api::APPLY_SELECTOR, api::Term(dt[0][n].getSelector()), args[0]); + api::Term ret = + d_solver->mkTerm(api::APPLY_SELECTOR, + api::Term(d_solver, dt[0][n].getSelector()), + args[0]); Debug("parser") << "applyParseOp: return selector " << ret << std::endl; return ret; } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 35d088601..af1e36795 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -98,6 +98,13 @@ class Smt2 : public Parser bool isTheoryEnabled(theory::TheoryId theory) const; + /** + * Checks if higher-order support is enabled. + * + * @return true if higher-order support is enabled, false otherwise + */ + bool isHoEnabled() const; + bool logicIsSet() override; /** diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index c2f4675b1..e26709595 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -1441,7 +1441,7 @@ tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); std::vector<api::Term> lchildren(++lhs.begin(), lhs.end()); rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs); - lhs = api::Term(lhs.getExpr().getOperator()); + lhs = api::Term(SOLVER, lhs.getExpr().getOperator()); } | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK ; @@ -1463,7 +1463,7 @@ tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true); std::vector<api::Term> lchildren(++lhs.begin(), lhs.end()); rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs); - lhs = api::Term(lhs.getExpr().getOperator()); + lhs = api::Term(SOLVER, lhs.getExpr().getOperator()); } | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK ; |