Searched refs:bdd_apply (Results 1 - 9 of 9) sorted by relevance
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/cmilner/ |
H A D | milner.c | 23 tmp1 = bdd_addref(bdd_apply(x[i],y[i],bddop_biimp)); 24 tmp2 = bdd_apply(res, tmp1, bddop_and); 44 tmp1 = bdd_addref( bdd_apply(c[i], cp[i], bddop_diff) ); 45 tmp2 = bdd_addref( bdd_apply(tp[i], t[i], bddop_diff) ); 50 tmp6 = bdd_addref( bdd_apply(tmp1, tmp2, bddop_and) ); 54 tmp1 = bdd_addref( bdd_apply(tmp6, hp[i], bddop_and) ); 57 tmp2 = bdd_addref( bdd_apply(tmp1, tmp3, bddop_and) ); 61 tmp3 = bdd_addref( bdd_apply(tmp2, tmp4, bddop_and) ); 65 tmp1 = bdd_addref( bdd_apply(tmp3, tmp5, bddop_and) ); 70 tmp4 = bdd_addref( bdd_apply( [all...] |
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | bdd.h | 61 /* Should *not* be used in bdd_apply calls !!! */ 279 extern BDD bdd_apply(BDD, BDD, int); 476 friend bdd bdd_apply(const bdd &, const bdd &, int); 612 inline bdd bdd_apply(const bdd &l, const bdd &r, int op) function 613 { return bdd_apply(l.root, r.root, op); } 616 { return bdd_apply(l.root, r.root, bddop_and); } 619 { return bdd_apply(l.root, r.root, bddop_or); } 622 { return bdd_apply(l.root, r.root, bddop_xor); } 625 { return bdd_apply(l.root, r.root, bddop_imp); } 628 { return bdd_apply( [all...] |
H A D | bvec.c | 545 tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_xor) ); 546 tmp2 = bdd_addref( bdd_apply(tmp1, c, bddop_xor) ); 551 tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_or) ); 552 tmp2 = bdd_addref( bdd_apply(c, tmp1, bddop_and) ); 555 tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_and) ); 556 tmp3 = bdd_addref( bdd_apply(tmp1, tmp2, bddop_or) ); 614 tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_xor) ); 615 tmp2 = bdd_addref( bdd_apply(tmp1, c, bddop_xor) ); 620 tmp1 = bdd_addref( bdd_apply(r.bitvec[n], c, bddop_or) ); 621 tmp2 = bdd_addref( bdd_apply( [all...] |
H A D | fdd.c | 405 tmp = bdd_apply(bdd_ithvar(domain[var].ivar[n]), v, bddop_and); 407 tmp = bdd_apply(bdd_nithvar(domain[var].ivar[n]), v, bddop_and); 580 tmp = bdd_apply( bdd_nithvar(dom->ivar[n]), d, bddop_or ); 582 tmp = bdd_apply( bdd_nithvar(dom->ivar[n]), d, bddop_and ); 630 tmp1 = bdd_addref( bdd_apply(bdd_ithvar(domain[left].ivar[n]), 634 tmp2 = bdd_addref( bdd_apply(e, tmp1, bddop_and) ); 911 tmp = bdd_apply(domain[varset[n]].var, res, bddop_and); 945 tmp = bdd_apply(domain[n].var, res, bddop_and);
|
H A D | bddop.c | 342 tmp = bdd_apply(result,v,bddop_and); 369 tmp = bdd_apply(result,v,bddop_and); 463 PROTO {* BDD bdd_apply(BDD left, BDD right, int opr) *} 495 BDD bdd_apply(BDD l, BDD r, int op) function 648 return bdd_apply(l,r,bddop_and); 663 return bdd_apply(l,r,bddop_or); 678 return bdd_apply(l,r,bddop_xor); 693 return bdd_apply(l,r,bddop_imp); 708 return bdd_apply(l,r,bddop_biimp); 889 bdd R = bdd_addref( bdd_apply(R [all...] |
H A D | kernel.c | 1480 tmp = bdd_apply(res, bdd_ithvar(varset[v]), bddop_and);
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/milner/ |
H A D | milner.cxx | 22 res &= bdd_apply(x[i],y[i],bddop_biimp);
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
H A D | parser.y | 310 res->bval = new bdd( bdd_apply(*left->bval, *right->bval, opr) );
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/ |
H A D | muddy.c | 278 return mlbdd_make(bdd_apply(Bdd_val(left),Bdd_val(right),
|
Completed in 100 milliseconds