AbcGlucose.h File Reference

#include "aig/gia/gia.h"

Include dependency graph for AbcGlucose.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	Glucose_Pars_

Macros
#define	GLUCOSE_UNSAT   -1
	INCLUDES ///.
#define	GLUCOSE_SAT   1
#define	GLUCOSE_UNDEC   0

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Glucose_Pars_	Glucose_Pars
	BASIC TYPES ///.
typedef void	bmcg_sat_solver

Functions
bmcg_sat_solver *	bmcg_sat_solver_start ()
	MACRO DEFINITIONS ///.
void	bmcg_sat_solver_stop (bmcg_sat_solver *s)
void	bmcg_sat_solver_reset (bmcg_sat_solver *s)
int	bmcg_sat_solver_addclause (bmcg_sat_solver *s, int *plits, int nlits)
void	bmcg_sat_solver_setcallback (bmcg_sat_solver *s, void *pman, int(*pfunc)(void *, int, int *))
int	bmcg_sat_solver_solve (bmcg_sat_solver *s, int *plits, int nlits)
int	bmcg_sat_solver_final (bmcg_sat_solver *s, int **ppArray)
int	bmcg_sat_solver_addvar (bmcg_sat_solver *s)
void	bmcg_sat_solver_set_nvars (bmcg_sat_solver *s, int nvars)
int	bmcg_sat_solver_eliminate (bmcg_sat_solver *s, int turn_off_elim)
int	bmcg_sat_solver_var_is_elim (bmcg_sat_solver *s, int v)
void	bmcg_sat_solver_var_set_frozen (bmcg_sat_solver *s, int v, int freeze)
int	bmcg_sat_solver_elim_varnum (bmcg_sat_solver *s)
int *	bmcg_sat_solver_read_cex (bmcg_sat_solver *s)
int	bmcg_sat_solver_read_cex_varvalue (bmcg_sat_solver *s, int)
void	bmcg_sat_solver_set_stop (bmcg_sat_solver *s, int *pstop)
abctime	bmcg_sat_solver_set_runtime_limit (bmcg_sat_solver *s, abctime Limit)
void	bmcg_sat_solver_set_conflict_budget (bmcg_sat_solver *s, int Limit)
int	bmcg_sat_solver_varnum (bmcg_sat_solver *s)
int	bmcg_sat_solver_clausenum (bmcg_sat_solver *s)
int	bmcg_sat_solver_learntnum (bmcg_sat_solver *s)
int	bmcg_sat_solver_conflictnum (bmcg_sat_solver *s)
int	bmcg_sat_solver_minimize_assumptions (bmcg_sat_solver *s, int *plits, int nlits, int pivot)
int	bmcg_sat_solver_add_and (bmcg_sat_solver *s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl)
int	bmcg_sat_solver_add_xor (bmcg_sat_solver *s, int iVarA, int iVarB, int iVarC, int fCompl)
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)
int	bmcg_sat_solver_equiv_overlap_check (bmcg_sat_solver *s, Gia_Man_t *p, int iLit0, int iLit1, int fEquiv)
Vec_Str_t *	bmcg_sat_solver_sop (Gia_Man_t *p, int CubeLimit)
int	bmcg_sat_solver_jftr (bmcg_sat_solver *s)
void	bmcg_sat_solver_set_jftr (bmcg_sat_solver *s, int jftr)
void	bmcg_sat_solver_set_var_fanin_lit (bmcg_sat_solver *s, int var, int lit0, int lit1)
void	bmcg_sat_solver_start_new_round (bmcg_sat_solver *s)
void	bmcg_sat_solver_mark_cone (bmcg_sat_solver *s, int var)
void	Glucose_SolveCnf (char *pFilename, Glucose_Pars *pPars, int fDumpCnf)
int	Glucose_SolveAig (Gia_Man_t *p, Glucose_Pars *pPars)

Macro Definition Documentation

GLUCOSE_SAT

#define GLUCOSE_SAT   1

Definition at line 35 of file AbcGlucose.h.

GLUCOSE_UNDEC

#define GLUCOSE_UNDEC   0

Definition at line 36 of file AbcGlucose.h.

GLUCOSE_UNSAT

#define GLUCOSE_UNSAT   -1

INCLUDES ///.

CFile****************************************************************

FileName [AbcGlucose.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.]

Synopsis [Interface to Glucose.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 6, 2017.]

Revision [

Id

AbcGlucose.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS ///

Definition at line 34 of file AbcGlucose.h.

Typedef Documentation

bmcg_sat_solver

typedef void bmcg_sat_solver

Definition at line 63 of file AbcGlucose.h.

Glucose_Pars

typedef typedefABC_NAMESPACE_HEADER_START struct Glucose_Pars_ Glucose_Pars

BASIC TYPES ///.

Definition at line 45 of file AbcGlucose.h.

Function Documentation

bmcg_sat_solver_add_and()

int bmcg_sat_solver_add_and ( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )

extern

Definition at line 306 of file AbcGlucose.cpp.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_add_xor()

int bmcg_sat_solver_add_xor ( bmcg_sat_solver * s, int iVarA, int iVarB, int iVarC, int fCompl )

extern

bmcg_sat_solver_addclause()

int bmcg_sat_solver_addclause ( bmcg_sat_solver * s, int * plits, int nlits )

extern

Definition at line 160 of file AbcGlucose.cpp.

{
    return glucose_solver_addclause((Gluco::SimpSolver*)s,plits,nlits);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_addvar()

int bmcg_sat_solver_addvar ( bmcg_sat_solver * s )

extern

Definition at line 181 of file AbcGlucose.cpp.

{
    return glucose_solver_addvar((Gluco::SimpSolver*)s);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_clausenum()

int bmcg_sat_solver_clausenum ( bmcg_sat_solver * s )

extern

Definition at line 249 of file AbcGlucose.cpp.

{
    return ((Gluco::SimpSolver*)s)->nClauses();
}

Here is the caller graph for this function:

bmcg_sat_solver_conflictnum()

int bmcg_sat_solver_conflictnum ( bmcg_sat_solver * s )

extern

Definition at line 257 of file AbcGlucose.cpp.

{
    return ((Gluco::SimpSolver*)s)->conflicts;
}

Here is the caller graph for this function:

bmcg_sat_solver_elim_varnum()

int bmcg_sat_solver_elim_varnum ( bmcg_sat_solver * s )

extern

Definition at line 210 of file AbcGlucose.cpp.

{
//    return 0; 
    return ((Gluco::SimpSolver*)s)->eliminated_vars;
}

Here is the caller graph for this function:

bmcg_sat_solver_eliminate()

int bmcg_sat_solver_eliminate ( bmcg_sat_solver * s, int turn_off_elim )

extern

Definition at line 193 of file AbcGlucose.cpp.

{
//    return 1; 
    return ((Gluco::SimpSolver*)s)->eliminate(turn_off_elim != 0);
}

Here is the caller graph for this function:

bmcg_sat_solver_equiv_overlap_check()

int bmcg_sat_solver_equiv_overlap_check ( bmcg_sat_solver * pSat, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv )

extern

Function*************************************************************

Synopsis [Checks equivalence or intersection of two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1414 of file AbcGlucose.cpp.

{
    bmcg_sat_solver * pSats[2] = { pSat, NULL };
    Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 ); 
    int i, iVar, iSatVar[2], iSatLit[2], Lits[2], status;
    if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) )
        Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 );
 
    // assign const0 variable number 0
    iVar = Vec_IntSize(vObjsUsed);
    Vec_IntPush( vObjsUsed, 0 );
    Gia_ObjSetCopyArray( p, 0, iVar );
    assert( iVar == 0 );
 
    iSatVar[0] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit0), vObjsUsed, NULL );
    iSatVar[1] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit1), vObjsUsed, NULL );
 
    iSatLit[0] = Abc_Var2Lit( iSatVar[0], Abc_LitIsCompl(iLit0) );
    iSatLit[1] = Abc_Var2Lit( iSatVar[1], Abc_LitIsCompl(iLit1) );
    Gia_ManQuantLoadCnf( p, vObjsUsed, pSats );
    Vec_IntForEachEntry( vObjsUsed, iVar, i )
        Gia_ObjSetCopyArray( p, iVar, -1 );
    Vec_IntFree( vObjsUsed );
 
    if ( fEquiv )
    {
        Lits[0] = iSatLit[0];
        Lits[1] = Abc_LitNot(iSatLit[1]);
        status  = bmcg_sat_solver_solve( pSats[0], Lits, 2 );
        if ( status == GLUCOSE_UNSAT )
        {
            Lits[0] = Abc_LitNot(iSatLit[0]);
            Lits[1] = iSatLit[1];
            status  = bmcg_sat_solver_solve( pSats[0], Lits, 2 );
        }
        return status == GLUCOSE_UNSAT;
    }
    else
    {
        Lits[0] = iSatLit[0];
        Lits[1] = iSatLit[1];
        status  = bmcg_sat_solver_solve( pSats[0], Lits, 2 );
        return status == GLUCOSE_SAT;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_final()

int bmcg_sat_solver_final ( bmcg_sat_solver * s, int ** ppArray )

extern

Definition at line 175 of file AbcGlucose.cpp.

{
    *ppArray = (int *)(Lit *)((Gluco::SimpSolver*)s)->conflict;
    return ((Gluco::SimpSolver*)s)->conflict.size();
}

Here is the caller graph for this function:

bmcg_sat_solver_jftr()

int bmcg_sat_solver_jftr ( bmcg_sat_solver * s )

extern

Definition at line 361 of file AbcGlucose.cpp.

{
    return ((Gluco::SimpSolver*)s)->jftr;
}

bmcg_sat_solver_learntnum()

int bmcg_sat_solver_learntnum ( bmcg_sat_solver * s )

extern

Definition at line 253 of file AbcGlucose.cpp.

{
    return ((Gluco::SimpSolver*)s)->nLearnts();
}

Here is the caller graph for this function:

bmcg_sat_solver_mark_cone()

void bmcg_sat_solver_mark_cone ( bmcg_sat_solver * s, int var )

extern

Definition at line 381 of file AbcGlucose.cpp.

{
    ((Gluco::SimpSolver*)s)->sat_solver_mark_cone(var);
}

Here is the call graph for this function:

bmcg_sat_solver_minimize_assumptions()

int bmcg_sat_solver_minimize_assumptions ( bmcg_sat_solver * s, int * plits, int nlits, int pivot )

extern

Definition at line 262 of file AbcGlucose.cpp.

{
    vec<int>*array = &((Gluco::SimpSolver*)s)->user_vec;
    int i, nlitsL, nlitsR, nresL, nresR, status;
    assert( pivot >= 0 );
//    assert( nlits - pivot >= 2 );
    assert( nlits - pivot >= 1 );
    if ( nlits - pivot == 1 )
    {
        // since the problem is UNSAT, we try to solve it without assuming the last literal
        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
        status = bmcg_sat_solver_solve( s, plits, pivot );
        return status != GLUCOSE_UNSAT; // return 1 if the problem is not UNSAT
    }
    assert( nlits - pivot >= 2 );
    nlitsL = (nlits - pivot) / 2;
    nlitsR = (nlits - pivot) - nlitsL;
    assert( nlitsL + nlitsR == nlits - pivot );
    // solve with these assumptions
    status = bmcg_sat_solver_solve( s, plits, pivot + nlitsL );
    if ( status == GLUCOSE_UNSAT ) // these are enough
        return bmcg_sat_solver_minimize_assumptions( s, plits, pivot + nlitsL, pivot );
    // these are not enough
    // solve for the right lits
//    nResL = nLitsR == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
    nresL = nlitsR == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits, nlits, pivot + nlitsL );
    // swap literals
    array->clear();
    for ( i = 0; i < nlitsL; i++ )
        array->push(plits[pivot + i]);
    for ( i = 0; i < nresL; i++ )
        plits[pivot + i] = plits[pivot + nlitsL + i];
    for ( i = 0; i < nlitsL; i++ )
        plits[pivot + nresL + i] = (*array)[i];
    // solve with these assumptions
    status = bmcg_sat_solver_solve( s, plits, pivot + nresL );
    if ( status == GLUCOSE_UNSAT ) // these are enough
        return nresL;
    // solve for the left lits
//    nResR = nLitsL == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
    nresR = nlitsL == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits, pivot + nresL + nlitsL, pivot + nresL );
    return nresL + nresR;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_quantify()

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

Definition at line 1256 of file AbcGlucose.cpp.

{
    Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 ); // GIA objs
    Vec_Int_t * vCiVars = Vec_IntAlloc( 100 );   // CI SAT vars
    Vec_Int_t * vVarMap = NULL; Vec_Str_t * vSop = NULL; 
    int i, iVar, iVarLast, Lit, RetValue, Count = 0, Result = -1;
    if ( vDLits ) Vec_IntClear( vDLits );
    if ( iLit < 2 )
        return iLit;
    if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) )
        Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 );
    // assign variable number 0 to const0 node
    iVar = Vec_IntSize(vObjsUsed); 
    Vec_IntPush( vObjsUsed, 0 );
    Gia_ObjSetCopyArray( p, 0, iVar );
    assert( iVar == 0 );    
 
    // collect other variables
    iVarLast = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit), vObjsUsed, vCiVars );
    Gia_ManQuantLoadCnf( p, vObjsUsed, pSats );
 
    // check constants
    Lit = Abc_Var2Lit( iVarLast, !Abc_LitIsCompl(iLit) ); 
    RetValue = bmcg_sat_solver_addclause( pSats[0], &Lit, 1 ); // offset
    if ( !RetValue || bmcg_sat_solver_solve(pSats[0], NULL, 0) == GLUCOSE_UNSAT )
    {
        Result = 1;
        goto cleanup;
    }
    Lit = Abc_Var2Lit( iVarLast, Abc_LitIsCompl(iLit) );
    RetValue = bmcg_sat_solver_addclause( pSats[1], &Lit, 1 ); // onset
    if ( !RetValue || bmcg_sat_solver_solve(pSats[1], NULL, 0) == GLUCOSE_UNSAT )
    {
        Result = 0;
        goto cleanup;
    }
/*
    // reorder CI SAT variables to have keep-vars first
    Vec_Int_t * vCiVars2 = Vec_IntAlloc( 100 );   // CI SAT vars
    Vec_IntForEachEntry( vCiVars, iVar, i )
    {
        Gia_Obj_t * pObj = Gia_ManObj( p, Vec_IntEntry(vObjsUsed, iVar) );
        assert( Gia_ObjIsCi(pObj) );
        if ( pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) )
            Vec_IntPush( vCiVars2, iVar );
    }
    Vec_IntForEachEntry( vCiVars, iVar, i )
    {
        Gia_Obj_t * pObj = Gia_ManObj( p, Vec_IntEntry(vObjsUsed, iVar) );
        assert( Gia_ObjIsCi(pObj) );
        if ( !pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) )
            Vec_IntPush( vCiVars2, iVar );
    }
    ABC_SWAP( Vec_Int_t *, vCiVars2, vCiVars );
    Vec_IntFree( vCiVars2 );
*/
    // map CI SAT variables into their indexes used in the cubes
    vVarMap = Vec_IntStartFull( Vec_IntSize(vObjsUsed) );
    Vec_IntForEachEntry( vCiVars, iVar, i )
    {
        Gia_Obj_t * pObj = Gia_ManObj( p, Vec_IntEntry(vObjsUsed, iVar) );
        assert( Gia_ObjIsCi(pObj) );
        if ( pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) )
            Vec_IntWriteEntry( vVarMap, iVar, i ), Count++;
    }
    if ( Count == 0 || Count == Vec_IntSize(vCiVars) )
    {
        Result = Count == 0 ? 1 : iLit;
        goto cleanup;
    }
    // generate cubes
    vSop = Glucose_GenerateCubes( pSats, vCiVars, vVarMap, 0 );
    //printf( "%s", Vec_StrArray(vSop) );
    // convert into object IDs
    Vec_IntForEachEntry( vCiVars, iVar, i )
        Vec_IntWriteEntry( vCiVars, i, Vec_IntEntry(vObjsUsed, iVar) );
    // generate unate variables
    if ( vDLits )
        bmcg_sat_generate_dvars( vCiVars, vSop, vDLits );
    // convert into an AIG
    RetValue = Gia_ManAndNum(p);
    Result = Gia_ManFactorSop( p, vCiVars, vSop, fHash );
 
    // report the result
//    printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ", 
//        Vec_IntSize(vObjsUsed), Count, Vec_IntSize(vCiVars) - Count, Vec_StrCountEntry(vSop, '\n'), Gia_ManAndNum(p)-RetValue );
//    Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll );
 
cleanup:
    Vec_IntForEachEntry( vObjsUsed, iVar, i )
        Gia_ObjSetCopyArray( p, iVar, -1 );
    Vec_IntFree( vObjsUsed );
    Vec_IntFree( vCiVars );
    Vec_IntFreeP( &vVarMap );
    Vec_StrFreeP( &vSop );
    return Result;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_read_cex()

int * bmcg_sat_solver_read_cex ( bmcg_sat_solver * s )

extern

Definition at line 216 of file AbcGlucose.cpp.

{
    return glucose_solver_read_cex((Gluco::SimpSolver*)s);
}

Here is the call graph for this function:

bmcg_sat_solver_read_cex_varvalue()

int bmcg_sat_solver_read_cex_varvalue ( bmcg_sat_solver * s, int ivar )

extern

Definition at line 220 of file AbcGlucose.cpp.

{
    return glucose_solver_read_cex_varvalue((Gluco::SimpSolver*)s, ivar);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_reset()

void bmcg_sat_solver_reset ( bmcg_sat_solver * s )

extern

Definition at line 154 of file AbcGlucose.cpp.

{
    glucose_solver_reset((Gluco::SimpSolver*)s);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_set_conflict_budget()

void bmcg_sat_solver_set_conflict_budget ( bmcg_sat_solver * s, int Limit )

extern

Definition at line 237 of file AbcGlucose.cpp.

{
    if ( Limit > 0 ) 
        ((Gluco::SimpSolver*)s)->setConfBudget( (int64_t)Limit );
    else 
        ((Gluco::SimpSolver*)s)->budgetOff();
}

Here is the caller graph for this function:

bmcg_sat_solver_set_jftr()

void bmcg_sat_solver_set_jftr ( bmcg_sat_solver * s, int jftr )

extern

Definition at line 366 of file AbcGlucose.cpp.

{
    ((Gluco::SimpSolver*)s)->jftr = jftr;
}

bmcg_sat_solver_set_nvars()

void bmcg_sat_solver_set_nvars ( bmcg_sat_solver * s, int nvars )

extern

Definition at line 186 of file AbcGlucose.cpp.

{
    int i;
    for ( i = bmcg_sat_solver_varnum(s); i < nvars; i++ )
        bmcg_sat_solver_addvar(s);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_set_runtime_limit()

abctime bmcg_sat_solver_set_runtime_limit ( bmcg_sat_solver * s, abctime Limit )

extern

Definition at line 230 of file AbcGlucose.cpp.

{
    abctime nRuntimeLimit = ((Gluco::SimpSolver*)s)->nRuntimeLimit;
    ((Gluco::SimpSolver*)s)->nRuntimeLimit = Limit;
    return nRuntimeLimit;
}

Here is the caller graph for this function:

bmcg_sat_solver_set_stop()

void bmcg_sat_solver_set_stop ( bmcg_sat_solver * s, int * pstop )

extern

Definition at line 225 of file AbcGlucose.cpp.

{
    glucose_solver_setstop((Gluco::SimpSolver*)s, pstop);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_set_var_fanin_lit()

void bmcg_sat_solver_set_var_fanin_lit ( bmcg_sat_solver * s, int var, int lit0, int lit1 )

extern

Definition at line 371 of file AbcGlucose.cpp.

{
    ((Gluco::SimpSolver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1);
}

Here is the call graph for this function:

bmcg_sat_solver_setcallback()

void bmcg_sat_solver_setcallback ( bmcg_sat_solver * s, void * pman, int(* pfunc )(void *, int, int *) )

extern

Definition at line 165 of file AbcGlucose.cpp.

{
    glucose_solver_setcallback((Gluco::SimpSolver*)s,pman,pfunc);
}

Here is the call graph for this function:

bmcg_sat_solver_solve()

int bmcg_sat_solver_solve ( bmcg_sat_solver * s, int * plits, int nlits )

extern

Definition at line 170 of file AbcGlucose.cpp.

{
    return glucose_solver_solve((Gluco::SimpSolver*)s,plits,nlits);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_sop()

Vec_Str_t * bmcg_sat_solver_sop ( Gia_Man_t * p, int CubeLimit )

extern

Definition at line 980 of file AbcGlucose.cpp.

{
    bmcg_sat_solver * pSat[2] = { bmcg_sat_solver_start(), bmcg_sat_solver_start() };
 
    // generate CNF for the on-set and off-set
    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 0/*fAddOrCla*/, 0, 0/*verbose*/ );
    int i, n, nVars = Gia_ManCiNum(p), Lit;//, Count = 0;
    int iFirstVar = pCnf->nVars - nVars;
    assert( Gia_ManCoNum(p) == 1 );
    for ( n = 0; n < 2; n++ )
    {
        bmcg_sat_solver_set_nvars( pSat[n], pCnf->nVars );
        Lit = Abc_Var2Lit( 1, !n );  // output variable is 1
        for ( i = 0; i < pCnf->nClauses; i++ )
            if ( !bmcg_sat_solver_addclause( pSat[n], pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
                assert( 0 );
        if ( !bmcg_sat_solver_addclause( pSat[n], &Lit, 1 ) )
        {
            Vec_Str_t * vSop = Vec_StrAlloc( 10 );
            Vec_StrPrintF( vSop, " %d\n\0", !n );
            Cnf_DataFree( pCnf );
            return vSop;
        }
    }
    Cnf_DataFree( pCnf );
 
    // collect cube vars and map SAT vars into them
    Vec_Int_t * vVars = Vec_IntAlloc( 100 ); 
    Vec_Int_t * vVarMap = Vec_IntStartFull( iFirstVar + nVars ); 
    for ( i = 0; i < nVars; i++ )
    {
        Vec_IntPush( vVars, iFirstVar+i );
        Vec_IntWriteEntry( vVarMap, iFirstVar+i, i );
    }
 
    Vec_Str_t * vSop = Glucose_GenerateCubes( pSat, vVars, vVarMap, CubeLimit );
    Vec_IntFree( vVarMap );
    Vec_IntFree( vVars );
 
    bmcg_sat_solver_stop( pSat[0] );
    bmcg_sat_solver_stop( pSat[1] );
    return vSop;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_start()

bmcg_sat_solver * bmcg_sat_solver_start ( )

extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

Function*************************************************************

Synopsis [Wrapper APIs to calling from ABC.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file AbcGlucose.cpp.

{
    return (bmcg_sat_solver *)glucose_solver_start();
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_start_new_round()

void bmcg_sat_solver_start_new_round ( bmcg_sat_solver * s )

extern

Definition at line 376 of file AbcGlucose.cpp.

{
    ((Gluco::SimpSolver*)s)->sat_solver_start_new_round();
}

bmcg_sat_solver_stop()

void bmcg_sat_solver_stop ( bmcg_sat_solver * s )

extern

Definition at line 150 of file AbcGlucose.cpp.

{
    glucose_solver_stop((Gluco::SimpSolver*)s);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bmcg_sat_solver_var_is_elim()

int bmcg_sat_solver_var_is_elim ( bmcg_sat_solver * s, int v )

extern

Definition at line 199 of file AbcGlucose.cpp.

{
//    return 0; 
    return ((Gluco::SimpSolver*)s)->isEliminated(v);
}

Here is the caller graph for this function:

bmcg_sat_solver_var_set_frozen()

void bmcg_sat_solver_var_set_frozen ( bmcg_sat_solver * s, int v, int freeze )

extern

Definition at line 205 of file AbcGlucose.cpp.

{
    ((Gluco::SimpSolver*)s)->setFrozen(v, freeze != 0);
}

Here is the caller graph for this function:

bmcg_sat_solver_varnum()

int bmcg_sat_solver_varnum ( bmcg_sat_solver * s )

extern

Definition at line 245 of file AbcGlucose.cpp.

{
    return ((Gluco::SimpSolver*)s)->nVars();
}

Here is the caller graph for this function:

Glucose_SolveAig()

int Glucose_SolveAig ( Gia_Man_t * p, Glucose_Pars * pPars )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1487 of file AbcGlucose.cpp.

{  
    abctime clk = Abc_Clock();
 
    SimpSolver S;
    S.verbosity = pPars->verb;
    S.verbEveryConflicts = 50000;
    S.showModel = false;
    //S.verbosity = 2;
    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);
        printf( "c Simplification removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    
    vec<Lit> 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 );
 
    // 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);
}

Here is the call graph for this function:

Glucose_SolveCnf()

void Glucose_SolveCnf ( char * pFileName, Glucose_Pars * pPars, int fDumpCnf )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 821 of file AbcGlucose.cpp.

{
    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);
    Glucose_ReadDimacs( pFileName, S );
 
    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);
        printf( "c Simplification removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
        if ( fDumpCnf )
        {
            char * pFileCnf = Extra_FileNameGenericAppend( pFileName, "_out.cnf" );
            S.toDimacs(pFileCnf);
            printf( "Finished dumping CNF after preprocessing into file \"%s\".\n", pFileCnf );
            printf( "SAT solving is not performed.\n" );
            return;
        }
    }
 
    vec<Lit> 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 );
}

Here is the call graph for this function: