| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | btoraig.h | 26 struct BtorAIG struct
38 typedef struct BtorAIG BtorAIG; typedef
129 static inline BtorAIG *
147 static inline BtorAIG *
176 BtorAIG *btor_aig_not (BtorAIGMgr *amgr, BtorAIG *aig);
179 BtorAIG *btor_aig_and (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right);
182 BtorAIG *btor_aig_or (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right);
185 BtorAIG *btor_aig_eq (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right);
194 BtorAIG *btor_aig_copy (BtorAIGMgr *amgr, BtorAIG *aig);
224 int32_t btor_aig_compare (const BtorAIG *aig0, const BtorAIG *aig1);
[all …]
|
| H A D | btoraig.c | 79 static BtorAIG *
80 new_and_aig (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right) in new_and_aig()
86 BtorAIG *aig; in new_and_aig()
286 BtorAIG *
350 BtorAIG *
364 BtorAIG *
375 BtorAIGMgr *amgr, BtorAIG *aig, BtorAIG *a0, BtorAIG *a1, uint32_t *calls) in find_and_contradiction_aig()
426 BtorAIG *
742 BtorAIG *
750 BtorAIG *
[all …]
|
| H A D | btoraigvec.c | 150 static BtorAIG *
221 static BtorAIG *
222 half_adder (BtorAIGMgr *amgr, BtorAIG *x, BtorAIG *y, BtorAIG **cout) in half_adder()
236 static BtorAIG *
238 BtorAIGMgr *amgr, BtorAIG *x, BtorAIG *y, BtorAIG *cin, BtorAIG **cout) in full_adder()
276 BtorAIG *cout, *cin; in btor_aigvec_add()
606 BtorAIGMgr *amgr, BtorAIG **CO, BtorAIG *R, BtorAIG *D, BtorAIG *CI) in SC_GATE_CO_aigvec()
621 BtorAIG *R, in SC_GATE_S_aigvec()
622 BtorAIG *D, in SC_GATE_S_aigvec()
628 BtorAIG *T1, *T2; in SC_GATE_S_aigvec()
[all …]
|
| H A D | aigprop.c | 126 BtorAIG *cur, *real_cur, *left, *right; in compute_score_aig()
507 BtorAIG *cur, *left, *right; in update_cone()
516 BtorAIG *root; in update_cone()
595 sizeof (BtorAIG *), in update_cone()
712 static BtorAIG *
719 BtorAIG *res, *cur; in select_root()
791 BtorAIG *root, in select_move()
792 BtorAIG **input, in select_move()
803 BtorAIG *cur, *real_cur, *c[2]; in select_move()
889 BtorAIG *root, *input; in move()
[all …]
|
| H A D | aigprop.h | 63 int32_t btor_aigprop_get_assignment_aig (BtorAIGProp *aprop, BtorAIG *aig);
|
| H A D | btoraigvec.h | 25 BtorAIG *aigs[]; /* vector of AIGs (MSB is at index 0) */
|
| H A D | btorslvaigprop.c | 65 get_assignment_aig (BtorAIGProp *aprop, BtorAIG *aig) in get_assignment_aig()
201 BtorAIG *aig; in sat_aigprop_solver()
|
| H A D | btorcore.c | 73 ((BtorAIG *) (((uint32_t long int) (exp) &1ul) ^ ((uint32_t long int) (aig))))
82 static BtorAIG *exp_to_aig (Btor *, BtorNode *);
1082 BtorAIG *aig; in btor_process_unsynthesized_constraints()
1784 BtorAIG *aig; in exp_to_cnf_lit()
1885 BtorAIG *aig; in btor_failed_exp()
2779 BtorAIG *aig; in btor_add_again_assumptions()
3144 static BtorAIG *
3149 BtorAIG *result; in exp_to_aig()
|
| H A D | btorclone.c | 1019 + 2 * sizeof (BtorAIG *) in clone_aux_btor()
1033 + (amgr->cur_num_aigs + amgr->cur_num_aig_vars) * sizeof (BtorAIG) in clone_aux_btor()
1038 + BTOR_SIZE_STACK (amgr->id2aig) * sizeof (BtorAIG *) in clone_aux_btor()
1109 allocated += sizeof (*(cur->av)) + cur->av->width * sizeof (BtorAIG *); in clone_aux_btor()
|
| H A D | btorchkclone.c | 367 chkclone_aig (BtorAIG *aig, BtorAIG *clone) in chkclone_aig()
370 BtorAIG *real_aig, *real_clone; in chkclone_aig()
|
| /dports/math/boolector/boolector-3.2.2/test/ |
| H A D | test_aig.cpp | 23 BtorAIG *aig1 = btor_aig_var (amgr); in binary_commutative_aig_test()
24 BtorAIG *aig2 = btor_aig_var (amgr); in binary_commutative_aig_test()
66 BtorAIG *var = btor_aig_var (amgr); in TEST_F()
77 BtorAIG *var = btor_aig_var (amgr); in TEST_F()
107 BtorAIG *aig1 = btor_aig_var (amgr); in TEST_F()
108 BtorAIG *aig2 = btor_aig_var (amgr); in TEST_F()
109 BtorAIG *aig3 = btor_aig_var (amgr); in TEST_F()
126 BtorAIG *var1 = btor_aig_var (amgr); in TEST_F()
127 BtorAIG *var2 = btor_aig_var (amgr); in TEST_F()
128 BtorAIG *var3 = btor_aig_var (amgr); in TEST_F()
[all …]
|
| H A D | test_aigvec.cpp | 48 ASSERT_EQ (memcmp (av1->aigs, av2->aigs, sizeof (BtorAIG *) * av1->width), 0); in TEST_F()
58 ASSERT_GT (memcmp (av1->aigs, av2->aigs, sizeof (BtorAIG *) * av1->width), 0); in TEST_F()
68 ASSERT_GT (memcmp (av1->aigs, av2->aigs, sizeof (BtorAIG *) * av1->width), 0); in TEST_F()
|
| /dports/math/boolector/boolector-3.2.2/src/utils/ |
| H A D | btoraigmap.h | 34 BtorAIG *btor_aigmap_mapped (BtorAIGMap *, BtorAIG *);
35 void btor_aigmap_map (BtorAIGMap *, BtorAIG *src, BtorAIG *dst);
|
| H A D | btoraigmap.c | 32 BtorAIG *
33 btor_aigmap_mapped (BtorAIGMap *map, BtorAIG *aig) in btor_aigmap_mapped()
39 BtorAIG *real_aig, *res; in btor_aigmap_mapped()
51 btor_aigmap_map (BtorAIGMap *map, BtorAIG *src, BtorAIG *dst) in btor_aigmap_map()
|
| /dports/math/boolector/boolector-3.2.2/src/dumper/ |
| H A D | btordumpaig.h | 21 BtorAIG* aig);
28 BtorAIG** aigs,
30 BtorAIG** regs,
31 BtorAIG** nexts,
|
| H A D | btordumpaig.c | 17 aiger_encode_aig (BtorPtrHashTable *table, BtorAIG *aig) in aiger_encode_aig()
20 BtorAIG *real_aig; in aiger_encode_aig()
43 BtorAIG *aig) in btor_dumpaig_dump_aig()
62 BtorAIG *tmp, *merged; in dumpaig_dump_aux()
199 BtorAIG **aigs, in btor_dumpaig_dump_seq()
201 BtorAIG **regs, in btor_dumpaig_dump_seq()
202 BtorAIG **nexts, in btor_dumpaig_dump_seq()
207 BtorAIG *aig, *left, *right; in btor_dumpaig_dump_seq()
|
| /dports/math/boolector/boolector-3.2.2/src/preprocess/ |
| H A D | btorskel.c | 24 BtorAIG *aig; in fixed_exp()
|