cprover
Loading...
Searching...
No Matches
smt2_dect Class Reference

Decision procedure interface for various SMT 2.x solvers. More...

#include <smt2_dec.h>

+ Inheritance diagram for smt2_dect:
+ Collaboration diagram for smt2_dect:

Public Member Functions

 smt2_dect (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, message_handlert &_message_handler)
 
resultt dec_solve () override
 Run the decision procedure to solve the problem.
 
std::string decision_procedure_text () const override
 Return a textual description of the decision procedure.
 
- Public Member Functions inherited from smt2_convt
 smt2_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
 
 ~smt2_convt () override=default
 
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.
 
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'.
 
exprt get (const exprt &expr) const override
 Return expr with variables replaced by values from satisfying assignment if available.
 
std::string decision_procedure_text () const override
 Return a textual description of the decision procedure.
 
void print_assignment (std::ostream &out) const override
 Print satisfying assignment to out.
 
void push () override
 Unimplemented.
 
void push (const std::vector< exprt > &_assumptions) override
 Currently, only implements a single stack element (no nested contexts)
 
void pop () override
 Currently, only implements a single stack element (no nested contexts)
 
std::size_t get_number_of_solver_calls () const override
 Return the number of incremental solver calls.
 
- 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 read_result (std::istream &in)
 
- Protected Member Functions inherited from smt2_convt
resultt dec_solve () override
 Run the decision procedure to solve the problem.
 
void write_header ()
 
void write_footer ()
 Writes the end of the SMT file to the smt_convt::out stream.
 
bool use_array_theory (const exprt &)
 
void flatten_array (const exprt &)
 produce a flat bit-vector for a given array of fixed size
 
void convert_typecast (const typecast_exprt &expr)
 
void convert_floatbv_typecast (const floatbv_typecast_exprt &expr)
 
void convert_struct (const struct_exprt &expr)
 
void convert_union (const union_exprt &expr)
 
void convert_constant (const constant_exprt &expr)
 
void convert_relation (const binary_relation_exprt &)
 
void convert_is_dynamic_object (const unary_exprt &)
 
void convert_plus (const plus_exprt &expr)
 
void convert_minus (const minus_exprt &expr)
 
void convert_div (const div_exprt &expr)
 
void convert_mult (const mult_exprt &expr)
 
void convert_rounding_mode_FPA (const exprt &expr)
 Converting a constant or symbolic rounding mode to SMT-LIB.
 
void convert_floatbv_plus (const ieee_float_op_exprt &expr)
 
void convert_floatbv_minus (const ieee_float_op_exprt &expr)
 
void convert_floatbv_div (const ieee_float_op_exprt &expr)
 
void convert_floatbv_mult (const ieee_float_op_exprt &expr)
 
void convert_floatbv_rem (const binary_exprt &expr)
 
void convert_mod (const mod_exprt &expr)
 
void convert_euclidean_mod (const euclidean_mod_exprt &expr)
 
void convert_index (const index_exprt &expr)
 
void convert_member (const member_exprt &expr)
 
void convert_with (const with_exprt &expr)
 
void convert_update (const exprt &expr)
 
void convert_expr (const exprt &)
 
void convert_type (const typet &)
 
void convert_literal (const literalt)
 
literalt convert (const exprt &expr)
 
tvt l_get (literalt l) const
 
exprt prepare_for_convert_expr (const exprt &expr)
 Perform steps necessary before an expression is passed to convert_expr.
 
exprt lower_byte_operators (const exprt &expr)
 Lower byte_update and byte_extract operations within expr.
 
void find_symbols (const exprt &expr)
 
void find_symbols (const typet &type)
 
void find_symbols_rec (const typet &type, std::set< irep_idt > &recstack)
 
constant_exprt parse_literal (const irept &, const typet &type)
 
struct_exprt parse_struct (const irept &s, const struct_typet &type)
 
exprt parse_union (const irept &s, const union_typet &type)
 
exprt parse_array (const irept &s, const array_typet &type)
 This function is for parsing array output from SMT solvers when "(get-value |???|)" returns an array object.
 
exprt parse_rec (const irept &s, const typet &type)
 
void walk_array_tree (std::unordered_map< int64_t, exprt > *operands_map, const irept &src, const array_typet &type)
 This function walks the SMT output and populates a map with index/value pairs for the array.
 
void convert_floatbv (const exprt &expr)
 
std::string type2id (const typet &) const
 
std::string floatbv_suffix (const exprt &) const
 
const smt2_symboltto_smt2_symbol (const exprt &expr)
 
void flatten2bv (const exprt &)
 
void unflatten (wheret, const typet &, unsigned nesting=0)
 
void convert_address_of_rec (const exprt &expr, const pointer_typet &result_type)
 
void define_object_size (const irep_idt &id, const exprt &expr)
 
 smt2_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
 
 ~smt2_convt () override=default
 
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.
 
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'.
 
exprt get (const exprt &expr) const override
 Return expr with variables replaced by values from satisfying assignment if available.
 
std::string decision_procedure_text () const override
 Return a textual description of the decision procedure.
 
void print_assignment (std::ostream &out) const override
 Print satisfying assignment to out.
 
void push () override
 Unimplemented.
 
void push (const std::vector< exprt > &_assumptions) override
 Currently, only implements a single stack element (no nested contexts)
 
void pop () override
 Currently, only implements a single stack element (no nested contexts)
 
std::size_t get_number_of_solver_calls () const override
 Return the number of incremental solver calls.
 
- Protected 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
 
virtual resultt dec_solve ()=0
 Run the decision procedure to solve the problem.
 
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 Attributes

message_handlertmessage_handler
 
std::stringstream cached_output
 Everything except the footer is cached, so that output files can be rewritten with varying footers.
 
- Protected Attributes inherited from smt2_stringstreamt
std::stringstream stringstream
 
- Protected Attributes inherited from smt2_convt
const namespacetns
 
std::ostream & out
 
std::string benchmark
 
std::string notes
 
std::string logic
 
solvert solver
 
std::vector< exprtassumptions
 
boolbv_widtht boolbv_width
 
std::size_t number_of_solver_calls = 0
 
letifyt letify
 
std::set< irep_idtbvfp_set
 
pointer_logict pointer_logic
 
identifier_mapt identifier_map
 
datatype_mapt datatype_map
 
defined_expressionst defined_expressions
 
std::unordered_map< irep_idt, bool > set_values
 The values which boolean identifiers have been smt2_convt::set_to or in other words those which are asserted as true / false in the output smt2 formula.
 
defined_expressionst object_sizes
 
smt2_identifierst smt2_identifiers
 
std::size_t no_boolean_variables
 
std::vector< bool > boolean_assignment
 
bool use_FPA_theory
 
bool use_array_of_bool
 
bool use_as_const
 
bool use_check_sat_assuming
 
bool use_datatypes
 
bool use_lambda_for_array
 
bool emit_set_logic
 

Additional Inherited Members

- Public Types inherited from smt2_convt
enum class  solvert {
  GENERIC , BOOLECTOR , CPROVER_SMT2 , CVC3 ,
  CVC4 , MATHSAT , YICES , Z3
}
 
- Public Types inherited from decision_proceduret
enum class  resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }
 Result of running the decision procedure. More...
 
- Static Public Member Functions inherited from smt2_convt
static std::string convert_identifier (const irep_idt &identifier)
 
- Public Attributes inherited from smt2_convt
bool use_FPA_theory
 
bool use_array_of_bool
 
bool use_as_const
 
bool use_check_sat_assuming
 
bool use_datatypes
 
bool use_lambda_for_array
 
bool emit_set_logic
 
- Protected Types inherited from smt2_convt
enum class  wheret { BEGIN , END }
 
typedef std::unordered_map< irep_idt, identifiertidentifier_mapt
 
typedef std::map< typet, std::string > datatype_mapt
 
typedef std::map< exprt, irep_idtdefined_expressionst
 
typedef std::set< std::string > smt2_identifierst
 
enum class  solvert {
  GENERIC , BOOLECTOR , CPROVER_SMT2 , CVC3 ,
  CVC4 , MATHSAT , YICES , Z3
}
 
- Protected Types inherited from decision_proceduret
enum class  resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }
 Result of running the decision procedure. More...
 
- Static Protected Member Functions inherited from smt2_convt
static std::string convert_identifier (const irep_idt &identifier)
 

Detailed Description

Decision procedure interface for various SMT 2.x solvers.

Definition at line 27 of file smt2_dec.h.

Constructor & Destructor Documentation

◆ smt2_dect()

smt2_dect::smt2_dect ( const namespacet _ns,
const std::string &  _benchmark,
const std::string &  _notes,
const std::string &  _logic,
solvert  _solver,
message_handlert _message_handler 
)
inline

Definition at line 30 of file smt2_dec.h.

Member Function Documentation

◆ dec_solve()

decision_proceduret::resultt smt2_dect::dec_solve ( )
overridevirtual

Run the decision procedure to solve the problem.

Reimplemented from smt2_convt.

Definition at line 34 of file smt2_dec.cpp.

◆ decision_procedure_text()

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

Return a textual description of the decision procedure.

Reimplemented from smt2_convt.

Definition at line 18 of file smt2_dec.cpp.

◆ read_result()

decision_proceduret::resultt smt2_dect::read_result ( std::istream &  in)
protected

Definition at line 133 of file smt2_dec.cpp.

Member Data Documentation

◆ cached_output

std::stringstream smt2_dect::cached_output
protected

Everything except the footer is cached, so that output files can be rewritten with varying footers.

Definition at line 50 of file smt2_dec.h.

◆ message_handler

message_handlert& smt2_dect::message_handler
protected

Definition at line 46 of file smt2_dec.h.


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