summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--abclib.dsp4
-rw-r--r--src/base/abci/abc.c73
-rw-r--r--src/sat/bmc/module.make1
-rw-r--r--src/sat/bsat/satSolver.c48
-rw-r--r--src/sat/bsat/satSolver.h11
5 files changed, 129 insertions, 8 deletions
diff --git a/abclib.dsp b/abclib.dsp
index b0e82fa8..3e07c5aa 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1819,6 +1819,10 @@ SOURCE=.\src\sat\bmc\bmcChain.c
# End Source File
# Begin Source File
+SOURCE=.\src\sat\bmc\bmcClp.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\sat\bmc\bmcEco.c
# End Source File
# Begin Source File
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 148d8451..83077cb8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -445,6 +445,7 @@ static int Abc_CommandAbc9FFTest ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Qbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenQbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatFx ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SatClp ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Inse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Maxi ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1059,6 +1060,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&qbf", Abc_CommandAbc9Qbf, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&genqbf", Abc_CommandAbc9GenQbf, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satfx", Abc_CommandAbc9SatFx, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&satclp", Abc_CommandAbc9SatClp, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&inse", Abc_CommandAbc9Inse, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&maxi", Abc_CommandAbc9Maxi, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmci", Abc_CommandAbc9Bmci, 0 );
@@ -37120,6 +37122,77 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern int Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fVerbose );
+ int nCubeLim = 1000;
+ int nBTLimit = 1000000;
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "LCvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'L':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nCubeLim = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nCubeLim < 0 )
+ goto usage;
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nBTLimit < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9SatClp(): There is no AIG.\n" );
+ return 0;
+ }
+ Bmc_CollapseOne( pAbc->pGia, nCubeLim, nBTLimit, fVerbose );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &satclp [-LC num] [-vh]\n" );
+ Abc_Print( -2, "\t performs SAT based collapsing\n" );
+ Abc_Print( -2, "\t-L num : the limit on the SOP size of one output [default = %d]\n", nCubeLim );
+ Abc_Print( -2, "\t-C num : the limit on the number of conflicts in one call [default = %d]\n", nBTLimit );
+ Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index 57039320..6d09b15c 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -11,6 +11,7 @@ SRC += src/sat/bmc/bmcBCore.c \
src/sat/bmc/bmcCexMin2.c \
src/sat/bmc/bmcCexTools.c \
src/sat/bmc/bmcChain.c \
+ src/sat/bmc/bmcClp.c \
src/sat/bmc/bmcEco.c \
src/sat/bmc/bmcFault.c \
src/sat/bmc/bmcFx.c \
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 5ea0b348..053b0587 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -556,6 +556,8 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
s->qhead = s->qtail = bound;
veci_resize(&s->trail_lim,level);
+ // update decision level
+ s->iDeciVar = level;
}
static void sat_solver_canceluntil_rollback(sat_solver* s, int NewBound) {
@@ -1156,6 +1158,7 @@ void sat_solver_delete(sat_solver* s)
veci_delete(&s->pivot_vars);
veci_delete(&s->temp_clause);
veci_delete(&s->conf_final);
+ veci_delete(&s->vDeciVars);
// delete arrays
if (s->reasons != 0){
@@ -1577,8 +1580,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
// double var_decay = 0.95;
// double clause_decay = 0.999;
double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
-
- ABC_INT64_T conflictC = 0;
+ int fGuided = (veci_size(&s->vDeciVars) > 0);
+ ABC_INT64_T conflictC = 0;
veci learnt_clause;
int i;
@@ -1591,6 +1594,15 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
// veci_resize(&s->model,0);
veci_new(&learnt_clause);
+ // update variable polarity
+ if ( fGuided )
+ {
+ int * pVars = veci_begin(&s->vDeciVars);
+ for ( i = 0; i < veci_size(&s->vDeciVars); i++ )
+ var_set_polar( s, pVars[i], 0 );
+ s->iDeciVar = 0;
+ }
+
// use activity factors in every even restart
if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
// if ( veci_size(&s->act_vars) > 0 )
@@ -1639,11 +1651,14 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
int next;
// Reached bound on number of conflicts:
- if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
- s->progress_estimate = sat_solver_progress(s);
- sat_solver_canceluntil(s,s->root_level);
- veci_delete(&learnt_clause);
- return l_Undef; }
+ if ( !fGuided )
+ {
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
+ s->progress_estimate = sat_solver_progress(s);
+ sat_solver_canceluntil(s,s->root_level);
+ veci_delete(&learnt_clause);
+ return l_Undef; }
+ }
// Reached bound on number of conflicts:
if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
@@ -1666,7 +1681,24 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
// New variable decision:
s->stats.decisions++;
- next = order_select(s,(float)random_var_freq);
+ if ( fGuided )
+ {
+ int nVars = veci_size(&s->vDeciVars);
+ int * pVars = veci_begin(&s->vDeciVars);
+ next = var_Undef;
+ assert( s->iDeciVar <= nVars );
+ while ( s->iDeciVar < nVars )
+ {
+ int iVar = pVars[s->iDeciVar++];
+ if ( var_value(s, iVar) == varX )
+ {
+ next = iVar;
+ break;
+ }
+ }
+ }
+ else
+ next = order_select(s,(float)random_var_freq);
if (next == var_Undef){
// Model found:
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index d328e6d5..8e171031 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -179,6 +179,9 @@ struct sat_solver_t
// clause store
void * pStore;
int fSolved;
+ // decision variables
+ veci vDeciVars;
+ int iDeciVar;
// trace recording
FILE * pFile;
@@ -223,6 +226,14 @@ static void sat_solver_compress(sat_solver* s)
(void) RetValue;
}
}
+static void sat_solver_prepare_enum(sat_solver* s, int * pVars, int nVars )
+{
+ int v;
+ assert( veci_size(&s->vDeciVars) == 0 );
+ veci_new(&s->vDeciVars);
+ for ( v = 0; v < nVars; v++ )
+ veci_push(&s->vDeciVars,pVars[v]);
+}
static int sat_solver_final(sat_solver* s, int ** ppArray)
{