#include <bitblast_conv.h>
|
| | bitblast_smt_ast (smt_solver_baset *ctx, const smt_sort *s) |
| | smt_ast (smt_solver_baset *ctx, smt_sortt s) |
| virtual | ~smt_ast ()=default |
| virtual smt_astt | with_sort (smt_solver_baset *ctx, smt_sortt s) const |
| | The same solver term under a different sort.
|
| virtual smt_astt | ite (smt_solver_baset *ctx, smt_astt cond, smt_astt falseop) const |
| virtual smt_astt | eq (smt_solver_baset *ctx, smt_astt other) const |
| | Abstractly produce an equality.
|
| virtual void | assign (smt_solver_baset *ctx, smt_astt sym) const |
| | Abstractly produce an assign.
|
| virtual smt_astt | update (smt_solver_baset *ctx, smt_astt value, unsigned int idx, const expr2tc &idx_expr=expr2tc()) const |
| | Abstractly produce an "update", i.e., an array 'with' or tuple 'with'.
|
| virtual smt_astt | select (smt_solver_baset *ctx, const expr2tc &idx) const |
| | Select a value from an array, for both normal arrays and tuple arrays.
|
| virtual smt_astt | project (smt_solver_baset *ctx, unsigned int elem) const |
| | Project a member from a structure, or an field-array from a struct array.
|
| virtual void | dump () const |
◆ bitblast_smt_ast()
◆ bv
The documentation for this class was generated from the following file:
1.15.0