cprover
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:

Public Member Functions

 smt2_incremental_decision_proceduret (std::string solver_command)
 
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. More...
 
exprt get (const exprt &expr) const override
 Return expr with variables replaced by values from satisfying assignment if available. More...
 
void print_assignment (std::ostream &out) const override
 Print satisfying assignment to out. More...
 
std::string decision_procedure_text () const override
 Return a textual description of the decision procedure. More...
 
std::size_t get_number_of_solver_calls () const override
 Return the number of incremental solver calls. More...
 
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'. More...
 
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. More...
 
void push () override
 Push a new context on the stack This context becomes a child context nested in the current context. More...
 
void pop () override
 Pop whatever is on top of the stack. More...
 
- Public Member Functions inherited from stack_decision_proceduret
virtual ~stack_decision_proceduret ()=default
 
- Public Member Functions inherited from decision_proceduret
void set_to_true (const exprt &expr)
 For a Boolean expression expr, add the constraint 'expr'. More...
 
void set_to_false (const exprt &expr)
 For a Boolean expression expr, add the constraint 'not expr'. More...
 
resultt operator() ()
 Run the decision procedure to solve the problem. More...
 
virtual ~decision_proceduret ()
 

Protected Member Functions

resultt dec_solve () override
 Run the decision procedure to solve the problem. More...
 

Protected Attributes

std::string solver_command
 This is where we store the solver command for reporting the solver used. More...
 
size_t number_of_solver_calls
 

Additional Inherited Members

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

Detailed Description

Definition at line 11 of file smt2_incremental_decision_procedure.h.

Constructor & Destructor Documentation

◆ smt2_incremental_decision_proceduret()

smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret ( std::string  solver_command)
explicit
Parameters
solver_commandThe command and arguments for invoking the smt2 solver.

Definition at line 7 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 69 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 30 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 18 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 36 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 13 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 64 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 23 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 59 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 48 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 41 of file smt2_incremental_decision_procedure.cpp.

Member Data Documentation

◆ number_of_solver_calls

size_t smt2_incremental_decision_proceduret::number_of_solver_calls
protected

Definition at line 38 of file smt2_incremental_decision_procedure.h.

◆ solver_command

std::string smt2_incremental_decision_proceduret::solver_command
protected

This is where we store the solver command for reporting the solver used.

Definition at line 37 of file smt2_incremental_decision_procedure.h.


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