00001
00002
00003
00004 #include "bddint.h"
00005
00006
00007 static
00008 bdd
00009 bdd_apply2_step(cmu_bdd_manager bddm,
00010 bdd (*terminal_fn)(cmu_bdd_manager, bdd *, bdd *, pointer),
00011 long op,
00012 bdd f,
00013 bdd g,
00014 pointer env)
00015 {
00016 bdd_indexindex_type top_indexindex;
00017 bdd f1, f2;
00018 bdd g1, g2;
00019 bdd temp1, temp2;
00020 bdd result;
00021
00022 if ((result=(*terminal_fn)(bddm, &f, &g, env)))
00023 {
00024 BDD_SETUP(result);
00025 BDD_TEMP_INCREFS(result);
00026 return (result);
00027 }
00028 if (bdd_lookup_in_cache2(bddm, op, f, g, &result))
00029 return (result);
00030 {
00031 BDD_SETUP(f);
00032 BDD_SETUP(g);
00033 BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00034 BDD_COFACTOR(top_indexindex, f, f1, f2);
00035 BDD_COFACTOR(top_indexindex, g, g1, g2);
00036 temp1=bdd_apply2_step(bddm, terminal_fn, op, f1, g1, env);
00037 temp2=bdd_apply2_step(bddm, terminal_fn, op, f2, g2, env);
00038 result=bdd_find(bddm, top_indexindex, temp1, temp2);
00039 bdd_insert_in_cache2(bddm, op, f, g, result);
00040 return (result);
00041 }
00042 }
00043
00044
00045 bdd
00046 bdd_apply2(cmu_bdd_manager bddm, bdd (*terminal_fn)(cmu_bdd_manager, bdd *, bdd *, pointer), bdd f, bdd g, pointer env)
00047 {
00048 long op;
00049
00050 if (bdd_check_arguments(2, f, g))
00051 {
00052 FIREWALL(bddm);
00053 op=bddm->temp_op--;
00054 RETURN_BDD(bdd_apply2_step(bddm, terminal_fn, op, f, g, env));
00055 }
00056 return ((bdd)0);
00057 }
00058
00059
00060 static
00061 bdd
00062 bdd_apply1_step(cmu_bdd_manager bddm, bdd (*terminal_fn)(cmu_bdd_manager, bdd *, pointer), long op, bdd f, pointer env)
00063 {
00064 bdd temp1, temp2;
00065 bdd result;
00066
00067 if ((result=(*terminal_fn)(bddm, &f, env)))
00068 {
00069 BDD_SETUP(result);
00070 BDD_TEMP_INCREFS(result);
00071 return (result);
00072 }
00073 if (bdd_lookup_in_cache1(bddm, op, f, &result))
00074 return (result);
00075 {
00076 BDD_SETUP(f);
00077 temp1=bdd_apply1_step(bddm, terminal_fn, op, BDD_THEN(f), env);
00078 temp2=bdd_apply1_step(bddm, terminal_fn, op, BDD_ELSE(f), env);
00079 result=bdd_find(bddm, BDD_INDEXINDEX(f), temp1, temp2);
00080 bdd_insert_in_cache1(bddm, op, f, result);
00081 return (result);
00082 }
00083 }
00084
00085
00086 bdd
00087 bdd_apply1(cmu_bdd_manager bddm, bdd (*terminal_fn)(cmu_bdd_manager, bdd *, pointer), bdd f, pointer env)
00088 {
00089 long op;
00090
00091 if (bdd_check_arguments(1, f))
00092 {
00093 FIREWALL(bddm);
00094 op=bddm->temp_op--;
00095 RETURN_BDD(bdd_apply1_step(bddm, terminal_fn, op, f, env));
00096 }
00097 return ((bdd)0);
00098 }
