summaryrefslogtreecommitdiffstats
path: root/src/opt/res/resSat.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/res/resSat.c')
-rw-r--r--src/opt/res/resSat.c62
1 files changed, 31 insertions, 31 deletions
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index 798e7abc..d5983942 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -63,50 +63,50 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
// assign unique numbers to each node
nNodes = 0;
- Abc_AigConst1(pAig)->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+ Abc_AigConst1(pAig)->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
Abc_NtkForEachPi( pAig, pObj, i )
- pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+ pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
Vec_PtrForEachEntry( vNodes, pObj, i )
- pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+ pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
- pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+ pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
// start the solver
pSat = sat_solver_new();
sat_solver_store_alloc( pSat );
// add clause for the constant node
- Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
+ Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
// add clauses for AND gates
Vec_PtrForEachEntry( vNodes, pObj, i )
- Res_SatAddAnd( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy,
- (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+ Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
+ (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
Vec_PtrFree( vNodes );
// add clauses for POs
Vec_PtrForEachEntry( vFanins, pObj, i )
- Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy,
- (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+ Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
+ (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
// add trivial clauses
pObj = Vec_PtrEntry(vFanins, 0);
- Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 0 ); // care-set
+ Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
pObj = Vec_PtrEntry(vFanins, 1);
- Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 0 ); // on-set
+ Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // on-set
// bookmark the clauses of A
sat_solver_store_mark_clauses_a( pSat );
// duplicate the clauses
pObj = Vec_PtrEntry(vFanins, 1);
- Sat_SolverDoubleClauses( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy );
+ Sat_SolverDoubleClauses( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy );
// add the equality constraints
Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 )
- Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, ((int)(PORT_PTRUINT_T)pObj->pCopy) + nNodes, 0 );
+ Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, ((int)(ABC_PTRUINT_T)pObj->pCopy) + nNodes, 0 );
// bookmark the roots
sat_solver_store_mark_roots( pSat );
// solve the problem
- status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+ status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_False )
{
pCnf = sat_solver_store_release( pSat );
@@ -155,39 +155,39 @@ void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet )
// assign unique numbers to each node
nNodes = 0;
- Abc_AigConst1(pAig)->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+ Abc_AigConst1(pAig)->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
Abc_NtkForEachPi( pAig, pObj, i )
- pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+ pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
Vec_PtrForEachEntry( vNodes, pObj, i )
- pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+ pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
- pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+ pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
// start the solver
pSat = sat_solver_new();
// add clause for the constant node
- Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
+ Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
// add clauses for AND gates
Vec_PtrForEachEntry( vNodes, pObj, i )
- Res_SatAddAnd( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy,
- (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+ Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
+ (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
Vec_PtrFree( vNodes );
// add clauses for the first PO
pObj = Abc_NtkPo( pAig, 0 );
- Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy,
- (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+ Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
+ (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
// add clauses for the second PO
pObj = Abc_NtkPo( pAig, 1 );
- Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy,
- (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+ Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
+ (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
// add trivial clauses
pObj = Abc_NtkPo( pAig, 0 );
- Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 0 ); // care-set
+ Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
pObj = Abc_NtkPo( pAig, 1 );
- Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, !fOnSet ); // on-set
+ Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, !fOnSet ); // on-set
Vec_PtrFree( vFanins );
return pSat;
@@ -218,7 +218,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
//printf( "Looking for %s: ", fOnSet? "onset " : "offset" );
// decide what problem should be solved
- Lit = toLitCond( (int)(PORT_PTRUINT_T)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
+ Lit = toLitCond( (int)(ABC_PTRUINT_T)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
if ( fOnSet )
{
iPat = p->nPats1;
@@ -254,8 +254,8 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
for ( k = iPat; k < nPatsLimit; k++ )
{
// solve with the assumption
-// status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
- status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+// status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+ status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_False )
{
//printf( "Const %d\n", !fOnSet );
@@ -275,7 +275,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
Vec_IntClear( vLits );
for ( i = 0; i < p->nTruePis; i++ )
{
- Var = (int)(PORT_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
+ Var = (int)(ABC_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
value = (int)(pSat->model.ptr[Var] == l_True);
if ( value )
Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k );
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-02 03:28:38 +0000