-/* ******************* */
-/*! \file Smt2.g
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Christopher L. Conway
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Parser for SMT-LIB v2 input language
- **
- ** Parser for SMT-LIB v2 input language.
- **/
+/* ****************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Morgan Deters, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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.
+ * ****************************************************************************
+ *
+ * Parser for SMT-LIB v2 input language.
+ */
grammar Smt2;
// defaultErrorHandler = false;
// Only lookahead of <= k requested (disable for LL* parsing)
- // Note that CVC4's BoundedTokenBuffer requires a fixed k !
+ // Note that cvc5's BoundedTokenBuffer requires a fixed k !
// If you change this k, change it also in smt2_input.cpp !
k = 2;
}/* options */
@header {
-/**
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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.
- **/
+/* ****************************************************************************
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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.
+ * ****************************************************************************
+ */
}/* @header */
@lexer::includes {
*/
#pragma GCC system_header
-#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
+#if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK)
/* This improves performance by ~10 percent on big inputs.
* This option is only valid if we know the input is ASCII (or some 8-bit encoding).
* If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
*/
# define ANTLR3_INLINE_INPUT_ASCII
# define ANTLR3_INLINE_INPUT_8BIT
-#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
-
-#include "parser/antlr_tracing.h"
+#endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
}/* @lexer::includes */
#include <memory>
#include "base/check.h"
-#include "parser/antlr_tracing.h"
#include "parser/parse_op.h"
#include "parser/parser.h"
#include "smt/command.h"
namespace cvc5 {
- namespace api {
- class Term;
- class Sort;
- }
-
-}/* CVC4 namespace */
+class Term;
+class Sort;
+
+}/* cvc5 namespace */
}/* @parser::includes */
#include <unordered_set>
#include <vector>
-#include "api/cvc4cpp.h"
+#include "api/cpp/cvc5.h"
#include "base/output.h"
-#include "options/set_language.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
#include "parser/smt2/smt2.h"
-#include "util/floatingpoint.h"
+#include "util/floatingpoint_size.h"
#include "util/hash.h"
-#include "util/integer.h"
-#include "util/rational.h"
using namespace cvc5;
using namespace cvc5::parser;
#undef SYM_MAN
#define SYM_MAN PARSER_STATE->getSymbolManager()
#undef MK_TERM
-#define MK_TERM SOLVER->mkTerm
+#define MK_TERM(KIND, ...) SOLVER->mkTerm(KIND, {__VA_ARGS__})
#define UNSUPPORTED PARSER_STATE->unimplementedFeature
}/* parser::postinclude */
* @return the parsed expression, or the Null Expr if we've reached the
* end of the input
*/
-parseExpr returns [cvc5::api::Term expr = cvc5::api::Term()]
+parseExpr returns [cvc5::Term expr = cvc5::Term()]
@declarations {
- cvc5::api::Term expr2;
+ cvc5::Term expr2;
}
: term[expr, expr2]
| EOF
/* This extended command has to be in the outermost production so that
* the RPAREN_TOK is properly eaten and we are in a good state to read
* the included file's tokens. */
- | LPAREN_TOK INCLUDE_TOK str[name,true] RPAREN_TOK
+ | LPAREN_TOK INCLUDE_TOK str[name] RPAREN_TOK
{ if(!PARSER_STATE->canIncludeFile()) {
PARSER_STATE->parseError("include-file feature was disabled for this "
"run.");
@declarations {
std::string name;
std::vector<std::string> names;
- cvc5::api::Term expr, expr2;
- cvc5::api::Sort t;
- std::vector<cvc5::api::Term> terms;
- std::vector<api::Sort> sorts;
- std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
- std::vector<cvc5::api::Term> flattenVars;
+ cvc5::Term expr, expr2;
+ cvc5::Sort t;
+ std::vector<cvc5::Term> terms;
+ std::vector<cvc5::Sort> sorts;
+ std::vector<std::pair<std::string, cvc5::Sort> > sortedVarNames;
+ std::vector<cvc5::Term> flattenVars;
}
: /* set the logic */
SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
symbol[name,CHECK_UNDECLARED,SYM_SORT]
{ PARSER_STATE->checkUserSymbol(name); }
n=INTEGER_LITERAL
- { Debug("parser") << "declare sort: '" << name
+ { Trace("parser") << "declare sort: '" << name
<< "' arity=" << n << std::endl;
unsigned arity = AntlrInput::tokenToUnsigned(n);
if(arity == 0) {
- api::Sort type = PARSER_STATE->mkSort(name);
+ cvc5::Sort type = PARSER_STATE->mkSort(name);
cmd->reset(new DeclareSortCommand(name, 0, type));
} else {
- api::Sort type = PARSER_STATE->mkSortConstructor(name, arity);
+ cvc5::Sort type = PARSER_STATE->mkSortConstructor(name, arity);
cmd->reset(new DeclareSortCommand(name, arity, type));
}
}
DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_SORT]
{ PARSER_STATE->checkUserSymbol(name); }
- LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
+ LPAREN_TOK symbolList[names,CHECK_UNDECLARED,SYM_SORT] RPAREN_TOK
{ PARSER_STATE->pushScope();
for(std::vector<std::string>::const_iterator i = names.begin(),
iend = names.end();
sorts.push_back(PARSER_STATE->mkSort(*i));
}
}
- sortSymbol[t,CHECK_DECLARED]
+ sortSymbol[t]
{ 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.
symbol[name,CHECK_NONE,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
LPAREN_TOK sortList[sorts] RPAREN_TOK
- sortSymbol[t,CHECK_DECLARED]
- { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
+ sortSymbol[t]
+ { Trace("parser") << "declare fun: '" << name << "'" << std::endl;
if( !sorts.empty() ) {
t = PARSER_STATE->mkFlatFunctionType(sorts, t);
}
// we allow overloading for function declarations
if( PARSER_STATE->sygus() )
{
- PARSER_STATE->parseErrorLogic("declare-fun are not allowed in sygus "
- "version 2.0");
+ PARSER_STATE->parseError("declare-fun are not allowed in sygus "
+ "version 2.0");
}
else
{
- api::Term func =
- PARSER_STATE->bindVar(name, t, false, true);
+ cvc5::Term func =
+ PARSER_STATE->bindVar(name, t, true);
cmd->reset(new DeclareFunctionCommand(name, func, t));
}
}
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
- sortSymbol[t,CHECK_DECLARED]
+ sortSymbol[t]
{ /* add variables to parser state before parsing term */
- Debug("parser") << "define fun: '" << name << "'" << std::endl;
+ Trace("parser") << "define fun: '" << name << "'" << std::endl;
if( sortedVarNames.size() > 0 ) {
sorts.reserve(sortedVarNames.size());
- for(std::vector<std::pair<std::string, api::Sort> >::const_iterator i =
+ for(std::vector<std::pair<std::string, cvc5::Sort> >::const_iterator i =
sortedVarNames.begin(), iend = sortedVarNames.end();
i != iend;
++i) {
}
t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
- PARSER_STATE->pushScope();
+ if (t.isFunction())
+ {
+ t = t.getFunctionCodomainSort();
+ }
+ if (sortedVarNames.size() > 0)
+ {
+ PARSER_STATE->pushScope();
+ }
terms = PARSER_STATE->bindBoundVars(sortedVarNames);
}
term[expr, expr2]
expr = PARSER_STATE->mkHoApply(expr, flattenVars);
terms.insert(terms.end(), flattenVars.begin(), flattenVars.end());
}
- PARSER_STATE->popScope();
- // declare the name down here (while parsing term, signature
- // must not be extended with the name itself; no recursion
- // permitted)
- // we allow overloading for function definitions
- api::Term func = PARSER_STATE->bindVar(name, t, false, true);
- cmd->reset(new DefineFunctionCommand(
- name, func, terms, expr, SYM_MAN->getGlobalDeclarations()));
+ if (sortedVarNames.size() > 0)
+ {
+ PARSER_STATE->popScope();
+ }
+ cmd->reset(new DefineFunctionCommand(name, terms, t, expr));
}
| DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
| DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
| /* value query */
- GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+ GET_VALUE_TOK
+ {
+ PARSER_STATE->checkThatLogicIsSet();
+ // bind all symbols specific to the model, e.g. uninterpreted constant
+ // values
+ PARSER_STATE->pushGetValueScope();
+ }
( LPAREN_TOK termList[terms,expr] RPAREN_TOK
{ cmd->reset(new GetValueCommand(terms)); }
| ~LPAREN_TOK
"parentheses?");
}
)
+ { PARSER_STATE->popScope(); }
| /* get-assignment */
GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
{ cmd->reset(new GetAssignmentCommand()); }
ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
{ PARSER_STATE->clearLastNamedTerm(); }
term[expr, expr2]
- { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
- cmd->reset(new AssertCommand(expr, inUnsatCore));
- if(inUnsatCore) {
+ { cmd->reset(new AssertCommand(expr));
+ if (PARSER_STATE->lastNamedTerm().first == expr)
+ {
// set the expression name, if there was a named term
- std::pair<api::Term, std::string> namedTerm =
+ std::pair<cvc5::Term, std::string> namedTerm =
PARSER_STATE->lastNamedTerm();
SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true);
}
}
| /* check-sat */
CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- { if( PARSER_STATE->sygus() ){
+ {
+ if (PARSER_STATE->sygus()) {
PARSER_STATE->parseError("Sygus does not support check-sat command.");
}
+ cmd->reset(new CheckSatCommand());
}
- ( term[expr, expr2]
- { if(PARSER_STATE->strictModeEnabled()) {
- PARSER_STATE->parseError(
- "Extended commands (such as check-sat with an argument) are not "
- "permitted while operating in strict compliance mode.");
- }
- }
- | { expr = api::Term(); }
- )
- { cmd->reset(new CheckSatCommand(expr)); }
| /* check-sat-assuming */
CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( LPAREN_TOK termList[terms,expr] RPAREN_TOK
| /* get-unsat-core */
GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
{ cmd->reset(new GetUnsatCoreCommand); }
+ | /* get-difficulty */
+ GET_DIFFICULTY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+ { cmd->reset(new GetDifficultyCommand); }
+ | /* get-learned-literals */
+ GET_LEARNED_LITERALS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+ { cmd->reset(new GetLearnedLiteralsCommand); }
| /* push */
PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- { if( PARSER_STATE->sygus() ){
- PARSER_STATE->parseError("Sygus does not support push command.");
- }
- }
( k=INTEGER_LITERAL
{ unsigned num = AntlrInput::tokenToUnsigned(k);
if(num == 0) {
}
} )
| POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- { if( PARSER_STATE->sygus() ){
- PARSER_STATE->parseError("Sygus does not support pop command.");
- }
- }
( k=INTEGER_LITERAL
{ unsigned num = AntlrInput::tokenToUnsigned(k);
- if(num > PARSER_STATE->scopeLevel()) {
- PARSER_STATE->parseError("Attempted to pop above the top stack "
- "frame.");
- }
+ // we don't compare num to PARSER_STATE->scopeLevel() here, since
+ // when global declarations is true, the scope level of the parser
+ // is not indicative of the context level.
if(num == 0) {
cmd->reset(new EmptyCommand());
} else if(num == 1) {
/* New SMT-LIB 2.5 command set */
| smt25Command[cmd]
- /* CVC4-extended SMT-LIB commands */
+ /* cvc5-extended SMT-LIB commands */
| extendedCommand[cmd]
{ if(PARSER_STATE->strictModeEnabled()) {
PARSER_STATE->parseError(
sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
@declarations {
- cvc5::api::Term expr, expr2, fun;
- cvc5::api::Sort t, range;
+ cvc5::Term expr, expr2, fun;
+ cvc5::Sort t, range;
std::vector<std::string> names;
- std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
- std::vector<cvc5::api::Term> sygusVars;
+ std::vector<std::pair<std::string, cvc5::Sort> > sortedVarNames;
+ std::vector<cvc5::Term> sygusVars;
std::string name;
+ bool isAssume;
bool isInv;
- cvc5::api::Grammar* grammar = nullptr;
+ cvc5::Grammar* grammar = nullptr;
}
: /* declare-var */
DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
- sortSymbol[t,CHECK_DECLARED]
+ sortSymbol[t]
{
- api::Term var = SOLVER->mkSygusVar(t, name);
+ cvc5::Term var = SOLVER->declareSygusVar(name, t);
PARSER_STATE->defineVar(name, var);
cmd.reset(new DeclareSygusVarCommand(name, var, t));
}
{ PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
- ( sortSymbol[range,CHECK_DECLARED] )?
+ ( sortSymbol[range] )?
{
PARSER_STATE->pushScope();
sygusVars = PARSER_STATE->bindBoundVars(sortedVarNames);
sygusGrammar[grammar, sygusVars, name]
)?
{
- Debug("parser-sygus") << "Define synth fun : " << name << std::endl;
+ Trace("parser-sygus") << "Define synth fun : " << name << std::endl;
fun = isInv ? (grammar == nullptr
? SOLVER->synthInv(name, sygusVars)
? SOLVER->synthFun(name, sygusVars, range)
: SOLVER->synthFun(name, sygusVars, range, *grammar));
- Debug("parser-sygus") << "...read synth fun " << name << std::endl;
+ Trace("parser-sygus") << "...read synth fun " << name << std::endl;
PARSER_STATE->popScope();
// we do not allow overloading for synth fun
PARSER_STATE->defineVar(name, fun);
new SynthFunCommand(name, fun, sygusVars, range, isInv, grammar));
}
| /* constraint */
- CONSTRAINT_TOK {
+ ( CONSTRAINT_TOK { isAssume = false; } | ASSUME_TOK { isAssume = true; } )
+ {
PARSER_STATE->checkThatLogicIsSet();
- Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
- Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
}
term[expr, expr2]
- { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
- cmd.reset(new SygusConstraintCommand(expr));
+ { Trace("parser-sygus") << "...read constraint " << expr << std::endl;
+ cmd.reset(new SygusConstraintCommand(expr, isAssume));
}
| /* inv-constraint */
INV_CONSTRAINT_TOK
}
| /* check-synth */
CHECK_SYNTH_TOK
- { PARSER_STATE->checkThatLogicIsSet(); }
{
+ PARSER_STATE->checkThatLogicIsSet();
cmd.reset(new CheckSynthCommand());
}
+ | /* check-synth-next */
+ CHECK_SYNTH_NEXT_TOK
+ {
+ PARSER_STATE->checkThatLogicIsSet();
+ cmd.reset(new CheckSynthCommand(true));
+ }
+ | /* set-feature */
+ SET_FEATURE_TOK keyword[name] symbolicExpr[expr]
+ {
+ PARSER_STATE->checkThatLogicIsSet();
+ // ":grammars" is defined in the SyGuS version 2.1 standard and is by
+ // default supported, all other features are not.
+ if (name != ":grammars")
+ {
+ std::stringstream ss;
+ ss << "SyGuS feature " << name << " not currently supported";
+ PARSER_STATE->warning(ss.str());
+ }
+ cmd.reset(new EmptyCommand());
+ }
| command[&cmd]
;
* The argument fun is a unique identifier to avoid naming clashes for the
* datatypes constructed by this call.
*/
-sygusGrammar[cvc5::api::Grammar*& ret,
- const std::vector<cvc5::api::Term>& sygusVars,
+sygusGrammar[cvc5::Grammar*& ret,
+ const std::vector<cvc5::Term>& sygusVars,
const std::string& fun]
@declarations
{
// the pre-declaration
- std::vector<std::pair<std::string, cvc5::api::Sort>> sortedVarNames;
+ std::vector<std::pair<std::string, cvc5::Sort>> sortedVarNames;
// non-terminal symbols of the grammar
- std::vector<cvc5::api::Term> ntSyms;
- cvc5::api::Sort t;
+ std::vector<cvc5::Term> ntSyms;
+ cvc5::Sort t;
std::string name;
- cvc5::api::Term e, e2;
+ cvc5::Term e, e2;
unsigned dtProcessed = 0;
}
:
// error to recognize if the user is using the (deprecated) version 1.0
// sygus syntax.
( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
- sortSymbol[t,CHECK_DECLARED] (
+ sortSymbol[t] (
// SyGuS version 1.0 expects a grammar ((Start Int ( ...
// SyGuS version 2.0 expects a predeclaration ((Start Int) ...
LPAREN_TOK
<< "2.0 format requires a predeclaration of the non-terminal "
<< "symbols of the grammar to be given prior to the definition "
<< "of the grammar. See https://sygus.org/language/ for details "
- << "and examples. CVC4 versions past 1.8 do not support SyGuS "
+ << "and examples. cvc5 versions past 1.8 do not support SyGuS "
<< "version 1.0.";
}
else
{
// non-terminal symbols in the pre-declaration are locally scoped
PARSER_STATE->pushScope();
- for (std::pair<std::string, api::Sort>& i : sortedVarNames)
+ for (std::pair<std::string, cvc5::Sort>& i : sortedVarNames)
{
PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
// make the non-terminal symbol, which will be parsed as an ordinary
// free variable.
- api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second);
+ cvc5::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second);
ntSyms.push_back(nts);
}
ret = PARSER_STATE->mkGrammar(sygusVars, ntSyms);
LPAREN_TOK
(
LPAREN_TOK
- symbol[name, CHECK_DECLARED, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED]
+ symbol[name, CHECK_DECLARED, SYM_VARIABLE] sortSymbol[t]
{
// check that it matches sortedVarNames
if (sortedVarNames[dtProcessed].first != name)
// add term as constructor to datatype
ret->addRule(ntSyms[dtProcessed], e);
}
- | LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
+ | LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t] RPAREN_TOK {
// allow constants in datatype for ntSyms[dtProcessed]
ret->addAnyConstant(ntSyms[dtProcessed]);
}
- | LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
+ | LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t] RPAREN_TOK {
// add variable constructors to datatype
ret->addAnyVariable(ntSyms[dtProcessed]);
}
setInfoInternal[std::unique_ptr<cvc5::Command>* cmd]
@declarations {
std::string name;
- api::Term sexpr;
+ cvc5::Term sexpr;
}
- : KEYWORD symbolicExpr[sexpr]
- { name = AntlrInput::tokenText($KEYWORD);
- cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr)));
- }
+ : keyword[name] symbolicExpr[sexpr]
+ { cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr))); }
;
setOptionInternal[std::unique_ptr<cvc5::Command>* cmd]
@init {
std::string name;
- api::Term sexpr;
+ cvc5::Term sexpr;
}
: keyword[name] symbolicExpr[sexpr]
{ cmd->reset(new SetOptionCommand(name.c_str() + 1, sexprToString(sexpr)));
// Ugly that this changes the state of the parser; but
// global-declarations affects parsing, so we can't hold off
- // on this until some SmtEngine eventually (if ever) executes it.
+ // on this until some SolverEngine eventually (if ever) executes it.
if(name == ":global-declarations")
{
SYM_MAN->setGlobalDeclarations(sexprToString(sexpr) == "true");
@declarations {
std::string name;
std::string fname;
- cvc5::api::Term expr, expr2;
- std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
+ cvc5::Term expr, expr2;
+ std::vector<std::pair<std::string, cvc5::Sort> > sortedVarNames;
std::string s;
- cvc5::api::Sort t;
- cvc5::api::Term func;
- std::vector<cvc5::api::Term> bvs;
- std::vector<std::vector<std::pair<std::string, cvc5::api::Sort>>>
+ cvc5::Sort t;
+ cvc5::Term func;
+ std::vector<cvc5::Term> bvs;
+ std::vector<std::vector<std::pair<std::string, cvc5::Sort>>>
sortedVarNamesList;
- std::vector<std::vector<cvc5::api::Term>> flattenVarsList;
- std::vector<std::vector<cvc5::api::Term>> formals;
- std::vector<cvc5::api::Term> funcs;
- std::vector<cvc5::api::Term> func_defs;
- cvc5::api::Term aexpr;
+ std::vector<std::vector<cvc5::Term>> flattenVarsList;
+ std::vector<std::vector<cvc5::Term>> formals;
+ std::vector<cvc5::Term> funcs;
+ std::vector<cvc5::Term> func_defs;
+ cvc5::Term aexpr;
std::unique_ptr<cvc5::CommandSequence> seq;
- std::vector<api::Sort> sorts;
- std::vector<cvc5::api::Term> flattenVars;
+ std::vector<cvc5::Sort> sorts;
+ std::vector<cvc5::Term> flattenVars;
}
/* declare-const */
: DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_NONE,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
- sortSymbol[t,CHECK_DECLARED]
+ sortSymbol[t]
{ // allow overloading here
- api::Term c =
- PARSER_STATE->bindVar(name, t, false, true);
+ if( PARSER_STATE->sygus() )
+ {
+ PARSER_STATE->parseError("declare-const is not allowed in sygus "
+ "version 2.0");
+ }
+ cvc5::Term c =
+ PARSER_STATE->bindVar(name, t, true);
cmd->reset(new DeclareFunctionCommand(name, c, t)); }
/* get model */
/* echo */
| ECHO_TOK
- ( simpleSymbolicExpr[s]
+ ( str[s]
{ cmd->reset(new EchoCommand(s)); }
| { cmd->reset(new EchoCommand()); }
)
symbol[fname,CHECK_NONE,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(fname); }
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
- sortSymbol[t,CHECK_DECLARED]
+ sortSymbol[t]
{
func =
PARSER_STATE->bindDefineFunRec(fname, sortedVarNames, t, flattenVars);
if( !flattenVars.empty() ){
expr = PARSER_STATE->mkHoApply( expr, flattenVars );
}
- cmd->reset(new DefineFunctionRecCommand(
- func, bvs, expr, SYM_MAN->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionRecCommand(func, bvs, expr));
}
| DEFINE_FUNS_REC_TOK
{ PARSER_STATE->checkThatLogicIsSet();}
symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(fname); }
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
- sortSymbol[t,CHECK_DECLARED]
+ sortSymbol[t]
{
flattenVars.clear();
func = PARSER_STATE->bindDefineFunRec(
"Number of functions defined does not match number listed in "
"define-funs-rec"));
}
- cmd->reset(new DefineFunctionRecCommand(
- funcs, formals, func_defs, SYM_MAN->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionRecCommand(funcs, formals, func_defs));
}
;
extendedCommand[std::unique_ptr<cvc5::Command>* cmd]
@declarations {
- std::vector<api::DatatypeDecl> dts;
- cvc5::api::Term e, e2;
- cvc5::api::Sort t, s;
+ std::vector<cvc5::DatatypeDecl> dts;
+ cvc5::Term e, e2;
+ cvc5::Sort t, s;
std::string name;
std::vector<std::string> names;
- std::vector<cvc5::api::Term> terms;
- std::vector<api::Sort> sorts;
- std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
+ std::vector<cvc5::Term> terms;
+ std::vector<cvc5::Sort> sorts;
+ std::vector<std::pair<std::string, cvc5::Sort> > sortedVarNames;
std::unique_ptr<cvc5::CommandSequence> seq;
- api::Grammar* g = nullptr;
+ cvc5::Grammar* g = nullptr;
}
/* Extended SMT-LIB set of commands syntax, not permitted in
* --smtlib2 compliance mode. */
LPAREN_TOK
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
{ PARSER_STATE->checkUserSymbol(name);
- api::Sort type = PARSER_STATE->mkSort(name);
+ cvc5::Sort type = PARSER_STATE->mkSort(name);
seq->addCommand(new DeclareSortCommand(name, 0, type));
}
)+
( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
nonemptySortList[sorts] RPAREN_TOK
- { api::Sort tt;
+ { cvc5::Sort tt;
if(sorts.size() > 1) {
PARSER_STATE->checkLogicAllowsFunctions();
// must flatten
- api::Sort range = sorts.back();
+ cvc5::Sort range = sorts.back();
sorts.pop_back();
tt = PARSER_STATE->mkFlatFunctionType(sorts, range);
} else {
tt = sorts[0];
}
// allow overloading
- api::Term func =
- PARSER_STATE->bindVar(name, tt, false, true);
+ cvc5::Term func =
+ PARSER_STATE->bindVar(name, tt, true);
seq->addCommand(new DeclareFunctionCommand(name, func, tt));
sorts.clear();
}
t = SOLVER->mkFunctionSort(sorts, t);
}
// allow overloading
- api::Term func =
- PARSER_STATE->bindVar(name, t, false, true);
+ cvc5::Term func =
+ PARSER_STATE->bindVar(name, t, true);
seq->addCommand(new DeclareFunctionCommand(name, func, t));
sorts.clear();
}
)+
RPAREN_TOK
{ cmd->reset(seq.release()); }
-
- | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- ( // (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());
- cmd->reset(new DefineFunctionCommand(
- name, func, e, SYM_MAN->getGlobalDeclarations()));
- }
- | // (define (f (v U) ...) t)
- LPAREN_TOK
- symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
- { PARSER_STATE->checkUserSymbol(name); }
- sortedVarList[sortedVarNames] RPAREN_TOK
- { /* add variables to parser state before parsing term */
- Debug("parser") << "define fun: '" << name << "'" << std::endl;
- PARSER_STATE->pushScope();
- terms = PARSER_STATE->bindBoundVars(sortedVarNames);
- }
- term[e,e2]
- {
- PARSER_STATE->popScope();
- // declare the name down here (while parsing term, signature
- // must not be extended with the name itself; no recursion
- // permitted)
- api::Sort tt = e.getSort();
- if( sortedVarNames.size() > 0 ) {
- sorts.reserve(sortedVarNames.size());
- for(std::vector<std::pair<std::string, api::Sort> >::const_iterator
- i = sortedVarNames.begin(), iend = sortedVarNames.end();
- i != iend; ++i) {
- sorts.push_back((*i).second);
- }
- tt = SOLVER->mkFunctionSort(sorts, tt);
- }
- api::Term func = PARSER_STATE->bindVar(name, tt);
- cmd->reset(new DefineFunctionCommand(
- name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
- }
- )
| // (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]
- { /* add variables to parser state before parsing term */
- Debug("parser") << "define const: '" << name << "'" << std::endl;
- PARSER_STATE->pushScope();
- terms = PARSER_STATE->bindBoundVars(sortedVarNames);
- }
+ sortSymbol[t]
term[e, e2]
{
- 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);
- cmd->reset(new DefineFunctionCommand(
- name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionCommand(name, t, e));
}
| SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
{
cmd->reset(new GetAbductCommand(name, e, g));
}
+ | GET_ABDUCT_NEXT_TOK {
+ PARSER_STATE->checkThatLogicIsSet();
+ cmd->reset(new GetAbductNextCommand);
+ }
| GET_INTERPOL_TOK {
PARSER_STATE->checkThatLogicIsSet();
}
sygusGrammar[g, terms, name]
)?
{
- cmd->reset(new GetInterpolCommand(name, e, g));
+ cmd->reset(new GetInterpolantCommand(name, e, g));
+ }
+ | GET_INTERPOL_NEXT_TOK {
+ PARSER_STATE->checkThatLogicIsSet();
+ cmd->reset(new GetInterpolantNextCommand);
}
| DECLARE_HEAP LPAREN_TOK
- sortSymbol[t, CHECK_DECLARED]
- sortSymbol[s, CHECK_DECLARED]
+ sortSymbol[t]
+ sortSymbol[s]
{ cmd->reset(new DeclareHeapCommand(t, s)); }
RPAREN_TOK
- | BLOCK_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- { cmd->reset(new BlockModelCommand()); }
-
+ | DECLARE_POOL { PARSER_STATE->checkThatLogicIsSet(); }
+ symbol[name,CHECK_NONE,SYM_VARIABLE]
+ { PARSER_STATE->checkUserSymbol(name); }
+ sortSymbol[t]
+ LPAREN_TOK
+ ( term[e, e2]
+ { terms.push_back( e ); }
+ )* RPAREN_TOK
+ { Trace("parser") << "declare pool: '" << name << "'" << std::endl;
+ cvc5::Term pool = SOLVER->declarePool(name, t, terms);
+ PARSER_STATE->defineVar(name, pool);
+ cmd->reset(new DeclarePoolCommand(name, pool, t, terms));
+ }
+ | BLOCK_MODEL_TOK KEYWORD { PARSER_STATE->checkThatLogicIsSet(); }
+ {
+ modes::BlockModelsMode mode =
+ PARSER_STATE->getBlockModelsMode(
+ AntlrInput::tokenText($KEYWORD).c_str() + 1);
+ cmd->reset(new BlockModelCommand(mode));
+ }
| BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( LPAREN_TOK termList[terms,e] RPAREN_TOK
{ cmd->reset(new BlockModelValuesCommand(terms)); }
datatypeDefCommand[bool isCo, std::unique_ptr<cvc5::Command>* cmd]
@declarations {
- std::vector<api::DatatypeDecl> dts;
+ std::vector<cvc5::DatatypeDecl> dts;
std::string name;
std::vector<std::string> dnames;
std::vector<int> arities;
datatypesDefCommand[bool isCo, std::unique_ptr<cvc5::Command>* cmd]
@declarations {
- std::vector<api::DatatypeDecl> dts;
+ std::vector<cvc5::DatatypeDecl> dts;
std::string name;
std::vector<std::string> dnames;
std::vector<int> arities;
LPAREN_TOK /* datatype definition prelude */
( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL RPAREN_TOK
{ unsigned arity = AntlrInput::tokenToUnsigned(n);
- Debug("parser-dt") << "Datatype : " << name << ", arity = " << arity << std::endl;
+ Trace("parser-dt") << "Datatype : " << name << ", arity = " << arity << std::endl;
dnames.push_back(name);
arities.push_back( static_cast<int>(arity) );
}
const std::vector<int>& arities,
std::unique_ptr<cvc5::Command>* cmd]
@declarations {
- std::vector<api::DatatypeDecl> dts;
+ std::vector<cvc5::DatatypeDecl> dts;
std::string name;
- std::vector<api::Sort> params;
+ std::vector<cvc5::Sort> params;
}
: { PARSER_STATE->pushScope();
// Declare the datatypes that are currently being defined as unresolved
}
( LPAREN_TOK {
params.clear();
- Debug("parser-dt") << "Processing datatype #" << dts.size() << std::endl;
+ Trace("parser-dt") << "Processing datatype #" << dts.size() << std::endl;
if( dts.size()>=dnames.size() ){
PARSER_STATE->parseError("Too many datatypes defined in this block.");
}
// 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;
+ Trace("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()], params, isCo));
}
LPAREN_TOK
// 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;
+ Trace("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()],
params,
isCo));
{ s = AntlrInput::tokenText($HEX_LITERAL); }
| BINARY_LITERAL
{ s = AntlrInput::tokenText($BINARY_LITERAL); }
- | str[s,false]
- | symbol[s,CHECK_NONE,SYM_SORT]
+ | SIMPLE_SYMBOL
+ { s = AntlrInput::tokenText($SIMPLE_SYMBOL); }
+ | QUOTED_SYMBOL
+ { s = AntlrInput::tokenText($QUOTED_SYMBOL); }
+ | STRING_LITERAL
+ { s = AntlrInput::tokenText($STRING_LITERAL); }
| tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
| DECLARE_SORT_TOK
| DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK
| DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK
| GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_ASSUMPTIONS_TOK
- | GET_UNSAT_CORE_TOK | EXIT_TOK
+ | GET_UNSAT_CORE_TOK | GET_DIFFICULTY_TOK | EXIT_TOK
| RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK
| GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK
| DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK)
| KEYWORD { s = AntlrInput::tokenText($KEYWORD); }
;
-symbolicExpr[cvc5::api::Term& sexpr]
+symbolicExpr[cvc5::Term& sexpr]
@declarations {
std::string s;
- std::vector<api::Term> children;
+ std::vector<cvc5::Term> children;
}
: simpleSymbolicExpr[s]
{ sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); }
| LPAREN_TOK
( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK
- { sexpr = SOLVER->mkTerm(cvc5::api::SEXPR, children); }
+ { sexpr = SOLVER->mkTerm(cvc5::SEXPR, children); }
;
/**
* Matches a term.
* @return the expression representing the term.
*/
-term[cvc5::api::Term& expr, cvc5::api::Term& expr2]
+term[cvc5::Term& expr, cvc5::Term& expr2]
@init {
- api::Kind kind = api::NULL_EXPR;
- cvc5::api::Term f;
+ cvc5::Kind kind = cvc5::NULL_TERM;
+ cvc5::Term f;
std::string name;
- cvc5::api::Sort type;
+ cvc5::Sort type;
ParseOp p;
}
: termNonVariable[expr, expr2]
* @return the expression expr representing the term or formula, and expr2, an
* optional annotation for expr (for instance, for attributed expressions).
*/
-termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2]
+termNonVariable[cvc5::Term& expr, cvc5::Term& expr2]
@init {
- Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
- api::Kind kind = api::NULL_EXPR;
+ Trace("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
+ cvc5::Kind kind = cvc5::NULL_TERM;
std::string name;
- std::vector<cvc5::api::Term> args;
- std::vector< std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
- cvc5::api::Term bvl;
- cvc5::api::Term f, f2, f3;
+ std::vector<cvc5::Term> args;
+ std::vector< std::pair<std::string, cvc5::Sort> > sortedVarNames;
+ cvc5::Term bvl;
+ cvc5::Term f, f2, f3;
std::string attr;
- cvc5::api::Term attexpr;
- std::vector<cvc5::api::Term> patexprs;
- std::vector<cvc5::api::Term> matchcases;
+ cvc5::Term attexpr;
+ std::vector<cvc5::Term> patexprs;
+ std::vector<cvc5::Term> matchcases;
std::unordered_set<std::string> names;
- std::vector< std::pair<std::string, cvc5::api::Term> > binders;
- cvc5::api::Sort type;
- cvc5::api::Sort type2;
- api::Term atomTerm;
+ std::vector< std::pair<std::string, cvc5::Term> > binders;
+ cvc5::Sort type;
+ cvc5::Sort type2;
+ cvc5::Term atomTerm;
ParseOp p;
- std::vector<api::Sort> argTypes;
+ std::vector<cvc5::Sort> argTypes;
}
: LPAREN_TOK quantOp[kind]
{
- if (!PARSER_STATE->isTheoryEnabled(theory::THEORY_QUANTIFIERS))
+ if (!PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_QUANTIFIERS))
{
PARSER_STATE->parseError("Quantifier used in non-quantified logic.");
}
}
expr = MK_TERM(kind, args);
}
- | LPAREN_TOK COMPREHENSION_TOK
+ | LPAREN_TOK SET_COMPREHENSION_TOK
{ PARSER_STATE->pushScope(); }
boundVarList[bvl]
{
term[f, f2] { args.push_back(f); }
term[f, f2] {
args.push_back(f);
- expr = MK_TERM(api::COMPREHENSION, args);
+ expr = MK_TERM(cvc5::SET_COMPREHENSION, args);
}
RPAREN_TOK
| LPAREN_TOK qualIdentifier[p]
}
binders.push_back(std::make_pair(name, expr)); } )+
{ // now implement these bindings
- for (const std::pair<std::string, api::Term>& binder : binders)
+ for (const std::pair<std::string, cvc5::Term>& binder : binders)
{
{
PARSER_STATE->defineVar(binder.first, binder.second);
PARSER_STATE->pushScope();
// f should be a constructor
type = f.getSort();
- Debug("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
- if (!type.isConstructor())
+ Trace("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
+ if (!type.isDatatypeConstructor())
{
PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
}
- api::Datatype dt = type.getConstructorCodomainSort().getDatatype();
+ cvc5::Datatype dt =
+ type.getDatatypeConstructorCodomainSort().getDatatype();
if (dt.isParametric())
{
// lookup constructor by name
- api::DatatypeConstructor dc = dt.getConstructor(f.toString());
- api::Term scons = dc.getSpecializedConstructorTerm(expr.getSort());
+ cvc5::DatatypeConstructor dc = dt.getConstructor(f.toString());
+ cvc5::Term scons = dc.getInstantiatedTerm(expr.getSort());
// take the type of the specialized constructor instead
type = scons.getSort();
}
- argTypes = type.getConstructorDomainSorts();
+ argTypes = type.getDatatypeConstructorDomainSorts();
}
// arguments of the pattern
( symbol[name,CHECK_NONE,SYM_VARIABLE] {
PARSER_STATE->parseError("Too many arguments for pattern.");
}
//make of proper type
- api::Term arg = PARSER_STATE->bindBoundVar(name, argTypes[args.size()]);
+ cvc5::Term arg = PARSER_STATE->bindBoundVar(name, argTypes[args.size()]);
args.push_back( arg );
}
)*
RPAREN_TOK term[f3, f2] {
// make the match case
- std::vector<cvc5::api::Term> cargs;
+ std::vector<cvc5::Term> cargs;
cargs.push_back(f);
cargs.insert(cargs.end(),args.begin(),args.end());
- api::Term c = MK_TERM(api::APPLY_CONSTRUCTOR,cargs);
- api::Term bvla = MK_TERM(api::BOUND_VAR_LIST,args);
- api::Term mc = MK_TERM(api::MATCH_BIND_CASE, bvla, c, f3);
+ cvc5::Term c = MK_TERM(cvc5::APPLY_CONSTRUCTOR,cargs);
+ cvc5::Term bvla = MK_TERM(cvc5::VARIABLE_LIST,args);
+ cvc5::Term mc = MK_TERM(cvc5::MATCH_BIND_CASE, bvla, c, f3);
matchcases.push_back(mc);
// now, pop the scope
PARSER_STATE->popScope();
{
f = PARSER_STATE->getVariable(name);
type = f.getSort();
- if (!type.isConstructor() ||
- !type.getConstructorDomainSorts().empty())
+ if (!type.isDatatypeConstructor() ||
+ !type.getDatatypeConstructorDomainSorts().empty())
{
PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern.");
}
// make nullary constructor application
- f = MK_TERM(api::APPLY_CONSTRUCTOR, f);
+ f = MK_TERM(cvc5::APPLY_CONSTRUCTOR, f);
}
else
{
}
}
term[f3, f2] {
- api::Term mc;
- if (f.getKind() == api::VARIABLE)
+ cvc5::Term mc;
+ if (f.getKind() == cvc5::VARIABLE)
{
- api::Term bvlf = MK_TERM(api::BOUND_VAR_LIST, f);
- mc = MK_TERM(api::MATCH_BIND_CASE, bvlf, f, f3);
+ cvc5::Term bvlf = MK_TERM(cvc5::VARIABLE_LIST, f);
+ mc = MK_TERM(cvc5::MATCH_BIND_CASE, bvlf, f, f3);
}
else
{
- mc = MK_TERM(api::MATCH_CASE, f, f3);
+ mc = MK_TERM(cvc5::MATCH_CASE, f, f3);
}
matchcases.push_back(mc);
}
{
PARSER_STATE->parseError("Must have at least one case in match.");
}
- std::vector<api::Term> mchildren;
+ std::vector<cvc5::Term> mchildren;
mchildren.push_back(expr);
mchildren.insert(mchildren.end(), matchcases.begin(), matchcases.end());
- expr = MK_TERM(api::MATCH, mchildren);
+ expr = MK_TERM(cvc5::MATCH, mchildren);
}
/* attributed expressions */
| LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
- ( attribute[expr, attexpr, attr]
+ ( attribute[expr, attexpr]
{ if( ! attexpr.isNull()) {
patexprs.push_back( attexpr );
}
)+ RPAREN_TOK
{
if(! patexprs.empty()) {
- if( !f2.isNull() && f2.getKind()==api::INST_PATTERN_LIST ){
+ if( !f2.isNull() && f2.getKind()==cvc5::INST_PATTERN_LIST ){
for( size_t i=0; i<f2.getNumChildren(); i++ ){
- if( f2[i].getKind()==api::INST_PATTERN ){
- patexprs.push_back( f2[i] );
- }else{
- std::stringstream ss;
- ss << "warning: rewrite rules do not support " << f2[i]
- << " within instantiation pattern list";
- PARSER_STATE->warning(ss.str());
- }
+ patexprs.push_back( f2[i] );
}
}
- expr2 = MK_TERM(api::INST_PATTERN_LIST, patexprs);
+ expr2 = MK_TERM(cvc5::INST_PATTERN_LIST, patexprs);
} else {
expr2 = f2;
}
args.push_back(bvl);
args.push_back(f);
PARSER_STATE->popScope();
- expr = MK_TERM(api::LAMBDA, args);
+ expr = MK_TERM(cvc5::LAMBDA, args);
}
| LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK
{
- std::vector<api::Sort> sorts;
- std::vector<api::Term> terms;
- for (const api::Term& arg : args)
+ std::vector<cvc5::Sort> sorts;
+ std::vector<cvc5::Term> terms;
+ for (const cvc5::Term& arg : args)
{
sorts.emplace_back(arg.getSort());
terms.emplace_back(arg);
| LPAREN_TOK TUPLE_PROJECT_TOK term[expr,expr2] RPAREN_TOK
{
std::vector<uint32_t> indices;
- api::Op op = SOLVER->mkOp(api::TUPLE_PROJECT, indices);
- expr = SOLVER->mkTerm(op, expr);
+ cvc5::Op op = SOLVER->mkOp(cvc5::TUPLE_PROJECT, indices);
+ expr = SOLVER->mkTerm(op, {expr});
}
| /* an atomic term (a term with no subterms) */
termAtomic[atomTerm] { expr = atomTerm; }
* - For declared functions f, we return (2).
* - For indexed functions like testers (_ is C) and bitvector extract
* (_ extract n m), we return (3) for the appropriate operator.
- * - For tuple selectors (_ tupSel n), we return (1) and (3). api::Kind is set to
- * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the
- * caller as the n^th generic tuple selector. We do this since there is no
- * AST expression representing generic tuple select, and we do not have enough
- * type information at this point to know the type of the tuple we will be
- * selecting from.
+ * - For tuple selectors (_ tuple_select n) and updaters (_ tuple_update n), we
+ * return (1) and (3). cvc5::Kind is set to APPLY_SELECTOR or APPLY_UPDATER
+ * respectively, and expr is set to n, which is to be interpreted by the
+ * caller as the n^th generic tuple selector or updater. We do this since there
+ * is no AST expression representing generic tuple select, and we do not have
+ * enough type information at this point to know the type of the tuple we will
+ * be selecting from.
*
* (Ascripted Identifiers)
*
* as (3).
* - Overloaded non-parametric constructors (as C T) return the appropriate
* expression, analogous to the parametric cases above.
- * - For other ascripted nullary constants like (as emptyset (Set T)),
+ * - For other ascripted nullary constants like (as set.empty (Set T)),
* (as sep.nil T), we return the appropriate expression (3).
* - For array constant specifications (as const (Array T1 T2)), we return (1)
* and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2),
*/
qualIdentifier[cvc5::ParseOp& p]
@init {
- api::Kind k;
+ cvc5::Kind k;
std::string baseName;
- cvc5::api::Term f;
- cvc5::api::Sort type;
+ cvc5::Term f;
+ cvc5::Sort type;
}
: identifier[p]
| LPAREN_TOK AS_TOK
- ( CONST_TOK sortSymbol[type, CHECK_DECLARED]
+ ( CONST_TOK sortSymbol[type]
{
- p.d_kind = api::CONST_ARRAY;
+ p.d_kind = cvc5::CONST_ARRAY;
PARSER_STATE->parseOpApplyTypeAscription(p, type);
}
| identifier[p]
- sortSymbol[type, CHECK_DECLARED]
+ sortSymbol[type]
{
PARSER_STATE->parseOpApplyTypeAscription(p, type);
}
*/
identifier[cvc5::ParseOp& p]
@init {
- cvc5::api::Term f;
- cvc5::api::Term f2;
- std::vector<uint64_t> numerals;
+ cvc5::Term f;
+ cvc5::Term f2;
+ std::vector<uint32_t> numerals;
+ std::string opName;
}
: functionName[p.d_name, CHECK_NONE]
| LPAREN_TOK INDEX_TOK
( TESTER_TOK term[f, f2]
{
- if (f.getKind() == api::APPLY_CONSTRUCTOR && f.getNumChildren() == 1)
+ if (f.getKind() == cvc5::APPLY_CONSTRUCTOR && f.getNumChildren() == 1)
{
// for nullary constructors, must get the operator
f = f[0];
}
- if (!f.getSort().isConstructor())
+ if (!f.getSort().isDatatypeConstructor())
{
PARSER_STATE->parseError(
- "Bad syntax for test (_ is X), X must be a constructor.");
+ "Bad syntax for (_ is X), X must be a constructor.");
}
// get the datatype that f belongs to
- api::Sort sf = f.getSort().getConstructorCodomainSort();
- api::Datatype d = sf.getDatatype();
+ cvc5::Sort sf = f.getSort().getDatatypeConstructorCodomainSort();
+ cvc5::Datatype d = sf.getDatatype();
// lookup by name
- api::DatatypeConstructor dc = d.getConstructor(f.toString());
+ cvc5::DatatypeConstructor dc = d.getConstructor(f.toString());
p.d_expr = dc.getTesterTerm();
}
- | TUPLE_SEL_TOK m=INTEGER_LITERAL
+ | UPDATE_TOK term[f, f2]
{
- // we adopt a special syntax (_ tupSel n)
- p.d_kind = api::APPLY_SELECTOR;
- // put m in expr so that the caller can deal with this case
- p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m));
+ if (!f.getSort().isDatatypeSelector())
+ {
+ PARSER_STATE->parseError(
+ "Bad syntax for (_ update X), X must be a selector.");
+ }
+ std::string sname = f.toString();
+ // get the datatype that f belongs to
+ cvc5::Sort sf = f.getSort().getDatatypeSelectorDomainSort();
+ cvc5::Datatype d = sf.getDatatype();
+ // find the selector
+ cvc5::DatatypeSelector ds = d.getSelector(f.toString());
+ // get the updater term
+ p.d_expr = ds.getUpdaterTerm();
}
| TUPLE_PROJECT_TOK nonemptyNumeralList[numerals]
{
- // we adopt a special syntax (_ tuple_project i_1 ... i_n) where
+ // we adopt a special syntax (_ tuple.project i_1 ... i_n) where
// i_1, ..., i_n are numerals
- p.d_kind = api::TUPLE_PROJECT;
- std::vector<uint32_t> indices(numerals.size());
- for(size_t i = 0; i < numerals.size(); ++i)
- {
- // convert uint64_t to uint32_t
- indices[i] = numerals[i];
- }
- p.d_op = SOLVER->mkOp(api::TUPLE_PROJECT, indices);
+ p.d_kind = cvc5::TUPLE_PROJECT;
+ p.d_op = SOLVER->mkOp(cvc5::TUPLE_PROJECT, numerals);
}
- | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
+ | functionName[opName, CHECK_NONE] nonemptyNumeralList[numerals]
{
- p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals);
+ cvc5::Kind k = PARSER_STATE->getIndexedOpKind(opName);
+ if (k == cvc5::UNDEFINED_KIND)
+ {
+ // We don't know which kind to use until we know the type of the
+ // arguments
+ p.d_name = opName;
+ p.d_indices = numerals;
+ p.d_kind = cvc5::UNDEFINED_KIND;
+ }
+ else if (k == cvc5::APPLY_SELECTOR || k == cvc5::APPLY_UPDATER)
+ {
+ // we adopt a special syntax (_ tuple_select n) and (_ tuple_update n)
+ // for tuple selectors and updaters
+ if (numerals.size() != 1)
+ {
+ PARSER_STATE->parseError(
+ "Unexpected syntax for tuple selector or updater.");
+ }
+ // The operator is dependent upon inferring the type of the arguments,
+ // and hence the type is not available yet. Hence, we remember the
+ // index as a numeral in the parse operator.
+ p.d_kind = k;
+ p.d_expr = SOLVER->mkInteger(numerals[0]);
+ }
+ else if (numerals.size() == 1 || numerals.size() == 2)
+ {
+ p.d_op = SOLVER->mkOp(k, numerals);
+ }
+ else
+ {
+ PARSER_STATE->parseError(
+ "Unexpected number of numerals for indexed symbol.");
+ }
}
)
RPAREN_TOK
* Matches an atomic term (a term with no subterms).
* @return the expression expr representing the term or formula.
*/
-termAtomic[cvc5::api::Term& atomTerm]
+termAtomic[cvc5::Term& atomTerm]
@init {
- cvc5::api::Sort type;
- cvc5::api::Sort type2;
+ cvc5::Sort t;
std::string s;
- std::vector<uint64_t> numerals;
+ std::vector<uint32_t> numerals;
}
/* constants */
: INTEGER_LITERAL
{
std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL);
- atomTerm = SOLVER->mkInteger(intStr);
+ atomTerm = PARSER_STATE->mkRealOrIntFromNumeral(intStr);
}
| DECIMAL_LITERAL
{
std::string realStr = AntlrInput::tokenText($DECIMAL_LITERAL);
- atomTerm = SOLVER->ensureTermSort(SOLVER->mkReal(realStr),
- SOLVER->getRealSort());
+ atomTerm = SOLVER->mkReal(realStr);
}
// Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity
// as a 32-bit floating-point constant)
| LPAREN_TOK INDEX_TOK
- ( EMP_TOK
- sortSymbol[type,CHECK_DECLARED]
- sortSymbol[type2,CHECK_DECLARED]
+ ( CHAR_TOK HEX_LITERAL
{
- // Empty heap constant in seperation logic
- api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
- api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2");
- atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
+ std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
+ atomTerm = PARSER_STATE->mkCharConstant(hexStr);
}
- | CHAR_TOK HEX_LITERAL
+ | FMF_CARD_TOK sortSymbol[t] INTEGER_LITERAL
{
- std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
- atomTerm = SOLVER->mkChar(hexStr);
+ uint32_t ubound = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+ atomTerm = SOLVER->mkCardinalityConstraint(t, ubound);
}
| sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
{
{
Assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0);
std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
- atomTerm = SOLVER->mkBitVector(hexStr, 16);
+ atomTerm = SOLVER->mkBitVector(hexStr.size() * 4, hexStr, 16);
}
| BINARY_LITERAL
{
Assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0);
std::string binStr = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
- atomTerm = SOLVER->mkBitVector(binStr, 2);
+ atomTerm = SOLVER->mkBitVector(binStr.size(), binStr, 2);
}
// String constant
- | str[s,false] { atomTerm = PARSER_STATE->mkStringConstant(s); }
+ | str[s] { atomTerm = PARSER_STATE->mkStringConstant(s); }
// NOTE: Theory constants go here
// Empty tuple constant
| TUPLE_CONST_TOK
{
- atomTerm = SOLVER->mkTuple(std::vector<api::Sort>(),
- std::vector<api::Term>());
+ atomTerm = SOLVER->mkTuple(std::vector<cvc5::Sort>(),
+ std::vector<cvc5::Term>());
}
;
/**
* Read attribute
*/
-attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr, std::string& attr]
+attribute[cvc5::Term& expr, cvc5::Term& retExpr]
@init {
- api::Term sexpr;
+ cvc5::Term sexpr;
std::string s;
- cvc5::api::Term patexpr;
- std::vector<cvc5::api::Term> patexprs;
- cvc5::api::Term e2;
+ cvc5::Term patexpr;
+ std::vector<cvc5::Term> patexprs;
+ cvc5::Term e2;
bool hasValue = false;
+ cvc5::Kind k;
}
: KEYWORD ( simpleSymbolicExprNoKeyword[s] { hasValue = true; } )?
{
- attr = AntlrInput::tokenText($KEYWORD);
- PARSER_STATE->attributeNotSupported(attr);
+ PARSER_STATE->attributeNotSupported(AntlrInput::tokenText($KEYWORD));
}
- | ATTRIBUTE_PATTERN_TOK LPAREN_TOK
+ | ( ATTRIBUTE_PATTERN_TOK { k = cvc5::INST_PATTERN; } |
+ ATTRIBUTE_POOL_TOK { k = cvc5::INST_POOL; } |
+ ATTRIBUTE_INST_ADD_TO_POOL_TOK { k = cvc5::INST_ADD_TO_POOL; } |
+ ATTRIBUTE_SKOLEM_ADD_TO_POOL_TOK{ k = cvc5::SKOLEM_ADD_TO_POOL; }
+ )
+ LPAREN_TOK
( term[patexpr, e2]
{ patexprs.push_back( patexpr ); }
)+ RPAREN_TOK
{
- attr = std::string(":pattern");
- retExpr = MK_TERM(api::INST_PATTERN, patexprs);
+ retExpr = MK_TERM(k, patexprs);
}
| ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2]
{
- attr = std::string(":no-pattern");
- retExpr = MK_TERM(api::INST_NO_PATTERN, patexpr);
+ retExpr = MK_TERM(cvc5::INST_NO_PATTERN, patexpr);
}
| tok=( ATTRIBUTE_INST_LEVEL ) INTEGER_LITERAL
{
std::stringstream sIntLit;
sIntLit << $INTEGER_LITERAL;
- api::Term n = SOLVER->mkInteger(sIntLit.str());
- std::vector<api::Term> values;
- values.push_back( n );
- std::string attr_name(AntlrInput::tokenText($tok));
- attr_name.erase( attr_name.begin() );
- api::Sort boolType = SOLVER->getBooleanSort();
- api::Term avar = PARSER_STATE->bindVar(attr_name, boolType);
- retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
- Command* c = new SetUserAttributeCommand(attr_name, avar, values);
- c->setMuted(true);
- PARSER_STATE->preemptCommand(c);
- }
- | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr]
+ cvc5::Term keyword = SOLVER->mkString("quant-inst-max-level");
+ cvc5::Term n = SOLVER->mkInteger(sIntLit.str());
+ retExpr = MK_TERM(cvc5::INST_ATTRIBUTE, keyword, n);
+ }
+ | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbol[s,CHECK_UNDECLARED,SYM_VARIABLE]
{
- api::Sort boolType = SOLVER->getBooleanSort();
- api::Term avar = SOLVER->mkConst(boolType, sexprToString(sexpr));
- attr = std::string(":qid");
- retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
- Command* c = new SetUserAttributeCommand("qid", avar);
- c->setMuted(true);
- PARSER_STATE->preemptCommand(c);
- }
- | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
+ cvc5::Term keyword = SOLVER->mkString("qid");
+ // must create a variable whose name is the name of the quantified
+ // formula, not a string.
+ cvc5::Term name = SOLVER->mkConst(SOLVER->getBooleanSort(), s);
+ retExpr = MK_TERM(cvc5::INST_ATTRIBUTE, keyword, name);
+ }
+ | ATTRIBUTE_NAMED_TOK symbol[s,CHECK_UNDECLARED,SYM_VARIABLE]
{
- attr = std::string(":named");
// notify that expression was given a name
- PARSER_STATE->notifyNamedExpression(expr, sexprToString(sexpr));
+ DefineFunctionCommand* defFunCmd =
+ new DefineFunctionCommand(s, expr.getSort(), expr);
+ defFunCmd->setMuted(true);
+ PARSER_STATE->preemptCommand(defFunCmd);
+ PARSER_STATE->notifyNamedExpression(expr, s);
}
;
* Matches a sequence of terms and puts them into the formulas
* vector.
* @param formulas the vector to fill with terms
- * @param expr an cvc5::api::Term reference for the elements of the sequence
+ * @param expr an cvc5::Term reference for the elements of the sequence
*/
-/* NOTE: We pass an cvc5::api::Term in here just to avoid allocating a fresh cvc5::api::Term every
+/* NOTE: We pass an cvc5::Term in here just to avoid allocating a fresh cvc5::Term every
* time through this rule. */
-termList[std::vector<cvc5::api::Term>& formulas, cvc5::api::Term& expr]
+termList[std::vector<cvc5::Term>& formulas, cvc5::Term& expr]
@declarations {
- cvc5::api::Term expr2;
+ cvc5::Term expr2;
}
: ( term[expr, expr2] { formulas.push_back(expr); } )+
;
/**
* Matches a string, and strips off the quotes.
*/
-str[std::string& s, bool fsmtlib]
+str[std::string& s]
: STRING_LITERAL
{
s = AntlrInput::tokenText($STRING_LITERAL);
"as escape sequences");
}
}
- if (fsmtlib || PARSER_STATE->escapeDupDblQuote())
+ char* p_orig = strdup(s.c_str());
+ char *p = p_orig, *q = p_orig;
+ while (*q != '\0')
{
- char* p_orig = strdup(s.c_str());
- char *p = p_orig, *q = p_orig;
- while (*q != '\0')
+ if (*q == '"')
{
- if (PARSER_STATE->escapeDupDblQuote() && *q == '"')
- {
- // Handle SMT-LIB >=2.5 standard escape '""'.
- ++q;
- Assert(*q == '"');
- }
- else if (!PARSER_STATE->escapeDupDblQuote() && *q == '\\')
- {
- ++q;
- // Handle SMT-LIB 2.0 standard escapes '\\' and '\"'.
- if (*q != '\\' && *q != '"')
- {
- Assert(*q != '\0');
- *p++ = '\\';
- }
- }
- *p++ = *q++;
+ // Handle SMT-LIB >=2.5 standard escape '""'.
+ ++q;
+ Assert(*q == '"');
}
- *p = '\0';
- s = p_orig;
- free(p_orig);
+ *p++ = *q++;
}
+ *p = '\0';
+ s = p_orig;
+ free(p_orig);
}
;
-quantOp[cvc5::api::Kind& kind]
+quantOp[cvc5::Kind& kind]
@init {
- Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
+ Trace("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- : EXISTS_TOK { $kind = api::EXISTS; }
- | FORALL_TOK { $kind = api::FORALL; }
+ : EXISTS_TOK { $kind = cvc5::EXISTS; }
+ | FORALL_TOK { $kind = cvc5::FORALL; }
;
/**
* Matches a sequence of sort symbols and fills them into the given
* vector.
*/
-sortList[std::vector<cvc5::api::Sort>& sorts]
+sortList[std::vector<cvc5::Sort>& sorts]
@declarations {
- cvc5::api::Sort t;
+ cvc5::Sort t;
}
- : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
+ : ( sortSymbol[t] { sorts.push_back(t); } )*
;
-nonemptySortList[std::vector<cvc5::api::Sort>& sorts]
+nonemptySortList[std::vector<cvc5::Sort>& sorts]
@declarations {
- cvc5::api::Sort t;
+ cvc5::Sort t;
}
- : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
+ : ( sortSymbol[t] { sorts.push_back(t); } )+
;
/**
* Matches a sequence of (variable,sort) symbol pairs and fills them
* into the given vector.
*/
-sortedVarList[std::vector<std::pair<std::string, cvc5::api::Sort> >& sortedVars]
+sortedVarList[std::vector<std::pair<std::string, cvc5::Sort> >& sortedVars]
@declarations {
std::string name;
- cvc5::api::Sort t;
+ cvc5::Sort t;
}
: ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
- sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
+ sortSymbol[t] RPAREN_TOK
{ sortedVars.push_back(make_pair(name, t)); }
)*
;
* Matches a sequence of (variable, sort) symbol pairs, registers them as bound
* variables, and returns a term corresponding to the list of pairs.
*/
-boundVarList[cvc5::api::Term& expr]
+boundVarList[cvc5::Term& expr]
@declarations {
- std::vector<std::pair<std::string, cvc5::api::Sort>> sortedVarNames;
+ std::vector<std::pair<std::string, cvc5::Sort>> sortedVarNames;
}
: LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
{
- std::vector<cvc5::api::Term> args =
+ std::vector<cvc5::Term> args =
PARSER_STATE->bindBoundVars(sortedVarNames);
- expr = MK_TERM(api::BOUND_VAR_LIST, args);
+ expr = MK_TERM(cvc5::VARIABLE_LIST, args);
}
;
: symbol[name,check,SYM_SORT]
;
-sortSymbol[cvc5::api::Sort& t, cvc5::parser::DeclarationCheck check]
+sortSymbol[cvc5::Sort& t]
@declarations {
std::string name;
- std::vector<cvc5::api::Sort> args;
- std::vector<uint64_t> numerals;
+ std::vector<cvc5::Sort> args;
+ std::vector<uint32_t> numerals;
bool indexed = false;
}
: sortName[name,CHECK_NONE]
{
- if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) {
- t = PARSER_STATE->getSort(name);
- } else {
- t = PARSER_STATE->mkUnresolvedType(name);
- }
+ t = PARSER_STATE->getSort(name);
}
| LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;})
symbol[name,CHECK_NONE,SYM_SORT]
if( numerals.size() != 2 ) {
PARSER_STATE->parseError("Illegal floating-point type.");
}
- if(!validExponentSize(numerals[0])) {
+ if(!internal::validExponentSize(numerals[0])) {
PARSER_STATE->parseError("Illegal floating-point exponent size");
}
- if(!validSignificandSize(numerals[1])) {
+ if(!internal::validSignificandSize(numerals[1])) {
PARSER_STATE->parseError("Illegal floating-point significand size");
}
t = SOLVER->mkFloatingPointSort(numerals[0],numerals[1]);
PARSER_STATE->parseError("Extra parentheses around sort name not "
"permitted in SMT-LIB");
} else if(name == "Array" &&
- PARSER_STATE->isTheoryEnabled(theory::THEORY_ARRAYS) ) {
+ PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_ARRAYS) ) {
if(args.size() != 2) {
PARSER_STATE->parseError("Illegal array type.");
}
t = SOLVER->mkArraySort( args[0], args[1] );
} else if(name == "Set" &&
- PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) ) {
+ PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_SETS) ) {
if(args.size() != 1) {
PARSER_STATE->parseError("Illegal set type.");
}
t = SOLVER->mkSetSort( args[0] );
}
else if(name == "Bag" &&
- PARSER_STATE->isTheoryEnabled(theory::THEORY_BAGS) ) {
+ PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_BAGS) ) {
if(args.size() != 1) {
PARSER_STATE->parseError("Illegal bag type.");
}
t = SOLVER->mkBagSort( args[0] );
}
else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() &&
- PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) ) {
+ PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_STRINGS) ) {
if(args.size() != 1) {
PARSER_STATE->parseError("Illegal sequence type.");
}
t = SOLVER->mkSequenceSort( args[0] );
} else if (name == "Tuple" && !PARSER_STATE->strictModeEnabled()) {
t = SOLVER->mkTupleSort(args);
- } else if(check == CHECK_DECLARED ||
- PARSER_STATE->isDeclared(name, SYM_SORT)) {
- t = PARSER_STATE->getSort(name, args);
} else {
- // make unresolved type
- if(args.empty()) {
- t = PARSER_STATE->mkUnresolvedType(name);
- Debug("parser-param") << "param: make unres type " << name
- << std::endl;
- } else {
- t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
- t = t.instantiate( args );
- Debug("parser-param")
- << "param: make unres param type " << name << " " << args.size()
- << " " << PARSER_STATE->getArity( name ) << std::endl;
- }
+ t = PARSER_STATE->getSort(name, args);
}
}
) RPAREN_TOK
PARSER_STATE->parseError("Arrow types must have at least 2 arguments");
}
//flatten the type
- api::Sort rangeType = args.back();
+ cvc5::Sort rangeType = args.back();
args.pop_back();
t = PARSER_STATE->mkFlatFunctionType( args, rangeType );
}
: SIMPLE_SYMBOL
{ id = AntlrInput::tokenText($SIMPLE_SYMBOL);
if(!PARSER_STATE->isAbstractValue(id)) {
- // if an abstract value, SmtEngine handles declaration
+ // if an abstract value, SolverEngine handles declaration
PARSER_STATE->checkDeclaration(id, check, type);
}
}
/* strip off the quotes */
id = id.substr(1, id.size() - 2);
if(!PARSER_STATE->isAbstractValue(id)) {
- // if an abstract value, SmtEngine handles declaration
+ // if an abstract value, SolverEngine handles declaration
PARSER_STATE->checkDeclaration(id, check, type);
}
}
* Matches a nonempty list of numerals.
* @param numerals the (empty) vector to house the numerals.
*/
-nonemptyNumeralList[std::vector<uint64_t>& numerals]
+nonemptyNumeralList[std::vector<uint32_t>& numerals]
: ( INTEGER_LITERAL
{ numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
)+
/**
* Parses a datatype definition
*/
-datatypeDef[bool isCo, std::vector<cvc5::api::DatatypeDecl>& datatypes,
- std::vector< cvc5::api::Sort >& params]
+datatypeDef[bool isCo, std::vector<cvc5::DatatypeDecl>& datatypes,
+ std::vector< cvc5::Sort >& params]
@init {
std::string id;
}
/**
* Parses a constructor defintion for type
*/
-constructorDef[cvc5::api::DatatypeDecl& type]
+constructorDef[cvc5::DatatypeDecl& type]
@init {
std::string id;
- cvc5::api::DatatypeConstructorDecl* ctor = NULL;
+ cvc5::DatatypeConstructorDecl* ctor = NULL;
}
: symbol[id,CHECK_NONE,SYM_VARIABLE]
{
- ctor = new api::DatatypeConstructorDecl(
+ ctor = new cvc5::DatatypeConstructorDecl(
SOLVER->mkDatatypeConstructorDecl(id));
}
( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
{ // make the constructor
type.addConstructor(*ctor);
- Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
+ Trace("parser-idt") << "constructor: " << id.c_str() << std::endl;
delete ctor;
}
;
-selector[cvc5::api::DatatypeConstructorDecl& ctor]
+selector[cvc5::DatatypeConstructorDecl& ctor]
@init {
std::string id;
- cvc5::api::Sort t, t2;
+ cvc5::Sort t, t2;
}
- : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE]
+ : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t]
{
ctor.addSelector(id, t);
- Debug("parser-idt") << "selector: " << id.c_str()
+ Trace("parser-idt") << "selector: " << id.c_str()
<< " of type " << t << std::endl;
}
;
GET_PROOF_TOK : 'get-proof';
GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions';
GET_UNSAT_CORE_TOK : 'get-unsat-core';
+GET_DIFFICULTY_TOK : 'get-difficulty';
+GET_LEARNED_LITERALS_TOK : { !PARSER_STATE->strictModeEnabled() }? 'get-learned-literals';
EXIT_TOK : 'exit';
RESET_TOK : 'reset';
RESET_ASSERTIONS_TOK : 'reset-assertions';
CONST_TOK : { !PARSER_STATE->strictModeEnabled() }? 'const';
// extended commands
-DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-codatatype';
-DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-datatype';
-DECLARE_DATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-datatypes';
-DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-datatypes';
-DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes';
-DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes';
-PAR_TOK : { PARSER_STATE->v2_6() }?'par';
-COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) }?'comprehension';
-TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'is';
-MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'match';
+DECLARE_CODATATYPE_TOK : 'declare-codatatype';
+DECLARE_DATATYPE_TOK : 'declare-datatype';
+DECLARE_DATATYPES_TOK : 'declare-datatypes';
+DECLARE_CODATATYPES_TOK : 'declare-codatatypes';
+PAR_TOK : 'par';
+SET_COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_SETS) }?'set.comprehension';
+TESTER_TOK : { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }?'is';
+UPDATE_TOK : { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }?'update';
+MATCH_TOK : { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }?'match';
GET_MODEL_TOK : 'get-model';
BLOCK_MODEL_TOK : 'block-model';
BLOCK_MODEL_VALUES_TOK : 'block-model-values';
DECLARE_SORTS_TOK : 'declare-sorts';
DECLARE_FUNS_TOK : 'declare-funs';
DECLARE_PREDS_TOK : 'declare-preds';
-DEFINE_TOK : 'define';
DECLARE_CONST_TOK : 'declare-const';
DEFINE_CONST_TOK : 'define-const';
SIMPLIFY_TOK : 'simplify';
GET_QE_TOK : 'get-qe';
GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
GET_ABDUCT_TOK : 'get-abduct';
-GET_INTERPOL_TOK : 'get-interpol';
+GET_ABDUCT_NEXT_TOK : 'get-abduct-next';
+GET_INTERPOL_TOK : 'get-interpolant';
+GET_INTERPOL_NEXT_TOK : 'get-interpolant-next';
DECLARE_HEAP : 'declare-heap';
+DECLARE_POOL : 'declare-pool';
// SyGuS commands
SYNTH_FUN_TOK : { PARSER_STATE->sygus() }?'synth-fun';
SYNTH_INV_TOK : { PARSER_STATE->sygus()}?'synth-inv';
CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth';
+CHECK_SYNTH_NEXT_TOK : { PARSER_STATE->sygus()}?'check-synth-next';
DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var';
CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint';
+ASSUME_TOK : { PARSER_STATE->sygus()}?'assume';
INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint';
-SET_OPTIONS_TOK : { PARSER_STATE->sygus() }? 'set-options';
+SET_FEATURE_TOK : { PARSER_STATE->sygus() }? 'set-feature';
SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
// attributes
ATTRIBUTE_PATTERN_TOK : ':pattern';
ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
+ATTRIBUTE_POOL_TOK : ':pool';
+ATTRIBUTE_INST_ADD_TO_POOL_TOK : ':inst-add-to-pool';
+ATTRIBUTE_SKOLEM_ADD_TO_POOL_TOK : ':skolem-add-to-pool';
ATTRIBUTE_NAMED_TOK : ':named';
ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
ATTRIBUTE_QUANTIFIER_ID_TOK : ':qid';
EXISTS_TOK : 'exists';
FORALL_TOK : 'forall';
-EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
-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';
-TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project';
+CHAR_TOK : { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_STRINGS) }? 'char';
+TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }? 'tuple';
+TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }? 'tuple.project';
+FMF_CARD_TOK: { !PARSER_STATE->strictModeEnabled() && PARSER_STATE->hasCardinalityConstraints() }? 'fmf.card';
HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda';
char *start = (char*) GETCHARINDEX();
}
: DIGIT+
- { Debug("parser-extra") << "NUMERAL: "
+ { Trace("parser-extra") << "NUMERAL: "
<< (uintptr_t)start << ".." << GETCHARINDEX()
<< " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
<< " ^0? " << (bool)(*start == '0')
;
/**
- * Matches a double-quoted string literal. Depending on the language that is
- * being parsed, different escape sequences are supported:
- *
- * For SMT-LIB 2.0 the sequence \" is interpreted as a double quote (") and the
- * sequence \\ is interpreted as a backslash (\).
- *
- * For SMT-LIB >=2.5 and SyGuS a double-quote inside a string is escaped with
- * "", e.g., "This is a string literal with "" a single, embedded double
- * quote."
+ * Matches a double-quoted string literal. A double-quote inside a string is
+ * escaped with "", e.g., "This is a string literal with "" a single, embedded
+ * double quote."
*
- * You shouldn't generally use this in parser rules, as the quotes
- * will be part of the token text. Use the str[] parser rule instead.
+ * You shouldn't generally use this in parser rules, as the quotes will be part
+ * of the token text. Use the str[] parser rule instead.
*/
STRING_LITERAL
- : { !PARSER_STATE->escapeDupDblQuote() }?=>
- '"' ('\\' . | ~('\\' | '"'))* '"'
- | { PARSER_STATE->escapeDupDblQuote() }?=>
- '"' (~('"') | '""')* '"'
+ : '"' (~('"') | '""')* '"'
;
/**