SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Data Fields | Private Attributes
smtrat::parser::SMTLIBParser Class Reference

#include <Parser.h>

Collaboration diagram for smtrat::parser::SMTLIBParser:
Collaboration graph
[legend]

Public Member Functions

 SMTLIBParser (InstructionHandler &handler, bool queueInstructions)
 
 ~SMTLIBParser ()
 
bool parse (std::istream &in)
 
void add (const types::TermType &t, bool isSoftFormula=false, Rational weight=Rational(1), const std::string id=std::string())
 
void check ()
 
void declareConst (const std::string &name, const carl::Sort &sort)
 
void declareFun (const std::string &name, const std::vector< carl::Sort > &args, const carl::Sort &sort)
 
void declareSort (const std::string &name, Integer arity)
 
void echo (const std::string &s)
 
void qe ()
 
void exit ()
 
void getAllModels ()
 
void getAssertions ()
 
void getAssignment ()
 
void getInfo (const std::string &key)
 
void getModel ()
 
void getObjectives ()
 
void getOption (const std::string &key)
 
void getProof ()
 
void getUnsatCore ()
 
void getValue ([[maybe_unused]] const std::vector< types::TermType > &vars)
 
void addObjective (const types::TermType &t, OptimizationType ot)
 
void pop (const Integer &n)
 
void push (const Integer &n)
 
void reset ()
 
void resetAssertions ()
 
void setInfo (const Attribute &attribute)
 
void setLogic (const carl::Logic &name)
 
void setOption (const Attribute &option)
 
template<typename Function , typename... Args>
void callHandler (const Function &f, const Args &... args)
 

Data Fields

bool queueInstructions
 
InstructionHandler & handler
 
ParserState state
 
Theories theories
 
ScriptParser< SMTLIBParser > parser
 

Private Attributes

std::istream * mInputStream
 

Detailed Description

Definition at line 17 of file Parser.h.

Constructor & Destructor Documentation

◆ SMTLIBParser()

smtrat::parser::SMTLIBParser::SMTLIBParser ( InstructionHandler &  handler,
bool  queueInstructions 
)
inline

Definition at line 31 of file Parser.h.

◆ ~SMTLIBParser()

smtrat::parser::SMTLIBParser::~SMTLIBParser ( )
inline

Definition at line 40 of file Parser.h.

Member Function Documentation

◆ add()

void smtrat::parser::SMTLIBParser::add ( const types::TermType &  t,
bool  isSoftFormula = false,
Rational  weight = Rational(1),
const std::string  id = std::string() 
)
inline

Definition at line 59 of file Parser.h.

Here is the call graph for this function:

◆ addObjective()

void smtrat::parser::SMTLIBParser::addObjective ( const types::TermType &  t,
OptimizationType  ot 
)
inline

Definition at line 161 of file Parser.h.

Here is the call graph for this function:

◆ callHandler()

template<typename Function , typename... Args>
void smtrat::parser::SMTLIBParser::callHandler ( const Function &  f,
const Args &...  args 
)
inline

Definition at line 211 of file Parser.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ check()

void smtrat::parser::SMTLIBParser::check ( )
inline

Definition at line 86 of file Parser.h.

Here is the call graph for this function:

◆ declareConst()

void smtrat::parser::SMTLIBParser::declareConst ( const std::string &  name,
const carl::Sort &  sort 
)
inline

Definition at line 90 of file Parser.h.

Here is the call graph for this function:

◆ declareFun()

void smtrat::parser::SMTLIBParser::declareFun ( const std::string &  name,
const std::vector< carl::Sort > &  args,
const carl::Sort &  sort 
)
inline

Definition at line 94 of file Parser.h.

Here is the call graph for this function:

◆ declareSort()

void smtrat::parser::SMTLIBParser::declareSort ( const std::string &  name,
Integer  arity 
)
inline

Definition at line 102 of file Parser.h.

Here is the call graph for this function:

◆ echo()

void smtrat::parser::SMTLIBParser::echo ( const std::string &  s)
inline

Definition at line 108 of file Parser.h.

Here is the call graph for this function:

◆ exit()

void smtrat::parser::SMTLIBParser::exit ( )
inline

Definition at line 116 of file Parser.h.

Here is the call graph for this function:

◆ getAllModels()

void smtrat::parser::SMTLIBParser::getAllModels ( )
inline

Definition at line 121 of file Parser.h.

Here is the call graph for this function:

◆ getAssertions()

void smtrat::parser::SMTLIBParser::getAssertions ( )
inline

Definition at line 125 of file Parser.h.

Here is the call graph for this function:

◆ getAssignment()

void smtrat::parser::SMTLIBParser::getAssignment ( )
inline

Definition at line 129 of file Parser.h.

Here is the call graph for this function:

◆ getInfo()

void smtrat::parser::SMTLIBParser::getInfo ( const std::string &  key)
inline

Definition at line 133 of file Parser.h.

Here is the call graph for this function:

◆ getModel()

void smtrat::parser::SMTLIBParser::getModel ( )
inline

Definition at line 137 of file Parser.h.

Here is the call graph for this function:

◆ getObjectives()

void smtrat::parser::SMTLIBParser::getObjectives ( )
inline

Definition at line 141 of file Parser.h.

Here is the call graph for this function:

◆ getOption()

void smtrat::parser::SMTLIBParser::getOption ( const std::string &  key)
inline

Definition at line 145 of file Parser.h.

Here is the call graph for this function:

◆ getProof()

void smtrat::parser::SMTLIBParser::getProof ( )
inline

Definition at line 149 of file Parser.h.

Here is the call graph for this function:

◆ getUnsatCore()

void smtrat::parser::SMTLIBParser::getUnsatCore ( )
inline

Definition at line 153 of file Parser.h.

Here is the call graph for this function:

◆ getValue()

void smtrat::parser::SMTLIBParser::getValue ( [[maybe_unused] ] const std::vector< types::TermType > &  vars)
inline

Definition at line 157 of file Parser.h.

Here is the call graph for this function:

◆ parse()

bool smtrat::parser::SMTLIBParser::parse ( std::istream &  in)
inline

Definition at line 43 of file Parser.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ pop()

void smtrat::parser::SMTLIBParser::pop ( const Integer &  n)
inline

Definition at line 171 of file Parser.h.

Here is the call graph for this function:

◆ push()

void smtrat::parser::SMTLIBParser::push ( const Integer &  n)
inline

Definition at line 182 of file Parser.h.

Here is the call graph for this function:

◆ qe()

void smtrat::parser::SMTLIBParser::qe ( )
inline

Definition at line 112 of file Parser.h.

Here is the call graph for this function:

◆ reset()

void smtrat::parser::SMTLIBParser::reset ( )
inline

Definition at line 187 of file Parser.h.

Here is the call graph for this function:

◆ resetAssertions()

void smtrat::parser::SMTLIBParser::resetAssertions ( )
inline

Definition at line 192 of file Parser.h.

Here is the call graph for this function:

◆ setInfo()

void smtrat::parser::SMTLIBParser::setInfo ( const Attribute &  attribute)
inline

Definition at line 196 of file Parser.h.

Here is the call graph for this function:

◆ setLogic()

void smtrat::parser::SMTLIBParser::setLogic ( const carl::Logic &  name)
inline

Definition at line 200 of file Parser.h.

Here is the call graph for this function:

◆ setOption()

void smtrat::parser::SMTLIBParser::setOption ( const Attribute &  option)
inline

Definition at line 205 of file Parser.h.

Here is the call graph for this function:

Field Documentation

◆ handler

InstructionHandler& smtrat::parser::SMTLIBParser::handler

Definition at line 25 of file Parser.h.

◆ mInputStream

std::istream* smtrat::parser::SMTLIBParser::mInputStream
private

Definition at line 21 of file Parser.h.

◆ parser

ScriptParser<SMTLIBParser> smtrat::parser::SMTLIBParser::parser

Definition at line 28 of file Parser.h.

◆ queueInstructions

bool smtrat::parser::SMTLIBParser::queueInstructions

Definition at line 24 of file Parser.h.

◆ state

ParserState smtrat::parser::SMTLIBParser::state

Definition at line 26 of file Parser.h.

◆ theories

Theories smtrat::parser::SMTLIBParser::theories

Definition at line 27 of file Parser.h.

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