source: vis_dev/glu-2.3/src/cmuBdd/bddcmp.c @ 20

Last change on this file since 20 was 13, checked in by cecile, 13 years ago

library glu 2.3

File size: 1.9 KB
Line 
1/* BDD comparison routine */
2
3
4#include "bddint.h"
5
6
7static
8int
9bdd_fraction_compare(cmu_bdd_manager bddm, bdd f, bdd g)
10{
11  double f_frac, g_frac;
12
13  bddm->op_cache.cache_level++;
14  f_frac=cmu_bdd_satisfying_fraction_step(bddm, f);
15  g_frac=cmu_bdd_satisfying_fraction_step(bddm, g);
16  bddm->op_cache.cache_level--;
17  if (f_frac < g_frac)
18    return (-1);
19  if (f_frac > g_frac)
20    return (1);
21  return (0);
22}
23
24
25static
26int
27cmu_bdd_compare_step(cmu_bdd_manager bddm, bdd f, bdd g, bdd_indexindex_type v_indexindex, long op)
28{
29  bdd f1, f2;
30  bdd g1, g2;
31  bdd_indexindex_type top_indexindex;
32  INT_PTR result;
33
34  BDD_SETUP(f);
35  BDD_SETUP(g);
36  if (f == g)
37    return (0);
38  if (BDD_IS_CONST(f) || BDD_IS_CONST(g))
39    {
40      if (f == BDD_ZERO(bddm) || g == BDD_ONE(bddm))
41        return (-1);
42      return (1);
43    }
44  if (bdd_lookup_in_cache2d(bddm, op, f, g, &result))
45    return ((int)result);
46  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
47  if (bddm->indexes[top_indexindex] > bddm->indexes[v_indexindex])
48    result=bdd_fraction_compare(bddm, f, g);
49  else
50    {
51      BDD_COFACTOR(top_indexindex, f, f1, f2);
52      BDD_COFACTOR(top_indexindex, g, g1, g2);
53      if (!(result=cmu_bdd_compare_step(bddm, f2, g2, v_indexindex, op)))
54        result=cmu_bdd_compare_step(bddm, f1, g1, v_indexindex, op);
55    }
56  bdd_insert_in_cache2d(bddm, op, f, g, result);
57  return ((int)result);
58}
59
60
61int
62cmu_bdd_compare_temp(cmu_bdd_manager bddm, bdd f, bdd g, bdd v)
63{
64  BDD_SETUP(v);
65  return (cmu_bdd_compare_step(bddm, f, g, BDD_INDEXINDEX(v), OP_CMPTO+BDD_INDEXINDEX(v)));
66}
67
68
69int
70cmu_bdd_compare(cmu_bdd_manager bddm, bdd f, bdd g, bdd v)
71{
72  if (bdd_check_arguments(3, f, g, v))
73    {
74      BDD_SETUP(v);
75      if (cmu_bdd_type_aux(bddm, v) != BDD_TYPE_POSVAR)
76        {
77          cmu_bdd_warning("cmu_bdd_compare: third argument is not a positive variable");
78          return (0);
79        }
80      return (cmu_bdd_compare_step(bddm, f, g, BDD_INDEXINDEX(v), OP_CMPTO+BDD_INDEXINDEX(v)));
81    }
82  return (0);
83}
Note: See TracBrowser for help on using the repository browser.