summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaSatEdge.c106
-rw-r--r--src/base/abci/abc.c8
-rw-r--r--src/sat/bsat/satSolver.c13
-rw-r--r--src/sat/bsat/satSolver.h2
4 files changed, 74 insertions, 55 deletions
diff --git a/src/aig/gia/giaSatEdge.c b/src/aig/gia/giaSatEdge.c
index 982aaa79..0e7bdf15 100644
--- a/src/aig/gia/giaSatEdge.c
+++ b/src/aig/gia/giaSatEdge.c
@@ -33,7 +33,7 @@ typedef struct Seg_Man_t_ Seg_Man_t;
struct Seg_Man_t_
{
sat_solver * pSat; // SAT solver
- Vec_Int_t * vCardVars; // candinality variables
+ //Vec_Int_t * vCardVars; // candinality variables
int nVars; // max vars (edge num)
int LogN; // base-2 log of max vars
int Power2; // power-2 of LogN
@@ -82,11 +82,7 @@ Vec_Int_t * Seg_ManCountIntEdges( Gia_Man_t * p )
Gia_ManForEachLut( p, iLut )
Gia_LutForEachFanin( p, iLut, iFanin, i )
if ( Gia_ObjIsAnd(Gia_ManObj(p, iFanin)) )
- {
- //printf( "Var %d: %d -> %d\n", Vec_IntSize(vEdges)/2, iFanin, iLut );
-
Vec_IntPushTwo( vEdges, iFanin, iLut );
- }
return vEdges;
}
Vec_Wec_t * Seg_ManCollectObjEdges( Vec_Int_t * vEdges, int nObjs )
@@ -149,7 +145,6 @@ Seg_Man_t * Seg_ManAlloc( Gia_Man_t * pGia )
p->vLits = Vec_IntAlloc( 0 );
nVarsAll = Seg_ManCountIntLevels( p, p->FirstVar );
sat_solver_setnvars( p->pSat, nVarsAll );
-printf( "Edges = %d. Total = %d.\n", p->FirstVar, nVarsAll );
// other
Gia_ManFillValue( pGia );
return p;
@@ -192,7 +187,7 @@ void Seg_ManStop( Seg_Man_t * p )
SeeAlso []
***********************************************************************/
-void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo )
+void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo, int fVerbose )
{
Gia_Obj_t * pObj;
Vec_Wec_t * vObjEdges;
@@ -247,6 +242,7 @@ void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo )
}
}
assert( Count == p->nVars );
+ if ( fVerbose )
printf( "Delay constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
nConstr = sat_solver_nclauses(p->pSat);
/*
@@ -295,7 +291,9 @@ void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo )
}
}
Vec_WecFree( vObjEdges );
+ if ( fVerbose )
printf( "Edge constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
+ if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
@@ -310,15 +308,14 @@ void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo )
SeeAlso []
***********************************************************************/
-void Seg_ManConvertResult( Seg_Man_t * p )
+Vec_Int_t * Seg_ManConvertResult( Seg_Man_t * p )
{
int iFanin, iObj, i;
Vec_Int_t * vEdges2 = Vec_IntAlloc( 1000 );
Vec_IntForEachEntryDouble( p->vEdges, iFanin, iObj, i )
if ( sat_solver_var_value(p->pSat, i/2) )
Vec_IntPushTwo( vEdges2, iFanin, iObj );
- Gia_ManEdgeFromArray( p->pGia, vEdges2 );
- Vec_IntFree( vEdges2 );
+ return vEdges2;
}
/**Function*************************************************************
@@ -332,23 +329,34 @@ void Seg_ManConvertResult( Seg_Man_t * p )
SeeAlso []
***********************************************************************/
-void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int fTwo, int fVerbose )
+void Seg_ManComputeDelay( Gia_Man_t * pGia, int DelayInit, int fTwo, int fVerbose )
{
+ int nBTLimit = 0;
+ int nTimeOut = 0;
+ int fVeryVerbose = 0;
+
Gia_Obj_t * pObj;
abctime clk = Abc_Clock();
- int i, d, iLut, iFirst, nVars, status, Limit;//, value;
+ Vec_Int_t * vEdges2 = NULL;
+ int i, iLut, iFirst, nVars, status, Delay, nConfs;
Seg_Man_t * p = Seg_ManAlloc( pGia );
+ Vec_Int_t * vVars = Vec_IntStartNatural( p->nVars );
+ int DelayStart = DelayInit ? DelayInit : p->DelayMax;
- //if ( fVerbose )
- printf( "Running SatEdge with delay %d and edge %d\n", Delay, fTwo+1 );
-
- Seg_ManCreateCnf( p, fTwo );
+ if ( fVerbose )
+ printf( "Running SatEdge with starting delay %d and edge %d (edge vars %d, total vars %d)\n",
+ DelayStart, fTwo+1, p->FirstVar, sat_solver_nvars(p->pSat) );
+ Seg_ManCreateCnf( p, fTwo, fVerbose );
//Sat_SolverWriteDimacs( p->pSat, "test_edge.cnf", NULL, NULL, 0 );
-
-// for ( Delay = p->DelayMax; Delay >= 2; Delay-- )
+ // set resource limits
+ sat_solver_set_resource_limits( p->pSat, nBTLimit, 0, 0, 0 );
+ sat_solver_set_runtime_limit( p->pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
+ sat_solver_set_random( p->pSat, 1 );
+ sat_solver_set_var_activity( p->pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
+ Vec_IntFree( vVars );
+ // increment delay gradually
+ for ( Delay = p->DelayMax; Delay >= 0; Delay-- )
{
- // collect assumptions
- Vec_IntClear( p->vLits );
Gia_ManForEachCoDriver( p->pGia, pObj, i )
{
if ( !Gia_ObjIsAnd(pObj) )
@@ -356,36 +364,32 @@ void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int fTwo, int fVerbose )
iLut = Gia_ObjId( p->pGia, pObj );
iFirst = Vec_IntEntry( p->vFirsts, iLut );
nVars = Vec_IntEntry( p->vNvars, iLut );
- Limit = Abc_MinInt( nVars, Delay );
-
-// for ( d = 0; d < Limit; d++ )
-// Vec_IntPush( p->vLits, Abc_Var2Lit(iFirst + d, 0) );
-// value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
-// assert( value );
-
- for ( d = Delay; d < nVars; d++ )
- Vec_IntPush( p->vLits, Abc_Var2Lit(iFirst + d, 1) );
+ if ( Delay < nVars )
+ sat_solver_push( p->pSat, Abc_Var2Lit(iFirst + Delay, 1) );
}
+ if ( Delay > DelayStart )
+ continue;
// solve with assumptions
- status = sat_solver_solve( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits), 0, 0, 0, 0 );
-
- //if ( status != l_True )
- // break;
-
+ //clk = Abc_Clock();
+ nConfs = sat_solver_nconflicts( p->pSat );
+ status = sat_solver_solve_internal( p->pSat );
+ nConfs = sat_solver_nconflicts( p->pSat ) - nConfs;
if ( status == l_True )
{
- int Count = 0;
- for ( i = 0; i < p->nVars; i++ )
- Count += sat_solver_var_value(p->pSat, i);
-
- //printf( "\n" );
- //Vec_IntPrint( p->vLits );
- printf( "Solution with delay %d exists. Edges = %d. ", Delay, Count );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-
if ( fVerbose )
{
+ int Count = 0;
+ for ( i = 0; i < p->nVars; i++ )
+ Count += sat_solver_var_value(p->pSat, i);
+ printf( "Solution with delay %2d and %5d edges exists. Conf = %8d. ", Delay, Count, nConfs );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
+ // save the result
+ Vec_IntFreeP( &vEdges2 );
+ vEdges2 = Seg_ManConvertResult( p );
+ if ( fVeryVerbose )
+ {
for ( i = 0; i < p->nVars; i++ )
printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
printf( " " );
@@ -397,13 +401,19 @@ void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int fTwo, int fVerbose )
}
else
{
- printf( "Proved UNSAT for delay %d. ", Delay );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ if ( fVerbose )
+ {
+ if ( status == l_False )
+ printf( "Proved UNSAT for delay %d. ", Delay );
+ else
+ printf( "Resource limit reached for delay %d. ", Delay );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
+ break;
}
}
- // convert and quit
- if ( status == l_True )
- Seg_ManConvertResult( p );
+ Gia_ManEdgeFromArray( p->pGia, vEdges2 );
+ Vec_IntFreeP( &vEdges2 );
Seg_ManStop( p );
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1676385a..96becd9d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -34923,11 +34923,6 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManConvertPackingToEdges( pAbc->pGia );
return 0;
}
- if ( DelayMax )
- {
- Seg_ManComputeDelay( pAbc->pGia, DelayMax, nEdges==2, fVerbose );
- return 0;
- }
if ( !fUseOld )
{
if ( pAbc->pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pAbc->pGia->pManTime) )
@@ -34935,7 +34930,8 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Currently this version of the algorithm does not work for designs with boxes.\n" );
return 0;
}
- Edg_ManAssignEdgeNew( pAbc->pGia, nEdges, fVerbose );
+ //Edg_ManAssignEdgeNew( pAbc->pGia, nEdges, fVerbose );
+ Seg_ManComputeDelay( pAbc->pGia, DelayMax, nEdges==2, fVerbose );
return 0;
}
if ( pAbc->pGia->pManTime && fReverse )
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index b9ab0740..815626ad 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -211,6 +211,19 @@ static inline int order_select(sat_solver* s, float random_var_freq) // selectv
return var_Undef;
}
+void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars)
+{
+ int i;
+ for (i = 0; i < s->size; i++)
+ s->activity[i] = 0;
+ s->var_inc = 1;
+ for ( i = 0; i < nVars; i++ )
+ {
+ s->activity[pVars[i]] = nVars-i;
+ order_update( s, pVars[i] );
+ }
+}
+
//=================================================================================================
// Activity functions:
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index e729d2c8..c4888c73 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -64,7 +64,7 @@ extern int sat_solver_count_assigned(sat_solver* s);
extern void sat_solver_setnvars(sat_solver* s,int n);
extern int sat_solver_get_var_value(sat_solver* s, int v);
-
+extern void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars);
extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 01:35:26 +0000