Adding Glucose 3.0 as a separate package.

1 files changed, 268 insertions, 0 deletions

diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
new file mode 100644
index 00000000..7601ac39
--- /dev/null
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -0,0 +1,268 @@
+/**CFile****************************************************************
+
+  FileName    [AbcGlucose.cpp]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT solver Glucose 3.0.]
+
+  Synopsis    [Interface to Glucose.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 6, 2017.]
+
+  Revision    [$Id: AbcGlucose.cpp,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sat/glucose/System.h"
+#include "sat/glucose/ParseUtils.h"
+#include "sat/glucose/Options.h"
+#include "sat/glucose/Dimacs.h"
+#include "sat/glucose/SimpSolver.h"
+
+#include "sat/glucose/AbcGlucose.h"
+
+#include "aig/gia/gia.h"
+#include "sat/cnf/cnf.h"
+
+using namespace Glucose;
+
+ABC_NAMESPACE_IMPL_START
+
+extern "C" {
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Glucose::Solver * glucose_solver_start()
+{
+    Solver * S = new Solver;
+    S->setIncrementalMode();
+    return S;
+}
+
+void glucose_solver_stop(Glucose::Solver* S)
+{
+    delete S;
+}
+
+int glucose_solver_addclause(Glucose::Solver* S, int * plits, int nlits)
+{
+    vec<Lit> lits;
+    for ( int i = 0; i < nlits; i++,plits++)
+    {
+        // note: Glucose uses the same var->lit conventiaon as ABC
+        while ((*plits)/2 >= S->nVars()) S->newVar();
+        assert((*plits)/2 < S->nVars()); // NOTE: since we explicitely use new function bmc_add_var
+        Lit p;
+        p.x = *plits;
+        lits.push(p);
+    }
+    return S->addClause(lits); // returns 0 if the problem is UNSAT
+}
+
+int glucose_solver_setcallback(Glucose::Solver* S, void * pman, int(*pfunc)(void*, int, int*))
+{
+    S->pCnfMan = pman;
+    S->pCnfFunc = pfunc;
+    S->nCallConfl = 1000;
+    return 0;
+}
+
+int glucose_solver_solve(Glucose::Solver* S, int * plits, int nlits)
+{
+    vec<Lit> lits;
+    for (int i=0;i<nlits;i++,plits++)
+    {
+        Lit p;
+        p.x = *plits;
+        lits.push(p);
+    }
+    Glucose::lbool res = S->solveLimited(lits);
+    return (res == l_True ? 1 : res == l_False ? -1 : 0);
+}
+
+int glucose_solver_addvar(Glucose::Solver* S)
+{
+    S->newVar();
+    return S->nVars() - 1;
+}
+
+int glucose_solver_read_cex_varvalue(Glucose::Solver* S, int ivar)
+{
+    return S->model[ivar] == l_True;
+}
+
+void glucose_solver_setstop(Glucose::Solver* S, int * pstop)
+{
+    S->pstop = pstop;
+}
+
+void glucose_print_stats(Solver& s, abctime clk)
+{
+    double cpu_time = (double)(unsigned)clk / CLOCKS_PER_SEC;
+    double mem_used = memUsed();
+    printf("c restarts              : %d (%d conflicts on average)\n",         (int)s.starts, s.starts > 0 ? s.conflicts/s.starts : 0);
+    printf("c blocked restarts      : %d (multiple: %d) \n",                   (int)s.nbstopsrestarts,s.nbstopsrestartssame);
+    printf("c last block at restart : %d\n",                                   (int)s.lastblockatrestart);
+    printf("c nb ReduceDB           : %-12d\n",                                (int)s.nbReduceDB);
+    printf("c nb removed Clauses    : %-12d\n",                                (int)s.nbRemovedClauses);
+    printf("c nb learnts DL2        : %-12d\n",                                (int)s.nbDL2);
+    printf("c nb learnts size 2     : %-12d\n",                                (int)s.nbBin);
+    printf("c nb learnts size 1     : %-12d\n",                                (int)s.nbUn);
+    printf("c conflicts             : %-12d  (%.0f /sec)\n",                   (int)s.conflicts,    s.conflicts   /cpu_time);
+    printf("c decisions             : %-12d  (%4.2f %% random) (%.0f /sec)\n", (int)s.decisions,    (float)s.rnd_decisions*100 / (float)s.decisions, s.decisions   /cpu_time);
+    printf("c propagations          : %-12d  (%.0f /sec)\n",                   (int)s.propagations, s.propagations/cpu_time);
+    printf("c conflict literals     : %-12d  (%4.2f %% deleted)\n",            (int)s.tot_literals, (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
+    printf("c nb reduced Clauses    : %-12d\n", (int)s.nbReducedClauses);
+    if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
+    //printf("c CPU time              : %.2f sec\n", cpu_time);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Glucose_SolveCnf( char * pFilename, ExtSat_Pars * pPars )
+{
+    abctime clk = Abc_Clock();
+    SimpSolver  S;
+    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);
+
+    printf("c ============================[ Problem Statistics ]=============================\n");
+    printf("c |                                                                             |\n");
+    printf("c |  Number of variables:  %12d                                         |\n", S.nVars());
+    printf("c |  Number of clauses:    %12d                                         |\n", S.nClauses());
+    
+    if ( pPars->pre ) S.eliminate(true);
+
+    vec<Lit> dummy;
+    lbool ret = S.solveLimited(dummy);
+    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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& S )
+{
+    abctime clk = Abc_Clock();
+    int * pLit, * pStop, i;
+    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++ )
+    {
+        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);
+    }
+    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 );
+    //Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    Cnf_DataFree(pCnf);
+    return vCnfIds;
+}
+
+int Glucose_SolveAig(Gia_Man_t * p, ExtSat_Pars * pPars)
+{  
+    abctime clk = Abc_Clock();
+
+    SimpSolver S;
+    S.verbosity = pPars->verb;
+    S.verbEveryConflicts = 50000;
+    S.showModel = false;
+    S.setConfBudget( pPars->nConfls > 0 ? (int64_t)pPars->nConfls : -1 );
+
+    S.parsing = 1;
+    Vec_Int_t * vCnfIds = Glucose_SolverFromAig(p,S);
+    S.parsing = 0;
+
+    if (pPars->verb)
+    {
+        printf("c ============================[ Problem Statistics ]=============================\n");
+        printf("c |                                                                             |\n");
+        printf("c |  Number of variables:  %12d                                         |\n", S.nVars());
+        printf("c |  Number of clauses:    %12d                                         |\n", S.nClauses());
+    }
+
+    if (pPars->pre) 
+        S.eliminate(true);
+    
+    vec<Lit> dummy;
+    lbool ret = S.solveLimited(dummy);
+
+    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 );
+
+    // port counterexample
+    if (ret == l_True)
+    {
+        Gia_Obj_t * pObj;  int i;
+        p->pCexComb = Abc_CexAlloc(0,Gia_ManCiNum(p),1);
+        Gia_ManForEachCi( p, pObj, i )
+        {
+            assert(Vec_IntEntry(vCnfIds,Gia_ObjId(p, pObj))!=-1);
+            if (S.model[Vec_IntEntry(vCnfIds,Gia_ObjId(p, pObj))] == l_True)
+                Abc_InfoSetBit( p->pCexComb->pData, i);
+        }
+    }
+    Vec_IntFree(vCnfIds);
+    return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+}
+
+ABC_NAMESPACE_IMPL_END