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
|
/**CFile****************************************************************
FileName [giaSatoko.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Interface to Satoko solver.]
Author [Alan Mishchenko, Bruno Schmitt]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaSatoko.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "sat/cnf/cnf.h"
#include "sat/satoko/satoko.h"
#include "sat/satoko/solver.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
satoko_t * Gia_ManCreateSatoko( Gia_Man_t * p )
{
satoko_t * pSat = satoko_create();
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 );
int i, status;
//sat_solver_setnvars( pSat, p->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
{
if ( !satoko_add_clause( pSat, (unsigned *)pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
{
Cnf_DataFree( pCnf );
satoko_destroy( pSat );
return NULL;
}
}
Cnf_DataFree( pCnf );
status = satoko_simplify(pSat);
if ( status == SATOKO_OK )
return pSat;
satoko_destroy( pSat );
return NULL;
}
int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
{
abctime clk = Abc_Clock();
satoko_t * pSat;
int status, Cost = 0;
pSat = Gia_ManCreateSatoko( p );
if ( pSat )
{
satoko_configure(pSat, opts);
status = satoko_solve( pSat );
Cost = (unsigned)pSat->stats.n_conflicts;
satoko_destroy( pSat );
}
else
status = SATOKO_UNSAT;
if ( iOutput >= 0 )
Abc_Print( 1, "Output %6d : ", iOutput );
else
Abc_Print( 1, "Total: " );
if ( status == SATOKO_UNDEC )
Abc_Print( 1, "UNDECIDED " );
else if ( status == SATOKO_SAT )
Abc_Print( 1, "SATISFIABLE " );
else
Abc_Print( 1, "UNSATISFIABLE " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return Cost;
}
void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit )
{
if ( fSplit )
{
Gia_Man_t * pOne;
Gia_Obj_t * pRoot;
int i;
Gia_ManForEachCo( p, pRoot, i )
{
pOne = Gia_ManDupDfsCone( p, pRoot );
Gia_ManCallSatokoOne( pOne, opts, i );
Gia_ManStop( pOne );
}
return;
}
Gia_ManCallSatokoOne( p, opts, -1 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
|
