mirror of https://github.com/YosysHQ/abc.git
Adding and integrating new SAT solver APIs.
This commit is contained in:
Alan Mishchenko
parent
38d72c4343
commit
22388f901a
|
|
@ -36290,6 +36290,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
|
||||
int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0;
|
||||
Cec_ManFraSetDefaultParams( pPars );
|
||||
pPars->jType = 0; // solver type
|
||||
pPars->fSatSweeping = 1; // conflict limit at a node
|
||||
pPars->nWords = 4; // simulation words
|
||||
pPars->nRounds = 250; // simulation rounds
|
||||
|
|
@ -36299,10 +36300,21 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver
|
||||
pPars->nGenIters = 5; // pattern generation iterations
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCPrmdckngxwvh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCPrmdckngxwvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'J':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->jType = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->jType < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'W':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
|
|
@ -36431,8 +36443,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &fraig [-WRILDCP <num>] [-rmdckngwvh]\n" );
|
||||
Abc_Print( -2, "usage: &fraig [-JWRILDCP <num>] [-rmdckngwvh]\n" );
|
||||
Abc_Print( -2, "\t performs combinational SAT sweeping\n" );
|
||||
Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType );
|
||||
Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
|
||||
Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
|
||||
Abc_Print( -2, "\t-I num : the number of sweeping iterations [default = %d]\n", pPars->nItersMax );
|
||||
|
|
|
|||
|
|
@ -95,6 +95,7 @@ struct Cec_ParSmf_t_
|
|||
typedef struct Cec_ParFra_t_ Cec_ParFra_t;
|
||||
struct Cec_ParFra_t_
|
||||
{
|
||||
int jType; // solver type
|
||||
int nWords; // the number of simulation words
|
||||
int nRounds; // the number of simulation rounds
|
||||
int nItersMax; // the maximum number of iterations of SAT sweeping
|
||||
|
|
|
|||
|
|
@ -28,33 +28,45 @@
|
|||
|
||||
#include "sat/glucose2/AbcGlucose2.h"
|
||||
|
||||
#define sat_solver bmcg2_sat_solver
|
||||
#define sat_solver_start bmcg2_sat_solver_start
|
||||
#define sat_solver_stop bmcg2_sat_solver_stop
|
||||
#define sat_solver_addclause bmcg2_sat_solver_addclause
|
||||
#define sat_solver_addvar bmcg2_sat_solver_addvar
|
||||
#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
|
||||
#define sat_solver_reset bmcg2_sat_solver_reset
|
||||
#define sat_solver_set_conflict_budget bmcg2_sat_solver_set_conflict_budget
|
||||
#define sat_solver_conflictnum bmcg2_sat_solver_conflictnum
|
||||
#define sat_solver_solve bmcg2_sat_solver_solve
|
||||
#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
|
||||
#define sat_solver bmcg2_sat_solver
|
||||
#define sat_solver_start bmcg2_sat_solver_start
|
||||
#define sat_solver_stop bmcg2_sat_solver_stop
|
||||
#define sat_solver_addclause bmcg2_sat_solver_addclause
|
||||
#define sat_solver_addvar bmcg2_sat_solver_addvar
|
||||
#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
|
||||
#define sat_solver_reset bmcg2_sat_solver_reset
|
||||
#define sat_solver_set_conflict_budget bmcg2_sat_solver_set_conflict_budget
|
||||
#define sat_solver_conflictnum bmcg2_sat_solver_conflictnum
|
||||
#define sat_solver_solve bmcg2_sat_solver_solve
|
||||
#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
|
||||
#define sat_solver_read_cex bmcg2_sat_solver_read_cex
|
||||
#define sat_solver_jftr bmcg2_sat_solver_jftr
|
||||
#define sat_solver_set_jftr bmcg2_sat_solver_set_jftr
|
||||
#define sat_solver_set_var_fanin_lit bmcg2_sat_solver_set_var_fanin_lit
|
||||
#define sat_solver_start_new_round bmcg2_sat_solver_start_new_round
|
||||
#define sat_solver_mark_cone bmcg2_sat_solver_mark_cone
|
||||
|
||||
#else
|
||||
|
||||
#include "sat/glucose/AbcGlucose.h"
|
||||
|
||||
#define sat_solver bmcg_sat_solver
|
||||
#define sat_solver_start bmcg_sat_solver_start
|
||||
#define sat_solver_stop bmcg_sat_solver_stop
|
||||
#define sat_solver_addclause bmcg_sat_solver_addclause
|
||||
#define sat_solver_addvar bmcg_sat_solver_addvar
|
||||
#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
|
||||
#define sat_solver_reset bmcg_sat_solver_reset
|
||||
#define sat_solver_set_conflict_budget bmcg_sat_solver_set_conflict_budget
|
||||
#define sat_solver_conflictnum bmcg_sat_solver_conflictnum
|
||||
#define sat_solver_solve bmcg_sat_solver_solve
|
||||
#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
|
||||
#define sat_solver bmcg_sat_solver
|
||||
#define sat_solver_start bmcg_sat_solver_start
|
||||
#define sat_solver_stop bmcg_sat_solver_stop
|
||||
#define sat_solver_addclause bmcg_sat_solver_addclause
|
||||
#define sat_solver_addvar bmcg_sat_solver_addvar
|
||||
#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
|
||||
#define sat_solver_reset bmcg_sat_solver_reset
|
||||
#define sat_solver_set_conflict_budget bmcg_sat_solver_set_conflict_budget
|
||||
#define sat_solver_conflictnum bmcg_sat_solver_conflictnum
|
||||
#define sat_solver_solve bmcg_sat_solver_solve
|
||||
#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
|
||||
#define sat_solver_read_cex bmcg_sat_solver_read_cex
|
||||
#define sat_solver_jftr bmcg_sat_solver_jftr
|
||||
#define sat_solver_set_jftr bmcg_sat_solver_set_jftr
|
||||
#define sat_solver_set_var_fanin_lit bmcg_sat_solver_set_var_fanin_lit
|
||||
#define sat_solver_start_new_round bmcg_sat_solver_start_new_round
|
||||
#define sat_solver_mark_cone bmcg_sat_solver_mark_cone
|
||||
|
||||
#endif
|
||||
|
||||
|
|
@ -134,7 +146,8 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
|
|||
p->timeStart = Abc_Clock();
|
||||
p->pPars = pPars;
|
||||
p->pAig = pAig;
|
||||
p->pSat = sat_solver_start();
|
||||
p->pSat = sat_solver_start();
|
||||
sat_solver_set_jftr( p->pSat, pPars->jType );
|
||||
p->vFrontier = Vec_PtrAlloc( 1000 );
|
||||
p->vFanins = Vec_PtrAlloc( 100 );
|
||||
p->vCexMin = Vec_IntAlloc( 100 );
|
||||
|
|
@ -422,11 +435,19 @@ int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
|
|||
{
|
||||
Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) );
|
||||
Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) );
|
||||
Vec_PtrClear( p->vFanins );
|
||||
Vec_PtrPush( p->vFanins, Gia_ObjChild0(pObj) );
|
||||
Vec_PtrPush( p->vFanins, Gia_ObjChild1(pObj) );
|
||||
Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
|
||||
Cec4_AddClausesSuper( p->pNew, pObj, p->vFanins, p->pSat );
|
||||
if( sat_solver_jftr( p->pSat ) < 2 )
|
||||
{
|
||||
Vec_PtrClear( p->vFanins );
|
||||
Vec_PtrPush( p->vFanins, Gia_ObjChild0(pObj) );
|
||||
Vec_PtrPush( p->vFanins, Gia_ObjChild1(pObj) );
|
||||
Cec4_AddClausesSuper( p->pNew, pObj, p->vFanins, p->pSat );
|
||||
}
|
||||
if( 0 < sat_solver_jftr( p->pSat ) )
|
||||
sat_solver_set_var_fanin_lit( p->pSat\
|
||||
, Cec4_ObjSatId( p->pNew, pObj )\
|
||||
, Abc_Var2Lit( Cec4_ObjSatId( p->pNew, Gia_ObjFanin0(pObj) ), Gia_ObjFaninC0(pObj) )\
|
||||
, Abc_Var2Lit( Cec4_ObjSatId( p->pNew, Gia_ObjFanin1(pObj) ), Gia_ObjFaninC1(pObj) ) );
|
||||
return Cec4_ObjSatId( p->pNew, pObj );
|
||||
}
|
||||
// start the frontier
|
||||
|
|
@ -1064,6 +1085,12 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
|
|||
clk = Abc_Clock();
|
||||
iVar0 = Cec4_ObjGetCnfVar( p, iObj0 );
|
||||
iVar1 = Cec4_ObjGetCnfVar( p, iObj1 );
|
||||
if( sat_solver_jftr( p->pSat ) )
|
||||
{
|
||||
sat_solver_start_new_round( p->pSat );
|
||||
sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj0)) );
|
||||
sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj1)) );
|
||||
}
|
||||
p->timeCnf += Abc_Clock() - clk;
|
||||
// perform solving
|
||||
Lits[0] = Abc_Var2Lit(iVar0, 1);
|
||||
|
|
@ -1135,20 +1162,35 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
|
|||
int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
|
||||
{
|
||||
abctime clk = Abc_Clock();
|
||||
int i, IdAig, IdSat, status, fEasy, RetValue = 1;
|
||||
int i, iLit, IdAig, IdSat, status, fEasy, RetValue = 1;
|
||||
Gia_Obj_t * pObj = Gia_ManObj( p->pAig, iObj );
|
||||
Gia_Obj_t * pRepr = Gia_ManObj( p->pAig, iRepr );
|
||||
int fCompl = Abc_LitIsCompl(pObj->Value) ^ Abc_LitIsCompl(pRepr->Value) ^ pObj->fPhase ^ pRepr->fPhase;
|
||||
status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose );
|
||||
if ( status == GLUCOSE_SAT )
|
||||
{
|
||||
int * pCex;
|
||||
//printf( "Disproved: %d == %d.\n", Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value) );
|
||||
p->nSatSat++;
|
||||
p->nPatterns++;
|
||||
p->pAig->iPatsPi++;
|
||||
assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
|
||||
Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
|
||||
Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
|
||||
//Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
|
||||
// Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
|
||||
pCex = sat_solver_read_cex( p->pSat );
|
||||
Vec_IntClear( p->vPat );
|
||||
if ( pCex == NULL )
|
||||
{
|
||||
Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
|
||||
Vec_IntPush( p->vPat, Abc_Var2Lit(IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat)) );
|
||||
}
|
||||
else
|
||||
{
|
||||
for ( i = 0; i < pCex[0]; )
|
||||
Vec_IntPush( p->vPat, Abc_LitNot(pCex[++i]) );
|
||||
}
|
||||
Vec_IntForEachEntry( p->vPat, iLit, i )
|
||||
Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
|
||||
if ( fEasy )
|
||||
p->timeSatSat0 += Abc_Clock() - clk;
|
||||
else
|
||||
|
|
|
|||
|
|
@ -326,6 +326,32 @@ int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1
|
|||
return 1;
|
||||
}
|
||||
|
||||
int bmcg_sat_solver_jftr(bmcg_sat_solver* s)
|
||||
{
|
||||
return ((Gluco::SimpSolver*)s)->jftr;
|
||||
}
|
||||
|
||||
void bmcg_sat_solver_set_jftr(bmcg_sat_solver* s, int jftr)
|
||||
{
|
||||
((Gluco::SimpSolver*)s)->jftr = jftr;
|
||||
}
|
||||
|
||||
void bmcg_sat_solver_set_var_fanin_lit(bmcg_sat_solver* s, int var, int lit0, int lit1)
|
||||
{
|
||||
((Gluco::SimpSolver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1);
|
||||
}
|
||||
|
||||
void bmcg_sat_solver_start_new_round(bmcg_sat_solver* s)
|
||||
{
|
||||
((Gluco::SimpSolver*)s)->sat_solver_start_new_round();
|
||||
}
|
||||
|
||||
void bmcg_sat_solver_mark_cone(bmcg_sat_solver* s, int var)
|
||||
{
|
||||
((Gluco::SimpSolver*)s)->sat_solver_mark_cone(var);
|
||||
}
|
||||
|
||||
|
||||
#else
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
@ -351,6 +377,11 @@ void glucose_solver_stop(Gluco::Solver* S)
|
|||
delete S;
|
||||
}
|
||||
|
||||
void glucose_solver_reset(Gluco::Solver* S)
|
||||
{
|
||||
S->reset();
|
||||
}
|
||||
|
||||
int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits)
|
||||
{
|
||||
vec<Lit> lits;
|
||||
|
|
@ -427,6 +458,10 @@ void bmcg_sat_solver_stop(bmcg_sat_solver* s)
|
|||
{
|
||||
glucose_solver_stop((Gluco::Solver*)s);
|
||||
}
|
||||
void bmcg_sat_solver_reset(bmcg_sat_solver* s)
|
||||
{
|
||||
glucose_solver_reset((Gluco::Solver*)s);
|
||||
}
|
||||
|
||||
int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits)
|
||||
{
|
||||
|
|
@ -575,6 +610,54 @@ int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int
|
|||
return nresL + nresR;
|
||||
}
|
||||
|
||||
int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
|
||||
{
|
||||
int Lits[3];
|
||||
|
||||
Lits[0] = Abc_Var2Lit( iVar, !fCompl );
|
||||
Lits[1] = Abc_Var2Lit( iVar0, fCompl0 );
|
||||
if ( !bmcg_sat_solver_addclause( s, Lits, 2 ) )
|
||||
return 0;
|
||||
|
||||
Lits[0] = Abc_Var2Lit( iVar, !fCompl );
|
||||
Lits[1] = Abc_Var2Lit( iVar1, fCompl1 );
|
||||
if ( !bmcg_sat_solver_addclause( s, Lits, 2 ) )
|
||||
return 0;
|
||||
|
||||
Lits[0] = Abc_Var2Lit( iVar, fCompl );
|
||||
Lits[1] = Abc_Var2Lit( iVar0, !fCompl0 );
|
||||
Lits[2] = Abc_Var2Lit( iVar1, !fCompl1 );
|
||||
if ( !bmcg_sat_solver_addclause( s, Lits, 3 ) )
|
||||
return 0;
|
||||
|
||||
return 1;
|
||||
}
|
||||
|
||||
int bmcg_sat_solver_jftr(bmcg_sat_solver* s)
|
||||
{
|
||||
return ((Gluco::Solver*)s)->jftr;
|
||||
}
|
||||
|
||||
void bmcg_sat_solver_set_jftr(bmcg_sat_solver* s, int jftr)
|
||||
{
|
||||
((Gluco::Solver*)s)->jftr = jftr;
|
||||
}
|
||||
|
||||
void bmcg_sat_solver_set_var_fanin_lit(bmcg_sat_solver* s, int var, int lit0, int lit1)
|
||||
{
|
||||
((Gluco::Solver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1);
|
||||
}
|
||||
|
||||
void bmcg_sat_solver_start_new_round(bmcg_sat_solver* s)
|
||||
{
|
||||
((Gluco::Solver*)s)->sat_solver_start_new_round();
|
||||
}
|
||||
|
||||
void bmcg_sat_solver_mark_cone(bmcg_sat_solver* s, int var)
|
||||
{
|
||||
((Gluco::Solver*)s)->sat_solver_mark_cone(var);
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -97,6 +97,12 @@ extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar,
|
|||
extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits );
|
||||
extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv );
|
||||
extern Vec_Str_t * bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit );
|
||||
extern int bmcg_sat_solver_jftr( bmcg_sat_solver * s );
|
||||
extern void bmcg_sat_solver_set_jftr( bmcg_sat_solver * s, int jftr );
|
||||
extern void bmcg_sat_solver_set_var_fanin_lit( bmcg_sat_solver * s, int var, int lit0, int lit1 );
|
||||
extern void bmcg_sat_solver_start_new_round( bmcg_sat_solver * s );
|
||||
extern void bmcg_sat_solver_mark_cone( bmcg_sat_solver * s, int var );
|
||||
|
||||
|
||||
extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars );
|
||||
extern int Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars );
|
||||
|
|
|
|||
|
|
@ -64,6 +64,12 @@ public:
|
|||
vec<int> user_vec;
|
||||
vec<Lit> user_lits;
|
||||
|
||||
// circuit-based solving
|
||||
int jftr;
|
||||
void sat_solver_set_var_fanin_lit(int, int, int);
|
||||
void sat_solver_start_new_round();
|
||||
void sat_solver_mark_cone(int);
|
||||
|
||||
// Problem specification:
|
||||
//
|
||||
Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
|
||||
|
|
@ -457,6 +463,10 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ v
|
|||
|
||||
inline void Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
|
||||
|
||||
inline void Solver::sat_solver_set_var_fanin_lit(int var, int lit0, int lit1) {}
|
||||
inline void Solver::sat_solver_start_new_round() {}
|
||||
inline void Solver::sat_solver_mark_cone(int var) {}
|
||||
|
||||
//=================================================================================================
|
||||
// Debug etc:
|
||||
|
||||
|
|
|
|||
|
|
@ -326,6 +326,31 @@ int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVa
|
|||
return 1;
|
||||
}
|
||||
|
||||
int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s)
|
||||
{
|
||||
return ((Gluco2::SimpSolver*)s)->jftr;
|
||||
}
|
||||
|
||||
void bmcg2_sat_solver_set_jftr(bmcg2_sat_solver* s, int jftr)
|
||||
{
|
||||
((Gluco2::SimpSolver*)s)->jftr = jftr;
|
||||
}
|
||||
|
||||
void bmcg2_sat_solver_set_var_fanin_lit(bmcg2_sat_solver* s, int var, int lit0, int lit1)
|
||||
{
|
||||
((Gluco2::SimpSolver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1);
|
||||
}
|
||||
|
||||
void bmcg2_sat_solver_start_new_round(bmcg2_sat_solver* s)
|
||||
{
|
||||
((Gluco2::SimpSolver*)s)->sat_solver_start_new_round();
|
||||
}
|
||||
|
||||
void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var)
|
||||
{
|
||||
((Gluco2::SimpSolver*)s)->sat_solver_mark_cone(var);
|
||||
}
|
||||
|
||||
#else
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
@ -351,6 +376,11 @@ void glucose2_solver_stop(Gluco2::Solver* S)
|
|||
delete S;
|
||||
}
|
||||
|
||||
void glucose2_solver_reset(Gluco2::Solver* S)
|
||||
{
|
||||
S->reset();
|
||||
}
|
||||
|
||||
int glucose2_solver_addclause(Gluco2::Solver* S, int * plits, int nlits)
|
||||
{
|
||||
vec<Lit> lits;
|
||||
|
|
@ -427,6 +457,10 @@ void bmcg2_sat_solver_stop(bmcg2_sat_solver* s)
|
|||
{
|
||||
glucose2_solver_stop((Gluco2::Solver*)s);
|
||||
}
|
||||
void bmcg2_sat_solver_reset(bmcg2_sat_solver* s)
|
||||
{
|
||||
glucose2_solver_reset((Gluco2::Solver*)s);
|
||||
}
|
||||
|
||||
int bmcg2_sat_solver_addclause(bmcg2_sat_solver* s, int * plits, int nlits)
|
||||
{
|
||||
|
|
@ -575,6 +609,54 @@ int bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, in
|
|||
return nresL + nresR;
|
||||
}
|
||||
|
||||
int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
|
||||
{
|
||||
int Lits[3];
|
||||
|
||||
Lits[0] = Abc_Var2Lit( iVar, !fCompl );
|
||||
Lits[1] = Abc_Var2Lit( iVar0, fCompl0 );
|
||||
if ( !bmcg2_sat_solver_addclause( s, Lits, 2 ) )
|
||||
return 0;
|
||||
|
||||
Lits[0] = Abc_Var2Lit( iVar, !fCompl );
|
||||
Lits[1] = Abc_Var2Lit( iVar1, fCompl1 );
|
||||
if ( !bmcg2_sat_solver_addclause( s, Lits, 2 ) )
|
||||
return 0;
|
||||
|
||||
Lits[0] = Abc_Var2Lit( iVar, fCompl );
|
||||
Lits[1] = Abc_Var2Lit( iVar0, !fCompl0 );
|
||||
Lits[2] = Abc_Var2Lit( iVar1, !fCompl1 );
|
||||
if ( !bmcg2_sat_solver_addclause( s, Lits, 3 ) )
|
||||
return 0;
|
||||
|
||||
return 1;
|
||||
}
|
||||
|
||||
int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s)
|
||||
{
|
||||
return ((Gluco2::Solver*)s)->jftr;
|
||||
}
|
||||
|
||||
void bmcg2_sat_solver_set_jftr(bmcg2_sat_solver* s, int jftr)
|
||||
{
|
||||
((Gluco2::Solver*)s)->jftr = jftr;
|
||||
}
|
||||
|
||||
void bmcg2_sat_solver_set_var_fanin_lit(bmcg2_sat_solver* s, int var, int lit0, int lit1)
|
||||
{
|
||||
((Gluco2::Solver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1);
|
||||
}
|
||||
|
||||
void bmcg2_sat_solver_start_new_round(bmcg2_sat_solver* s)
|
||||
{
|
||||
((Gluco2::Solver*)s)->sat_solver_start_new_round();
|
||||
}
|
||||
|
||||
void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var)
|
||||
{
|
||||
((Gluco2::Solver*)s)->sat_solver_mark_cone(var);
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -97,6 +97,11 @@ extern int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVa
|
|||
extern int bmcg2_sat_solver_quantify( bmcg2_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits );
|
||||
extern int bmcg2_sat_solver_equiv_overlap_check( bmcg2_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv );
|
||||
extern Vec_Str_t * bmcg2_sat_solver_sop( Gia_Man_t * p, int CubeLimit );
|
||||
extern int bmcg2_sat_solver_jftr( bmcg2_sat_solver * s );
|
||||
extern void bmcg2_sat_solver_set_jftr( bmcg2_sat_solver * s, int jftr );
|
||||
extern void bmcg2_sat_solver_set_var_fanin_lit( bmcg2_sat_solver * s, int var, int lit0, int lit1 );
|
||||
extern void bmcg2_sat_solver_start_new_round( bmcg2_sat_solver * s );
|
||||
extern void bmcg2_sat_solver_mark_cone( bmcg2_sat_solver * s, int var );
|
||||
|
||||
extern void Glucose2_SolveCnf( char * pFilename, Glucose2_Pars * pPars );
|
||||
extern int Glucose2_SolveAig( Gia_Man_t * p, Glucose2_Pars * pPars );
|
||||
|
|
|
|||
|
|
@ -64,6 +64,12 @@ public:
|
|||
vec<int> user_vec;
|
||||
vec<Lit> user_lits;
|
||||
|
||||
// circuit-based solving
|
||||
int jftr;
|
||||
void sat_solver_set_var_fanin_lit(int, int, int);
|
||||
void sat_solver_start_new_round();
|
||||
void sat_solver_mark_cone(int);
|
||||
|
||||
// Problem specification:
|
||||
//
|
||||
Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
|
||||
|
|
@ -457,6 +463,10 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ v
|
|||
|
||||
inline void Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
|
||||
|
||||
inline void Solver::sat_solver_set_var_fanin_lit(int var, int lit0, int lit1) {}
|
||||
inline void Solver::sat_solver_start_new_round() {}
|
||||
inline void Solver::sat_solver_mark_cone(int var) {}
|
||||
|
||||
//=================================================================================================
|
||||
// Debug etc:
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue