1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 2007 SRI International, Menlo Park, CA 94025, USA.
6
7 This program is free software; you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation; either version 2 of the License, or
10 (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software
19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
20
21 */
22
23 //
24 // Implementation for class AllSat.
25 //
26 #include "macros.hh"
27 #include "vector.hh"
28 #include "allSat.hh"
29
AllSat(Bdd formula,int firstVariable,int lastVariable)30 AllSat::AllSat(Bdd formula, int firstVariable, int lastVariable)
31 : formula(formula),
32 firstVariable(firstVariable),
33 lastVariable(lastVariable),
34 nodeStack(0, lastVariable - firstVariable + 1),
35 dontCareSet(0, lastVariable - firstVariable + 1)
36 {
37 firstAssignment = true;
38 }
39
40 bool
nextAssignment()41 AllSat::nextAssignment()
42 {
43 if (firstAssignment)
44 {
45 //
46 // First solution.
47 //
48 if (formula == bddfalse)
49 return false;
50 assignment.resize(lastVariable + 1);
51 for (int i = firstVariable; i <= lastVariable; ++i)
52 assignment[i] = UNDEFINED;
53 forward(formula);
54 firstAssignment = false;
55 return true;
56 }
57 //
58 // Try to find another way of assigning to don't care variables.
59 //
60 int nrDontCares = dontCareSet.size();
61 for (int i = nrDontCares - 1; i >= 0; --i)
62 {
63 int var = dontCareSet[i];
64 if (assignment[var] == 0)
65 {
66 assignment[var] = 1;
67 for (++i; i < nrDontCares; ++i)
68 assignment[dontCareSet[i]] = 0;
69 return true;
70 }
71 }
72 for (int i = 0; i < nrDontCares; ++i)
73 assignment[dontCareSet[i]] = UNDEFINED;
74 dontCareSet.clear();
75 //
76 // Try to find another route to true through BDD.
77 //
78 int nodeDepth = nodeStack.size();
79 for (int i = nodeDepth - 1; i >= 0; --i)
80 {
81 Bdd b = nodeStack[i];
82 int var = bdd_var(b);
83 if (assignment[var] == 0)
84 {
85 Bdd n = bdd_high(b);
86 if (n != bddfalse)
87 {
88 assignment[var] = 1;
89 nodeStack.resize(i + 1);
90 forward(n);
91 return true;
92 }
93 }
94 assignment[var] = UNDEFINED;
95 }
96 return false;
97 }
98
99 void
forward(Bdd b)100 AllSat::forward(Bdd b)
101 {
102 Assert(b != bddfalse, "false BDD");
103 //
104 // There must be at least one path to true from b; find the least one.
105 //
106 while (b != bddtrue)
107 {
108 nodeStack.append(b);
109 int var = bdd_var(b);
110 Bdd n = bdd_low(b);
111 if (n == bddfalse)
112 {
113 n = bdd_high(b);
114 assignment[var] = 1;
115 }
116 else
117 assignment[var] = 0;
118 b = n;
119 }
120 //
121 // Any variables of interest not assigned to on this path are don't cares.
122 //
123 for (int i = firstVariable; i <= lastVariable; ++i)
124 {
125 if (assignment[i] == UNDEFINED)
126 {
127 assignment[i] = 0;
128 dontCareSet.append(i);
129 }
130 }
131 }
132