summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaSatoko.c133
-rw-r--r--src/base/abci/abc.c14
-rw-r--r--src/base/cmd/cmdAuto.c6
-rw-r--r--src/sat/satoko/satoko.h2
-rw-r--r--src/sat/satoko/solver.c16
-rw-r--r--src/sat/satoko/solver.h23
-rw-r--r--src/sat/satoko/solver_api.c27
7 files changed, 181 insertions, 40 deletions
diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c
index db81bd85..7cbc4184 100644
--- a/src/aig/gia/giaSatoko.c
+++ b/src/aig/gia/giaSatoko.c
@@ -45,39 +45,93 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-satoko_t * Gia_ManCreateSatoko( Gia_Man_t * p )
+void Gia_ManCollectVars_rec( int Var, Vec_Int_t * vMapping, Vec_Int_t * vRes, Vec_Bit_t * vVisit )
+{
+ int * pCut, i;
+ if ( Vec_BitEntry(vVisit, Var) )
+ return;
+ Vec_BitWriteEntry(vVisit, Var, 1);
+ if ( Vec_IntEntry(vMapping, Var) ) // primary input or constant 0
+ {
+ pCut = Vec_IntEntryP( vMapping, Vec_IntEntry(vMapping, Var) );
+ for ( i = 1; i <= pCut[0]; i++ )
+ Gia_ManCollectVars_rec( pCut[i], vMapping, vRes, vVisit );
+ }
+ Vec_IntPush( vRes, Var );
+}
+Vec_Int_t * Gia_ManCollectVars( int Root, Vec_Int_t * vMapping, int nVars )
+{
+ Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+ Vec_Bit_t * vVisit = Vec_BitStart( nVars );
+ assert( Vec_IntEntry(vMapping, Root) );
+ Gia_ManCollectVars_rec( Root, vMapping, vRes, vVisit );
+ Vec_BitFree( vVisit );
+ return vRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+satoko_t * Gia_ManSatokoInit( Cnf_Dat_t * pCnf, satoko_opts_t * opts )
{
satoko_t * pSat = satoko_create();
- Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 );
- int i, status;
+ int i;
//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;
}
}
+ satoko_configure(pSat, opts);
+ return pSat;
+}
+void Gia_ManSatokoReport( int iOutput, int status, abctime clk )
+{
+ 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", clk );
+}
+satoko_t * Gia_ManSatokoCreate( Gia_Man_t * p, satoko_opts_t * opts )
+{
+ Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 );
+ satoko_t * pSat = Gia_ManSatokoInit( pCnf, opts );
+ int status = pSat ? satoko_simplify(pSat) : SATOKO_OK;
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 )
+int Gia_ManSatokoCallOne( 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 );
+ pSat = Gia_ManSatokoCreate( p, opts );
if ( pSat )
{
- satoko_configure(pSat, opts);
status = satoko_solve( pSat );
Cost = (unsigned)pSat->stats.n_conflicts;
satoko_destroy( pSat );
@@ -85,37 +139,60 @@ int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
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 );
+ Gia_ManSatokoReport( iOutput, status, Abc_Clock() - clk );
return Cost;
}
-void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit )
+void Gia_ManSatokoCall( Gia_Man_t * p, satoko_opts_t * opts, int fSplit, int fIncrem )
{
+ int fUseCone = 1;
+ Gia_Man_t * pOne;
+ Gia_Obj_t * pRoot;
+ Vec_Int_t * vCone;
+ int i, iLit, status;
+ if ( fIncrem )
+ {
+ abctime clk = Abc_Clock();
+ Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, fUseCone, 0 );
+ satoko_t * pSat = Gia_ManSatokoInit( pCnf, opts );
+ Gia_ManForEachCo( p, pRoot, i )
+ {
+ abctime clk = Abc_Clock();
+ iLit = Abc_Var2Lit( i+1, 0 );
+ satoko_assump_push( pSat, iLit );
+ if ( fUseCone )
+ {
+ vCone = Gia_ManCollectVars( i+1, pCnf->vMapping, pCnf->nVars );
+ satoko_mark_cone( pSat, Vec_IntArray(vCone), Vec_IntSize(vCone) );
+ printf( "Cone has %6d vars (out of %6d). ", Vec_IntSize(vCone), pCnf->nVars );
+ status = satoko_solve( pSat );
+ satoko_unmark_cone( pSat, Vec_IntArray(vCone), Vec_IntSize(vCone) );
+ Vec_IntFree( vCone );
+ }
+ else
+ {
+ status = satoko_solve( pSat );
+ }
+ satoko_assump_pop( pSat );
+ Gia_ManSatokoReport( i, status, Abc_Clock() - clk );
+ }
+ Cnf_DataFree( pCnf );
+ satoko_destroy( pSat );
+ Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
+ return;
+ }
if ( fSplit )
{
- Gia_Man_t * pOne;
- Gia_Obj_t * pRoot;
- int i;
+ abctime clk = Abc_Clock();
Gia_ManForEachCo( p, pRoot, i )
{
pOne = Gia_ManDupDfsCone( p, pRoot );
- Gia_ManCallSatokoOne( pOne, opts, i );
+ Gia_ManSatokoCallOne( pOne, opts, i );
Gia_ManStop( pOne );
}
+ Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
return;
}
- Gia_ManCallSatokoOne( p, opts, -1 );
+ Gia_ManSatokoCallOne( p, opts, -1 );
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f10be02b..bb0b8c8d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -23410,13 +23410,13 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit );
- int c, fSplit = 0;
+ extern void Gia_ManSatokoCall( Gia_Man_t * p, satoko_opts_t * opts, int fSplit, int fIncrem );
+ int c, fSplit = 0, fIncrem = 0;
satoko_opts_t opts;
satoko_default_opts(&opts);
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Csvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Csivh" ) ) != EOF )
{
switch ( c )
{
@@ -23434,6 +23434,9 @@ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
fSplit ^= 1;
break;
+ case 'i':
+ fIncrem ^= 1;
+ break;
case 'v':
opts.verbose ^= 1;
break;
@@ -23449,13 +23452,14 @@ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Satoko(): There is no AIG.\n" );
return 1;
}
- Gia_ManCallSatoko( pAbc->pGia, &opts, fSplit );
+ Gia_ManSatokoCall( pAbc->pGia, &opts, fSplit, fIncrem );
return 0;
usage:
- Abc_Print( -2, "usage: &satoko [-C num] [-svh]\n" );
+ Abc_Print( -2, "usage: &satoko [-C num] [-sivh]\n" );
Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit );
Abc_Print( -2, "\t-s : split multi-output miter into individual outputs [default = %s]\n", fSplit? "yes": "no" );
+ Abc_Print( -2, "\t-i : split multi-output miter and solve incrementally [default = %s]\n", fIncrem? "yes": "no" );
Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/cmd/cmdAuto.c b/src/base/cmd/cmdAuto.c
index e279b19d..8151c2e5 100644
--- a/src/base/cmd/cmdAuto.c
+++ b/src/base/cmd/cmdAuto.c
@@ -47,7 +47,7 @@ ABC_NAMESPACE_IMPL_START
#define CMD_AUTO_LINE_MAX 1000 // max number of chars in the string
#define CMD_AUTO_ARG_MAX 100 // max number of arguments in the call
-extern int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput );
+extern int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -92,7 +92,7 @@ int Cmd_RunAutoTunerEvalSimple( Vec_Ptr_t * vAigs, satoko_opts_t * pOpts )
//printf( "Tuning with options: " );
//Cmd_RunAutoTunerPrintOptions( pOpts );
Vec_PtrForEachEntry( Gia_Man_t *, vAigs, pGia, i )
- TotalCost += Gia_ManCallSatokoOne( pGia, pOpts, -1 );
+ TotalCost += Gia_ManSatokoCallOne( pGia, pOpts, -1 );
return TotalCost;
}
@@ -142,7 +142,7 @@ void * Cmd_RunAutoTunerEvalWorkerThread( void * pArg )
assert( 0 );
return NULL;
}
- pThData->Result = Gia_ManCallSatokoOne( pThData->pGia, pThData->pOpts, -1 );
+ pThData->Result = Gia_ManSatokoCallOne( pThData->pGia, pThData->pOpts, -1 );
pThData->fWorking = 0;
}
assert( 0 );
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index e3134b77..8d55a81c 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -89,6 +89,8 @@ extern void satoko_assump_push(satoko_t *s, unsigned);
extern void satoko_assump_pop(satoko_t *s);
extern int satoko_simplify(satoko_t *);
extern int satoko_solve(satoko_t *);
+extern void satoko_mark_cone(satoko_t *s, int * pvars, int nvars);
+extern void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars);
/* If problem is unsatisfiable under assumptions, this function is used to
* obtain the final conflict clause expressed in the assumptions.
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index cdd3141e..2abc9833 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -190,14 +190,18 @@ static inline unsigned solver_decide(solver_t *s)
if (heap_size(s->var_order) == 0) {
next_var = UNDEF;
return UNDEF;
- } else
- next_var = heap_remove_min(s->var_order);
+ }
+ next_var = heap_remove_min(s->var_order);
+ if (solver_has_marks(s) && !var_mark(s, next_var))
+ next_var = UNDEF;
}
return var2lit(next_var, vec_char_at(s->polarity, next_var));
}
static inline void solver_new_decision(solver_t *s, unsigned lit)
{
+ if (solver_has_marks(s) && !var_mark(s, lit2var(lit)))
+ return;
assert(var_value(s, lit2var(lit)) == VAR_UNASSING);
vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
solver_enqueue(s, lit, UNDEF);
@@ -538,6 +542,8 @@ unsigned solver_propagate(solver_t *s)
n_propagations++;
watch_list_foreach(s->bin_watches, i, p) {
+ if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
+ continue;
if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING)
solver_enqueue(s, i->blocker, i->cref);
else if (lit_value(s, i->blocker) == LIT_FALSE)
@@ -551,6 +557,12 @@ unsigned solver_propagate(solver_t *s)
struct clause *clause;
struct watcher w;
+ if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
+ {
+ *j++ = *i++;
+ continue;
+ }
+
if (lit_value(s, i->blocker) == LIT_TRUE) {
*j++ = *i++;
continue;
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index 849d738a..01912a6e 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -93,6 +93,9 @@ struct solver_t_ {
vec_uint_t *stamps; /* Multipurpose stamp used to calculate LBD and
* clauses minimization with binary resolution */
+ /* Temporary data used for solving cones */
+ vec_char_t *marks;
+
struct satoko_stats stats;
struct satoko_opts opts;
};
@@ -133,6 +136,18 @@ static inline unsigned var_reason(solver_t *s, unsigned var)
{
return vec_uint_at(s->reasons, var);
}
+static inline int var_mark(solver_t *s, unsigned var)
+{
+ return (int)vec_char_at(s->marks, var);
+}
+static inline void var_set_mark(solver_t *s, unsigned var)
+{
+ vec_char_assign(s->marks, var, 1);
+}
+static inline void var_clean_mark(solver_t *s, unsigned var)
+{
+ vec_char_assign(s->marks, var, 0);
+}
//===------------------------------------------------------------------------===
// Inline lit functions
//===------------------------------------------------------------------------===
@@ -185,6 +200,14 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason)
vec_uint_push_back(s->trail, lit);
return SATOKO_OK;
}
+static inline int solver_varnum(solver_t *s)
+{
+ return vec_char_size(s->assigns);
+}
+static inline int solver_has_marks(solver_t *s)
+{
+ return (int)(s->marks != NULL);
+}
//===------------------------------------------------------------------------===
// Inline clause functions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index f3f3d781..b446fb05 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -145,11 +145,13 @@ void satoko_destroy(solver_t *s)
vec_uint_free(s->stack);
vec_uint_free(s->last_dlevel);
vec_uint_free(s->stamps);
+ if (s->marks) vec_char_free(s->marks);
satoko_free(s);
}
void satoko_default_opts(satoko_opts_t *opts)
{
+ memset(opts, 0, sizeof(satoko_opts_t));
opts->verbose = 0;
/* Limits */
opts->conf_limit = 0;
@@ -232,6 +234,7 @@ void satoko_add_variable(solver_t *s, char sign)
vec_uint_push_back(s->stamps, 0);
vec_char_push_back(s->seen, 0);
heap_insert(s->var_order, var);
+ if (s->marks) vec_char_push_back(s->marks, 0);
}
int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
@@ -287,8 +290,8 @@ int satoko_solve(solver_t *s)
char status = SATOKO_UNDEC;
assert(s);
- if (s->opts.verbose)
- print_opts(s);
+ //if (s->opts.verbose)
+ // print_opts(s);
while (status == SATOKO_UNDEC) {
status = solver_search(s);
@@ -317,4 +320,24 @@ satoko_stats_t satoko_stats(satoko_t *s)
return s->stats;
}
+void satoko_mark_cone(satoko_t *s, int * pvars, int nvars)
+{
+ int i;
+ if (!solver_has_marks(s))
+ s->marks = vec_char_init(solver_varnum(s), 0);
+ for (i = 0; i < nvars; i++)
+ {
+ var_set_mark(s, pvars[i]);
+ if (!heap_in_heap(s->var_order, pvars[i]))
+ heap_insert(s->var_order, pvars[i]);
+ }
+}
+void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars)
+{
+ int i;
+ assert(solver_has_marks(s));
+ for (i = 0; i < nvars; i++)
+ var_clean_mark(s, pvars[i]);
+}
+
ABC_NAMESPACE_IMPL_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 08:11:28 +0000