1 /**CFile****************************************************************
2
3 FileName [simSymSat.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Satisfiability to determine two variable symmetries.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: simSymSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22 #include "proof/fraig/fraig.h"
23 #include "sim.h"
24
25 ABC_NAMESPACE_IMPL_START
26
27
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31
32 static int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
33
34 ////////////////////////////////////////////////////////////////////////
35 /// FUNCTION DEFINITIONS ///
36 ////////////////////////////////////////////////////////////////////////
37
38 /**Function*************************************************************
39
40 Synopsis [Tries to prove the remaining pairs using SAT.]
41
42 Description [Continues to prove as long as it encounters symmetric pairs.
43 Returns 1 if a non-symmetric pair is found (which gives a counter-example).
44 Returns 0 if it finishes considering all pairs for all outputs.]
45
46 SideEffects []
47
48 SeeAlso []
49
50 ***********************************************************************/
Sim_SymmsGetPatternUsingSat(Sym_Man_t * p,unsigned * pPattern)51 int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern )
52 {
53 Vec_Int_t * vSupport;
54 Extra_BitMat_t * pMatSym, * pMatNonSym;
55 int Index1, Index2, Index3, IndexU, IndexV;
56 int v, u, i, k, b, out;
57
58 // iterate through outputs
59 for ( out = p->iOutput; out < p->nOutputs; out++ )
60 {
61 pMatSym = (Extra_BitMat_t *)Vec_PtrEntry( p->vMatrSymms, out );
62 pMatNonSym = (Extra_BitMat_t *)Vec_PtrEntry( p->vMatrNonSymms, out );
63
64 // go through the remaining variable pairs
65 vSupport = Vec_VecEntryInt( p->vSupports, out );
66 Vec_IntForEachEntry( vSupport, v, Index1 )
67 Vec_IntForEachEntryStart( vSupport, u, Index2, Index1+1 )
68 {
69 if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
70 continue;
71 p->nSatRuns++;
72
73 // collect the support variables that are symmetric with u and v
74 Vec_IntClear( p->vVarsU );
75 Vec_IntClear( p->vVarsV );
76 Vec_IntForEachEntry( vSupport, b, Index3 )
77 {
78 if ( Extra_BitMatrixLookup1( pMatSym, u, b ) )
79 Vec_IntPush( p->vVarsU, b );
80 if ( Extra_BitMatrixLookup1( pMatSym, v, b ) )
81 Vec_IntPush( p->vVarsV, b );
82 }
83
84 if ( Sim_SymmsSatProveOne( p, out, v, u, pPattern ) )
85 { // update the symmetric variable info
86 p->nSatRunsUnsat++;
87 Vec_IntForEachEntry( p->vVarsU, i, IndexU )
88 Vec_IntForEachEntry( p->vVarsV, k, IndexV )
89 {
90 Extra_BitMatrixInsert1( pMatSym, i, k ); // Theorem 1
91 Extra_BitMatrixInsert2( pMatSym, i, k ); // Theorem 1
92 Extra_BitMatrixOrTwo( pMatNonSym, i, k ); // Theorem 2
93 }
94 }
95 else
96 { // update the assymmetric variable info
97 p->nSatRunsSat++;
98 Vec_IntForEachEntry( p->vVarsU, i, IndexU )
99 Vec_IntForEachEntry( p->vVarsV, k, IndexV )
100 {
101 Extra_BitMatrixInsert1( pMatNonSym, i, k ); // Theorem 3
102 Extra_BitMatrixInsert2( pMatNonSym, i, k ); // Theorem 3
103 }
104
105 // remember the out
106 p->iOutput = out;
107 p->iVar1Old = p->iVar1;
108 p->iVar2Old = p->iVar2;
109 p->iVar1 = v;
110 p->iVar2 = u;
111 return 1;
112
113 }
114 }
115 // make sure that the symmetry matrix contains only cliques
116 assert( Extra_BitMatrixIsClique( pMatSym ) );
117 }
118
119 // mark that we finished all outputs
120 p->iOutput = p->nOutputs;
121 return 0;
122 }
123
124 /**Function*************************************************************
125
126 Synopsis [Returns 1 if the variables are symmetric; 0 otherwise.]
127
128 Description []
129
130 SideEffects []
131
132 SeeAlso []
133
134 ***********************************************************************/
Sim_SymmsSatProveOne(Sym_Man_t * p,int Out,int Var1,int Var2,unsigned * pPattern)135 int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern )
136 {
137 Fraig_Params_t Params;
138 Fraig_Man_t * pMan;
139 Abc_Ntk_t * pMiter;
140 int RetValue, i;
141 abctime clk;
142 int * pModel;
143
144 // get the miter for this problem
145 pMiter = Abc_NtkMiterForCofactors( p->pNtk, Out, Var1, Var2 );
146 // transform the miter into a fraig
147 Fraig_ParamsSetDefault( &Params );
148 Params.fInternal = 1;
149 Params.nPatsRand = 512;
150 Params.nPatsDyna = 512;
151 Params.nSeconds = ABC_INFINITY;
152
153 clk = Abc_Clock();
154 pMan = (Fraig_Man_t *)Abc_NtkToFraig( pMiter, &Params, 0, 0 );
155 p->timeFraig += Abc_Clock() - clk;
156 clk = Abc_Clock();
157 Fraig_ManProveMiter( pMan );
158 p->timeSat += Abc_Clock() - clk;
159
160 // analyze the result
161 RetValue = Fraig_ManCheckMiter( pMan );
162 // assert( RetValue >= 0 );
163 // save the pattern
164 if ( RetValue == 0 )
165 {
166 // get the pattern
167 pModel = Fraig_ManReadModel( pMan );
168 assert( pModel != NULL );
169 //printf( "Disproved by SAT: out = %d pair = (%d, %d)\n", Out, Var1, Var2 );
170 // transfer the model into the pattern
171 for ( i = 0; i < p->nSimWords; i++ )
172 pPattern[i] = 0;
173 for ( i = 0; i < p->nInputs; i++ )
174 if ( pModel[i] )
175 Sim_SetBit( pPattern, i );
176 // make sure these variables have the same value (1)
177 Sim_SetBit( pPattern, Var1 );
178 Sim_SetBit( pPattern, Var2 );
179 }
180 else if ( RetValue == -1 )
181 {
182 // this should never happen; if it happens, such is life
183 // we are conservative and assume that there is no symmetry
184 //printf( "STRANGE THING: out = %d %s pair = (%d %s, %d %s)\n",
185 // Out, Abc_ObjName(Abc_NtkCo(p->pNtk,Out)),
186 // Var1, Abc_ObjName(Abc_NtkCi(p->pNtk,Var1)),
187 // Var2, Abc_ObjName(Abc_NtkCi(p->pNtk,Var2)) );
188 memset( pPattern, 0, sizeof(unsigned) * p->nSimWords );
189 RetValue = 0;
190 }
191 // delete the fraig manager
192 Fraig_ManFree( pMan );
193 // delete the miter
194 Abc_NtkDelete( pMiter );
195 return RetValue;
196 }
197
198
199 ////////////////////////////////////////////////////////////////////////
200 /// END OF FILE ///
201 ////////////////////////////////////////////////////////////////////////
202
203
204 ABC_NAMESPACE_IMPL_END
205
206