cvc4-1.3
CVC4::parser::Parser Class Reference

This class encapsulates all of the state of a parser, including the name of the file, line number and column information, and in-scope declarations. More...

#include <parser.h>

Data Structures

class  ExprStream
 An expression stream interface for a parser. More...
 

Public Member Functions

virtual ~Parser ()
 
ExprManagergetExprManager () const
 Get the associated ExprManager. More...
 
InputgetInput () const
 Get the associated input. More...
 
void setInput (Input *input)
 Deletes and replaces the current parser input. More...
 
bool done () const
 Check if we are done – either the end of input has been reached, or some error has been encountered. More...
 
void setDone (bool done=true)
 Sets the done flag. More...
 
void enableChecks ()
 Enable semantic checks during parsing. More...
 
void disableChecks ()
 Disable semantic checks during parsing. More...
 
void enableStrictMode ()
 Enable strict parsing, according to the language standards. More...
 
void disableStrictMode ()
 Disable strict parsing. More...
 
bool strictModeEnabled ()
 
void allowIncludeFile ()
 
void disallowIncludeFile ()
 
bool canIncludeFile () const
 
Expr getVariable (const std::string &name)
 Returns a variable, given a name. More...
 
Expr getFunction (const std::string &name)
 Returns a function, given a name. More...
 
Type getSort (const std::string &sort_name)
 Returns a sort, given a name. More...
 
Type getSort (const std::string &sort_name, const std::vector< Type > &params)
 Returns a (parameterized) sort, given a name and args. More...
 
size_t getArity (const std::string &sort_name)
 Returns arity of a (parameterized) sort, given a name and args. More...
 
bool isDeclared (const std::string &name, SymbolType type=SYM_VARIABLE)
 Checks if a symbol has been declared. More...
 
void checkDeclaration (const std::string &name, DeclarationCheck check, SymbolType type=SYM_VARIABLE, std::string notes="") throw (ParserException)
 Checks if the declaration policy we want to enforce holds for the given symbol. More...
 
void reserveSymbolAtAssertionLevel (const std::string &name)
 Reserve a symbol at the assertion level. More...
 
void checkFunctionLike (const std::string &name) throw (ParserException)
 Checks whether the given name is bound to a function. More...
 
void checkArity (Kind kind, unsigned numArgs) throw (ParserException)
 Check that kind can accept numArgs arguments. More...
 
void checkOperator (Kind kind, unsigned numArgs) throw (ParserException)
 Check that kind is a legal operator in the current logic and that it can accept numArgs arguments. More...
 
Type getType (const std::string &var_name, SymbolType type=SYM_VARIABLE)
 Returns the type for the variable with the given name. More...
 
Expr mkVar (const std::string &name, const Type &type, uint32_t flags=ExprManager::VAR_FLAG_NONE)
 Create a new CVC4 variable expression of the given type. More...
 
std::vector< ExprmkVars (const std::vector< std::string > names, const Type &type, uint32_t flags=ExprManager::VAR_FLAG_NONE)
 Create a set of new CVC4 variable expressions of the given type. More...
 
Expr mkBoundVar (const std::string &name, const Type &type)
 Create a new CVC4 bound variable expression of the given type. More...
 
std::vector< ExprmkBoundVars (const std::vector< std::string > names, const Type &type)
 Create a set of new CVC4 bound variable expressions of the given type. More...
 
Expr mkFunction (const std::string &name, const Type &type, uint32_t flags=ExprManager::VAR_FLAG_NONE)
 Create a new CVC4 function expression of the given type. More...
 
Expr mkAnonymousFunction (const std::string &prefix, const Type &type, uint32_t flags=ExprManager::VAR_FLAG_NONE)
 Create a new CVC4 function expression of the given type, appending a unique index to its name. More...
 
void defineVar (const std::string &name, const Expr &val, bool levelZero=false)
 Create a new variable definition (e.g., from a let binding). More...
 
void defineFunction (const std::string &name, const Expr &val, bool levelZero=false)
 Create a new function definition (e.g., from a define-fun). More...
 
void defineType (const std::string &name, const Type &type)
 Create a new type definition. More...
 
void defineType (const std::string &name, const std::vector< Type > &params, const Type &type)
 Create a new (parameterized) type definition. More...
 
void defineParameterizedType (const std::string &name, const std::vector< Type > &params, const Type &type)
 Create a new type definition (e.g., from an SMT-LIBv2 define-sort). More...
 
SortType mkSort (const std::string &name, uint32_t flags=ExprManager::SORT_FLAG_NONE)
 Creates a new sort with the given name. More...
 
SortConstructorType mkSortConstructor (const std::string &name, size_t arity)
 Creates a new sort constructor with the given name and arity. More...
 
SortType mkUnresolvedType (const std::string &name)
 Creates a new "unresolved type," used only during parsing. More...
 
SortConstructorType mkUnresolvedTypeConstructor (const std::string &name, size_t arity)
 Creates a new unresolved (parameterized) type constructor of the given arity. More...
 
SortConstructorType mkUnresolvedTypeConstructor (const std::string &name, const std::vector< Type > &params)
 Creates a new unresolved (parameterized) type constructor given the type parameters. More...
 
bool isUnresolvedType (const std::string &name)
 Returns true IFF name is an unresolved type. More...
 
std::vector< DatatypeTypemkMutualDatatypeTypes (const std::vector< Datatype > &datatypes)
 Create sorts of mutually-recursive datatypes. More...
 
void addOperator (Kind kind)
 Add an operator to the current legal set. More...
 
void preemptCommand (Command *cmd)
 Preempt the next returned command with other ones; used to support the :named attribute in SMT-LIBv2, which implicitly inserts a new command before the current one. More...
 
bool isBoolean (const std::string &name)
 Is the symbol bound to a boolean variable? More...
 
bool isFunctionLike (const std::string &name)
 Is the symbol bound to a function (or function-like thing)? More...
 
bool isDefinedFunction (const std::string &name)
 Is the symbol bound to a defined function? More...
 
bool isDefinedFunction (Expr func)
 Is the Expr a defined function? More...
 
bool isPredicate (const std::string &name)
 Is the symbol bound to a predicate? More...
 
CommandnextCommand () throw (ParserException)
 Parse and return the next command. More...
 
Expr nextExpression () throw (ParserException)
 Parse and return the next expression. More...
 
void warning (const std::string &msg)
 Issue a warning to the user. More...
 
void attributeNotSupported (const std::string &attr)
 Issue a warning to the user, but only once per attribute. More...
 
void parseError (const std::string &msg) throw (ParserException)
 Raise a parse error with the given message. More...
 
void unexpectedEOF (const std::string &msg) throw (ParserException)
 Unexpectedly encountered an EOF. More...
 
void unimplementedFeature (const std::string &msg) throw (ParserException)
 If we are parsing only, don't raise an exception; if we are not, raise a parse error with the given message. More...
 
size_t scopeLevel () const
 Gets the current declaration level. More...
 
void pushScope (bool bindingLevel=false)
 
void popScope ()
 
void useDeclarationsFrom (Parser *parser)
 Set the current symbol table used by this parser. More...
 
void useDeclarationsFrom (SymbolTable *symtab)
 
SymbolTablegetSymbolTable () const
 

Protected Member Functions

 Parser (ExprManager *exprManager, Input *input, bool strictMode=false, bool parseOnly=false)
 Create a parser state. More...
 

Friends

class ParserBuilder
 

Detailed Description

This class encapsulates all of the state of a parser, including the name of the file, line number and column information, and in-scope declarations.

Definition at line 106 of file parser.h.

Constructor & Destructor Documentation

CVC4::parser::Parser::Parser ( ExprManager exprManager,
Input input,
bool  strictMode = false,
bool  parseOnly = false 
)
protected

Create a parser state.

Attention
The parser takes "ownership" of the given input and will delete it on destruction.
Parameters
exprManagerthe expression manager to use when creating expressions
inputthe parser input
strictModewhether to incorporate strict(er) compliance checks
parseOnlywhether we are parsing only (and therefore certain checks need not be performed, like those about unimplemented features,
See also
unimplementedFeature())
virtual CVC4::parser::Parser::~Parser ( )
inlinevirtual

Definition at line 210 of file parser.h.

Member Function Documentation

void CVC4::parser::Parser::addOperator ( Kind  kind)

Add an operator to the current legal set.

Parameters
kindthe built-in operator to add
void CVC4::parser::Parser::allowIncludeFile ( )
inline

Definition at line 261 of file parser.h.

void CVC4::parser::Parser::attributeNotSupported ( const std::string &  attr)

Issue a warning to the user, but only once per attribute.

bool CVC4::parser::Parser::canIncludeFile ( ) const
inline

Definition at line 263 of file parser.h.

void CVC4::parser::Parser::checkArity ( Kind  kind,
unsigned  numArgs 
)
throw (ParserException
)

Check that kind can accept numArgs arguments.

Parameters
kindthe built-in operator to check
numArgsthe number of actual arguments
Exceptions
ParserExceptionif checks are enabled and the operator kind cannot be applied to numArgs arguments.
void CVC4::parser::Parser::checkDeclaration ( const std::string &  name,
DeclarationCheck  check,
SymbolType  type = SYM_VARIABLE,
std::string  notes = "" 
)
throw (ParserException
)

Checks if the declaration policy we want to enforce holds for the given symbol.

Parameters
namethe symbol to check
checkthe kind of check to perform
typethe type of the symbol
Exceptions
ParserExceptionif checks are enabled and the check fails
void CVC4::parser::Parser::checkFunctionLike ( const std::string &  name)
throw (ParserException
)

Checks whether the given name is bound to a function.

Parameters
namethe name to check
Exceptions
ParserExceptionif checks are enabled and name is not bound to a function
void CVC4::parser::Parser::checkOperator ( Kind  kind,
unsigned  numArgs 
)
throw (ParserException
)

Check that kind is a legal operator in the current logic and that it can accept numArgs arguments.

Parameters
kindthe built-in operator to check
numArgsthe number of actual arguments
Exceptions
ParserExceptionif the parser mode is strict and the operator kind has not been enabled
void CVC4::parser::Parser::defineFunction ( const std::string &  name,
const Expr val,
bool  levelZero = false 
)

Create a new function definition (e.g., from a define-fun).

void CVC4::parser::Parser::defineParameterizedType ( const std::string &  name,
const std::vector< Type > &  params,
const Type type 
)

Create a new type definition (e.g., from an SMT-LIBv2 define-sort).

void CVC4::parser::Parser::defineType ( const std::string &  name,
const Type type 
)

Create a new type definition.

void CVC4::parser::Parser::defineType ( const std::string &  name,
const std::vector< Type > &  params,
const Type type 
)

Create a new (parameterized) type definition.

void CVC4::parser::Parser::defineVar ( const std::string &  name,
const Expr val,
bool  levelZero = false 
)

Create a new variable definition (e.g., from a let binding).

void CVC4::parser::Parser::disableChecks ( )
inline

Disable semantic checks during parsing.

Disabling checks may lead to crashes on bad inputs.

Definition at line 250 of file parser.h.

void CVC4::parser::Parser::disableStrictMode ( )
inline

Disable strict parsing.

Allows certain syntactic infelicities to pass without comment.

Definition at line 257 of file parser.h.

void CVC4::parser::Parser::disallowIncludeFile ( )
inline

Definition at line 262 of file parser.h.

bool CVC4::parser::Parser::done ( ) const
inline

Check if we are done – either the end of input has been reached, or some error has been encountered.

Returns
true if parser is done

Definition at line 237 of file parser.h.

void CVC4::parser::Parser::enableChecks ( )
inline

Enable semantic checks during parsing.

Definition at line 247 of file parser.h.

void CVC4::parser::Parser::enableStrictMode ( )
inline

Enable strict parsing, according to the language standards.

Definition at line 253 of file parser.h.

size_t CVC4::parser::Parser::getArity ( const std::string &  sort_name)

Returns arity of a (parameterized) sort, given a name and args.

ExprManager* CVC4::parser::Parser::getExprManager ( ) const
inline

Get the associated ExprManager.

Definition at line 215 of file parser.h.

Expr CVC4::parser::Parser::getFunction ( const std::string &  name)

Returns a function, given a name.

Parameters
namethe name of the variable
Returns
the variable expression
Input* CVC4::parser::Parser::getInput ( ) const
inline

Get the associated input.

Definition at line 220 of file parser.h.

Type CVC4::parser::Parser::getSort ( const std::string &  sort_name)

Returns a sort, given a name.

Parameters
sort_namethe name to look up
Type CVC4::parser::Parser::getSort ( const std::string &  sort_name,
const std::vector< Type > &  params 
)

Returns a (parameterized) sort, given a name and args.

SymbolTable* CVC4::parser::Parser::getSymbolTable ( ) const
inline

Definition at line 582 of file parser.h.

Type CVC4::parser::Parser::getType ( const std::string &  var_name,
SymbolType  type = SYM_VARIABLE 
)

Returns the type for the variable with the given name.

Parameters
var_namethe symbol to lookup
typethe (namespace) type of the symbol
Expr CVC4::parser::Parser::getVariable ( const std::string &  name)

Returns a variable, given a name.

Parameters
namethe name of the variable
Returns
the variable expression
bool CVC4::parser::Parser::isBoolean ( const std::string &  name)

Is the symbol bound to a boolean variable?

bool CVC4::parser::Parser::isDeclared ( const std::string &  name,
SymbolType  type = SYM_VARIABLE 
)

Checks if a symbol has been declared.

Parameters
namethe symbol name
typethe symbol type
Returns
true iff the symbol has been declared with the given type
bool CVC4::parser::Parser::isDefinedFunction ( const std::string &  name)

Is the symbol bound to a defined function?

bool CVC4::parser::Parser::isDefinedFunction ( Expr  func)

Is the Expr a defined function?

bool CVC4::parser::Parser::isFunctionLike ( const std::string &  name)

Is the symbol bound to a function (or function-like thing)?

bool CVC4::parser::Parser::isPredicate ( const std::string &  name)

Is the symbol bound to a predicate?

bool CVC4::parser::Parser::isUnresolvedType ( const std::string &  name)

Returns true IFF name is an unresolved type.

Expr CVC4::parser::Parser::mkAnonymousFunction ( const std::string &  prefix,
const Type type,
uint32_t  flags = ExprManager::VAR_FLAG_NONE 
)

Create a new CVC4 function expression of the given type, appending a unique index to its name.

(That's the ONLY difference between mkAnonymousFunction() and mkFunction()).

Expr CVC4::parser::Parser::mkBoundVar ( const std::string &  name,
const Type type 
)

Create a new CVC4 bound variable expression of the given type.

std::vector<Expr> CVC4::parser::Parser::mkBoundVars ( const std::vector< std::string >  names,
const Type type 
)

Create a set of new CVC4 bound variable expressions of the given type.

Expr CVC4::parser::Parser::mkFunction ( const std::string &  name,
const Type type,
uint32_t  flags = ExprManager::VAR_FLAG_NONE 
)

Create a new CVC4 function expression of the given type.

std::vector<DatatypeType> CVC4::parser::Parser::mkMutualDatatypeTypes ( const std::vector< Datatype > &  datatypes)

Create sorts of mutually-recursive datatypes.

SortType CVC4::parser::Parser::mkSort ( const std::string &  name,
uint32_t  flags = ExprManager::SORT_FLAG_NONE 
)

Creates a new sort with the given name.

SortConstructorType CVC4::parser::Parser::mkSortConstructor ( const std::string &  name,
size_t  arity 
)

Creates a new sort constructor with the given name and arity.

SortType CVC4::parser::Parser::mkUnresolvedType ( const std::string &  name)

Creates a new "unresolved type," used only during parsing.

SortConstructorType CVC4::parser::Parser::mkUnresolvedTypeConstructor ( const std::string &  name,
size_t  arity 
)

Creates a new unresolved (parameterized) type constructor of the given arity.

SortConstructorType CVC4::parser::Parser::mkUnresolvedTypeConstructor ( const std::string &  name,
const std::vector< Type > &  params 
)

Creates a new unresolved (parameterized) type constructor given the type parameters.

Expr CVC4::parser::Parser::mkVar ( const std::string &  name,
const Type type,
uint32_t  flags = ExprManager::VAR_FLAG_NONE 
)

Create a new CVC4 variable expression of the given type.

std::vector<Expr> CVC4::parser::Parser::mkVars ( const std::vector< std::string >  names,
const Type type,
uint32_t  flags = ExprManager::VAR_FLAG_NONE 
)

Create a set of new CVC4 variable expressions of the given type.

Command* CVC4::parser::Parser::nextCommand ( )
throw (ParserException
)

Parse and return the next command.

Expr CVC4::parser::Parser::nextExpression ( )
throw (ParserException
)

Parse and return the next expression.

void CVC4::parser::Parser::parseError ( const std::string &  msg)
throw (ParserException
)
inline

Raise a parse error with the given message.

Definition at line 496 of file parser.h.

void CVC4::parser::Parser::popScope ( )
inline

Definition at line 537 of file parser.h.

void CVC4::parser::Parser::preemptCommand ( Command cmd)

Preempt the next returned command with other ones; used to support the :named attribute in SMT-LIBv2, which implicitly inserts a new command before the current one.

Also used in TPTP because function and predicate symbols are implicitly declared.

void CVC4::parser::Parser::pushScope ( bool  bindingLevel = false)
inline

Definition at line 530 of file parser.h.

void CVC4::parser::Parser::reserveSymbolAtAssertionLevel ( const std::string &  name)

Reserve a symbol at the assertion level.

size_t CVC4::parser::Parser::scopeLevel ( ) const
inline

Gets the current declaration level.

Definition at line 528 of file parser.h.

void CVC4::parser::Parser::setDone ( bool  done = true)
inline

Sets the done flag.

Definition at line 242 of file parser.h.

void CVC4::parser::Parser::setInput ( Input input)
inline

Deletes and replaces the current parser input.

Definition at line 225 of file parser.h.

References CVC4::parser::Input::setParser().

bool CVC4::parser::Parser::strictModeEnabled ( )
inline

Definition at line 259 of file parser.h.

void CVC4::parser::Parser::unexpectedEOF ( const std::string &  msg)
throw (ParserException
)
inline

Unexpectedly encountered an EOF.

Definition at line 501 of file parser.h.

void CVC4::parser::Parser::unimplementedFeature ( const std::string &  msg)
throw (ParserException
)
inline

If we are parsing only, don't raise an exception; if we are not, raise a parse error with the given message.

There is no actual parse error, everything is as expected, but we cannot create the Expr, Type, or other requested thing yet due to internal limitations. Even though it's not a parse error, we throw a parse error so that the input line and column information is available.

Think quantifiers. We don't have a TheoryQuantifiers yet, so we have no kind::FORALL or kind::EXISTS. But we might want to support parsing quantifiers (just not doing anything with them). So this mechanism gives you a way to do it with –parse-only.

Definition at line 519 of file parser.h.

void CVC4::parser::Parser::useDeclarationsFrom ( Parser parser)
inline

Set the current symbol table used by this parser.

From now on, this parser will perform its definitions and lookups in the declaration scope of the "parser" argument (but doesn't re-delegate if the other parser's declaration scope changes later). A NULL argument restores this parser's "primordial" declaration scope assigned at its creation. Calling p->useDeclarationsFrom(p) is a no-op.

This feature is useful when e.g. reading out-of-band expression data:

  1. Parsing –replay log files produced with –replay-log.
  2. Perhaps a multi-query benchmark file is being single-stepped with intervening queries on stdin that must reference the same declaration scope(s).

However, the feature must be used carefully. Pushes and pops should be performed with the correct current declaration scope. Care must be taken to match up declaration scopes, of course; If variables in the deferred-to parser go out of scope, the secondary parser will give errors that they are undeclared. Also, an outer-scope variable shadowed by an inner-scope one of the same name may be temporarily inaccessible.

In short, caveat emptor.

Definition at line 570 of file parser.h.

void CVC4::parser::Parser::useDeclarationsFrom ( SymbolTable symtab)
inline

Definition at line 578 of file parser.h.

void CVC4::parser::Parser::warning ( const std::string &  msg)
inline

Issue a warning to the user.

Definition at line 488 of file parser.h.

Friends And Related Function Documentation

friend class ParserBuilder
friend

Definition at line 107 of file parser.h.


The documentation for this class was generated from the following file: