Home
last modified time | relevance | path

Searched refs:BtorNode (Results 1 – 25 of 88) sorted by relevance

1234

/dports/math/boolector/boolector-3.2.2/src/
H A Dbtorexp.h53 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 Dbtornode.h743 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 Dbtorrewrite.c372 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 Dbtorexp.c19 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 Dbtordbg.h43 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 Dbtorbeta.h17 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 Dbtornode.c296 BtorNode *
1042 BtorNode *
1053 BtorNode *
1110 BtorNode *
1121 BtorNode *
1133 BtorNode *
1292 BtorNode *
1387 BtorNode *
1446 BtorNode *
1453 BtorNode *
[all …]
H A Dbtorcore.h56 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 Dbtorrewrite.h16 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 Dbtorproputils.h37 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 Dbtordbg.c27 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 Dbtormodel.h23 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 Dbtorsynth.h18 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 Dbtornodeiter.h25 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 Dbtornodeiter.c32 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 Dbtorunionfind.h26 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 Dbtornodemap.c36 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 Dbtorunionfind.c24 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 Dbtordumpbtor.h21 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 Dbtorextract.c24 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 Dbtornormadd.c34 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 Dbtorder.c19 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 Dbtornormquant.h15 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 Dtest_lambda.cpp54 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 Dtest_unionfind.cpp40 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 …]

1234