1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
/**CFile****************************************************************
FileName [fraigCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: fraigCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Top-level equivalence checking procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan )
{
Aig_ProofType_t RetValue;
int clk, status;
// create the solver
RetValue = Aig_ClauseSolverStart( pMan );
if ( RetValue != AIG_PROOF_NONE )
return RetValue;
// perform solving
// simplify the problem
clk = clock();
status = solver_simplify(pMan->pSat);
if ( status == 0 )
{
// printf( "The problem is UNSATISFIABLE after simplification.\n" );
return AIG_PROOF_UNSAT;
}
// try to prove the output
RetValue = Aig_FraigProveOutput( pMan );
if ( RetValue != AIG_PROOF_TIMEOUT )
return RetValue;
// create equivalence classes
Aig_EngineSimulateRandomFirst( pMan );
// reduce equivalence classes using simulation
Aig_EngineSimulateFirst( pMan );
return RetValue;
}
/**Function*************************************************************
Synopsis [Top-level equivalence checking procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan )
{
Aig_ProofType_t RetValue;
int clk, status;
// solve the miter
clk = clock();
pMan->pSat->verbosity = pMan->pParam->fSatVerbose;
status = solver_solve( pMan->pSat, NULL, NULL, pMan->pParam->nSeconds );
if ( status == l_Undef )
{
// printf( "The problem timed out.\n" );
RetValue = AIG_PROOF_TIMEOUT;
}
else if ( status == l_True )
{
// printf( "The problem is SATISFIABLE.\n" );
RetValue = AIG_PROOF_SAT;
}
else if ( status == l_False )
{
// printf( "The problem is UNSATISFIABLE.\n" );
RetValue = AIG_PROOF_UNSAT;
}
else
assert( 0 );
// PRT( "SAT solver time", clock() - clk );
// if the problem is SAT, get the counterexample
if ( status == l_True )
{
if ( pMan->pModel ) free( pMan->pModel );
pMan->pModel = solver_get_model( pMan->pSat, pMan->vPiSatNums->pArray, pMan->vPiSatNums->nSize );
printf( "%d %d %d %d\n", pMan->pModel[0], pMan->pModel[1], pMan->pModel[2], pMan->pModel[3] );
}
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
