cnfUtil.c File Reference

#include "cnf.h"
#include "sat/bsat/satSolver.h"
#include <unistd.h>

Include dependency graph for cnfUtil.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Vec_Int_t *	Exa4_ManParse (char *pFileName)
	DECLARATIONS ///.
Vec_Int_t *	Cnf_RunSolverOnce (int Id, int Rand, int TimeOut, int fVerbose)
	FUNCTION DEFINITIONS ///.
Vec_Int_t *	Cnf_RunSolverArray (int nProcs, int TimeOut, int fVerbose)
Vec_Int_t *	Cnf_RunSolver (int nProcs, int TimeOut, int fVerbose)
int	Aig_ManScanMapping_rec (Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped)
Vec_Ptr_t *	Aig_ManScanMapping (Cnf_Man_t *p, int fCollect)
int	Cnf_ManScanMapping_rec (Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped, int fPreorder)
Vec_Ptr_t *	Cnf_ManScanMapping (Cnf_Man_t *p, int fCollect, int fPreorder)
Vec_Int_t *	Cnf_DataCollectCiSatNums (Cnf_Dat_t *pCnf, Aig_Man_t *p)
Vec_Int_t *	Cnf_DataCollectCoSatNums (Cnf_Dat_t *pCnf, Aig_Man_t *p)
unsigned char *	Cnf_DataDeriveLitPolarities (Cnf_Dat_t *p)
Cnf_Dat_t *	Cnf_DataReadFromFile (char *pFileName)
int	Cnf_DataSolveFromFile (char *pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int **ppModel, int nPis)
int	Cnf_DataBestVar (Cnf_Dat_t *p, int *pSkip)
void	Cnf_Experiment1 ()
Vec_Int_t *	Cnf_GenRandLits (int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fVerbose)
void	Cnf_SplitCnfFile (char *pFileName, int nParts, int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fPrepro, int fVerbose)
void	Cnf_SplitCnfCleanup (int nParts)
void	Cnf_SplitSat (char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose)

Function Documentation

Aig_ManScanMapping()

Vec_Ptr_t * Aig_ManScanMapping	(	Cnf_Man_t *	p,
		int	fCollect )

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

Synopsis [Computes area, references, and nodes used in the mapping.]

Description [Collects the nodes in reverse topological order.]

SideEffects []

SeeAlso []

Definition at line 297 of file cnfUtil.c.

{
    Vec_Ptr_t *vMapped = NULL;
    Aig_Obj_t *pObj;
    int i;
    // clean all references
    Aig_ManForEachObj(p->pManAig, pObj, i)
        pObj->nRefs = 0;
    // allocate the array
    if (fCollect)
        vMapped = Vec_PtrAlloc(1000);
    // collect nodes reachable from POs in the DFS order through the best cuts
    p->aArea = 0;
    Aig_ManForEachCo(p->pManAig, pObj, i)
        p->aArea += Aig_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped);
    //    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
    return vMapped;
}

Here is the call graph for this function:

Aig_ManScanMapping_rec()

int Aig_ManScanMapping_rec	(	Cnf_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vMapped )

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

Synopsis [Computes area, references, and nodes used in the mapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file cnfUtil.c.

{
    Aig_Obj_t *pLeaf;
    Dar_Cut_t *pCutBest;
    int aArea, i;
    if (pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj))
        return 0;
    assert(Aig_ObjIsAnd(pObj));
    // collect the node first to derive pre-order
    if (vMapped)
        Vec_PtrPush(vMapped, pObj);
    // visit the transitive fanin of the selected cut
    if (pObj->fMarkB)
    {
        Vec_Ptr_t *vSuper = Vec_PtrAlloc(100);
        Aig_ObjCollectSuper(pObj, vSuper);
        aArea = Vec_PtrSize(vSuper) + 1;
        Vec_PtrForEachEntry(Aig_Obj_t *, vSuper, pLeaf, i)
            aArea += Aig_ManScanMapping_rec(p, Aig_Regular(pLeaf), vMapped);
        Vec_PtrFree(vSuper);
        pObj->fMarkB = 1;
    }
    else
    {
        pCutBest = Dar_ObjBestCut(pObj);
        aArea = Cnf_CutSopCost(p, pCutBest);
        Dar_CutForEachLeaf(p->pManAig, pCutBest, pLeaf, i)
            aArea += Aig_ManScanMapping_rec(p, pLeaf, vMapped);
    }
    return aArea;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_DataBestVar()

int Cnf_DataBestVar	(	Cnf_Dat_t *	p,
		int *	pSkip )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 690 of file cnfUtil.c.

{
    int *pNums = ABC_CALLOC(int, p->nVars);
    int i, *pLit, NumMax = -1, iVarMax = -1;
    for (i = 0; i < p->nClauses; i++)
        for (pLit = p->pClauses[i]; pLit < p->pClauses[i + 1]; pLit++)
            pNums[Abc_Lit2Var(*pLit)]++;
    for (i = 0; i < p->nVars; i++)
        if ((!pSkip || !pSkip[i]) && NumMax < pNums[i])
            NumMax = pNums[i], iVarMax = i;
    ABC_FREE(pNums);
    return iVarMax;
}

Here is the caller graph for this function:

Cnf_DataCollectCiSatNums()

Vec_Int_t * Cnf_DataCollectCiSatNums	(	Cnf_Dat_t *	pCnf,
		Aig_Man_t *	p )

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

Synopsis [Returns the array of CI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 407 of file cnfUtil.c.

{
    Vec_Int_t *vCiIds;
    Aig_Obj_t *pObj;
    int i;
    vCiIds = Vec_IntAlloc(Aig_ManCiNum(p));
    Aig_ManForEachCi(p, pObj, i)
        Vec_IntPush(vCiIds, pCnf->pVarNums[pObj->Id]);
    return vCiIds;
}

Here is the caller graph for this function:

Cnf_DataCollectCoSatNums()

Vec_Int_t * Cnf_DataCollectCoSatNums	(	Cnf_Dat_t *	pCnf,
		Aig_Man_t *	p )

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

Synopsis [Returns the array of CI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 429 of file cnfUtil.c.

{
    Vec_Int_t *vCoIds;
    Aig_Obj_t *pObj;
    int i;
    vCoIds = Vec_IntAlloc(Aig_ManCoNum(p));
    Aig_ManForEachCo(p, pObj, i)
        Vec_IntPush(vCoIds, pCnf->pVarNums[pObj->Id]);
    return vCoIds;
}

Here is the caller graph for this function:

Cnf_DataDeriveLitPolarities()

unsigned char * Cnf_DataDeriveLitPolarities

(

Cnf_Dat_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 451 of file cnfUtil.c.

{
    int i, c, iClaBeg, iClaEnd, *pLit;
    unsigned *pPols0 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan));
    unsigned *pPols1 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan));
    unsigned char *pPres = ABC_CALLOC(unsigned char, p->nClauses);
    for (i = 0; i < Aig_ManObjNumMax(p->pMan); i++)
    {
        if (p->pObj2Count[i] == 0)
            continue;
        iClaBeg = p->pObj2Clause[i];
        iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i];
        // go through the negative polarity clauses
        for (c = iClaBeg; c < iClaEnd; c++)
            for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
                if (Abc_LitIsCompl(p->pClauses[c][0]))
                    pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
                else
                    pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
        // record these clauses
        for (c = iClaBeg; c < iClaEnd; c++)
            for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
                if (Abc_LitIsCompl(p->pClauses[c][0]))
                    pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1))));
                else
                    pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1))));
        // clean negative polarity
        for (c = iClaBeg; c < iClaEnd; c++)
            for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
                pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0;
    }
    ABC_FREE(pPols0);
    ABC_FREE(pPols1);
    /*
    //    for ( c = 0; c < p->nClauses; c++ )
        for ( c = 0; c < 100; c++ )
        {
            printf( "Clause %6d : ", c );
            for ( i = 0; i < 4; i++ )
                printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
            printf( "  " );
            for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
                printf( "%6d ", *pLit );
            printf( "\n" );
        }
    */
    return pPres;
}

Cnf_DataReadFromFile()

Cnf_Dat_t * Cnf_DataReadFromFile

(

char *

pFileName

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 511 of file cnfUtil.c.

{
    int MaxLine = 1000000;
    int Var, Lit, nVars = -1, nClas = -1, i, Entry, iLine = 0;
    Cnf_Dat_t *pCnf = NULL;
    Vec_Int_t *vClas = NULL;
    Vec_Int_t *vLits = NULL;
    char *pBuffer, *pToken;
    FILE *pFile = fopen(pFileName, "rb");
    if (pFile == NULL)
    {
        printf("Cannot open file \"%s\" for writing.\n", pFileName);
        return NULL;
    }
    pBuffer = ABC_ALLOC(char, MaxLine);
    while (fgets(pBuffer, MaxLine, pFile) != NULL)
    {
        iLine++;
        if (pBuffer[0] == 'c')
            continue;
        if (pBuffer[0] == 'p')
        {
            pToken = strtok(pBuffer + 1, " \t");
            if (strcmp(pToken, "cnf"))
            {
                printf("Incorrect input file.\n");
                goto finish;
            }
            pToken = strtok(NULL, " \t");
            nVars = atoi(pToken);
            pToken = strtok(NULL, " \t");
            nClas = atoi(pToken);
            if (nVars <= 0 || nClas <= 0)
            {
                printf("Incorrect parameters.\n");
                goto finish;
            }
            // temp storage
            vClas = Vec_IntAlloc(nClas + 1);
            vLits = Vec_IntAlloc(nClas * 8);
            continue;
        }
        pToken = strtok(pBuffer, " \t\r\n");
        if (pToken == NULL)
            continue;
        Vec_IntPush(vClas, Vec_IntSize(vLits));
        while (pToken)
        {
            Var = atoi(pToken);
            if (Var == 0)
                break;
            Lit = (Var > 0) ? Abc_Var2Lit(Var - 1, 0) : Abc_Var2Lit(-Var - 1, 1);
            if (Lit >= 2 * nVars)
            {
                printf("Literal %d is out-of-bound for %d variables.\n", Lit, nVars);
                goto finish;
            }
            Vec_IntPush(vLits, Lit);
            pToken = strtok(NULL, " \t\r\n");
        }
        if (Var != 0)
        {
            printf("There is no zero-terminator in line %d.\n", iLine);
            goto finish;
        }
    }
    // finalize
    if (Vec_IntSize(vClas) != nClas)
        printf("Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas);
    Vec_IntPush(vClas, Vec_IntSize(vLits));
    // create
    pCnf = ABC_CALLOC(Cnf_Dat_t, 1);
    pCnf->nVars = nVars;
    pCnf->nClauses = Vec_IntSize(vClas) - 1;
    pCnf->nLiterals = Vec_IntSize(vLits);
    pCnf->pClauses = ABC_ALLOC(int *, Vec_IntSize(vClas));
    pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
    Vec_IntForEachEntry(vClas, Entry, i)
        pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
finish:
    fclose(pFile);
    Vec_IntFreeP(&vClas);
    Vec_IntFreeP(&vLits);
    ABC_FREE(pBuffer);
    return pCnf;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_DataSolveFromFile()

int Cnf_DataSolveFromFile	(	char *	pFileName,
		int	nConfLimit,
		int	nLearnedStart,
		int	nLearnedDelta,
		int	nLearnedPerce,
		int	fVerbose,
		int	fShowPattern,
		int **	ppModel,
		int	nPis )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 609 of file cnfUtil.c.

{
    abctime clk = Abc_Clock();
    Cnf_Dat_t *pCnf = Cnf_DataReadFromFile(pFileName);
    sat_solver *pSat;
    int i, status, RetValue = -1;
    if (pCnf == NULL)
        return -1;
    if (fVerbose)
    {
        printf("CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals);
        Abc_PrintTime(1, "Time", Abc_Clock() - clk);
    }
    // convert into SAT solver
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
    if (pSat == NULL)
    {
        printf("The problem is trivially UNSAT.\n");
        Cnf_DataFree(pCnf);
        return 1;
    }
    if (nLearnedStart)
        pSat->nLearntStart = pSat->nLearntMax = nLearnedStart;
    if (nLearnedDelta)
        pSat->nLearntDelta = nLearnedDelta;
    if (nLearnedPerce)
        pSat->nLearntRatio = nLearnedPerce;
    if (fVerbose)
        pSat->fVerbose = fVerbose;
 
    // sat_solver_start_cardinality( pSat, 100 );
 
    // solve the miter
    status = sat_solver_solve(pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0);
    if (status == l_Undef)
        RetValue = -1;
    else if (status == l_True)
        RetValue = 0;
    else if (status == l_False)
        RetValue = 1;
    else
        assert(0);
    if (fVerbose)
        Sat_SolverPrintStats(stdout, pSat);
    if (RetValue == -1)
        Abc_Print(1, "UNDECIDED      ");
    else if (RetValue == 0)
        Abc_Print(1, "SATISFIABLE    ");
    else
        Abc_Print(1, "UNSATISFIABLE  ");
    // Abc_Print( -1, "\n" );
    Abc_PrintTime(1, "Time", Abc_Clock() - clk);
    // derive SAT assignment
    if (RetValue == 0 && nPis > 0)
    {
        *ppModel = ABC_ALLOC(int, nPis);
        for (i = 0; i < nPis; i++)
            (*ppModel)[i] = sat_solver_var_value(pSat, pCnf->nVars - nPis + i);
    }
    if (RetValue == 0 && fShowPattern)
    {
        for (i = 0; i < pCnf->nVars; i++)
            printf("%d", sat_solver_var_value(pSat, i));
        printf("\n");
    }
    Cnf_DataFree(pCnf);
    sat_solver_delete(pSat);
    return RetValue;
}

Here is the call graph for this function:

Cnf_Experiment1()

void Cnf_Experiment1

(

)

Definition at line 703 of file cnfUtil.c.

{
    Cnf_Dat_t *pTemp, *p = Cnf_DataReadFromFile("../166b.cnf");
    int i, *pSkip = ABC_CALLOC(int, p->nVars);
    for (i = 0; i < 100; i++)
    {
        int iVar = Cnf_DataBestVar(p, pSkip);
        char FileName[100];
        sprintf(FileName, "cnf/%03d.cnf", i);
        Cnf_DataWriteIntoFile(p, FileName, 0, NULL, NULL);
        printf("Dumped file \"%s\".\n", FileName);
        p = Cnf_DataDupCof(pTemp = p, Abc_Var2Lit(iVar, 0));
        Cnf_DataFree(pTemp);
        pSkip[iVar] = 1;
    }
    Cnf_DataFree(p);
    ABC_FREE(pSkip);
}

Here is the call graph for this function:

Cnf_GenRandLits()

Vec_Int_t * Cnf_GenRandLits	(	int	iVarBeg,
		int	iVarEnd,
		int	nLits,
		int	Value,
		int	Rand,
		int	fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 733 of file cnfUtil.c.

{
    Vec_Int_t *vLits = Vec_IntAlloc(nLits);
    assert(iVarBeg < iVarEnd && nLits < iVarEnd - iVarBeg);
    while (Vec_IntSize(vLits) < nLits)
    {
        int iVar = iVarBeg + (Abc_Random(0) ^ Rand) % (iVarEnd - iVarBeg);
        assert(iVar >= iVarBeg && iVar < iVarEnd);
        if (Vec_IntFind(vLits, Abc_Var2Lit(iVar, 0)) == -1 && Vec_IntFind(vLits, Abc_Var2Lit(iVar, 1)) == -1)
        {
            if (Value == 0)
                Vec_IntPush(vLits, Abc_Var2Lit(iVar, 1));
            else if (Value == 1)
                Vec_IntPush(vLits, Abc_Var2Lit(iVar, 0));
            else
                Vec_IntPush(vLits, Abc_Var2Lit(iVar, Abc_Random(0) & 1));
        }
    }
    Vec_IntSort(vLits, 0);
    if ( fVerbose )
    Vec_IntPrint(vLits);
    fflush(stdout);
    return vLits;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_ManScanMapping()

Vec_Ptr_t * Cnf_ManScanMapping	(	Cnf_Man_t *	p,
		int	fCollect,
		int	fPreorder )

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

Synopsis [Computes area, references, and nodes used in the mapping.]

Description [Collects the nodes in reverse topological order.]

SideEffects []

SeeAlso []

Definition at line 377 of file cnfUtil.c.

{
    Vec_Ptr_t *vMapped = NULL;
    Aig_Obj_t *pObj;
    int i;
    // clean all references
    Aig_ManForEachObj(p->pManAig, pObj, i)
        pObj->nRefs = 0;
    // allocate the array
    if (fCollect)
        vMapped = Vec_PtrAlloc(1000);
    // collect nodes reachable from POs in the DFS order through the best cuts
    p->aArea = 0;
    Aig_ManForEachCo(p->pManAig, pObj, i)
        p->aArea += Cnf_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped, fPreorder);
    //    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
    return vMapped;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_ManScanMapping_rec()

int Cnf_ManScanMapping_rec	(	Cnf_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vMapped,
		int	fPreorder )

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

Synopsis [Computes area, references, and nodes used in the mapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 327 of file cnfUtil.c.

{
    Aig_Obj_t *pLeaf;
    Cnf_Cut_t *pCutBest;
    int aArea, i;
    if (pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj))
        return 0;
    assert(Aig_ObjIsAnd(pObj));
    assert(pObj->pData != NULL);
    // add the node to the mapping
    if (vMapped && fPreorder)
        Vec_PtrPush(vMapped, pObj);
    // visit the transitive fanin of the selected cut
    if (pObj->fMarkB)
    {
        Vec_Ptr_t *vSuper = Vec_PtrAlloc(100);
        Aig_ObjCollectSuper(pObj, vSuper);
        aArea = Vec_PtrSize(vSuper) + 1;
        Vec_PtrForEachEntry(Aig_Obj_t *, vSuper, pLeaf, i)
            aArea += Cnf_ManScanMapping_rec(p, Aig_Regular(pLeaf), vMapped, fPreorder);
        Vec_PtrFree(vSuper);
        pObj->fMarkB = 1;
    }
    else
    {
        pCutBest = (Cnf_Cut_t *)pObj->pData;
        //        assert( pCutBest->nFanins > 0 );
        assert(pCutBest->Cost < 127);
        aArea = pCutBest->Cost;
        Cnf_CutForEachLeaf(p->pManAig, pCutBest, pLeaf, i)
            aArea += Cnf_ManScanMapping_rec(p, pLeaf, vMapped, fPreorder);
    }
    // add the node to the mapping
    if (vMapped && !fPreorder)
        Vec_PtrPush(vMapped, pObj);
    return aArea;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_RunSolver()

Vec_Int_t * Cnf_RunSolver	(	int	nProcs,
		int	TimeOut,
		int	fVerbose )

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

Synopsis [Solving problems using many cores.]

Description []

SideEffects []

SeeAlso []

Definition at line 134 of file cnfUtil.c.

{
    return Cnf_RunSolverArray(nProcs, TimeOut, fVerbose);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_RunSolverArray()

Vec_Int_t * Cnf_RunSolverArray	(	int	nProcs,
		int	TimeOut,
		int	fVerbose )

Definition at line 112 of file cnfUtil.c.

{
    Vec_Int_t *vRes = NULL; int i;
    for ( i = 0; i < nProcs; i++ )
        if ((vRes = Cnf_RunSolverOnce(i, 0, TimeOut, fVerbose))) 
            break;
    return vRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_RunSolverOnce()

Vec_Int_t * Cnf_RunSolverOnce	(	int	Id,
		int	Rand,
		int	TimeOut,
		int	fVerbose )

FUNCTION DEFINITIONS ///.

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

Synopsis [Solving problems using one core.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file cnfUtil.c.

{
    int fVerboseSolver = 0;
    Vec_Int_t *vRes = NULL;
    abctime clkTotal = Abc_Clock();
    char FileNameIn[100], FileNameOut[100];
    sprintf(FileNameIn,  "%02d.cnf", Id);
    sprintf(FileNameOut, "%02d.txt", Id);
#ifdef _WIN32
    char *pKissat = "kissat.exe";
#else
    char *pKissat = "kissat";
#endif
    char Command[1000], *pCommand = (char *)&Command;
    if (TimeOut)
        sprintf(pCommand, "%s --seed=%d --time=%d %s %s > %s", pKissat, Rand, TimeOut, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut);
    else
        sprintf(pCommand, "%s --seed=%d %s %s > %s", pKissat, Rand, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut);
    //printf( "Thread command: %s\n", pCommand);
    FILE * pFile = fopen(FileNameIn, "rb");
    if ( pFile != NULL ) {
        fclose( pFile );
#if defined(__wasm)
        if ( 1 ) {
#else
        if (system(pCommand) == -1) {
#endif
            fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand);
            return 0;
        }
        vRes = Exa4_ManParse(FileNameOut); // FileNameOut is removed here
    }
    if (fVerbose) {
        double SolvingTime = ((double)(Abc_Clock() - clkTotal))/((double)CLOCKS_PER_SEC);
        if (vRes)
            printf("Problem %2d has a solution. ", Id);
        else if (vRes == NULL && (TimeOut == 0 || SolvingTime < (double)TimeOut))
            printf("Problem %2d has no solution. ", Id);
        else if (vRes == NULL)
            printf("Problem %2d has no solution or timed out after %d sec. ", Id, TimeOut);
        Abc_PrintTime(1, "Solving time", Abc_Clock() - clkTotal );
    }
    else if (vRes) {   
        printf("Problem %2d has a solution. ", Id);
        Abc_PrintTime(1, "Solving time", Abc_Clock() - clkTotal );
        printf("(Currently waiting for %d sec for other threads to finish.)\n", TimeOut);
    }
    return vRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_SplitCnfCleanup()

void Cnf_SplitCnfCleanup

(

int

nParts

)

Definition at line 788 of file cnfUtil.c.

{
    char FileName[100];  int k;
    for (k = 0; k < nParts; k++) {
        sprintf(FileName, "%02d.cnf", k);
        unlink(FileName);
    }   
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_SplitCnfFile()

void Cnf_SplitCnfFile	(	char *	pFileName,
		int	nParts,
		int	iVarBeg,
		int	iVarEnd,
		int	nLits,
		int	Value,
		int	Rand,
		int	fPrepro,
		int	fVerbose )

Definition at line 757 of file cnfUtil.c.

{
    Cnf_Dat_t *p = Cnf_DataReadFromFile(pFileName); int k;
    if (iVarEnd == ABC_INFINITY)
        iVarEnd = p->nVars;
    for (k = 0; k < nParts; k++)
    {
        Vec_Int_t *vLits = Cnf_GenRandLits(iVarBeg, iVarEnd, nLits, Value, Rand, fVerbose);
        Cnf_Dat_t *pCnf = Cnf_DataDupCofArray(p, vLits);
        char FileName[100];  sprintf(FileName, "%02d.cnf", k);
        if ( fPrepro ) {
            char Command[1000];   
            sprintf(Command, "satelite --verbosity=0 -pre temp.cnf %s", FileName);
            Cnf_DataWriteIntoFile(pCnf, "temp.cnf", 0, NULL, NULL);
#if defined(__wasm)
            if ( 1 ) {
#else
            if (system(Command) == -1) {
#endif
                fprintf(stdout, "Command \"%s\" did not succeed. Preprocessing skipped.\n", Command);
                Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
            }
            unlink("temp.cnf");
        }
        else 
            Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
        Cnf_DataFree(pCnf);
        Vec_IntFree(vLits);
    }    
    Cnf_DataFree(p);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_SplitSat()

void Cnf_SplitSat	(	char *	pFileName,
		int	iVarBeg,
		int	iVarEnd,
		int	nLits,
		int	Value,
		int	TimeOut,
		int	nProcs,
		int	nIters,
		int	Seed,
		int	fPrepro,
		int	fVerbose )

Definition at line 796 of file cnfUtil.c.

{
    abctime clk = Abc_Clock();
    Vec_Int_t *vSol = NULL;
    int i, Rand = 0;
    if ( nIters == 0 )
        nIters = ABC_INFINITY;
    Abc_Random(1);
    for ( i = 0; i < Seed; i++ )
        Abc_Random(0);
    Rand = Abc_Random(0);
    for (i = 0; i < nIters && !vSol; i++)
    {
        abctime clk2 = Abc_Clock();
        Cnf_SplitCnfFile(pFileName, nProcs, iVarBeg, iVarEnd, nLits, Value, Rand, fPrepro, fVerbose);
        vSol = Cnf_RunSolver(nProcs, TimeOut, fVerbose);
        Cnf_SplitCnfCleanup(nProcs);
        if (fVerbose) {
            printf( "Finished iteration %d.  ", i);    
            Abc_PrintTime(0, "Time", Abc_Clock() - clk2);
        }
    }
    printf("%solution is found.  ", vSol ? "S" : "No s");
    Abc_PrintTime(0, "Total time", Abc_Clock() - clk);
    Vec_IntFreeP(&vSol);
}

Here is the call graph for this function:

Exa4_ManParse()

ABC_NAMESPACE_IMPL_START Vec_Int_t * Exa4_ManParse ( char * pFileName )

extern

DECLARATIONS ///.

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

FileName [cnfUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG-to-CNF conversion.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id

cnfUtil.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1812 of file bmcMaj.c.

{
    Vec_Int_t * vRes = NULL;
    char * pToken, pBuffer[1000];
    FILE * pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        Abc_Print( -1, "Cannot open file \"%s\".\n", pFileName );
        return NULL;
    }
    while ( fgets( pBuffer, 1000, pFile ) != NULL )
    {
        if ( pBuffer[0] == 's' )
        {
            if ( strncmp(pBuffer+2, "SAT", 3) )
                break;
            assert( vRes == NULL );
            vRes = Vec_IntAlloc( 100 );
        }
        else if ( pBuffer[0] == 'v' )
        {
            pToken = strtok( pBuffer+1, " \n\r\t" );
            while ( pToken )
            {
                int Token = atoi(pToken);
                if ( Token == 0 )
                    break;
                Vec_IntSetEntryFull( vRes, Abc_AbsInt(Token), Token > 0 );
                pToken = strtok( NULL, " \n\r\t" );
            }
        }
        else if ( pBuffer[0] != 'c' )
            assert( 0 );
    }
    fclose( pFile );
    unlink( pFileName );
    return vRes;
}

Here is the call graph for this function:

Here is the caller graph for this function: