cprover
|
#include <solvers/smt2_incremental/convert_expr_to_smt.h>
#include <solvers/prop/literal_expr.h>
#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
#include <solvers/smt2_incremental/smt_core_theory.h>
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/byte_operators.h>
#include <util/expr.h>
#include <util/expr_cast.h>
#include <util/floatbv_expr.h>
#include <util/mathematical_expr.h>
#include <util/pointer_expr.h>
#include <util/pointer_predicates.h>
#include <util/range.h>
#include <util/std_expr.h>
#include <util/string_constant.h>
#include <functional>
#include <numeric>
Go to the source code of this file.
Classes | |
struct | sort_based_literal_convertert |
Definition at line 583 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 472 of file convert_expr_to_smt.cpp.
Definition at line 222 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 486 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 618 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 479 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 127 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 148 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 134 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 141 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 649 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 569 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 576 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 120 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 112 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 664 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 672 of file convert_expr_to_smt.cpp.
Definition at line 372 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 251 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 445 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 637 of file convert_expr_to_smt.cpp.
Converts the expression
to an smt encoding of the same expression stored as term ast (abstract syntax tree).
Definition at line 679 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 548 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 555 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 66 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 631 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 263 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 271 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 402 of file convert_expr_to_smt.cpp.
Definition at line 186 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 240 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 493 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 526 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 534 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 597 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 604 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 590 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 611 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 625 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 518 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 354 of file convert_expr_to_smt.cpp.
Definition at line 411 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 452 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 53 of file convert_expr_to_smt.cpp.
Definition at line 246 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 257 of file convert_expr_to_smt.cpp.
Definition at line 228 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 337 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 656 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 562 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 499 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 179 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 541 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 73 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 47 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 60 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 155 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 172 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 80 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 512 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 643 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 506 of file convert_expr_to_smt.cpp.
Definition at line 234 of file convert_expr_to_smt.cpp.
|
static |
Converts operator expressions with 2 or more operands to terms expressed as binary operator application.
expr | The expression to convert. |
factory | The factory function which makes applications of the relevant smt term, when applied to the term operands. |
The conversion used is left associative for instances with 3 or more operands. The SMT standard / core theory version 2.6 actually supports applying the and
, or
and xor
to 3 or more operands. However our internal smt_core_theoryt
does not support this currently and converting to binary application has the advantage of making the order of evaluation explicit.
Definition at line 206 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 279 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 29 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 24 of file convert_expr_to_smt.cpp.
Converts the type
to an smt encoding of the same expression stored as sort ast (abstract syntax tree).
Definition at line 34 of file convert_expr_to_smt.cpp.
Definition at line 300 of file convert_expr_to_smt.cpp.