/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/aig/ |
H A D | module.make | 1 SRC += src/aig/aig/aigCheck.c \ 2 src/aig/aig/aigCanon.c \ 3 src/aig/aig/aigCuts.c \ 4 src/aig/aig/aigDfs.c \ 5 src/aig/aig/aigDup.c \ 6 src/aig/aig/aigFanout.c \ 7 src/aig/aig/aigFrames.c \ 8 src/aig/aig/aigInter.c \ 9 src/aig/aig/aigJust.c \ 10 src/aig/aig/aigMan.c \ [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
H A D | module.make | 1 SRC += src/aig/gia/giaAig.c \ 2 src/aig/gia/giaAgi.c \ 3 src/aig/gia/giaAiger.c \ 5 src/aig/gia/giaBalAig.c \ 6 src/aig/gia/giaBalLut.c \ 8 src/aig/gia/giaBidec.c \ 9 src/aig/gia/giaCCof.c \ 10 src/aig/gia/giaCex.c \ 11 src/aig/gia/giaClp.c \ 12 src/aig/gia/giaCof.c \ [all …]
|
/dports/math/boolector/boolector-3.2.2/src/ |
H A D | btoraig.h | 78 #define BTOR_INVERT_AIG(aig) ((BtorAIG *) ((uintptr_t) 1 ^ (uintptr_t) (aig))) argument 80 #define BTOR_IS_INVERTED_AIG(aig) ((uintptr_t) 1 & (uintptr_t) (aig)) argument 85 #define BTOR_IS_REGULAR_AIG(aig) (!((uintptr_t) 1 & (uintptr_t) (aig))) argument 92 return aig == BTOR_AIG_TRUE || aig == BTOR_AIG_FALSE; in btor_aig_is_const() 111 return aig->is_var; in btor_aig_is_var() 118 return !aig->is_var; in btor_aig_is_and() 124 assert (aig); in btor_aig_get_id() 126 return BTOR_IS_INVERTED_AIG (aig) ? -BTOR_REAL_ADDR_AIG (aig)->id : aig->id; in btor_aig_get_id() 143 return BTOR_IS_INVERTED_AIG (aig) ? -BTOR_REAL_ADDR_AIG (aig)->cnf_id in btor_aig_get_cnf_id() 151 assert (aig); in btor_aig_get_left_child() [all …]
|
H A D | btoraig.c | 71 aig->refs = 1; in setup_aig_and_add_to_id_table() 76 assert (BTOR_PEEK_STACK (amgr->id2aig, aig->id) == aig); in setup_aig_and_add_to_id_table() 86 BtorAIG *aig; in new_and_aig() local 98 return aig; in new_and_aig() 107 assert (amgr->cnfid2aig.start[aig->cnf_id] == aig->id); in release_cnf_id_aig_mgr() 120 if (aig->cnf_id) release_cnf_id_aig_mgr (amgr, aig); in delete_aig_node() 198 return aig; in inc_aig_ref_counter_and_return() 291 if (btor_aig_is_const (aig)) return aig; in btor_aig_copy() 361 return aig; in btor_aig_var() 410 if (btor_aig_is_const (aig)) return aig; in simp_aig_by_sat() [all …]
|
H A D | aigprop.c | 59 if (btor_aig_is_true (aig)) return 1; in btor_aigprop_get_assignment_aig() 121 assert (!btor_aig_is_const (aig)); in compute_score_aig() 134 curid = btor_aig_get_id (aig); in compute_score_aig() 144 BTOR_PUSH_STACK (stack, aig); in compute_score_aig() 347 assert (aig); in recursively_compute_assignment() 361 BTOR_PUSH_STACK (stack, aig); in recursively_compute_assignment() 453 assert (aig); in update_unsatroots_table() 463 id = btor_aig_get_id (aig); in update_unsatroots_table() 495 assert (aig); in update_cone() 497 assert (btor_aig_is_var (aig)); in update_cone() [all …]
|
H A D | btorslvaigprop.c | 65 get_assignment_aig (BtorAIGProp *aprop, BtorAIG *aig) in get_assignment_aig() argument 70 if (aig == BTOR_AIG_TRUE) return 1; in get_assignment_aig() 71 if (aig == BTOR_AIG_FALSE) return -1; in get_assignment_aig() 74 return BTOR_IS_INVERTED_AIG (aig) ? 1 : -1; in get_assignment_aig() 75 return btor_aigprop_get_assignment_aig (aprop, aig); in get_assignment_aig() 201 BtorAIG *aig; in sat_aigprop_solver() local 258 aig = btor_node_real_addr (root)->av->aigs[0]; in sat_aigprop_solver() 259 if (btor_node_is_inverted (root)) aig = BTOR_INVERT_AIG (aig); in sat_aigprop_solver() 260 if (aig == BTOR_AIG_FALSE) goto UNSAT; in sat_aigprop_solver() 261 if (aig == BTOR_AIG_TRUE) continue; in sat_aigprop_solver() [all …]
|
/dports/math/boolector/boolector-3.2.2/src/dumper/ |
H A D | btordumpaig.c | 235 if (!btor_aig_is_const (aig)) BTOR_PUSH_STACK (stack, aig); in btor_dumpaig_dump_seq() 240 if (!btor_aig_is_const (aig)) BTOR_PUSH_STACK (stack, aig); in btor_dumpaig_dump_seq() 252 aig = BTOR_REAL_ADDR_AIG (aig); in btor_dumpaig_dump_seq() 273 aig = btor_aig_get_left_child (amgr, aig); in btor_dumpaig_dump_seq() 299 if (!btor_aig_is_const (aig)) BTOR_PUSH_STACK (stack, aig); in btor_dumpaig_dump_seq() 304 if (!btor_aig_is_const (aig)) BTOR_PUSH_STACK (stack, aig); in btor_dumpaig_dump_seq() 311 if (aig) in btor_dumpaig_dump_seq() 316 aig = BTOR_REAL_ADDR_AIG (aig); in btor_dumpaig_dump_seq() 330 aig = btor_aig_get_left_child (amgr, aig); in btor_dumpaig_dump_seq() 342 assert (BTOR_REAL_ADDR_AIG (aig) == aig); in btor_dumpaig_dump_seq() [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/saig/ |
H A D | module.make | 1 SRC += src/aig/saig/saigCone.c \ 2 src/aig/saig/saigConstr.c \ 3 src/aig/saig/saigConstr2.c \ 4 src/aig/saig/saigDual.c \ 5 src/aig/saig/saigDup.c \ 6 src/aig/saig/saigInd.c \ 7 src/aig/saig/saigIoa.c \ 8 src/aig/saig/saigIso.c \ 11 src/aig/saig/saigMiter.c \ 17 src/aig/saig/saigScl.c \ [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/ivy/ |
H A D | module.make | 2 src/aig/ivy/ivyCanon.c \ 3 src/aig/ivy/ivyCheck.c \ 4 src/aig/ivy/ivyCut.c \ 6 src/aig/ivy/ivyDfs.c \ 7 src/aig/ivy/ivyDsd.c \ 11 src/aig/ivy/ivyHaig.c \ 12 src/aig/ivy/ivyMan.c \ 13 src/aig/ivy/ivyMem.c \ 15 src/aig/ivy/ivyObj.c \ 18 src/aig/ivy/ivyRwr.c \ [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/hop/ |
H A D | module.make | 1 SRC += src/aig/hop/hopBalance.c \ 2 src/aig/hop/hopCheck.c \ 3 src/aig/hop/hopDfs.c \ 4 src/aig/hop/hopMan.c \ 5 src/aig/hop/hopMem.c \ 6 src/aig/hop/hopObj.c \ 7 src/aig/hop/hopOper.c \ 8 src/aig/hop/hopTable.c \ 9 src/aig/hop/hopTruth.c \ 10 src/aig/hop/hopUtil.c
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/aig/ |
H A D | aig.cpp | 26 struct aig; 30 aig * m_ref; 47 struct aig { struct 52 aig() {} in aig() argument 85 bool operator()(aig * n1, aig * n2) const { in operator ()() 146 void delete_node(aig * n) { in delete_node() 163 aig * allocate_node() { in allocate_node() 164 return static_cast<aig*>(m_allocator.allocate(sizeof(aig))); in allocate_node() 167 aig * mk_var(expr * t) { in mk_var() 213 aig * n1 = l.ptr(); in mk_node() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/aig/ |
H A D | aig.cpp | 26 struct aig; 30 aig * m_ref; 47 struct aig { struct 52 aig() {} in aig() function 85 bool operator()(aig * n1, aig * n2) const { in operator ()() 146 void delete_node(aig * n) { in delete_node() 163 aig * allocate_node() { in allocate_node() 164 return static_cast<aig*>(m_allocator.allocate(sizeof(aig))); in allocate_node() 167 aig * mk_var(expr * t) { in mk_var() 213 aig * n1 = l.ptr(); in mk_node() [all …]
|
/dports/cad/yosys/yosys-yosys-0.12/tests/aiger/ |
H A D | run-test.sh | 39 for aig in *.aig; do 40 echo "Checking $aig." 41 $abcprog -q "read -c $aig; write ${aig%.*}_ref.v" 46 read_aiger -clk_name clock $aig 53 " -l ${aig}.log
|
/dports/math/boolector/boolector-3.2.2/examples/generators/addcom/ |
H A D | generate.sh | 20 aig=addcom$n.aig 23 $boolector -rwl 2 --no-sort-exp --no-sort-aig --no-sort-aigvec -dai -o $aig $smt 24 $aigtocnf $aig $cnf
|
/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 3343 strat2_s = aig.as_automaton(True) 3365 aig = spot.mealy_machine_to_aig(strat, "isop") variable 3378 aig.circ_init() 3382 if (aig.circ_state()[4], aig.circ_state()[6]) != e_latch: 3384 (aig.circ_state()[4], aig.circ_state()[6])) 3385 aig.circ_step([i])
|
/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 3343 strat2_s = aig.as_automaton(True) 3365 aig = spot.mealy_machine_to_aig(strat, "isop") variable 3378 aig.circ_init() 3382 if (aig.circ_state()[4], aig.circ_state()[6]) != e_latch: 3384 (aig.circ_state()[4], aig.circ_state()[6])) 3385 aig.circ_step([i])
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/ |
H A D | abclib.dsp | 4470 SOURCE=.\src\aig\aig\aig.h 4482 SOURCE=.\src\aig\aig\aigCuts.c 4486 SOURCE=.\src\aig\aig\aigDfs.c 4490 SOURCE=.\src\aig\aig\aigDoms.c 4494 SOURCE=.\src\aig\aig\aigDup.c 4518 SOURCE=.\src\aig\aig\aigMan.c 4522 SOURCE=.\src\aig\aig\aigMem.c 4530 SOURCE=.\src\aig\aig\aigObj.c 4562 SOURCE=.\src\aig\aig\aigRet.c 4570 SOURCE=.\src\aig\aig\aigScl.c [all …]
|
/dports/math/stp/stp-2.3.3/include/stp/Util/ |
H A D | BBAsProp.h | 46 stp::ToSATAIG aig; variable 56 aig.release_cnf_memory(cnf); in ~BBAsProp() 60 : aig(mgr, stp::GlobalSTP->arrayTransformer) in BBAsProp() 81 cnf = aig.bitblast(eq, false); in BBAsProp() 84 node_to_satvar_map = aig.SATVar_to_SymbolIndexMap(); in BBAsProp() 101 aig.add_cnf_to_solver(ss, cnf); in BBAsProp() 111 aig.add_cnf_to_solver(ss, cnf); in fixed_count_unit_prop_with_assumps()
|
/dports/multimedia/obs-studio/obs-studio-27.1.3/plugins/obs-transitions/data/locale/ |
H A D | gd-GB.ini | 26 …eLayoutVertical="An t-aon fhaidhle, stacaichte (an sgaradair aig a’ bhàrr, masg an traca aig a’ bh… 37 LumaWipe.Type.BarndoorBottomLeft="Doras sabhail taobh clì aig a’ bhonn" 39 LumaWipe.Type.BarndoorTopLeft="Doras sabhail taobh clì aig a’ bhàrr" 42 LumaWipe.Type.BoxBottomLeft="Bogsa taobh clì aig a’ bhonn" 43 LumaWipe.Type.BoxBottomRight="Bogsa taobh deas aig a’ bhonn" 44 LumaWipe.Type.BoxTopLeft="Bogsa taobh clì aig a’ bhàrr" 45 LumaWipe.Type.BoxTopRight="Bogsa taobh deas aig a’ bhàrr" 56 LumaWipe.Type.LinearTopLeft="Loidhneach taobh clì aig a’ bhàrr" 57 LumaWipe.Type.LinearTopRight="Loidhneach taobh deas aig a’ bhàrr"
|
/dports/math/boolector/boolector-3.2.2/examples/generators/mulass/ |
H A D | generate.sh | 20 aig=mulass$n.aig 23 $boolector -rwl 2 -dai -o $aig $smt 24 $aigtocnf $aig $cnf
|
/dports/math/boolector/boolector-3.2.2/examples/generators/addass/ |
H A D | generate.sh | 20 aig=addass$n.aig 23 $boolector -rwl 2 -dai -o $aig $smt 24 $aigtocnf $aig $cnf
|
/dports/math/boolector/boolector-3.2.2/examples/generators/hwb/ |
H A D | generate.sh | 21 aig=hwb$n.aig 24 $boolector -rwl 2 --no-sort-exp --no-sort-aigvec -dai -o $aig $smt 25 $aigtocnf $aig $cnf
|
/dports/math/boolector/boolector-3.2.2/examples/generators/mulcom/ |
H A D | generate.sh | 20 aig=mulcom$n.aig 23 $boolector -rwl 2 --no-sort-exp --no-sort-aigvec -dai -o $aig $smt 24 $aigtocnf $aig $cnf
|
/dports/multimedia/obs-studio/obs-studio-27.1.3/plugins/mac-syphon/data/locale/ |
H A D | gd-GB.ini | 7 Crop.origin.x="Beàrr aig an taobh chlì" 8 Crop.origin.y="Beàrr aig a’ bhàrr" 9 Crop.size.width="Beàrr aig an taobh deas" 10 Crop.size.height="Beàrr aig a’ bhonn"
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/ioa/ |
H A D | module.make | 1 SRC += src/aig/ioa/ioaReadAig.c \ 2 src/aig/ioa/ioaWriteAig.c \ 3 src/aig/ioa/ioaUtil.c
|