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 485 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 374 of file convert_expr_to_smt.cpp.
Definition at line 212 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 388 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 520 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 381 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 291 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 551 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 471 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 478 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 566 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 574 of file convert_expr_to_smt.cpp.
Definition at line 338 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 241 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 361 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 539 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 581 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 450 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 457 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 66 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 533 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 253 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 261 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 344 of file convert_expr_to_smt.cpp.
Definition at line 176 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 230 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 395 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 428 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 436 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 499 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 506 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 492 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 513 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 527 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 420 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 332 of file convert_expr_to_smt.cpp.
Definition at line 353 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 368 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 53 of file convert_expr_to_smt.cpp.
Definition at line 236 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 247 of file convert_expr_to_smt.cpp.
Definition at line 218 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 326 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 558 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 464 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 401 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 169 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 443 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 162 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 80 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 414 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 545 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 408 of file convert_expr_to_smt.cpp.
Definition at line 224 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 196 of file convert_expr_to_smt.cpp.
|
static |
Definition at line 269 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.