summaryrefslogtreecommitdiffstats
path: root/src/opt/res/resSat.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2010-11-01 01:35:04 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2010-11-01 01:35:04 -0700
commit6130e39b18b5f53902e4eab14f6d5cdde5219563 (patch)
tree0db0628479a1b750e9af1f66cb8379ebd0913d31 /src/opt/res/resSat.c
parentf0e77f6797c0504b0da25a56152b707d3357f386 (diff)
downloadabc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.gz
abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.bz2
abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.zip
initial commit of public abc
Diffstat (limited to 'src/opt/res/resSat.c')
-rw-r--r--src/opt/res/resSat.c49
1 files changed, 27 insertions, 22 deletions
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index d5983942..a17f92fa 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -23,6 +23,9 @@
#include "hop.h"
#include "satSolver.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -55,7 +58,7 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
int i, nNodes, status;
// make sure fanins contain POs of the AIG
- pObj = Vec_PtrEntry( vFanins, 0 );
+ pObj = (Abc_Obj_t *)Vec_PtrEntry( vFanins, 0 );
assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
// collect reachable nodes
@@ -63,13 +66,13 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
// assign unique numbers to each node
nNodes = 0;
- Abc_AigConst1(pAig)->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
+ Abc_AigConst1(pAig)->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
Abc_NtkForEachPi( pAig, pObj, i )
- pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
- Vec_PtrForEachEntry( vNodes, pObj, i )
- pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
- Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
- pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
+ pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+ pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
+ Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i ) // useful POs
+ pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
// start the solver
pSat = sat_solver_new();
@@ -78,28 +81,28 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
// add clause for the constant node
Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
// add clauses for AND gates
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
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 )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i )
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);
+ pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 0);
Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
- pObj = Vec_PtrEntry(vFanins, 1);
+ pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 1);
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);
+ pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 1);
Sat_SolverDoubleClauses( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy );
// add the equality constraints
- Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 )
+ Vec_PtrForEachEntryStart( Abc_Obj_t *, vFanins, pObj, i, 2 )
Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, ((int)(ABC_PTRUINT_T)pObj->pCopy) + nNodes, 0 );
// bookmark the roots
@@ -155,13 +158,13 @@ void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet )
// assign unique numbers to each node
nNodes = 0;
- Abc_AigConst1(pAig)->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
+ Abc_AigConst1(pAig)->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
Abc_NtkForEachPi( pAig, pObj, i )
- pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
- Vec_PtrForEachEntry( vNodes, pObj, i )
- pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
- Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
- pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
+ pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+ pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
+ Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i ) // useful POs
+ pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
// start the solver
pSat = sat_solver_new();
@@ -169,7 +172,7 @@ void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet )
// add clause for the constant node
Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
// add clauses for AND gates
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
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 );
@@ -232,7 +235,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
assert( iPat < nPatsLimit );
// derive the SAT solver
- pSat = Res_SatSimulateConstr( p->pAig, fOnSet );
+ pSat = (sat_solver *)Res_SatSimulateConstr( p->pAig, fOnSet );
pSat->fSkipSimplify = 1;
status = sat_solver_simplify( pSat );
if ( status == 0 )
@@ -278,7 +281,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
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 );
+ Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(vPats, i), k );
Lit = toLitCond( Var, value );
Vec_IntPush( vLits, Lit );
// printf( "%d", value );
@@ -406,3 +409,5 @@ int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+