cvc4-1.3
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::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-2013  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.