source: vis_dev/glu-2.3/src/cmuBdd/bddqnt.c @ 33

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

library glu 2.3

File size: 2.1 KB
Line 
1/* BDD quantification routines */
2
3
4#include "bddint.h"
5
6
7static
8bdd
9cmu_bdd_exists_step(cmu_bdd_manager bddm, bdd f, long op, var_assoc vars)
10{
11  bdd temp1, temp2;
12  bdd result;
13  int quantifying;
14
15  BDD_SETUP(f);
16  if ((long)BDD_INDEX(bddm, f) > vars->last)
17    {
18      BDD_TEMP_INCREFS(f);
19      return (f);
20    }
21  if (bdd_lookup_in_cache1(bddm, op, f, &result))
22    return (result);
23  quantifying=(vars->assoc[BDD_INDEXINDEX(f)] != 0);
24  temp1=cmu_bdd_exists_step(bddm, BDD_THEN(f), op, vars);
25  if (quantifying && temp1 == BDD_ONE(bddm))
26    result=temp1;
27  else
28    {
29      temp2=cmu_bdd_exists_step(bddm, BDD_ELSE(f), op, vars);
30      if (quantifying)
31        {
32          BDD_SETUP(temp1);
33          BDD_SETUP(temp2);
34          bddm->op_cache.cache_level++;
35          result=cmu_bdd_ite_step(bddm, temp1, BDD_ONE(bddm), temp2);
36          BDD_TEMP_DECREFS(temp1);
37          BDD_TEMP_DECREFS(temp2);
38          bddm->op_cache.cache_level--;
39        }
40      else
41        result=bdd_find(bddm, BDD_INDEXINDEX(f), temp1, temp2);
42    }
43  bdd_insert_in_cache1(bddm, op, f, result);
44  return (result);
45}
46
47
48/* cmu_bdd_exists_temp is used internally by cmu_bdd_rel_prod. */
49
50bdd
51cmu_bdd_exists_temp(cmu_bdd_manager bddm, bdd f, long op)
52{
53  if (bddm->curr_assoc_id != -1)
54    op=OP_QNT+bddm->curr_assoc_id;
55  return (cmu_bdd_exists_step(bddm, f, op, bddm->curr_assoc));
56}
57
58
59/* cmu_bdd_exists(bddm, f) returns the BDD for existentially quantifying */
60/* out in f all variables which are associated with something in the */
61/* current variable association. */
62
63bdd
64cmu_bdd_exists(cmu_bdd_manager bddm, bdd f)
65{
66  long op;
67
68  if (bdd_check_arguments(1, f))
69    {
70      FIREWALL(bddm);
71      if (bddm->curr_assoc_id == -1)
72        op=bddm->temp_op--;
73      else
74        op=OP_QNT+bddm->curr_assoc_id;
75      RETURN_BDD(cmu_bdd_exists_step(bddm, f, op, bddm->curr_assoc));
76    }
77  return ((bdd)0);
78}
79
80
81/* cmu_bdd_forall(bddm, f) returns the BDD for universally quantifying */
82/* out in f all variables which are associated with something in the */
83/* current variable association. */
84
85bdd
86cmu_bdd_forall(cmu_bdd_manager bddm, bdd f)
87{
88  bdd temp;
89
90  if ((temp=cmu_bdd_exists(bddm, BDD_NOT(f))))
91    return (BDD_NOT(temp));
92  return ((bdd)0);
93}
Note: See TracBrowser for help on using the repository browser.