1 /**CFile****************************************************************
2
3 FileName [intUtil.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Interpolation engine.]
8
9 Synopsis [Various interpolation utilities.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 24, 2008.]
16
17 Revision [$Id: intUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "intInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34
35 /**Function*************************************************************
36
37 Synopsis [Returns 1 if the property fails in the initial state.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Inter_ManCheckInitialState(Aig_Man_t * p)46 int Inter_ManCheckInitialState( Aig_Man_t * p )
47 {
48 Cnf_Dat_t * pCnf;
49 Aig_Obj_t * pObj;
50 sat_solver * pSat;
51 int i, status;
52 //abctime clk = Abc_Clock();
53 pCnf = Cnf_Derive( p, Saig_ManRegNum(p) );
54 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
55 if ( pSat == NULL )
56 {
57 Cnf_DataFree( pCnf );
58 return 0;
59 }
60 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
61 //ABC_PRT( "Time", Abc_Clock() - clk );
62 if ( status == l_True )
63 {
64 p->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), 1 );
65 Saig_ManForEachPi( p, pObj, i )
66 if ( sat_solver_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pObj)] ) )
67 Abc_InfoSetBit( p->pSeqModel->pData, Aig_ManRegNum(p) + i );
68 }
69 Cnf_DataFree( pCnf );
70 sat_solver_delete( pSat );
71 return status == l_True;
72 }
73
74 /**Function*************************************************************
75
76 Synopsis [Returns 1 if the property holds in all states.]
77
78 Description []
79
80 SideEffects []
81
82 SeeAlso []
83
84 ***********************************************************************/
Inter_ManCheckAllStates(Aig_Man_t * p)85 int Inter_ManCheckAllStates( Aig_Man_t * p )
86 {
87 Cnf_Dat_t * pCnf;
88 sat_solver * pSat;
89 int status;
90 abctime clk = Abc_Clock();
91 pCnf = Cnf_Derive( p, Saig_ManRegNum(p) );
92 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
93 Cnf_DataFree( pCnf );
94 if ( pSat == NULL )
95 return 1;
96 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
97 sat_solver_delete( pSat );
98 ABC_PRT( "Time", Abc_Clock() - clk );
99 return status == l_False;
100 }
101
102 ////////////////////////////////////////////////////////////////////////
103 /// END OF FILE ///
104 ////////////////////////////////////////////////////////////////////////
105
106
107 ABC_NAMESPACE_IMPL_END
108
109