luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Bug fix in Glucose integration.

This commit is contained in:
Alan Mishchenko 2017-09-16 12:37:27 -07:00
parent adce11979f
commit f5cb9d6448
4 changed files with 78 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

83
src/sat/glucose/AbcGlucose.cpp
View File

@ -28,6 +28,7 @@
#include "aig/gia/gia.h"
#include "sat/cnf/cnf.h"
#include "misc/extra/extra.h"
using namespace Gluco;
@ -46,7 +47,6 @@ extern "C" {
////////////////////////////////////////////////////////////////////////
#ifdef USE_SIMP_SOLVER
/**Function*************************************************************
@ -547,7 +547,57 @@ void glucose_print_stats(SimpSolver& s, abctime clk)
SeeAlso []
***********************************************************************/
void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars )
void Glucose_ReadDimacs( char * pFileName, SimpSolver& s )
{
vec<Lit> * lits = &s.user_lits;
char * pBuffer = Extra_FileReadContents( pFileName );
char * pTemp; int fComp, Var, VarMax = 0;
lits->clear();
for ( pTemp = pBuffer; *pTemp; pTemp++ )
{
if ( *pTemp == 'c' || *pTemp == 'p' ) {
while ( *pTemp != '\n' )
pTemp++;
continue;
}
while ( *pTemp == ' ' || *pTemp == '\t' || *pTemp == '\r' || *pTemp == '\n' )
pTemp++;
fComp = 0;
if ( *pTemp == '-' )
fComp = 1, pTemp++;
if ( *pTemp == '+' )
pTemp++;
Var = atoi( pTemp );
if ( Var == 0 ) {
if ( lits->size() > 0 ) {
s.addVar( VarMax );
s.addClause(*lits);
lits->clear();
}
}
else {
Var--;
VarMax = Abc_MaxInt( VarMax, Var );
lits->push( toLit(Abc_Var2Lit(Var, fComp)) );
}
while ( *pTemp >= '0' && *pTemp <= '9' )
pTemp++;
}
ABC_FREE( pBuffer );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars )
{
abctime clk = Abc_Clock();
@ -555,9 +605,10 @@ void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars )
S.verbosity = pPars->verb;
S.setConfBudget( pPars->nConfls > 0 ? (int64_t)pPars->nConfls : -1 );
gzFile in = gzopen(pFilename, "rb");
parse_DIMACS(in, S);
gzclose(in);
// gzFile in = gzopen(pFilename, "rb");
// parse_DIMACS(in, S);
// gzclose(in);
Glucose_ReadDimacs( pFileName, S );
if ( pPars->verb )
{
@ -570,7 +621,7 @@ void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars )
if ( pPars->pre ) S.eliminate(true);
vec<Lit> dummy;
lbool ret = S.solveLimited(dummy);
lbool ret = S.solveLimited(dummy, 0);
if ( pPars->verb ) glucose_print_stats(S, Abc_Clock() - clk);
printf(ret == l_True ? "SATISFIABLE" : ret == l_False ? "UNSATISFIABLE" : "INDETERMINATE");
Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
@ -587,23 +638,17 @@ void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars )
SeeAlso []
***********************************************************************/
Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& S )
Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& s )
{
abctime clk = Abc_Clock();
int * pLit, * pStop, i;
vec<Lit> * lits = &s.user_lits;
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
for ( i = 0; i < pCnf->nClauses; i++ )
for ( int i = 0; i < pCnf->nClauses; i++ )
{
vec<Lit> lits;
for ( pLit = pCnf->pClauses[i], pStop = pCnf->pClauses[i+1]; pLit < pStop; pLit++ )
{
int Lit = *pLit;
int parsed_lit = (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1;
int var = abs(parsed_lit)-1;
while (var >= S.nVars()) S.newVar();
lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
}
S.addClause(lits);
lits->clear();
for ( int * pLit = pCnf->pClauses[i]; pLit < pCnf->pClauses[i+1]; pLit++ )
lits->push( toLit(*pLit) ), s.addVar( *pLit >> 1 );
s.addClause(*lits);
}
Vec_Int_t * vCnfIds = Vec_IntAllocArrayCopy(pCnf->pVarNums,pCnf->nVars);
printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );

4
src/sat/glucose/Glucose.cpp
View File

@ -209,7 +209,7 @@ Var Solver::newVar(bool sign, bool dvar)
//activity .push(0);
activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
seen .push(0);
permDiff .push(0);
permDiff .push(0);
polarity .push(sign);
decision .push();
trail .capacity(v+1);
@ -226,7 +226,7 @@ bool Solver::addClause_(vec<Lit>& ps)
if ( 0 ) {
for ( int i = 0; i < ps.size(); i++ )
printf( "%d ", toInt(ps[i]) );
printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 );
printf( "\n" );
}

3
src/sat/glucose/SimpSolver.h
View File

@ -40,6 +40,7 @@ class SimpSolver : public Solver {
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true);
void addVar (Var v);
bool addClause (const vec<Lit>& ps);
bool addEmptyClause(); // Add the empty clause to the solver.
bool addClause (Lit p); // Add a unit clause to the solver.
@ -193,6 +194,8 @@ inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, boo
inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
inline void SimpSolver::addVar(Var v) { while (v >= nVars()) newVar(); }
//=================================================================================================
}

15
src/sat/glucose/Solver.h
View File

@ -61,10 +61,12 @@ public:
int * pstop; // another callback
uint64_t nRuntimeLimit; // runtime limit
vec<int> user_vec;
vec<Lit> user_lits;
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
void addVar (Var v); // Add enough variables to make sure there is variable v.
bool addClause (const vec<Lit>& ps); // Add a clause to the solver.
bool addEmptyClause(); // Add the empty clause, making the solver contradictory.
@ -129,7 +131,7 @@ public:
// Memory managment:
//
/*virtual*/ void garbageCollect(); // virtuality causes segfault for some reason
virtual void garbageCollect(); // virtuality causes segfault for some reason
void checkGarbage(double gf);
void checkGarbage();
@ -393,7 +395,7 @@ inline bool Solver::addEmptyClause () { add_tmp.clear(
inline bool Solver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
inline bool Solver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
inline bool Solver::locked (const Clause& c) const {
inline bool Solver::locked (const Clause& c) const {
if(c.size()>2)
return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c;
return
@ -444,11 +446,12 @@ inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); as
inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
inline bool Solver::okay () const { return ok; }
inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); }
inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); }
inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
inline void Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
//=================================================================================================
// Debug etc: