Searched refs:bdd_apply (Results 1 - 9 of 9) sorted by relevance

/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/cmilner/
H A Dmilner.c23 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 Dbdd.h61 /* 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 Dbvec.c545 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 Dfdd.c405 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 Dbddop.c342 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 Dkernel.c1480 tmp = bdd_apply(res, bdd_ithvar(varset[v]), bddop_and);
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/milner/
H A Dmilner.cxx22 res &= bdd_apply(x[i],y[i],bddop_biimp);
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/calculator/
H A Dparser.y310 res->bval = new bdd( bdd_apply(*left->bval, *right->bval, opr) );
/seL4-l4v-master/HOL4/examples/muddy/muddyC/
H A Dmuddy.c278 return mlbdd_make(bdd_apply(Bdd_val(left),Bdd_val(right),

Completed in 100 milliseconds