|
Function Name  |
Hit count  |
| cvc5::parser::GetValueCommand::GetValueCommand(cvc5::Term) |
0 |
| cvc5::parser::SimplifyCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
0 |
| cvc5::parser::SimplifyCommand::SimplifyCommand(cvc5::Term) |
0 |
| cvc5::parser::GetAbductCommand::GetAbductCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, cvc5::Term) |
0 |
| cvc5::parser::DefineSortCommand::DefineSortCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, cvc5::Sort) |
0 |
| cvc5::parser::GetInterpolantCommand::GetInterpolantCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, cvc5::Term) |
0 |
| cvc5::parser::CheckSatAssumingCommand::CheckSatAssumingCommand(cvc5::Term) |
0 |
| cvc5::parser::DeclareOracleFunCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
0 |
| cvc5::parser::DeclareOracleFunCommand::DeclareOracleFunCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::vector<cvc5::Sort, std::allocator<cvc5::Sort> > const&, cvc5::Sort) |
0 |
| cvc5::parser::DeclareOracleFunCommand::DeclareOracleFunCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::vector<cvc5::Sort, std::allocator<cvc5::Sort> > const&, cvc5::Sort, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) |
0 |
| cvc5::parser::SygusInvConstraintCommand::SygusInvConstraintCommand(cvc5::Term const&, cvc5::Term const&, cvc5::Term const&, cvc5::Term const&) |
0 |
| cvc5::parser::DatatypeDeclarationCommand::DatatypeDeclarationCommand(cvc5::Sort const&) |
0 |
| cvc5::parser::GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() |
0 |
| cvc5::parser::Cmd::Cmd(cvc5::parser::Cmd const&) |
0 |
| cvc5::parser::Cmd::~Cmd() |
0 |
| cvc5::parser::operator<<(std::basic_ostream<char, std::char_traits<char> >&, cvc5::parser::Cmd const*) |
0 |
| cvc5::parser::operator<<(std::basic_ostream<char, std::char_traits<char> >&, cvc5::parser::Cmd const&) |
0 |
| cvc5::parser::PopCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::EchoCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::EchoCommand::getOutput[abi:cxx11]() const |
0 |
| cvc5::parser::PushCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::QuitCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::EmptyCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::EmptyCommand::getName[abi:cxx11]() const |
0 |
| cvc5::parser::ResetCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::AssertCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::AssertCommand::getTerm() const |
0 |
| cvc5::parser::GetInfoCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetInfoCommand::getFlag[abi:cxx11]() const |
0 |
| cvc5::parser::GetInfoCommand::getResult[abi:cxx11]() const |
0 |
| cvc5::parser::SetInfoCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::SetInfoCommand::getFlag[abi:cxx11]() const |
0 |
| cvc5::parser::SetInfoCommand::getValue[abi:cxx11]() const |
0 |
| cvc5::parser::CheckSatCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetProofCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetValueCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetValueCommand::getTerms() const |
0 |
| cvc5::parser::GetValueCommand::getResult() const |
0 |
| cvc5::parser::SimplifyCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
0 |
| cvc5::parser::SimplifyCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::SimplifyCommand::getTerm() const |
0 |
| cvc5::parser::SimplifyCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
0 |
| cvc5::parser::SimplifyCommand::getResult() const |
0 |
| cvc5::parser::SynthFunCommand::getGrammar() const |
0 |
| cvc5::parser::SynthFunCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::SynthFunCommand::getSort() const |
0 |
| cvc5::parser::SynthFunCommand::getVars() const |
0 |
| cvc5::parser::FindSynthCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::FindSynthCommand::getResult() const |
0 |
| cvc5::parser::GetAbductCommand::getGrammar() const |
0 |
| cvc5::parser::GetAbductCommand::getAbductName[abi:cxx11]() const |
0 |
| cvc5::parser::GetAbductCommand::getConjecture() const |
0 |
| cvc5::parser::GetAbductCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetAbductCommand::getResult() const |
0 |
| cvc5::parser::GetOptionCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetOptionCommand::getFlag[abi:cxx11]() const |
0 |
| cvc5::parser::GetOptionCommand::getResult[abi:cxx11]() const |
0 |
| cvc5::parser::SetOptionCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::SetOptionCommand::getFlag[abi:cxx11]() const |
0 |
| cvc5::parser::SetOptionCommand::getValue[abi:cxx11]() const |
0 |
| cvc5::parser::BlockModelCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::CheckSynthCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::CheckSynthCommand::getResult() const |
0 |
| cvc5::parser::DefineSortCommand::getParameters() const |
0 |
| cvc5::parser::DefineSortCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::DefineSortCommand::getSort() const |
0 |
| cvc5::parser::DeclareHeapCommand::getDataSort() const |
0 |
| cvc5::parser::DeclareHeapCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::DeclareHeapCommand::getLocationSort() const |
0 |
| cvc5::parser::DeclarePoolCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::DeclarePoolCommand::getInitialValue() const |
0 |
| cvc5::parser::DeclarePoolCommand::getSort() const |
0 |
| cvc5::parser::DeclareSortCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::DeclareSortCommand::getArity() const |
0 |
| cvc5::parser::GetUnsatCoreCommand::getUnsatCore() const |
0 |
| cvc5::parser::GetUnsatCoreCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::FindSynthNextCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::FindSynthNextCommand::getResult() const |
0 |
| cvc5::parser::GetAbductNextCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetAbductNextCommand::getResult() const |
0 |
| cvc5::parser::GetAssertionsCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetAssertionsCommand::getResult[abi:cxx11]() const |
0 |
| cvc5::parser::GetAssignmentCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetAssignmentCommand::getResult() const |
0 |
| cvc5::parser::GetDifficultyCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetDifficultyCommand::getDifficultyMap() const |
0 |
| cvc5::parser::DefineFunctionCommand::getFormals() const |
0 |
| cvc5::parser::DefineFunctionCommand::getFormula() const |
0 |
| cvc5::parser::DefineFunctionCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::DefineFunctionCommand::getSort() const |
0 |
| cvc5::parser::GetInterpolantCommand::getGrammar() const |
0 |
| cvc5::parser::GetInterpolantCommand::getConjecture() const |
0 |
| cvc5::parser::GetInterpolantCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetInterpolantCommand::getResult() const |
0 |
| cvc5::parser::GetTimeoutCoreCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetTimeoutCoreCommand::getTimeoutCore() const |
0 |
| cvc5::parser::GetTimeoutCoreCommand::getResult() const |
0 |
| cvc5::parser::DeclareFunctionCommand::getArgSorts() const |
0 |
| cvc5::parser::DeclareFunctionCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::DeclareFunctionCommand::getSort() const |
0 |
| cvc5::parser::DeclareSygusVarCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::DeclareSygusVarCommand::getSort() const |
0 |
| cvc5::parser::ResetAssertionsCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::SygusConstraintCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::SygusConstraintCommand::getTerm() const |
0 |
| cvc5::parser::BlockModelValuesCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::BlockModelValuesCommand::getTerms() const |
0 |
| cvc5::parser::CheckSatAssumingCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::CheckSatAssumingCommand::getTerms() const |
0 |
| cvc5::parser::DeclareOracleFunCommand::getBinaryName[abi:cxx11]() const |
0 |
| cvc5::parser::DeclareOracleFunCommand::getIdentifier[abi:cxx11]() const |
0 |
| cvc5::parser::DeclareOracleFunCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::DeclareOracleFunCommand::getSort() const |
0 |
| cvc5::parser::DeclareOracleFunCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
0 |
| cvc5::parser::DefineFunctionRecCommand::getFormals() const |
0 |
| cvc5::parser::DefineFunctionRecCommand::getFormulas() const |
0 |
| cvc5::parser::DefineFunctionRecCommand::getFunctions() const |
0 |
| cvc5::parser::DefineFunctionRecCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetInstantiationsCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetInstantiationsCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
0 |
| cvc5::parser::SetBenchmarkLogicCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetInterpolantNextCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetInterpolantNextCommand::getResult() const |
0 |
| cvc5::parser::GetLearnedLiteralsCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetLearnedLiteralsCommand::getLearnedLiterals() const |
0 |
| cvc5::parser::GetUnsatCoreLemmasCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::SygusInvConstraintCommand::getPredicates() const |
0 |
| cvc5::parser::SygusInvConstraintCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::DatatypeDeclarationCommand::getDatatypes() const |
0 |
| cvc5::parser::DatatypeDeclarationCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetUnsatAssumptionsCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetUnsatAssumptionsCommand::getResult() const |
0 |
| cvc5::parser::DeclarationDefinitionCommand::getSymbol[abi:cxx11]() const |
0 |
| cvc5::parser::GetModelDomainElementsCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetModelDomainElementsCommand::getSort() const |
0 |
| cvc5::parser::GetModelDomainElementsCommand::getResult() const |
0 |
| cvc5::parser::GetQuantifierEliminationCommand::getCommandName[abi:cxx11]() const |
0 |
| cvc5::parser::GetQuantifierEliminationCommand::getTerm() const |
0 |
| cvc5::parser::GetQuantifierEliminationCommand::getDoFull() const |
0 |
| cvc5::parser::GetQuantifierEliminationCommand::getResult() const |
0 |
| cvc5::parser::FindSynthNextCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
1 |
| cvc5::parser::GetInterpolantNextCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
1 |
| cvc5::parser::FindSynthNextCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
1 |
| cvc5::parser::FindSynthNextCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
1 |
| cvc5::parser::GetAssertionsCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
1 |
| cvc5::parser::SetBenchmarkLogicCommand::getLogic[abi:cxx11]() const |
1 |
| cvc5::parser::GetInterpolantNextCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
1 |
| cvc5::parser::GetInterpolantNextCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
1 |
| cvc5::parser::GetModelDomainElementsCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
1 |
| cvc5::parser::GetAssertionsCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
2 |
| cvc5::parser::GetAssertionsCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
2 |
| cvc5::parser::GetUnsatCoreLemmasCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
2 |
| cvc5::parser::GetInterpolantNextCommand::GetInterpolantNextCommand() |
3 |
| cvc5::parser::GetModelCommand::getCommandName[abi:cxx11]() const |
3 |
| cvc5::parser::GetDifficultyCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
3 |
| cvc5::parser::BlockModelValuesCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
3 |
| cvc5::parser::GetAssertionsCommand::GetAssertionsCommand() |
4 |
| cvc5::parser::DeclarePoolCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
4 |
| cvc5::parser::GetAssignmentCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
5 |
| cvc5::parser::GetUnsatAssumptionsCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
5 |
| cvc5::parser::GetUnsatCoreLemmasCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
6 |
| cvc5::parser::GetModelDomainElementsCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
6 |
| cvc5::parser::GetProofCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
6 |
| cvc5::parser::GetAbductNextCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
6 |
| cvc5::parser::GetTimeoutCoreCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
6 |
| cvc5::parser::GetUnsatCoreLemmasCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
6 |
| cvc5::parser::GetModelDomainElementsCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
6 |
| cvc5::parser::BlockModelCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
7 |
| cvc5::parser::GetLearnedLiteralsCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
7 |
| cvc5::parser::GetUnsatCoreLemmasCommand::GetUnsatCoreLemmasCommand() |
8 |
| cvc5::parser::GetModelDomainElementsCommand::GetModelDomainElementsCommand(cvc5::Sort) |
8 |
| cvc5::parser::GetAssignmentCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
8 |
| cvc5::parser::EchoCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
9 |
| cvc5::parser::EmptyCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
9 |
| cvc5::parser::EchoCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
10 |
| cvc5::parser::GetAssignmentCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
10 |
| cvc5::parser::EchoCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
10 |
| cvc5::parser::GetUnsatCoreCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
10 |
| cvc5::parser::GetAbductNextCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
12 |
| cvc5::parser::BlockModelValuesCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
12 |
| cvc5::parser::GetInstantiationsCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
12 |
| cvc5::parser::GetInstantiationsCommand::GetInstantiationsCommand() |
12 |
| cvc5::parser::GetAbductNextCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
12 |
| cvc5::parser::GetInstantiationsCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
12 |
| cvc5::parser::GetTimeoutCoreCommand::GetTimeoutCoreCommand() |
13 |
| cvc5::parser::ResetAssertionsCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
13 |
| cvc5::parser::SygusInvConstraintCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
13 |
| cvc5::parser::GetLearnedLiteralsCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
14 |
| cvc5::parser::GetLearnedLiteralsCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
14 |
| cvc5::parser::GetDifficultyCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
15 |
| cvc5::parser::GetDifficultyCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
15 |
| cvc5::parser::GetTimeoutCoreCommand::GetTimeoutCoreCommand(std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&) |
16 |
| cvc5::parser::EmptyCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
17 |
| cvc5::parser::GetTimeoutCoreCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
17 |
| cvc5::parser::GetUnsatAssumptionsCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
17 |
| cvc5::parser::ResetCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
17 |
| cvc5::parser::GetInfoCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
17 |
| cvc5::parser::GetTimeoutCoreCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
17 |
| cvc5::parser::GetUnsatAssumptionsCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
17 |
| cvc5::parser::BlockModelValuesCommand::BlockModelValuesCommand(std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&) |
18 |
| cvc5::parser::GetQuantifierEliminationCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
19 |
| cvc5::parser::GetQuantifierEliminationCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
19 |
| cvc5::parser::GetQuantifierEliminationCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
19 |
| cvc5::parser::GetAssignmentCommand::GetAssignmentCommand() |
20 |
| cvc5::parser::GetDifficultyCommand::GetDifficultyCommand() |
21 |
| cvc5::parser::GetInstantiationsCommand::isEnabled(cvc5::Solver*, cvc5::Result const&) |
22 |
| cvc5::parser::GetInterpolantCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
22 |
| cvc5::parser::GetInterpolantCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
23 |
| cvc5::parser::GetInfoCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
23 |
| cvc5::parser::GetInterpolantCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
23 |
| cvc5::parser::BlockModelCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
24 |
| cvc5::parser::GetAbductNextCommand::GetAbductNextCommand() |
24 |
| cvc5::parser::GetModelCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
24 |
| cvc5::parser::GetUnsatCoreCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
25 |
| cvc5::parser::EmptyCommand::EmptyCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >) |
26 |
| cvc5::parser::FindSynthCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
26 |
| cvc5::parser::SygusInvConstraintCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
27 |
| cvc5::parser::GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() |
27 |
| cvc5::parser::EchoCommand::EchoCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >) |
28 |
| cvc5::parser::GetLearnedLiteralsCommand::GetLearnedLiteralsCommand(cvc5::modes::LearnedLitType) |
28 |
| cvc5::parser::DeclarePoolCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
29 |
| cvc5::parser::DeclarePoolCommand::DeclarePoolCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, cvc5::Sort, std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&) |
29 |
| cvc5::parser::GetUnsatCoreCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
32 |
| cvc5::parser::GetInfoCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
33 |
| cvc5::parser::GetAbductCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
33 |
| cvc5::parser::FindSynthCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
34 |
| cvc5::parser::ResetAssertionsCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
36 |
| cvc5::parser::BlockModelCommand::BlockModelCommand(cvc5::modes::BlockModelsMode) |
38 |
| cvc5::parser::DefineFunctionCommand::DefineFunctionCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, cvc5::Sort, cvc5::Term) |
38 |
| cvc5::parser::FindSynthCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
41 |
| cvc5::parser::GetOptionCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
43 |
| cvc5::parser::GetModelCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
46 |
| cvc5::parser::GetInfoCommand::GetInfoCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >) |
47 |
| cvc5::parser::GetOptionCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
49 |
| cvc5::parser::GetOptionCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
49 |
| cvc5::parser::DeclareHeapCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
49 |
| cvc5::parser::GetValueCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
50 |
| cvc5::parser::SygusInvConstraintCommand::SygusInvConstraintCommand(std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&) |
53 |
| cvc5::parser::GetUnsatCoreCommand::GetUnsatCoreCommand() |
54 |
| cvc5::parser::GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(cvc5::Term const&, bool) |
57 |
| cvc5::parser::GetModelCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
60 |
| cvc5::parser::GetAbductCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
62 |
| cvc5::parser::GetAbductCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
66 |
| cvc5::parser::GetInterpolantCommand::GetInterpolantCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, cvc5::Term, cvc5::Grammar*) |
69 |
| cvc5::parser::DefineFunctionRecCommand::DefineFunctionRecCommand(std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&, std::vector<std::vector<cvc5::Term, std::allocator<cvc5::Term> >, std::allocator<std::vector<cvc5::Term, std::allocator<cvc5::Term> > > > const&, std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&) |
75 |
| cvc5::parser::ResetCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
83 |
| cvc5::parser::Cmd::resetSolver(cvc5::Solver*) |
83 |
| cvc5::parser::Cmd::interrupted() const |
89 |
| cvc5::parser::GetValueCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
102 |
| cvc5::parser::GetValueCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
106 |
| cvc5::parser::GetModelCommand::GetModelCommand() |
111 |
| cvc5::parser::DefineFunctionRecCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
120 |
| cvc5::parser::DefineSortCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
128 |
| cvc5::parser::GetAbductCommand::GetAbductCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, cvc5::Term, cvc5::Grammar*) |
132 |
| cvc5::parser::GetOptionCommand::GetOptionCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >) |
135 |
| cvc5::parser::DeclareHeapCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
160 |
| cvc5::parser::GetValueCommand::GetValueCommand(std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&) |
206 |
| cvc5::parser::CheckSynthCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
238 |
| cvc5::parser::Cmd::grammarToTypeNode(cvc5::Grammar*) |
249 |
| cvc5::parser::DeclareHeapCommand::DeclareHeapCommand(cvc5::Sort, cvc5::Sort) |
258 |
| cvc5::parser::DeclareSygusVarCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
360 |
| cvc5::parser::SynthFunCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
403 |
| cvc5::parser::QuitCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
465 |
| cvc5::parser::CheckSynthCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
470 |
| cvc5::parser::CheckSynthCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
476 |
| cvc5::parser::DefineFunctionRecCommand::DefineFunctionRecCommand(cvc5::Term, std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&, cvc5::Term) |
564 |
| cvc5::parser::DefineFunctionRecCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
639 |
| cvc5::parser::CheckSatAssumingCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
670 |
| cvc5::parser::DatatypeDeclarationCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
680 |
| cvc5::parser::SygusConstraintCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
703 |
| cvc5::parser::DefineSortCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
753 |
| cvc5::parser::DefineSortCommand::DefineSortCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::vector<cvc5::Sort, std::allocator<cvc5::Sort> > const&, cvc5::Sort) |
753 |
| cvc5::parser::PopCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
821 |
| cvc5::parser::Cmd::invoke(cvc5::Solver*, cvc5::parser::SymManager*, std::basic_ostream<char, std::char_traits<char> >&) |
829 |
| cvc5::parser::PushCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
1031 |
| cvc5::parser::DefineFunctionCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
1326 |
| cvc5::parser::SygusConstraintCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
1402 |
| cvc5::parser::SetOptionCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
1423 |
| cvc5::parser::DeclareSygusVarCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
1441 |
| cvc5::parser::DeclareSygusVarCommand::DeclareSygusVarCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, cvc5::Sort) |
1441 |
| cvc5::parser::SynthFunCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
1611 |
| cvc5::parser::SynthFunCommand::SynthFunCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&, cvc5::Sort, cvc5::Grammar*) |
1611 |
| cvc5::parser::DeclareSortCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
1680 |
| cvc5::parser::QuitCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
2109 |
| cvc5::parser::CheckSatAssumingCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
2777 |
| cvc5::parser::CheckSatAssumingCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
2782 |
| cvc5::parser::SygusConstraintCommand::SygusConstraintCommand(cvc5::Term const&, bool) |
2808 |
| cvc5::parser::Cmd::termVectorToNodes(std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&) |
2886 |
| cvc5::parser::PopCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
2922 |
| cvc5::parser::SetInfoCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
3171 |
| cvc5::parser::PushCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
3619 |
| cvc5::parser::DatatypeDeclarationCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
3869 |
| cvc5::parser::DatatypeDeclarationCommand::DatatypeDeclarationCommand(std::vector<cvc5::Sort, std::allocator<cvc5::Sort> > const&) |
3869 |
| cvc5::parser::CheckSatAssumingCommand::CheckSatAssumingCommand(std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&) |
4116 |
| cvc5::parser::CheckSatAssumingCommand::getResult() const |
4116 |
| cvc5::parser::SetBenchmarkLogicCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
4231 |
| cvc5::parser::PopCommand::PopCommand(unsigned int) |
4564 |
| cvc5::parser::CheckSatCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
4649 |
| cvc5::parser::SetOptionCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
4836 |
| cvc5::parser::GetProofCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
5215 |
| cvc5::parser::GetProofCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
5216 |
| cvc5::parser::GetProofCommand::GetProofCommand(cvc5::modes::ProofComponent) |
5228 |
| cvc5::parser::PushCommand::PushCommand(unsigned int) |
5681 |
| cvc5::parser::DefineFunctionCommand::DefineFunctionCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::vector<cvc5::Term, std::allocator<cvc5::Term> > const&, cvc5::Sort, cvc5::Term) |
7291 |
| cvc5::parser::DefineFunctionCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
7329 |
| cvc5::parser::SetOptionCommand::SetOptionCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) |
7682 |
| cvc5::parser::DeclareSortCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
11514 |
| cvc5::parser::DeclareSortCommand::DeclareSortCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, unsigned long) |
11514 |
| cvc5::parser::SetInfoCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
12739 |
| cvc5::parser::CheckSatCommand::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
17181 |
| cvc5::parser::CheckSatCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
17224 |
| cvc5::parser::SetInfoCommand::SetInfoCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) |
19082 |
| cvc5::parser::SetBenchmarkLogicCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
24131 |
| cvc5::parser::SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >) |
24135 |
| cvc5::parser::CheckSatCommand::getResult() const |
26515 |
| cvc5::parser::CheckSatCommand::CheckSatCommand() |
26520 |
| cvc5::parser::sexprToString[abi:cxx11](cvc5::Term) |
26873 |
| cvc5::parser::AssertCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
36064 |
| cvc5::parser::Cmd::termToNode(cvc5::Term const&) |
38242 |
| cvc5::parser::DeclareFunctionCommand::toStream(std::basic_ostream<char, std::char_traits<char> >&) const |
79454 |
| cvc5::parser::Cmd::sortVectorToTypeNodes(std::vector<cvc5::Sort, std::allocator<cvc5::Sort> > const&) |
80262 |
| cvc5::parser::Cmd::sortToTypeNode(cvc5::Sort const&) |
82000 |
| cvc5::parser::AssertCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
137839 |
| cvc5::parser::Cmd::toString[abi:cxx11]() const |
138030 |
| cvc5::parser::AssertCommand::AssertCommand(cvc5::Term const&) |
209955 |
| cvc5::parser::DeclareFunctionCommand::invoke(cvc5::Solver*, cvc5::parser::SymManager*) |
332283 |
| cvc5::parser::DeclareFunctionCommand::DeclareFunctionCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::vector<cvc5::Sort, std::allocator<cvc5::Sort> > const&, cvc5::Sort) |
332283 |
| cvc5::parser::DeclarationDefinitionCommand::bindToTerm(cvc5::parser::SymManager*, cvc5::Term, bool) |
342688 |
| cvc5::parser::tryBindToTerm(cvc5::parser::SymManager*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, cvc5::Term, bool, std::basic_ostream<char, std::char_traits<char> >*) |
343448 |
| cvc5::parser::DeclarationDefinitionCommand::DeclarationDefinitionCommand(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) |
354960 |
| cvc5::parser::Cmd::printResult(cvc5::Solver*, std::basic_ostream<char, std::char_traits<char> >&) const |
549405 |
| cvc5::parser::Cmd::fail() const |
574843 |
| cvc5::parser::Cmd::invokeAndPrintResult(cvc5::Solver*, cvc5::parser::SymManager*) |
574845 |
| cvc5::parser::Cmd::~Cmd().2 |
674877 |
| cvc5::parser::Cmd::Cmd() |
674887 |
| cvc5::parser::Cmd::ok() const |
1125077 |