command.h File Reference

Implementation of the command pattern on SmtEngines. More...

#include "cvc4_public.h"
#include <iostream>
#include <sstream>
#include <string>
#include <vector>
#include <map>
#include "expr/expr.h"
#include "expr/type.h"
#include "expr/variable_type_map.h"
#include "util/result.h"
#include "util/sexpr.h"
#include "util/datatype.h"
#include "util/proof.h"

Go to the source code of this file.

Data Structures
class	CVC4::CommandPrintSuccess
	IOStream manipulator to print success messages or not. More...
class	CVC4::CommandPrintSuccess::Scope
	Set the print-success state on the output stream for the current stack scope. More...
class	CVC4::CommandStatus
class	CVC4::CommandSuccess
class	CVC4::CommandUnsupported
class	CVC4::CommandFailure
class	CVC4::Command
class	CVC4::Command::ExportTransformer
class	CVC4::EmptyCommand
	EmptyCommands are the residue of a command after the parser handles them (and there's nothing left to do). More...
class	CVC4::EchoCommand
class	CVC4::AssertCommand
class	CVC4::PushCommand
class	CVC4::PopCommand
class	CVC4::DeclarationDefinitionCommand
class	CVC4::DeclareFunctionCommand
class	CVC4::DeclareTypeCommand
class	CVC4::DefineTypeCommand
class	CVC4::DefineFunctionCommand
class	CVC4::DefineNamedFunctionCommand
	This differs from DefineFunctionCommand only in that it instructs the SmtEngine to "remember" this function for later retrieval with getAssignment(). More...
class	CVC4::SetUserAttributeCommand
	The command when an attribute is set by a user. More...
class	CVC4::CheckSatCommand
class	CVC4::QueryCommand
class	CVC4::SimplifyCommand
class	CVC4::ExpandDefinitionsCommand
class	CVC4::GetValueCommand
class	CVC4::GetAssignmentCommand
class	CVC4::GetModelCommand
class	CVC4::GetProofCommand
class	CVC4::GetInstantiationsCommand
class	CVC4::GetUnsatCoreCommand
class	CVC4::GetAssertionsCommand
class	CVC4::SetBenchmarkStatusCommand
class	CVC4::SetBenchmarkLogicCommand
class	CVC4::SetInfoCommand
class	CVC4::GetInfoCommand
class	CVC4::SetOptionCommand
class	CVC4::GetOptionCommand
class	CVC4::DatatypeDeclarationCommand
class	CVC4::RewriteRuleCommand
class	CVC4::PropagateRuleCommand
class	CVC4::QuitCommand
class	CVC4::CommentCommand
class	CVC4::CommandSequence
class	CVC4::DeclarationSequence

Namespaces
	CVC4

Enumerations
enum	CVC4::BenchmarkStatus { CVC4::SMT_SATISFIABLE, CVC4::SMT_UNSATISFIABLE, CVC4::SMT_UNKNOWN }
	The status an SMT benchmark can have. More...

Functions
std::ostream &	CVC4::operator<< (std::ostream &, const Command &) throw ()
std::ostream &	CVC4::operator<< (std::ostream &, const Command *) throw ()
std::ostream &	CVC4::operator<< (std::ostream &, const CommandStatus &) throw ()
std::ostream &	CVC4::operator<< (std::ostream &, const CommandStatus *) throw ()
std::ostream &	CVC4::operator<< (std::ostream &out, BenchmarkStatus status) throw ()
std::ostream &	CVC4::operator<< (std::ostream &out, CommandPrintSuccess cps) throw ()
	Sets the default print-success setting when pretty-printing an Expr to an ostream. More...

Detailed Description

Implementation of the command pattern on SmtEngines.

** Original author: Morgan Deters
** Major contributors: none
** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014  New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.

Implementation of the command pattern on SmtEngines. Command objects are generated by the parser (typically) to implement the commands in parsed input (see Parser::parseNextCommand()), or by client code.

Definition in file command.h.