source: vis_dev/vis-2.3/src/ctlp/ctlpUtil.c @ 31

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

vis2.3
File size: 146.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ctlpUtil.c]
4
5  PackageName [ctlp]
6
7  Synopsis    [Routines for manipulating CTL formulas.]
8
9  Description [This file contains routines for accessing the fields of the CTL
10  formula data structure, for printing CTL formulas, for reading CTL formulas
11  from a file, and for converting formulas to the existential form.]
12
13  Remarks [There are two types of conversion routines.  One set, for
14  mc and amc, converts a formula to existential normal form, i.e. the
15  AX, AU and AG operators are converted.  The other set, used in imc,
16  converts to simple existential form, a form consisting only of
17  E-operators and the boolean operators AND and NOT.
18
19  Simple existential form is incompatible with the mc debug routines,
20  because these depend on the specific form of the converted formula
21  to decide what the original formula was.
22
23  In the long run, the existential form should probably go, and the
24  debug routines should be adapted.  The only drawback of simple
25  existential form is that the XOR gets expanded into three nontrivial
26  operations, so maybe XOR (or IFF) should be retained. (RB.)]
27
28
29  Author      [Gary York, Ramin Hojati, Tom Shiple, Adnan Aziz, Yuji Kukimoto,
30               Jae-Young Jang, In-Ho Moon]
31
32  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
33  All rights reserved.
34
35  Permission is hereby granted, without written agreement and without license
36  or royalty fees, to use, copy, modify, and distribute this software and its
37  documentation for any purpose, provided that the above copyright notice and
38  the following two paragraphs appear in all copies of this software.
39
40  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
41  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
42  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
43  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
44
45  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
46  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
47  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
48  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
49  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
50
51******************************************************************************/
52
53#include "ctlpInt.h"
54#include "errno.h"
55
56static char rcsid[] UNUSED = "$Id: ctlpUtil.c,v 1.71 2009/04/11 18:25:53 fabio Exp $";
57
58
59/*---------------------------------------------------------------------------*/
60/* Variable declarations                                                     */
61/*---------------------------------------------------------------------------*/
62
63/**Variable********************************************************************
64
65  Synopsis    [Array of CTL formulas (Ctlp_Formula_t) read from a file.]
66
67  SeeAlso     [Ctlp_FormulaArrayFree]
68
69******************************************************************************/
70static array_t *globalFormulaArray;
71static int      changeBracket = 1;
72
73/* see ctlpInt.h for documentation */
74int CtlpGlobalError;
75Ctlp_Formula_t *CtlpGlobalFormula;
76st_table *CtlpMacroTable;
77
78/*---------------------------------------------------------------------------*/
79/* Macro declarations                                                        */
80/*---------------------------------------------------------------------------*/
81
82
83/**AutomaticStart*************************************************************/
84
85/*---------------------------------------------------------------------------*/
86/* Static function prototypes                                                */
87/*---------------------------------------------------------------------------*/
88
89static Ctlp_Formula_t * FormulaCreateWithType(Ctlp_FormulaType type);
90static int FormulaCompare(const char *key1, const char *key2);
91static int FormulaHash(char *key, int modulus);
92static Ctlp_Formula_t * FormulaHashIntoUniqueTable(Ctlp_Formula_t *formula, st_table *uniqueTable);
93static Ctlp_Formula_t * FormulaConvertToExistentialDAG(Ctlp_Formula_t *formula);
94static void FormulaConvertToForward(Ctlp_Formula_t *formula, int compareValue);
95static void FormulaInsertForwardCompareNodes(Ctlp_Formula_t *formula, Ctlp_Formula_t *parent, int compareValue);
96static int FormulaGetCompareValue(Ctlp_Formula_t *formula);
97static int FormulaIsConvertible(Ctlp_Formula_t *formula);
98static Ctlp_Formula_t * ReplaceSimpleFormula(Ctlp_Formula_t *formula);
99
100/**AutomaticEnd***************************************************************/
101
102
103/*---------------------------------------------------------------------------*/
104/* Definition of exported functions                                          */
105/*---------------------------------------------------------------------------*/
106
107/**Function********************************************************************
108
109  Synopsis    [Parses a file containing a set of CTL formulas.]
110
111  Description [Parses a file containing a set of semicolon-ending CTL
112  formulas, and returns an array of Ctlp_Formula_t representing those
113  formulas.  If an error is detected while parsing the file, the routine frees
114  any allocated memory and returns NULL.]
115
116  SideEffects [Manipulates the global variables globalFormulaArray,
117  CtlpGlobalError and CtlpGlobalFormula.]
118
119  SeeAlso     [Ctlp_FormulaArrayFree Ctlp_FormulaPrint]
120
121******************************************************************************/
122array_t *
123Ctlp_FileParseFormulaArray(
124  FILE * fp)
125{
126  st_generator *stGen;
127  char *name;
128  Ctlp_Formula_t *formula;
129  char *flagValue;
130  /*
131   * Initialize the global variables.
132   */
133  globalFormulaArray = array_alloc(Ctlp_Formula_t *, 0);
134  CtlpGlobalError = 0;
135  CtlpGlobalFormula = NIL(Ctlp_Formula_t);
136  CtlpMacroTable = st_init_table(strcmp,st_strhash);
137  CtlpFileSetup(fp);
138  /*
139   * Check if changing "[] -> <>" is disabled.
140   */
141  flagValue = Cmd_FlagReadByName("ctl_change_bracket");
142  if (flagValue != NIL(char)) {
143    if (strcmp(flagValue, "yes") == 0)
144      changeBracket = 1;
145    else if (strcmp(flagValue, "no") == 0)
146      changeBracket = 0;
147    else {
148      fprintf(vis_stderr,
149        "** ctl error : invalid value %s for ctl_change_bracket[yes/no]. ***\n",
150        flagValue);
151    }
152  }
153
154  (void)CtlpYyparse();
155  st_foreach_item(CtlpMacroTable,stGen,&name,&formula){
156     FREE(name);
157     CtlpFormulaFree(formula);
158  }
159  st_free_table(CtlpMacroTable);
160
161  /*
162   * Clean up if there was an error, otherwise return the array.
163   */
164  if (CtlpGlobalError){
165    Ctlp_FormulaArrayFree(globalFormulaArray);
166    return NIL(array_t);
167  }
168  else {
169    return globalFormulaArray;
170  }
171}
172
173/**Function********************************************************************
174
175  Synopsis    [Returns formula as a character string.]
176
177  Description [Returns formula as a character string. All subformulas are
178  delimited by parenthesis. The syntax used is the same as used by the CTL
179  parser.  Does nothing if passed a NULL formula.]
180
181  SideEffects []
182
183******************************************************************************/
184char *
185Ctlp_FormulaConvertToString(
186  Ctlp_Formula_t * formula)
187{
188  char *s1        = NIL(char);
189  char *s2        = NIL(char);
190  char *tmpString = NIL(char);
191  char *result;
192
193
194  if (formula == NIL(Ctlp_Formula_t)) {
195    return NIL(char);
196  }
197
198  /* The formula is a leaf. */
199  if (formula->type == Ctlp_ID_c){
200    return util_strcat3((char *)(formula->left), "=",(char *)(formula->right));
201  }
202
203  /* If the formula is a non-leaf, the function is called recursively */
204  s1 = Ctlp_FormulaConvertToString(formula->left);
205  s2 = Ctlp_FormulaConvertToString(formula->right);
206
207  switch(formula->type) {
208    /*
209     * The cases are listed in rough order of their expected frequency.
210     */
211    case Ctlp_OR_c:
212      tmpString = util_strcat3(s1, " + ",s2);
213      result    = util_strcat3("(", tmpString, ")");
214      break;
215    case Ctlp_AND_c:
216      tmpString = util_strcat3(s1, " * ", s2);
217      result    = util_strcat3("(", tmpString, ")");
218      break;
219    case Ctlp_THEN_c:
220      tmpString = util_strcat3(s1, " -> ", s2);
221      result    = util_strcat3("(", tmpString, ")");
222      break;
223    case Ctlp_XOR_c:
224      tmpString = util_strcat3(s1, " ^ ", s2);
225      result    = util_strcat3("(", tmpString, ")");
226      break;
227    case Ctlp_EQ_c:
228      tmpString = util_strcat3(s1, " <-> ", s2);
229      result    = util_strcat3("(", tmpString, ")");
230      break;
231    case Ctlp_NOT_c:
232      tmpString = util_strcat3("(", s1, ")");
233      result    = util_strcat3("!", tmpString, "");
234      break;
235    case Ctlp_EX_c:
236      result = util_strcat3("EX(", s1, ")");
237      FREE(s1);
238      break;
239    case Ctlp_EG_c:
240      result = util_strcat3("EG(", s1, ")");
241      break;
242    case Ctlp_EF_c:
243      result = util_strcat3("EF(", s1, ")");
244      break;
245    case Ctlp_EU_c:
246      tmpString = util_strcat3("E(", s1, " U ");
247      result    = util_strcat3(tmpString, s2, ")");
248      break;
249    case Ctlp_AX_c:
250      result = util_strcat3("AX(", s1, ")");
251      break;
252    case Ctlp_AG_c:
253      result = util_strcat3("AG(", s1, ")");
254      break;
255    case Ctlp_AF_c:
256      result = util_strcat3("AF(", s1, ")");
257      break;
258    case Ctlp_AU_c:
259      tmpString = util_strcat3("A(", s1, " U ");
260      result    = util_strcat3(tmpString, s2, ")");
261      break;
262    case Ctlp_TRUE_c:
263      result = util_strsav("TRUE");
264      break;
265    case Ctlp_FALSE_c:
266      result = util_strsav("FALSE");
267      break;
268    case Ctlp_Init_c:
269      result = util_strsav("Init");
270      break;
271    case Ctlp_Cmp_c:
272      if (formula->compareValue == 0)
273        tmpString = util_strcat3("[", s1, "] = ");
274      else
275        tmpString = util_strcat3("[", s1, "] != ");
276      result    = util_strcat3(tmpString, s2, "");
277      break;
278    case Ctlp_FwdU_c:
279      tmpString = util_strcat3("FwdU(", s1, ",");
280      result    = util_strcat3(tmpString, s2, ")");
281      break;
282    case Ctlp_FwdG_c:
283      tmpString = util_strcat3("FwdG(", s1, ",");
284      result    = util_strcat3(tmpString, s2, ")");
285      break;
286    case Ctlp_EY_c:
287      result = util_strcat3("EY(", s1, ")");
288      break;
289    default:
290      fail("Unexpected type");
291  }
292
293  if (s1 != NIL(char)) {
294    FREE(s1);
295  }
296
297  if (s2 != NIL(char)) {
298    FREE(s2);
299  }
300
301  if (tmpString != NIL(char)) {
302    FREE(tmpString);
303  }
304
305  return result;
306}
307
308
309/**Function********************************************************************
310
311  Synopsis    [Prints a formula to a file.]
312
313  Description [Prints a formula to a file. All subformulas are delimited by
314  parenthesis. The syntax used is the same as used by the CTL parser.  Does
315  nothing if passed a NULL formula.]
316
317  SideEffects []
318
319******************************************************************************/
320void
321Ctlp_FormulaPrint(
322  FILE * fp,
323  Ctlp_Formula_t * formula)
324{
325  char *tmpString;
326  if (formula == NIL(Ctlp_Formula_t)) {
327    return;
328  }
329  tmpString = Ctlp_FormulaConvertToString(formula);
330  (void) fprintf(fp, "%s", tmpString);
331  FREE(tmpString);
332}
333
334
335/**Function********************************************************************
336
337  Synopsis    [Gets the type of a formula.]
338
339  Description [Gets the type of a formula. See ctlp.h for all the types. It is
340  an error to call this function on a NULL formula.]
341
342  SideEffects []
343
344  SeeAlso     []
345
346******************************************************************************/
347Ctlp_FormulaType
348Ctlp_FormulaReadType(
349  Ctlp_Formula_t * formula)
350{
351  assert( formula != NIL(Ctlp_Formula_t) );
352  return (formula->type);
353}
354
355#if 0
356boolean
357Ctlp_FormulaReadEvenNegations(
358  Ctlp_Formula_t * formula)
359{
360  assert(formula != NIL(Ctlp_Formula_t));
361  return (formula->even_negations);
362}
363#endif
364
365
366/**Function********************************************************************
367
368  Synopsis    [Gets the compare value of a formula.]
369
370  Description [Gets the compare value of a formula.  It is an error to call
371  this function on a NULL formula.]
372
373  SideEffects []
374
375  SeeAlso     []
376
377******************************************************************************/
378int
379Ctlp_FormulaReadCompareValue(
380  Ctlp_Formula_t * formula)
381{
382  int value;
383
384  assert( formula != NIL(Ctlp_Formula_t));
385  value = formula->compareValue;
386  return (value);
387}
388
389
390/**Function********************************************************************
391
392  Synopsis    [Reads the variable name of a leaf formula.]
393
394  Description [Reads the variable name of a leaf formula.
395  It is an error to call this function on a non-leaf formula.]
396
397  SideEffects []
398
399******************************************************************************/
400char *
401Ctlp_FormulaReadVariableName(
402  Ctlp_Formula_t * formula)
403{
404  if (formula->type != Ctlp_ID_c){
405    fail("Ctlp_FormulaReadVariableName() was called on a non-leaf formula.");
406  }
407  return ((char *)(formula->left));
408}
409
410
411/**Function********************************************************************
412
413  Synopsis    [Reads the value name of a leaf formula.]
414
415  Description [Reads the value name of a leaf formula.
416  It is an error to call this function on a non-leaf formula.]
417
418  SideEffects []
419
420******************************************************************************/
421char *
422Ctlp_FormulaReadValueName(
423  Ctlp_Formula_t * formula)
424{
425  if (formula->type != Ctlp_ID_c){
426    fail("Ctlp_FormulaReadValueName() was called on a non-leaf formula.");
427  }
428  return ((char *)(formula->right));
429}
430
431/**Function********************************************************************
432
433  Synopsis    [Gets the left child of a formula.]
434
435  Description [Gets the left child of a formula.  User must not free this
436  formula. If a formula is a leaf formula, NIL(Ctlp_Formula_t) is returned.]
437
438  SideEffects []
439
440  SeeAlso     [Ctlp_FormulaReadRightChild]
441
442******************************************************************************/
443Ctlp_Formula_t *
444Ctlp_FormulaReadLeftChild(
445  Ctlp_Formula_t * formula)
446{
447  if (formula->type != Ctlp_ID_c){
448    return (formula->left);
449  }
450  return NIL(Ctlp_Formula_t);
451}
452
453
454/**Function********************************************************************
455
456  Synopsis    [Gets the right child of a formula.]
457
458  Description [Gets the right child of a formula.  User must not free this
459  formula. If a formula is a leaf formula, NIL(Ctlp_Formula_t) is returned.]
460
461  SideEffects []
462
463  SeeAlso     [Ctlp_FormulaReadLeftChild]
464
465******************************************************************************/
466Ctlp_Formula_t *
467Ctlp_FormulaReadRightChild(
468  Ctlp_Formula_t * formula)
469{
470  if (formula->type != Ctlp_ID_c){
471    return (formula->right);
472  }
473  return NIL(Ctlp_Formula_t);
474}
475
476
477/**Function********************************************************************
478
479  Synopsis [Gets a copy of the set of states for which this formula is
480  true.]
481
482  Description [Gets a copy of the MDD representing the set of states for which
483  this formula is true.  It is the user's responsibility to free this MDD. If
484  the set of states has not yet been computed, then a NULL mdd_t is
485  returned. It is an error to call this function on a NULL formula.]
486
487  SideEffects []
488
489  SeeAlso     [Ctlp_FormulaSetStates]
490
491******************************************************************************/
492mdd_t *
493Ctlp_FormulaObtainStates(
494  Ctlp_Formula_t * formula)
495{
496  assert(formula != NIL(Ctlp_Formula_t));
497  if (formula->states == NIL(mdd_t) ||
498      formula->latest == Ctlp_Incomparable_c) {
499    return NIL(mdd_t);
500  }
501  else {
502    return mdd_dup(formula->states);
503  }
504}
505
506
507/**Function********************************************************************
508
509  Synopsis    [Stores the set of states with the formula.]
510
511  Description [Stores the MDD with the formula (a copy is not made,
512  and hence, the caller should not later free this MDD). This MDD is
513  intended to represent the set of states for which the formula is
514  true. It is an error to call this function on a NULL formula.]
515
516  SideEffects []
517
518  SeeAlso     [Ctlp_FormulaObtainStates]
519
520******************************************************************************/
521void
522Ctlp_FormulaSetStates(
523  Ctlp_Formula_t * formula,
524  mdd_t * states)
525{
526  assert(formula != NIL(Ctlp_Formula_t));
527  /* RB: added the next two lines.  Given the Description, this was a
528     bug */
529  if(formula->states != NIL(mdd_t))
530    mdd_free(formula->states);
531  formula->states = states;
532  formula->latest = Ctlp_Exact_c;
533}
534
535
536/**Function********************************************************************
537
538  Synopsis [Gets (a copy of) the latest approximation of the satisfying set]
539
540  Description [Gets the satisfying set or an approximation of it.  The most
541  recently computed approximation is returned.  If the
542  exact set is available, it will return that, because it is never superseded.
543  If neither exact nor approximate satisfying set is available, or
544  approx is Ctlp_Incomparable_c, it fails.]
545
546  SideEffects []
547
548  SeeAlso     [Ctlp_FormulaSetApproxStates]
549
550******************************************************************************/
551mdd_t *
552Ctlp_FormulaObtainLatestApprox(
553  Ctlp_Formula_t *formula)
554{
555  if (formula->latest == Ctlp_Exact_c)
556    return mdd_dup(formula->states);
557
558  if (formula->latest == Ctlp_Overapprox_c)
559    return mdd_dup(formula->overapprox);
560
561  if (formula->latest == Ctlp_Underapprox_c)
562    return mdd_dup(formula->underapprox);
563
564  if (formula->latest == Ctlp_Incomparable_c)
565    return mdd_dup(formula->states);
566
567  assert(0);  /* we should never get here */
568  return NIL(mdd_t);
569}
570
571
572/**Function********************************************************************
573
574  Synopsis [Gets (a copy of) an approximation of the satisfying set]
575
576  Description [Gets the required approximation of the satisfying set.  If the
577  exact set is available, it will return that.  If neither is available, or
578  approx is Ctlp_Incomparable_c, it will return NULL.]
579
580  SideEffects []
581
582  SeeAlso     [Ctlp_FormulaSetApproxStates]
583
584******************************************************************************/
585mdd_t *
586Ctlp_FormulaObtainApproxStates(
587  Ctlp_Formula_t *formula,
588  Ctlp_Approx_t approx)
589{
590  if(approx == Ctlp_Incomparable_c)
591    return NIL(mdd_t);
592
593  if (formula->states != NIL(mdd_t))
594    return mdd_dup(formula->states);
595
596  if(approx == Ctlp_Exact_c)
597    return NIL(mdd_t);
598
599  if(approx == Ctlp_Overapprox_c){
600    if(formula->overapprox == NIL(mdd_t))
601      return NIL(mdd_t);
602    else
603      return mdd_dup(formula->overapprox);
604  }
605
606  if(approx == Ctlp_Underapprox_c){
607    if(formula->underapprox == NIL(mdd_t))
608      return NIL(mdd_t);
609    else
610      return mdd_dup(formula->underapprox);
611  }
612
613  assert(0);  /* we should never get here */
614  return NIL(mdd_t);
615}
616
617
618/**Function********************************************************************
619
620  Synopsis [Stores (an approximation of) the set of states with the
621  formula.]
622
623  Description [Sets the set of states or an under or overapproximation
624  thereof, depending on the approx flag.  If there is already an under
625  or overapproximation, it is overwritten.  If the exact set is given,
626  the approx fields are cleared.  Setting an incomparable
627  approximation results in no action being taken.  An approximation
628  does not replace the exact set.  A copy of the mdd is not made, so
629  the caller should not free it.]
630
631  SideEffects []
632
633  SeeAlso     [Ctlp_FormulaObtainApproxStates Ctlp_FormulaObtainLatestApprox]
634
635******************************************************************************/
636void
637Ctlp_FormulaSetApproxStates(
638  Ctlp_Formula_t * formula,
639  mdd_t * states,
640  Ctlp_Approx_t approx)
641{
642  if (formula->latest == Ctlp_Exact_c) {
643    mdd_free(states);
644    return;
645  }
646
647  formula->latest = approx;
648
649  if (approx == Ctlp_Exact_c) {
650    if (formula->states != NIL(mdd_t))
651      mdd_free(formula->states);
652    formula->states = states;
653
654    if (formula->underapprox != NIL(mdd_t)) {
655      mdd_free(formula->underapprox);
656      formula->underapprox = NIL(mdd_t);
657    }
658
659    if (formula->overapprox != NIL(mdd_t)) {
660      mdd_free(formula->overapprox);
661      formula->overapprox = NIL(mdd_t);
662    }
663
664    return;
665  }
666
667  if (approx == Ctlp_Underapprox_c) {
668    /* you could perform a union instead, but typical use will
669       have monotonically increasing underapproximations */
670    if(formula->underapprox != NIL(mdd_t))
671      mdd_free(formula->underapprox);
672    formula->underapprox = states;
673  }
674
675  if (approx == Ctlp_Overapprox_c) {
676    /* you could perform an intersection instead */
677    if (formula->overapprox != NIL(mdd_t))
678      mdd_free(formula->overapprox);
679    formula->overapprox = states;
680  }
681
682  /* This case is possible; for instance when both children of an implication
683   * with (All, S) condition are underapproximated.  We may lose some states
684   * from the left if they are not in S.  These cause an overapproximation.
685   * We may also lose some states from the right.  These cause an
686   * underapproximation.  When the two effects are combined, we get something
687   * incomparable, yet sufficient to produce the exact result, because it is
688   * accurate over S. */
689  if (approx == Ctlp_Incomparable_c) {
690    if (formula->states != NIL(mdd_t))
691      mdd_free(formula->states);
692    formula->states = states;
693  }
694
695  return;
696}
697
698
699/**Function********************************************************************
700
701  Synopsis    [Sets the debug information of a formula.]
702
703  Description [Sets the debug information of a CTL formula.  The data is
704  uninterpreted.  FreeFn is a pointer to a function that takes a formula as
705  input and returns void.  FreeFn should free all the memory associated with
706  the debug data; it is called when this formula is freed.]
707
708  SideEffects []
709
710  SeeAlso     [Ctlp_FormulaReadDebugData]
711
712******************************************************************************/
713void
714Ctlp_FormulaSetDbgInfo(
715  Ctlp_Formula_t * formula,
716  void *data,
717  Ctlp_DbgInfoFreeFn freeFn)
718{
719  if (formula->dbgInfo.data != NIL(void)){
720    assert(formula->dbgInfo.freeFn != NULL);
721
722    (*formula->dbgInfo.freeFn)(formula);
723  }
724
725  formula->dbgInfo.data   = data;
726  formula->dbgInfo.freeFn = freeFn;
727}
728
729
730/**Function********************************************************************
731
732  Synopsis    [Returns the debug data associated with a formula.]
733
734  Description [Returns the debug data associated with a formula.  These data
735  are uninterpreted by the ctlp package.]
736
737  SideEffects []
738
739  SeeAlso     [Ctlp_FormulaSetDbgInfo]
740
741******************************************************************************/
742void *
743Ctlp_FormulaReadDebugData(
744  Ctlp_Formula_t * formula)
745{
746  return formula->dbgInfo.data;
747}
748
749
750/**Function********************************************************************
751
752  Synopsis    [Returns TRUE if formula was converted, else FALSE.]
753  from AX/AG/AU/AF]
754
755  Description [Returns TRUE if formula was converted from a formula of type
756  AG, AX, AU, AF, or EF via a call to
757  Ctlp_FormulaConvertToExistentialFormTree or
758  Ctlp_FormulaConvertToExistentialFormDAG. Otherwise, returns FALSE.]
759
760  SideEffects []
761
762******************************************************************************/
763boolean
764Ctlp_FormulaTestIsConverted(
765  Ctlp_Formula_t * formula)
766{
767  return formula->dbgInfo.convertedFlag;
768}
769
770
771/**Function********************************************************************
772
773  Synopsis    [Returns TRUE if formula contains no path quantifiers.]
774
775  Description [Test if a CTL formula has any path quantifiers in it;
776  if so return false, else true.  For a CTL formula, being quantifier-free
777  and being propositional are equivalent.]
778
779  SideEffects []
780
781******************************************************************************/
782boolean
783Ctlp_FormulaTestIsQuantifierFree(
784  Ctlp_Formula_t *formula)
785{
786  boolean lCheck;
787  boolean rCheck;
788  Ctlp_Formula_t *leftChild;
789  Ctlp_Formula_t *rightChild;
790  Ctlp_FormulaType type;
791
792  if ( formula == NIL( Ctlp_Formula_t ) ) {
793    return TRUE;
794  }
795
796  type = Ctlp_FormulaReadType( formula );
797
798  if ( ( type == Ctlp_ID_c ) ||
799       ( type == Ctlp_TRUE_c ) ||
800       ( type == Ctlp_FALSE_c ) ) {
801    return TRUE;
802  }
803
804  if ( ( type !=  Ctlp_OR_c )   &&
805       ( type !=  Ctlp_AND_c )  &&
806       ( type !=  Ctlp_NOT_c )  &&
807       ( type !=  Ctlp_THEN_c ) &&
808       ( type !=  Ctlp_XOR_c )  &&
809       ( type !=  Ctlp_EQ_c ) ) {
810    return FALSE;
811  }
812
813  leftChild = Ctlp_FormulaReadLeftChild( formula );
814  lCheck = Ctlp_FormulaTestIsQuantifierFree( leftChild );
815
816  if (lCheck == FALSE)
817    return FALSE;
818
819  rightChild = Ctlp_FormulaReadRightChild( formula );
820  rCheck = Ctlp_FormulaTestIsQuantifierFree( rightChild );
821
822  return rCheck;
823}
824
825
826/**Function********************************************************************
827
828  Synopsis    [Annotates the each node in parse tree with its negation
829  parity.]
830
831  Description [This function must be called at the top level with
832  parity = Ctlp_Even_c.  It will then annotate each node with its parity.
833  A node in a formula with sharing may have both parities and a descendant
834  of a XOR or EQ node will have both.  Only backward CTL formulae are
835  considered.]
836
837  SideEffects [changes the negation_parity fields of all nodes in the formula]
838
839******************************************************************************/
840void
841Ctlp_FormulaNegations(
842  Ctlp_Formula_t * formula,
843  Ctlp_Parity_t parity)
844{
845
846  Ctlp_FormulaType formulaType;
847  Ctlp_Formula_t *leftChild;
848  Ctlp_Formula_t *rightChild;
849  Ctlp_Parity_t newparity;
850
851  assert(formula != NIL(Ctlp_Formula_t));
852  if (formula->negation_parity == parity)
853    return; /* already done */
854  if (formula->negation_parity != Ctlp_NoParity_c)
855    parity = Ctlp_EvenOdd_c; /* reconverging paths with different parity */
856  formula->negation_parity = parity;
857
858  formulaType = Ctlp_FormulaReadType(formula);
859  leftChild = Ctlp_FormulaReadLeftChild(formula);
860  rightChild = Ctlp_FormulaReadRightChild(formula);
861
862  switch (formulaType) {
863  case Ctlp_AX_c:
864  case Ctlp_AG_c:
865  case Ctlp_AF_c:
866  case Ctlp_EX_c:
867  case Ctlp_EG_c:
868  case Ctlp_EF_c:
869    Ctlp_FormulaNegations(leftChild,parity);
870    break;
871  case Ctlp_AU_c:
872  case Ctlp_EU_c:
873  case Ctlp_OR_c:
874  case Ctlp_AND_c:
875    Ctlp_FormulaNegations(leftChild,parity);
876    Ctlp_FormulaNegations(rightChild,parity);
877    break;
878  case Ctlp_NOT_c:
879    if (parity == Ctlp_Even_c)
880      newparity = Ctlp_Odd_c;
881    else if (parity == Ctlp_Odd_c)
882      newparity = Ctlp_Even_c;
883    else newparity = Ctlp_EvenOdd_c;
884    Ctlp_FormulaNegations(leftChild,newparity);
885    break;
886  case Ctlp_THEN_c:
887    if (parity == Ctlp_Even_c)
888      newparity = Ctlp_Odd_c;
889    else if (parity == Ctlp_Odd_c)
890      newparity = Ctlp_Even_c;
891    else newparity = Ctlp_EvenOdd_c;
892    Ctlp_FormulaNegations(leftChild,newparity);
893    Ctlp_FormulaNegations(rightChild,parity);
894    break;
895  case Ctlp_XOR_c:
896  case Ctlp_EQ_c:
897    Ctlp_FormulaNegations(leftChild,Ctlp_EvenOdd_c);
898    Ctlp_FormulaNegations(rightChild,Ctlp_EvenOdd_c);
899    break;
900  default:
901      break;
902  }
903}
904
905
906/**Function********************************************************************
907
908  Synopsis    [Checks whether an ACTL formula is W-ACTL.]
909
910  Description [Test if the binary operators in an ACTL formula have at
911  least one propositional formula as one of the operands.  If not return
912  Ctlp_NONWACTL_c, else return either Ctlp_WACTLsimple_c for propositional
913  formulae or Ctlp_WACTLstate_c for formulae containing temporal operators.
914  A W-ACTL formula must contain no exitential operators and no forward
915  operators.  XOR and EQ are allowed only in propositional subformulae.]
916
917  SideEffects [none]
918
919******************************************************************************/
920Ctlp_FormulaACTLSubClass
921Ctlp_CheckIfWACTL(
922  Ctlp_Formula_t *formula)
923{
924  Ctlp_FormulaType formulaType;
925  Ctlp_Formula_t *rightFormula, *leftFormula;
926  Ctlp_FormulaACTLSubClass resultLeft, resultRight;
927
928  assert(formula != NIL(Ctlp_Formula_t));
929  if(formula == NIL(Ctlp_Formula_t))
930    return Ctlp_WACTLsimple_c;
931
932  formulaType = Ctlp_FormulaReadType(formula);
933  leftFormula = Ctlp_FormulaReadLeftChild(formula);
934  rightFormula = Ctlp_FormulaReadRightChild(formula);
935
936  /* Depending on the formula type, create result or recur. */
937  switch (formulaType) {
938  case Ctlp_AX_c:
939  case Ctlp_AG_c:
940  case Ctlp_AF_c:
941    resultLeft = Ctlp_CheckIfWACTL(leftFormula);
942    if (resultLeft == Ctlp_NONWACTL_c)
943      return Ctlp_NONWACTL_c;
944    else
945      return Ctlp_WACTLstate_c;
946    break;
947  case Ctlp_AU_c:
948    resultLeft = Ctlp_CheckIfWACTL(leftFormula);
949    if (resultLeft == Ctlp_NONWACTL_c)
950      return Ctlp_NONWACTL_c;
951    resultRight = Ctlp_CheckIfWACTL(rightFormula);
952    if (resultRight == Ctlp_NONWACTL_c)
953      return Ctlp_NONWACTL_c;
954    if (resultLeft == Ctlp_WACTLsimple_c || resultRight == Ctlp_WACTLsimple_c)
955      return Ctlp_WACTLstate_c;
956    else
957      return Ctlp_NONWACTL_c;
958    break;
959  case Ctlp_OR_c:
960  case Ctlp_AND_c:
961  case Ctlp_THEN_c:
962    resultLeft = Ctlp_CheckIfWACTL(leftFormula);
963    if (resultLeft == Ctlp_NONWACTL_c) {
964      return Ctlp_NONWACTL_c;
965    } else {
966      resultRight = Ctlp_CheckIfWACTL(rightFormula);
967      if (resultRight == Ctlp_WACTLsimple_c) {
968        return resultLeft;
969      } else if (resultLeft == Ctlp_WACTLsimple_c) {
970        return resultRight;
971      } else {
972        return Ctlp_NONWACTL_c;
973      }
974    }
975    break;
976  case Ctlp_NOT_c:
977    resultLeft = Ctlp_CheckIfWACTL(leftFormula);
978    return resultLeft;
979    break;
980  case Ctlp_XOR_c:
981  case Ctlp_EQ_c:
982    resultLeft = Ctlp_CheckIfWACTL(leftFormula);
983    if (resultLeft != Ctlp_WACTLsimple_c) {
984      return Ctlp_NONWACTL_c;
985    } else {
986      resultRight = Ctlp_CheckIfWACTL(rightFormula);
987      if (resultRight == Ctlp_WACTLsimple_c)
988        return Ctlp_WACTLsimple_c;
989      else
990        return Ctlp_NONWACTL_c;
991    }
992    break;
993  case Ctlp_ID_c:
994  case Ctlp_TRUE_c:
995  case Ctlp_FALSE_c:
996    return Ctlp_WACTLsimple_c;
997    break;
998  default:
999    fprintf(vis_stderr, "#Ctlp Result : The formula should be in Universal operators!\n");
1000    return Ctlp_NONWACTL_c;
1001    break;
1002  }
1003} /* End of Ctlp_CheckTypeOfExistentialFormula */
1004
1005
1006/**Function********************************************************************
1007
1008  Synopsis    [Returns original formula corresponding to converted formula.]
1009
1010  SideEffects []
1011
1012******************************************************************************/
1013Ctlp_Formula_t *
1014Ctlp_FormulaReadOriginalFormula(
1015  Ctlp_Formula_t * formula)
1016{
1017  return formula->dbgInfo.originalFormula;
1018}
1019
1020
1021/**Function********************************************************************
1022
1023  Synopsis    [Frees a formula if no other formula refers to it as a
1024  sub-formula.]
1025
1026  Description [The function decrements the refCount of the formula. As a
1027  consequence, if the refCount becomes 0, the formula is freed.]
1028
1029  SideEffects []
1030
1031  SeeAlso     [CtlpFormulaFree, CtlpDecrementRefCount]
1032
1033******************************************************************************/
1034void
1035Ctlp_FormulaFree(
1036  Ctlp_Formula_t *formula)
1037{
1038  CtlpFormulaDecrementRefCount(formula);
1039}
1040
1041/**Function********************************************************************
1042
1043  Synopsis [Recursively frees states, underapprox and overapprox fields of
1044  Ctlp_Formula_t, and the debug data]
1045
1046  Description []
1047
1048  SideEffects []
1049
1050  SeeAlso     [Ctlp_FormulaFree]
1051
1052******************************************************************************/
1053void
1054Ctlp_FlushStates(
1055  Ctlp_Formula_t * formula)
1056{
1057  if (formula != NIL(Ctlp_Formula_t)) {
1058
1059    if (formula->type != Ctlp_ID_c){
1060      if (formula->left  != NIL(Ctlp_Formula_t)) {
1061        Ctlp_FlushStates(formula->left);
1062      }
1063      if (formula->right != NIL(Ctlp_Formula_t)) {
1064        Ctlp_FlushStates(formula->right);
1065      }
1066    }
1067
1068    if (formula->states != NIL(mdd_t)){
1069      mdd_free(formula->states);
1070      formula->states = NIL(mdd_t);
1071    }
1072    if (formula->underapprox != NIL(mdd_t)){
1073      mdd_free(formula->underapprox);
1074      formula->underapprox = NIL(mdd_t);
1075    }
1076    if (formula->overapprox != NIL(mdd_t)){
1077      mdd_free(formula->overapprox);
1078      formula->overapprox = NIL(mdd_t);
1079    }
1080
1081    if (formula->dbgInfo.data != NIL(void)){
1082      (*formula->dbgInfo.freeFn)(formula);
1083      formula->dbgInfo.data = NIL(void);
1084    }
1085
1086  }
1087
1088}
1089
1090/**Function********************************************************************
1091
1092
1093  Synopsis    [Duplicates a CTL formula.]
1094
1095  Description [Recursively duplicate a formula. Does nothing if the formula
1096  is NIL. Does not copy mdd for states, underapprox, overapprox, dbgInfo, and
1097  in general all the information that is used to annotate the formula.]
1098
1099  SideEffects []
1100
1101  SeeAlso     []
1102
1103******************************************************************************/
1104Ctlp_Formula_t *
1105Ctlp_FormulaDup(
1106  Ctlp_Formula_t * formula)
1107{
1108  Ctlp_Formula_t *result = NIL(Ctlp_Formula_t);
1109
1110  if ( formula == NIL(Ctlp_Formula_t)) {
1111        return NIL(Ctlp_Formula_t);
1112  }
1113
1114  result = ALLOC(Ctlp_Formula_t, 1);
1115
1116  result->type                    = formula->type;
1117  result->states                  = NIL(mdd_t);
1118  result->underapprox             = NIL(mdd_t);
1119  result->overapprox              = NIL(mdd_t);
1120  result->latest                  = Ctlp_Incomparable_c;
1121  result->Bottomstates            = NIL(array_t);
1122  result->Topstates               = NIL(array_t);
1123  result->negation_parity         = Ctlp_NoParity_c;
1124  result->leaves                  = formula->leaves == NIL(array_t) ?
1125    NIL(array_t) : array_dup(formula->leaves);
1126  result->matchfound_top          = NIL(array_t);
1127  result->matchelement_top        = NIL(array_t);
1128  result->matchfound_bot          = NIL(array_t);
1129  result->matchelement_bot        = NIL(array_t);
1130  result->refCount                = 1;
1131  result->dbgInfo.data            = NIL(void);
1132  result->dbgInfo.freeFn          = (Ctlp_DbgInfoFreeFn) NULL;
1133  result->dbgInfo.convertedFlag   = FALSE;
1134  result->dbgInfo.originalFormula = NIL(Ctlp_Formula_t);
1135  result->top                     = 0;
1136  result->compareValue            = 0;
1137
1138  if ( formula->type != Ctlp_ID_c )  {
1139    result->left                    = Ctlp_FormulaDup( formula->left );
1140    result->right                   = Ctlp_FormulaDup( formula->right );
1141  }
1142  else {
1143    result->left  = (Ctlp_Formula_t *) util_strsav((char *)formula->left );
1144    result->right = (Ctlp_Formula_t *) util_strsav((char *)formula->right );
1145  }
1146  result->share           = 1;
1147  result->BotOnionRings   = NIL(array_t);
1148  result->TopOnionRings   = NIL(array_t);
1149  return result;
1150}
1151
1152/**Function********************************************************************
1153
1154
1155  Synopsis    [Complements a CTL formula.]
1156
1157  Description []
1158
1159  SideEffects []
1160
1161  SeeAlso     []
1162
1163******************************************************************************/
1164Ctlp_Formula_t *
1165Ctlp_FormulaConverttoComplement(
1166  Ctlp_Formula_t * formula)
1167{
1168  Ctlp_Formula_t *result;
1169
1170  if (formula == NIL(Ctlp_Formula_t)) {
1171        return NIL(Ctlp_Formula_t);
1172  }
1173  result = Ctlp_FormulaCreate(Ctlp_NOT_c,formula,NIL(Ctlp_Formula_t));
1174  CtlpFormulaIncrementRefCount(formula);
1175#if 0
1176  result = FormulaCreateWithType(Ctlp_NOT_c);
1177  result->left = FormulaCreateWithType(formula->type);
1178  result->left->left = formula->left;
1179  result->left->right = formula->right;
1180  switch (formula->type) {
1181  case Ctlp_ID_c:
1182  case Ctlp_TRUE_c:
1183  case Ctlp_FALSE_c:
1184  case Ctlp_Init_c:
1185    break;
1186  default:
1187    CtlpFormulaIncrementRefCount(formula->left);
1188    CtlpFormulaIncrementRefCount(formula->right);
1189    break;
1190  }
1191#endif
1192  return result;
1193} /* Ctlp_FormulaConverttoComplement */
1194
1195
1196/**Function********************************************************************
1197
1198
1199  Synopsis    [Converts AFp to A (TRUE) U p.]
1200
1201  Description []
1202
1203  SideEffects [Should be called only for AF formula]
1204
1205  SeeAlso     []
1206
1207******************************************************************************/
1208Ctlp_Formula_t *
1209Ctlp_FormulaConvertAFtoAU(
1210  Ctlp_Formula_t * formula)
1211{
1212  Ctlp_Formula_t *result;
1213  /* AFf --> (A true U f)  */
1214  assert(formula->type == Ctlp_AF_c);
1215  result = FormulaCreateWithType(Ctlp_AU_c);
1216  result->left  = FormulaCreateWithType(Ctlp_TRUE_c);
1217  result->right = formula->left;
1218  CtlpFormulaIncrementRefCount(formula->left);
1219  return result;
1220}
1221
1222
1223/**Function********************************************************************
1224
1225
1226  Synopsis    [Converts EFp to p + EX(EFp).]
1227
1228  Description []
1229
1230  SideEffects [Should be called only for EF formula]
1231
1232  SeeAlso     []
1233
1234******************************************************************************/
1235Ctlp_Formula_t *
1236Ctlp_FormulaConvertEFtoOR(
1237  Ctlp_Formula_t * formula)
1238{
1239  Ctlp_Formula_t *result;
1240  /* EFf --> f + EX(EF(f))  */
1241  assert(formula->type == Ctlp_EF_c);
1242  result = FormulaCreateWithType(Ctlp_OR_c);
1243  result->left = formula->left;
1244  result->right = FormulaCreateWithType(Ctlp_EX_c);
1245  result->right->left = formula;
1246  CtlpFormulaIncrementRefCount(formula->left);
1247  CtlpFormulaIncrementRefCount(formula);
1248  return result;
1249}
1250
1251
1252/**Function********************************************************************
1253
1254
1255  Synopsis    [Converts EpUq to q + p*EX(EpUq).]
1256
1257  Description []
1258
1259  SideEffects [Should be called only for EU formula]
1260
1261  SeeAlso     []
1262
1263******************************************************************************/
1264Ctlp_Formula_t *
1265Ctlp_FormulaConvertEUtoOR(
1266  Ctlp_Formula_t * formula)
1267{
1268  Ctlp_Formula_t *result;
1269  assert(formula->type == Ctlp_EU_c);
1270  /* E(f1)U(f2) --> f2 + f1*EX( E(f1)U(f2) )  */
1271  result = FormulaCreateWithType(Ctlp_OR_c);
1272  result->left = formula->right;
1273  result->right = FormulaCreateWithType(Ctlp_AND_c);
1274  result->right->left = formula->left;
1275  result->right->right = FormulaCreateWithType(Ctlp_EX_c);
1276  result->right->right->left = formula;
1277  CtlpFormulaIncrementRefCount(formula->left);
1278  CtlpFormulaIncrementRefCount(formula->right);
1279  CtlpFormulaIncrementRefCount(formula);
1280  return result;
1281}
1282
1283
1284/**Function********************************************************************
1285
1286
1287  Synopsis    [Convert p^q to !p*q + p*!q.]
1288
1289  Description []
1290
1291  SideEffects [Should be called only for XOR formula]
1292
1293  SeeAlso     []
1294
1295******************************************************************************/
1296Ctlp_Formula_t *
1297Ctlp_FormulaConvertXORtoOR(
1298  Ctlp_Formula_t * formula)
1299{
1300  Ctlp_Formula_t *result;
1301  assert(formula->type == Ctlp_XOR_c);
1302  result = FormulaCreateWithType(Ctlp_OR_c);
1303  result->left = FormulaCreateWithType(Ctlp_AND_c);
1304  result->right = FormulaCreateWithType(Ctlp_AND_c);
1305  result->left->left = Ctlp_FormulaConverttoComplement(formula->left);
1306  result->left->right = formula->right;
1307  result->right->left = formula->left;
1308  result->right->right = Ctlp_FormulaConverttoComplement(formula->right);
1309  CtlpFormulaIncrementRefCount(formula->left);
1310  CtlpFormulaIncrementRefCount(formula->right);
1311  return result;
1312}
1313
1314
1315/**Function********************************************************************
1316
1317
1318  Synopsis    [Converts p<->q to p*q + !p*!q.]
1319
1320  Description []
1321
1322  SideEffects [Should be called only for EQ formula]
1323
1324  SeeAlso     []
1325
1326******************************************************************************/
1327Ctlp_Formula_t *
1328Ctlp_FormulaConvertEQtoOR(
1329  Ctlp_Formula_t * formula)
1330{
1331  Ctlp_Formula_t *result;
1332  assert(formula->type == Ctlp_EQ_c);
1333  result = FormulaCreateWithType(Ctlp_OR_c);
1334  result->left = FormulaCreateWithType(Ctlp_AND_c);
1335  result->right = FormulaCreateWithType(Ctlp_AND_c);
1336  result->left->left = formula->left;
1337  result->left->right = formula->right;
1338  result->right->left = Ctlp_FormulaConverttoComplement(formula->left);
1339  result->right->right = Ctlp_FormulaConverttoComplement(formula->right);
1340  CtlpFormulaIncrementRefCount(formula->left);
1341  CtlpFormulaIncrementRefCount(formula->right);
1342  return result;
1343}
1344
1345
1346/**Function********************************************************************
1347
1348  Synopsis    [Returns formula with a negation pushed down]
1349
1350  Description [Returns formula with a negation pushed down. It is assumed that
1351               the formula being passsed to it is not a proposition]
1352
1353  SideEffects []
1354
1355******************************************************************************/
1356Ctlp_Formula_t *
1357Ctlp_FormulaPushNegation(
1358  Ctlp_Formula_t * formula)
1359{
1360  Ctlp_Formula_t *result;
1361  if (formula == NIL(Ctlp_Formula_t)) {
1362    return NIL(Ctlp_Formula_t);
1363  }
1364
1365  switch(formula->type) {
1366    /*
1367     * The cases are listed in rough order of their expected frequency.
1368     */
1369  case Ctlp_OR_c: /*!(f1 v f2) = !f1 * !f2*/
1370    result = FormulaCreateWithType(Ctlp_AND_c);
1371    result->left  = Ctlp_FormulaConverttoComplement(formula->left);
1372    result->right = Ctlp_FormulaConverttoComplement(formula->right);
1373    break;
1374  case Ctlp_AND_c: /*!(f1 * f2) = !f1 v !f2*/
1375    result = FormulaCreateWithType(Ctlp_OR_c);
1376    result->left  = Ctlp_FormulaConverttoComplement(formula->left);
1377    result->right = Ctlp_FormulaConverttoComplement(formula->right);
1378    break;
1379  case Ctlp_THEN_c: /*!(f1 -> f2) = !(!f1 v f2) = f1 * !f2 */
1380    result = FormulaCreateWithType(Ctlp_AND_c);
1381    result->left  = formula->left;
1382    CtlpFormulaIncrementRefCount(formula->left);
1383    result->right = Ctlp_FormulaConverttoComplement(formula->right);
1384    break;
1385  case Ctlp_XOR_c: /*!(f1 ^ f2) = f1 <-> f2*/
1386    result = FormulaCreateWithType(Ctlp_EQ_c);
1387    result->left  = formula->left;
1388    result->right = formula->right;
1389    CtlpFormulaIncrementRefCount(formula->left);
1390    CtlpFormulaIncrementRefCount(formula->right);
1391    break;
1392  case Ctlp_EQ_c: /*!(f1 <-> f2) = f1 ^ f2*/
1393    result = FormulaCreateWithType(Ctlp_XOR_c);
1394    result->left  = formula->left;
1395    result->right = formula->right;
1396    CtlpFormulaIncrementRefCount(formula->left);
1397    CtlpFormulaIncrementRefCount(formula->right);
1398    break;
1399  case Ctlp_NOT_c:/* !(!f1) = f1*/
1400    result = formula->left;
1401    CtlpFormulaIncrementRefCount(formula->left);
1402    break;
1403  case Ctlp_EX_c:/* !(EX(f1)) = AX(!f1)*/
1404    result = FormulaCreateWithType(Ctlp_AX_c);
1405    result->left  = Ctlp_FormulaConverttoComplement(formula->left);
1406    break;
1407  case Ctlp_EG_c: /*!(EG(f1)) = AF(!f1)*/
1408    result = FormulaCreateWithType(Ctlp_AF_c);
1409    result->left  = Ctlp_FormulaConverttoComplement(formula->left);
1410    break;
1411  case Ctlp_EF_c: /*!(EF(f1)) = AG(!f1)*/
1412    result = FormulaCreateWithType(Ctlp_AG_c);
1413    result->left  = Ctlp_FormulaConverttoComplement(formula->left);
1414    break;
1415  case Ctlp_EU_c: /* !(EpUq) = A(!q)U(!(p+q) + AG(!q))*/
1416    result = FormulaCreateWithType(Ctlp_AU_c);
1417    result->left  = Ctlp_FormulaConverttoComplement(formula->right);
1418    result->right = FormulaCreateWithType(Ctlp_OR_c);
1419    result->right->left = FormulaCreateWithType(Ctlp_NOT_c);
1420    result->right->left->left = FormulaCreateWithType(Ctlp_OR_c);
1421    result->right->left->left->left = formula->left;
1422    result->right->left->left->right = formula->right;
1423    result->right->right = FormulaCreateWithType(Ctlp_AG_c);
1424    result->right->right->left = Ctlp_FormulaConverttoComplement(formula->right);
1425    CtlpFormulaIncrementRefCount(formula->left);
1426    CtlpFormulaIncrementRefCount(formula->right);
1427    break;
1428  case Ctlp_AX_c:/* !AX(f1) = EX(!f1)*/
1429    result = FormulaCreateWithType(Ctlp_EX_c);
1430    result->left  = Ctlp_FormulaConverttoComplement(formula->left);
1431    break;
1432  case Ctlp_AG_c:/* !AG(f1) = EF(!f1) */
1433    result = FormulaCreateWithType(Ctlp_EF_c);
1434    result->left  = Ctlp_FormulaConverttoComplement(formula->left);
1435    break;
1436  case Ctlp_AF_c: /* !AF(f1) = EG(!f1)*/
1437    result = FormulaCreateWithType(Ctlp_EG_c);
1438    result->left  = Ctlp_FormulaConverttoComplement(formula->left);
1439    break;
1440  case Ctlp_AU_c: /* !(ApUq) = (E(!q)U(!(p+q)))+(EG!q)*/
1441    result = FormulaCreateWithType(Ctlp_OR_c);
1442    result->left = FormulaCreateWithType(Ctlp_EU_c);
1443    result->left->left  = Ctlp_FormulaConverttoComplement(formula->right);
1444    result->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1445    result->left->right->left= FormulaCreateWithType(Ctlp_OR_c);
1446    result->left->right->left->left = formula->left;
1447    result->left->right->left->right = formula->right;
1448    result->right = FormulaCreateWithType(Ctlp_EG_c);
1449    result->right->left = Ctlp_FormulaConverttoComplement(formula->right);
1450    CtlpFormulaIncrementRefCount(formula->left);
1451    CtlpFormulaIncrementRefCount(formula->right);
1452    break;
1453  case Ctlp_TRUE_c:/* !TRUE = FALSE*/
1454    result = FormulaCreateWithType(Ctlp_FALSE_c);
1455    break;
1456  case Ctlp_FALSE_c:/*!FALSE = TRUE*/
1457    result = FormulaCreateWithType(Ctlp_TRUE_c);
1458    break;
1459  case Ctlp_Init_c: /* ???*/
1460  case Ctlp_Cmp_c: /* ???*/
1461    /* if (formula->compareValue == 0)
1462        tmpString = util_strcat3("[", s1, "] = ");
1463      else
1464        tmpString = util_strcat3("[", s1, "] != ");
1465      result    = util_strcat3(tmpString, s2, "");
1466      break;*/
1467  case Ctlp_FwdU_c: /* ???*/
1468  case Ctlp_FwdG_c:  /* ??? */
1469  case Ctlp_EY_c: /* ??? */
1470    result = formula;
1471    break;
1472  default:
1473      fail("Unexpected type");
1474  }
1475
1476  return result;
1477}
1478/*****************************************************************************/
1479
1480/**Function********************************************************************
1481
1482  Synopsis    [Frees an array of CTL formulas.]
1483
1484  Description [Calls CtlpFormulaDecrementRefCount on each formula in
1485  formulaArray, and then frees the array itself. It is okay to call this
1486  function with an empty array, but it is an error to call it with a NULL
1487  array.]
1488
1489  SideEffects []
1490
1491  SeeAlso     [Ctlp_FormulaFree]
1492
1493******************************************************************************/
1494void
1495Ctlp_FormulaArrayFree(
1496  array_t * formulaArray /* of Ctlp_Formula_t */)
1497{
1498  int i;
1499  int numFormulas = array_n(formulaArray);
1500
1501  assert(formulaArray != NIL(array_t));
1502  for (i = 0; i < numFormulas; i++) {
1503    Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
1504
1505    CtlpFormulaDecrementRefCount(formula);
1506  }
1507
1508  array_free(formulaArray);
1509}
1510
1511
1512/**Function********************************************************************
1513
1514  Synopsis    [Converts a CTL formula to existential form.]
1515
1516  Description [Converts a CTL formula to existential form.  That is, all
1517  universal path quantifiers are replaced with the appropriate combination of
1518  existential quantifiers and Boolean negation.  Also converts "finally"
1519  operators to "until" operators.<p>
1520
1521  <p>Returns a new formula that shares absolutely nothing with the original
1522  formula (not even the strings). Also, the new formula does not have any MDDs
1523  associated with it.  The "originalFormula" field of each new subformula is
1524  set to point to the formula passed as an argument.  In addition, if (and only
1525  if) the original formula is of type AG, AX, AU, AF, or EF, the "converted
1526  flag" is set. Returns NULL if called with a NULL formula.
1527
1528  <p>Note: the debugger takes advantage of the exact way that the conversion is
1529  done.  Hence, you cannot play around much with the syntax of the converted
1530  formula.
1531
1532  <p>A list of conversion rules shouls be included here (RB).
1533
1534  <br> AG phi turns into !EU(true,! phi'), where the top ! has converted set
1535  and points to the AG, and phi' points to phi.
1536
1537  <br> AU?
1538
1539  <br> AX?
1540
1541  <br> Any others?
1542  ]
1543
1544  SideEffects []
1545
1546
1547  SeeAlso [Ctlp_FormulaArrayConvertToExistentialForm,
1548  Ctlp_ConvertToSimpleExistentialForm]
1549
1550******************************************************************************/
1551Ctlp_Formula_t *
1552Ctlp_FormulaConvertToExistentialForm(
1553  Ctlp_Formula_t * formula)
1554{
1555  Ctlp_Formula_t *new_;
1556  char *variableNameCopy, *valueNameCopy;
1557
1558  if (formula == NIL(Ctlp_Formula_t)) {
1559    return NIL(Ctlp_Formula_t);
1560  }
1561
1562  /*
1563   * Recursively convert each subformula.
1564   */
1565
1566  switch(formula->type) {
1567    case Ctlp_EF_c:
1568      /* EFf --> (E true U f)  */
1569      new_ = FormulaCreateWithType(Ctlp_EU_c);
1570      new_->left  = FormulaCreateWithType(Ctlp_TRUE_c);
1571      new_->right = Ctlp_FormulaConvertToExistentialForm(formula->left);
1572      new_->dbgInfo.convertedFlag = TRUE;
1573      break;
1574
1575    case Ctlp_AX_c:
1576      /* AXf --> !(EX(!f)) */
1577      new_ = FormulaCreateWithType(Ctlp_NOT_c);
1578      new_->left = FormulaCreateWithType(Ctlp_EX_c);
1579      new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1580      new_->left->left->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
1581      new_->dbgInfo.convertedFlag = TRUE;
1582      break;
1583
1584    case Ctlp_AG_c:
1585      /* AGf --> ![(E true U !f)] */
1586      new_ = FormulaCreateWithType(Ctlp_NOT_c);
1587      new_->left = FormulaCreateWithType(Ctlp_EU_c);
1588      new_->left->left = FormulaCreateWithType(Ctlp_TRUE_c);
1589      new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1590      new_->left->right->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
1591      new_->dbgInfo.convertedFlag = TRUE;
1592      break;
1593
1594    case Ctlp_AF_c:
1595      /* AFf --> ![EG(!f)] */
1596      new_ = FormulaCreateWithType(Ctlp_NOT_c);
1597      new_->left = FormulaCreateWithType(Ctlp_EG_c);
1598      new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1599      new_->left->left->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
1600      new_->dbgInfo.convertedFlag = TRUE;
1601      break;
1602
1603    case Ctlp_AU_c:
1604      /* A[fUg] --> !((E[!g U (!f*!g)]) + (EG!g)) */
1605
1606      new_ = FormulaCreateWithType(Ctlp_NOT_c); /* top */
1607      new_->left = FormulaCreateWithType(Ctlp_OR_c); /* ((E[!g U (!f*!g)]) + (EG!g)) */
1608
1609      new_->left->right = FormulaCreateWithType(Ctlp_EG_c); /* EG !g */
1610      new_->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1611      new_->left->right->left->left = Ctlp_FormulaConvertToExistentialForm(formula->right); /* g */
1612
1613      new_->left->left = FormulaCreateWithType(Ctlp_EU_c); /* E[!g U (!f*!g)] */
1614      new_->left->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1615      new_->left->left->left->left = Ctlp_FormulaConvertToExistentialForm(formula->right); /* g */
1616      new_->left->left->right = FormulaCreateWithType(Ctlp_AND_c); /* !f*!g */
1617      new_->left->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !f */
1618      new_->left->left->right->left->left = Ctlp_FormulaConvertToExistentialForm(formula->left); /* f */
1619      new_->left->left->right->right = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1620      new_->left->left->right->right->left = Ctlp_FormulaConvertToExistentialForm(formula->right); /* g */
1621      new_->dbgInfo.convertedFlag = TRUE;
1622      break;
1623
1624    case Ctlp_ID_c:
1625      /* Make a copy of the name, and create a new formula. */
1626      variableNameCopy = util_strsav((char *)(formula->left));
1627      valueNameCopy = util_strsav((char *)(formula->right));
1628      new_ = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
1629      break;
1630
1631    case Ctlp_THEN_c:
1632    case Ctlp_EX_c:
1633    case Ctlp_EG_c:
1634    case Ctlp_EU_c:
1635    case Ctlp_OR_c:
1636    case Ctlp_AND_c:
1637    case Ctlp_NOT_c:
1638    case Ctlp_XOR_c:
1639    case Ctlp_EQ_c:
1640    case Ctlp_TRUE_c:
1641    case Ctlp_FALSE_c:
1642      /* These are already in the correct form.  Just convert subformulas. */
1643      new_ = FormulaCreateWithType(formula->type);
1644      new_->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
1645      new_->right = Ctlp_FormulaConvertToExistentialForm(formula->right);
1646      break;
1647
1648    default:
1649      fail("Unexpected type");
1650  }
1651
1652  new_->dbgInfo.originalFormula = formula;
1653  return new_;
1654}
1655
1656/**Function********************************************************************
1657
1658  Synopsis    [Converts a CTL formula to simple existential form.]
1659
1660  Description [Converts a CTL formula to simple existential form.
1661  That is, all universal path quantifiers are replaced with the
1662  appropriate combination of existential quantifiers and Boolean
1663  negation. Only `NOT' and `AND' Boolean operators are allowed.  Also
1664  converts "finally" operators to "until" operators.
1665
1666  The converted bit is set in the converted formula only when temporal
1667  operators are converted, not when boolean operators are converted.
1668
1669  A  new formula is created that needs to be freed seperately.]
1670
1671  SideEffects []
1672
1673  Remarks     [Ctl formulas in simple existential form are incompatible
1674  with the mc debug routines.  The reason is that the debug routines
1675  count on a very specific form of the converted formula to conclude
1676  what the original formula was.]
1677
1678  SeeAlso     [Ctlp_FormulaArrayConvertToExistentialForm]
1679
1680******************************************************************************/
1681Ctlp_Formula_t *
1682Ctlp_FormulaConvertToSimpleExistentialForm(
1683  Ctlp_Formula_t * formula)
1684{
1685  Ctlp_Formula_t *new_;
1686  char *variableNameCopy, *valueNameCopy;
1687
1688  if (formula == NIL(Ctlp_Formula_t)) {
1689    return NIL(Ctlp_Formula_t);
1690  }
1691
1692  /*
1693   * Recursively convert each subformula.
1694   */
1695
1696  switch(formula->type) {
1697    case Ctlp_EF_c:
1698      /* EFf --> (E true U f)  */
1699      new_ = FormulaCreateWithType(Ctlp_EU_c);
1700      new_->left  = FormulaCreateWithType(Ctlp_TRUE_c);
1701      new_->right = Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1702      new_->dbgInfo.convertedFlag = TRUE;
1703      break;
1704
1705    case Ctlp_AX_c:
1706      /* AXf --> !(EX(!f)) */
1707      new_ = FormulaCreateWithType(Ctlp_NOT_c);
1708      new_->left = FormulaCreateWithType(Ctlp_EX_c);
1709      new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1710      new_->left->left->left =
1711        Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1712      new_->dbgInfo.convertedFlag = TRUE;
1713      break;
1714
1715    case Ctlp_AG_c:
1716      /* AGf --> ![(E true U !f)] */
1717      new_ = FormulaCreateWithType(Ctlp_NOT_c);
1718      new_->left = FormulaCreateWithType(Ctlp_EU_c);
1719      new_->left->left = FormulaCreateWithType(Ctlp_TRUE_c);
1720      new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1721      new_->left->right->left =
1722        Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1723      new_->dbgInfo.convertedFlag = TRUE;
1724      break;
1725
1726    case Ctlp_AF_c:
1727      /* AFf --> ![EG(!f)] */
1728      new_ = FormulaCreateWithType(Ctlp_NOT_c);
1729      new_->left = FormulaCreateWithType(Ctlp_EG_c);
1730      new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1731      new_->left->left->left = Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1732      new_->dbgInfo.convertedFlag = TRUE;
1733      break;
1734
1735    case Ctlp_AU_c:
1736      /* A[fUg] --> !(E[!g U (!f*!g)]) * !(EG!g)) */
1737
1738      new_ = FormulaCreateWithType(Ctlp_AND_c); /* top */
1739      new_->left = FormulaCreateWithType(Ctlp_NOT_c);
1740      new_->right = FormulaCreateWithType(Ctlp_NOT_c);
1741      new_->left->left = FormulaCreateWithType(Ctlp_EG_c); /* EG !g */
1742      new_->left->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1743      new_->left->left->left->left =
1744        Ctlp_FormulaConvertToSimpleExistentialForm(formula->right); /* g */
1745
1746      new_->right->left = FormulaCreateWithType(Ctlp_EU_c); /* E[!g U (!f*!g)] */
1747      new_->right->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1748      new_->right->left->left->left =
1749        Ctlp_FormulaConvertToSimpleExistentialForm(formula->right); /* g */
1750      new_->right->left->right = FormulaCreateWithType(Ctlp_AND_c); /* !f*!g */
1751      new_->right->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !f */
1752      new_->right->left->right->left->left =
1753        Ctlp_FormulaConvertToSimpleExistentialForm(formula->left); /* f */
1754      new_->right->left->right->right = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1755      new_->right->left->right->right->left =
1756        Ctlp_FormulaConvertToSimpleExistentialForm(formula->right); /* g */
1757      new_->dbgInfo.convertedFlag = TRUE;
1758      break;
1759
1760    case Ctlp_ID_c:
1761      /* Make a copy of the name, and create a new formula. */
1762      variableNameCopy = util_strsav((char *)(formula->left));
1763      valueNameCopy = util_strsav((char *)(formula->right));
1764      new_ = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
1765      break;
1766
1767      /* RB: I think THEN (and also OR, and maybe some others) should also have converted set. */
1768    case Ctlp_THEN_c:
1769      /* p->q --> !(p * !q) */
1770      new_ = FormulaCreateWithType(Ctlp_NOT_c);
1771      new_->left = FormulaCreateWithType(Ctlp_AND_c);
1772      new_->left->left =
1773        Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1774      new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1775      new_->left->right->left =
1776        Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1777      break;
1778
1779    case Ctlp_EX_c:
1780    case Ctlp_EG_c:
1781    case Ctlp_EU_c:
1782    case Ctlp_AND_c:
1783    case Ctlp_NOT_c:
1784    case Ctlp_TRUE_c:
1785    case Ctlp_FALSE_c:
1786      /* These are already in the correct form.  Just convert subformulas. */
1787      new_ = FormulaCreateWithType(formula->type);
1788      new_->left = Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1789      new_->right = Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1790      break;
1791
1792    case Ctlp_OR_c:
1793      /* p + q --> !(!p * !q) */
1794      new_ = FormulaCreateWithType(Ctlp_NOT_c);
1795      new_->left = FormulaCreateWithType(Ctlp_AND_c);
1796      new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1797      new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1798      new_->left->left->left =
1799        Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1800      new_->left->right->left =
1801        Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1802      break;
1803    case Ctlp_XOR_c:
1804      /* p ^ q --> !(p * q) * !(!p * !q) */
1805      new_ = FormulaCreateWithType(Ctlp_AND_c);
1806      new_->left = FormulaCreateWithType(Ctlp_NOT_c);
1807      new_->left->left = FormulaCreateWithType(Ctlp_AND_c);
1808      new_->left->left->left =
1809        Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1810      new_->left->left->right =
1811        Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1812      new_->right = FormulaCreateWithType(Ctlp_NOT_c);
1813      new_->right->left = FormulaCreateWithType(Ctlp_AND_c);
1814      new_->right->left->left =  FormulaCreateWithType(Ctlp_NOT_c);
1815      new_->right->left->left->left =
1816        Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1817      new_->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1818      new_->right->left->right->left =
1819        Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1820      break;
1821
1822    case Ctlp_EQ_c:
1823      /* p <-> q --> !(p * !q) * !(!p * q) */
1824      new_ = FormulaCreateWithType(Ctlp_AND_c);
1825      new_->left = FormulaCreateWithType(Ctlp_NOT_c);
1826      new_->left->left = FormulaCreateWithType(Ctlp_AND_c);
1827      new_->left->left->left =
1828        Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1829      new_->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1830      new_->left->left->right->left =
1831        Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1832      new_->right = FormulaCreateWithType(Ctlp_NOT_c);
1833      new_->right->left = FormulaCreateWithType(Ctlp_AND_c);
1834      new_->right->left->left =  FormulaCreateWithType(Ctlp_NOT_c);
1835      new_->right->left->left->left =
1836        Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1837      new_->right->left->right =
1838        Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1839      break;
1840
1841    default:
1842      fail("Unexpected type");
1843  }
1844
1845  new_->dbgInfo.originalFormula = formula;
1846  return new_;
1847}
1848
1849/**Function********************************************************************
1850
1851  Synopsis    [Converts an array of CTL formulas to existential form.]
1852
1853  Description [Calls Ctlp_FormulaConvertToExistentialForm on each formula. It
1854  is okay to call this function with an empty array (in which case an empty
1855  array is returned), but it is an error to call it with a NULL array.
1856
1857  All formulas in the array are copied, and hence Ctlp_FormulaArrayFree() needs
1858  to be called on the result at the end.]
1859
1860  SideEffects []
1861
1862  SeeAlso [Ctlp_FormulaConvertToExistentialForm]
1863
1864******************************************************************************/
1865array_t *
1866Ctlp_FormulaArrayConvertToExistentialFormTree(
1867  array_t * formulaArray /* of Ctlp_Formula_t  */)
1868{
1869  int i;
1870  int numFormulas = array_n(formulaArray);
1871  array_t *convertedArray = array_alloc(Ctlp_Formula_t *, numFormulas);
1872
1873  assert(formulaArray != NIL(array_t));
1874
1875  for (i = 0; i < numFormulas; i++) {
1876    Ctlp_Formula_t *formula          = array_fetch(Ctlp_Formula_t *, formulaArray, i);
1877    Ctlp_Formula_t *convertedFormula = Ctlp_FormulaConvertToExistentialForm(formula);
1878
1879    array_insert(Ctlp_Formula_t *, convertedArray, i, convertedFormula);
1880  }
1881
1882  return convertedArray;
1883}
1884
1885/**Function********************************************************************
1886
1887  Synopsis    [Converts an array of CTL formulas to simple existential form.]
1888
1889  Description [Calls Ctlp_FormulaConvertToSimpleExistentialForm on
1890  each formula.  It is okay to call this function with an empty array
1891  (in which case an empty array is returned), but it is an error to
1892  call it with a NULL array.]
1893
1894  SideEffects []
1895
1896  SeeAlso     [Ctlp_FormulaConvertToExistentialForm]
1897
1898******************************************************************************/
1899array_t *
1900Ctlp_FormulaArrayConvertToSimpleExistentialFormTree(
1901  array_t * formulaArray /* of Ctlp_Formula_t  */)
1902{
1903  int i;
1904  int numFormulas;
1905  array_t *convertedArray;
1906
1907  assert( formulaArray != NIL(array_t));
1908
1909  numFormulas = array_n(formulaArray);
1910  convertedArray = array_alloc(Ctlp_Formula_t *, numFormulas);
1911
1912  for (i = 0; i < numFormulas; i++) {
1913    Ctlp_Formula_t *formula;
1914    Ctlp_Formula_t *convertedFormula;
1915
1916    formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
1917    convertedFormula = Ctlp_FormulaConvertToSimpleExistentialForm(formula);
1918
1919    array_insert(Ctlp_Formula_t *, convertedArray, i, convertedFormula);
1920  }
1921
1922  return convertedArray;
1923}
1924
1925/**Function********************************************************************
1926
1927  Synopsis    [Converts an array of CTL formulae to a multi-rooted DAG.]
1928
1929  Description [The function hashes each subformula of a formula
1930  (including the formula itself) into a uniqueTable.  It returns an
1931  array containing the roots of the multi-rooted DAG thus created by
1932  the sharing of the subformulae.  It is okay to call this function
1933  with an empty array (in which case an empty array is returned), but
1934  it is an error to call it with a NULL array.]
1935
1936  SideEffects [A formula in formulaArray might be freed if it had been
1937  encountered as a subformula of some other formula. Other formulae in
1938  formulaArray might be present in the returned array. Therefore, the
1939  formulae in formulaArray should not be freed. Only formulaArray
1940  itself should be freed.
1941
1942
1943
1944  RB:  What does that mean?
1945
1946  I understand this as follows.  Copies of the formulae are not made,
1947  but rather pointers to the argument subformulae are kept.  Hence, not only
1948  should the formulae in the result not be freed, but also you cannot free the
1949  argument before you are done with the result.  Furthermore, by invocation of
1950  this function, the argument gets altered.  It is still valid, but pointers
1951  may have changed.  Is this correct?
1952
1953
1954  RB rewrite: A formula in formulaArray is freed if it is encountered as a
1955  subformula of some other formula. Other formulae in formulaArray might be
1956  present in the returned array. Therefore, the formulae in formulaArray should
1957  not be freed. Only formulaArray itself should be freed.]
1958
1959  SeeAlso     []
1960
1961******************************************************************************/
1962array_t *
1963Ctlp_FormulaArrayConvertToDAG(
1964  array_t *formulaArray)
1965{
1966  int i;
1967  Ctlp_Formula_t *formula, *uniqueFormula;
1968  st_table *uniqueTable = st_init_table(FormulaCompare, FormulaHash);
1969  int numFormulae = array_n(formulaArray);
1970  array_t *rootsOfFormulaDAG = array_alloc(Ctlp_Formula_t *, numFormulae);
1971
1972  assert(formulaArray != NIL(array_t));
1973
1974  for(i=0; i < numFormulae; i++) {
1975    formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
1976    uniqueFormula = FormulaHashIntoUniqueTable(formula, uniqueTable);
1977    if(uniqueFormula != formula) {
1978      CtlpFormulaDecrementRefCount(formula);
1979      CtlpFormulaIncrementRefCount(uniqueFormula);
1980      array_insert(Ctlp_Formula_t *, rootsOfFormulaDAG, i, uniqueFormula);
1981    }
1982    else
1983      array_insert(Ctlp_Formula_t *, rootsOfFormulaDAG, i, formula);
1984  }
1985  st_free_table(uniqueTable);
1986  return rootsOfFormulaDAG;
1987}
1988
1989/**Function********************************************************************
1990
1991  Synopsis    [Converts a DAG of CTL formulae to a DAG of existential CTL
1992  formulae.]
1993
1994  Description [The function converts a DAG of CTL formulae to a DAG of
1995  existential CTL formulae. The function recursively converts each
1996  subformula of each of the formulae in the DAG and remembers the
1997  converted formula in the field states. It is okay to call this
1998  function with an empty array (in which case an empty array is
1999  returned), but it is an error to call it with a NULL array.
2000
2001  The states fileds in the formula need to be NULL.]
2002
2003  SideEffects []
2004
2005  SeeAlso     [FormulaConvertToExistentialDAG]
2006
2007******************************************************************************/
2008array_t *
2009Ctlp_FormulaDAGConvertToExistentialFormDAG(
2010  array_t *formulaDAG)
2011{
2012  int i;
2013  Ctlp_Formula_t *formula;
2014  int numFormulae = array_n(formulaDAG);
2015  array_t *existentialFormulaDAG = array_alloc(Ctlp_Formula_t *, numFormulae);
2016
2017  assert( formulaDAG != NIL(array_t));
2018
2019  for(i=0; i<numFormulae; i++) {
2020    formula = array_fetch(Ctlp_Formula_t *, formulaDAG, i);
2021    array_insert(Ctlp_Formula_t *, existentialFormulaDAG, i,
2022                 FormulaConvertToExistentialDAG(formula));
2023  }
2024  for(i=0; i<numFormulae; i++) {
2025    formula = array_fetch(Ctlp_Formula_t *, formulaDAG, i);
2026    CtlpFormulaSetStatesToNULL(formula);
2027  }
2028  return existentialFormulaDAG;
2029}
2030
2031
2032/**Function********************************************************************
2033
2034  Synopsis    [Creates a CTL formula with the specified fields.]
2035
2036  Description [Allocates a Ctlp_Formula_t, and sets the 2 fields given as
2037  arguments.  If the type is Ctlp_ID_c, then the left and right fields
2038  should contain a pointer to a variable name and a pointer to a value
2039  respectively. Otherwise, the two fields point to subformulas. refCount is
2040  set to 1. The states field is set to NULL, the converted flag is set to
2041  FALSE, and the originalFormula field is set to NULL.]
2042
2043  Comment     []
2044
2045  SideEffects []
2046
2047  SeeAlso     [CtlpFormulaDecrementRefCount]
2048
2049******************************************************************************/
2050Ctlp_Formula_t *
2051Ctlp_FormulaCreate(
2052  Ctlp_FormulaType  type,
2053  void * left,
2054  void * right)
2055{
2056  Ctlp_Formula_t *formula = ALLOC(Ctlp_Formula_t, 1);
2057
2058  formula->type                    = type;
2059  formula->left                    = (Ctlp_Formula_t *)left;
2060  formula->right                   = (Ctlp_Formula_t *)right;
2061  formula->refCount                = 1;
2062  formula->states                  = NIL(mdd_t);
2063  formula->underapprox             = NIL(mdd_t);
2064  formula->overapprox              = NIL(mdd_t);
2065  formula->Topstates               = NIL(array_t);
2066  formula->Bottomstates            = NIL(array_t);
2067  formula->leaves                  = NIL(array_t);
2068  formula->matchfound_top          = NIL(array_t);
2069  formula->matchelement_top        = NIL(array_t);
2070  formula->matchfound_bot          = NIL(array_t);
2071  formula->matchelement_bot        = NIL(array_t);
2072  formula->negation_parity         = Ctlp_NoParity_c;
2073  formula->share                   = 1;
2074  formula->dbgInfo.data            = NIL(void);
2075  formula->dbgInfo.freeFn          = (Ctlp_DbgInfoFreeFn) NULL;
2076  formula->dbgInfo.convertedFlag   = FALSE;
2077  formula->dbgInfo.originalFormula = NIL(Ctlp_Formula_t);
2078  formula->top                     = 0;
2079  formula->compareValue            = 0;
2080  formula->latest                  = Ctlp_Incomparable_c;
2081  formula->BotOnionRings           = NIL(array_t);
2082  formula->TopOnionRings           = NIL(array_t);
2083
2084  return formula;
2085}
2086
2087
2088/**Function********************************************************************
2089
2090  Synopsis    [Creates a CTL formula with disjunction of atomic propositions]
2091
2092  Description [This function returns Ctlp_Formula_t for name = {v1,v2,...}.
2093  In case of failure, a NULL pointer is returned.]
2094
2095  SideEffects []
2096
2097  SeeAlso     []
2098
2099******************************************************************************/
2100Ctlp_Formula_t *
2101Ctlp_FormulaCreateOr(
2102  char *name,
2103  char *valueStr)
2104{
2105  Ctlp_Formula_t *formula, *tempFormula;
2106  char *preStr;
2107
2108  preStr = strtok(valueStr,",");
2109  formula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
2110                               util_strsav(preStr));
2111  if (formula == NIL(Ctlp_Formula_t)) {
2112     return NIL(Ctlp_Formula_t);
2113  }
2114  while ((preStr = strtok(NIL(char),",")) != NIL(char)) {
2115    tempFormula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
2116                                     util_strsav(preStr));
2117    if (tempFormula == NIL(Ctlp_Formula_t)) {
2118      Ctlp_FormulaFree(formula);
2119      return NIL(Ctlp_Formula_t);
2120    }
2121    formula = Ctlp_FormulaCreate(Ctlp_OR_c,formula,tempFormula);
2122  }
2123  return formula;
2124}
2125
2126
2127/**Function********************************************************************
2128
2129  Synopsis    [Creates a CTL formula with conjunction of atomic propositions]
2130
2131  Description [This function returns Ctlp_Formula_t for nameVector = value,
2132  nameVector is a form of var[i:j] or var<j:j> and value is any integer n or
2133  binary string starting with 'b', for instance, b0011. If n is not
2134  fitted in var[i:j] or size of binary string is not matched with
2135  var[i:j], NULL pointer is returned]
2136
2137  SideEffects []
2138
2139  SeeAlso     []
2140
2141******************************************************************************/
2142Ctlp_Formula_t *
2143Ctlp_FormulaCreateVectorAnd(
2144  char *nameVector,
2145  char *value)
2146{
2147  Ctlp_Formula_t *formula, *tempFormula;
2148  int startValue, endValue, inc, i,j, interval,startInd;
2149  char *binValueStr, *varName, *name;
2150  char *bitValue;
2151
2152  varName = CtlpGetVectorInfoFromStr(nameVector,&startValue,&endValue,&interval,&inc);
2153  binValueStr = ALLOC(char,interval+1);
2154  if (!CtlpStringChangeValueStrToBinString(value,binValueStr,interval) ){
2155    FREE(varName);
2156    FREE(binValueStr);
2157    return NIL(Ctlp_Formula_t);
2158  }
2159
2160  name = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
2161  (void) sprintf(name,"%s[%d]",varName,startValue);
2162  (void) CtlpChangeBracket(name);
2163
2164  bitValue = ALLOC(char,2);
2165  bitValue[0] = binValueStr[0];
2166  bitValue[1] = '\0';
2167
2168  formula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
2169                               util_strsav(bitValue));
2170  j = 0;
2171  startInd = startValue;
2172  for(i=startValue;i!=endValue;i=i+inc){
2173    startInd += inc;
2174    j++;
2175    (void) sprintf(name,"%s[%d]",varName,startInd);
2176    (void) CtlpChangeBracket(name);
2177    bitValue[0] = binValueStr[j];
2178    tempFormula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
2179                                     util_strsav(bitValue));
2180    formula = Ctlp_FormulaCreate(Ctlp_AND_c,formula,tempFormula);
2181  }
2182  FREE(varName);
2183  FREE(name);
2184  FREE(binValueStr);
2185  FREE(bitValue);
2186  return formula;
2187}
2188
2189
2190/**Function********************************************************************
2191
2192  Synopsis    [Creates a CTL formula with OR of Vector AND]
2193
2194  Description [This function returns Ctlp_Formula_t for nameVector = valueStr,
2195  nameVector is a form of var[i:j] or var<j:j>, valueStr is "k,l,...,q",
2196  and k,l,...,q is either integer or binary string.  Binary string starting
2197  with 'b', for instance, b0011. If n is not fitted in var[i:j] or size of
2198  binary string is not matched with var[i:j], NULL pointer is returned]
2199
2200  SideEffects []
2201
2202  SeeAlso     []
2203
2204******************************************************************************/
2205Ctlp_Formula_t *
2206Ctlp_FormulaCreateVectorOr(
2207  char *nameVector,
2208  char *valueStr)
2209{
2210  Ctlp_Formula_t *formula,*tempFormula;
2211  char *preStr;
2212
2213  preStr = strtok(valueStr,",");
2214  formula = Ctlp_FormulaCreateVectorAnd(nameVector,preStr);
2215  if ( formula == NIL(Ctlp_Formula_t)){
2216    return NIL(Ctlp_Formula_t);
2217  }
2218  while( (preStr = strtok(NIL(char),",")) != NIL(char) ){
2219    tempFormula = Ctlp_FormulaCreateVectorAnd(nameVector,preStr);
2220    if ( tempFormula == NIL(Ctlp_Formula_t)){
2221      Ctlp_FormulaFree(formula);
2222      return NIL(Ctlp_Formula_t);
2223    }
2224    formula = Ctlp_FormulaCreate(Ctlp_OR_c,formula,tempFormula);
2225  }
2226  return formula;
2227}
2228
2229
2230/**Function********************************************************************
2231
2232  Synopsis    [Creates a CTL formula for equivalent property]
2233
2234  Description [This function assumes that each child is defined in binary
2235  domain. Enumerate type is not supported]
2236
2237  SideEffects []
2238
2239  SeeAlso     []
2240
2241******************************************************************************/
2242Ctlp_Formula_t *
2243Ctlp_FormulaCreateEquiv(
2244   char *left,
2245   char *right)
2246{
2247   Ctlp_Formula_t *formula,*formula1,*formula2;
2248
2249   char *one;
2250   char *zero;
2251
2252   one = "1";
2253   zero = "0";
2254
2255   formula1 = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(left),
2256                                 util_strsav(one));
2257   formula2 = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(right),
2258                                 util_strsav(zero));
2259   formula = Ctlp_FormulaCreate(Ctlp_XOR_c,formula1,formula2);
2260   return formula;
2261}
2262
2263/**Function********************************************************************
2264
2265  Synopsis    [Creates a CTL formula for equivalent of vector]
2266
2267  Description [This function returns a formula, which is the AND of a bitwise
2268  equivalence]
2269
2270  SideEffects []
2271
2272  SeeAlso     []
2273
2274******************************************************************************/
2275Ctlp_Formula_t *
2276Ctlp_FormulaCreateVectorEquiv(
2277  char *left,
2278  char *right)
2279{
2280  Ctlp_Formula_t *formula,*tempFormula;
2281  char *leftName,*rightName;
2282  char *leftVar, *rightVar;
2283  int  leftStart,leftEnd,rightStart,rightEnd,leftInterval,rightInterval;
2284  int  leftInc,rightInc,leftInd,rightInd,i;
2285
2286  leftName  = CtlpGetVectorInfoFromStr(left,&leftStart,&leftEnd,&leftInterval,&leftInc);
2287  rightName = CtlpGetVectorInfoFromStr(right,&rightStart,&rightEnd,&rightInterval,&rightInc);
2288  if (leftInterval != rightInterval){
2289     return NIL(Ctlp_Formula_t);
2290  }
2291  leftVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
2292  (void) sprintf(leftVar,"%s[%d]",leftName,leftStart);
2293  (void) CtlpChangeBracket(leftVar);
2294  rightVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
2295  (void) sprintf(rightVar,"%s[%d]",rightName,rightStart);
2296  (void) CtlpChangeBracket(rightVar);
2297
2298  formula = Ctlp_FormulaCreateEquiv(leftVar,rightVar);
2299  leftInd  = leftStart;
2300  rightInd = rightStart;
2301  for(i=leftStart;i!=leftEnd;i+=leftInc){
2302     leftInd  += leftInc;
2303     rightInd += rightInc;
2304     (void) sprintf(leftVar,"%s[%d]",leftName,leftInd);
2305     (void) CtlpChangeBracket(leftVar);
2306     (void) sprintf(rightVar,"%s[%d]",rightName,rightInd);
2307     (void) CtlpChangeBracket(rightVar);
2308     tempFormula = Ctlp_FormulaCreateEquiv(leftVar,rightVar);
2309     formula = Ctlp_FormulaCreate(Ctlp_AND_c,formula,tempFormula);
2310  }
2311  FREE(leftName);
2312  FREE(rightName);
2313  FREE(leftVar);
2314  FREE(rightVar);
2315  return formula;
2316}
2317
2318
2319/**Function********************************************************************
2320
2321  Synopsis    [Creates a CTL formula for multiple AX]
2322
2323  Description [This function returns a formula, which is the multiple
2324  times of AX. The given string includes the number of depth]
2325
2326  SideEffects []
2327
2328  SeeAlso     []
2329
2330******************************************************************************/
2331Ctlp_Formula_t *
2332Ctlp_FormulaCreateAXMult(
2333  char *string,
2334  Ctlp_Formula_t *formula)
2335{
2336  int i,num;
2337  char *str, *ptr;
2338  Ctlp_Formula_t *result;
2339  str = strchr(string,':');
2340  if ( str == NULL) return(NIL(Ctlp_Formula_t));
2341  str++;
2342
2343  num = strtol(str,&ptr,0);
2344
2345  if (num<=0){
2346    return (NIL(Ctlp_Formula_t));
2347  }
2348  result = Ctlp_FormulaCreate(Ctlp_AX_c,formula,NIL(Ctlp_Formula_t));
2349  for(i=1;i<num;i++){
2350    result = Ctlp_FormulaCreate(Ctlp_AX_c,result,NIL(Ctlp_Formula_t));
2351  }
2352  return result;
2353}
2354
2355
2356/**Function********************************************************************
2357
2358  Synopsis    [Creates a CTL formula for multiple EX]
2359
2360  Description [This function returns a formula, which is the multiple
2361  times of EX. The given string includes the number of depth]
2362
2363  SideEffects []
2364
2365  SeeAlso     []
2366
2367******************************************************************************/
2368Ctlp_Formula_t *
2369Ctlp_FormulaCreateEXMult(
2370  char *string,
2371  Ctlp_Formula_t *formula)
2372{
2373  int i, num;
2374  char *str, *ptr;
2375  Ctlp_Formula_t *result;
2376  str = strchr(string,':');
2377  if ( str == NULL) return(NIL(Ctlp_Formula_t));
2378  str++;
2379
2380  num = strtol(str,&ptr,0);
2381
2382  if (num<=0){
2383    return (NIL(Ctlp_Formula_t));
2384  }
2385  result = Ctlp_FormulaCreate(Ctlp_EX_c,formula,NIL(Ctlp_Formula_t));
2386  for(i=1;i<num;i++){
2387    result = Ctlp_FormulaCreate(Ctlp_EX_c,result,NIL(Ctlp_Formula_t));
2388  }
2389  return result;
2390}
2391
2392/**Function********************************************************************
2393
2394  Synopsis [Converts an array of CTL formulae to forward form.]
2395
2396  Description [Converts an array of CTL formulae to forward.  Creates a
2397  maximally shared representation if noshare is false, a representation without
2398  any sharing otherwise. ]
2399
2400  SideEffects []
2401
2402  SeeAlso     []
2403
2404******************************************************************************/
2405array_t *
2406Ctlp_FormulaArrayConvertToForward(array_t *formulaArray, int singleInitial,
2407                                  boolean doNotShareFlag)
2408{
2409  int i;
2410  Ctlp_Formula_t *formula, *existentialFormula, *forwardFormula;
2411  int numFormulae = array_n(formulaArray);
2412  array_t *forwardFormulaArray = array_alloc(Ctlp_Formula_t *, numFormulae);
2413  array_t *forwardDagArray;
2414  int compareValue;
2415
2416  for(i=0; i < numFormulae; i++) {
2417    formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
2418    existentialFormula = Ctlp_FormulaConvertToExistentialForm(formula);
2419    assert(existentialFormula != NIL(Ctlp_Formula_t));
2420    formula = NIL(Ctlp_Formula_t);
2421   /*
2422    ** compareValue = 0 : check with FALSE
2423    ** compareValue = 1 : check with not-FALSE
2424    */
2425    if (singleInitial)
2426      compareValue = FormulaGetCompareValue(existentialFormula);
2427    else
2428      compareValue = 0;
2429    forwardFormula = FormulaCreateWithType(Ctlp_AND_c);
2430    forwardFormula->left = FormulaCreateWithType(Ctlp_Init_c);
2431    if (compareValue == 0) {
2432      forwardFormula->right = FormulaCreateWithType(Ctlp_NOT_c);
2433      forwardFormula->right->left = existentialFormula;
2434    } else
2435      forwardFormula->right = existentialFormula;
2436    forwardFormula->right->states = (mdd_t *)forwardFormula;
2437    /* if formula was converted before, keep that reference */
2438    if(existentialFormula->dbgInfo.originalFormula != NIL(Ctlp_Formula_t))
2439      forwardFormula->dbgInfo.originalFormula =
2440        existentialFormula->dbgInfo.originalFormula;
2441    else
2442      forwardFormula->dbgInfo.originalFormula = existentialFormula;
2443
2444    forwardFormula->top = 1;
2445    forwardFormula->compareValue = compareValue;
2446    FormulaConvertToForward(forwardFormula->right, compareValue);
2447    CtlpFormulaSetStatesToNULL(forwardFormula);
2448    FormulaInsertForwardCompareNodes(forwardFormula, NULL, compareValue);
2449    array_insert(Ctlp_Formula_t *, forwardFormulaArray, i, forwardFormula);
2450  }
2451
2452  if (doNotShareFlag)
2453    return(forwardFormulaArray);
2454
2455  forwardDagArray = Ctlp_FormulaArrayConvertToDAG(forwardFormulaArray);
2456  array_free(forwardFormulaArray);
2457  return forwardDagArray;
2458}
2459
2460
2461/**Function********************************************************************
2462
2463  Synopsis    [Returns a string for each formula type.]
2464
2465  Description [Returns a string for each formula type.]
2466
2467  SideEffects []
2468
2469  SeeAlso     []
2470
2471******************************************************************************/
2472char *
2473Ctlp_FormulaGetTypeString(Ctlp_Formula_t *formula)
2474{
2475  char *result;
2476
2477  switch(formula->type) {
2478    /*
2479     * The cases are listed in rough order of their expected frequency.
2480     */
2481    case Ctlp_ID_c:
2482      result = util_strsav("ID");
2483      break;
2484    case Ctlp_OR_c:
2485      result = util_strsav("OR");
2486      break;
2487    case Ctlp_AND_c:
2488      result = util_strsav("AND");
2489      break;
2490    case Ctlp_THEN_c:
2491      result = util_strsav("THEN");
2492      break;
2493    case Ctlp_XOR_c:
2494      result = util_strsav("XOR");
2495      break;
2496    case Ctlp_EQ_c:
2497      result = util_strsav("EQ");
2498      break;
2499    case Ctlp_NOT_c:
2500      result = util_strsav("NOT");
2501      break;
2502    case Ctlp_EX_c:
2503      result = util_strsav("EX");
2504      break;
2505    case Ctlp_EG_c:
2506      result = util_strsav("EG");
2507      break;
2508    case Ctlp_EF_c:
2509      result = util_strsav("EF");
2510      break;
2511    case Ctlp_EU_c:
2512      result = util_strsav("EU");
2513      break;
2514    case Ctlp_AX_c:
2515      result = util_strsav("AX");
2516      break;
2517    case Ctlp_AG_c:
2518      result = util_strsav("AG");
2519      break;
2520    case Ctlp_AF_c:
2521      result = util_strsav("AF");
2522      break;
2523    case Ctlp_AU_c:
2524      result = util_strsav("AU");
2525      break;
2526    case Ctlp_TRUE_c:
2527      result = util_strsav("TRUE");
2528      break;
2529    case Ctlp_FALSE_c:
2530      result = util_strsav("FALSE");
2531      break;
2532    case Ctlp_Init_c:
2533      result = util_strsav("Init");
2534      break;
2535    case Ctlp_Cmp_c:
2536      result = util_strsav("Cmp");
2537      break;
2538    case Ctlp_FwdU_c:
2539      result = util_strsav("FwdU");
2540      break;
2541    case Ctlp_FwdG_c:
2542      result = util_strsav("FwdG");
2543      break;
2544    case Ctlp_EY_c:
2545      result = util_strsav("EY");
2546      break;
2547    case Ctlp_EH_c:
2548      result = util_strsav("EH");
2549      break;
2550    default:
2551      fail("Unexpected type");
2552  }
2553  return(result);
2554}
2555
2556
2557/**Function********************************************************************
2558
2559  Synopsis           [Tests if a formula is quantifier-free, ACTL, ECTL or
2560  mixed.]
2561
2562  Description [Tests if a formula is Quantifier free, ACTL, ECTL or mixed.  We
2563  assume that the formula is in existential normal form, and hence only
2564  contains existential temporal operators.
2565
2566  <p>The formula is ECTL if every temporal operator appears under an even
2567  number of negations, and it is ACTL if every temporal operator appears under
2568  an odd number of negations.  It is quantifier-free if it is both ECTL and
2569  ACTL (i.e., no temporal operators occur), and it is mixed if it is neither
2570  ECTL nor ACTL.]
2571
2572  SideEffects        []
2573
2574  SeeAlso            []
2575
2576******************************************************************************/
2577Ctlp_FormulaClass
2578Ctlp_CheckClassOfExistentialFormula(
2579  Ctlp_Formula_t *formula)
2580{
2581  Ctlp_FormulaType formulaType;
2582  Ctlp_Formula_t *rightFormula, *leftFormula;
2583  Ctlp_FormulaClass resultLeft, resultRight, tempResult, currentClass;
2584
2585  assert(formula != NIL(Ctlp_Formula_t));
2586  if(formula == NIL(Ctlp_Formula_t))
2587    return Ctlp_QuantifierFree_c;
2588
2589  formulaType = Ctlp_FormulaReadType(formula);
2590  leftFormula = Ctlp_FormulaReadLeftChild(formula);
2591  rightFormula = Ctlp_FormulaReadRightChild(formula);
2592
2593  /* Depending on the formula type, create result or recur */
2594  switch (formulaType) {
2595  case Ctlp_EX_c:
2596  case Ctlp_EG_c:
2597  case Ctlp_EF_c:
2598  case Ctlp_EU_c:
2599  case Ctlp_FwdU_c:
2600  case Ctlp_FwdG_c:
2601  case Ctlp_EY_c:
2602  case Ctlp_EH_c:
2603    resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
2604    if (formulaType == Ctlp_EU_c || formulaType == Ctlp_FwdU_c ||
2605        formulaType == Ctlp_FwdG_c )
2606      resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
2607    else
2608      resultRight = Ctlp_QuantifierFree_c;
2609
2610    tempResult = CtlpResolveClass(resultLeft, resultRight);
2611    currentClass = Ctlp_ECTL_c;
2612    return CtlpResolveClass(currentClass, tempResult);
2613  case Ctlp_AX_c:
2614  case Ctlp_AG_c:
2615  case Ctlp_AF_c:
2616  case Ctlp_AU_c:
2617    /* The formula is supposed to be only existential */
2618    fprintf(vis_stdout,
2619            "** Ctlp Error: unexpected (universal) operator type\n");
2620    assert(0);
2621    return Ctlp_Mixed_c;
2622  case Ctlp_OR_c:
2623  case Ctlp_AND_c:
2624    resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
2625    resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
2626    return CtlpResolveClass(resultLeft, resultRight);
2627  case Ctlp_NOT_c:
2628    tempResult = Ctlp_CheckClassOfExistentialFormula(leftFormula);
2629    return CtlpNegateFormulaClass(tempResult);
2630   case Ctlp_THEN_c:
2631    resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
2632    resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
2633    tempResult = CtlpNegateFormulaClass(resultLeft);
2634    return CtlpResolveClass(tempResult, resultRight);
2635  case Ctlp_XOR_c:
2636  case Ctlp_EQ_c:
2637    resultLeft =  Ctlp_CheckClassOfExistentialFormula(leftFormula);
2638    resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
2639    tempResult = CtlpResolveClass(resultLeft, resultRight);
2640    if( tempResult == Ctlp_QuantifierFree_c)
2641      return Ctlp_QuantifierFree_c;
2642    else
2643      return Ctlp_Mixed_c;
2644  case Ctlp_ID_c:
2645  case Ctlp_TRUE_c:
2646  case Ctlp_FALSE_c:
2647  case Ctlp_Init_c:
2648     return Ctlp_QuantifierFree_c;
2649  case Ctlp_Cmp_c:
2650    return Ctlp_Mixed_c;
2651  default:
2652    fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
2653    assert(0);
2654    return Ctlp_Mixed_c;
2655  }
2656} /* End of Ctlp_CheckTypeOfExistentialFormula */
2657
2658/**Function********************************************************************
2659
2660  Synopsis [Tests if an array of simple existential formulae has only
2661  ACTL, only ECTL or mixture of formula.]
2662
2663  Description        [Returns Ctlp_ECTL_c if the array contains only
2664  ECTL formulae, Ctlp_ACTL_c if it contains only ACTL formulae,
2665  Ctlp_QuantifierFree_c if there are no quantifiers in any formulae,
2666  and Ctlp_Mixed otherwise.]
2667
2668  SideEffects        []
2669
2670  SeeAlso            [Ctlp_CheckClassOfExistentialFormula]
2671
2672******************************************************************************/
2673Ctlp_FormulaClass
2674Ctlp_CheckClassOfExistentialFormulaArray(
2675  array_t *formulaArray)
2676{
2677  Ctlp_FormulaClass result;
2678  Ctlp_Formula_t *formula;
2679  int formulanr;
2680
2681  result = Ctlp_QuantifierFree_c;
2682  arrayForEachItem(Ctlp_Formula_t *, formulaArray, formulanr, formula){
2683    Ctlp_FormulaClass  formulaType;
2684    formulaType = Ctlp_CheckClassOfExistentialFormula(formula);
2685    result = CtlpResolveClass(result, formulaType);
2686    if(result == Ctlp_Mixed_c)
2687      return result;
2688  }
2689  return result;
2690} /* End of Ctlp_CheckTypeOfExistentialFormulaArray */
2691
2692
2693/**Function********************************************************************
2694
2695  Synopsis    [Compare two formulas for equality]
2696
2697  Description [Checks if two formulas are syntactically the same.  Equivalent
2698  constructions such as TRUE and TRUE+FALSE are not recognized, but copies are
2699  handled correctly, and strings are compared using strcmp.]
2700
2701  SideEffects []
2702
2703  SeeAlso     [FormulaCompare]
2704
2705******************************************************************************/
2706boolean
2707Ctlp_FormulaIdentical(
2708  Ctlp_Formula_t *formula1,
2709  Ctlp_Formula_t *formula2)
2710{
2711  return(FormulaCompare((char *)formula1, (char *)formula2) == 0);
2712}
2713
2714
2715/**Function********************************************************************
2716
2717  Synopsis    [Replaces non-monotonic operators in a formula.]
2718
2719  Description [This function takes a parse tree for a CTL formula and
2720  transforms it into another tree that has only monotonic operators.
2721  The non-monotonic operators are <code>XOR</code> and <code>EQ</code>.
2722  They are replaced by eqivalent trees.  Specificallt, <code>XOR(a,b)</code>
2723  is replaced by <code>OR(AND(a,NOT(b)),AND(NOT(a),b))</code> and
2724  <code>f <-> g</code> is replaced by <code>AND(f->g,g->f)</code>.<p>
2725
2726  It is important that the original formula be a tree.  The idea is that this
2727  function should be called right after reading the formulae from file.  Since
2728  the information attached to the parse tree by the model checking procedures
2729  is not preserved, it is also important that no such information exists.
2730  These conditions are checked by an assertion.<p>
2731
2732  This function does not deal with the forward CTL operators.  Reduction to
2733  monotonic operators should be performed before conversion to forward CTL.]
2734
2735  SideEffects [The argument is modified.  The new formulae will apprear
2736  when they are printed out.]
2737
2738  SeeAlso     [Ctlp_FormulaArrayMakeMonotonic]
2739
2740******************************************************************************/
2741void
2742Ctlp_FormulaMakeMonotonic(
2743  Ctlp_Formula_t *formula)
2744{
2745  Ctlp_Formula_t *left, *right;
2746  Ctlp_FormulaType type;
2747
2748  if (formula == NIL(Ctlp_Formula_t)) {
2749    return;
2750  }
2751
2752  /* Make sure (recursively) that this (sub)-formula is still in its pristine
2753   * state.  Specifically, that the parse graph is a tree.
2754   */
2755  assert(formula->refCount == 1 &&
2756         formula->states == NIL(mdd_t) &&
2757         formula->underapprox == NIL(mdd_t) &&
2758         formula->overapprox == NIL(mdd_t) &&
2759         formula->latest == Ctlp_Incomparable_c &&
2760         formula->dbgInfo.data == NIL(void) &&
2761         formula->dbgInfo.freeFn == (Ctlp_DbgInfoFreeFn) NULL &&
2762         formula->dbgInfo.convertedFlag == FALSE &&
2763         formula->dbgInfo.originalFormula == NIL(Ctlp_Formula_t) &&
2764         formula->top == 0 &&
2765         formula->compareValue == 0
2766         );
2767
2768  type = Ctlp_FormulaReadType(formula);
2769
2770  /* Leaves remain unchanged. */
2771  if (type == Ctlp_ID_c || type == Ctlp_TRUE_c || type == Ctlp_FALSE_c) {
2772    return;
2773  }
2774
2775  /* First recursively fix the children. */
2776  left  = Ctlp_FormulaReadLeftChild(formula);
2777  Ctlp_FormulaMakeMonotonic(left);
2778  right = Ctlp_FormulaReadRightChild(formula);
2779  Ctlp_FormulaMakeMonotonic(right);
2780
2781  /* Fix this node if it is not monotonic. */
2782  switch (type) {
2783  case Ctlp_EX_c:
2784  case Ctlp_EG_c:
2785  case Ctlp_EF_c:
2786  case Ctlp_EU_c:
2787  case Ctlp_AX_c:
2788  case Ctlp_AG_c:
2789  case Ctlp_AF_c:
2790  case Ctlp_AU_c:
2791  case Ctlp_OR_c:
2792  case Ctlp_AND_c:
2793  case Ctlp_NOT_c:
2794  case Ctlp_THEN_c:
2795  case Ctlp_EY_c:
2796  case Ctlp_EH_c:
2797    /* Nothing to be done */
2798    break;
2799  case Ctlp_EQ_c: {
2800    Ctlp_Formula_t *dupLeft, *dupRight;
2801    Ctlp_Formula_t *thenLeft, *thenRight;
2802    dupLeft   = Ctlp_FormulaDup(left);
2803    dupRight  = Ctlp_FormulaDup(right);
2804    thenLeft  = Ctlp_FormulaCreate(Ctlp_THEN_c, left, right);
2805    thenRight = Ctlp_FormulaCreate(Ctlp_THEN_c, dupRight, dupLeft);
2806    /* Fix the node in place. */
2807    formula->type  = Ctlp_AND_c;
2808    formula->left  = thenLeft;
2809    formula->right = thenRight;
2810    break;
2811  }
2812  case Ctlp_XOR_c: {
2813    Ctlp_Formula_t *dupLeft, *dupRight;
2814    Ctlp_Formula_t *negLeft, *negRight;
2815    Ctlp_Formula_t *andLeft, *andRight;
2816    dupLeft  = Ctlp_FormulaDup(left);
2817    dupRight = Ctlp_FormulaDup(right);
2818    negLeft  = Ctlp_FormulaCreate(Ctlp_NOT_c, dupLeft, NIL(Ctlp_Formula_t));
2819    negRight = Ctlp_FormulaCreate(Ctlp_NOT_c, dupRight, NIL(Ctlp_Formula_t));
2820    andLeft  = Ctlp_FormulaCreate(Ctlp_AND_c, left, negRight);
2821    andRight = Ctlp_FormulaCreate(Ctlp_AND_c, negLeft, right);
2822    /* Fix the node in place. */
2823    formula->type  = Ctlp_OR_c;
2824    formula->left  = andLeft;
2825    formula->right = andRight;
2826    break;
2827  }
2828  default:
2829    /* Forward CTL operators (that are not supported) and leaves (that are
2830     * dealt with above) would fall here.
2831     */
2832    fail("unexpected CTL formula type\n");
2833  }
2834
2835  return;
2836
2837} /* Ctlp_FormulaMakeMonotonic */
2838
2839
2840/**Function********************************************************************
2841
2842  Synopsis    [Replaces non-monotonic operators in an array of formulae.]
2843
2844  Description [Apply Ctlp_FormulaMakeMonotonic to each formula in the array.]
2845
2846  SideEffects [The formulae in the array are modified.]
2847
2848  SeeAlso     [Ctlp_FormulaMakeMonotonic]
2849
2850******************************************************************************/
2851void
2852Ctlp_FormulaArrayMakeMonotonic(
2853  array_t *formulaArray /* of Ctlp_Formula_t */)
2854{
2855  int i;
2856  Ctlp_Formula_t *formula;
2857
2858  if (formulaArray == NIL(array_t)) return;
2859  arrayForEachItem(Ctlp_Formula_t *, formulaArray, i, formula) {
2860    Ctlp_FormulaMakeMonotonic(formula);
2861  }
2862
2863} /* Ctlp_FormulaArrayMakeMonotonic */
2864
2865
2866/*---------------------------------------------------------------------------*/
2867/* Definition of internal functions                                          */
2868/*---------------------------------------------------------------------------*/
2869
2870
2871/**Function********************************************************************
2872
2873  Synopsis    [Increments the reference count of a formula.]
2874
2875  Description [The function increments the reference count of a formula. If
2876  the formula is NULL, the function does nothing.]
2877
2878  SideEffects []
2879
2880  SeeAlso     []
2881
2882******************************************************************************/
2883void
2884CtlpFormulaIncrementRefCount(
2885  Ctlp_Formula_t *formula)
2886{
2887  if(formula!=NIL(Ctlp_Formula_t)) {
2888    ++(formula->refCount);
2889  }
2890}
2891
2892/**Function********************************************************************
2893
2894  Synopsis    [Decrements the reference count of a formula.]
2895
2896  Description [The function decrements the reference count of formula and if
2897  the reference count reaches 0, the formula is freed. If the formula is NULL,
2898  the function does nothing. It is an error to decrement the reference count
2899  below 0.]
2900
2901  SideEffects []
2902
2903  SeeAlso     []
2904
2905******************************************************************************/
2906void
2907CtlpFormulaDecrementRefCount(
2908  Ctlp_Formula_t *formula)
2909{
2910  if(formula!=NIL(Ctlp_Formula_t)) {
2911    assert(formula->refCount>0);
2912    if(--(formula->refCount) == 0)
2913      CtlpFormulaFree(formula);
2914  }
2915}
2916/**Function********************************************************************
2917
2918  Synopsis    [Adds formula to the end of globalFormulaArray.]
2919
2920  SideEffects [Manipulates the global variable globalFormulaArray.]
2921
2922  SeeAlso     [CtlpYyparse]
2923
2924******************************************************************************/
2925void
2926CtlpFormulaAddToGlobalArray(
2927  Ctlp_Formula_t * formula)
2928{
2929  array_insert_last(Ctlp_Formula_t *, globalFormulaArray, formula);
2930}
2931
2932/**Function********************************************************************
2933
2934  Synopsis    [Frees a CTL formula.]
2935
2936  Description [The function frees all memory associated with the formula,
2937  including all MDDs and all character strings (however, does not free
2938  dbgInfo.originalFormula). It also decrements the reference counts of its two
2939  chidren. The function does nothing if formula is NULL.]
2940
2941  SideEffects []
2942
2943  SeeAlso     [Ctlp_FormulaArrayFree]
2944
2945******************************************************************************/
2946void
2947CtlpFormulaFree(
2948  Ctlp_Formula_t * formula)
2949{
2950  if (formula != NIL(Ctlp_Formula_t)) {
2951
2952    /*
2953     * Free any fields that are not NULL.
2954     */
2955
2956    if (formula->type == Ctlp_ID_c) {
2957      FREE(formula->left);
2958      FREE(formula->right);
2959    }
2960    else {
2961      if (formula->left  != NIL(Ctlp_Formula_t)) {
2962        CtlpFormulaDecrementRefCount(formula->left);
2963      }
2964      if (formula->right != NIL(Ctlp_Formula_t)) {
2965        CtlpFormulaDecrementRefCount(formula->right);
2966      }
2967    }
2968    if (formula->states != NIL(mdd_t))
2969      mdd_free(formula->states);
2970    if (formula->underapprox != NIL(mdd_t))
2971      mdd_free(formula->underapprox);
2972    if (formula->overapprox != NIL(mdd_t))
2973      mdd_free(formula->overapprox);
2974    if (formula->Bottomstates != NIL(array_t))
2975      mdd_array_free(formula->Bottomstates);
2976    if (formula->Topstates != NIL(array_t))
2977      mdd_array_free(formula->Topstates);
2978    if (formula->matchfound_top != NIL(array_t))
2979      array_free(formula->matchfound_top);
2980    if (formula->matchelement_top != NIL(array_t))
2981      array_free(formula->matchelement_top);
2982    if (formula->matchfound_bot != NIL(array_t))
2983      array_free(formula->matchfound_bot);
2984    if (formula->matchelement_bot != NIL(array_t))
2985      array_free(formula->matchelement_bot);
2986    if (formula->leaves != NIL(array_t))
2987      array_free(formula->leaves);
2988    if (formula->dbgInfo.data != NIL(void)) {
2989      (*formula->dbgInfo.freeFn)(formula);
2990    }
2991    FREE(formula);
2992  }
2993}
2994
2995
2996/**Function********************************************************************
2997
2998  Synopsis    [Create a binary string of given value with size of interval ]
2999
3000  Description [The value is a binary string starting with 'b',
3001  a hexadecimal string starting with 'x', or an
3002  integer string. If Value is not fitted in the interval, 0 is return.
3003  Otherwise 1 is returned. Result string is saved at given pointer.]
3004
3005  SideEffects []
3006
3007  SeeAlso     []
3008
3009******************************************************************************/
3010int
3011CtlpStringChangeValueStrToBinString(
3012  char *value,
3013  char *binValueStr,
3014  int  interval)
3015{
3016  int i;
3017  long int num, mask;
3018  double maxNum;
3019  char *ptr;
3020
3021  mask = 1;
3022  maxNum = pow(2.0,(double)interval);
3023  errno = 0;
3024
3025  if(value[0] == 'b'){
3026    if ((int)strlen(value)-1 == interval){
3027                        for(i=1;i<=interval;i++){
3028        if (value[i] == '0' || value[i] == '1'){
3029          binValueStr[i-1] =  value[i];
3030        }else{
3031          return 0;
3032        }
3033      }
3034      binValueStr[interval] = '\0';
3035    }else{
3036      return 0;
3037    }
3038  }else if (value[0] == 'x'){
3039    for(i=1; i < (int)strlen(value); i++){
3040      if (!isxdigit((int)value[i])){
3041        return 0;
3042      }
3043    }
3044    num = strtol(++value,&ptr,16);
3045    if (errno) return 0;
3046    if ( num >= maxNum) return 0;
3047    for(i=0;i<interval;i++){
3048      if(num & (mask<<i)) binValueStr[interval-i-1] = '1';
3049      else binValueStr[interval-i-1] = '0';
3050    }
3051    binValueStr[interval] = '\0';
3052  }else{
3053    for(i=0;i<(int)strlen(value);i++){
3054      if (!isdigit((int)value[i])){
3055        return 0;
3056      }
3057    }
3058    num = strtol(value,&ptr,0);
3059    if (errno) return 0;
3060    if ( num >= maxNum) return 0;
3061    mask = 1;
3062    for(i=0;i<interval;i++){
3063      if(num & (mask<<i)) binValueStr[interval-i-1] = '1';
3064      else binValueStr[interval-i-1] = '0';
3065    }
3066    binValueStr[interval] = '\0';
3067  }
3068
3069  return(1);
3070}
3071
3072
3073/**Function********************************************************************
3074
3075  Synopsis    [Change [] to <>]
3076
3077  Description []
3078
3079  SideEffects [The input string contains ...[num] and this function changes it
3080  to ...<num>.]
3081
3082  SeeAlso     []
3083
3084******************************************************************************/
3085void
3086CtlpChangeBracket(
3087  char *inStr)
3088{
3089  int i, j;
3090  char *str;
3091
3092  j = 0;
3093  for (i=0;i<(int)strlen(inStr)+1;i++){
3094    if (inStr[i] != ' '){
3095      inStr[i-j] = inStr[i];
3096    }else{
3097      j++;
3098    }
3099  }
3100
3101  if (changeBracket == 0)
3102    return;
3103
3104  str = strchr(inStr,'[');
3105  if (str == NULL) return;
3106
3107  *str = '<';
3108  str = strchr(inStr,']');
3109  *str = '>';
3110}
3111
3112
3113/**Function********************************************************************
3114
3115  Synopsis    [Parse a given vector string.]
3116
3117  Description [Parse given vector string of the form of var<i:j> and
3118  string var is returned. Other information such as i, j, interval between
3119  i and j, and increment or decrement from i to j are saved.]
3120
3121  SideEffects []
3122
3123  SeeAlso     []
3124
3125******************************************************************************/
3126char *
3127CtlpGetVectorInfoFromStr(
3128   char *str,
3129   int  *start,
3130   int  *end,
3131   int  *interval,
3132   int  *inc)
3133{
3134  char *str1, *str2, *str3;
3135  char *startStr, *endStr;
3136  char *name, *ptr;
3137
3138  str1 = strchr(str,'[');
3139  str2 = strchr(str,':');
3140  str3 = strchr(str,']');
3141  startStr = ALLOC(char, str2-str1);
3142  endStr = ALLOC(char, str3-str2);
3143  name = ALLOC(char, str1-str+1);
3144
3145  (void) strncpy(name, str, str1-str);
3146  (void) strncpy(startStr, str1+1, str2-str1-1);
3147  (void) strncpy(endStr, str2+1, str3-str2-1);
3148
3149  startStr[str2-str1-1] = '\0';
3150  endStr[str3-str2-1] = '\0';
3151  name[str1-str] = '\0';
3152  *start = strtol(startStr,&ptr,0);
3153  *end = strtol(endStr,&ptr,0);
3154  if(*start > *end){
3155      *inc = -1;
3156      *interval = *start - *end + 1;
3157  } else {
3158      *inc = 1;
3159      *interval = *end - *start + 1;
3160  }
3161  FREE(startStr);
3162  FREE(endStr);
3163  return name;
3164}
3165
3166/**Function********************************************************************
3167
3168  Synopsis    [Insert macro formula into symbol table.]
3169
3170  Description [If the name is already in table return 0, otherwise insert the
3171  formula into the table and return 1]
3172
3173  SideEffects []
3174
3175  SeeAlso     []
3176
3177******************************************************************************/
3178int
3179CtlpFormulaAddToTable(
3180   char *name,
3181   Ctlp_Formula_t *formula,
3182   st_table *macroTable)
3183{
3184   if(macroTable == NIL(st_table)){
3185      macroTable = st_init_table(strcmp, st_strhash);
3186   }
3187   if(st_is_member(macroTable, name)){
3188      return 0;
3189   }
3190   st_insert(macroTable, name, (char *)formula);
3191   return 1;
3192}
3193
3194
3195/**Function********************************************************************
3196
3197  Synopsis    [Get macro formula from symbol table]
3198
3199  Description [If macro string is not found in table, NULL pointer is returned]
3200
3201  SideEffects []
3202
3203  SeeAlso     []
3204
3205******************************************************************************/
3206Ctlp_Formula_t *
3207CtlpFormulaFindInTable(
3208   char *name,
3209   st_table *macroTable)
3210{
3211   Ctlp_Formula_t *formula;
3212   if (st_lookup(macroTable, name, &formula)){
3213      return (Ctlp_FormulaDup(formula));
3214   }else{
3215      return NIL(Ctlp_Formula_t);
3216   }
3217}
3218
3219/**Function********************************************************************
3220
3221  Synopsis    [Returns the greatest lower bound of two classes]
3222
3223  Description [Returns the class of a formula that is the combination of a
3224  formula of class1 and class2.  Does this by computing the glb, where mixed <
3225  ECTL < quantifierFree, and mixed < ACTL < quantifierfree.]
3226
3227  SideEffects []
3228
3229  SeeAlso [Ctlp_CheckClassOfExistentialFormula]
3230
3231******************************************************************************/
3232Ctlp_FormulaClass
3233CtlpResolveClass(
3234  Ctlp_FormulaClass class1,
3235  Ctlp_FormulaClass class2)
3236{
3237  if ((class1 == Ctlp_Mixed_c) || (class2 == Ctlp_Mixed_c))
3238    return Ctlp_Mixed_c;
3239  if (class1 == Ctlp_QuantifierFree_c)
3240    return class2;
3241  if (class2 == Ctlp_QuantifierFree_c)
3242    return class1;
3243  if (class1 == class2)
3244    return class1;
3245
3246  return Ctlp_Mixed_c;
3247
3248}
3249
3250
3251/**Function********************************************************************
3252
3253  Synopsis    [Returns the class of a formula that is the negation of a formula
3254  of class "class".]
3255
3256  Description [The negation of a mixed (quantifier free, ECTL, ACTL) formula is
3257  mixed (quantifier free, ACTL, ECTL).]
3258
3259  SideEffects []
3260
3261  SeeAlso [Ctlp_CheckClassOfExistentialFormula]
3262
3263******************************************************************************/
3264Ctlp_FormulaClass
3265CtlpNegateFormulaClass(
3266  Ctlp_FormulaClass class_
3267)
3268{
3269  switch(class_){
3270  case Ctlp_Mixed_c:
3271    return Ctlp_Mixed_c;
3272  case Ctlp_QuantifierFree_c:
3273    return Ctlp_QuantifierFree_c;
3274  case Ctlp_ECTL_c:
3275    return Ctlp_ACTL_c;
3276  case Ctlp_ACTL_c:
3277    return Ctlp_ECTL_c;
3278  default:
3279    fprintf(vis_stderr, "**Ctlp Error: Unknown formula class\n");
3280    assert(0);
3281    return Ctlp_Mixed_c;
3282  }
3283}
3284
3285
3286/**Function********************************************************************
3287
3288  Synopsis    [Replaces the smallest important sub-fomula in a w-ACTL
3289  formula by bottom.]
3290
3291  Description [Creates a witness formula for a given w-ACTL formula by
3292  replacing the smallest inpurtant subformula with bottom.  This function is
3293  used in the approach to vacuity detection of Beer et al. (CAV97).  Formulae
3294  in w-ACTL are guaranteed to have a unique smallest important subformula,
3295  which is defined as follow.  If the formula is simple, its operands are not
3296  important.  (An exception is made for implications.  See
3297  ReplaceSimpleFormula.)  Otherwise, the non-simple operand is the important
3298  operand.  For (A p U q) or (E p U q), where p and q are both simple, p is the
3299  important operand.  For unary formulae, the only child is the important
3300  operand.  This function works also for ACTL formulae that are not in w-ACTL,
3301  and for which smallest important subformulae are not unique.
3302  The function picks up a smallest important subformula.]
3303
3304  SideEffects [none]
3305
3306  SeeAlso     [ReplaceSimpleFormula]
3307
3308******************************************************************************/
3309Ctlp_Formula_t *
3310Ctlp_FormulaCreateWitnessFormula(
3311  Ctlp_Formula_t *formula)
3312{
3313  Ctlp_FormulaType formulaType;
3314  Ctlp_Formula_t *rightFormula, *leftFormula;
3315  Ctlp_Formula_t *newLeftFormula, *newRightFormula;
3316
3317  assert(formula != NIL(Ctlp_Formula_t));
3318
3319  if(formula == NIL(Ctlp_Formula_t))
3320    return NIL(Ctlp_Formula_t);
3321
3322  formulaType = Ctlp_FormulaReadType(formula);
3323  leftFormula = Ctlp_FormulaReadLeftChild(formula);
3324  rightFormula = Ctlp_FormulaReadRightChild(formula);
3325
3326  if (Ctlp_FormulaTestIsQuantifierFree(formula)) {
3327    return ReplaceSimpleFormula(formula);
3328  }
3329
3330  switch (formulaType) {
3331  case Ctlp_AX_c:
3332  case Ctlp_EX_c:
3333  case Ctlp_AG_c:
3334  case Ctlp_EG_c:
3335  case Ctlp_AF_c:
3336  case Ctlp_EF_c:
3337  case Ctlp_NOT_c:
3338    newLeftFormula = Ctlp_FormulaCreateWitnessFormula(leftFormula);
3339    newRightFormula = NIL(Ctlp_Formula_t);
3340    break;
3341  case Ctlp_AU_c:
3342  case Ctlp_EU_c:
3343    /* If both or neither operands are simple, we choose the left one
3344       as important.  Deal with special case of converted AG p (E true U p). */
3345    if ((formulaType == Ctlp_EU_c &&
3346         Ctlp_FormulaReadType(leftFormula) == Ctlp_TRUE_c) ||
3347        (Ctlp_FormulaTestIsQuantifierFree(leftFormula) &&
3348         !Ctlp_FormulaTestIsQuantifierFree(rightFormula))) {
3349      newLeftFormula = Ctlp_FormulaDup(leftFormula);
3350      newRightFormula = Ctlp_FormulaCreateWitnessFormula(rightFormula);
3351    } else {
3352      newLeftFormula = Ctlp_FormulaCreateWitnessFormula(leftFormula);
3353      newRightFormula = Ctlp_FormulaDup(rightFormula);
3354    }
3355    break;
3356  case Ctlp_OR_c:
3357  case Ctlp_AND_c:
3358  case Ctlp_THEN_c:
3359    /* Here we know one is not simple */
3360    if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) {
3361      newLeftFormula = Ctlp_FormulaDup(leftFormula);
3362      newRightFormula = Ctlp_FormulaCreateWitnessFormula(rightFormula);
3363    } else {
3364      newLeftFormula = Ctlp_FormulaCreateWitnessFormula(leftFormula);
3365      newRightFormula = Ctlp_FormulaDup(rightFormula);
3366    }
3367    break;
3368  case Ctlp_XOR_c:
3369  case Ctlp_EQ_c:
3370    newLeftFormula = Ctlp_FormulaDup(leftFormula);
3371    newRightFormula = Ctlp_FormulaDup(rightFormula);
3372    break;
3373  default:
3374    newLeftFormula = NIL(Ctlp_Formula_t);
3375    newRightFormula = NIL(Ctlp_Formula_t);
3376    fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
3377    assert(0);
3378    break;
3379  }
3380  return Ctlp_FormulaCreate(formulaType,newLeftFormula,newRightFormula);
3381
3382} /* Ctlp_FormulaCreateWitnessFormula */
3383
3384
3385/*---------------------------------------------------------------------------*/
3386/* Definition of static functions                                            */
3387/*---------------------------------------------------------------------------*/
3388
3389/**Function********************************************************************
3390
3391  Synopsis    [Creates a CTL formula with just the type set.]
3392
3393  Description [Calls Ctlp_FormulaCreate with type, and all other fields NULL.]
3394
3395  SideEffects []
3396
3397  SeeAlso     [Ctlp_FormulaCreate]
3398
3399******************************************************************************/
3400static Ctlp_Formula_t *
3401FormulaCreateWithType(
3402  Ctlp_FormulaType  type)
3403{
3404  return (Ctlp_FormulaCreate(type, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t)));
3405}
3406
3407
3408/**Function********************************************************************
3409
3410  Synopsis    [The comparison function for the formula unique table.]
3411
3412  Description [The function takes as parameters two CTL formulae. It compares
3413  the formula type, the left child and the right child, and returns 0 if they
3414  match. Otherwise, it returns -1.]
3415
3416  SideEffects []
3417
3418  SeeAlso     [FormulaHash]
3419
3420******************************************************************************/
3421static int
3422FormulaCompare(
3423  const char *key1,
3424  const char *key2)
3425{
3426  Ctlp_Formula_t *formula1 = (Ctlp_Formula_t *) key1;
3427  Ctlp_Formula_t *formula2 = (Ctlp_Formula_t *) key2;
3428
3429  assert(key1 != NIL(char));
3430  assert(key2 != NIL(char));
3431
3432
3433  if(formula1->type != formula2->type) {
3434    return -1;
3435  }
3436  if(formula1->type == Ctlp_ID_c) {
3437    if(strcmp((char *) (formula1->left), (char *) (formula2->left)) ||
3438       strcmp((char *) (formula1->right), (char *) (formula2->right))) {
3439      return -1;
3440    } else
3441      return 0;
3442  } else {
3443    if(formula1->left != formula2->left)
3444      return -1;
3445    if(formula1->right != formula2->right)
3446      return -1;
3447    if (formula1->type == Ctlp_Cmp_c &&
3448        formula1->compareValue != formula2->compareValue) {
3449      return -1;
3450    }
3451    return 0;
3452  }
3453}
3454
3455/**Function********************************************************************
3456
3457  Synopsis    [The hash function for the formula unique table.]
3458
3459  Description [The function takes as parameter a CTL formula. If the formula
3460  type is Ctlp_ID_c, st_strhash is used with a concatenation of left and
3461  right children as the key string. Otherwise, something very similar to
3462  st_ptrhash is done.]
3463
3464  SideEffects []
3465
3466  SeeAlso     [FormulaCompare]
3467
3468******************************************************************************/
3469static int
3470FormulaHash(
3471  char *key,
3472  int modulus)
3473{
3474  char *hashString;
3475  int hashValue;
3476  Ctlp_Formula_t *formula = (Ctlp_Formula_t *) key;
3477
3478  if(formula->type==Ctlp_ID_c) {
3479    hashString = util_strcat3((char *) (formula->left), (char *)
3480                              (formula->right), "");
3481    hashValue = st_strhash(hashString, modulus);
3482    FREE(hashString);
3483    return hashValue;
3484  }
3485  return (int) ((((unsigned long) formula->left >>2) +
3486                 ((unsigned long) formula->right >>2)) % modulus);
3487}
3488
3489/**Function********************************************************************
3490
3491  Synopsis    [Hashes the formula into the unique table.]
3492
3493  Description [The function takes a formula and hashes it and all its
3494  subformulae into a unique table. It returns the unique formula identical to
3495  the formula being hashed. The formula returned will have maximum sharing
3496  with the formulae that are already present in uniqueTable. It returns
3497  NIL(Ctlp_Formula_t) if the formula is NIL(Ctlp_Formula_t).]
3498
3499  SideEffects [If a copy of some subformula of formula is present in
3500  uniqueTable then the copy is substituted for it and the reference count of
3501  the subform
3502  ula is decremented.]
3503
3504  SeeAlso     [FormulaCompare]
3505
3506******************************************************************************/
3507static Ctlp_Formula_t *
3508FormulaHashIntoUniqueTable(
3509  Ctlp_Formula_t *formula,
3510  st_table *uniqueTable)
3511{
3512  Ctlp_Formula_t *uniqueFormula, *uniqueLeft, *uniqueRight;
3513
3514  if(formula == NIL(Ctlp_Formula_t))
3515    return NIL(Ctlp_Formula_t);
3516  if(st_lookup(uniqueTable, formula, &uniqueFormula)) {
3517    return uniqueFormula;
3518  }
3519  else {
3520    if(formula->type == Ctlp_ID_c) {
3521      st_insert(uniqueTable, formula, formula);
3522      return formula;
3523    }
3524    else {
3525      uniqueLeft = FormulaHashIntoUniqueTable(formula->left, uniqueTable);
3526      if(uniqueLeft != NIL(Ctlp_Formula_t))
3527        if(uniqueLeft != formula->left) {
3528          CtlpFormulaDecrementRefCount(formula->left);
3529          formula->left = uniqueLeft;
3530          CtlpFormulaIncrementRefCount(formula->left);
3531        }
3532      uniqueRight = FormulaHashIntoUniqueTable(formula->right, uniqueTable);
3533      if(uniqueRight != NIL(Ctlp_Formula_t))
3534        if(uniqueRight != formula->right) {
3535          CtlpFormulaDecrementRefCount(formula->right);
3536          formula->right = uniqueRight;
3537          CtlpFormulaIncrementRefCount(formula->right);
3538        }
3539      if(st_lookup(uniqueTable, formula, &uniqueFormula)) {
3540        return uniqueFormula;
3541      }
3542      else {
3543        st_insert(uniqueTable, formula, formula);
3544        return formula;
3545      }
3546    }
3547  }
3548}
3549
3550/**Function********************************************************************
3551
3552  Synopsis    [Converts the formula tree to a DAG.]
3553
3554  Description [The function recursively builds an existential DAG for the
3555  formula. If a particular sub-formula has been encountered before, the
3556  converted existential sub-formula is pointed to by the field states and it
3557  is returned without creating a new formula.]
3558
3559  SideEffects [We abuse states to store which converted formula an original
3560  formula points to.]
3561
3562  SeeAlso     []
3563
3564******************************************************************************/
3565static Ctlp_Formula_t *
3566FormulaConvertToExistentialDAG(
3567  Ctlp_Formula_t *formula)
3568{
3569
3570  Ctlp_Formula_t *new_;
3571  char *variableNameCopy, *valueNameCopy;
3572
3573  if(formula==NIL(Ctlp_Formula_t))
3574    return NIL(Ctlp_Formula_t);
3575
3576  if(formula->states!=NIL(mdd_t)) {
3577    Ctlp_Formula_t *temp = (Ctlp_Formula_t *) (formula->states);
3578
3579    ++(temp->refCount);
3580    return temp;
3581  }
3582
3583  /*
3584   * Recursively convert each subformula.
3585   */
3586
3587  switch(formula->type) {
3588    case Ctlp_EF_c:
3589      /* EFf --> (E true U f)  */
3590      new_ = FormulaCreateWithType(Ctlp_EU_c);
3591      new_->left  = FormulaCreateWithType(Ctlp_TRUE_c);
3592      new_->right = FormulaConvertToExistentialDAG(formula->left);
3593      new_->dbgInfo.convertedFlag = TRUE;
3594      break;
3595
3596    case Ctlp_AX_c:
3597      /* AXf --> !(EX(!f)) */
3598      new_ = FormulaCreateWithType(Ctlp_NOT_c);
3599      new_->left = FormulaCreateWithType(Ctlp_EX_c);
3600      new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
3601      new_->left->left->left = FormulaConvertToExistentialDAG(formula->left);
3602      new_->dbgInfo.convertedFlag = TRUE;
3603      break;
3604
3605    case Ctlp_AG_c:
3606      /* AGf --> ![(E true U !f)] */
3607      new_ = FormulaCreateWithType(Ctlp_NOT_c);
3608      new_->left = FormulaCreateWithType(Ctlp_EU_c);
3609      new_->left->left = FormulaCreateWithType(Ctlp_TRUE_c);
3610      new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
3611      new_->left->right->left = FormulaConvertToExistentialDAG(formula->left);
3612      new_->dbgInfo.convertedFlag = TRUE;
3613      break;
3614
3615    case Ctlp_AF_c:
3616      /* AFf --> ![EG(!f)] */
3617      new_ = FormulaCreateWithType(Ctlp_NOT_c);
3618      new_->left = FormulaCreateWithType(Ctlp_EG_c);
3619      new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
3620      new_->left->left->left = FormulaConvertToExistentialDAG(formula->left);
3621      new_->dbgInfo.convertedFlag = TRUE;
3622      break;
3623
3624    case Ctlp_AU_c:
3625      /* A[fUg] --> !((E[!g U (!f*!g)]) + (EG!g)) */
3626
3627      new_ = FormulaCreateWithType(Ctlp_NOT_c); /* top */
3628      new_->left = FormulaCreateWithType(Ctlp_OR_c); /* ((E[!g U (!f*!g)]) + (EG!g)) */
3629
3630      new_->left->right = FormulaCreateWithType(Ctlp_EG_c); /* EG !g */
3631      new_->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
3632      new_->left->right->left->left = FormulaConvertToExistentialDAG(formula->right); /* g */
3633
3634      new_->left->left = FormulaCreateWithType(Ctlp_EU_c); /* E[!g U (!f*!g)] */
3635      new_->left->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
3636      new_->left->left->left->left = FormulaConvertToExistentialDAG(formula->right); /* g */
3637      new_->left->left->right = FormulaCreateWithType(Ctlp_AND_c); /* !f*!g */
3638      new_->left->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !f */
3639      new_->left->left->right->left->left = FormulaConvertToExistentialDAG(formula->left); /* f */
3640      new_->left->left->right->right = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
3641      new_->left->left->right->right->left = FormulaConvertToExistentialDAG(formula->right); /* g */
3642      new_->dbgInfo.convertedFlag = TRUE;
3643      break;
3644
3645    case Ctlp_ID_c:
3646      /* Make a copy of the name, and create a new formula. */
3647      variableNameCopy = util_strsav((char *)(formula->left));
3648      valueNameCopy = util_strsav((char *)(formula->right));
3649      new_ = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
3650      break;
3651
3652    case Ctlp_THEN_c:
3653    case Ctlp_EX_c:
3654    case Ctlp_EG_c:
3655    case Ctlp_EU_c:
3656    case Ctlp_OR_c:
3657    case Ctlp_AND_c:
3658    case Ctlp_NOT_c:
3659    case Ctlp_XOR_c:
3660    case Ctlp_EQ_c:
3661    case Ctlp_TRUE_c:
3662    case Ctlp_FALSE_c:
3663      /* These are already in the correct form.  Just convert subformulas. */
3664      new_ = FormulaCreateWithType(formula->type);
3665      new_->left = FormulaConvertToExistentialDAG(formula->left);
3666      new_->right = FormulaConvertToExistentialDAG(formula->right);
3667      break;
3668
3669    default:
3670      fail("Unexpected type");
3671  }
3672
3673  formula->states = (mdd_t *) new_; /*using states as pointer to the converted
3674                                     formula */
3675  new_->dbgInfo.originalFormula = formula;
3676  return new_;
3677}
3678
3679
3680/**Function********************************************************************
3681
3682  Synopsis    [Converts an existential formula to forward form.]
3683
3684  Description [Converts an existential formula to forward form. To
3685  convert current formula, it always refer to its parent node and left
3686  child of parent node. Current formula is right child of parent node.
3687  Parent node should be always Ctlp_AND_c and left child of parent node
3688  is already converted.  States is used to store a parent pointer
3689  throughout the procedure.]
3690
3691  SideEffects []
3692
3693  SeeAlso     []
3694
3695******************************************************************************/
3696static void
3697FormulaConvertToForward(Ctlp_Formula_t *formula, int compareValue)
3698{
3699  Ctlp_Formula_t *parent, *save;
3700  Ctlp_Formula_t *p, *q, *r, *f, *g;
3701  int            p_qf, q_qf;
3702  int            same_order;
3703
3704  if (formula == NIL(Ctlp_Formula_t))
3705    return;
3706
3707  parent = (Ctlp_Formula_t *)formula->states;
3708  r = parent->left; /* already converted */
3709
3710  /*
3711   * Recursively convert each subformula.
3712   */
3713
3714  switch(formula->type) {
3715    case Ctlp_EX_c:
3716      /*
3717      ** p ^ EXf -> Img(p) ^ f , Img(p) = EY(p)
3718      **
3719      **   *           *
3720      **  / \         / \
3721      ** p  EX  =>  EY   f
3722      **    |       |
3723      **    f       p
3724      */
3725
3726      formula->type = Ctlp_EY_c;
3727      save = formula->left;
3728      formula->left = parent->left;
3729      parent->left = formula;
3730      parent->right = save;
3731
3732      parent->top = 1;
3733      parent->compareValue = compareValue;
3734      parent->right->states = (mdd_t *)parent;
3735
3736      FormulaConvertToForward(parent->right, compareValue);
3737      break;
3738
3739    case Ctlp_EF_c:
3740      /*
3741      ** EFf --> (E true U f)
3742      ** p ^ (E true U f) --> FwdU(p, true) ^ f
3743      **
3744      **   *             *
3745      **  / \          /   \
3746      ** p  EF  =>  FwdU    f
3747      **    |        / \
3748      **    f       p  true
3749      */
3750
3751      formula->type = Ctlp_FwdU_c;
3752      save = formula->left;
3753      formula->right = FormulaCreateWithType(Ctlp_TRUE_c);
3754      formula->left = parent->left;
3755      parent->left = formula;
3756      parent->right = save;
3757
3758      parent->top = 1;
3759      parent->compareValue = compareValue;
3760      parent->right->states = (mdd_t *)parent;
3761
3762
3763      FormulaConvertToForward(parent->right, compareValue);
3764      break;
3765
3766    case Ctlp_EU_c:
3767      /*
3768      ** p ^ (E q U f) --> FwdU(p, q) ^ f
3769      **
3770      **   *             *
3771      **  / \          /   \
3772      ** p  EU  =>   FwdU   f
3773      **    /\        / \
3774      **   q  f      p   q
3775      */
3776
3777      formula->type = Ctlp_FwdU_c;
3778      save = formula->right;
3779      formula->right = formula->left;
3780      formula->left = parent->left;
3781      parent->left = formula;
3782      parent->right = save;
3783
3784      parent->top = 1;
3785      parent->compareValue = compareValue;
3786      parent->right->states = (mdd_t *)parent;
3787
3788      FormulaConvertToForward(parent->right, compareValue);
3789      break;
3790
3791    case Ctlp_EG_c:
3792      /*
3793      ** p ^ EGq --> FwdG(p, q)
3794      **
3795      **   *        FwdG
3796      **  / \        / \
3797      ** p  EG  =>  p   q
3798      **    /
3799      **   q
3800      */
3801
3802      parent->type = Ctlp_FwdG_c;
3803      parent->right = formula->left;
3804
3805      formula->left = NIL(Ctlp_Formula_t);
3806      formula->states = NIL(mdd_t);
3807      Ctlp_FormulaFree(formula);
3808
3809      parent->top = 1;
3810      parent->compareValue = compareValue;
3811      break;
3812
3813    case Ctlp_NOT_c:
3814      if (formula->left->type == Ctlp_NOT_c) {
3815        /*
3816        **   *             *
3817        **  / \      =>   / \
3818        ** r  NOT        r   f
3819        **     /
3820        **   NOT
3821        **   /
3822        **  f
3823        */
3824
3825        parent->right = formula->left->left;
3826        formula->left->left = NIL(Ctlp_Formula_t);
3827        formula->left->states = NIL(mdd_t);
3828        Ctlp_FormulaFree(formula->left);
3829        formula->left = NIL(Ctlp_Formula_t);
3830        formula->states = NIL(mdd_t);
3831        Ctlp_FormulaFree(formula);
3832
3833        parent->top = 1;
3834        parent->compareValue = compareValue;
3835        parent->right->states = (mdd_t *)parent;
3836
3837        FormulaConvertToForward(parent->right, compareValue);
3838      } else if (formula->left->type == Ctlp_THEN_c) {
3839        /*
3840        **   *
3841        **  / \
3842        ** r  NOT
3843        **    /
3844        **  THEN
3845        **   / \
3846        **  p   q
3847        */
3848
3849        p = formula->left->left;
3850        q = formula->left->right;
3851        p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
3852        q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
3853
3854        if (p_qf && q_qf)
3855          break;
3856        else if (p_qf ||
3857                 (p_qf == 0 && q_qf == 0 && !FormulaIsConvertible(q))) {
3858          /*
3859          ** !(p -> q) = p * !q
3860          **
3861          **   *     =>     *     =>      *
3862          **  / \          / \          /   \
3863          ** r  NOT       r   *        *    NOT
3864          **    /            / \      / \   /
3865          **  THEN          p  NOT   r   p q
3866          **   / \              /
3867          **  p   q            q
3868          */
3869
3870          parent->left = formula->left;
3871          parent->left->type = Ctlp_AND_c;
3872          parent->left->left = r;
3873          parent->left->right = p;
3874          parent->right = formula;
3875          parent->right->left = q;
3876
3877          parent->top = 1;
3878          parent->compareValue = compareValue;
3879          parent->right->states = (mdd_t *)parent;
3880
3881          FormulaConvertToForward(parent->right, compareValue);
3882        } else {
3883          /*
3884          ** !(p -> q) = p * !q
3885          **
3886          **   *     =>     *     =>      *
3887          **  / \          / \          /   \
3888          ** r  NOT       r   *        *     p
3889          **    /            / \      / \
3890          **  THEN          p  NOT   r  NOT
3891          **   / \              /       /
3892          **  p   q            q       q
3893          */
3894
3895          parent->left = formula->left;
3896          parent->left->type = Ctlp_AND_c;
3897          parent->left->left = r;
3898          parent->left->right = formula;
3899          parent->left->right->left = q;
3900          parent->left->right->right = NIL(Ctlp_Formula_t);
3901          parent->right = p;
3902
3903          parent->top = 1;
3904          parent->compareValue = compareValue;
3905          p->states = (mdd_t *)parent;
3906
3907          FormulaConvertToForward(p, compareValue);
3908        }
3909      } else if (formula->left->type == Ctlp_OR_c) {
3910        /*
3911        ** !(p + q) = !p * !q
3912        **
3913        **   *     =>     *     =>        *
3914        **  / \          / \            /   \
3915        ** r  NOT       r   *          *    NOT
3916        **    /            / \        / \    /
3917        **    OR         NOT NOT     r  NOT g=q(p)
3918        **   / \          /   /         /
3919        **  p   q        p   q         f=p(q)
3920        */
3921
3922        p = formula->left->left;
3923        q = formula->left->right;
3924        p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
3925        q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
3926
3927        if (p_qf && q_qf)
3928          break;
3929        else if (p_qf) {
3930          f = p;
3931          g = q;
3932        } else if (q_qf) {
3933          f = q;
3934          g = p;
3935        } else  {
3936          if (!FormulaIsConvertible(q)) {
3937            f = p;
3938            g = q;
3939          } else {
3940            f = q;
3941            g = p;
3942          }
3943        }
3944
3945        parent->left = formula->left;
3946        parent->left->type = Ctlp_AND_c;
3947        parent->left->left = r;
3948        parent->left->right = formula;
3949        parent->left->right->left = f;
3950        parent->left->right->right = NIL(Ctlp_Formula_t);
3951        parent->right = FormulaCreateWithType(Ctlp_NOT_c);
3952        parent->right->left = g;
3953
3954        parent->top = 1;
3955        parent->compareValue = compareValue;
3956        parent->right->states = (mdd_t *)parent;
3957
3958        FormulaConvertToForward(parent->right, compareValue);
3959      } else if (formula->left->type == Ctlp_AND_c) {
3960        /*
3961        ** !(p * q) = !p + !q
3962        **
3963        **   *          *(+)           *(+)
3964        **  / \         / \           /    \
3965        ** r  NOT  =>  r  OR    =>   *      *
3966        **    /           / \       / \    / \
3967        **   AND        NOT NOT    r  NOT r  NOT
3968        **   / \        /   /         /      /
3969        **  p   q      p   q         p      q
3970        */
3971
3972        p = formula->left->left;
3973        q = formula->left->right;
3974
3975        if (Ctlp_FormulaTestIsQuantifierFree(p) &&
3976            Ctlp_FormulaTestIsQuantifierFree(q)) {
3977          break;
3978        }
3979
3980        if (compareValue)
3981          parent->type = Ctlp_OR_c;
3982        parent->left = formula->left;
3983        parent->left->left = r;
3984        parent->left->right = formula;
3985        parent->left->right->left = p;
3986
3987        parent->right = FormulaCreateWithType(Ctlp_AND_c);
3988        parent->right->left = Ctlp_FormulaDup(r);
3989        parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
3990        parent->right->right->left = q;
3991
3992        parent->top = 0;
3993        parent->left->top = 1;
3994        parent->right->top = 1;
3995        parent->left->compareValue = compareValue;
3996        parent->right->compareValue = compareValue;
3997        parent->left->right->states = (mdd_t *)parent->left;
3998        parent->right->right->states = (mdd_t *)parent->right;
3999
4000        FormulaConvertToForward(parent->left->right, compareValue);
4001        FormulaConvertToForward(parent->right->right, compareValue);
4002      } else if (formula->left->type == Ctlp_XOR_c) {
4003        /*
4004        ** !(p ^ q) = p * q + !p * !q
4005        **
4006        **   *              *(+)                   *(+)
4007        **  / \            /     \               /      \
4008        ** |   |   =>     *       *      =>    *          *
4009        ** |   |         / \     / \          / \      /     \
4010        ** r  NOT       r   *   r   *        *   g    *      NOT
4011        **    /            / \     / \      / \      / \     /
4012        **   XOR          p   q  NOT NOT   r   f    r  NOT  g=q(p)
4013        **   / \                 /   /                 /
4014        **  p   q               p   q                 f=p(q)
4015        */
4016
4017        p = formula->left->left;
4018        q = formula->left->right;
4019        p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
4020        q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
4021
4022        same_order = 1;
4023        if (p_qf && q_qf)
4024          break;
4025        else if (p_qf) {
4026          f = p;
4027          g = q;
4028        } else if (q_qf) {
4029          f = q;
4030          g = p;
4031        } else {
4032          if (FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
4033            /*
4034            ** !(p ^ q) = q * p + !p * !q
4035            **
4036            **   *              *(+)                   *(+)
4037            **  / \            /     \               /      \
4038            ** |   |   =>     *       *      =>    *          *
4039            ** |   |         / \     / \          / \      /     \
4040            ** r  NOT       r   *   r   *        *   p    *      NOT
4041            **    /            / \     / \      / \      / \     /
4042            **   XOR          p   q  NOT NOT   r   q    r  NOT  q
4043            **   / \                 /   /                 /
4044            **  p   q               p   q                 p
4045            */
4046
4047            f = q;
4048            g = p;
4049            same_order = 0;
4050          } else if (!FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
4051            /*
4052            ** !(p ^ q) = p * q + !q * !p
4053            **
4054            **   *              *(+)                   *(+)
4055            **  / \            /     \               /      \
4056            ** |   |   =>     *       *      =>    *          *
4057            ** |   |         / \     / \          / \      /     \
4058            ** r  NOT       r   *   r   *        *   q    *      NOT
4059            **    /            / \     / \      / \      / \     /
4060            **   XOR          p   q  NOT NOT   r   p    r  NOT  p
4061            **   / \                 /   /                 /
4062            **  p   q               p   q                 q
4063            */
4064
4065            f = p;
4066            g = q;
4067            same_order = 0;
4068          } else {
4069            f = p;
4070            g = q;
4071          }
4072        }
4073
4074        if (compareValue)
4075          parent->type = Ctlp_OR_c;
4076        parent->left = formula;
4077        parent->left->type = Ctlp_AND_c;
4078        parent->left->left->type = Ctlp_AND_c;
4079        parent->left->left->left = r;
4080        parent->left->left->right = f;
4081        parent->left->right = g;
4082
4083        parent->right = FormulaCreateWithType(Ctlp_AND_c);
4084        parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4085        parent->right->left->left = Ctlp_FormulaDup(r);
4086        parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4087        if (same_order)
4088          parent->right->left->right->left = Ctlp_FormulaDup(f);
4089        else
4090          parent->right->left->right->left = Ctlp_FormulaDup(g);
4091        parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
4092        if (same_order)
4093          parent->right->right->left = Ctlp_FormulaDup(g);
4094        else
4095          parent->right->right->left = Ctlp_FormulaDup(f);
4096
4097        parent->top = 0;
4098        parent->left->top = 1;
4099        parent->right->top = 1;
4100        parent->left->compareValue = compareValue;
4101        parent->right->compareValue = compareValue;
4102        parent->left->right->states = (mdd_t *)parent->left;
4103        parent->right->right->states = (mdd_t *)parent->right;
4104
4105        FormulaConvertToForward(parent->left->right, compareValue);
4106        FormulaConvertToForward(parent->right->right, compareValue);
4107      } else if (formula->left->type == Ctlp_EQ_c) {
4108        /*
4109        ** !(EQ(p, q) = XOR(p, q)
4110        **
4111        **   *              *(+)                   *(+)
4112        **  / \            /     \                /     \
4113        ** |   |   =>     *       *      =>     *         *
4114        ** |   |         / \     / \          /   \     /   \
4115        ** r  NOT       r   *   r   *        *     g   *    NOT
4116        **    /            / \     / \      / \       / \   /
4117        **   EQ           p  NOT NOT  q    r  NOT    r   f g=q(p)
4118        **   / \             /   /            /
4119        **  p   q           q   p            f=p(q)
4120        */
4121
4122        p = formula->left->left;
4123        q = formula->left->right;
4124        p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
4125        q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
4126
4127        if (p_qf && q_qf)
4128          break;
4129        else if (p_qf) {
4130          f = p;
4131          g = q;
4132        } else if (q_qf) {
4133          f = q;
4134          g = p;
4135        } else {
4136          if (FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
4137            /*
4138            ** !(EQ(p, q) = XOR(p, q)
4139            **
4140            **   *              *(+)                   *(+)
4141            **  / \            /     \                /     \
4142            ** |   |   =>     *       *      =>     *         *
4143            ** |   |         / \     / \          /   \     /   \
4144            ** r  NOT       r   *   r   *        *     p   *     q
4145            **    /            / \     / \      / \       / \
4146            **   EQ           p  NOT NOT  q    r  NOT    r  NOT
4147            **   / \             /   /            /         /
4148            **  p   q           q   p            q         p
4149            */
4150
4151            if (compareValue)
4152              parent->type = Ctlp_OR_c;
4153            parent->left = parent->right;
4154            parent->left->type = Ctlp_AND_c;
4155            parent->left->left->type = Ctlp_AND_c;
4156            parent->left->left->left = r;
4157            parent->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4158            parent->left->left->right->left = q;
4159            parent->left->right = p;
4160
4161            parent->right = FormulaCreateWithType(Ctlp_AND_c);
4162            parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4163            parent->right->left->left = Ctlp_FormulaDup(r);
4164            parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4165            parent->right->left->right->left = Ctlp_FormulaDup(p);
4166            parent->right->right = Ctlp_FormulaDup(q);
4167
4168            parent->top = 0;
4169            parent->left->top = 1;
4170            parent->right->top = 1;
4171            parent->left->compareValue = compareValue;
4172            parent->right->compareValue = compareValue;
4173            parent->left->right->states = (mdd_t *)parent->left;
4174            parent->right->right->states = (mdd_t *)parent->right;
4175
4176            FormulaConvertToForward(parent->left->right, compareValue);
4177            FormulaConvertToForward(parent->right->right, compareValue);
4178            break;
4179          } else if (!FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
4180            /*
4181            ** !(EQ(p, q) = XOR(p, q)
4182            **
4183            **   *              *(+)                   *(+)
4184            **  / \            /     \                /     \
4185            ** |   |   =>     *       *      =>     *         *
4186            ** |   |         / \     / \          /   \     /   \
4187            ** r  NOT       r   *   r   *        *    NOT  *    NOT
4188            **    /            / \     / \      / \   /   / \   /
4189            **   EQ           p  NOT NOT  q    r   p q   r   q p
4190            **   / \             /   /
4191            **  p   q           q   p
4192            */
4193
4194            if (compareValue)
4195              parent->type = Ctlp_OR_c;
4196            parent->left = parent->right;
4197            parent->left->type = Ctlp_AND_c;
4198            parent->left->left->type = Ctlp_AND_c;
4199            parent->left->left->left = r;
4200            parent->left->left->right = p;
4201            parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4202            parent->left->right->left = q;
4203
4204            parent->right = FormulaCreateWithType(Ctlp_AND_c);
4205            parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4206            parent->right->left->left = Ctlp_FormulaDup(r);
4207            parent->right->left->right = Ctlp_FormulaDup(q);
4208            parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
4209            parent->right->right->left = Ctlp_FormulaDup(p);
4210
4211            parent->top = 0;
4212            parent->left->top = 1;
4213            parent->right->top = 1;
4214            parent->left->compareValue = compareValue;
4215            parent->right->compareValue = compareValue;
4216            parent->left->right->states = (mdd_t *)parent->left;
4217            parent->right->right->states = (mdd_t *)parent->right;
4218
4219            FormulaConvertToForward(parent->left->right, compareValue);
4220            FormulaConvertToForward(parent->right->right, compareValue);
4221            break;
4222          } else {
4223            f = p;
4224            g = q;
4225          }
4226        }
4227
4228        if (compareValue)
4229          parent->type = Ctlp_OR_c;
4230        parent->left = parent->right;
4231        parent->left->type = Ctlp_AND_c;
4232        parent->left->left->type = Ctlp_AND_c;
4233        parent->left->left->left = r;
4234        parent->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4235        parent->left->left->right->left = f;
4236        parent->left->right = g;
4237
4238        parent->right = FormulaCreateWithType(Ctlp_AND_c);
4239        parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4240        parent->right->left->left = Ctlp_FormulaDup(r);
4241        parent->right->left->right = Ctlp_FormulaDup(f);
4242        parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
4243        parent->right->right->left = Ctlp_FormulaDup(g);
4244
4245        parent->top = 0;
4246        parent->left->top = 1;
4247        parent->right->top = 1;
4248        parent->left->compareValue = compareValue;
4249        parent->right->compareValue = compareValue;
4250        parent->left->right->states = (mdd_t *)parent->left;
4251        parent->right->right->states = (mdd_t *)parent->right;
4252
4253        FormulaConvertToForward(parent->left->right, compareValue);
4254        FormulaConvertToForward(parent->right->right, compareValue);
4255      }
4256      break;
4257
4258    case Ctlp_THEN_c:
4259      /*
4260      ** (p -> q) = !p + q
4261      **
4262      **   *              *(+)
4263      **  / \            /    \
4264      ** r THEN  =>     *      *
4265      **    / \        / \    / \
4266      **   p   q      r  NOT r   q
4267      **                 /
4268      **                p
4269      */
4270
4271      p = formula->left;
4272      q = formula->right;
4273
4274      if (Ctlp_FormulaTestIsQuantifierFree(p) &&
4275          Ctlp_FormulaTestIsQuantifierFree(q)) {
4276        break;
4277      }
4278
4279      if (compareValue)
4280        parent->type = Ctlp_OR_c;
4281      parent->left = formula;
4282      parent->left->type = Ctlp_AND_c;
4283      parent->left->left = r;
4284      parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4285      parent->left->right->left = p;
4286
4287      parent->right = FormulaCreateWithType(Ctlp_AND_c);
4288      parent->right->left = Ctlp_FormulaDup(r);
4289      parent->right->right = q;
4290
4291      parent->top = 0;
4292      parent->left->top = 1;
4293      parent->right->top = 1;
4294      parent->left->compareValue = compareValue;
4295      parent->right->compareValue = compareValue;
4296      parent->left->right->states = (mdd_t *)parent->left;
4297      parent->right->right->states = (mdd_t *)parent->right;
4298
4299      FormulaConvertToForward(parent->left->right, compareValue);
4300      FormulaConvertToForward(parent->right->right, compareValue);
4301      break;
4302
4303    case Ctlp_OR_c:
4304      /*
4305      **   *              *(+)
4306      **  / \            /    \
4307      ** r  OR   =>     *      *
4308      **    / \        / \    / \
4309      **   p   q      r   p  r   q
4310      */
4311
4312      p = formula->left;
4313      q = formula->right;
4314
4315      if (Ctlp_FormulaTestIsQuantifierFree(p) &&
4316          Ctlp_FormulaTestIsQuantifierFree(q)) {
4317        break;
4318      }
4319
4320      if (compareValue)
4321        parent->type = Ctlp_OR_c;
4322      parent->left = formula;
4323      parent->left->type = Ctlp_AND_c;
4324      parent->left->left = r;
4325      parent->left->right = p;
4326
4327      parent->right = FormulaCreateWithType(Ctlp_AND_c);
4328      parent->right->left = Ctlp_FormulaDup(r);
4329      parent->right->right = q;
4330
4331      parent->top = 0;
4332      parent->left->top = 1;
4333      parent->right->top = 1;
4334      parent->left->compareValue = compareValue;
4335      parent->right->compareValue = compareValue;
4336      parent->left->right->states = (mdd_t *)parent->left;
4337      parent->right->right->states = (mdd_t *)parent->right;
4338
4339      FormulaConvertToForward(parent->left->right, compareValue);
4340      FormulaConvertToForward(parent->right->right, compareValue);
4341      break;
4342
4343    case Ctlp_AND_c:
4344      /*
4345      **   *     =>     *
4346      **  / \          / \
4347      ** r  AND      AND  g=q(p)
4348      **    / \      / \
4349      **   p   q    r   f=p(q)
4350      */
4351
4352      p = formula->left;
4353      q = formula->right;
4354      p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
4355      q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
4356
4357      if (p_qf && q_qf)
4358        break;
4359      else if (q_qf) {
4360        f = q;
4361        g = p;
4362      } else {
4363        f = p;
4364        g = q;
4365      }
4366
4367      parent->left = parent->right;
4368      parent->left->left = r;
4369      parent->left->right = f;
4370      parent->right = g;
4371
4372      parent->top = 1;
4373      parent->compareValue = compareValue;
4374      g->states = (mdd_t *)parent;
4375
4376      FormulaConvertToForward(g, compareValue);
4377      break;
4378
4379    case Ctlp_XOR_c:
4380      /*
4381      **   *             *(+)                  *(+)
4382      **  / \           /    \                /     \
4383      ** |   |   =>    *      *     =>      *         *
4384      ** |   |        / \    / \          /   \      / \
4385      ** r  XOR      r   *  r   *        *    NOT   *   g=q(p)
4386      **    / \         / \    / \      / \   /    / \
4387      **   p   q       q  NOT NOT p    r   f g    r  NOT
4388      **                  /   /                      /
4389      **                 p   q                      f=p(q)
4390      */
4391
4392      p = formula->left;
4393      q = formula->right;
4394      p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
4395      q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
4396
4397      if (p_qf && q_qf)
4398        break;
4399      else if (p_qf) {
4400        f = p;
4401        g = q;
4402      } else if (q_qf) {
4403        f = q;
4404        g = p;
4405      } else {
4406        if (FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
4407          /*
4408          **   *             *(+)                  *(+)
4409          **  / \           /    \                /     \
4410          ** |   |   =>    *      *     =>      *         *
4411          ** |   |        / \    / \          /   \      / \
4412          ** r  XOR      r   *  r   *        *     q    *   p
4413          **    / \         / \    / \      / \        / \
4414          **   p   q       q  NOT NOT p    r  NOT     r  NOT
4415          **                  /   /           /          /
4416          **                 p   q           p          q
4417          */
4418
4419          if (compareValue)
4420            parent->type = Ctlp_OR_c;
4421          parent->left = parent->right;
4422          parent->left->type = Ctlp_AND_c;
4423          parent->left->left->type = Ctlp_AND_c;
4424          parent->left->left->left = r;
4425          parent->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4426          parent->left->left->right->left = p;
4427          parent->left->right = q;
4428
4429          parent->right = FormulaCreateWithType(Ctlp_AND_c);
4430          parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4431          parent->right->left->left = Ctlp_FormulaDup(r);
4432          parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4433          parent->right->left->right->left = Ctlp_FormulaDup(q);
4434          parent->right->right = Ctlp_FormulaDup(p);
4435
4436          parent->top = 0;
4437          parent->left->top = 1;
4438          parent->right->top = 1;
4439          parent->left->compareValue = compareValue;
4440          parent->right->compareValue = compareValue;
4441          parent->left->right->states = (mdd_t *)parent->left;
4442          parent->right->right->states = (mdd_t *)parent->right;
4443
4444          FormulaConvertToForward(parent->left->right, compareValue);
4445          FormulaConvertToForward(parent->right->right, compareValue);
4446          break;
4447        } else if (!FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
4448          /*
4449          **   *             *(+)                   *(+)
4450          **  / \           /    \                /      \
4451          ** |   |   =>    *      *     =>      *          *
4452          ** |   |        / \    / \          /   \      /   \
4453          ** r  XOR      r   *  r   *        *    NOT   *    NOT
4454          **    / \         / \    / \      / \   /    / \   /
4455          **   p   q       q  NOT NOT p    r   p q    r   q p
4456          **                  /   /
4457          **                 p   q
4458          */
4459
4460          if (compareValue)
4461            parent->type = Ctlp_OR_c;
4462          parent->left = parent->right;
4463          parent->left->type = Ctlp_AND_c;
4464          parent->left->left->type = Ctlp_AND_c;
4465          parent->left->left->left = r;
4466          parent->left->left->right = p;
4467          parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4468          parent->left->right->left = q;
4469
4470          parent->right = FormulaCreateWithType(Ctlp_AND_c);
4471          parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4472          parent->right->left->left = Ctlp_FormulaDup(r);
4473          parent->right->left->right = Ctlp_FormulaDup(q);
4474          parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
4475          parent->right->right->left = Ctlp_FormulaDup(p);
4476
4477          parent->top = 0;
4478          parent->left->top = 1;
4479          parent->right->top = 1;
4480          parent->left->compareValue = compareValue;
4481          parent->right->compareValue = compareValue;
4482          parent->left->right->states = (mdd_t *)parent->left;
4483          parent->right->right->states = (mdd_t *)parent->right;
4484
4485          FormulaConvertToForward(parent->left->right, compareValue);
4486          FormulaConvertToForward(parent->right->right, compareValue);
4487          break;
4488        } else {
4489          f = p;
4490          g = q;
4491        }
4492      }
4493
4494      if (compareValue)
4495        parent->type = Ctlp_OR_c;
4496      parent->left = parent->right;
4497      parent->left->type = Ctlp_AND_c;
4498      parent->left->left = FormulaCreateWithType(Ctlp_AND_c);
4499      parent->left->left->left = r;
4500      parent->left->left->right = f;
4501      parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4502      parent->left->right->left = g;
4503
4504      parent->right = FormulaCreateWithType(Ctlp_AND_c);
4505      parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4506      parent->right->left->left = Ctlp_FormulaDup(r);
4507      parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4508      parent->right->left->right->left = Ctlp_FormulaDup(f);
4509      parent->right->right = Ctlp_FormulaDup(g);
4510
4511      parent->top = 0;
4512      parent->left->top = 1;
4513      parent->right->top = 1;
4514      parent->left->compareValue = compareValue;
4515      parent->right->compareValue = compareValue;
4516      parent->left->right->states = (mdd_t *)parent->left;
4517      parent->right->right->states = (mdd_t *)parent->right;
4518
4519      FormulaConvertToForward(parent->left->right, compareValue);
4520      FormulaConvertToForward(parent->right->right, compareValue);
4521      break;
4522
4523    case Ctlp_EQ_c:
4524      /*
4525      **   *              *(+)                   *(+)
4526      **  / \            /     \               /      \
4527      ** |   |   =>     *       *      =>    *          *
4528      ** |   |         / \     / \          / \      /     \
4529      ** r  EQ        r   *   r   *        *   g    *      NOT
4530      **    /\           / \     / \      / \      / \     /
4531      **   p  q         p   q  NOT NOT   r   f    r  NOT  g=q(p)
4532      **                       /   /                 /
4533      **                      p   q                 f=p(q)
4534      */
4535
4536      p = formula->left;
4537      q = formula->right;
4538      p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
4539      q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
4540
4541      same_order = 1;
4542      if (p_qf && q_qf)
4543        break;
4544      else if (p_qf) {
4545        f = p;
4546        g = q;
4547      } else if (q_qf) {
4548        f = q;
4549        g = p;
4550      } else {
4551        if (FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
4552          /*
4553          **   *              *(+)                   *(+)
4554          **  / \            /     \               /      \
4555          ** |   |   =>     *       *      =>    *          *
4556          ** |   |         / \     / \          / \      /     \
4557          ** r  EQ        r   *   r   *        *   p    *      NOT
4558          **    /\           / \     / \      / \      / \     /
4559          **   p  q         p   q  NOT NOT   r   q    r  NOT  q
4560          **                       /   /                 /
4561          **                      p   q                 p
4562          */
4563
4564          f = q;
4565          g = p;
4566          same_order = 0;
4567        } else if (!FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
4568          /*
4569          **   *              *(+)                   *(+)
4570          **  / \            /     \               /      \
4571          ** |   |   =>     *       *      =>    *          *
4572          ** |   |         / \     / \          / \      /     \
4573          ** r  EQ        r   *   r   *        *   q    *      NOT
4574          **    /\           / \     / \      / \      / \     /
4575          **   p  q         p   q  NOT NOT   r   p    r  NOT  p
4576          **                       /   /                 /
4577          **                      p   q                 q
4578          */
4579
4580          f = p;
4581          g = q;
4582          same_order = 0;
4583        } else {
4584          f = p;
4585          g = q;
4586        }
4587      }
4588
4589      if (compareValue)
4590        parent->type = Ctlp_OR_c;
4591      parent->left = parent->right;
4592      parent->left->type = Ctlp_AND_c;
4593      parent->left->left = FormulaCreateWithType(Ctlp_AND_c);
4594      parent->left->left->left = r;
4595      parent->left->left->right = f;
4596      parent->left->right = g;
4597
4598      parent->right = FormulaCreateWithType(Ctlp_AND_c);
4599      parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4600      parent->right->left->left = Ctlp_FormulaDup(r);
4601      parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4602      if (same_order)
4603        parent->right->left->right->left = Ctlp_FormulaDup(f);
4604      else
4605        parent->right->left->right->left = Ctlp_FormulaDup(g);
4606      parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
4607      if (same_order)
4608        parent->right->right->left = Ctlp_FormulaDup(g);
4609      else
4610        parent->right->right->left = Ctlp_FormulaDup(f);
4611
4612      parent->top = 0;
4613      parent->left->top = 1;
4614      parent->right->top = 1;
4615      parent->left->compareValue = compareValue;
4616      parent->right->compareValue = compareValue;
4617      parent->left->right->states = (mdd_t *)parent->left;
4618      parent->right->right->states = (mdd_t *)parent->right;
4619
4620      FormulaConvertToForward(parent->left->right, compareValue);
4621      FormulaConvertToForward(parent->right->right, compareValue);
4622      break;
4623
4624    case Ctlp_AX_c:
4625    case Ctlp_AG_c:
4626    case Ctlp_AF_c:
4627    case Ctlp_AU_c:
4628      fprintf(vis_stderr,
4629        "** ctl error : invalid node type in converting to forward formula.\n"
4630              );
4631      assert(0);
4632      break;
4633
4634    case Ctlp_ID_c:
4635    case Ctlp_TRUE_c:
4636    case Ctlp_FALSE_c:
4637      break;
4638
4639    default:
4640      fail("Unexpected type");
4641  }
4642}
4643
4644
4645/**Function********************************************************************
4646
4647  Synopsis    [Inserts compare nodes into forward formula.]
4648
4649  Description [Inserts compare nodes into forward formula.]
4650
4651  SideEffects []
4652
4653  SeeAlso     []
4654
4655******************************************************************************/
4656static void
4657FormulaInsertForwardCompareNodes(Ctlp_Formula_t *formula,
4658                                 Ctlp_Formula_t *parent,
4659                                 int compareValue)
4660{
4661  Ctlp_Formula_t *new_;
4662
4663  if (formula->top) {
4664    if (!parent) {
4665      new_ = FormulaCreateWithType(Ctlp_Cmp_c);
4666      memcpy((void *)new_, (void *)formula, sizeof(Ctlp_Formula_t));
4667      formula->type = Ctlp_Cmp_c;
4668      formula->left = new_;
4669      formula->right = FormulaCreateWithType(Ctlp_FALSE_c);
4670      formula->compareValue = compareValue;
4671    } else {
4672      new_ = FormulaCreateWithType(Ctlp_Cmp_c);
4673      new_->left = formula;
4674      new_->right = FormulaCreateWithType(Ctlp_FALSE_c);
4675      new_->compareValue = compareValue;
4676      if (parent->left == formula)
4677        parent->left = new_;
4678      else
4679        parent->right = new_;
4680    }
4681    return;
4682  }
4683  FormulaInsertForwardCompareNodes(formula->left, formula, compareValue);
4684  FormulaInsertForwardCompareNodes(formula->right, formula, compareValue);
4685}
4686
4687
4688/**Function********************************************************************
4689
4690  Synopsis    [Determines which conversion formula is better.]
4691
4692  Description [Determines which conversion formula is better between
4693  init ^ f != FALSE and init ^ !f == FALSE.]
4694
4695  SideEffects []
4696
4697  SeeAlso     []
4698
4699******************************************************************************/
4700static int
4701FormulaGetCompareValue(Ctlp_Formula_t *formula)
4702{
4703  int   compareValue;
4704
4705  if (FormulaIsConvertible(formula))
4706    compareValue = 1; /* check whether the result is not FALSE */
4707  else
4708    compareValue = 0; /* check whether the result is FALSE. */
4709
4710  return(compareValue);
4711}
4712
4713
4714/**Function********************************************************************
4715
4716  Synopsis    [Checks whether a formula can be converted to forward further.]
4717
4718  Description [Checks whether a formula can be converted to forward further.
4719  It returns 1 if it is convertible, and returns 0 if it is not convertible,
4720  and returns 2 if it is partially convertible.]
4721
4722  SideEffects []
4723
4724  SeeAlso     []
4725
4726******************************************************************************/
4727static int
4728FormulaIsConvertible(Ctlp_Formula_t *formula)
4729{
4730  int   convertible;
4731  int   value1, value2;
4732
4733  if (Ctlp_FormulaTestIsQuantifierFree(formula))
4734    convertible = 1;
4735  else if (formula->type == Ctlp_ID_c)
4736    convertible = 1;
4737  else if (formula->type == Ctlp_EX_c ||
4738           formula->type == Ctlp_EU_c ||
4739           formula->type == Ctlp_EF_c ||
4740           formula->type == Ctlp_EG_c) {
4741    convertible = 1;
4742  } else if (formula->type == Ctlp_NOT_c) {
4743    if (formula->left->type == Ctlp_NOT_c) {
4744      if (formula->left->left->type == Ctlp_EX_c ||
4745          formula->left->left->type == Ctlp_EU_c ||
4746          formula->left->left->type == Ctlp_EF_c ||
4747          formula->left->left->type == Ctlp_EG_c) {
4748        convertible = 1;
4749      } else {
4750        convertible = FormulaIsConvertible(formula->left->left);
4751      }
4752    } else {
4753      if (formula->left->type == Ctlp_EX_c ||
4754          formula->left->type == Ctlp_EU_c ||
4755          formula->left->type == Ctlp_EF_c ||
4756          formula->left->type == Ctlp_EG_c) {
4757        convertible = 0;
4758      } else {
4759        value1 = FormulaIsConvertible(formula->left);
4760        value2 = FormulaIsConvertible(formula->right);
4761        switch (formula->type) {
4762        case Ctlp_AND_c:
4763        case Ctlp_OR_c:
4764          convertible = (value1 & 0x1) * (value2 & 0x1);
4765          break;
4766        case Ctlp_THEN_c:
4767          convertible = value1 * (value2 & 0x1);
4768          break;
4769        default :
4770          convertible = 2;
4771          break;
4772        }
4773      }
4774    }
4775  } else {
4776    value1 = FormulaIsConvertible(formula->left);
4777    value2 = FormulaIsConvertible(formula->right);
4778    switch (formula->type) {
4779    case Ctlp_AND_c:
4780    case Ctlp_OR_c:
4781      convertible = value1 * value2;
4782      break;
4783    case Ctlp_THEN_c:
4784      convertible = (value1 & 0x1) * value2;
4785      break;
4786    default :
4787      convertible = 2;
4788      break;
4789    }
4790  }
4791
4792  return(convertible);
4793}
4794
4795
4796/**Function********************************************************************
4797
4798  Synopsis    [Replaces a simple formula with bottom.]
4799
4800  Description [This function is used in generating the witness formula from a
4801  w-ACTL formula in Beer's approach to vacuity detection.  Replaces a simple
4802  (propositional) subformula with bottom, which is FALSE for even negation
4803  parity and TRUE for odd negation parity.  An exception is made when the top
4804  node of the subformula is an implication.  In that case, the top node and the
4805  antecedent (left child) are retained in the replacement, while the
4806  consequent (right child) is replaced by bottom.]
4807
4808  SideEffects [none]
4809
4810  SeeAlso     [Ctlp_FormulaCreateWitnessFormula]
4811
4812******************************************************************************/
4813static Ctlp_Formula_t *
4814ReplaceSimpleFormula(
4815  Ctlp_Formula_t * formula)
4816{
4817  Ctlp_Formula_t *newFormula;
4818
4819  assert(formula->negation_parity == Ctlp_Even_c ||
4820         formula->negation_parity == Ctlp_Odd_c);
4821
4822  if (Ctlp_FormulaReadType(formula) == Ctlp_THEN_c) {
4823    Ctlp_Formula_t *leftFormula, *rightFormula;
4824    Ctlp_Formula_t *newLeftFormula, *newRightFormula;
4825
4826    leftFormula = Ctlp_FormulaReadLeftChild(formula);
4827    rightFormula = Ctlp_FormulaReadRightChild(formula);
4828    newLeftFormula = Ctlp_FormulaDup(leftFormula);
4829    newRightFormula = ReplaceSimpleFormula(rightFormula);
4830    return Ctlp_FormulaCreate(Ctlp_THEN_c,newLeftFormula,newRightFormula);
4831  }
4832
4833  fprintf(vis_stderr, "Replacing formula ");
4834  Ctlp_FormulaPrint(vis_stderr, formula);
4835  if (formula->negation_parity == Ctlp_Even_c){
4836    fprintf(vis_stderr, " by FALSE\n");
4837    newFormula = FormulaCreateWithType(Ctlp_FALSE_c);
4838  } else{
4839    fprintf(vis_stderr, " by TRUE\n");
4840    newFormula = FormulaCreateWithType(Ctlp_TRUE_c);
4841  }
4842  newFormula->negation_parity = formula->negation_parity;
4843  return(newFormula);
4844}
Note: See TracBrowser for help on using the repository browser.