cprover
decision_proceduret Class Referenceabstract

#include <decision_procedure.h>

+ Inheritance diagram for decision_proceduret:

Public Types

enum  resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }
 

Public Member Functions

virtual ~decision_proceduret ()
 
virtual exprt get (const exprt &expr) const =0
 
virtual void print_assignment (std::ostream &out) const =0
 
virtual void set_to (const exprt &expr, bool value)=0
 
void set_to_true (const exprt &expr)
 
void set_to_false (const exprt &expr)
 
virtual resultt dec_solve ()=0
 
resultt operator() ()
 
virtual std::string decision_procedure_text () const =0
 

Detailed Description

Definition at line 20 of file decision_procedure.h.

Member Enumeration Documentation

◆ resultt

Enumerator
D_SATISFIABLE 
D_UNSATISFIABLE 
D_ERROR 

Definition at line 43 of file decision_procedure.h.

Constructor & Destructor Documentation

◆ ~decision_proceduret()

decision_proceduret::~decision_proceduret ( )
virtual

Definition at line 14 of file decision_procedure.cpp.

Member Function Documentation

◆ dec_solve()

virtual resultt decision_proceduret::dec_solve ( )
pure virtual

◆ decision_procedure_text()

virtual std::string decision_proceduret::decision_procedure_text ( ) const
pure virtual

◆ get()

virtual exprt decision_proceduret::get ( const exprt expr) const
pure virtual

◆ operator()()

resultt decision_proceduret::operator() ( void  )
inline

Definition at line 48 of file decision_procedure.h.

◆ print_assignment()

virtual void decision_proceduret::print_assignment ( std::ostream &  out) const
pure virtual

Implemented in smt2_convt, prop_conv_solvert, and boolbvt.

◆ set_to()

virtual void decision_proceduret::set_to ( const exprt expr,
bool  value 
)
pure virtual

◆ set_to_false()

void decision_proceduret::set_to_false ( const exprt expr)
inline

Definition at line 39 of file decision_procedure.h.

◆ set_to_true()

void decision_proceduret::set_to_true ( const exprt expr)
inline

Definition at line 36 of file decision_procedure.h.


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