| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | btoraig.h | 80 #define BTOR_IS_INVERTED_AIG(aig) ((uintptr_t) 1 & (uintptr_t) (aig)) argument
82 #define BTOR_REAL_ADDR_AIG(aig) \ argument
90 btor_aig_is_const (const BtorAIG *aig) in btor_aig_is_const()
96 btor_aig_is_false (const BtorAIG *aig) in btor_aig_is_false()
102 btor_aig_is_true (const BtorAIG *aig) in btor_aig_is_true()
108 btor_aig_is_var (const BtorAIG *aig) in btor_aig_is_var()
115 btor_aig_is_and (const BtorAIG *aig) in btor_aig_is_and()
122 btor_aig_get_id (const BtorAIG *aig) in btor_aig_get_id()
139 btor_aig_get_cnf_id (const BtorAIG *aig) in btor_aig_get_cnf_id()
148 btor_aig_get_left_child (BtorAIGMgr *amgr, const BtorAIG *aig) in btor_aig_get_left_child()
[all …]
|
| H A D | btoraig.c | 86 BtorAIG *aig; in new_and_aig() local
115 delete_aig_node (BtorAIGMgr *amgr, BtorAIG *aig) in delete_aig_node()
184 inc_aig_ref_counter (BtorAIG *aig) in inc_aig_ref_counter()
195 inc_aig_ref_counter_and_return (BtorAIG *aig) in inc_aig_ref_counter_and_return()
287 btor_aig_copy (BtorAIGMgr *amgr, BtorAIG *aig) in btor_aig_copy()
353 BtorAIG *aig; in btor_aig_var() local
365 btor_aig_not (BtorAIGMgr *amgr, BtorAIG *aig) in btor_aig_not()
803 clone_aig (BtorMemMgr *mm, BtorAIG *aig) in clone_aig()
831 BtorAIG *aig; in clone_aigs() local
1352 BtorAIG *aig, *left; in btor_aig_add_toplevel_to_sat() local
[all …]
|
| H A D | aigprop.c | 52 btor_aigprop_get_assignment_aig (BtorAIGProp *aprop, BtorAIG *aig) in btor_aigprop_get_assignment_aig()
118 compute_score_aig (BtorAIGProp *aprop, BtorAIG *aig) in compute_score_aig()
343 recursively_compute_assignment (BtorAIGProp *aprop, BtorAIG *aig) in recursively_compute_assignment()
450 update_unsatroots_table (BtorAIGProp *aprop, BtorAIG *aig, int32_t assignment) in update_unsatroots_table()
492 update_cone (BtorAIGProp *aprop, BtorAIG *aig, int32_t assignment) in update_cone()
|
| H A D | btorslvaigprop.c | 65 get_assignment_aig (BtorAIGProp *aprop, BtorAIG *aig) in get_assignment_aig()
201 BtorAIG *aig; in sat_aigprop_solver() local
|
| H A D | btorcore.c | 72 #define BTOR_COND_INVERT_AIG_NODE(exp, aig) \ argument
1082 BtorAIG *aig; in btor_process_unsynthesized_constraints() local
1784 BtorAIG *aig; in exp_to_cnf_lit() local
1885 BtorAIG *aig; in btor_failed_exp() local
2779 BtorAIG *aig; in btor_add_again_assumptions() local
|
| H A D | btorchkclone.c | 367 chkclone_aig (BtorAIG *aig, BtorAIG *clone) in chkclone_aig()
|
| /dports/math/spot/spot-2.10.2/tests/python/ |
| H A D | aiger.py | 3342 aig = spot.mealy_machine_to_aig(strat, m+ss+ddx+uud) variable
3365 aig = spot.mealy_machine_to_aig(strat, "isop") variable
|
| /dports/math/py-spot/spot-2.10.2/tests/python/ |
| H A D | aiger.py | 3342 aig = spot.mealy_machine_to_aig(strat, m+ss+ddx+uud) variable
3365 aig = spot.mealy_machine_to_aig(strat, "isop") variable
|
| /dports/math/boolector/boolector-3.2.2/src/dumper/ |
| H A D | btordumpaig.c | 17 aiger_encode_aig (BtorPtrHashTable *table, BtorAIG *aig) in aiger_encode_aig()
43 BtorAIG *aig) in btor_dumpaig_dump_aig()
207 BtorAIG *aig, *left, *right; in btor_dumpaig_dump_seq() local
|
| /dports/math/boolector/boolector-3.2.2/src/utils/ |
| H A D | btoraigmap.c | 33 btor_aigmap_mapped (BtorAIGMap *map, BtorAIG *aig) in btor_aigmap_mapped()
|
| /dports/math/stp/stp-2.3.3/include/stp/Util/ |
| H A D | BBAsProp.h | 46 stp::ToSATAIG aig; variable
|
| /dports/cad/yosys/yosys-yosys-0.12/backends/protobuf/ |
| H A D | protobuf.cc | 132 Aig aig(c); in serialize_module() local
172 for (auto &aig : aig_models_) { in serialize_models() local
|
| /dports/cad/yosys/yosys-yosys-0.12/backends/json/ |
| H A D | json.cc | 185 Aig aig(c); in write_module() local
290 for (auto &aig : aig_models) { in write_design() local
|
| /dports/cad/yosys/yosys-yosys-0.12/passes/techmap/ |
| H A D | aigmap.cc | 78 Aig aig(cell); in execute() local
|
| /dports/math/boolector/boolector-3.2.2/src/preprocess/ |
| H A D | btorskel.c | 24 BtorAIG *aig; in fixed_exp() local
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/aig/ |
| H A D | aig.cpp | 47 struct aig { struct
50 aig_lit m_children[2]; argument
52 aig() {} in aig() function
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/aig/ |
| H A D | aig.cpp | 47 struct aig { struct
50 aig_lit m_children[2]; argument
52 aig() {} in aig() argument
|
| /dports/math/spot/spot-2.10.2/spot/twaalgos/ |
| H A D | aiger.hh | 58 class SPOT_API aig class
|
| /dports/math/py-spot/spot-2.10.2/spot/twaalgos/ |
| H A D | aiger.hh | 58 class SPOT_API aig class
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/rel/ |
| H A D | aig_exporter.cpp | 156 aig_ref aig = m_aigm.mk_aig(tr); in operator ()() local
|
| H A D | rel_context.cpp | 161 aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts); in saturate() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/ |
| H A D | aig_bitblaster.cpp | 296 void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) { in cacheAig()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
| H A D | ba_internalize.cpp | 56 auto* aig = s().get_cut_simplifier(); in internalize_xor() local
|
| /dports/cad/yosys/yosys-yosys-0.12/kernel/ |
| H A D | cellaigs.cc | 64 Aig *aig; member
|
| /dports/cad/yosys/yosys-yosys-0.12/backends/aiger/ |
| H A D | xaiger.cc | 447 int aig; in XAigerWriter() local
|