cprover
Loading...
Searching...
No Matches
smt2_incremental_decision_proceduret Class Referencefinal

#include <smt2_incremental_decision_procedure.h>

+ Inheritance diagram for smt2_incremental_decision_proceduret:
+ Collaboration diagram for smt2_incremental_decision_proceduret:

Classes

class  sequencet
 

Public Member Functions

 smt2_incremental_decision_proceduret (const namespacet &_ns, std::unique_ptr< smt_base_solver_processt > solver_process, message_handlert &message_handler)
 
exprt handle (const exprt &expr) override
 Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.
 
exprt get (const exprt &expr) const override
 Return expr with variables replaced by values from satisfying assignment if available.
 
void print_assignment (std::ostream &out) const override
 Print satisfying assignment to out.
 
std::string decision_procedure_text () const override
 Return a textual description of the decision procedure.
 
std::size_t get_number_of_solver_calls () const override
 Return the number of incremental solver calls.
 
void set_to (const exprt &expr, bool value) override
 For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
 
void push (const std::vector< exprt > &assumptions) override
 Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.
 
void push () override
 Push a new context on the stack This context becomes a child context nested in the current context.
 
void pop () override
 Pop whatever is on top of the stack.
 
- Public Member Functions inherited from stack_decision_proceduret
virtual void push (const std::vector< exprt > &assumptions)=0
 Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.
 
virtual void push ()=0
 Push a new context on the stack This context becomes a child context nested in the current context.
 
virtual void pop ()=0
 Pop whatever is on top of the stack.
 
virtual ~stack_decision_proceduret ()=default
 
- Public Member Functions inherited from decision_proceduret
virtual void set_to (const exprt &expr, bool value)=0
 For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
 
void set_to_true (const exprt &expr)
 For a Boolean expression expr, add the constraint 'expr'.
 
void set_to_false (const exprt &expr)
 For a Boolean expression expr, add the constraint 'not expr'.
 
virtual exprt handle (const exprt &expr)=0
 Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.
 
resultt operator() ()
 Run the decision procedure to solve the problem.
 
virtual exprt get (const exprt &expr) const =0
 Return expr with variables replaced by values from satisfying assignment if available.
 
virtual void print_assignment (std::ostream &out) const =0
 Print satisfying assignment to out.
 
virtual std::string decision_procedure_text () const =0
 Return a textual description of the decision procedure.
 
virtual std::size_t get_number_of_solver_calls () const =0
 Return the number of incremental solver calls.
 
virtual ~decision_proceduret ()
 

Protected Member Functions

resultt dec_solve () override
 Run the decision procedure to solve the problem.
 
void define_dependent_functions (const exprt &expr)
 Defines any functions which expr depends on, which have not yet been defined, along with their dependencies in turn.
 
void ensure_handle_for_expr_defined (const exprt &expr)
 
virtual resultt dec_solve ()=0
 Run the decision procedure to solve the problem.
 

Protected Attributes

const namespacetns
 
size_t number_of_solver_calls
 
std::unique_ptr< smt_base_solver_processtsolver_process
 
messaget log
 
class smt2_incremental_decision_proceduret::sequencet handle_sequence
 
std::unordered_map< exprt, smt_identifier_termt, irep_hashexpression_handle_identifiers
 
std::unordered_map< exprt, smt_identifier_termt, irep_hashexpression_identifiers
 

Additional Inherited Members

- Public Types inherited from decision_proceduret
enum class  resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }
 Result of running the decision procedure. More...
 

Detailed Description

Definition at line 23 of file smt2_incremental_decision_procedure.h.

Constructor & Destructor Documentation

◆ smt2_incremental_decision_proceduret()

smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret ( const namespacet _ns,
std::unique_ptr< smt_base_solver_processt solver_process,
message_handlert message_handler 
)
explicit
Parameters
_nsNamespace for looking up the expressions which symbol_exprts relate to.
solver_processThe smt2 solver process communication interface.
message_handlerThe messaging system to be used for logging purposes.

Definition at line 128 of file smt2_incremental_decision_procedure.cpp.

Member Function Documentation

◆ dec_solve()

decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve ( )
overrideprotectedvirtual

Run the decision procedure to solve the problem.

Implements decision_proceduret.

Definition at line 305 of file smt2_incremental_decision_procedure.cpp.

◆ decision_procedure_text()

std::string smt2_incremental_decision_proceduret::decision_procedure_text ( ) const
overridevirtual

Return a textual description of the decision procedure.

Implements decision_proceduret.

Definition at line 240 of file smt2_incremental_decision_procedure.cpp.

◆ define_dependent_functions()

void smt2_incremental_decision_proceduret::define_dependent_functions ( const exprt expr)
protected

Defines any functions which expr depends on, which have not yet been defined, along with their dependencies in turn.

Definition at line 75 of file smt2_incremental_decision_procedure.cpp.

◆ ensure_handle_for_expr_defined()

void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined ( const exprt expr)
protected

Definition at line 143 of file smt2_incremental_decision_procedure.cpp.

◆ get()

exprt smt2_incremental_decision_proceduret::get ( const exprt expr) const
overridevirtual

Return expr with variables replaced by values from satisfying assignment if available.

Return nil if not available

Implements decision_proceduret.

Definition at line 183 of file smt2_incremental_decision_procedure.cpp.

◆ get_number_of_solver_calls()

std::size_t smt2_incremental_decision_proceduret::get_number_of_solver_calls ( ) const
overridevirtual

Return the number of incremental solver calls.

Implements decision_proceduret.

Definition at line 246 of file smt2_incremental_decision_procedure.cpp.

◆ handle()

exprt smt2_incremental_decision_proceduret::handle ( const exprt expr)
overridevirtual

Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.

The returned expression may be the expression itself or a more compact but solver-specific representation.

Implements decision_proceduret.

Definition at line 160 of file smt2_incremental_decision_procedure.cpp.

◆ pop()

void smt2_incremental_decision_proceduret::pop ( )
overridevirtual

Pop whatever is on top of the stack.

Popping from the empty stack results in an invariant violation.

Implements stack_decision_proceduret.

Definition at line 287 of file smt2_incremental_decision_procedure.cpp.

◆ print_assignment()

void smt2_incremental_decision_proceduret::print_assignment ( std::ostream &  out) const
overridevirtual

Print satisfying assignment to out.

Implements decision_proceduret.

Definition at line 233 of file smt2_incremental_decision_procedure.cpp.

◆ push() [1/2]

void smt2_incremental_decision_proceduret::push ( )
overridevirtual

Push a new context on the stack This context becomes a child context nested in the current context.

Implements stack_decision_proceduret.

Definition at line 282 of file smt2_incremental_decision_procedure.cpp.

◆ push() [2/2]

void smt2_incremental_decision_proceduret::push ( const std::vector< exprt > &  assumptions)
overridevirtual

Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.

This context becomes a child context nested in the current context. An assumption is usually obtained by calling decision_proceduret::handle. Thus it can be a Boolean expression or something more solver-specific such as literal_exprt. An empty vector of assumptions counts as an element on the stack (and therefore needs to be popped), but has no effect beyond that.

Implements stack_decision_proceduret.

Definition at line 271 of file smt2_incremental_decision_procedure.cpp.

◆ set_to()

void smt2_incremental_decision_proceduret::set_to ( const exprt expr,
bool  value 
)
overridevirtual

For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.

Implements decision_proceduret.

Definition at line 251 of file smt2_incremental_decision_procedure.cpp.

Member Data Documentation

◆ expression_handle_identifiers

std::unordered_map<exprt, smt_identifier_termt, irep_hash> smt2_incremental_decision_proceduret::expression_handle_identifiers
protected

Definition at line 78 of file smt2_incremental_decision_procedure.h.

◆ expression_identifiers

std::unordered_map<exprt, smt_identifier_termt, irep_hash> smt2_incremental_decision_proceduret::expression_identifiers
protected

Definition at line 80 of file smt2_incremental_decision_procedure.h.

◆ handle_sequence

class smt2_incremental_decision_proceduret::sequencet smt2_incremental_decision_proceduret::handle_sequence
protected

◆ log

messaget smt2_incremental_decision_proceduret::log
protected

Definition at line 64 of file smt2_incremental_decision_procedure.h.

◆ ns

const namespacet& smt2_incremental_decision_proceduret::ns
protected

Definition at line 59 of file smt2_incremental_decision_procedure.h.

◆ number_of_solver_calls

size_t smt2_incremental_decision_proceduret::number_of_solver_calls
protected

Definition at line 61 of file smt2_incremental_decision_procedure.h.

◆ solver_process

std::unique_ptr<smt_base_solver_processt> smt2_incremental_decision_proceduret::solver_process
protected

Definition at line 63 of file smt2_incremental_decision_procedure.h.


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