diff options
Diffstat (limited to 'src/parser')
40 files changed, 296 insertions, 1177 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 6dc26d439..1d5190e3f 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -2,9 +2,9 @@ /*! \file antlr_input.cpp ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Kshitij Bansal, Morgan Deters + ** Christopher L. Conway, Kshitij Bansal, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -247,7 +247,6 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre break; } - case LANG_SYGUS_V1: case LANG_SYGUS_V2: input = new SygusInput(inputStream); break; case LANG_TPTP: diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 9c53e0349..d3ae9761d 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index 39b109232..dd0c078a2 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway, Francois Bobot, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp index 052bd5f7f..cdf553880 100644 --- a/src/parser/antlr_line_buffered_input.cpp +++ b/src/parser/antlr_line_buffered_input.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h index 34cb72f1e..edd119d75 100644 --- a/src/parser/antlr_line_buffered_input.h +++ b/src/parser/antlr_line_buffered_input.h @@ -2,9 +2,9 @@ /*! \file antlr_line_buffered_input.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli + ** Andres Noetzli, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h index d2eb742c2..c59b21233 100644 --- a/src/parser/antlr_tracing.h +++ b/src/parser/antlr_tracing.h @@ -2,9 +2,9 @@ /*! \file antlr_tracing.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index 5746793e3..f93b47042 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h index 8afe6864a..f5237dc9d 100644 --- a/src/parser/bounded_token_buffer.h +++ b/src/parser/bounded_token_buffer.h @@ -2,9 +2,9 @@ /*! \file bounded_token_buffer.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters + ** Christopher L. Conway, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp index fb6208d0c..2af675dbc 100644 --- a/src/parser/bounded_token_factory.cpp +++ b/src/parser/bounded_token_factory.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h index f2df9ac36..0f6cd5afe 100644 --- a/src/parser/bounded_token_factory.h +++ b/src/parser/bounded_token_factory.h @@ -2,9 +2,9 @@ /*! \file bounded_token_factory.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters + ** Christopher L. Conway, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 8e4152e2e..b504d290b 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -935,15 +935,8 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd] PARSER_STATE->parseError("Type mismatch in definition"); } } - std::vector<std::vector<Expr>> eformals; - for (unsigned i=0, fsize = formals.size(); i<fsize; i++) - { - eformals.push_back(api::termVectorToExprs(formals[i])); - } cmd->reset( - new DefineFunctionRecCommand(api::termVectorToExprs(funcs), - eformals, - api::termVectorToExprs(formulas))); + new DefineFunctionRecCommand(SOLVER, funcs, formals, formulas, true)); } | toplevelDeclaration[cmd] ; @@ -1159,11 +1152,11 @@ 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 = - new DefineFunctionCommand(*i, func.getExpr(), f.getExpr()); + new DefineFunctionCommand(*i, func.getExpr(), f.getExpr(), true); seq->addCommand(decl); } } @@ -1654,7 +1647,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 +1680,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 +1824,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 +1841,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 +1854,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 +1865,7 @@ postfixTerm[CVC4::api::Term& f] ) ( typeAscription[f, t] { - f = PARSER_STATE->applyTypeAscription(f,t).getExpr(); + f = PARSER_STATE->applyTypeAscription(f,t); } )? ; @@ -1885,8 +1882,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 +2133,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 +2143,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 +2153,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 +2252,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 +2360,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/cvc/cvc.cpp b/src/parser/cvc/cvc.cpp index f312fe13c..4d409a0b4 100644 --- a/src/parser/cvc/cvc.cpp +++ b/src/parser/cvc/cvc.cpp @@ -2,9 +2,9 @@ /*! \file cvc.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h index 58d387ca8..7c226168f 100644 --- a/src/parser/cvc/cvc.h +++ b/src/parser/cvc/cvc.h @@ -2,9 +2,9 @@ /*! \file cvc.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 38e3594e8..32ed589ab 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -2,9 +2,9 @@ /*! \file cvc_input.cpp ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters + ** Christopher L. Conway, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 50be82903..3e46dcb65 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -2,9 +2,9 @@ /*! \file cvc_input.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King + ** Christopher L. Conway, Mathias Preiner, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 78e9b474d..13903eaf5 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/input.h b/src/parser/input.h index f63a55707..35f2ae0fb 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/line_buffer.cpp b/src/parser/line_buffer.cpp index 6e7614d88..35ecbfdbb 100644 --- a/src/parser/line_buffer.cpp +++ b/src/parser/line_buffer.cpp @@ -2,9 +2,9 @@ /*! \file line_buffer.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli, Aina Niemetz + ** Andres Noetzli, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/line_buffer.h b/src/parser/line_buffer.h index e8ab05691..6557539eb 100644 --- a/src/parser/line_buffer.h +++ b/src/parser/line_buffer.h @@ -2,9 +2,9 @@ /*! \file line_buffer.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index 2fa0bd7b9..a753c2404 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h index ee143c6b3..a601704c7 100644 --- a/src/parser/memory_mapped_input_buffer.h +++ b/src/parser/memory_mapped_input_buffer.h @@ -2,9 +2,9 @@ /*! \file memory_mapped_input_buffer.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway + ** Morgan Deters, Mathias Preiner, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/parse_op.cpp b/src/parser/parse_op.cpp index 899ae6893..8ff1619fb 100644 --- a/src/parser/parse_op.cpp +++ b/src/parser/parse_op.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h index 1105cf0c8..c68de390f 100644 --- a/src/parser/parse_op.h +++ b/src/parser/parse_op.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c860d14c7..5d80dd55f 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -2,9 +2,9 @@ /*! \file parser.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Christopher L. Conway + ** Andrew Reynolds, Morgan Deters, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -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,14 +377,25 @@ 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); return unresolved; } +api::Sort Parser::mkUnresolvedType(const std::string& name, size_t arity) +{ + if (arity == 0) + { + return mkUnresolvedType(name); + } + return mkUnresolvedTypeConstructor(name, arity); +} + bool Parser::isUnresolvedType(const std::string& name) { if (!isDeclared(name, SYM_SORT)) { return false; @@ -588,11 +597,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 +634,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 +902,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..84dd4be0c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -2,9 +2,9 @@ /*! \file parser.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Christopher L. Conway + ** Andrew Reynolds, Morgan Deters, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -589,6 +589,13 @@ public: const std::vector<api::Sort>& params); /** + * Creates a new unresolved (parameterized) type constructor of the given + * arity. Calls either mkUnresolvedType or mkUnresolvedTypeConstructor + * depending on the arity. + */ + api::Sort mkUnresolvedType(const std::string& name, size_t arity); + + /** * Returns true IFF name is an unresolved type. */ bool isUnresolvedType(const std::string& name); @@ -805,10 +812,12 @@ public: d_globalDeclarations = flag; } + bool getGlobalDeclarations() { return d_globalDeclarations; } + inline SymbolTable* getSymbolTable() const { return d_symtab; } - + //------------------------ operator overloading /** is this function overloaded? */ bool isOverloadedFunction(api::Term fun) @@ -822,7 +831,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 +843,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 +856,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/parser_builder.cpp b/src/parser/parser_builder.cpp index 651dd560c..f65618267 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Christopher L. Conway, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -89,7 +89,6 @@ Parser* ParserBuilder::build() Parser* parser = NULL; switch (d_lang) { - case language::input::LANG_SYGUS_V1: case language::input::LANG_SYGUS_V2: parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly); break; diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 1a9ca719e..52dc76581 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Christopher L. Conway, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index cd5e162d2..118cc589f 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d591c29de..703696cf5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2,9 +2,9 @@ /*! \file Smt2.g ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -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())); } @@ -305,14 +305,7 @@ command [std::unique_ptr<CVC4::Command>* cmd] PARSER_STATE->checkLogicAllowsFunctions(); } // we allow overloading for function declarations - if (PARSER_STATE->sygus_v1()) - { - // it is a higher-order universal variable - api::Term func = PARSER_STATE->bindBoundVar(name, t); - cmd->reset( - new DeclareSygusFunctionCommand(name, func.getExpr(), t.getType())); - } - else if( PARSER_STATE->sygus() ) + if( PARSER_STATE->sygus() ) { PARSER_STATE->parseErrorLogic("declare-fun are not allowed in sygus " "version 2.0"); @@ -361,8 +354,12 @@ command [std::unique_ptr<CVC4::Command>* cmd] // we allow overloading for function definitions api::Term func = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_DEFINED, true); - cmd->reset(new DefineFunctionCommand( - name, func.getExpr(), api::termVectorToExprs(terms), expr.getExpr())); + cmd->reset( + new DefineFunctionCommand(name, + func.getExpr(), + api::termVectorToExprs(terms), + expr.getExpr(), + PARSER_STATE->getGlobalDeclarations())); } | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd] | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] @@ -563,40 +560,8 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] api::Term var = PARSER_STATE->bindBoundVar(name, t); cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType())); } - | /* declare-primed-var */ - DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } - symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] - { PARSER_STATE->checkUserSymbol(name); } - sortSymbol[t,CHECK_DECLARED] - { - // spurious command, we do not need to create a variable. We only keep - // track of the command for sanity checking / dumping - cmd.reset(new DeclareSygusPrimedVarCommand(name, t.getType())); - } | /* synth-fun */ - ( SYNTH_FUN_V1_TOK { isInv = false; } - | SYNTH_INV_V1_TOK { isInv = true; range = SOLVER->getBooleanSort(); } - ) - { PARSER_STATE->checkThatLogicIsSet(); } - symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] - LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - ( sortSymbol[range,CHECK_DECLARED] )? - { - synthFunFactory.reset(new Smt2::SynthFunFactory( - PARSER_STATE, fun, isInv, range, sortedVarNames)); - } - ( - // optionally, read the sygus grammar - // - // `grammar` specifies the required grammar for the function to - // synthesize, expressed as a type - sygusGrammarV1[grammar, synthFunFactory->getSygusVars(), fun] - )? - { - cmd = synthFunFactory->mkCommand(grammar); - } - | /* synth-fun */ ( SYNTH_FUN_TOK { isInv = false; } | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); } ) @@ -643,292 +608,6 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] | command[&cmd] ; -/** Reads a sygus grammar - * - * The resulting sygus datatype encoding the grammar is stored in ret. - * The argument sygus_vars indicates the sygus bound variable list, which is - * the argument list of the function-to-synthesize (or null if the grammar - * has bound variables). - * The argument fun is a unique identifier to avoid naming clashes for the - * datatypes constructed by this call. - */ -sygusGrammarV1[CVC4::api::Sort & ret, - const std::vector<CVC4::api::Term>& sygus_vars, - const std::string& fun] -@declarations -{ - CVC4::api::Sort t; - std::string name; - unsigned startIndex = 0; - std::vector<std::vector<CVC4::SygusGTerm>> sgts; - std::vector<api::DatatypeDecl> datatypes; - std::vector<api::Sort> sorts; - std::vector<std::vector<ParseOp>> ops; - std::vector<std::vector<std::string>> cnames; - std::vector<std::vector<std::vector<CVC4::api::Sort>>> cargs; - std::vector<bool> allow_const; - std::vector<std::vector<std::string>> unresolved_gterm_sym; - std::map<CVC4::api::Sort, CVC4::api::Sort> sygus_to_builtin; - std::map<CVC4::api::Sort, CVC4::api::Term> sygus_to_builtin_expr; -} - : LPAREN_TOK { PARSER_STATE->pushScope(); } - (LPAREN_TOK - symbol[name, CHECK_NONE, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED] { - if (name == "Start") - { - startIndex = datatypes.size(); - } - sgts.push_back(std::vector<CVC4::SygusGTerm>()); - sgts.back().push_back(CVC4::SygusGTerm()); - PARSER_STATE->pushSygusDatatypeDef(t, - name, - datatypes, - sorts, - ops, - cnames, - cargs, - allow_const, - unresolved_gterm_sym); - api::Sort unres_t; - if (!PARSER_STATE->isUnresolvedType(name)) - { - // if not unresolved, must be undeclared - Debug("parser-sygus") << "Make unresolved type : " << name - << std::endl; - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT); - unres_t = PARSER_STATE->mkUnresolvedType(name); - } - else - { - Debug("parser-sygus") << "Get sort : " << name << std::endl; - unres_t = PARSER_STATE->getSort(name); - } - sygus_to_builtin[unres_t] = t; - Debug("parser-sygus") << "--- Read sygus grammar " << name - << " under function " << fun << "..." - << std::endl - << " type to resolve " << unres_t << std::endl - << " builtin type " << t << std::endl; - } - // Note the official spec for NTDef is missing the ( parens ) - // but they are necessary to parse SyGuS examples - LPAREN_TOK(sygusGTerm[sgts.back().back(), fun] { - sgts.back().push_back(CVC4::SygusGTerm()); - }) - + RPAREN_TOK { sgts.back().pop_back(); } RPAREN_TOK) - + RPAREN_TOK - { - unsigned numSTerms = sgts.size(); - Debug("parser-sygus") << "--- Process " << numSTerms << " sygus gterms..." - << std::endl; - for (unsigned i = 0; i < numSTerms; i++) - { - for (unsigned j = 0, size = sgts[i].size(); j < size; j++) - { - api::Sort sub_ret; - PARSER_STATE->processSygusGTerm(sgts[i][j], - i, - datatypes, - sorts, - ops, - cnames, - cargs, - allow_const, - unresolved_gterm_sym, - sygus_vars, - sygus_to_builtin, - sygus_to_builtin_expr, - sub_ret); - } - } - // swap index if necessary - Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl; - unsigned ndatatypes = datatypes.size(); - for (unsigned i = 0; i < ndatatypes; i++) - { - Debug("parser-sygus") << "..." << datatypes[i].getName() - << " has builtin sort " << sorts[i] << std::endl; - } - api::Term bvl; - if (!sygus_vars.empty()) - { - bvl = MK_TERM(api::BOUND_VAR_LIST, sygus_vars); - } - for (unsigned i = 0; i < ndatatypes; i++) - { - Debug("parser-sygus") << "...make " << datatypes[i].getName() - << " with builtin sort " << sorts[i] << std::endl; - if (sorts[i].isNull()) - { - PARSER_STATE->parseError( - "Internal error : could not infer " - "builtin sort for nested gterm."); - } - datatypes[i].getDatatype().setSygus( - sorts[i].getType(), bvl.getExpr(), allow_const[i], false); - PARSER_STATE->mkSygusDatatype(datatypes[i], - ops[i], - cnames[i], - cargs[i], - unresolved_gterm_sym[i], - sygus_to_builtin); - } - PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, ops); - PARSER_STATE->popScope(); - Debug("parser-sygus") << "--- Make " << ndatatypes - << " mutual datatypes..." << std::endl; - for (unsigned i = 0; i < ndatatypes; i++) - { - Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName() - << std::endl; - } - - std::vector<CVC4::Datatype> dtypes; - dtypes.reserve(ndatatypes); - - for (api::DatatypeDecl i : datatypes) - { - dtypes.push_back(i.getDatatype()); - } - - std::set<Type> tset = - api::sortSetToTypes(PARSER_STATE->getUnresolvedSorts()); - - std::vector<DatatypeType> datatypeTypes = - SOLVER->getExprManager()->mkMutualDatatypeTypes( - dtypes, tset, ExprManager::DATATYPE_FLAG_PLACEHOLDER); - - PARSER_STATE->getUnresolvedSorts().clear(); - - ret = datatypeTypes[0]; - }; - -// SyGuS grammar term. -// -// fun is the name of the synth-fun this grammar term is for. -// This method adds N operators to ops[index], N names to cnames[index] and N -// type argument vectors to cargs[index] (where typically N=1) -// This method may also add new elements pairwise into -// datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms. -sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] -@declarations { - std::string name, name2; - CVC4::api::Kind k; - CVC4::api::Sort t; - std::string sname; - std::vector< CVC4::api::Term > let_vars; - std::string s; - CVC4::api::Term atomTerm; -} - : LPAREN_TOK - //read operator - ( SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_constant; - sgt.d_type = t; - Debug("parser-sygus") << "Sygus grammar constant." << std::endl; - } - | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_variable; - sgt.d_type = t; - Debug("parser-sygus") << "Sygus grammar variable." << std::endl; - } - | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_local_variable; - sgt.d_type = t; - Debug("parser-sygus") << "Sygus grammar local variable...ignore." - << std::endl; - } - | SYGUS_INPUT_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_input_variable; - sgt.d_type = t; - Debug("parser-sygus") << "Sygus grammar (input) variable." - << std::endl; - } - | symbol[name,CHECK_NONE,SYM_VARIABLE] { - bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); - if(isBuiltinOperator) { - Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " - << name << std::endl; - k = PARSER_STATE->getOperatorKind(name); - sgt.d_name = api::kindToString(k); - sgt.d_gterm_type = SygusGTerm::gterm_op; - 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 - // fail, but we need an operator to continue here.. - Debug("parser-sygus") - << "Sygus grammar " << fun << " : op (declare=" - << PARSER_STATE->isDeclared(name) << ") : " << name - << std::endl; - if (!PARSER_STATE->isDeclared(name)) - { - PARSER_STATE->parseError("Functions in sygus grammars must be " - "defined."); - } - sgt.d_name = name; - sgt.d_gterm_type = SygusGTerm::gterm_op; - sgt.d_op.d_expr = PARSER_STATE->getVariable(name) ; - } - } - ) - //read arguments - { Debug("parser-sygus") << "Read arguments under " << sgt.d_name - << std::endl; - sgt.addChild(); - } - ( sygusGTerm[sgt.d_children.back(), fun] - { Debug("parser-sygus") << "Finished read argument #" - << sgt.d_children.size() << "..." << std::endl; - sgt.addChild(); - } - )* - RPAREN_TOK { - //pop last child index - sgt.d_children.pop_back(); - } - | termAtomic[atomTerm] - { - Debug("parser-sygus") << "Sygus grammar " << fun << " : atomic " - << "expression " << atomTerm << std::endl; - std::stringstream ss; - ss << atomTerm; - sgt.d_op.d_expr = atomTerm.getExpr(); - sgt.d_name = ss.str(); - sgt.d_gterm_type = SygusGTerm::gterm_op; - } - | symbol[name,CHECK_NONE,SYM_VARIABLE] - { - if( name[0] == '-' ){ //hack for unary minus - Debug("parser-sygus") << "Sygus grammar " << fun - << " : unary minus integer literal " << name - << std::endl; - sgt.d_op.d_expr = SOLVER->mkReal(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_op.d_expr = PARSER_STATE->getExpressionForName(name); - sgt.d_name = name; - sgt.d_gterm_type = SygusGTerm::gterm_op; - }else{ - if( PARSER_STATE->isDeclared(name, SYM_SORT) ){ - Debug("parser-sygus") << "Sygus grammar " << fun - << " : nested sort " << name << std::endl; - sgt.d_type = PARSER_STATE->getSort(name); - sgt.d_gterm_type = SygusGTerm::gterm_nested_sort; - }else{ - Debug("parser-sygus") << "Sygus grammar " << fun - << " : unresolved symbol " << name - << std::endl; - sgt.d_gterm_type = SygusGTerm::gterm_unresolved; - sgt.d_name = name; - } - } - } - ; - /** Reads a sygus grammar in the sygus version 2 format * @@ -1204,7 +883,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] expr = PARSER_STATE->mkHoApply( expr, flattenVars ); } cmd->reset(new DefineFunctionRecCommand( - func.getExpr(), api::termVectorToExprs(bvs), expr.getExpr())); + SOLVER, func, bvs, expr, PARSER_STATE->getGlobalDeclarations())); } | DEFINE_FUNS_REC_TOK { PARSER_STATE->checkThatLogicIsSet();} @@ -1267,15 +946,12 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] "Number of functions defined does not match number listed in " "define-funs-rec")); } - std::vector<std::vector<Expr>> eformals; - for (unsigned i=0, fsize = formals.size(); i<fsize; i++) - { - eformals.push_back(api::termVectorToExprs(formals[i])); - } cmd->reset( - new DefineFunctionRecCommand(api::termVectorToExprs(funcs), - eformals, - api::termVectorToExprs(func_defs))); + new DefineFunctionRecCommand(SOLVER, + funcs, + formals, + func_defs, + PARSER_STATE->getGlobalDeclarations())); } ; @@ -1365,14 +1041,21 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] { cmd->reset(seq.release()); } | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); } - ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + ( // (define f t) + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } term[e,e2] - { api::Term func = PARSER_STATE->bindVar(name, e.getSort(), + { + api::Term func = PARSER_STATE->bindVar(name, e.getSort(), ExprManager::VAR_FLAG_DEFINED); - cmd->reset(new DefineFunctionCommand(name, func.getExpr(), e.getExpr())); + cmd->reset( + new DefineFunctionCommand(name, + func.getExpr(), + e.getExpr(), + PARSER_STATE->getGlobalDeclarations())); } - | LPAREN_TOK + | // (define (f (v U) ...) t) + LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortedVarList[sortedVarNames] RPAREN_TOK @@ -1382,7 +1065,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] terms = PARSER_STATE->bindBoundVars(sortedVarNames); } term[e,e2] - { PARSER_STATE->popScope(); + { + PARSER_STATE->popScope(); // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) @@ -1398,11 +1082,16 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] } api::Term func = PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_DEFINED); - cmd->reset(new DefineFunctionCommand( - name, func.getExpr(), api::termVectorToExprs(terms), e.getExpr())); + cmd->reset( + new DefineFunctionCommand(name, + func.getExpr(), + api::termVectorToExprs(terms), + e.getExpr(), + PARSER_STATE->getGlobalDeclarations())); } ) - | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } + | // (define-const x U t) + DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] @@ -1412,14 +1101,19 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] terms = PARSER_STATE->bindBoundVars(sortedVarNames); } term[e, e2] - { PARSER_STATE->popScope(); + { + PARSER_STATE->popScope(); // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) api::Term func = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_DEFINED); - cmd->reset(new DefineFunctionCommand( - name, func.getExpr(), api::termVectorToExprs(terms), e.getExpr())); + cmd->reset( + new DefineFunctionCommand(name, + func.getExpr(), + api::termVectorToExprs(terms), + e.getExpr(), + PARSER_STATE->getGlobalDeclarations())); } | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -1442,6 +1136,17 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] { cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType())); } + | GET_INTERPOL_TOK { + PARSER_STATE->checkThatLogicIsSet(); + } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + term[e,e2] + ( + sygusGrammar[t, terms, name] + )? + { + cmd->reset(new GetInterpolCommand(SOLVER, name, e, t.getType())); + } | DECLARE_HEAP LPAREN_TOK sortSymbol[t, CHECK_DECLARED] sortSymbol[t, CHECK_DECLARED] @@ -1530,7 +1235,10 @@ datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] /** * Read a list of datatype definitions for datatypes with names dnames and * parametric arities arities. A negative value in arities indicates that the - * arity for the corresponding datatype has not been fixed. + * arity for the corresponding datatype has not been fixed: notice that we do + * not know the arity of datatypes in the declare-datatype command prior to + * parsing their body, whereas the arity of datatypes in declare-datatypes is + * given in the preamble of that command and thus is known prior to this call. */ datatypesDef[bool isCo, const std::vector<std::string>& dnames, @@ -1541,7 +1249,26 @@ datatypesDef[bool isCo, std::string name; std::vector<api::Sort> params; } - : { PARSER_STATE->pushScope(true); } + : { PARSER_STATE->pushScope(true); + // Declare the datatypes that are currently being defined as unresolved + // types. If we do not know the arity of the datatype yet, we wait to + // define it until parsing the preamble of its body, which may optionally + // involve `par`. This is limited to the case of single datatypes defined + // via declare-datatype, and hence no datatype body is parsed without + // having all types declared. This ensures we can parse datatypes with + // nested recursion, e.g. datatypes D having a subfield type + // (Array Int D). + for (unsigned i=0, dsize=dnames.size(); i<dsize; i++) + { + if( arities[i]<0 ) + { + // do not know the arity yet + continue; + } + unsigned arity = static_cast<unsigned>(arities[i]); + PARSER_STATE->mkUnresolvedType(dnames[i], arity); + } + } ( LPAREN_TOK { params.clear(); Debug("parser-dt") << "Processing datatype #" << dts.size() << std::endl; @@ -1559,6 +1286,11 @@ datatypesDef[bool isCo, if( arities[dts.size()]>=0 && static_cast<int>(params.size())!=arities[dts.size()] ){ PARSER_STATE->parseError("Wrong number of parameters for datatype."); } + if (arities[dts.size()]<0) + { + // now declare it as an unresolved type + PARSER_STATE->mkUnresolvedType(dnames[dts.size()], params.size()); + } Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl; dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()], params, isCo)); } @@ -1569,6 +1301,11 @@ datatypesDef[bool isCo, if( arities[dts.size()]>0 ){ PARSER_STATE->parseError("No parameters given for datatype."); } + else if (arities[dts.size()]<0) + { + // now declare it as an unresolved type + PARSER_STATE->mkUnresolvedType(dnames[dts.size()], 0); + } Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl; dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()], params, @@ -1692,7 +1429,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 { @@ -1723,7 +1466,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] expr = PARSER_STATE->applyParseOp(p, args); } | /* a let or sygus let binding */ - LPAREN_TOK ( + LPAREN_TOK LET_TOK LPAREN_TOK { PARSER_STATE->pushScope(true); } ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] @@ -1739,24 +1482,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] } else { names.insert(name); } - binders.push_back(std::make_pair(name, expr)); } )+ | - SYGUS_LET_TOK LPAREN_TOK - { PARSER_STATE->pushScope(true); } - ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] - sortSymbol[type,CHECK_DECLARED] - term[expr, f2] - RPAREN_TOK - // this is a parallel let, so we have to save up all the contributions - // of the let and define them only later on - { if(names.count(name) == 1) { - std::stringstream ss; - ss << "warning: symbol `" << name << "' bound multiple times by let;" - << " the last binding will be used, shadowing earlier ones"; - PARSER_STATE->warning(ss.str()); - } else { - names.insert(name); - } - binders.push_back(std::make_pair(name, expr)); } )+ ) + binders.push_back(std::make_pair(name, expr)); } )+ { // now implement these bindings for (const std::pair<std::string, api::Term>& binder : binders) { @@ -1791,8 +1517,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 +1642,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; } ; @@ -1982,7 +1710,7 @@ qualIdentifier[CVC4::ParseOp& p] | LPAREN_TOK AS_TOK ( CONST_TOK sortSymbol[type, CHECK_DECLARED] { - p.d_kind = api::STORE_ALL; + p.d_kind = api::CONST_ARRAY; PARSER_STATE->parseOpApplyTypeAscription(p, type); } | identifier[p] @@ -2177,7 +1905,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] std::string name = sexpr.getValue(); // bind name to expr with define-fun Command* c = new DefineNamedFunctionCommand( - name, func.getExpr(), std::vector<Expr>(), expr.getExpr()); + name, func.getExpr(), std::vector<Expr>(), expr.getExpr(), PARSER_STATE->getGlobalDeclarations()); c->setMuted(true); PARSER_STATE->preemptCommand(c); } @@ -2339,8 +2067,9 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check] | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;}) symbol[name,CHECK_NONE,SYM_SORT] ( nonemptyNumeralList[numerals] - { // allow sygus inputs to elide the `_' - if( !indexed && !PARSER_STATE->sygus_v1() ) { + { + if (!indexed) + { std::stringstream ss; ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name << " ...)"; @@ -2513,7 +2242,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 @@ -2555,8 +2285,7 @@ GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; RESET_TOK : { PARSER_STATE->v2_5() }? 'reset'; RESET_ASSERTIONS_TOK : 'reset-assertions'; -LET_TOK : { !PARSER_STATE->sygus_v1() }? 'let'; -SYGUS_LET_TOK : { PARSER_STATE->sygus_v1() }? 'let'; +LET_TOK : 'let'; ATTRIBUTE_TOK : '!'; LPAREN_TOK : '('; RPAREN_TOK : ')'; @@ -2597,23 +2326,19 @@ INCLUDE_TOK : 'include'; GET_QE_TOK : 'get-qe'; GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; GET_ABDUCT_TOK : 'get-abduct'; +GET_INTERPOL_TOK : 'get-interpol'; DECLARE_HEAP : 'declare-heap'; // SyGuS commands -SYNTH_FUN_V1_TOK : { PARSER_STATE->sygus_v1() }?'synth-fun'; -SYNTH_FUN_TOK : { PARSER_STATE->sygus() && !PARSER_STATE->sygus_v1() }?'synth-fun'; -SYNTH_INV_V1_TOK : { PARSER_STATE->sygus_v1()}?'synth-inv'; -SYNTH_INV_TOK : { PARSER_STATE->sygus() && !PARSER_STATE->sygus_v1()}?'synth-inv'; +SYNTH_FUN_TOK : { PARSER_STATE->sygus() }?'synth-fun'; +SYNTH_INV_TOK : { PARSER_STATE->sygus()}?'synth-inv'; CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth'; DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var'; -DECLARE_PRIMED_VAR_TOK : { PARSER_STATE->sygus_v1() }?'declare-primed-var'; CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint'; INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint'; SET_OPTIONS_TOK : { PARSER_STATE->sygus() }? 'set-options'; SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant'; SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable'; -SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus_v1() }? 'InputVariable'; -SYGUS_LOCAL_VARIABLE_TOK : { PARSER_STATE->sygus_v1() }? 'LocalVariable'; // attributes ATTRIBUTE_PATTERN_TOK : ':pattern'; @@ -2630,8 +2355,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..68b1945fc 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -2,9 +2,9 @@ /*! \file smt2.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Kshitij Bansal, Morgan Deters + ** Andrew Reynolds, Andres Noetzli, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -156,6 +156,8 @@ void Smt2::addStringOperators() { addOperator(api::STRING_CHARAT, "str.at"); addOperator(api::STRING_INDEXOF, "str.indexof"); addOperator(api::STRING_REPLACE, "str.replace"); + addOperator(api::STRING_REPLACE_RE, "str.replace_re"); + addOperator(api::STRING_REPLACE_RE_ALL, "str.replace_re_all"); if (!strictModeEnabled()) { addOperator(api::STRING_TOLOWER, "str.tolower"); @@ -315,6 +317,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; } @@ -560,16 +568,6 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } } - if (sygus_v1()) - { - // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2) - if(name == "Arrays") { - name = "A"; - }else if(name == "Reals") { - name = "LRA"; - } - } - d_logicSet = true; d_logic = name; @@ -634,6 +632,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) { addOperator(api::SELECT, "select"); addOperator(api::STORE, "store"); + addOperator(api::EQ_RANGE, "eqrange"); } if(d_logic.isTheoryEnabled(theory::THEORY_BV)) { @@ -743,13 +742,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) bool Smt2::sygus() const { InputLanguage ilang = getLanguage(); - return ilang == language::input::LANG_SYGUS_V1 - || ilang == language::input::LANG_SYGUS_V2; -} - -bool Smt2::sygus_v1() const -{ - return getLanguage() == language::input::LANG_SYGUS_V1; + return ilang == language::input::LANG_SYGUS_V2; } bool Smt2::sygus_v2() const @@ -890,538 +883,6 @@ api::Term Smt2::mkAbstractValue(const std::string& name) return d_solver->mkAbstractValue(name.substr(1)); } -void Smt2::mkSygusConstantsForType(const api::Sort& type, - std::vector<api::Term>& ops) -{ - if( type.isInteger() ){ - ops.push_back(d_solver->mkReal(0)); - ops.push_back(d_solver->mkReal(1)); - }else if( type.isBitVector() ){ - uint32_t sz = type.getBVSize(); - ops.push_back(d_solver->mkBitVector(sz, 0)); - ops.push_back(d_solver->mkBitVector(sz, 1)); - }else if( type.isBoolean() ){ - ops.push_back(d_solver->mkTrue()); - ops.push_back(d_solver->mkFalse()); - } - //TODO : others? -} - -// This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1) -// This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms. -void Smt2::processSygusGTerm( - CVC4::SygusGTerm& sgt, - int index, - std::vector<api::DatatypeDecl>& datatypes, - std::vector<api::Sort>& sorts, - std::vector<std::vector<ParseOp>>& ops, - std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<api::Sort>>>& cargs, - std::vector<bool>& allow_const, - std::vector<std::vector<std::string>>& unresolved_gterm_sym, - const std::vector<api::Term>& sygus_vars, - std::map<api::Sort, api::Sort>& sygus_to_builtin, - std::map<api::Sort, api::Term>& sygus_to_builtin_expr, - api::Sort& ret, - bool isNested) -{ - if (sgt.d_gterm_type == SygusGTerm::gterm_op) - { - Debug("parser-sygus") << "Add " << sgt.d_op << " to datatype " - << index << std::endl; - api::Kind oldKind; - api::Kind newKind = api::UNDEFINED_KIND; - //convert to UMINUS if one child of MINUS - if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == api::MINUS) - { - oldKind = api::MINUS; - newKind = api::UMINUS; - } - if (newKind != api::UNDEFINED_KIND) - { - Debug("parser-sygus") - << "Replace " << sgt.d_op.d_kind << " with " << newKind << std::endl; - sgt.d_op.d_kind = newKind; - std::string oldName = api::kindToString(oldKind); - std::string newName = api::kindToString(newKind); - size_t pos = 0; - if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){ - sgt.d_name.replace(pos, oldName.length(), newName); - } - } - ops[index].push_back(sgt.d_op); - cnames[index].push_back( sgt.d_name ); - cargs[index].push_back(std::vector<api::Sort>()); - for( unsigned i=0; i<sgt.d_children.size(); i++ ){ - std::stringstream ss; - ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i; - std::string sub_dname = ss.str(); - //add datatype for child - api::Sort null_type; - pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); - int sub_dt_index = datatypes.size()-1; - //process child - api::Sort sub_ret; - processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, - sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true ); - //process the nested gterm (either pop the last datatype, or flatten the argument) - api::Sort tt = processSygusNestedGTerm(sub_dt_index, - sub_dname, - datatypes, - sorts, - ops, - cnames, - cargs, - allow_const, - unresolved_gterm_sym, - sygus_to_builtin, - sygus_to_builtin_expr, - sub_ret); - cargs[index].back().push_back(tt); - } - } - else if (sgt.d_gterm_type == SygusGTerm::gterm_constant) - { - if( sgt.getNumChildren()!=0 ){ - parseError("Bad syntax for Sygus Constant."); - } - std::vector<api::Term> consts; - mkSygusConstantsForType( sgt.d_type, consts ); - Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl; - for( unsigned i=0; i<consts.size(); i++ ){ - std::stringstream ss; - ss << consts[i]; - Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl; - ParseOp constOp; - constOp.d_expr = consts[i]; - ops[index].push_back(constOp); - cnames[index].push_back( ss.str() ); - cargs[index].push_back(std::vector<api::Sort>()); - } - allow_const[index] = true; - } - else if (sgt.d_gterm_type == SygusGTerm::gterm_variable - || sgt.d_gterm_type == SygusGTerm::gterm_input_variable) - { - if( sgt.getNumChildren()!=0 ){ - parseError("Bad syntax for Sygus Variable."); - } - Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl; - for( unsigned i=0; i<sygus_vars.size(); i++ ){ - if (sygus_vars[i].getSort() == sgt.d_type) - { - std::stringstream ss; - ss << sygus_vars[i]; - Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; - 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<api::Sort>()); - } - } - } - else if (sgt.d_gterm_type == SygusGTerm::gterm_nested_sort) - { - ret = sgt.d_type; - } - else if (sgt.d_gterm_type == SygusGTerm::gterm_unresolved) - { - if( isNested ){ - if( isUnresolvedType(sgt.d_name) ){ - ret = getSort(sgt.d_name); - }else{ - //nested, unresolved symbol...fail - std::stringstream ss; - ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl; - parseError(ss.str()); - } - }else{ - //will resolve when adding constructors - unresolved_gterm_sym[index].push_back(sgt.d_name); - } - } - else if (sgt.d_gterm_type == SygusGTerm::gterm_ignore) - { - // do nothing - } -} - -bool Smt2::pushSygusDatatypeDef( - api::Sort t, - std::string& dname, - std::vector<api::DatatypeDecl>& datatypes, - std::vector<api::Sort>& sorts, - std::vector<std::vector<ParseOp>>& ops, - std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<api::Sort>>>& cargs, - std::vector<bool>& allow_const, - std::vector<std::vector<std::string>>& unresolved_gterm_sym) -{ - sorts.push_back(t); - datatypes.push_back(d_solver->mkDatatypeDecl(dname)); - ops.push_back(std::vector<ParseOp>()); - cnames.push_back(std::vector<std::string>()); - cargs.push_back(std::vector<std::vector<api::Sort>>()); - allow_const.push_back(false); - unresolved_gterm_sym.push_back(std::vector< std::string >()); - return true; -} - -bool Smt2::popSygusDatatypeDef( - std::vector<api::DatatypeDecl>& datatypes, - std::vector<api::Sort>& sorts, - std::vector<std::vector<ParseOp>>& ops, - std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<api::Sort>>>& cargs, - std::vector<bool>& allow_const, - std::vector<std::vector<std::string>>& unresolved_gterm_sym) -{ - sorts.pop_back(); - datatypes.pop_back(); - ops.pop_back(); - cnames.pop_back(); - cargs.pop_back(); - allow_const.pop_back(); - unresolved_gterm_sym.pop_back(); - return true; -} - -api::Sort Smt2::processSygusNestedGTerm( - int sub_dt_index, - std::string& sub_dname, - std::vector<api::DatatypeDecl>& datatypes, - std::vector<api::Sort>& sorts, - std::vector<std::vector<ParseOp>>& ops, - std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<api::Sort>>>& cargs, - std::vector<bool>& allow_const, - std::vector<std::vector<std::string>>& unresolved_gterm_sym, - std::map<api::Sort, api::Sort>& sygus_to_builtin, - std::map<api::Sort, CVC4::api::Term>& sygus_to_builtin_expr, - api::Sort sub_ret) -{ - api::Sort t = sub_ret; - Debug("parser-sygus") << "Argument is "; - if( t.isNull() ){ - //then, it is the datatype we constructed, which should have a single constructor - t = mkUnresolvedType(sub_dname); - Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t << std::endl; - Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs[sub_dt_index].size() << std::endl; - if( cargs[sub_dt_index].empty() ){ - parseError(std::string("Internal error : datatype for nested gterm does not have a constructor.")); - } - ParseOp op = ops[sub_dt_index][0]; - api::Sort curr_t; - if (!op.d_expr.isNull() - && (op.d_expr.isConst() || cargs[sub_dt_index][0].empty())) - { - api::Term sop = op.d_expr; - curr_t = sop.getSort(); - Debug("parser-sygus") - << ": it is constant/0-arg cons " << sop << " with type " - << sop.getSort() << ", debug=" << sop.isConst() << " " - << cargs[sub_dt_index][0].size() << std::endl; - // only cache if it is a singleton datatype (has unique expr) - if (ops[sub_dt_index].size() == 1) - { - sygus_to_builtin_expr[t] = sop; - // store that term sop has dedicated sygus type t - if (d_sygus_bound_var_type.find(sop) == d_sygus_bound_var_type.end()) - { - d_sygus_bound_var_type[sop] = t; - } - } - } - else - { - std::vector<api::Term> children; - for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){ - std::map<api::Sort, CVC4::api::Term>::iterator it = - sygus_to_builtin_expr.find(cargs[sub_dt_index][0][i]); - if( it==sygus_to_builtin_expr.end() ){ - if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){ - std::stringstream ss; - ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl; - ss << "Builtin types are currently : " << std::endl; - for (std::map<api::Sort, api::Sort>::iterator itb = - sygus_to_builtin.begin(); - itb != sygus_to_builtin.end(); - ++itb) - { - ss << " " << itb->first << " -> " << itb->second << std::endl; - } - parseError(ss.str()); - } - api::Sort bt = sygus_to_builtin[cargs[sub_dt_index][0][i]]; - Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl; - std::stringstream ss; - ss << t << "_x_" << i; - api::Term bv = bindBoundVar(ss.str(), bt); - children.push_back( bv ); - d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i]; - }else{ - Debug("parser-sygus") << ": child " << i << " existing sygus to builtin expr : " << it->second << std::endl; - children.push_back( it->second ); - } - } - api::Term e = applyParseOp(op, children); - Debug("parser-sygus") << ": constructed " << e << ", which has type " - << e.getSort() << std::endl; - curr_t = e.getSort(); - sygus_to_builtin_expr[t] = e; - } - sorts[sub_dt_index] = curr_t; - sygus_to_builtin[t] = curr_t; - }else{ - Debug("parser-sygus") << "simple argument " << t << std::endl; - Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl; - //otherwise, datatype was unecessary - //pop argument datatype definition - popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); - } - return t; -} - -void Smt2::setSygusStartIndex(const std::string& fun, - int startIndex, - std::vector<api::DatatypeDecl>& datatypes, - std::vector<api::Sort>& sorts, - std::vector<std::vector<ParseOp>>& ops) -{ - if( startIndex>0 ){ - api::DatatypeDecl tmp_dt = datatypes[0]; - api::Sort tmp_sort = sorts[0]; - std::vector<ParseOp> tmp_ops; - tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() ); - datatypes[0] = datatypes[startIndex]; - sorts[0] = sorts[startIndex]; - ops[0].clear(); - ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() ); - datatypes[startIndex] = tmp_dt; - sorts[startIndex] = tmp_sort; - ops[startIndex].clear(); - ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() ); - }else if( startIndex<0 ){ - std::stringstream ss; - ss << "warning: no symbol named Start for synth-fun " << fun << std::endl; - warning(ss.str()); - } -} - -void Smt2::mkSygusDatatype(api::DatatypeDecl& dt, - std::vector<ParseOp>& ops, - std::vector<std::string>& cnames, - std::vector<std::vector<api::Sort>>& cargs, - std::vector<std::string>& unresolved_gterm_sym, - std::map<api::Sort, api::Sort>& sygus_to_builtin) -{ - Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; - Debug("parser-sygus") << " add constructors..." << std::endl; - - Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl; - Debug("parser-sygus") << " add constructors..." << std::endl; - // size of cnames changes, this loop must check size - for (unsigned i = 0; i < cnames.size(); i++) - { - bool is_dup = false; - bool is_dup_op = false; - for (unsigned j = 0; j < i; j++) - { - if( ops[i]==ops[j] ){ - is_dup_op = true; - if( cargs[i].size()==cargs[j].size() ){ - is_dup = true; - for( unsigned k=0; k<cargs[i].size(); k++ ){ - if( cargs[i][k]!=cargs[j][k] ){ - is_dup = false; - break; - } - } - } - if( is_dup ){ - break; - } - } - } - Debug("parser-sygus") << "SYGUS CONS " << i << " : "; - if( is_dup ){ - Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl; - ops.erase( ops.begin() + i, ops.begin() + i + 1 ); - cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 ); - cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 ); - i--; - } - else - { - std::shared_ptr<SygusPrintCallback> spc; - if (is_dup_op) - { - Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] - << std::endl; - // make into define-fun - std::vector<api::Sort> ltypes; - for (unsigned j = 0, size = cargs[i].size(); j < size; j++) - { - ltypes.push_back(sygus_to_builtin[cargs[i][j]]); - } - std::vector<api::Term> largs; - api::Term lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); - - // make the let_body - std::vector<api::Term> largsApply = largs; - api::Term body = applyParseOp(ops[i], largsApply); - // replace by lambda - ParseOp pLam; - pLam.d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body); - ops[i] = pLam; - Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; - // callback prints as the expression - spc = std::make_shared<printer::SygusExprPrintCallback>( - body.getExpr(), api::termVectorToExprs(largs)); - } - else - { - api::Term sop = ops[i].d_expr; - if (!sop.isNull() && sop.getSort().isBitVector() && sop.isConst()) - { - 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 - // format given by the user, we use a print callback to custom print - // the given name. - spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]); - } - else if (!sop.isNull() && sop.getKind() == api::CONSTANT) - { - 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 (sop.getSort().isFunction()) - { - std::vector<api::Sort> ftypes = - sop.getSort().getFunctionDomainSorts(); - std::vector<api::Term> largs; - api::Term lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); - largs.insert(largs.begin(), sop); - api::Term body = d_solver->mkTerm(api::APPLY_UF, largs); - ops[i].d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body); - Debug("parser-sygus") << " ...replace op : " << ops[i] - << std::endl; - } - else - { - Debug("parser-sygus") << " ...replace op : " << ops[i] - << std::endl; - } - // keep a callback to say it should be printed with the defined name - spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]); - } - else - { - Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl; - } - } - // must rename to avoid duplication - std::stringstream ss; - ss << dt.getName() << "_" << i << "_" << cnames[i]; - cnames[i] = ss.str(); - Debug("parser-sygus") << " construct the datatype " << cnames[i] << "..." - << std::endl; - - // Add the sygus constructor, either using the expression operator of - // ops[i], or the kind. - if (!ops[i].d_expr.isNull()) - { - dt.getDatatype().addSygusConstructor(ops[i].d_expr.getExpr(), - cnames[i], - api::sortVectorToTypes(cargs[i]), - spc); - } - else if (ops[i].d_kind != api::NULL_EXPR) - { - dt.getDatatype().addSygusConstructor(extToIntKind(ops[i].d_kind), - cnames[i], - api::sortVectorToTypes(cargs[i]), - spc); - } - else - { - std::stringstream ess; - ess << "unexpected parse operator for sygus constructor" << ops[i]; - parseError(ess.str()); - } - Debug("parser-sygus") << " finished constructing the datatype" - << std::endl; - } - } - - Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl; - if( !unresolved_gterm_sym.empty() ){ - std::vector<api::Sort> types; - Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl; - for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){ - Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym[i] << std::endl; - if( isUnresolvedType(unresolved_gterm_sym[i]) ){ - Debug("parser-sygus") << " it is an unresolved type." << std::endl; - api::Sort t = getSort(unresolved_gterm_sym[i]); - if( std::find( types.begin(), types.end(), t )==types.end() ){ - types.push_back( t ); - //identity element - api::Sort bt = dt.getDatatype().getSygusType(); - Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl; - - std::stringstream ss; - ss << t << "_x"; - api::Term var = bindBoundVar(ss.str(), bt); - std::vector<api::Term> lchildren; - lchildren.push_back(d_solver->mkTerm(api::BOUND_VAR_LIST, var)); - lchildren.push_back(var); - api::Term id_op = d_solver->mkTerm(api::LAMBDA, lchildren); - - // empty sygus callback (should not be printed) - std::shared_ptr<SygusPrintCallback> sepc = - std::make_shared<printer::SygusEmptyPrintCallback>(); - - //make the sygus argument list - std::vector<api::Sort> id_carg; - id_carg.push_back( t ); - dt.getDatatype().addSygusConstructor(id_op.getExpr(), - unresolved_gterm_sym[i], - api::sortVectorToTypes(id_carg), - sepc); - - //add to operators - ParseOp idOp; - idOp.d_expr = id_op; - ops.push_back(idOp); - } - }else{ - std::stringstream ss; - ss << "Unhandled sygus constructor " << unresolved_gterm_sym[i]; - throw ParserException(ss.str()); - } - } - } -} - -api::Term Smt2::makeSygusBoundVarList(api::DatatypeDecl& dt, - unsigned i, - const std::vector<api::Sort>& ltypes, - std::vector<api::Term>& lvars) -{ - for (unsigned j = 0, size = ltypes.size(); j < size; j++) - { - std::stringstream ss; - ss << dt.getName() << "_x_" << i << "_" << j; - api::Term v = bindBoundVar(ss.str(), ltypes[j]); - lvars.push_back(v); - } - return d_solver->mkTerm(api::BOUND_VAR_LIST, lvars); -} void Smt2::addSygusConstructorTerm( api::DatatypeDecl& dt, @@ -1475,7 +936,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; } @@ -1529,7 +990,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type << std::endl; // (as const (Array T1 T2)) - if (p.d_kind == api::STORE_ALL) + if (p.d_kind == api::CONST_ARRAY) { if (!type.isArray()) { @@ -1565,8 +1026,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) @@ -1584,18 +1044,9 @@ api::Term Smt2::parseOpToExpr(ParseOp& p) } else if (!isDeclared(p.d_name, SYM_VARIABLE)) { - if (sygus_v1() && p.d_name[0] == '-' - && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos) - { - // allow unary minus in sygus version 1 - expr = d_solver->mkReal(p.d_name); - } - else - { - std::stringstream ss; - ss << "Symbol " << p.d_name << " is not declared."; - parseError(ss.str()); - } + std::stringstream ss; + ss << "Symbol " << p.d_name << " is not declared."; + parseError(ss.str()); } else { @@ -1696,7 +1147,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) // Second phase: apply the arguments to the parse op const Options& opts = d_solver->getExprManager()->getOptions(); // handle special cases - if (p.d_kind == api::STORE_ALL && !p.d_type.isNull()) + if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull()) { if (args.size() != 1) { @@ -1770,8 +1221,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; } @@ -1815,6 +1268,11 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) Debug("parser") << "applyParseOp: return uminus " << ret << std::endl; return ret; } + if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true") + { + parseError( + "eqrange predicate requires option --arrays-exp to be enabled."); + } api::Term ret = d_solver->mkTerm(kind, args); Debug("parser") << "applyParseOp: return default builtin " << ret << std::endl; diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 35d088601..579fa90ce 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -2,9 +2,9 @@ /*! \file smt2.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Christopher L. Conway + ** Andrew Reynolds, Andres Noetzli, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -60,9 +60,6 @@ class Smt2 : public Parser */ std::unordered_map<std::string, api::Kind> d_indexedOpKindMap; std::pair<api::Term, std::string> d_lastNamedTerm; - // for sygus - std::vector<api::Term> d_sygusVars, d_sygusVarPrimed, d_sygusConstraints, - d_sygusFunSymbols; protected: Smt2(api::Solver* solver, @@ -98,6 +95,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; /** @@ -275,8 +279,6 @@ class Smt2 : public Parser } /** Are we using a sygus language? */ bool sygus() const; - /** Are we using the sygus version 1.0 format? */ - bool sygus_v1() const; /** Are we using the sygus version 2.0 format? */ bool sygus_v2() const; @@ -343,58 +345,6 @@ class Smt2 : public Parser */ api::Term mkAbstractValue(const std::string& name); - void mkSygusConstantsForType(const api::Sort& type, - std::vector<api::Term>& ops); - - void processSygusGTerm( - CVC4::SygusGTerm& sgt, - int index, - std::vector<api::DatatypeDecl>& datatypes, - std::vector<api::Sort>& sorts, - std::vector<std::vector<ParseOp>>& ops, - std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<api::Sort>>>& cargs, - std::vector<bool>& allow_const, - std::vector<std::vector<std::string>>& unresolved_gterm_sym, - const std::vector<api::Term>& sygus_vars, - std::map<api::Sort, api::Sort>& sygus_to_builtin, - std::map<api::Sort, api::Term>& sygus_to_builtin_expr, - api::Sort& ret, - bool isNested = false); - - bool pushSygusDatatypeDef( - api::Sort t, - std::string& dname, - std::vector<api::DatatypeDecl>& datatypes, - std::vector<api::Sort>& sorts, - std::vector<std::vector<ParseOp>>& ops, - std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<api::Sort>>>& cargs, - std::vector<bool>& allow_const, - std::vector<std::vector<std::string>>& unresolved_gterm_sym); - - bool popSygusDatatypeDef( - std::vector<api::DatatypeDecl>& datatypes, - std::vector<api::Sort>& sorts, - std::vector<std::vector<ParseOp>>& ops, - std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<api::Sort>>>& cargs, - std::vector<bool>& allow_const, - std::vector<std::vector<std::string>>& unresolved_gterm_sym); - - void setSygusStartIndex(const std::string& fun, - int startIndex, - std::vector<api::DatatypeDecl>& datatypes, - std::vector<api::Sort>& sorts, - std::vector<std::vector<ParseOp>>& ops); - - void mkSygusDatatype(api::DatatypeDecl& dt, - std::vector<ParseOp>& ops, - std::vector<std::string>& cnames, - std::vector<std::vector<api::Sort>>& cargs, - std::vector<std::string>& unresolved_gterm_sym, - std::map<api::Sort, api::Sort>& sygus_to_builtin); - /** * Adds a constructor to sygus datatype dt whose sygus operator is term. * @@ -420,7 +370,6 @@ class Smt2 : public Parser void addSygusConstructorVariables(api::DatatypeDecl& dt, const std::vector<api::Term>& sygusVars, api::Sort type) const; - /** * Smt2 parser provides its own checkDeclaration, which does the * same as the base, but with some more helpful errors. @@ -435,11 +384,6 @@ class Smt2 : public Parser if (name.length() > 1 && name[0] == '-' && name.find_first_not_of("0123456789", 1) == std::string::npos) { - if (sygus_v1()) - { - // "-1" is allowed in SyGuS version 1.0 - return; - } std::stringstream ss; ss << notes << "You may have intended to apply unary minus: `(- " << name.substr(1) << ")'\n"; @@ -530,34 +474,6 @@ class Smt2 : public Parser api::Term applyParseOp(ParseOp& p, std::vector<api::Term>& args); //------------------------- end processing parse operators private: - std::map<api::Term, api::Sort> d_sygus_bound_var_type; - - api::Sort processSygusNestedGTerm( - int sub_dt_index, - std::string& sub_dname, - std::vector<api::DatatypeDecl>& datatypes, - std::vector<api::Sort>& sorts, - std::vector<std::vector<ParseOp>>& ops, - std::vector<std::vector<std::string>>& cnames, - std::vector<std::vector<std::vector<api::Sort>>>& cargs, - std::vector<bool>& allow_const, - std::vector<std::vector<std::string>>& unresolved_gterm_sym, - std::map<api::Sort, api::Sort>& sygus_to_builtin, - std::map<api::Sort, api::Term>& sygus_to_builtin_expr, - api::Sort sub_ret); - - /** make sygus bound var list - * - * This is used for converting non-builtin sygus operators to lambda - * expressions. It takes as input a datatype and constructor index (for - * naming) and a vector of type ltypes. - * It appends a bound variable to lvars for each type in ltypes, and returns - * a bound variable list whose children are lvars. - */ - api::Term makeSygusBoundVarList(api::DatatypeDecl& dt, - unsigned i, - const std::vector<api::Sort>& ltypes, - std::vector<api::Term>& lvars); /** Purify sygus grammar term * diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index c0bece257..521602e87 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -2,9 +2,9 @@ /*! \file smt2_input.cpp ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Andres Noetzli + ** Christopher L. Conway, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 9d4ed2857..843cdf584 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -2,9 +2,9 @@ /*! \file smt2_input.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Tim King, Morgan Deters + ** Christopher L. Conway, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp index a908bf4d5..fa0038bd5 100644 --- a/src/parser/smt2/sygus_input.cpp +++ b/src/parser/smt2/sygus_input.cpp @@ -2,9 +2,9 @@ /*! \file sygus_input.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h index 39b161655..d2cc58e34 100644 --- a/src/parser/smt2/sygus_input.h +++ b/src/parser/smt2/sygus_input.h @@ -2,9 +2,9 @@ /*! \file sygus_input.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Mathias Preiner, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index c2f4675b1..bae02a5d2 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -2,9 +2,9 @@ /*! \file Tptp.g ** \verbatim ** Top contributors (to current version): - ** Francois Bobot, Morgan Deters, Andrew Reynolds + ** Haniel Barbosa, Francois Bobot, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -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 ; diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 51b852eac..403cab42b 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -2,9 +2,9 @@ /*! \file tptp.cpp ** \verbatim ** Top contributors (to current version): - ** Francois Bobot, Andrew Reynolds, Morgan Deters + ** Andrew Reynolds, Francois Bobot, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 50557c95a..3d5419be9 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -2,9 +2,9 @@ /*! \file tptp.h ** \verbatim ** Top contributors (to current version): - ** Francois Bobot, Andrew Reynolds, Tim King + ** Andrew Reynolds, Francois Bobot, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index 741650150..cdd2ac7e5 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -2,9 +2,9 @@ /*! \file tptp_input.cpp ** \verbatim ** Top contributors (to current version): - ** Francois Bobot, Morgan Deters + ** Francois Bobot, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h index 1ca746298..9f8cd386f 100644 --- a/src/parser/tptp/tptp_input.h +++ b/src/parser/tptp/tptp_input.h @@ -2,9 +2,9 @@ /*! \file tptp_input.h ** \verbatim ** Top contributors (to current version): - ** Francois Bobot, Tim King + ** Francois Bobot, Mathias Preiner, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 |