/dports/math/boolector/boolector-3.2.2/src/ |
H A D | btorexp.h | 53 BtorNode *btor_exp_implies (Btor *btor, BtorNode *e0, BtorNode *e1); 60 BtorNode *btor_exp_iff (Btor *btor, BtorNode *e0, BtorNode *e1); 69 BtorNode *btor_exp_eq (Btor *btor, BtorNode *e0, BtorNode *e1); 76 BtorNode *btor_exp_ne (Btor *btor, BtorNode *e0, BtorNode *e1); 157 BtorNode *btor_exp_bv_xor (Btor *btor, BtorNode *e0, BtorNode *e1); 164 BtorNode *btor_exp_bv_xnor (Btor *btor, BtorNode *e0, BtorNode *e1); 171 BtorNode *btor_exp_bv_and (Btor *btor, BtorNode *e0, BtorNode *e1); 192 BtorNode *btor_exp_bv_or (Btor *btor, BtorNode *e0, BtorNode *e1); 199 BtorNode *btor_exp_bv_nor (Btor *btor, BtorNode *e0, BtorNode *e1); 206 BtorNode *btor_exp_bv_add (Btor *btor, BtorNode *e0, BtorNode *e1); [all …]
|
H A D | btornode.h | 743 BtorNode *btor_node_param_set_assigned_exp (BtorNode *param, BtorNode *exp); 764 BtorNode *btor_node_create_bv_and (Btor *btor, BtorNode *e0, BtorNode *e1); 766 BtorNode *btor_node_create_eq (Btor *btor, BtorNode *e0, BtorNode *e1); 768 BtorNode *btor_node_create_bv_add (Btor *btor, BtorNode *e0, BtorNode *e1); 770 BtorNode *btor_node_create_bv_mul (Btor *btor, BtorNode *e0, BtorNode *e1); 772 BtorNode *btor_node_create_bv_ult (Btor *btor, BtorNode *e0, BtorNode *e1); 774 BtorNode *btor_node_create_bv_sll (Btor *btor, BtorNode *e0, BtorNode *e1); 776 BtorNode *btor_node_create_bv_srl (Btor *btor, BtorNode *e0, BtorNode *e1); 778 BtorNode *btor_node_create_bv_udiv (Btor *btor, BtorNode *e0, BtorNode *e1); 780 BtorNode *btor_node_create_bv_urem (Btor *btor, BtorNode *e0, BtorNode *e1); [all …]
|
H A D | btorrewrite.c | 372 BtorNode *a = *(BtorNode **) p; in cmp_node_id() 373 BtorNode *b = *(BtorNode **) q; in cmp_node_id() 554 static BtorNode *rewrite_eq_exp (Btor *, BtorNode *, BtorNode *); 555 static BtorNode *rewrite_ult_exp (Btor *, BtorNode *, BtorNode *); 556 static BtorNode *rewrite_and_exp (Btor *, BtorNode *, BtorNode *); 557 static BtorNode *rewrite_add_exp (Btor *, BtorNode *, BtorNode *); 558 static BtorNode *rewrite_mul_exp (Btor *, BtorNode *, BtorNode *); 559 static BtorNode *rewrite_udiv_exp (Btor *, BtorNode *, BtorNode *); 562 static BtorNode *rewrite_sll_exp (Btor *, BtorNode *, BtorNode *); 563 static BtorNode *rewrite_srl_exp (Btor *, BtorNode *, BtorNode *); [all …]
|
H A D | btorexp.c | 19 BtorNode * 85 BtorNode * 91 BtorNode * 97 BtorNode * 115 BtorNode * 142 BtorNode * 150 BtorNode * 164 BtorNode * 247 btor_exp_cond (Btor *btor, BtorNode *e_cond, BtorNode *e_if, BtorNode *e_else) in btor_exp_cond() 629 BtorNode *(*func) (Btor *, BtorNode *, BtorNode *), in create_bin_n_exp() argument [all …]
|
H A D | btordbg.h | 43 BtorNode* nodes[], 51 const BtorNode* exp, 64 const BtorNode* e0, 65 const BtorNode* e1); 68 const BtorNode* e0, 69 const BtorNode* e1); 72 const BtorNode* e0, 73 const BtorNode* e1); 85 const BtorNode* e_cond, 86 const BtorNode* e_if, [all …]
|
H A D | btorbeta.h | 17 BtorNode* btor_beta_reduce_full (Btor* btor, 18 BtorNode* exp, 21 BtorNode* btor_beta_reduce_merge (Btor* btor, 22 BtorNode* exp, 25 BtorNode* btor_beta_reduce_partial (Btor* btor, 26 BtorNode* exp, 29 BtorNode* btor_beta_reduce_partial_collect (Btor* btor, 30 BtorNode* exp, 39 BtorNode* btor_beta_reduce_bounded (Btor* btor, BtorNode* exp, int32_t bound); 41 void btor_beta_assign_param (Btor* btor, BtorNode* lambda, BtorNode* arg); [all …]
|
H A D | btornode.c | 296 BtorNode * 1042 BtorNode * 1053 BtorNode * 1110 BtorNode * 1121 BtorNode * 1133 BtorNode * 1292 BtorNode * 1387 BtorNode * 1446 BtorNode * 1453 BtorNode * [all …]
|
H A D | btorcore.h | 56 BtorNode **chains; 117 BtorNode *true_exp; 306 BtorNode *fun); 319 BtorNode *btor_simplify_exp (Btor *btor, BtorNode *exp); 322 BtorNode *exp, 326 BtorNode *btor_node_get_simplified (Btor *btor, BtorNode *exp); 332 void btor_insert_substitution (Btor *, BtorNode *, BtorNode *, bool); 333 BtorNode *btor_find_substitution (Btor *, BtorNode *); 336 BtorNode *btor_substitute_node (Btor *btor, 342 BtorNode *btor_substitute_nodes (Btor *btor, [all …]
|
H A D | btorrewrite.h | 16 BtorNode *btor_rewrite_slice_exp (Btor *btor, 17 BtorNode *exp, 21 BtorNode *btor_rewrite_binary_exp (Btor *btor, 23 BtorNode *e0, 24 BtorNode *e1); 26 BtorNode *btor_rewrite_ternary_exp ( 27 Btor *btor, BtorNodeKind kind, BtorNode *e0, BtorNode *e1, BtorNode *e2); 30 BtorNode *term, 32 BtorNode **lp, 33 BtorNode **rp);
|
H A D | btorproputils.h | 37 BtorNode* add_exp, 43 BtorNode* and_exp, 49 BtorNode* eq_exp, 55 BtorNode* ult_exp, 61 BtorNode* sll_exp, 67 BtorNode* srl_exp, 73 BtorNode* mul_exp, 79 BtorNode* div_exp, 85 BtorNode* urem_exp, 91 BtorNode* conc_exp, [all …]
|
H A D | btordbg.c | 27 BtorNode *cur, *data, *key; in btor_dbg_check_lambdas_static_rho_proxy_free() 55 BtorNode *cur; in btor_dbg_check_unique_table_children_proxy_free() 75 BtorNode *cur; in btor_dbg_check_hash_table_proxy_free() 113 BtorNode *cur; in btor_dbg_check_unique_table_rebuild() 144 BtorNode *cur; in btor_dbg_check_constraints_not_const() 181 BtorNode *cur; in btor_dbg_check_nodes_simp_free() 243 BtorNode *cur; in btor_dbg_check_constraints_simp_free() 302 btor_dbg_precond_eq_exp (Btor *btor, const BtorNode *e0, const BtorNode *e1) in btor_dbg_precond_eq_exp() 304 BtorNode *real_e0, *real_e1; in btor_dbg_precond_eq_exp() 327 btor_dbg_precond_concat_exp (Btor *btor, const BtorNode *e0, const BtorNode *e1) in btor_dbg_precond_concat_exp() [all …]
|
H A D | btormodel.h | 23 BtorNode* exp); 51 const BtorBitVector* btor_model_get_bv (Btor* btor, BtorNode* exp); 55 BtorNode* exp); 57 const BtorPtrHashTable* btor_model_get_fun (Btor* btor, BtorNode* exp); 61 BtorNode* exp); 67 BtorNode* exp, 71 BtorNode* exp);
|
H A D | btorsynth.h | 18 BtorNode* btor_synthesize_term (Btor* btor, 19 BtorNode* params[], 25 BtorNode* constraints[], 27 BtorNode* consts[], 31 BtorNode* prev_synth);
|
/dports/math/boolector/boolector-3.2.2/src/utils/ |
H A D | btornodeiter.h | 25 BtorNode *cur; 36 BtorNode *btor_iter_apply_parent_next (BtorNodeIterator *it); 40 BtorNode *btor_iter_parent_next (BtorNodeIterator *it); 42 void btor_iter_lambda_init (BtorNodeIterator *it, BtorNode *exp); 44 BtorNode *btor_iter_lambda_next (BtorNodeIterator *it); 48 BtorNode *btor_iter_binder_next (BtorNodeIterator *it); 53 BtorNode * btor_iter_param_next (BtorNodeIterator * it); 57 BtorNode * btor_iter_unique_table_next (BtorNodeIterator * it); 65 BtorNode *cur; 66 const BtorNode *exp; [all …]
|
H A D | btornodeiter.c | 32 BtorNode * 35 BtorNode *result; in btor_iter_apply_parent_next() 62 BtorNode * 67 BtorNode *result; in btor_iter_parent_next() 97 BtorNode * 103 BtorNode *result; in btor_iter_args_next() 142 BtorNode * 148 BtorNode *result; in btor_iter_binder_next() 169 BtorNode * 192 BtorNode * [all …]
|
H A D | btorunionfind.h | 26 void btor_ufind_add (BtorUnionFind *ufind, BtorNode *x); 29 void btor_ufind_merge (BtorUnionFind *ufind, BtorNode *x, BtorNode *y); 32 BtorNode *btor_ufind_get_repr (BtorUnionFind *ufind, BtorNode *x); 35 bool btor_ufind_is_equal (BtorUnionFind *ufind, BtorNode *x, BtorNode *y);
|
H A D | btornodemap.c | 36 BtorNode *src; in btor_nodemap_delete() 37 BtorNode *dst; in btor_nodemap_delete() 42 dst = (BtorNode *) it.bucket->data.as_ptr; in btor_nodemap_delete() 51 BtorNode * 52 btor_nodemap_mapped (BtorNodeMap *map, const BtorNode *node) in btor_nodemap_mapped() 55 BtorNode *real_node; in btor_nodemap_mapped() 56 BtorNode *res; in btor_nodemap_mapped() 68 btor_nodemap_map (BtorNodeMap *map, BtorNode *src, BtorNode *dst) in btor_nodemap_map() 122 BtorNode *
|
H A D | btorunionfind.c | 24 BtorNode *node; 30 get_node (BtorUnionFind *ufind, BtorNode *n) in get_node() 41 new_node (BtorUnionFind *ufind, BtorNode *n) in new_node() 119 btor_ufind_add (BtorUnionFind *ufind, BtorNode *x) in btor_ufind_add() 128 btor_ufind_merge (BtorUnionFind *ufind, BtorNode *x, BtorNode *y) in btor_ufind_merge() 156 BtorNode * 157 btor_ufind_get_repr (BtorUnionFind *ufind, BtorNode *x) in btor_ufind_get_repr() 172 btor_ufind_is_equal (BtorUnionFind *ufind, BtorNode *x, BtorNode *y) in btor_ufind_is_equal()
|
/dports/math/boolector/boolector-3.2.2/src/dumper/ |
H A D | btordumpbtor.h | 21 void btor_dumpbtor_add_input_to_dump_context (BtorDumpContext *, BtorNode *); 22 void btor_dumpbtor_add_state_to_dump_context (BtorDumpContext *, BtorNode *); 24 BtorNode *, 25 BtorNode *); 27 BtorNode *, 28 BtorNode *); 29 void btor_dumpbtor_add_bad_to_dump_context (BtorDumpContext *, BtorNode *); 32 BtorNode *); 33 void btor_dumpbtor_add_root_to_dump_context (BtorDumpContext *, BtorNode *); 36 void btor_dumpbtor_dump_node (Btor *, FILE *, BtorNode *); [all …]
|
/dports/math/boolector/boolector-3.2.2/src/preprocess/ |
H A D | btorextract.c | 24 extract_base_addr_offset (BtorNode *bvadd, BtorNode **base, BtorNode **offset) in extract_base_addr_offset() 49 x = *((BtorNode **) a); in cmp_abs_rel_indices() 50 y = *((BtorNode **) b); in cmp_abs_rel_indices() 101 static inline BtorNode * 349 is_array_ite_exp (BtorNode *exp, BtorNode **array_if, BtorNode **array_else) in is_array_ite_exp() 390 is_itoi_pattern (BtorNode *index, BtorNode *value) in is_itoi_pattern() 396 is_itoip1_pattern (BtorNode *index, BtorNode *value) in is_itoip1_pattern() 399 BtorNode *inc; in is_itoip1_pattern() 408 is_cpy_pattern (BtorNode *index, BtorNode *value) in is_cpy_pattern() 457 is_abs_set_pattern (BtorNode *index, BtorNode *prev_index) in is_abs_set_pattern() [all …]
|
H A D | btornormadd.c | 34 BtorNode *n, in add_leaf_coeff() 35 BtorNode *coeff) in add_leaf_coeff() 58 BtorNode *old_coeff = b->data.as_ptr; in add_leaf_coeff() 80 static BtorNode * 81 mul_get_coeff (BtorNode *n, BtorNode **res) in mul_get_coeff() 177 BtorNode *cur, *coeff, *leaf; in prep_leafs() 383 static BtorNode * 423 BtorNode *lhs_c, *rhs_c; in normalize_eq_adds() 441 BtorNode *add_lhs = in normalize_eq_adds() 443 BtorNode *add_rhs = in normalize_eq_adds() [all …]
|
H A D | btorder.c | 19 static BtorNode * 23 BtorNode *result; in mk_param_with_symbol() 55 BtorNode *term, in occurs() 67 BtorNode *cur; in occurs() 121 static BtorNode * 143 map_subst_node (BtorIntHashTable *map, BtorNode *left, BtorNode *right) in map_subst_node() 235 BtorNode *cur; in collect_quantifier_block_vars() 264 BtorNode *cur, *q; in compute_deps() 314 static BtorNode * 450 BtorNode * [all …]
|
H A D | btornormquant.h | 15 BtorNode* btor_normalize_quantifiers_node (Btor* btor, BtorNode* root); 17 BtorNode* btor_normalize_quantifiers (Btor* btor); 21 BtorNode * btor_invert_quantifiers (Btor * btor, BtorNode * root,
|
/dports/math/boolector/boolector-3.2.2/test/ |
H A D | test_lambda.cpp | 54 BtorNode *e; in assert_parameterized() 69 BtorNode *e; in assert_not_parameterized() 122 void unary_param_exp_test (BtorNode *(*func) (Btor *, BtorNode *) ) in unary_param_exp_test() argument 124 BtorNode *result; in unary_param_exp_test() 183 int32_t param_pos, BtorNode *(*func) (Btor *, BtorNode *, BtorNode *) ) in binary_param_exp_test() argument 255 BtorNode *result; in TEST_F() 284 BtorNode *result; in TEST_F() 313 BtorNode *result; in TEST_F() 340 BtorNode *result; in TEST_F() 372 BtorNode *result; in TEST_F() [all …]
|
H A D | test_unionfind.cpp | 40 BtorNode *x = btor_exp_var (d_btor, d_sort, "x"); in TEST_F() 59 BtorNode *x = btor_exp_var (d_btor, d_sort, "x"); in TEST_F() 60 BtorNode *y = btor_exp_var (d_btor, d_sort, "y"); in TEST_F() 77 BtorNode *x = btor_exp_var (d_btor, d_sort, "x"); in TEST_F() 78 BtorNode *y = btor_exp_var (d_btor, d_sort, "y"); in TEST_F() 79 BtorNode *z = btor_exp_var (d_btor, d_sort, "z"); in TEST_F() 97 BtorNode *w = btor_exp_var (d_btor, d_sort, "w"); in TEST_F() 98 BtorNode *x = btor_exp_var (d_btor, d_sort, "x"); in TEST_F() 99 BtorNode *y = btor_exp_var (d_btor, d_sort, "y"); in TEST_F() 100 BtorNode *z = btor_exp_var (d_btor, d_sort, "z"); in TEST_F() [all …]
|