summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorBruno Schmitt <bruno@oschmitt.com>2017-08-29 09:40:51 +0200
committerBruno Schmitt <bruno@oschmitt.com>2017-08-29 09:40:51 +0200
commitba8112ff3a64d527cf6c8a6c0d9385ca27b52c27 (patch)
treeb8575b157b1019275f5f1da040b18d3c36fd6e11 /src/sat
parentd0f81fcf2952b8a46548c0dd74f95fa1cd0a504f (diff)
downloadabc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.tar.gz
abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.tar.bz2
abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.zip
Fixing bronken C++ build; Satoko internal header, solver.h, should not be used in other packages
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmcBmc.c7
-rw-r--r--src/sat/bmc/bmcBmc2.c11
-rw-r--r--src/sat/bmc/bmcBmc3.c29
-rw-r--r--src/sat/bmc/bmcBmcS.c15
-rw-r--r--src/sat/bmc/bmcMesh.c9
-rw-r--r--src/sat/bmc/bmcMesh2.c7
-rw-r--r--src/sat/satoko/satoko.h21
-rw-r--r--src/sat/satoko/solver.c34
-rw-r--r--src/sat/satoko/solver.h47
-rw-r--r--src/sat/satoko/solver_api.c88
10 files changed, 149 insertions, 119 deletions
diff --git a/src/sat/bmc/bmcBmc.c b/src/sat/bmc/bmcBmc.c
index 8f7452e5..6ab8a92e 100644
--- a/src/sat/bmc/bmcBmc.c
+++ b/src/sat/bmc/bmcBmc.c
@@ -22,7 +22,6 @@
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
#include "bmc.h"
ABC_NAMESPACE_IMPL_START
@@ -190,7 +189,7 @@ int * Sat2_SolverGetModel( satoko_t * p, int * pVars, int nVars )
int i;
pModel = ABC_CALLOC( int, nVars+1 );
for ( i = 0; i < nVars; i++ )
- pModel[i] = solver_read_cex_varvalue(p, pVars[i]);
+ pModel[i] = satoko_read_cex_varvalue(p, pVars[i]);
return pModel;
}
@@ -320,8 +319,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
printf( "Solved %2d outputs of frame %3d. ",
Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
printf( "Conf =%8.0f. Imp =%11.0f. ",
- (double)(pSat ? pSat->stats.conflicts : solver_conflictnum(pSat2)),
- (double)(pSat ? pSat->stats.propagations : satoko_stats(pSat2).n_propagations) );
+ (double)(pSat ? pSat->stats.conflicts : satoko_conflictnum(pSat2)),
+ (double)(pSat ? pSat->stats.propagations : satoko_stats(pSat2)->n_propagations) );
ABC_PRT( "T", Abc_Clock() - clkPart );
clkPart = Abc_Clock();
fflush( stdout );
diff --git a/src/sat/bmc/bmcBmc2.c b/src/sat/bmc/bmcBmc2.c
index 5c2df0d7..f9d65bbb 100644
--- a/src/sat/bmc/bmcBmc2.c
+++ b/src/sat/bmc/bmcBmc2.c
@@ -21,7 +21,6 @@
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
#include "proof/ssw/ssw.h"
#include "bmc.h"
@@ -690,7 +689,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
iVarNum = Saig_BmcSatNum( p, pObjFrm );
if ( iVarNum == 0 )
continue;
- if ( p->pSat2 ? solver_read_cex_varvalue(p->pSat2, iVarNum) : sat_solver_var_value(p->pSat, iVarNum) )
+ if ( p->pSat2 ? satoko_read_cex_varvalue(p->pSat2, iVarNum) : sat_solver_var_value(p->pSat, iVarNum) )
Abc_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i );
}
}
@@ -729,7 +728,7 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
{
if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
continue;
- if ( p->nConfMaxAll && (p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > p->nConfMaxAll )
+ if ( p->nConfMaxAll && (p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > p->nConfMaxAll )
return l_Undef;
VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
@@ -838,7 +837,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
if ( nTimeOut )
{
if ( p->pSat2 )
- solver_set_runtime_limit( p->pSat2, nTimeToStop );
+ satoko_set_runtime_limit( p->pSat2, nTimeToStop );
else
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
}
@@ -867,7 +866,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
{
printf( "%4d : F =%5d. O =%4d. And =%8d. Var =%8d. Conf =%7d. ",
Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars,
- p->pSat ? (int)p->pSat->stats.conflicts : solver_conflictnum(p->pSat2) );
+ p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2) );
printf( "%4.0f MB", 4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
printf( "%9.2f sec", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
printf( "\n" );
@@ -922,7 +921,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
{
if ( p->iFrameLast >= p->nFramesMax )
printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
- else if ( p->nConfMaxAll && (p->pSat ? (int)p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > p->nConfMaxAll )
+ else if ( p->nConfMaxAll && (p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > p->nConfMaxAll )
printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
else if ( nTimeOut && Abc_Clock() > nTimeToStop )
printf( "Reached timeout (%d seconds).\n", nTimeOut );
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 26c93b72..f990a982 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -22,7 +22,6 @@
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
#include "misc/vec/vecHsh.h"
#include "misc/vec/vecWec.h"
#include "bmc.h"
@@ -798,9 +797,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
p->pSat ? p->pSat->nLearntDelta : 0,
p->pSat ? p->pSat->nLearntRatio : 0,
p->pSat ? p->pSat->nDBreduces : 0,
- p->pSat ? sat_solver_nvars(p->pSat) : solver_varnum(p->pSat2),
+ p->pSat ? sat_solver_nvars(p->pSat) : satoko_varnum(p->pSat2),
nUsedVars,
- 100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : solver_varnum(p->pSat2)) );
+ 100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : satoko_varnum(p->pSat2)) );
Abc_Print( 1, "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n",
p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps );
}
@@ -1382,7 +1381,7 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
if ( p->pSat2 )
{
- if ( iLit != ~0 && solver_read_cex_varvalue(p->pSat2, lit_var(iLit)) )
+ if ( iLit != ~0 && satoko_read_cex_varvalue(p->pSat2, lit_var(iLit)) )
Abc_InfoSetBit( pCex->pData, iBit + k );
}
else
@@ -1465,8 +1464,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
}
else
{
- p->pSat2->RunId = p->pPars->RunId;
- p->pSat2->pFuncStop = p->pPars->pFuncStop;
+ satoko_set_runid(p->pSat2, p->pPars->RunId);
+ satoko_set_stop_func(p->pSat2, p->pPars->pFuncStop);
}
if ( pPars->fSolveAll && p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
@@ -1483,7 +1482,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
if ( nTimeToStop )
{
if ( p->pSat2 )
- solver_set_runtime_limit( p->pSat2, nTimeToStop );
+ satoko_set_runtime_limit( p->pSat2, nTimeToStop );
else
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
}
@@ -1614,7 +1613,7 @@ clkOther += Abc_Clock() - clk2;
assert( p->pTime4Outs[i] > 0 );
clkOne = Abc_Clock();
if ( p->pSat2 )
- solver_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() );
+ satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() );
else
sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
}
@@ -1673,8 +1672,8 @@ nTimeSat += clkSatRun;
{
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
- Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : solver_clausenum(p->pSat2)) );
- Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) );
+ Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : satoko_clausenum(p->pSat2)) );
+ Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) );
// Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
// ABC_PRT( "Time", Abc_Clock() - clk );
@@ -1721,7 +1720,7 @@ nTimeSat += clkSatRun;
if ( nTimeToStop )
{
if ( p->pSat2 )
- solver_set_runtime_limit( p->pSat2, nTimeToStop );
+ satoko_set_runtime_limit( p->pSat2, nTimeToStop );
else
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
}
@@ -1738,7 +1737,7 @@ nTimeSat += clkSatRun;
Lit = Saig_ManBmcCreateCnf( p, pObj, f );
if ( p->pSat2 )
{
- if ( solver_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
+ if ( satoko_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
continue;
}
else
@@ -1781,7 +1780,7 @@ nTimeUndec += clkSatRun;
}
if ( pPars->fVerbose )
{
- if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > 1 )
+ if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > 1 )
{
fFirst = 0;
// Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
@@ -1789,8 +1788,8 @@ nTimeUndec += clkSatRun;
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
// Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
- Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : solver_clausenum(p->pSat2)) );
- Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) );
+ Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : satoko_clausenum(p->pSat2)) );
+ Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) );
// Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
if ( pPars->fSolveAll )
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c
index 1bfcd9d0..ea8ec2f6 100644
--- a/src/sat/bmc/bmcBmcS.c
+++ b/src/sat/bmc/bmcBmcS.c
@@ -21,7 +21,6 @@
#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
//#define ABC_USE_EXT_SOLVERS 1
@@ -41,8 +40,8 @@
#define bmc_sat_solver_addclause satoko_add_clause
#define bmc_sat_solver_addvar(s) satoko_add_variable(s, 0)
#define bmc_sat_solver_solve satoko_solve_assumptions
- #define bmc_sat_solver_read_cex_varvalue solver_read_cex_varvalue
- #define bmc_sat_solver_setstop solver_set_stop
+ #define bmc_sat_solver_read_cex_varvalue satoko_read_cex_varvalue
+ #define bmc_sat_solver_setstop satoko_set_stop
#endif
@@ -546,7 +545,7 @@ Cnf_Dat_t * Bmcs_ManAddNewCnf( Bmcs_Man_t * p, int f, int nFramesAdd )
if ( pNew == NULL )
return NULL;
clk = Abc_Clock();
- pCnf = Mf_ManGenerateCnf( pNew, 8, 1, 0, 0, 0 );
+ pCnf = (Cnf_Dat_t *) Mf_ManGenerateCnf( pNew, 8, 1, 0, 0, 0 );
pMap = ABC_FALLOC( int, Gia_ManObjNum(pNew) );
pMap[0] = 0;
Gia_ManForEachObj1( pNew, pObj, i )
@@ -584,10 +583,10 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim
return;
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
#ifndef ABC_USE_EXT_SOLVERS
- Abc_Print( 1, "Var =%8.0f. ", (double)solver_varnum(p->pSats[0]) );
- Abc_Print( 1, "Cla =%9.0f. ", (double)solver_clausenum(p->pSats[0]) );
- Abc_Print( 1, "Learn =%9.0f. ",(double)solver_learntnum(p->pSats[0]) );
- Abc_Print( 1, "Conf =%9.0f. ", (double)solver_conflictnum(p->pSats[0]) );
+ Abc_Print( 1, "Var =%8.0f. ", (double)satoko_varnum(p->pSats[0]) );
+ Abc_Print( 1, "Cla =%9.0f. ", (double)satoko_clausenum(p->pSats[0]) );
+ Abc_Print( 1, "Learn =%9.0f. ",(double)satoko_learntnum(p->pSats[0]) );
+ Abc_Print( 1, "Conf =%9.0f. ", (double)satoko_conflictnum(p->pSats[0]) );
#else
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
Abc_Print( 1, "Cla =%9.0f. ", (double)nClauses );
diff --git a/src/sat/bmc/bmcMesh.c b/src/sat/bmc/bmcMesh.c
index 6da70a1c..ee27496f 100644
--- a/src/sat/bmc/bmcMesh.c
+++ b/src/sat/bmc/bmcMesh.c
@@ -20,7 +20,6 @@
#include "bmc.h"
#include "sat/satoko/satoko.h"
-#include "sat/satoko/solver.h"
ABC_NAMESPACE_IMPL_START
@@ -53,9 +52,9 @@ static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][
***********************************************************************/
static inline int Bmc_MeshVarValue( satoko_t * p, int v )
{
-// int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v);
-// return value == LIT_TRUE;
- return var_polarity(p, v) == LIT_TRUE;
+// int value = var_value(p, v) != SATOKO_VAR_UNASSING ? var_value(p, v) : satoko_var_polarity(p, v);
+// return value == SATOKO_LIT_TRUE;
+ return satoko_var_polarity(p, v) == SATOKO_LIT_TRUE;
}
/**Function*************************************************************
@@ -360,7 +359,7 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
}
printf( "Satisfying solution found. " );
/*
- iVar = solver_varnum(pSat);
+ iVar = satoko_varnum(pSat);
for ( i = 0; i < iVar; i++ )
if ( Bmc_MeshVarValue(pSat, i) )
printf( "%d ", i );
diff --git a/src/sat/bmc/bmcMesh2.c b/src/sat/bmc/bmcMesh2.c
index e6662d7c..1553e5bb 100644
--- a/src/sat/bmc/bmcMesh2.c
+++ b/src/sat/bmc/bmcMesh2.c
@@ -20,7 +20,6 @@
#include "bmc.h"
//#include "sat/satoko/satoko.h"
-//#include "sat/satoko/solver.h"
#include "sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
@@ -56,8 +55,8 @@ static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][
***********************************************************************/
static inline int Bmc_MeshVarValue2( sat_solver * p, int v )
{
-// int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v);
-// return value == LIT_TRUE;
+// int value = var_value(p, v) != SATOKO_VAR_UNASSING ? var_value(p, v) : satoko_var_polarity(p, v);
+// return value == SATOKO_LIT_TRUE;
return sat_solver_var_value( p, v );
}
@@ -370,7 +369,7 @@ void Bmc_MeshTest2( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
}
printf( "Satisfying solution found. " );
/*
-// iVar = solver_varnum(pSat);
+// iVar = satoko_varnum(pSat);
iVar = sat_solver_nvars(pSat);
for ( i = 0; i < iVar; i++ )
if ( Bmc_MeshVarValue2(pSat, i) )
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index 537cc394..5c0de7ad 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -25,6 +25,12 @@ enum {
SATOKO_UNSAT = -1
};
+enum {
+ SATOKO_LIT_FALSE = 1,
+ SATOKO_LIT_TRUE = 0,
+ SATOKO_VAR_UNASSING = 3
+};
+
struct solver_t_;
typedef struct solver_t_ satoko_t;
@@ -120,7 +126,20 @@ extern int satoko_final_conflict(satoko_t *, int **);
* file will not be a DIMACS. (value 1 will use 0 as ID).
*/
extern void satoko_write_dimacs(satoko_t *, char *, int, int);
-extern satoko_stats_t satoko_stats(satoko_t *);
+extern satoko_stats_t * satoko_stats(satoko_t *);
+extern satoko_opts_t * satoko_options(satoko_t *);
+
+extern int satoko_varnum(satoko_t *);
+extern int satoko_clausenum(satoko_t *);
+extern int satoko_learntnum(satoko_t *);
+extern int satoko_conflictnum(satoko_t *);
+extern void satoko_set_stop(satoko_t *, int *);
+extern void satoko_set_stop_func(satoko_t *s, int (*fnct)(int));
+extern void satoko_set_runid(satoko_t *, int);
+extern int satoko_read_cex_varvalue(satoko_t *, int);
+extern abctime satoko_set_runtime_limit(satoko_t *, abctime);
+extern char satoko_var_polarity(satoko_t *, unsigned);
+
ABC_NAMESPACE_HEADER_END
#endif /* satoko__satoko_h */
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index b35574ab..9f5d3424 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -43,8 +43,8 @@ static inline int lit_is_removable(solver_t* s, unsigned lit, unsigned min_level
unsigned *lits = &(c->data[0].lit);
assert(var_reason(s, var) != UNDEF);
- if (c->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) {
- assert(lit_value(s, lits[1]) == LIT_TRUE);
+ if (c->size == 2 && lit_value(s, lits[0]) == SATOKO_LIT_FALSE) {
+ assert(lit_value(s, lits[1]) == SATOKO_LIT_TRUE);
stk_swap(unsigned, lits[0], lits[1]);
}
@@ -117,7 +117,7 @@ static inline void clause_bin_resolution(solver_t *s, vec_uint_t *clause_lits)
watch_list_foreach_bin(s->watches, w, neg_lit) {
unsigned imp_lit = w->blocker;
if (vec_uint_at(s->stamps, lit2var(imp_lit)) == s->cur_stamp &&
- lit_value(s, imp_lit) == LIT_TRUE) {
+ lit_value(s, imp_lit) == SATOKO_LIT_TRUE) {
counter++;
vec_uint_assign(s->stamps, lit2var(imp_lit), (s->cur_stamp - 1));
}
@@ -186,7 +186,7 @@ static inline unsigned solver_decide(solver_t *s)
{
unsigned next_var = UNDEF;
- while (next_var == UNDEF || var_value(s, next_var) != VAR_UNASSING) {
+ while (next_var == UNDEF || var_value(s, next_var) != SATOKO_VAR_UNASSING) {
if (heap_size(s->var_order) == 0) {
next_var = UNDEF;
return UNDEF;
@@ -195,14 +195,14 @@ static inline unsigned solver_decide(solver_t *s)
if (solver_has_marks(s) && !var_mark(s, next_var))
next_var = UNDEF;
}
- return var2lit(next_var, var_polarity(s, next_var));
+ return var2lit(next_var, satoko_var_polarity(s, 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);
+ assert(var_value(s, lit2var(lit)) == SATOKO_VAR_UNASSING);
vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
solver_enqueue(s, lit, UNDEF);
}
@@ -270,8 +270,8 @@ static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt
clause = clause_fetch(s, cref);
lits = &(clause->data[0].lit);
- if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) {
- assert(lit_value(s, lits[1]) == LIT_TRUE);
+ if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == SATOKO_LIT_FALSE) {
+ assert(lit_value(s, lits[1]) == SATOKO_LIT_TRUE);
stk_swap(unsigned, lits[0], lits[1] );
}
@@ -522,7 +522,7 @@ void solver_cancel_until(solver_t *s, unsigned level)
unsigned var = lit2var(vec_uint_at(s->trail, i));
vec_char_assign(s->polarity, var, vec_char_at(s->assigns, var));
- vec_char_assign(s->assigns, var, VAR_UNASSING);
+ vec_char_assign(s->assigns, var, SATOKO_VAR_UNASSING);
vec_uint_assign(s->reasons, var, UNDEF);
if (!heap_in_heap(s->var_order, var))
heap_insert(s->var_order, var);
@@ -550,9 +550,9 @@ unsigned solver_propagate(solver_t *s)
watch_list_foreach_bin(s->watches, i, p) {
if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
continue;
- if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING)
+ if (var_value(s, lit2var(i->blocker)) == SATOKO_VAR_UNASSING)
solver_enqueue(s, i->blocker, i->cref);
- else if (lit_value(s, i->blocker) == LIT_FALSE)
+ else if (lit_value(s, i->blocker) == SATOKO_LIT_FALSE)
return i->cref;
}
@@ -567,7 +567,7 @@ unsigned solver_propagate(solver_t *s)
*j++ = *i++;
continue;
}
- if (lit_value(s, i->blocker) == LIT_TRUE) {
+ if (lit_value(s, i->blocker) == SATOKO_LIT_TRUE) {
*j++ = *i++;
continue;
}
@@ -585,13 +585,13 @@ unsigned solver_propagate(solver_t *s)
w.blocker = lits[0];
/* If 0th watch is true, then clause is already satisfied. */
- if (lits[0] != i->blocker && lit_value(s, lits[0]) == LIT_TRUE)
+ if (lits[0] != i->blocker && lit_value(s, lits[0]) == SATOKO_LIT_TRUE)
*j++ = w;
else {
/* Look for new watch */
unsigned k;
for (k = 2; k < clause->size; k++) {
- if (lit_value(s, lits[k]) != LIT_FALSE) {
+ if (lit_value(s, lits[k]) != SATOKO_LIT_FALSE) {
lits[1] = lits[k];
lits[k] = neg_lit;
watch_list_push(vec_wl_at(s->watches, lit_compl(lits[1])), w, 0);
@@ -602,7 +602,7 @@ unsigned solver_propagate(solver_t *s)
*j++ = w;
/* Clause becomes unit under this assignment */
- if (lit_value(s, lits[0]) == LIT_FALSE) {
+ if (lit_value(s, lits[0]) == SATOKO_LIT_FALSE) {
conf_cref = i->cref;
s->i_qhead = vec_uint_size(s->trail);
i++;
@@ -665,9 +665,9 @@ char solver_search(solver_t *s)
next_lit = UNDEF;
while (solver_dlevel(s) < vec_uint_size(s->assumptions)) {
unsigned lit = vec_uint_at(s->assumptions, solver_dlevel(s));
- if (lit_value(s, lit) == LIT_TRUE) {
+ if (lit_value(s, lit) == SATOKO_LIT_TRUE) {
vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
- } else if (lit_value(s, lit) == LIT_FALSE) {
+ } else if (lit_value(s, lit) == SATOKO_LIT_FALSE) {
solver_analyze_final(s, lit_compl(lit));
return SATOKO_UNSAT;
} else {
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index ee7b84e2..1a20632f 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -30,11 +30,7 @@
#include "misc/util/abc_global.h"
ABC_NAMESPACE_HEADER_START
-enum {
- LIT_FALSE = 1,
- LIT_TRUE = 0,
- VAR_UNASSING = 3
-};
+
#define UNDEF 0xFFFFFFFF
@@ -145,11 +141,6 @@ static inline char var_value(solver_t *s, unsigned var)
return vec_char_at(s->assigns, var);
}
-static inline char var_polarity(solver_t *s, unsigned var)
-{
- return vec_char_at(s->polarity, var);
-}
-
static inline unsigned var_dlevel(solver_t *s, unsigned var)
{
return vec_uint_at(s->levels, var);
@@ -226,45 +217,15 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason)
return SATOKO_OK;
}
-static inline int solver_varnum(solver_t *s)
-{
- return vec_char_size(s->assigns);
-}
-static inline int solver_clausenum(solver_t *s)
-{
- return vec_uint_size(s->originals);
-}
-static inline int solver_learntnum(solver_t *s)
-{
- return vec_uint_size(s->learnts);
-}
-static inline int solver_conflictnum(solver_t *s)
-{
- return satoko_stats(s).n_conflicts;
-}
-
-static inline int solver_has_marks(solver_t *s)
+static inline int solver_has_marks(satoko_t *s)
{
return (int)(s->marks != NULL);
}
-static inline int solver_stop(solver_t *s)
+
+static inline int solver_stop(satoko_t *s)
{
return s->pstop && *s->pstop;
}
-static inline void solver_set_stop(solver_t *s, int * pstop)
-{
- s->pstop = pstop;
-}
-static inline int solver_read_cex_varvalue(solver_t *s, int ivar)
-{
- return var_polarity(s, ivar) == LIT_TRUE;
-}
-static abctime solver_set_runtime_limit(solver_t* s, abctime Limit)
-{
- abctime nRuntimeLimit = s->nRuntimeLimit;
- s->nRuntimeLimit = Limit;
- return nRuntimeLimit;
-}
//===------------------------------------------------------------------------===
// Inline clause functions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 0d073ec7..837d64e7 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -27,7 +27,7 @@ static inline void solver_rebuild_order(solver_t *s)
vec_uint_t *vars = vec_uint_alloc(vec_char_size(s->assigns));
for (var = 0; var < vec_char_size(s->assigns); var++)
- if (var_value(s, var) == VAR_UNASSING)
+ if (var_value(s, var) == SATOKO_VAR_UNASSING)
vec_uint_push_back(vars, var);
heap_build(s->var_order, vars);
vec_uint_free(vars);
@@ -38,7 +38,7 @@ static inline int clause_is_satisfied(solver_t *s, struct clause *clause)
unsigned i;
unsigned *lits = &(clause->data[0].lit);
for (i = 0; i < clause->size; i++)
- if (lit_value(s, lits[i]) == LIT_TRUE)
+ if (lit_value(s, lits[i]) == SATOKO_LIT_TRUE)
return SATOKO_OK;
return SATOKO_ERR;
}
@@ -226,7 +226,7 @@ int satoko_simplify(solver_t * s)
void satoko_setnvars(solver_t *s, int nvars)
{
int i;
- for (i = solver_varnum(s); i < nvars; i++)
+ for (i = satoko_varnum(s); i < nvars; i++)
satoko_add_variable(s, 0);
}
@@ -237,7 +237,7 @@ int satoko_add_variable(solver_t *s, char sign)
vec_wl_push(s->watches);
vec_act_push_back(s->activity, 0);
vec_uint_push_back(s->levels, 0);
- vec_char_push_back(s->assigns, VAR_UNASSING);
+ vec_char_push_back(s->assigns, SATOKO_VAR_UNASSING);
vec_char_push_back(s->polarity, sign);
vec_uint_push_back(s->reasons, UNDEF);
vec_uint_push_back(s->stamps, 0);
@@ -258,15 +258,15 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
qsort((void *) lits, size, sizeof(unsigned), stk_uint_compare);
max_var = lit2var(lits[size - 1]);
while (max_var >= vec_act_size(s->activity))
- satoko_add_variable(s, LIT_FALSE);
+ satoko_add_variable(s, SATOKO_LIT_FALSE);
vec_uint_clear(s->temp_lits);
j = 0;
prev_lit = UNDEF;
for (i = 0; i < (unsigned)size; i++) {
- if ((unsigned)lits[i] == lit_compl(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE)
+ if ((unsigned)lits[i] == lit_compl(prev_lit) || lit_value(s, lits[i]) == SATOKO_LIT_TRUE)
return SATOKO_OK;
- else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == VAR_UNASSING) {
+ else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == SATOKO_VAR_UNASSING) {
prev_lit = lits[i];
vec_uint_push_back(s->temp_lits, lits[i]);
}
@@ -287,7 +287,7 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
void satoko_assump_push(solver_t *s, int lit)
{
- assert(lit2var(lit) < solver_varnum(s));
+ assert(lit2var(lit) < satoko_varnum(s));
// printf("[Satoko] Push assumption: %d\n", lit);
vec_uint_push_back(s->assumptions, lit);
}
@@ -337,8 +337,8 @@ int satoko_solve_assumptions(solver_t *s, int * plits, int nlits)
{
int i, status;
// printf("\n[Satoko] Solve with assumptions.. (%d)\n", vec_uint_size(s->assumptions));
- // printf("[Satoko] + Variables: %d\n", solver_varnum(s));
- // printf("[Satoko] + Clauses: %d\n", solver_clausenum(s));
+ // printf("[Satoko] + Variables: %d\n", satoko_varnum(s));
+ // printf("[Satoko] + Clauses: %d\n", satoko_clausenum(s));
// printf("[Satoko] + Trail size: %d\n", vec_uint_size(s->trail));
// printf("[Satoko] + Queue head: %d\n", s->i_qhead);
// solver_debug_check_trail(s);
@@ -365,9 +365,14 @@ int satoko_final_conflict(solver_t *s, int **out)
return vec_uint_size(s->final_conflict);
}
-satoko_stats_t satoko_stats(satoko_t *s)
+satoko_stats_t * satoko_stats(satoko_t *s)
{
- return s->stats;
+ return &s->stats;
+}
+
+satoko_opts_t * satoko_options(satoko_t *s)
+{
+ return &s->opts;
}
void satoko_bookmark(satoko_t *s)
@@ -493,7 +498,7 @@ void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars)
{
int i;
if (!solver_has_marks(s))
- s->marks = vec_char_init(solver_varnum(s), 0);
+ s->marks = vec_char_init(satoko_varnum(s), 0);
for (i = 0; i < n_vars; i++) {
var_set_mark(s, pvars[i]);
vec_sdbl_assign(s->activity, pvars[i], 0);
@@ -532,11 +537,11 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
}
fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
for (i = 0; i < vec_char_size(s->assigns); i++) {
- if ( var_value(s, i) != VAR_UNASSING ) {
+ if ( var_value(s, i) != SATOKO_VAR_UNASSING ) {
if (zero_var)
- fprintf(file, "%d\n", var_value(s, i) == LIT_FALSE ? -(int)(i) : i);
+ fprintf(file, "%d\n", var_value(s, i) == SATOKO_LIT_FALSE ? -(int)(i) : i);
else
- fprintf(file, "%d 0\n", var_value(s, i) == LIT_FALSE ? -(int)(i + 1) : i + 1);
+ fprintf(file, "%d 0\n", var_value(s, i) == SATOKO_LIT_FALSE ? -(int)(i + 1) : i + 1);
}
}
array = vec_uint_data(s->originals);
@@ -552,5 +557,56 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
}
+int satoko_varnum(satoko_t *s)
+{
+ return vec_char_size(s->assigns);
+}
+
+int satoko_clausenum(satoko_t *s)
+{
+ return vec_uint_size(s->originals);
+}
+
+int satoko_learntnum(satoko_t *s)
+{
+ return vec_uint_size(s->learnts);
+}
+
+int satoko_conflictnum(satoko_t *s)
+{
+ return satoko_stats(s)->n_conflicts;
+}
+
+void satoko_set_stop(satoko_t *s, int * pstop)
+{
+ s->pstop = pstop;
+}
+
+void satoko_set_stop_func(satoko_t *s, int (*fnct)(int))
+{
+ s->pFuncStop = fnct;
+}
+
+void satoko_set_runid(satoko_t *s, int id)
+{
+ s->RunId = id;
+}
+
+int satoko_read_cex_varvalue(satoko_t *s, int ivar)
+{
+ return satoko_var_polarity(s, ivar) == SATOKO_LIT_TRUE;
+}
+
+abctime satoko_set_runtime_limit(satoko_t* s, abctime Limit)
+{
+ abctime nRuntimeLimit = s->nRuntimeLimit;
+ s->nRuntimeLimit = Limit;
+ return nRuntimeLimit;
+}
+
+char satoko_var_polarity(satoko_t *s, unsigned var)
+{
+ return vec_char_at(s->polarity, var);
+}
ABC_NAMESPACE_IMPL_END