From f5cb9d6448a9c1d450fd9f578c18b7b51c290fd4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 16 Sep 2017 12:37:27 -0700 Subject: Bug fix in Glucose integration. --- src/sat/glucose/AbcGlucose.cpp | 83 ++++++++++++++++++++++++++++++++---------- src/sat/glucose/Glucose.cpp | 4 +- src/sat/glucose/SimpSolver.h | 3 ++ src/sat/glucose/Solver.h | 15 +++++--- 4 files changed, 78 insertions(+), 27 deletions(-) (limited to 'src') diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 9011665a..f4bc41b7 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -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 * 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 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 * 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 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 ); diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp index 8d520474..2a67d903 100644 --- a/src/sat/glucose/Glucose.cpp +++ b/src/sat/glucose/Glucose.cpp @@ -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& 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" ); } diff --git a/src/sat/glucose/SimpSolver.h b/src/sat/glucose/SimpSolver.h index 8daf99d1..260ab5e3 100644 --- a/src/sat/glucose/SimpSolver.h +++ b/src/sat/glucose/SimpSolver.h @@ -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& 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& assumps, bool do_simp, boo inline lbool SimpSolver::solveLimited (const vec& 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(); } + //================================================================================================= } diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h index 3a90f847..bb4c6d0f 100644 --- a/src/sat/glucose/Solver.h +++ b/src/sat/glucose/Solver.h @@ -61,10 +61,12 @@ public: int * pstop; // another callback uint64_t nRuntimeLimit; // runtime limit vec user_vec; + vec 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& 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& assumps){ budgetOff(); as inline lbool Solver::solveLimited (const vec& assumps){ assumps.copyTo(assumptions); return solve_(); } inline bool Solver::okay () const { return ok; } -inline void Solver::toDimacs (const char* file){ vec as; toDimacs(file, as); } -inline void Solver::toDimacs (const char* file, Lit p){ vec as; as.push(p); toDimacs(file, as); } -inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec as; as.push(p); as.push(q); toDimacs(file, as); } -inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); } +inline void Solver::toDimacs (const char* file){ vec as; toDimacs(file, as); } +inline void Solver::toDimacs (const char* file, Lit p){ vec as; as.push(p); toDimacs(file, as); } +inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec as; as.push(p); as.push(q); toDimacs(file, as); } +inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec 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: -- cgit v1.2.3