src/cmuBdd/bddqnt.c File Reference

#include "bddint.h"

Include dependency graph for bddqnt.c:

Functions
static bdd	cmu_bdd_exists_step (cmu_bdd_manager bddm, bdd f, long op, var_assoc vars)
bdd	cmu_bdd_exists_temp (cmu_bdd_manager bddm, bdd f, long op)
bdd	cmu_bdd_exists (cmu_bdd_manager bddm, bdd f)
bdd	cmu_bdd_forall (cmu_bdd_manager bddm, bdd f)

Function Documentation

bdd cmu_bdd_exists	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 64 of file bddqnt.c.

00065 {
00066   long op;
00067 
00068   if (bdd_check_arguments(1, f))
00069     {
00070       FIREWALL(bddm);
00071       if (bddm->curr_assoc_id == -1)
00072         op=bddm->temp_op--;
00073       else
00074         op=OP_QNT+bddm->curr_assoc_id;
00075       RETURN_BDD(cmu_bdd_exists_step(bddm, f, op, bddm->curr_assoc));
00076     }
00077   return ((bdd)0);
00078 }

static bdd cmu_bdd_exists_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		long	op,
		var_assoc	vars
	)			`[static]`

Definition at line 9 of file bddqnt.c.

00010 {
00011   bdd temp1, temp2;
00012   bdd result;
00013   int quantifying;
00014 
00015   BDD_SETUP(f);
00016   if ((long)BDD_INDEX(bddm, f) > vars->last)
00017     {
00018       BDD_TEMP_INCREFS(f);
00019       return (f);
00020     }
00021   if (bdd_lookup_in_cache1(bddm, op, f, &result))
00022     return (result);
00023   quantifying=(vars->assoc[BDD_INDEXINDEX(f)] != 0);
00024   temp1=cmu_bdd_exists_step(bddm, BDD_THEN(f), op, vars);
00025   if (quantifying && temp1 == BDD_ONE(bddm))
00026     result=temp1;
00027   else
00028     {
00029       temp2=cmu_bdd_exists_step(bddm, BDD_ELSE(f), op, vars);
00030       if (quantifying)
00031         {
00032           BDD_SETUP(temp1);
00033           BDD_SETUP(temp2);
00034           bddm->op_cache.cache_level++;
00035           result=cmu_bdd_ite_step(bddm, temp1, BDD_ONE(bddm), temp2);
00036           BDD_TEMP_DECREFS(temp1);
00037           BDD_TEMP_DECREFS(temp2);
00038           bddm->op_cache.cache_level--;
00039         }
00040       else
00041         result=bdd_find(bddm, BDD_INDEXINDEX(f), temp1, temp2);
00042     }
00043   bdd_insert_in_cache1(bddm, op, f, result);
00044   return (result);
00045 }

bdd cmu_bdd_exists_temp	(	cmu_bdd_manager	bddm,
		bdd	f,
		long	op
	)

Definition at line 51 of file bddqnt.c.

00052 {
00053   if (bddm->curr_assoc_id != -1)
00054     op=OP_QNT+bddm->curr_assoc_id;
00055   return (cmu_bdd_exists_step(bddm, f, op, bddm->curr_assoc));
00056 }

bdd cmu_bdd_forall	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 86 of file bddqnt.c.

00087 {
00088   bdd temp;
00089 
00090   if ((temp=cmu_bdd_exists(bddm, BDD_NOT(f))))
00091     return (BDD_NOT(temp));
00092   return ((bdd)0);
00093 }

src/cmuBdd/bddqnt.c File Reference

Functions

Function Documentation