diff options
Diffstat (limited to 'src/sat')
58 files changed, 3972 insertions, 240 deletions
diff --git a/src/sat/bsat/satChecker.c b/src/sat/bsat/satChecker.c index 1488fe2f..041bc9ed 100644 --- a/src/sat/bsat/satChecker.c +++ b/src/sat/bsat/satChecker.c @@ -25,6 +25,9 @@ #include <time.h> #include "vec.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -185,3 +188,5 @@ void Sat_ProofChecker( char * pFileName ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c index 849ceb71..8617def9 100644 --- a/src/sat/bsat/satInter.c +++ b/src/sat/bsat/satInter.c @@ -25,6 +25,9 @@ #include <time.h> #include "satStore.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -222,7 +225,7 @@ void Int_ManResize( Int_Man_t * p ) p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); } - // clean the ABC_FREE space + // clean the free space memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); @@ -1070,3 +1073,5 @@ p->timeTotal += clock() - clkTotal; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index 5dcc7f0b..a635516c 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -26,6 +26,9 @@ #include "satStore.h" #include "aig.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -186,6 +189,7 @@ int Inta_ManGlobalVars( Inta_Man_t * p ) ***********************************************************************/ void Inta_ManResize( Inta_Man_t * p ) { + p->Counter = 0; // check if resizing is needed if ( p->nVarsAlloc < p->pCnf->nVars ) { @@ -203,7 +207,7 @@ void Inta_ManResize( Inta_Man_t * p ) p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); } - // clean the ABC_FREE space + // clean the free space memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); @@ -956,7 +960,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); p->pCnf = pCnf; p->fVerbose = fVerbose; - p->vVarsAB = vVarsAB; + p->vVarsAB = (Vec_Int_t *)vVarsAB; p->pAig = pRes = Aig_ManStart( 10000 ); Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 ); @@ -1071,3 +1075,5 @@ Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fCla //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satInterA_mod.c b/src/sat/bsat/satInterA_mod.c index faf396a6..199e9bd3 100644 --- a/src/sat/bsat/satInterA_mod.c +++ b/src/sat/bsat/satInterA_mod.c @@ -26,6 +26,9 @@ #include "satStore.h" #include "aig.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -1102,3 +1105,5 @@ Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fCla //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satInterA_old.c b/src/sat/bsat/satInterA_old.c index 57628989..02db6c79 100644 --- a/src/sat/bsat/satInterA_old.c +++ b/src/sat/bsat/satInterA_old.c @@ -26,6 +26,9 @@ #include "satStore.h" #include "aig.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -1045,3 +1048,5 @@ Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fCla //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satInterA_yu_hu.c b/src/sat/bsat/satInterA_yu_hu.c index aa2289f2..9afd2dd8 100644 --- a/src/sat/bsat/satInterA_yu_hu.c +++ b/src/sat/bsat/satInterA_yu_hu.c @@ -26,6 +26,9 @@ #include "satStore.h" #include "aig.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -1079,3 +1082,5 @@ Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fCla //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c index cb7f7828..1ffb0dc5 100644 --- a/src/sat/bsat/satInterB.c +++ b/src/sat/bsat/satInterB.c @@ -26,6 +26,9 @@ #include "satStore.h" #include "aig.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -188,6 +191,7 @@ int Intb_ManGlobalVars( Intb_Man_t * p ) ***********************************************************************/ void Intb_ManResize( Intb_Man_t * p ) { + p->Counter = 0; // check if resizing is needed if ( p->nVarsAlloc < p->pCnf->nVars ) { @@ -205,7 +209,7 @@ void Intb_ManResize( Intb_Man_t * p ) p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); } - // clean the ABC_FREE space + // clean the free space memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); @@ -232,7 +236,7 @@ void Intb_ManResize( Intb_Man_t * p ) if ( p->nIntersAlloc < p->pCnf->nClauses ) { p->nIntersAlloc = p->pCnf->nClauses; - p->pInters = ABC_REALLOC(Aig_Obj_t *, p->pInters, p->nIntersAlloc ); + p->pInters = ABC_REALLOC( Aig_Obj_t *, p->pInters, p->nIntersAlloc ); } memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses ); } @@ -550,7 +554,6 @@ int Intb_ManGetGlobalVar( Intb_Man_t * p, int Var ) return VarAB; } - /**Function************************************************************* Synopsis [Traces the proof for one clause.] @@ -608,7 +611,6 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF for ( v = 1; v < (int)pReason->nLits; v++ ) p->pSeens[lit_var(pReason->pLits[v])] = 1; - // record the reason clause assert( Intb_ManProofGet(p, pReason) > 0 ); p->Counter++; @@ -677,7 +679,6 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); } } - // Vec_PtrPush( pFinal->pAntis, pReason ); } @@ -710,6 +711,27 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF Intb_ManPrintResolvent( p->pResLits, p->nResLits ); Intb_ManPrintClause( p, pFinal ); } + + // if there are literals in the clause that are not in the resolvent + // it means that the derived resolvent is stronger than the clause + // we can replace the clause with the resolvent by removing these literals + if ( p->nResLits != (int)pFinal->nLits ) + { + for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ ) + { + for ( v2 = 0; v2 < p->nResLits; v2++ ) + if ( pFinal->pLits[v1] == p->pResLits[v2] ) + break; + if ( v2 < p->nResLits ) + continue; + // remove literal v1 from the final clause + pFinal->nLits--; + for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ ) + pFinal->pLits[v2] = pFinal->pLits[v2+1]; + v1--; + } + assert( p->nResLits == (int)pFinal->nLits ); + } } p->timeTrace += clock() - clk; @@ -719,6 +741,10 @@ p->timeTrace += clock() - clk; // Intb_ManPrintInterOne( p, pFinal ); } Intb_ManProofSet( p, pFinal, p->Counter ); + // make sure the same proof ID is not asssigned to two consecutive clauses + assert( p->pProofNums[pFinal->Id-1] != p->Counter ); +// if ( p->pProofNums[pFinal->Id] == p->pProofNums[pFinal->Id-1] ) +// p->pProofNums[pFinal->Id] = p->pProofNums[pConflict->Id]; return p->Counter; } @@ -743,9 +769,16 @@ int Intb_ManProofRecordOne( Intb_Man_t * p, Sto_Cls_t * pClause ) if ( pClause->nLits == 0 ) printf( "Error: Empty clause is attempted.\n" ); - // add assumptions to the trail assert( !pClause->fRoot ); assert( p->nTrailSize == p->nRootSize ); + + // if any of the clause literals are already assumed + // it means that the clause is redundant and can be skipped + for ( i = 0; i < (int)pClause->nLits; i++ ) + if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] ) + return 1; + + // add assumptions to the trail for ( i = 0; i < (int)pClause->nLits; i++ ) if ( !Intb_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) { @@ -759,6 +792,27 @@ int Intb_ManProofRecordOne( Intb_Man_t * p, Sto_Cls_t * pClause ) { assert( 0 ); // cannot prove return 0; + } + + // skip the clause if it is weaker or the same as the conflict clause + if ( pClause->nLits >= pConflict->nLits ) + { + // check if every literal of conflict clause can be found in the given clause + int j; + for ( i = 0; i < (int)pConflict->nLits; i++ ) + { + for ( j = 0; j < (int)pClause->nLits; j++ ) + if ( pConflict->pLits[i] == pClause->pLits[j] ) + break; + if ( j == (int)pClause->nLits ) // literal pConflict->pLits[i] is not found + break; + } + if ( i == (int)pConflict->nLits ) // all lits are found + { + // undo to the root level + Intb_ManCancelUntil( p, p->nRootSize ); + return 1; + } } // construct the proof @@ -846,8 +900,12 @@ int Intb_ManProcessRoots( Intb_Man_t * p ) if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) ) { // detected root level conflict - printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" ); - assert( 0 ); +// printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" ); +// assert( 0 ); + // detected root level conflict + Intb_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); return 0; } } @@ -895,7 +953,6 @@ void Intb_ManPrepareInter( Intb_Man_t * p ) } // clause of A Intb_ManAigClear( p, Intb_ManAigRead(p, pClause) ); - for ( v = 0; v < (int)pClause->nLits; v++ ) { Var = lit_var(pClause->pLits[v]); @@ -909,7 +966,6 @@ void Intb_ManPrepareInter( Intb_Man_t * p ) Intb_ManAigOrVar( p, Intb_ManAigRead(p, pClause), VarAB ); } } - // Intb_ManPrintInterOne( p, pClause ); } } @@ -940,7 +996,7 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); p->pCnf = pCnf; p->fVerbose = fVerbose; - p->vVarsAB = vVarsAB; + p->vVarsAB = (Vec_Int_t *)vVarsAB; p->pAig = pRes = Aig_ManStart( 10000 ); Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 ); @@ -980,8 +1036,9 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in // stop the proof if ( p->fProofWrite ) - { + { fclose( p->pFile ); +// Sat_ProofChecker( "proof.cnf_" ); p->pFile = NULL; } @@ -1004,6 +1061,7 @@ p->timeTotal += clock() - clkTotal; } + /**Function************************************************************* Synopsis [] @@ -1053,3 +1111,5 @@ Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fCla //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satInterB_.c b/src/sat/bsat/satInterB_.c new file mode 100644 index 00000000..ac005422 --- /dev/null +++ b/src/sat/bsat/satInterB_.c @@ -0,0 +1,1060 @@ +/**CFile**************************************************************** + + FileName [satInter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sat_solver.] + + Synopsis [Interpolation package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> +#include "satStore.h" +#include "aig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// variable assignments +static const lit LIT_UNDEF = 0xffffffff; + +// interpolation manager +struct Inta_Man_t_ +{ + // clauses of the problems + Sto_Man_t * pCnf; // the set of CNF clauses for A and B + Vec_Int_t * vVarsAB; // the array of global variables + // various parameters + int fVerbose; // verbosiness flag + int fProofVerif; // verifies the proof + int fProofWrite; // writes the proof file + int nVarsAlloc; // the allocated size of var arrays + int nClosAlloc; // the allocated size of clause arrays + // internal BCP + int nRootSize; // the number of root level assignments + int nTrailSize; // the number of assignments made + lit * pTrail; // chronological order of assignments (size nVars) + lit * pAssigns; // assignments by variable (size nVars) + char * pSeens; // temporary mark (size nVars) + Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars) + Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) + // interpolation data + Aig_Man_t * pAig; // the AIG manager for recording the interpolant + int * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] + Aig_Obj_t ** pInters; // storage for interpolants as truth tables (size nClauses) + int nIntersAlloc; // the allocated size of truth table array + // proof recording + int Counter; // counter of resolved clauses + int * pProofNums; // the proof numbers for each clause (size nClauses) + FILE * pFile; // the file for proof recording + // internal verification + lit * pResLits; // the literals of the resolvent + int nResLits; // the number of literals of the resolvent + int nResLitsAlloc;// the number of literals of the resolvent + // runtime stats + int timeBcp; // the runtime for BCP + int timeTrace; // the runtime of trace construction + int timeTotal; // the total runtime of interpolation +}; + +// procedure to get hold of the clauses' truth table +static inline Aig_Obj_t ** Inta_ManAigRead( Inta_Man_t * pMan, Sto_Cls_t * pCls ) { return pMan->pInters + pCls->Id; } +static inline void Inta_ManAigClear( Inta_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst0(pMan->pAig); } +static inline void Inta_ManAigFill( Inta_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst1(pMan->pAig); } +static inline void Inta_ManAigCopy( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = *q; } +static inline void Inta_ManAigAnd( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_And(pMan->pAig, *p, *q); } +static inline void Inta_ManAigOr( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, *q); } +static inline void Inta_ManAigOrNot( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); } +static inline void Inta_ManAigOrVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v)); } +static inline void Inta_ManAigOrNotVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); } +static inline void Inta_ManAigMux0( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *q, *p); } +static inline void Inta_ManAigMux1( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *p, *q); } + +// reading/writing the proof for a clause +static inline int Inta_ManProofGet( Inta_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; } +static inline void Inta_ManProofSet( Inta_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Inta_Man_t * Inta_ManAlloc() +{ + Inta_Man_t * p; + // allocate the manager + p = (Inta_Man_t *)ABC_ALLOC( char, sizeof(Inta_Man_t) ); + memset( p, 0, sizeof(Inta_Man_t) ); + // verification + p->nResLitsAlloc = (1<<16); + p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc ); + // parameters + p->fProofWrite = 0; + p->fProofVerif = 1; + return p; +} + +/**Function************************************************************* + + Synopsis [Count common variables in the clauses of A and B.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inta_ManGlobalVars( Inta_Man_t * p ) +{ + Sto_Cls_t * pClause; + int LargeNum = -100000000; + int Var, nVarsAB, v; + + // mark the variable encountered in the clauses of A + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( !pClause->fA ) + break; + for ( v = 0; v < (int)pClause->nLits; v++ ) + p->pVarTypes[lit_var(pClause->pLits[v])] = 1; + } + + // check variables that appear in clauses of B + nVarsAB = 0; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( pClause->fA ) + continue; + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] == 1 ) // var of A + { + // change it into a global variable + nVarsAB++; + p->pVarTypes[Var] = LargeNum; + } + } + } + assert( nVarsAB <= Vec_IntSize(p->vVarsAB) ); + + // order global variables + nVarsAB = 0; + Vec_IntForEachEntry( p->vVarsAB, Var, v ) + p->pVarTypes[Var] = -(1+nVarsAB++); + + // check that there is no extra global variables + for ( v = 0; v < p->pCnf->nVars; v++ ) + assert( p->pVarTypes[v] != LargeNum ); + return nVarsAB; +} + +/**Function************************************************************* + + Synopsis [Resize proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inta_ManResize( Inta_Man_t * p ) +{ + // check if resizing is needed + if ( p->nVarsAlloc < p->pCnf->nVars ) + { + // find the new size + if ( p->nVarsAlloc == 0 ) + p->nVarsAlloc = 1; + while ( p->nVarsAlloc < p->pCnf->nVars ) + p->nVarsAlloc *= 2; + // resize the arrays + p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); + p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); + p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); + p->pVarTypes = ABC_REALLOC(int, p->pVarTypes, p->nVarsAlloc ); + p->pReasons = ABC_REALLOC(Sto_Cls_t *, p->pReasons, p->nVarsAlloc ); + p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); + } + + // clean the free space + memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); + memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); + memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); + memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars ); + memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 ); + + // compute the number of common variables + Inta_ManGlobalVars( p ); + + // check if resizing of clauses is needed + if ( p->nClosAlloc < p->pCnf->nClauses ) + { + // find the new size + if ( p->nClosAlloc == 0 ) + p->nClosAlloc = 1; + while ( p->nClosAlloc < p->pCnf->nClauses ) + p->nClosAlloc *= 2; + // resize the arrays + p->pProofNums = ABC_REALLOC( int, p->pProofNums, p->nClosAlloc ); + } + memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); + + // check if resizing of truth tables is needed + if ( p->nIntersAlloc < p->pCnf->nClauses ) + { + p->nIntersAlloc = p->pCnf->nClauses; + p->pInters = ABC_REALLOC(Aig_Obj_t *, p->pInters, p->nIntersAlloc ); + } + memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses ); +} + +/**Function************************************************************* + + Synopsis [Deallocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inta_ManFree( Inta_Man_t * p ) +{ +/* + printf( "Runtime stats:\n" ); +ABC_PRT( "BCP ", p->timeBcp ); +ABC_PRT( "Trace ", p->timeTrace ); +ABC_PRT( "TOTAL ", p->timeTotal ); +*/ + ABC_FREE( p->pInters ); + ABC_FREE( p->pProofNums ); + ABC_FREE( p->pTrail ); + ABC_FREE( p->pAssigns ); + ABC_FREE( p->pSeens ); + ABC_FREE( p->pVarTypes ); + ABC_FREE( p->pReasons ); + ABC_FREE( p->pWatches ); + ABC_FREE( p->pResLits ); + ABC_FREE( p ); +} + + + + +/**Function************************************************************* + + Synopsis [Prints the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inta_ManPrintClause( Inta_Man_t * p, Sto_Cls_t * pClause ) +{ + int i; + printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Inta_ManProofGet(p, pClause) ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + printf( " %d", pClause->pLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the resolvent.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inta_ManPrintResolvent( lit * pResLits, int nResLits ) +{ + int i; + printf( "Resolvent: {" ); + for ( i = 0; i < nResLits; i++ ) + printf( " %d", pResLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the interpolant for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inta_ManPrintInterOne( Inta_Man_t * p, Sto_Cls_t * pClause ) +{ + printf( "Clause %2d : ", pClause->Id ); +// Extra_PrintBinary___( stdout, Inta_ManAigRead(p, pClause), (1 << p->nVarsAB) ); + printf( "\n" ); +} + + + +/**Function************************************************************* + + Synopsis [Adds one clause to the watcher list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Inta_ManWatchClause( Inta_Man_t * p, Sto_Cls_t * pClause, lit Lit ) +{ + assert( lit_check(Lit, p->pCnf->nVars) ); + if ( pClause->pLits[0] == Lit ) + pClause->pNext0 = p->pWatches[lit_neg(Lit)]; + else + { + assert( pClause->pLits[1] == Lit ); + pClause->pNext1 = p->pWatches[lit_neg(Lit)]; + } + p->pWatches[lit_neg(Lit)] = pClause; +} + + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Inta_ManEnqueue( Inta_Man_t * p, lit Lit, Sto_Cls_t * pReason ) +{ + int Var = lit_var(Lit); + if ( p->pAssigns[Var] != LIT_UNDEF ) + return p->pAssigns[Var] == Lit; + p->pAssigns[Var] = Lit; + p->pReasons[Var] = pReason; + p->pTrail[p->nTrailSize++] = Lit; +//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Inta_ManCancelUntil( Inta_Man_t * p, int Level ) +{ + lit Lit; + int i, Var; + for ( i = p->nTrailSize - 1; i >= Level; i-- ) + { + Lit = p->pTrail[i]; + Var = lit_var( Lit ); + p->pReasons[Var] = NULL; + p->pAssigns[Var] = LIT_UNDEF; +//printf( "cancelling var %d\n", Var ); + } + p->nTrailSize = Level; +} + +/**Function************************************************************* + + Synopsis [Propagate one assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Sto_Cls_t * Inta_ManPropagateOne( Inta_Man_t * p, lit Lit ) +{ + Sto_Cls_t ** ppPrev, * pCur, * pTemp; + lit LitF = lit_neg(Lit); + int i; + // iterate through the literals + ppPrev = p->pWatches + Lit; + for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev ) + { + // make sure the false literal is in the second literal of the clause + if ( pCur->pLits[0] == LitF ) + { + pCur->pLits[0] = pCur->pLits[1]; + pCur->pLits[1] = LitF; + pTemp = pCur->pNext0; + pCur->pNext0 = pCur->pNext1; + pCur->pNext1 = pTemp; + } + assert( pCur->pLits[1] == LitF ); + + // if the first literal is true, the clause is satisfied + if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // look for a new literal to watch + for ( i = 2; i < (int)pCur->nLits; i++ ) + { + // skip the case when the literal is false + if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) + continue; + // the literal is either true or unassigned - watch it + pCur->pLits[1] = pCur->pLits[i]; + pCur->pLits[i] = LitF; + // remove this clause from the watch list of Lit + *ppPrev = pCur->pNext1; + // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1]) + Inta_ManWatchClause( p, pCur, pCur->pLits[1] ); + break; + } + if ( i < (int)pCur->nLits ) // found new watch + continue; + + // clause is unit - enqueue new implication + if ( Inta_ManEnqueue(p, pCur->pLits[0], pCur) ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // conflict detected - return the conflict clause + return pCur; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Propagate the current assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sto_Cls_t * Inta_ManPropagate( Inta_Man_t * p, int Start ) +{ + Sto_Cls_t * pClause; + int i; + int clk = clock(); + for ( i = Start; i < p->nTrailSize; i++ ) + { + pClause = Inta_ManPropagateOne( p, p->pTrail[i] ); + if ( pClause ) + { +p->timeBcp += clock() - clk; + return pClause; + } + } +p->timeBcp += clock() - clk; + return NULL; +} + + +/**Function************************************************************* + + Synopsis [Writes one root clause into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inta_ManProofWriteOne( Inta_Man_t * p, Sto_Cls_t * pClause ) +{ + Inta_ManProofSet( p, pClause, ++p->Counter ); + + if ( p->fProofWrite ) + { + int v; + fprintf( p->pFile, "%d", Inta_ManProofGet(p, pClause) ); + for ( v = 0; v < (int)pClause->nLits; v++ ) + fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) ); + fprintf( p->pFile, " 0 0\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Traces the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inta_ManGetGlobalVar( Inta_Man_t * p, int Var ) +{ + int VarAB; + if ( p->pVarTypes[Var] >= 0 ) // global var + return -1; + VarAB = -p->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) ); + return VarAB; +} + + +/**Function************************************************************* + + Synopsis [Traces the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal ) +{ + Sto_Cls_t * pReason; + int i, v, Var, PrevId; + int fPrint = 0; + int clk = clock(); + + // collect resolvent literals + if ( p->fProofVerif ) + { + assert( (int)pConflict->nLits <= p->nResLitsAlloc ); + memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits ); + p->nResLits = pConflict->nLits; + } + + // mark all the variables in the conflict as seen + for ( v = 0; v < (int)pConflict->nLits; v++ ) + p->pSeens[lit_var(pConflict->pLits[v])] = 1; + + // start the anticedents +// pFinal->pAntis = Vec_PtrAlloc( 32 ); +// Vec_PtrPush( pFinal->pAntis, pConflict ); + + if ( p->pCnf->nClausesA ) + Inta_ManAigCopy( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pConflict) ); + + // follow the trail backwards + PrevId = Inta_ManProofGet(p, pConflict); + for ( i = p->nTrailSize - 1; i >= 0; i-- ) + { + // skip literals that are not involved + Var = lit_var(p->pTrail[i]); + if ( !p->pSeens[Var] ) + continue; + p->pSeens[Var] = 0; + + // skip literals of the resulting clause + pReason = p->pReasons[Var]; + if ( pReason == NULL ) + continue; + assert( p->pTrail[i] == pReason->pLits[0] ); + + // add the variables to seen + for ( v = 1; v < (int)pReason->nLits; v++ ) + p->pSeens[lit_var(pReason->pLits[v])] = 1; + + + // record the reason clause + assert( Inta_ManProofGet(p, pReason) > 0 ); + p->Counter++; + if ( p->fProofWrite ) + fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Inta_ManProofGet(p, pReason) ); + PrevId = p->Counter; + + if ( p->pCnf->nClausesA ) + { + if ( p->pVarTypes[Var] == 1 )// || rand() % 10 == 0 ) // var of A + Inta_ManAigOr( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) ); + else if ( p->pVarTypes[Var] == 0 ) // var of B + Inta_ManAigAnd( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) ); + else + { + int VarAB = Inta_ManGetGlobalVar(p, Var); + // check that the var is present in the reason + for ( v = 0; v < (int)pReason->nLits; v++ ) + if ( lit_var(pReason->pLits[v]) == Var ) + break; + assert( v < (int)pReason->nLits ); + if ( lit_sign(pReason->pLits[v]) ) // negative polarity + Inta_ManAigMux0( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason), VarAB ); + else + Inta_ManAigMux1( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason), VarAB ); + } + } + + // resolve the temporary resolvent with the reason clause + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Inta_ManPrintResolvent( p->pResLits, p->nResLits ); + // check that the var is present in the resolvent + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == Var ) + break; + if ( v1 == p->nResLits ) + printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var ); + if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) ) + printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var ); + // remove this variable from the resolvent + assert( lit_var(p->pResLits[v1]) == Var ); + p->nResLits--; + for ( ; v1 < p->nResLits; v1++ ) + p->pResLits[v1] = p->pResLits[v1+1]; + // add variables of the reason clause + for ( v2 = 1; v2 < (int)pReason->nLits; v2++ ) + { + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) ) + break; + // if it is a new variable, add it to the resolvent + if ( v1 == p->nResLits ) + { + if ( p->nResLits == p->nResLitsAlloc ) + printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id ); + p->pResLits[ p->nResLits++ ] = pReason->pLits[v2]; + continue; + } + // if the variable is the same, the literal should be the same too + if ( p->pResLits[v1] == pReason->pLits[v2] ) + continue; + // the literal is different + printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); + } + } + +// Vec_PtrPush( pFinal->pAntis, pReason ); + } + + // unmark all seen variables +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// p->pSeens[lit_var(p->pTrail[i])] = 0; + // check that the literals are unmarked +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 ); + + // use the resulting clause to check the correctness of resolution + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Inta_ManPrintResolvent( p->pResLits, p->nResLits ); + for ( v1 = 0; v1 < p->nResLits; v1++ ) + { + for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ ) + if ( pFinal->pLits[v2] == p->pResLits[v1] ) + break; + if ( v2 < (int)pFinal->nLits ) + continue; + break; + } + if ( v1 < p->nResLits ) + { + printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id ); + Inta_ManPrintClause( p, pConflict ); + Inta_ManPrintResolvent( p->pResLits, p->nResLits ); + Inta_ManPrintClause( p, pFinal ); + } + } +p->timeTrace += clock() - clk; + + // return the proof pointer + if ( p->pCnf->nClausesA ) + { +// Inta_ManPrintInterOne( p, pFinal ); + } + Inta_ManProofSet( p, pFinal, p->Counter ); + return p->Counter; +} + +/**Function************************************************************* + + Synopsis [Records the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inta_ManProofRecordOne( Inta_Man_t * p, Sto_Cls_t * pClause ) +{ + Sto_Cls_t * pConflict; + int i; + + // empty clause never ends up there + assert( pClause->nLits > 0 ); + if ( pClause->nLits == 0 ) + printf( "Error: Empty clause is attempted.\n" ); + + // add assumptions to the trail + assert( !pClause->fRoot ); + assert( p->nTrailSize == p->nRootSize ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + if ( !Inta_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumptions + pConflict = Inta_ManPropagate( p, p->nRootSize ); + if ( pConflict == NULL ) + { + assert( 0 ); // cannot prove + return 0; + } + + // construct the proof + Inta_ManProofTraceOne( p, pConflict, pClause ); + + // undo to the root level + Inta_ManCancelUntil( p, p->nRootSize ); + + // add large clauses to the watched lists + if ( pClause->nLits > 1 ) + { + Inta_ManWatchClause( p, pClause, pClause->pLits[0] ); + Inta_ManWatchClause( p, pClause, pClause->pLits[1] ); + return 1; + } + assert( pClause->nLits == 1 ); + + // if the clause proved is unit, add it and propagate + if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumption + pConflict = Inta_ManPropagate( p, p->nRootSize ); + if ( pConflict ) + { + // construct the proof + Inta_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty ); +// if ( p->fVerbose ) +// printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); + return 0; + } + + // update the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Propagate the root clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inta_ManProcessRoots( Inta_Man_t * p ) +{ + Sto_Cls_t * pClause; + int Counter; + + // make sure the root clauses are preceeding the learnt clauses + Counter = 0; + Sto_ManForEachClause( p->pCnf, pClause ) + { + assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) ); + assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) ); + Counter++; + } + assert( p->pCnf->nClauses == Counter ); + + // make sure the last clause if empty + assert( p->pCnf->pTail->nLits == 0 ); + + // go through the root unit clauses + p->nTrailSize = 0; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + // create watcher lists for the root clauses + if ( pClause->nLits > 1 ) + { + Inta_ManWatchClause( p, pClause, pClause->pLits[0] ); + Inta_ManWatchClause( p, pClause, pClause->pLits[1] ); + } + // empty clause and large clauses + if ( pClause->nLits != 1 ) + continue; + // unit clause + assert( lit_check(pClause->pLits[0], p->pCnf->nVars) ); + if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + // detected root level conflict + printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" ); + assert( 0 ); + return 0; + } + } + + // propagate the root unit clauses + pClause = Inta_ManPropagate( p, 0 ); + if ( pClause ) + { + // detected root level conflict + Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); + return 0; + } + + // set the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inta_ManPrepareInter( Inta_Man_t * p ) +{ + Sto_Cls_t * pClause; + int Var, VarAB, v; + + // set interpolants for root clauses + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( !pClause->fA ) // clause of B + { + Inta_ManAigFill( p, Inta_ManAigRead(p, pClause) ); +// Inta_ManPrintInterOne( p, pClause ); + continue; + } + // clause of A + Inta_ManAigClear( p, Inta_ManAigRead(p, pClause) ); + + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] < 0 ) // global var + { + VarAB = -p->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) ); + if ( lit_sign(pClause->pLits[v]) ) // negative var + Inta_ManAigOrNotVar( p, Inta_ManAigRead(p, pClause), VarAB ); + else + Inta_ManAigOrVar( p, Inta_ManAigRead(p, pClause), VarAB ); + } + } + +// Inta_ManPrintInterOne( p, pClause ); + } +} + +/**Function************************************************************* + + Synopsis [Computes interpolant for the given CNF.] + + Description [Takes the interpolation manager, the CNF deriving by the SAT + solver, which includes ClausesA, ClausesB, and learned clauses. Additional + arguments are the vector of variables common to AB and the verbosiness flag. + Returns the AIG manager with a single output, containing the interpolant.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose ) +{ + Aig_Man_t * pRes; + Aig_Obj_t * pObj; + Sto_Cls_t * pClause; + int RetValue = 1; + int clkTotal = clock(); + + // check that the CNF makes sense + assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); + p->pCnf = pCnf; + p->fVerbose = fVerbose; + p->vVarsAB = vVarsAB; + p->pAig = pRes = Aig_ManStart( 10000 ); + Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 ); + + // adjust the manager + Inta_ManResize( p ); + + // prepare the interpolant computation + Inta_ManPrepareInter( p ); + + // construct proof for each clause + // start the proof + if ( p->fProofWrite ) + { + p->pFile = fopen( "proof.cnf_", "w" ); + p->Counter = 0; + } + + // write the root clauses + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + Inta_ManProofWriteOne( p, pClause ); + + // propagate root level assignments + if ( Inta_ManProcessRoots( p ) ) + { + // if there is no conflict, consider learned clauses + Sto_ManForEachClause( p->pCnf, pClause ) + { + if ( pClause->fRoot ) + continue; + if ( !Inta_ManProofRecordOne( p, pClause ) ) + { + RetValue = 0; + break; + } + } + } + + // stop the proof + if ( p->fProofWrite ) + { + fclose( p->pFile ); + p->pFile = NULL; + } + + if ( fVerbose ) + { +// ABC_PRT( "Interpo", clock() - clkTotal ); + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", + p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, + 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), + 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); +p->timeTotal += clock() - clkTotal; + } + + pObj = *Inta_ManAigRead( p, p->pCnf->pTail ); + Aig_ObjCreatePo( pRes, pObj ); + Aig_ManCleanup( pRes ); + + p->pAig = NULL; + return pRes; + +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ) +{ + Aig_Man_t * p; + Aig_Obj_t * pMiter, * pSum, * pLit; + Sto_Cls_t * pClause; + int Var, VarAB, v; + p = Aig_ManStart( 10000 ); + pMiter = Aig_ManConst1(p); + Sto_ManForEachClauseRoot( pCnf, pClause ) + { + if ( fClausesA ^ pClause->fA ) // clause of B + continue; + // clause of A + pSum = Aig_ManConst0(p); + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( pMan->pVarTypes[Var] < 0 ) // global var + { + VarAB = -pMan->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) ); + pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) ); + } + else + pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) ); + pSum = Aig_Or( p, pSum, pLit ); + } + pMiter = Aig_And( p, pMiter, pSum ); + } + Aig_ObjCreatePo( p, pMiter ); + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satInterB_new.c b/src/sat/bsat/satInterB_new.c new file mode 100644 index 00000000..f6f54c8c --- /dev/null +++ b/src/sat/bsat/satInterB_new.c @@ -0,0 +1,1115 @@ +/**CFile**************************************************************** + + FileName [satInter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sat_solver.] + + Synopsis [Interpolation package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> +#include "satStore.h" +#include "aig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// variable assignments +static const lit LIT_UNDEF = 0xffffffff; + +// interpolation manager +struct Intb_Man_t_ +{ + // clauses of the problems + Sto_Man_t * pCnf; // the set of CNF clauses for A and B + Vec_Int_t * vVarsAB; // the array of global variables + // various parameters + int fVerbose; // verbosiness flag + int fProofVerif; // verifies the proof + int fProofWrite; // writes the proof file + int nVarsAlloc; // the allocated size of var arrays + int nClosAlloc; // the allocated size of clause arrays + // internal BCP + int nRootSize; // the number of root level assignments + int nTrailSize; // the number of assignments made + lit * pTrail; // chronological order of assignments (size nVars) + lit * pAssigns; // assignments by variable (size nVars) + char * pSeens; // temporary mark (size nVars) + Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars) + Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) + // interpolation data + Aig_Man_t * pAig; // the AIG manager for recording the interpolant + int * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] + Aig_Obj_t ** pInters; // storage for interpolants as truth tables (size nClauses) + int nIntersAlloc; // the allocated size of truth table array + // proof recording + int Counter; // counter of resolved clauses + int * pProofNums; // the proof numbers for each clause (size nClauses) + FILE * pFile; // the file for proof recording + // internal verification + lit * pResLits; // the literals of the resolvent + int nResLits; // the number of literals of the resolvent + int nResLitsAlloc;// the number of literals of the resolvent + // runtime stats + int timeBcp; // the runtime for BCP + int timeTrace; // the runtime of trace construction + int timeTotal; // the total runtime of interpolation +}; + +// procedure to get hold of the clauses' truth table +static inline Aig_Obj_t ** Intb_ManAigRead( Intb_Man_t * pMan, Sto_Cls_t * pCls ) { return pMan->pInters + pCls->Id; } +static inline void Intb_ManAigClear( Intb_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst0(pMan->pAig); } +static inline void Intb_ManAigFill( Intb_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst1(pMan->pAig); } +static inline void Intb_ManAigCopy( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = *q; } +static inline void Intb_ManAigAnd( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_And(pMan->pAig, *p, *q); } +static inline void Intb_ManAigOr( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, *q); } +static inline void Intb_ManAigOrNot( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); } +static inline void Intb_ManAigOrVar( Intb_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v)); } +static inline void Intb_ManAigOrNotVar( Intb_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); } +static inline void Intb_ManAigMux0( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *q, *p); } +static inline void Intb_ManAigMux1( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *p, *q); } + +// reading/writing the proof for a clause +static inline int Intb_ManProofGet( Intb_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; } +static inline void Intb_ManProofSet( Intb_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Intb_Man_t * Intb_ManAlloc() +{ + Intb_Man_t * p; + // allocate the manager + p = (Intb_Man_t *)ABC_ALLOC( char, sizeof(Intb_Man_t) ); + memset( p, 0, sizeof(Intb_Man_t) ); + // verification + p->nResLitsAlloc = (1<<16); + p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc ); + // parameters + p->fProofWrite = 0; + p->fProofVerif = 1; + return p; +} + +/**Function************************************************************* + + Synopsis [Count common variables in the clauses of A and B.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManGlobalVars( Intb_Man_t * p ) +{ + Sto_Cls_t * pClause; + int LargeNum = -100000000; + int Var, nVarsAB, v; + + // mark the variable encountered in the clauses of A + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( !pClause->fA ) + break; + for ( v = 0; v < (int)pClause->nLits; v++ ) + p->pVarTypes[lit_var(pClause->pLits[v])] = 1; + } + + // check variables that appear in clauses of B + nVarsAB = 0; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( pClause->fA ) + continue; + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] == 1 ) // var of A + { + // change it into a global variable + nVarsAB++; + p->pVarTypes[Var] = LargeNum; + } + } + } + assert( nVarsAB <= Vec_IntSize(p->vVarsAB) ); + + // order global variables + nVarsAB = 0; + Vec_IntForEachEntry( p->vVarsAB, Var, v ) + p->pVarTypes[Var] = -(1+nVarsAB++); + + // check that there is no extra global variables + for ( v = 0; v < p->pCnf->nVars; v++ ) + assert( p->pVarTypes[v] != LargeNum ); + return nVarsAB; +} + +/**Function************************************************************* + + Synopsis [Resize proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManResize( Intb_Man_t * p ) +{ + p->Counter = 0; + // check if resizing is needed + if ( p->nVarsAlloc < p->pCnf->nVars ) + { + // find the new size + if ( p->nVarsAlloc == 0 ) + p->nVarsAlloc = 1; + while ( p->nVarsAlloc < p->pCnf->nVars ) + p->nVarsAlloc *= 2; + // resize the arrays + p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); + p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); + p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); + p->pVarTypes = ABC_REALLOC(int, p->pVarTypes, p->nVarsAlloc ); + p->pReasons = ABC_REALLOC(Sto_Cls_t *, p->pReasons, p->nVarsAlloc ); + p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); + } + + // clean the free space + memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); + memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); + memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); + memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars ); + memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 ); + + // compute the number of common variables + Intb_ManGlobalVars( p ); + + // check if resizing of clauses is needed + if ( p->nClosAlloc < p->pCnf->nClauses ) + { + // find the new size + if ( p->nClosAlloc == 0 ) + p->nClosAlloc = 1; + while ( p->nClosAlloc < p->pCnf->nClauses ) + p->nClosAlloc *= 2; + // resize the arrays + p->pProofNums = ABC_REALLOC( int, p->pProofNums, p->nClosAlloc ); + } + memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); + + // check if resizing of truth tables is needed + if ( p->nIntersAlloc < p->pCnf->nClauses ) + { + p->nIntersAlloc = p->pCnf->nClauses; + p->pInters = ABC_REALLOC( Aig_Obj_t *, p->pInters, p->nIntersAlloc ); + } + memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses ); +} + +/**Function************************************************************* + + Synopsis [Deallocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManFree( Intb_Man_t * p ) +{ +/* + printf( "Runtime stats:\n" ); +ABC_PRT( "BCP ", p->timeBcp ); +ABC_PRT( "Trace ", p->timeTrace ); +ABC_PRT( "TOTAL ", p->timeTotal ); +*/ + ABC_FREE( p->pInters ); + ABC_FREE( p->pProofNums ); + ABC_FREE( p->pTrail ); + ABC_FREE( p->pAssigns ); + ABC_FREE( p->pSeens ); + ABC_FREE( p->pVarTypes ); + ABC_FREE( p->pReasons ); + ABC_FREE( p->pWatches ); + ABC_FREE( p->pResLits ); + ABC_FREE( p ); +} + + + + +/**Function************************************************************* + + Synopsis [Prints the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrintClause( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + int i; + printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Intb_ManProofGet(p, pClause) ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + printf( " %d", pClause->pLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the resolvent.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrintResolvent( lit * pResLits, int nResLits ) +{ + int i; + printf( "Resolvent: {" ); + for ( i = 0; i < nResLits; i++ ) + printf( " %d", pResLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the interpolant for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrintInterOne( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + printf( "Clause %2d : ", pClause->Id ); +// Extra_PrintBinary___( stdout, Intb_ManAigRead(p, pClause), (1 << p->nVarsAB) ); + printf( "\n" ); +} + + + +/**Function************************************************************* + + Synopsis [Adds one clause to the watcher list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Intb_ManWatchClause( Intb_Man_t * p, Sto_Cls_t * pClause, lit Lit ) +{ + assert( lit_check(Lit, p->pCnf->nVars) ); + if ( pClause->pLits[0] == Lit ) + pClause->pNext0 = p->pWatches[lit_neg(Lit)]; + else + { + assert( pClause->pLits[1] == Lit ); + pClause->pNext1 = p->pWatches[lit_neg(Lit)]; + } + p->pWatches[lit_neg(Lit)] = pClause; +} + + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Intb_ManEnqueue( Intb_Man_t * p, lit Lit, Sto_Cls_t * pReason ) +{ + int Var = lit_var(Lit); + if ( p->pAssigns[Var] != LIT_UNDEF ) + return p->pAssigns[Var] == Lit; + p->pAssigns[Var] = Lit; + p->pReasons[Var] = pReason; + p->pTrail[p->nTrailSize++] = Lit; +//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Intb_ManCancelUntil( Intb_Man_t * p, int Level ) +{ + lit Lit; + int i, Var; + for ( i = p->nTrailSize - 1; i >= Level; i-- ) + { + Lit = p->pTrail[i]; + Var = lit_var( Lit ); + p->pReasons[Var] = NULL; + p->pAssigns[Var] = LIT_UNDEF; +//printf( "cancelling var %d\n", Var ); + } + p->nTrailSize = Level; +} + +/**Function************************************************************* + + Synopsis [Propagate one assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Sto_Cls_t * Intb_ManPropagateOne( Intb_Man_t * p, lit Lit ) +{ + Sto_Cls_t ** ppPrev, * pCur, * pTemp; + lit LitF = lit_neg(Lit); + int i; + // iterate through the literals + ppPrev = p->pWatches + Lit; + for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev ) + { + // make sure the false literal is in the second literal of the clause + if ( pCur->pLits[0] == LitF ) + { + pCur->pLits[0] = pCur->pLits[1]; + pCur->pLits[1] = LitF; + pTemp = pCur->pNext0; + pCur->pNext0 = pCur->pNext1; + pCur->pNext1 = pTemp; + } + assert( pCur->pLits[1] == LitF ); + + // if the first literal is true, the clause is satisfied + if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // look for a new literal to watch + for ( i = 2; i < (int)pCur->nLits; i++ ) + { + // skip the case when the literal is false + if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) + continue; + // the literal is either true or unassigned - watch it + pCur->pLits[1] = pCur->pLits[i]; + pCur->pLits[i] = LitF; + // remove this clause from the watch list of Lit + *ppPrev = pCur->pNext1; + // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1]) + Intb_ManWatchClause( p, pCur, pCur->pLits[1] ); + break; + } + if ( i < (int)pCur->nLits ) // found new watch + continue; + + // clause is unit - enqueue new implication + if ( Intb_ManEnqueue(p, pCur->pLits[0], pCur) ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // conflict detected - return the conflict clause + return pCur; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Propagate the current assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sto_Cls_t * Intb_ManPropagate( Intb_Man_t * p, int Start ) +{ + Sto_Cls_t * pClause; + int i; + int clk = clock(); + for ( i = Start; i < p->nTrailSize; i++ ) + { + pClause = Intb_ManPropagateOne( p, p->pTrail[i] ); + if ( pClause ) + { +p->timeBcp += clock() - clk; + return pClause; + } + } +p->timeBcp += clock() - clk; + return NULL; +} + + +/**Function************************************************************* + + Synopsis [Writes one root clause into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManProofWriteOne( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + Intb_ManProofSet( p, pClause, ++p->Counter ); + + if ( p->fProofWrite ) + { + int v; + fprintf( p->pFile, "%d", Intb_ManProofGet(p, pClause) ); + for ( v = 0; v < (int)pClause->nLits; v++ ) + fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) ); + fprintf( p->pFile, " 0 0\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Traces the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManGetGlobalVar( Intb_Man_t * p, int Var ) +{ + int VarAB; + if ( p->pVarTypes[Var] >= 0 ) // global var + return -1; + VarAB = -p->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) ); + return VarAB; +} + +/**Function************************************************************* + + Synopsis [Traces the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal ) +{ + Sto_Cls_t * pReason; + int i, v, Var, PrevId; + int fPrint = 0; + int clk = clock(); + + // collect resolvent literals + if ( p->fProofVerif ) + { + assert( (int)pConflict->nLits <= p->nResLitsAlloc ); + memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits ); + p->nResLits = pConflict->nLits; + } + + // mark all the variables in the conflict as seen + for ( v = 0; v < (int)pConflict->nLits; v++ ) + p->pSeens[lit_var(pConflict->pLits[v])] = 1; + + // start the anticedents +// pFinal->pAntis = Vec_PtrAlloc( 32 ); +// Vec_PtrPush( pFinal->pAntis, pConflict ); + + if ( p->pCnf->nClausesA ) + Intb_ManAigCopy( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pConflict) ); + + // follow the trail backwards + PrevId = Intb_ManProofGet(p, pConflict); + for ( i = p->nTrailSize - 1; i >= 0; i-- ) + { + // skip literals that are not involved + Var = lit_var(p->pTrail[i]); + if ( !p->pSeens[Var] ) + continue; + p->pSeens[Var] = 0; + + // skip literals of the resulting clause + pReason = p->pReasons[Var]; + if ( pReason == NULL ) + continue; + assert( p->pTrail[i] == pReason->pLits[0] ); + + // add the variables to seen + for ( v = 1; v < (int)pReason->nLits; v++ ) + p->pSeens[lit_var(pReason->pLits[v])] = 1; + + // record the reason clause + assert( Intb_ManProofGet(p, pReason) > 0 ); + p->Counter++; + if ( p->fProofWrite ) + fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Intb_ManProofGet(p, pReason) ); + PrevId = p->Counter; + + if ( p->pCnf->nClausesA ) + { + if ( p->pVarTypes[Var] == 1 )// || rand() % 10 == 0 ) // var of A + Intb_ManAigOr( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason) ); + else if ( p->pVarTypes[Var] == 0 ) // var of B + Intb_ManAigAnd( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason) ); + else + { + int VarAB = Intb_ManGetGlobalVar(p, Var); + // check that the var is present in the reason + for ( v = 0; v < (int)pReason->nLits; v++ ) + if ( lit_var(pReason->pLits[v]) == Var ) + break; + assert( v < (int)pReason->nLits ); + if ( lit_sign(pReason->pLits[v]) ) // negative polarity + Intb_ManAigMux0( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason), VarAB ); + else + Intb_ManAigMux1( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason), VarAB ); + } + } + + // resolve the temporary resolvent with the reason clause + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Intb_ManPrintResolvent( p->pResLits, p->nResLits ); + // check that the var is present in the resolvent + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == Var ) + break; + if ( v1 == p->nResLits ) + printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var ); + if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) ) + printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var ); + // remove this variable from the resolvent + assert( lit_var(p->pResLits[v1]) == Var ); + p->nResLits--; + for ( ; v1 < p->nResLits; v1++ ) + p->pResLits[v1] = p->pResLits[v1+1]; + // add variables of the reason clause + for ( v2 = 1; v2 < (int)pReason->nLits; v2++ ) + { + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) ) + break; + // if it is a new variable, add it to the resolvent + if ( v1 == p->nResLits ) + { + if ( p->nResLits == p->nResLitsAlloc ) + printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id ); + p->pResLits[ p->nResLits++ ] = pReason->pLits[v2]; + continue; + } + // if the variable is the same, the literal should be the same too + if ( p->pResLits[v1] == pReason->pLits[v2] ) + continue; + // the literal is different + printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); + } + } +// Vec_PtrPush( pFinal->pAntis, pReason ); + } + + // unmark all seen variables +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// p->pSeens[lit_var(p->pTrail[i])] = 0; + // check that the literals are unmarked +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 ); + + // use the resulting clause to check the correctness of resolution + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Intb_ManPrintResolvent( p->pResLits, p->nResLits ); + for ( v1 = 0; v1 < p->nResLits; v1++ ) + { + for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ ) + if ( pFinal->pLits[v2] == p->pResLits[v1] ) + break; + if ( v2 < (int)pFinal->nLits ) + continue; + break; + } + if ( v1 < p->nResLits ) + { + printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id ); + Intb_ManPrintClause( p, pConflict ); + Intb_ManPrintResolvent( p->pResLits, p->nResLits ); + Intb_ManPrintClause( p, pFinal ); + } + + // if there are literals in the clause that are not in the resolvent + // it means that the derived resolvent is stronger than the clause + // we can replace the clause with the resolvent by removing these literals + if ( p->nResLits != (int)pFinal->nLits ) + { + for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ ) + { + for ( v2 = 0; v2 < p->nResLits; v2++ ) + if ( pFinal->pLits[v1] == p->pResLits[v2] ) + break; + if ( v2 < p->nResLits ) + continue; + // remove literal v1 from the final clause + pFinal->nLits--; + for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ ) + pFinal->pLits[v2] = pFinal->pLits[v2+1]; + v1--; + } + assert( p->nResLits == (int)pFinal->nLits ); + } + } +p->timeTrace += clock() - clk; + + // return the proof pointer + if ( p->pCnf->nClausesA ) + { +// Intb_ManPrintInterOne( p, pFinal ); + } + Intb_ManProofSet( p, pFinal, p->Counter ); + // make sure the same proof ID is not asssigned to two consecutive clauses + assert( p->pProofNums[pFinal->Id-1] != p->Counter ); +// if ( p->pProofNums[pFinal->Id] == p->pProofNums[pFinal->Id-1] ) +// p->pProofNums[pFinal->Id] = p->pProofNums[pConflict->Id]; + return p->Counter; +} + +/**Function************************************************************* + + Synopsis [Records the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManProofRecordOne( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + Sto_Cls_t * pConflict; + int i; + + // empty clause never ends up there + assert( pClause->nLits > 0 ); + if ( pClause->nLits == 0 ) + printf( "Error: Empty clause is attempted.\n" ); + + assert( !pClause->fRoot ); + assert( p->nTrailSize == p->nRootSize ); + + // if any of the clause literals are already assumed + // it means that the clause is redundant and can be skipped + for ( i = 0; i < (int)pClause->nLits; i++ ) + if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] ) + return 1; + + // add assumptions to the trail + for ( i = 0; i < (int)pClause->nLits; i++ ) + if ( !Intb_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumptions + pConflict = Intb_ManPropagate( p, p->nRootSize ); + if ( pConflict == NULL ) + { + assert( 0 ); // cannot prove + return 0; + } + + // skip the clause if it is weaker or the same as the conflict clause + if ( pClause->nLits >= pConflict->nLits ) + { + // check if every literal of conflict clause can be found in the given clause + int j; + for ( i = 0; i < (int)pConflict->nLits; i++ ) + { + for ( j = 0; j < (int)pClause->nLits; j++ ) + if ( pConflict->pLits[i] == pClause->pLits[j] ) + break; + if ( j == (int)pClause->nLits ) // literal pConflict->pLits[i] is not found + break; + } + if ( i == (int)pConflict->nLits ) // all lits are found + { + // undo to the root level + Intb_ManCancelUntil( p, p->nRootSize ); + return 1; + } + } + + // construct the proof + Intb_ManProofTraceOne( p, pConflict, pClause ); + + // undo to the root level + Intb_ManCancelUntil( p, p->nRootSize ); + + // add large clauses to the watched lists + if ( pClause->nLits > 1 ) + { + Intb_ManWatchClause( p, pClause, pClause->pLits[0] ); + Intb_ManWatchClause( p, pClause, pClause->pLits[1] ); + return 1; + } + assert( pClause->nLits == 1 ); + + // if the clause proved is unit, add it and propagate + if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumption + pConflict = Intb_ManPropagate( p, p->nRootSize ); + if ( pConflict ) + { + // construct the proof + Intb_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty ); +// if ( p->fVerbose ) +// printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); + return 0; + } + + // update the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Propagate the root clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManProcessRoots( Intb_Man_t * p ) +{ + Sto_Cls_t * pClause; + int Counter; + + // make sure the root clauses are preceeding the learnt clauses + Counter = 0; + Sto_ManForEachClause( p->pCnf, pClause ) + { + assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) ); + assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) ); + Counter++; + } + assert( p->pCnf->nClauses == Counter ); + + // make sure the last clause if empty + assert( p->pCnf->pTail->nLits == 0 ); + + // go through the root unit clauses + p->nTrailSize = 0; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + // create watcher lists for the root clauses + if ( pClause->nLits > 1 ) + { + Intb_ManWatchClause( p, pClause, pClause->pLits[0] ); + Intb_ManWatchClause( p, pClause, pClause->pLits[1] ); + } + // empty clause and large clauses + if ( pClause->nLits != 1 ) + continue; + // unit clause + assert( lit_check(pClause->pLits[0], p->pCnf->nVars) ); + if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + // detected root level conflict +// printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" ); +// assert( 0 ); + // detected root level conflict + Intb_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); + return 0; + } + } + + // propagate the root unit clauses + pClause = Intb_ManPropagate( p, 0 ); + if ( pClause ) + { + // detected root level conflict + Intb_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); + return 0; + } + + // set the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrepareInter( Intb_Man_t * p ) +{ + Sto_Cls_t * pClause; + int Var, VarAB, v; + + // set interpolants for root clauses + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( !pClause->fA ) // clause of B + { + Intb_ManAigFill( p, Intb_ManAigRead(p, pClause) ); +// Intb_ManPrintInterOne( p, pClause ); + continue; + } + // clause of A + Intb_ManAigClear( p, Intb_ManAigRead(p, pClause) ); + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] < 0 ) // global var + { + VarAB = -p->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) ); + if ( lit_sign(pClause->pLits[v]) ) // negative var + Intb_ManAigOrNotVar( p, Intb_ManAigRead(p, pClause), VarAB ); + else + Intb_ManAigOrVar( p, Intb_ManAigRead(p, pClause), VarAB ); + } + } +// Intb_ManPrintInterOne( p, pClause ); + } +} + +/**Function************************************************************* + + Synopsis [Computes interpolant for the given CNF.] + + Description [Takes the interpolation manager, the CNF deriving by the SAT + solver, which includes ClausesA, ClausesB, and learned clauses. Additional + arguments are the vector of variables common to AB and the verbosiness flag. + Returns the AIG manager with a single output, containing the interpolant.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose ) +{ + Aig_Man_t * pRes; + Aig_Obj_t * pObj; + Sto_Cls_t * pClause; + int RetValue = 1; + int clkTotal = clock(); + + // check that the CNF makes sense + assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); + p->pCnf = pCnf; + p->fVerbose = fVerbose; + p->vVarsAB = vVarsAB; + p->pAig = pRes = Aig_ManStart( 10000 ); + Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 ); + + // adjust the manager + Intb_ManResize( p ); + + // prepare the interpolant computation + Intb_ManPrepareInter( p ); + + // construct proof for each clause + // start the proof + if ( p->fProofWrite ) + { + p->pFile = fopen( "proof.cnf_", "w" ); + p->Counter = 0; + } + + // write the root clauses + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + Intb_ManProofWriteOne( p, pClause ); + + // propagate root level assignments + if ( Intb_ManProcessRoots( p ) ) + { + // if there is no conflict, consider learned clauses + Sto_ManForEachClause( p->pCnf, pClause ) + { + if ( pClause->fRoot ) + continue; + if ( !Intb_ManProofRecordOne( p, pClause ) ) + { + RetValue = 0; + break; + } + } + } + + // stop the proof + if ( p->fProofWrite ) + { + fclose( p->pFile ); +// Sat_ProofChecker( "proof.cnf_" ); + p->pFile = NULL; + } + + if ( fVerbose ) + { +// ABC_PRT( "Interpo", clock() - clkTotal ); + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", + p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, + 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), + 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); +p->timeTotal += clock() - clkTotal; + } + + pObj = *Intb_ManAigRead( p, p->pCnf->pTail ); + Aig_ObjCreatePo( pRes, pObj ); + Aig_ManCleanup( pRes ); + + p->pAig = NULL; + return pRes; + +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ) +{ + Aig_Man_t * p; + Aig_Obj_t * pMiter, * pSum, * pLit; + Sto_Cls_t * pClause; + int Var, VarAB, v; + p = Aig_ManStart( 10000 ); + pMiter = Aig_ManConst1(p); + Sto_ManForEachClauseRoot( pCnf, pClause ) + { + if ( fClausesA ^ pClause->fA ) // clause of B + continue; + // clause of A + pSum = Aig_ManConst0(p); + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( pMan->pVarTypes[Var] < 0 ) // global var + { + VarAB = -pMan->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) ); + pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) ); + } + else + pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) ); + pSum = Aig_Or( p, pSum, pLit ); + } + pMiter = Aig_And( p, pMiter, pSum ); + } + Aig_ObjCreatePo( p, pMiter ); + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satInterB_old.c b/src/sat/bsat/satInterB_old.c new file mode 100644 index 00000000..2afc9855 --- /dev/null +++ b/src/sat/bsat/satInterB_old.c @@ -0,0 +1,1061 @@ +/**CFile**************************************************************** + + FileName [satInter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sat_solver.] + + Synopsis [Interpolation package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> +#include "satStore.h" +#include "aig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// variable assignments +static const lit LIT_UNDEF = 0xffffffff; + +// interpolation manager +struct Intb_Man_t_ +{ + // clauses of the problems + Sto_Man_t * pCnf; // the set of CNF clauses for A and B + Vec_Int_t * vVarsAB; // the array of global variables + // various parameters + int fVerbose; // verbosiness flag + int fProofVerif; // verifies the proof + int fProofWrite; // writes the proof file + int nVarsAlloc; // the allocated size of var arrays + int nClosAlloc; // the allocated size of clause arrays + // internal BCP + int nRootSize; // the number of root level assignments + int nTrailSize; // the number of assignments made + lit * pTrail; // chronological order of assignments (size nVars) + lit * pAssigns; // assignments by variable (size nVars) + char * pSeens; // temporary mark (size nVars) + Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars) + Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) + // interpolation data + Aig_Man_t * pAig; // the AIG manager for recording the interpolant + int * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] + Aig_Obj_t ** pInters; // storage for interpolants as truth tables (size nClauses) + int nIntersAlloc; // the allocated size of truth table array + // proof recording + int Counter; // counter of resolved clauses + int * pProofNums; // the proof numbers for each clause (size nClauses) + FILE * pFile; // the file for proof recording + // internal verification + lit * pResLits; // the literals of the resolvent + int nResLits; // the number of literals of the resolvent + int nResLitsAlloc;// the number of literals of the resolvent + // runtime stats + int timeBcp; // the runtime for BCP + int timeTrace; // the runtime of trace construction + int timeTotal; // the total runtime of interpolation +}; + +// procedure to get hold of the clauses' truth table +static inline Aig_Obj_t ** Intb_ManAigRead( Intb_Man_t * pMan, Sto_Cls_t * pCls ) { return pMan->pInters + pCls->Id; } +static inline void Intb_ManAigClear( Intb_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst0(pMan->pAig); } +static inline void Intb_ManAigFill( Intb_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst1(pMan->pAig); } +static inline void Intb_ManAigCopy( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = *q; } +static inline void Intb_ManAigAnd( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_And(pMan->pAig, *p, *q); } +static inline void Intb_ManAigOr( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, *q); } +static inline void Intb_ManAigOrNot( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); } +static inline void Intb_ManAigOrVar( Intb_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v)); } +static inline void Intb_ManAigOrNotVar( Intb_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); } +static inline void Intb_ManAigMux0( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *q, *p); } +static inline void Intb_ManAigMux1( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *p, *q); } + +// reading/writing the proof for a clause +static inline int Intb_ManProofGet( Intb_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; } +static inline void Intb_ManProofSet( Intb_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Intb_Man_t * Intb_ManAlloc() +{ + Intb_Man_t * p; + // allocate the manager + p = (Intb_Man_t *)ABC_ALLOC( char, sizeof(Intb_Man_t) ); + memset( p, 0, sizeof(Intb_Man_t) ); + // verification + p->nResLitsAlloc = (1<<16); + p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc ); + // parameters + p->fProofWrite = 0; + p->fProofVerif = 1; + return p; +} + +/**Function************************************************************* + + Synopsis [Count common variables in the clauses of A and B.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManGlobalVars( Intb_Man_t * p ) +{ + Sto_Cls_t * pClause; + int LargeNum = -100000000; + int Var, nVarsAB, v; + + // mark the variable encountered in the clauses of A + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( !pClause->fA ) + break; + for ( v = 0; v < (int)pClause->nLits; v++ ) + p->pVarTypes[lit_var(pClause->pLits[v])] = 1; + } + + // check variables that appear in clauses of B + nVarsAB = 0; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( pClause->fA ) + continue; + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] == 1 ) // var of A + { + // change it into a global variable + nVarsAB++; + p->pVarTypes[Var] = LargeNum; + } + } + } + assert( nVarsAB <= Vec_IntSize(p->vVarsAB) ); + + // order global variables + nVarsAB = 0; + Vec_IntForEachEntry( p->vVarsAB, Var, v ) + p->pVarTypes[Var] = -(1+nVarsAB++); + + // check that there is no extra global variables + for ( v = 0; v < p->pCnf->nVars; v++ ) + assert( p->pVarTypes[v] != LargeNum ); + return nVarsAB; +} + +/**Function************************************************************* + + Synopsis [Resize proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManResize( Intb_Man_t * p ) +{ + p->Counter = 0; + // check if resizing is needed + if ( p->nVarsAlloc < p->pCnf->nVars ) + { + // find the new size + if ( p->nVarsAlloc == 0 ) + p->nVarsAlloc = 1; + while ( p->nVarsAlloc < p->pCnf->nVars ) + p->nVarsAlloc *= 2; + // resize the arrays + p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); + p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); + p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); + p->pVarTypes = ABC_REALLOC(int, p->pVarTypes, p->nVarsAlloc ); + p->pReasons = ABC_REALLOC(Sto_Cls_t *, p->pReasons, p->nVarsAlloc ); + p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); + } + + // clean the free space + memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); + memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); + memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); + memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars ); + memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 ); + + // compute the number of common variables + Intb_ManGlobalVars( p ); + + // check if resizing of clauses is needed + if ( p->nClosAlloc < p->pCnf->nClauses ) + { + // find the new size + if ( p->nClosAlloc == 0 ) + p->nClosAlloc = 1; + while ( p->nClosAlloc < p->pCnf->nClauses ) + p->nClosAlloc *= 2; + // resize the arrays + p->pProofNums = ABC_REALLOC( int, p->pProofNums, p->nClosAlloc ); + } + memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); + + // check if resizing of truth tables is needed + if ( p->nIntersAlloc < p->pCnf->nClauses ) + { + p->nIntersAlloc = p->pCnf->nClauses; + p->pInters = ABC_REALLOC(Aig_Obj_t *, p->pInters, p->nIntersAlloc ); + } + memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses ); +} + +/**Function************************************************************* + + Synopsis [Deallocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManFree( Intb_Man_t * p ) +{ +/* + printf( "Runtime stats:\n" ); +ABC_PRT( "BCP ", p->timeBcp ); +ABC_PRT( "Trace ", p->timeTrace ); +ABC_PRT( "TOTAL ", p->timeTotal ); +*/ + ABC_FREE( p->pInters ); + ABC_FREE( p->pProofNums ); + ABC_FREE( p->pTrail ); + ABC_FREE( p->pAssigns ); + ABC_FREE( p->pSeens ); + ABC_FREE( p->pVarTypes ); + ABC_FREE( p->pReasons ); + ABC_FREE( p->pWatches ); + ABC_FREE( p->pResLits ); + ABC_FREE( p ); +} + + + + +/**Function************************************************************* + + Synopsis [Prints the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrintClause( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + int i; + printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Intb_ManProofGet(p, pClause) ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + printf( " %d", pClause->pLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the resolvent.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrintResolvent( lit * pResLits, int nResLits ) +{ + int i; + printf( "Resolvent: {" ); + for ( i = 0; i < nResLits; i++ ) + printf( " %d", pResLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the interpolant for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrintInterOne( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + printf( "Clause %2d : ", pClause->Id ); +// Extra_PrintBinary___( stdout, Intb_ManAigRead(p, pClause), (1 << p->nVarsAB) ); + printf( "\n" ); +} + + + +/**Function************************************************************* + + Synopsis [Adds one clause to the watcher list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Intb_ManWatchClause( Intb_Man_t * p, Sto_Cls_t * pClause, lit Lit ) +{ + assert( lit_check(Lit, p->pCnf->nVars) ); + if ( pClause->pLits[0] == Lit ) + pClause->pNext0 = p->pWatches[lit_neg(Lit)]; + else + { + assert( pClause->pLits[1] == Lit ); + pClause->pNext1 = p->pWatches[lit_neg(Lit)]; + } + p->pWatches[lit_neg(Lit)] = pClause; +} + + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Intb_ManEnqueue( Intb_Man_t * p, lit Lit, Sto_Cls_t * pReason ) +{ + int Var = lit_var(Lit); + if ( p->pAssigns[Var] != LIT_UNDEF ) + return p->pAssigns[Var] == Lit; + p->pAssigns[Var] = Lit; + p->pReasons[Var] = pReason; + p->pTrail[p->nTrailSize++] = Lit; +//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Intb_ManCancelUntil( Intb_Man_t * p, int Level ) +{ + lit Lit; + int i, Var; + for ( i = p->nTrailSize - 1; i >= Level; i-- ) + { + Lit = p->pTrail[i]; + Var = lit_var( Lit ); + p->pReasons[Var] = NULL; + p->pAssigns[Var] = LIT_UNDEF; +//printf( "cancelling var %d\n", Var ); + } + p->nTrailSize = Level; +} + +/**Function************************************************************* + + Synopsis [Propagate one assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Sto_Cls_t * Intb_ManPropagateOne( Intb_Man_t * p, lit Lit ) +{ + Sto_Cls_t ** ppPrev, * pCur, * pTemp; + lit LitF = lit_neg(Lit); + int i; + // iterate through the literals + ppPrev = p->pWatches + Lit; + for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev ) + { + // make sure the false literal is in the second literal of the clause + if ( pCur->pLits[0] == LitF ) + { + pCur->pLits[0] = pCur->pLits[1]; + pCur->pLits[1] = LitF; + pTemp = pCur->pNext0; + pCur->pNext0 = pCur->pNext1; + pCur->pNext1 = pTemp; + } + assert( pCur->pLits[1] == LitF ); + + // if the first literal is true, the clause is satisfied + if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // look for a new literal to watch + for ( i = 2; i < (int)pCur->nLits; i++ ) + { + // skip the case when the literal is false + if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) + continue; + // the literal is either true or unassigned - watch it + pCur->pLits[1] = pCur->pLits[i]; + pCur->pLits[i] = LitF; + // remove this clause from the watch list of Lit + *ppPrev = pCur->pNext1; + // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1]) + Intb_ManWatchClause( p, pCur, pCur->pLits[1] ); + break; + } + if ( i < (int)pCur->nLits ) // found new watch + continue; + + // clause is unit - enqueue new implication + if ( Intb_ManEnqueue(p, pCur->pLits[0], pCur) ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // conflict detected - return the conflict clause + return pCur; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Propagate the current assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sto_Cls_t * Intb_ManPropagate( Intb_Man_t * p, int Start ) +{ + Sto_Cls_t * pClause; + int i; + int clk = clock(); + for ( i = Start; i < p->nTrailSize; i++ ) + { + pClause = Intb_ManPropagateOne( p, p->pTrail[i] ); + if ( pClause ) + { +p->timeBcp += clock() - clk; + return pClause; + } + } +p->timeBcp += clock() - clk; + return NULL; +} + + +/**Function************************************************************* + + Synopsis [Writes one root clause into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManProofWriteOne( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + Intb_ManProofSet( p, pClause, ++p->Counter ); + + if ( p->fProofWrite ) + { + int v; + fprintf( p->pFile, "%d", Intb_ManProofGet(p, pClause) ); + for ( v = 0; v < (int)pClause->nLits; v++ ) + fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) ); + fprintf( p->pFile, " 0 0\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Traces the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManGetGlobalVar( Intb_Man_t * p, int Var ) +{ + int VarAB; + if ( p->pVarTypes[Var] >= 0 ) // global var + return -1; + VarAB = -p->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) ); + return VarAB; +} + + +/**Function************************************************************* + + Synopsis [Traces the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal ) +{ + Sto_Cls_t * pReason; + int i, v, Var, PrevId; + int fPrint = 0; + int clk = clock(); + + // collect resolvent literals + if ( p->fProofVerif ) + { + assert( (int)pConflict->nLits <= p->nResLitsAlloc ); + memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits ); + p->nResLits = pConflict->nLits; + } + + // mark all the variables in the conflict as seen + for ( v = 0; v < (int)pConflict->nLits; v++ ) + p->pSeens[lit_var(pConflict->pLits[v])] = 1; + + // start the anticedents +// pFinal->pAntis = Vec_PtrAlloc( 32 ); +// Vec_PtrPush( pFinal->pAntis, pConflict ); + + if ( p->pCnf->nClausesA ) + Intb_ManAigCopy( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pConflict) ); + + // follow the trail backwards + PrevId = Intb_ManProofGet(p, pConflict); + for ( i = p->nTrailSize - 1; i >= 0; i-- ) + { + // skip literals that are not involved + Var = lit_var(p->pTrail[i]); + if ( !p->pSeens[Var] ) + continue; + p->pSeens[Var] = 0; + + // skip literals of the resulting clause + pReason = p->pReasons[Var]; + if ( pReason == NULL ) + continue; + assert( p->pTrail[i] == pReason->pLits[0] ); + + // add the variables to seen + for ( v = 1; v < (int)pReason->nLits; v++ ) + p->pSeens[lit_var(pReason->pLits[v])] = 1; + + + // record the reason clause + assert( Intb_ManProofGet(p, pReason) > 0 ); + p->Counter++; + if ( p->fProofWrite ) + fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Intb_ManProofGet(p, pReason) ); + PrevId = p->Counter; + + if ( p->pCnf->nClausesA ) + { + if ( p->pVarTypes[Var] == 1 )// || rand() % 10 == 0 ) // var of A + Intb_ManAigOr( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason) ); + else if ( p->pVarTypes[Var] == 0 ) // var of B + Intb_ManAigAnd( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason) ); + else + { + int VarAB = Intb_ManGetGlobalVar(p, Var); + // check that the var is present in the reason + for ( v = 0; v < (int)pReason->nLits; v++ ) + if ( lit_var(pReason->pLits[v]) == Var ) + break; + assert( v < (int)pReason->nLits ); + if ( lit_sign(pReason->pLits[v]) ) // negative polarity + Intb_ManAigMux0( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason), VarAB ); + else + Intb_ManAigMux1( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason), VarAB ); + } + } + + // resolve the temporary resolvent with the reason clause + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Intb_ManPrintResolvent( p->pResLits, p->nResLits ); + // check that the var is present in the resolvent + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == Var ) + break; + if ( v1 == p->nResLits ) + printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var ); + if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) ) + printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var ); + // remove this variable from the resolvent + assert( lit_var(p->pResLits[v1]) == Var ); + p->nResLits--; + for ( ; v1 < p->nResLits; v1++ ) + p->pResLits[v1] = p->pResLits[v1+1]; + // add variables of the reason clause + for ( v2 = 1; v2 < (int)pReason->nLits; v2++ ) + { + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) ) + break; + // if it is a new variable, add it to the resolvent + if ( v1 == p->nResLits ) + { + if ( p->nResLits == p->nResLitsAlloc ) + printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id ); + p->pResLits[ p->nResLits++ ] = pReason->pLits[v2]; + continue; + } + // if the variable is the same, the literal should be the same too + if ( p->pResLits[v1] == pReason->pLits[v2] ) + continue; + // the literal is different + printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); + } + } + +// Vec_PtrPush( pFinal->pAntis, pReason ); + } + + // unmark all seen variables +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// p->pSeens[lit_var(p->pTrail[i])] = 0; + // check that the literals are unmarked +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 ); + + // use the resulting clause to check the correctness of resolution + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Intb_ManPrintResolvent( p->pResLits, p->nResLits ); + for ( v1 = 0; v1 < p->nResLits; v1++ ) + { + for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ ) + if ( pFinal->pLits[v2] == p->pResLits[v1] ) + break; + if ( v2 < (int)pFinal->nLits ) + continue; + break; + } + if ( v1 < p->nResLits ) + { + printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id ); + Intb_ManPrintClause( p, pConflict ); + Intb_ManPrintResolvent( p->pResLits, p->nResLits ); + Intb_ManPrintClause( p, pFinal ); + } + } +p->timeTrace += clock() - clk; + + // return the proof pointer + if ( p->pCnf->nClausesA ) + { +// Intb_ManPrintInterOne( p, pFinal ); + } + Intb_ManProofSet( p, pFinal, p->Counter ); + return p->Counter; +} + +/**Function************************************************************* + + Synopsis [Records the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManProofRecordOne( Intb_Man_t * p, Sto_Cls_t * pClause ) +{ + Sto_Cls_t * pConflict; + int i; + + // empty clause never ends up there + assert( pClause->nLits > 0 ); + if ( pClause->nLits == 0 ) + printf( "Error: Empty clause is attempted.\n" ); + + // add assumptions to the trail + assert( !pClause->fRoot ); + assert( p->nTrailSize == p->nRootSize ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + if ( !Intb_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumptions + pConflict = Intb_ManPropagate( p, p->nRootSize ); + if ( pConflict == NULL ) + { + assert( 0 ); // cannot prove + return 0; + } + + // construct the proof + Intb_ManProofTraceOne( p, pConflict, pClause ); + + // undo to the root level + Intb_ManCancelUntil( p, p->nRootSize ); + + // add large clauses to the watched lists + if ( pClause->nLits > 1 ) + { + Intb_ManWatchClause( p, pClause, pClause->pLits[0] ); + Intb_ManWatchClause( p, pClause, pClause->pLits[1] ); + return 1; + } + assert( pClause->nLits == 1 ); + + // if the clause proved is unit, add it and propagate + if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumption + pConflict = Intb_ManPropagate( p, p->nRootSize ); + if ( pConflict ) + { + // construct the proof + Intb_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty ); +// if ( p->fVerbose ) +// printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); + return 0; + } + + // update the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Propagate the root clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Intb_ManProcessRoots( Intb_Man_t * p ) +{ + Sto_Cls_t * pClause; + int Counter; + + // make sure the root clauses are preceeding the learnt clauses + Counter = 0; + Sto_ManForEachClause( p->pCnf, pClause ) + { + assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) ); + assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) ); + Counter++; + } + assert( p->pCnf->nClauses == Counter ); + + // make sure the last clause if empty + assert( p->pCnf->pTail->nLits == 0 ); + + // go through the root unit clauses + p->nTrailSize = 0; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + // create watcher lists for the root clauses + if ( pClause->nLits > 1 ) + { + Intb_ManWatchClause( p, pClause, pClause->pLits[0] ); + Intb_ManWatchClause( p, pClause, pClause->pLits[1] ); + } + // empty clause and large clauses + if ( pClause->nLits != 1 ) + continue; + // unit clause + assert( lit_check(pClause->pLits[0], p->pCnf->nVars) ); + if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + // detected root level conflict + printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" ); + assert( 0 ); + return 0; + } + } + + // propagate the root unit clauses + pClause = Intb_ManPropagate( p, 0 ); + if ( pClause ) + { + // detected root level conflict + Intb_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); + return 0; + } + + // set the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Intb_ManPrepareInter( Intb_Man_t * p ) +{ + Sto_Cls_t * pClause; + int Var, VarAB, v; + + // set interpolants for root clauses + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( !pClause->fA ) // clause of B + { + Intb_ManAigFill( p, Intb_ManAigRead(p, pClause) ); +// Intb_ManPrintInterOne( p, pClause ); + continue; + } + // clause of A + Intb_ManAigClear( p, Intb_ManAigRead(p, pClause) ); + + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] < 0 ) // global var + { + VarAB = -p->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) ); + if ( lit_sign(pClause->pLits[v]) ) // negative var + Intb_ManAigOrNotVar( p, Intb_ManAigRead(p, pClause), VarAB ); + else + Intb_ManAigOrVar( p, Intb_ManAigRead(p, pClause), VarAB ); + } + } + +// Intb_ManPrintInterOne( p, pClause ); + } +} + +/**Function************************************************************* + + Synopsis [Computes interpolant for the given CNF.] + + Description [Takes the interpolation manager, the CNF deriving by the SAT + solver, which includes ClausesA, ClausesB, and learned clauses. Additional + arguments are the vector of variables common to AB and the verbosiness flag. + Returns the AIG manager with a single output, containing the interpolant.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose ) +{ + Aig_Man_t * pRes; + Aig_Obj_t * pObj; + Sto_Cls_t * pClause; + int RetValue = 1; + int clkTotal = clock(); + + // check that the CNF makes sense + assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); + p->pCnf = pCnf; + p->fVerbose = fVerbose; + p->vVarsAB = vVarsAB; + p->pAig = pRes = Aig_ManStart( 10000 ); + Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 ); + + // adjust the manager + Intb_ManResize( p ); + + // prepare the interpolant computation + Intb_ManPrepareInter( p ); + + // construct proof for each clause + // start the proof + if ( p->fProofWrite ) + { + p->pFile = fopen( "proof.cnf_", "w" ); + p->Counter = 0; + } + + // write the root clauses + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + Intb_ManProofWriteOne( p, pClause ); + + // propagate root level assignments + if ( Intb_ManProcessRoots( p ) ) + { + // if there is no conflict, consider learned clauses + Sto_ManForEachClause( p->pCnf, pClause ) + { + if ( pClause->fRoot ) + continue; + if ( !Intb_ManProofRecordOne( p, pClause ) ) + { + RetValue = 0; + break; + } + } + } + + // stop the proof + if ( p->fProofWrite ) + { + fclose( p->pFile ); + p->pFile = NULL; + } + + if ( fVerbose ) + { +// ABC_PRT( "Interpo", clock() - clkTotal ); + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", + p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, + 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), + 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); +p->timeTotal += clock() - clkTotal; + } + + pObj = *Intb_ManAigRead( p, p->pCnf->pTail ); + Aig_ObjCreatePo( pRes, pObj ); + Aig_ManCleanup( pRes ); + + p->pAig = NULL; + return pRes; + +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ) +{ + Aig_Man_t * p; + Aig_Obj_t * pMiter, * pSum, * pLit; + Sto_Cls_t * pClause; + int Var, VarAB, v; + p = Aig_ManStart( 10000 ); + pMiter = Aig_ManConst1(p); + Sto_ManForEachClauseRoot( pCnf, pClause ) + { + if ( fClausesA ^ pClause->fA ) // clause of B + continue; + // clause of A + pSum = Aig_ManConst0(p); + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( pMan->pVarTypes[Var] < 0 ) // global var + { + VarAB = -pMan->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) ); + pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) ); + } + else + pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) ); + pSum = Aig_Or( p, pSum, pLit ); + } + pMiter = Aig_And( p, pMiter, pSum ); + } + Aig_ObjCreatePo( p, pMiter ); + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c index 57fb79d2..76f6982d 100644 --- a/src/sat/bsat/satInterP.c +++ b/src/sat/bsat/satInterP.c @@ -27,6 +27,9 @@ #include "satStore.h" #include "vec.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -54,8 +57,10 @@ struct Intp_Man_t_ Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars) Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) // proof data - Vec_Int_t * vAnties; // anticedents for all clauses - Vec_Int_t * vBreaks; // beginnings of anticedents for each clause +// Vec_Int_t * vAnties; // anticedents for all clauses +// Vec_Int_t * vBreaks; // beginnings of anticedents for each clause + Vec_Ptr_t * vAntClas; // anticedant clauses + int nAntStart; // starting antecedant clause // proof recording int Counter; // counter of resolved clauses int * pProofNums; // the proof numbers for each clause (size nClauses) @@ -99,8 +104,10 @@ Intp_Man_t * Intp_ManAlloc() p->nResLitsAlloc = (1<<16); p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc ); // proof recording - p->vAnties = Vec_IntAlloc( 1000 ); - p->vBreaks = Vec_IntAlloc( 1000 ); +// p->vAnties = Vec_IntAlloc( 1000 ); +// p->vBreaks = Vec_IntAlloc( 1000 ); + p->vAntClas = Vec_PtrAlloc( 1000 ); + p->nAntStart = 0; // parameters p->fProofWrite = 0; p->fProofVerif = 1; @@ -137,7 +144,7 @@ void Intp_ManResize( Intp_Man_t * p ) p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); } - // clean the ABC_FREE space + // clean the free space memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); // memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); @@ -177,8 +184,9 @@ ABC_PRT( "BCP ", p->timeBcp ); ABC_PRT( "Trace ", p->timeTrace ); ABC_PRT( "TOTAL ", p->timeTotal ); */ - Vec_IntFree( p->vAnties ); - Vec_IntFree( p->vBreaks ); +// Vec_IntFree( p->vAnties ); +// Vec_IntFree( p->vBreaks ); + Vec_VecFree( (Vec_Vec_t *)p->vAntClas ); // ABC_FREE( p->pInters ); ABC_FREE( p->pProofNums ); ABC_FREE( p->pTrail ); @@ -485,9 +493,16 @@ int Intp_ManProofTraceOne( Intp_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF // start the anticedents // pFinal->pAntis = Vec_PtrAlloc( 32 ); // Vec_PtrPush( pFinal->pAntis, pConflict ); - assert( pFinal->Id == Vec_IntSize(p->vBreaks) ); - Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) ); - Vec_IntPush( p->vAnties, pConflict->Id ); + +// assert( pFinal->Id == Vec_IntSize(p->vBreaks) ); +// Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) ); +// Vec_IntPush( p->vAnties, pConflict->Id ); + { + Vec_Int_t * vAnts = Vec_IntAlloc( 16 ); + assert( Vec_PtrSize(p->vAntClas) == pFinal->Id - p->nAntStart ); + Vec_IntPush( vAnts, pConflict->Id ); + Vec_PtrPush( p->vAntClas, vAnts ); + } // if ( p->pCnf->nClausesA ) // Intp_ManAigCopy( p, Intp_ManAigRead(p, pFinal), Intp_ManAigRead(p, pConflict) ); @@ -570,7 +585,8 @@ int Intp_ManProofTraceOne( Intp_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF } // Vec_PtrPush( pFinal->pAntis, pReason ); - Vec_IntPush( p->vAnties, pReason->Id ); +// Vec_IntPush( p->vAnties, pReason->Id ); + Vec_IntPush( (Vec_Int_t *)Vec_PtrEntryLast(p->vAntClas), pReason->Id ); } // unmark all seen variables @@ -668,7 +684,8 @@ int Intp_ManProofRecordOne( Intp_Man_t * p, Sto_Cls_t * pClause ) for ( i = 0; i < (int)pClause->nLits; i++ ) if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] ) { - Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) ); +// Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) ); + Vec_PtrPush( p->vAntClas, Vec_IntAlloc(0) ); return 1; } @@ -705,7 +722,8 @@ int Intp_ManProofRecordOne( Intp_Man_t * p, Sto_Cls_t * pClause ) { // undo to the root level Intp_ManCancelUntil( p, p->nRootSize ); - Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) ); +// Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) ); + Vec_PtrPush( p->vAntClas, Vec_IntAlloc(0) ); return 1; } } @@ -736,7 +754,10 @@ int Intp_ManProofRecordOne( Intp_Man_t * p, Sto_Cls_t * pClause ) pConflict = Intp_ManPropagate( p, p->nRootSize ); if ( pConflict ) { - // construct the proof + // insert place-holders till the empty clause + while ( Vec_PtrSize(p->vAntClas) < p->pCnf->pEmpty->Id - p->nAntStart ) + Vec_PtrPush( p->vAntClas, Vec_IntAlloc(0) ); + // construct the proof for the empty clause Intp_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty ); // if ( p->fVerbose ) // printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); @@ -856,7 +877,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore ) // sat_solver_setnvars( pSat, nSatVars ); Vec_IntForEachEntry( vCore, iClause, i ) { - pClause = Vec_PtrEntry( vClauses, iClause ); + pClause = (Sto_Cls_t *)Vec_PtrEntry( vClauses, iClause ); if ( !sat_solver_addclause( pSat, pClause->pLits, pClause->pLits+pClause->nLits ) ) { printf( "The core verification problem is trivially UNSAT.\n" ); @@ -895,9 +916,11 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore ) SeeAlso [] ***********************************************************************/ -void Intp_ManUnsatCore_rec( Vec_Int_t * vAnties, Vec_Int_t * vBreaks, int iThis, Vec_Int_t * vCore, int nRoots, Vec_Int_t * vVisited ) +void Intp_ManUnsatCore_rec( Vec_Ptr_t * vAntClas, int iThis, Vec_Int_t * vCore, int nRoots, Vec_Int_t * vVisited ) { - int i, iStop, iStart; +// int i, iStop, iStart; + Vec_Int_t * vAnt; + int i, Entry; // skip visited clauses if ( Vec_IntEntry( vVisited, iThis ) ) return; @@ -906,14 +929,17 @@ void Intp_ManUnsatCore_rec( Vec_Int_t * vAnties, Vec_Int_t * vBreaks, int iThis, if ( iThis < nRoots ) { Vec_IntPush( vCore, iThis ); - return; + return; } // iterate through the clauses - iStart = Vec_IntEntry( vBreaks, iThis ); - iStop = Vec_IntEntry( vBreaks, iThis+1 ); - assert( iStop != -1 ); - for ( i = iStart; i < iStop; i++ ) - Intp_ManUnsatCore_rec( vAnties, vBreaks, Vec_IntEntry(vAnties, i), vCore, nRoots, vVisited ); +// iStart = Vec_IntEntry( vBreaks, iThis ); +// iStop = Vec_IntEntry( vBreaks, iThis+1 ); +// assert( iStop != -1 ); +// for ( i = iStart; i < iStop; i++ ) + vAnt = (Vec_Int_t *)Vec_PtrEntry( vAntClas, iThis - nRoots ); + Vec_IntForEachEntry( vAnt, Entry, i ) +// Intp_ManUnsatCore_rec( vAntClas, Vec_IntEntry(vAnties, i), vCore, nRoots, vVisited ); + Intp_ManUnsatCore_rec( vAntClas, Entry, vCore, nRoots, vVisited ); } /**Function************************************************************* @@ -944,7 +970,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose ) p->fVerbose = fVerbose; // adjust the manager - Intp_ManResize( p ); + Intp_ManResize( p ); // construct proof for each clause // start the proof @@ -955,8 +981,11 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose ) } // write the root clauses - Vec_IntClear( p->vAnties ); - Vec_IntFill( p->vBreaks, p->pCnf->nRoots, 0 ); +// Vec_IntClear( p->vAnties ); +// Vec_IntFill( p->vBreaks, p->pCnf->nRoots, 0 ); + Vec_PtrClear( p->vAntClas ); + p->nAntStart = p->pCnf->nRoots; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) Intp_ManProofWriteOne( p, pClause ); @@ -977,8 +1006,10 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose ) } // add the last breaker - assert( p->pCnf->pEmpty->Id == Vec_IntSize(p->vBreaks) - 1 ); - Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) ); +// assert( p->pCnf->pEmpty->Id == Vec_IntSize(p->vBreaks) - 1 ); +// Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) ); + assert( p->pCnf->pEmpty->Id - p->nAntStart == Vec_PtrSize(p->vAntClas) - 1 ); + Vec_PtrPush( p->vAntClas, Vec_IntAlloc(0) ); // stop the proof if ( p->fProofWrite ) @@ -1001,7 +1032,7 @@ p->timeTotal += clock() - clkTotal; // derive the UNSAT core vCore = Vec_IntAlloc( 1000 ); vVisited = Vec_IntStart( p->pCnf->pEmpty->Id+1 ); - Intp_ManUnsatCore_rec( p->vAnties, p->vBreaks, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots, vVisited ); + Intp_ManUnsatCore_rec( p->vAntClas, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots, vVisited ); Vec_IntFree( vVisited ); if ( fVerbose ) printf( "Root clauses = %d. Learned clauses = %d. UNSAT core size = %d.\n", @@ -1015,3 +1046,5 @@ p->timeTotal += clock() - clkTotal; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c index f789f927..30861993 100644 --- a/src/sat/bsat/satMem.c +++ b/src/sat/bsat/satMem.c @@ -21,9 +21,11 @@ #include <string.h> #include <assert.h> -#include "abc_global.h" #include "satMem.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -35,7 +37,7 @@ struct Sat_MmFixed_t_ int nEntriesAlloc; // the total number of entries allocated int nEntriesUsed; // the number of entries in use int nEntriesMax; // the max number of entries in use - char * pEntriesFree; // the linked list of ABC_FREE entries + char * pEntriesFree; // the linked list of free entries // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -52,8 +54,8 @@ struct Sat_MmFlex_t_ { // information about individual entries int nEntriesUsed; // the number of entries allocated - char * pCurrent; // the current pointer to ABC_FREE memory - char * pEnd; // the first entry outside the ABC_FREE memory + char * pCurrent; // the current pointer to free memory + char * pEnd; // the first entry outside the free memory // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -167,7 +169,7 @@ char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p ) char * pTemp; int i; - // check if there are still ABC_FREE entries + // check if there are still free entries if ( p->nEntriesUsed == p->nEntriesAlloc ) { // need to allocate more entries assert( p->pEntriesFree == NULL ); @@ -196,7 +198,7 @@ char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p ) p->nEntriesUsed++; if ( p->nEntriesMax < p->nEntriesUsed ) p->nEntriesMax = p->nEntriesUsed; - // return the first entry in the ABC_FREE entry list + // return the first entry in the free entry list pTemp = p->pEntriesFree; p->pEntriesFree = *((char **)pTemp); return pTemp; @@ -217,7 +219,7 @@ void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry ) { // decrement the counter of used entries p->nEntriesUsed--; - // add the entry to the linked list of ABC_FREE entries + // add the entry to the linked list of free entries *((char **)pEntry) = p->pEntriesFree; p->pEntriesFree = pEntry; } @@ -251,7 +253,7 @@ void Sat_MmFixedRestart( Sat_MmFixed_t * p ) } // set the last link *((char **)pTemp) = NULL; - // set the ABC_FREE entry list + // set the free entry list p->pEntriesFree = p->pChunks[0]; // set the correct statistics p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; @@ -353,7 +355,7 @@ void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose ) char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes ) { char * pTemp; - // check if there are still ABC_FREE entries + // check if there are still free entries if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd ) { // need to allocate more entries if ( p->nChunks == p->nChunksAlloc ) @@ -548,3 +550,5 @@ int Sat_MmStepReadMemUsage( Sat_MmStep_t * p ) nMemTotal += p->pMems[i]->nMemoryAlloc; return nMemTotal; } +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satMem.h b/src/sat/bsat/satMem.h index b6d93807..13afa9b9 100644 --- a/src/sat/bsat/satMem.h +++ b/src/sat/bsat/satMem.h @@ -23,6 +23,10 @@ /// INCLUDES /// //////////////////////////////////////////////////////////////////////// +#include "abc_global.h" + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// @@ -66,6 +70,10 @@ extern char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes ); extern void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes ); extern int Sat_MmStepReadMemUsage( Sat_MmStep_t * p ); + + +ABC_NAMESPACE_HEADER_END + #endif //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index df04cd1f..10dea1e3 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2,7 +2,7 @@ MiniSat -- Copyright (c) 2005, Niklas Sorensson http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ -Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is @@ -25,7 +25,21 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <math.h> #include "satSolver.h" - +#include "satStore.h" + +ABC_NAMESPACE_IMPL_START +/* +extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); +extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); +extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); +extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); +extern void * Sto_ManAlloc(); +extern void Sto_ManDumpClauses( void * p, char * pFileName ); +extern void Sto_ManFree( void * p ); +extern int Sto_ManChangeLastClause( void * p ); +extern void Sto_ManMarkRoots( void * p ); +extern void Sto_ManMarkClausesA( void * p ); +*/ //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT //================================================================================================= @@ -91,7 +105,7 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[ // Encode literals in clause pointers: static inline clause* clause_from_lit (lit l) { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); } -static inline bool clause_is_lit (clause* c) { return ((ABC_PTRUINT_T)c & 1); } +static inline int clause_is_lit (clause* c) { return ((ABC_PTRUINT_T)c & 1); } static inline lit clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1); } //================================================================================================= @@ -386,6 +400,7 @@ void sat_solver_setnvars(sat_solver* s,int n) s->levels = ABC_REALLOC(int, s->levels, s->cap); s->tags = ABC_REALLOC(lbool, s->tags, s->cap); s->trail = ABC_REALLOC(lit, s->trail, s->cap); + s->polarity = ABC_REALLOC(char, s->polarity, s->cap); } for (var = s->size; var < n; var++){ @@ -398,6 +413,7 @@ void sat_solver_setnvars(sat_solver* s,int n) s->reasons [var] = (clause*)0; s->levels [var] = 0; s->tags [var] = l_Undef; + s->polarity [var] = 0; /* does not hold because variables enqueued at top level will not be reinserted in the heap assert(veci_size(&s->order) == var); @@ -410,7 +426,7 @@ void sat_solver_setnvars(sat_solver* s,int n) } -static inline bool enqueue(sat_solver* s, lit l, clause* from) +static inline int enqueue(sat_solver* s, lit l, clause* from) { lbool* values = s->assigns; int v = lit_var(l); @@ -457,6 +473,7 @@ static void sat_solver_canceluntil(sat_solver* s, int level) { lbool* values; clause** reasons; int bound; + int lastLev; int c; if (sat_solver_dlevel(s) <= level) @@ -466,6 +483,7 @@ static void sat_solver_canceluntil(sat_solver* s, int level) { values = s->assigns; reasons = s->reasons; bound = (veci_begin(&s->trail_lim))[level]; + lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1]; //////////////////////////////////////// // added to cancel all assignments @@ -477,6 +495,8 @@ static void sat_solver_canceluntil(sat_solver* s, int level) { int x = lit_var(trail[c]); values [x] = l_Undef; reasons[x] = (clause*)0; + if ( c < lastLev ) + s->polarity[x] = !lit_sign(trail[c]); } for (c = s->qhead-1; c >= bound; c--) @@ -497,8 +517,7 @@ static void sat_solver_record(sat_solver* s, veci* cls) // add clause to internal storage if ( s->pStore ) { - extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); - int RetValue = Sto_ManAddClause( s->pStore, begin, end ); + int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end ); assert( RetValue ); } /////////////////////////////////// @@ -531,7 +550,7 @@ static double sat_solver_progress(sat_solver* s) //================================================================================================= // Major methods: -static bool sat_solver_lit_removable(sat_solver* s, lit l, int minl) +static int sat_solver_lit_removable(sat_solver* s, lit l, int minl) { lbool* tags = s->tags; clause** reasons = s->reasons; @@ -594,6 +613,92 @@ static bool sat_solver_lit_removable(sat_solver* s, lit l, int minl) return true; } + +/*_________________________________________________________________________________________________ +| +| analyzeFinal : (p : Lit) -> [void] +| +| Description: +| Specialized analysis procedure to express the final conflict in terms of assumptions. +| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and +| stores the result in 'out_conflict'. +|________________________________________________________________________________________________@*/ +/* +void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) +{ + out_conflict.clear(); + out_conflict.push(p); + + if (decisionLevel() == 0) + return; + + seen[var(p)] = 1; + + for (int i = trail.size()-1; i >= trail_lim[0]; i--){ + Var x = var(trail[i]); + if (seen[x]){ + if (reason(x) == GClause_NULL){ + assert(level(x) > 0); + out_conflict.push(~trail[i]); + }else{ + Clause& c = ca.deref(smartReason(x)); + for (int j = 1; j < c.size(); j++) + if (level(var(c[j])) > 0) + seen[var(c[j])] = 1; + } + seen[x] = 0; + } + } + + seen[var(p)] = 0; +} +*/ + +static void sat_solver_analyze_final(sat_solver* s, lit p, veci* out_conflict) +{ + int i, j; + veci_resize(out_conflict,0); +// veci_push(out_conflict,p); // do not write conflict literal + if ( sat_solver_dlevel(s) == 0 ) + return; + assert( veci_size(&s->tagged) == 0 ); + assert( s->tags[lit_var(p)] == l_Undef ); + s->tags[lit_var(p)] = l_True; + for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){ + int x = lit_var(s->trail[i]); + if (s->tags[x] == l_True){ + if (s->reasons[x] == NULL){ + assert(s->levels[x] > 0); + veci_push(out_conflict,lit_neg(s->trail[i])); + }else{ + clause* c = s->reasons[x]; + if (clause_is_lit(c)){ + lit q = clause_read_lit(c); + assert(lit_var(q) >= 0 && lit_var(q) < s->size); + if (s->levels[lit_var(q)] > 0) + { + s->tags[lit_var(q)] = l_True; + veci_push(&s->tagged,lit_var(q)); + } + } + else{ + int* lits = clause_begin(c); + for (j = 1; j < clause_size(c); j++) + if (s->levels[lit_var(lits[j])] > 0) + { + s->tags[lit_var(lits[j])] = l_True; + veci_push(&s->tagged,lit_var(lits[j])); + } + } + } + } + } + for (i = 0; i < veci_size(&s->tagged); i++) + s->tags[veci_begin(&s->tagged)[i]] = l_Undef; + veci_resize(&s->tagged,0); +} + + static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) { lit* trail = s->trail; @@ -871,6 +976,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT #endif s->stats.conflicts++; conflictC++; if (sat_solver_dlevel(s) == s->root_level){ +// lit p = clause_is_lit(confl)? clause_read_lit(confl) : clause_begin(confl)[0]; +// sat_solver_analyze_final(s, lit_neg(p), &s->conf_final); veci_delete(&learnt_clause); return l_False; } @@ -896,7 +1003,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT return l_Undef; } if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) || - (s->nInsLimit && s->stats.inspects > s->nInsLimit) ) +// (s->nInsLimit && s->stats.inspects > s->nInsLimit) ) + (s->nInsLimit && s->stats.propagations > s->nInsLimit) ) { // Reached bound on number of conflicts: s->progress_estimate = sat_solver_progress(s); @@ -938,7 +1046,10 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT return l_True; } - assume(s,lit_neg(toLit(next))); + if ( s->polarity[next] ) // positive polarity + assume(s,toLit(next)); + else + assume(s,lit_neg(toLit(next))); } } @@ -963,6 +1074,7 @@ sat_solver* sat_solver_new(void) veci_new(&s->model); veci_new(&s->act_vars); veci_new(&s->temp_clause); + veci_new(&s->conf_final); // initialize arrays s->wlists = 0; @@ -1038,6 +1150,7 @@ void sat_solver_delete(sat_solver* s) veci_delete(&s->model); veci_delete(&s->act_vars); veci_delete(&s->temp_clause); + veci_delete(&s->conf_final); ABC_FREE(s->binary); // delete arrays @@ -1056,6 +1169,7 @@ void sat_solver_delete(sat_solver* s) ABC_FREE(s->levels ); ABC_FREE(s->trail ); ABC_FREE(s->tags ); + ABC_FREE(s->polarity ); } sat_solver_store_free(s); @@ -1063,7 +1177,7 @@ void sat_solver_delete(sat_solver* s) } -bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) +int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) { lit *i,*j; int maxvar; @@ -1096,8 +1210,7 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) // add clause to internal storage if ( s->pStore ) { - extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); - int RetValue = Sto_ManAddClause( s->pStore, begin, end ); + int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end ); assert( RetValue ); } /////////////////////////////////// @@ -1135,7 +1248,7 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) } -bool sat_solver_simplify(sat_solver* s) +int sat_solver_simplify(sat_solver* s) { clause** reasons; int type; @@ -1171,10 +1284,30 @@ bool sat_solver_simplify(sat_solver* s) return true; } +double luby(double y, int x) +{ + int size, seq; + for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1); + while (size-1 != x){ + size = (size-1) >> 1; + seq--; + x = x % size; + } + return pow(y, (double)seq); +} + +void luby_test() +{ + int i; + for ( i = 0; i < 20; i++ ) + printf( "%d ", (int)luby(2,i) ); + printf( "\n" ); +} int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal) { - ABC_INT64_T nof_conflicts = 100; + int restart_iter = 0; + ABC_INT64_T nof_conflicts; ABC_INT64_T nof_learnts = sat_solver_nclauses(s) / 3; lbool status = l_Undef; lbool* values = s->assigns; @@ -1185,8 +1318,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit { if ( s->pStore ) { - extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); - int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL ); + int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL ); assert( RetValue ); } return l_False; @@ -1201,7 +1333,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit; if ( nInsLimit ) - s->nInsLimit = s->stats.inspects + nInsLimit; +// s->nInsLimit = s->stats.inspects + nInsLimit; + s->nInsLimit = s->stats.propagations + nInsLimit; if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) ) s->nConfLimit = nConfLimitGlobal; if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) ) @@ -1250,9 +1383,11 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit s->progress_estimate*100); fflush(stdout); } + nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) ); +//printf( "%d ", (int)nof_conflicts ); status = sat_solver_search(s, nof_conflicts, nof_learnts); - nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5; - nof_learnts = nof_learnts * 11 / 10; //*= 1.1; +// nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5; + nof_learnts = nof_learnts * 11 / 10; //*= 1.1; // quit the loop if reached an external limit if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ) @@ -1260,7 +1395,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit // printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit ); break; } - if ( s->nInsLimit && s->stats.inspects > s->nInsLimit ) +// if ( s->nInsLimit && s->stats.inspects > s->nInsLimit ) + if ( s->nInsLimit && s->stats.propagations > s->nInsLimit ) { // printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit ); break; @@ -1274,8 +1410,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit //////////////////////////////////////////////// if ( status == l_False && s->pStore ) { - extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); - int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL ); + int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL ); assert( RetValue ); } //////////////////////////////////////////////// @@ -1305,41 +1440,35 @@ int sat_solver_nconflicts(sat_solver* s) void sat_solver_store_alloc( sat_solver * s ) { - extern void * Sto_ManAlloc(); assert( s->pStore == NULL ); s->pStore = Sto_ManAlloc(); } void sat_solver_store_write( sat_solver * s, char * pFileName ) { - extern void Sto_ManDumpClauses( void * p, char * pFileName ); - if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName ); + if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName ); } void sat_solver_store_free( sat_solver * s ) { - extern void Sto_ManFree( void * p ); - if ( s->pStore ) Sto_ManFree( s->pStore ); + if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore ); s->pStore = NULL; } int sat_solver_store_change_last( sat_solver * s ) { - extern int Sto_ManChangeLastClause( void * p ); - if ( s->pStore ) return Sto_ManChangeLastClause( s->pStore ); + if ( s->pStore ) return Sto_ManChangeLastClause( (Sto_Man_t *)s->pStore ); return -1; } void sat_solver_store_mark_roots( sat_solver * s ) { - extern void Sto_ManMarkRoots( void * p ); - if ( s->pStore ) Sto_ManMarkRoots( s->pStore ); + if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore ); } void sat_solver_store_mark_clauses_a( sat_solver * s ) { - extern void Sto_ManMarkClausesA( void * p ); - if ( s->pStore ) Sto_ManMarkClausesA( s->pStore ); + if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore ); } void * sat_solver_store_release( sat_solver * s ) @@ -1404,3 +1533,5 @@ void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void // for ( i = 1; i < size; i++ ) // assert(comp(array[i-1], array[i])<0); } +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index f37c1738..2e435c59 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -2,7 +2,7 @@ MiniSat -- Copyright (c) 2005, Niklas Sorensson http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ -Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is @@ -22,28 +22,29 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef satSolver_h #define satSolver_h + #include <stdio.h> #include <stdlib.h> #include <string.h> #include <assert.h> -#include "abc_global.h" #include "satVec.h" #include "satMem.h" +ABC_NAMESPACE_HEADER_START + + //================================================================================================= // Simple types: -// does not work for c++ -//typedef int bool; #ifndef __cplusplus -#ifndef bool -#define bool int +#ifndef false +# define false 0 +#endif +#ifndef true +# define true 1 #endif #endif - -static const bool true = 1; -static const bool false = 0; typedef int lit; typedef char lbool; @@ -74,8 +75,8 @@ typedef struct sat_solver_t sat_solver; extern sat_solver* sat_solver_new(void); extern void sat_solver_delete(sat_solver* s); -extern bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end); -extern bool sat_solver_simplify(sat_solver* s); +extern int sat_solver_addclause(sat_solver* s, lit* begin, lit* end); +extern int sat_solver_simplify(sat_solver* s); extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern int sat_solver_nvars(sat_solver* s); @@ -89,7 +90,7 @@ struct stats_t ABC_INT64_T starts, decisions, propagations, inspects, conflicts; ABC_INT64_T clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; }; -typedef struct stats_t stats; +typedef struct stats_t stats_t; extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ); @@ -139,6 +140,7 @@ struct sat_solver_t clause** reasons; // int* levels; // lit* trail; + char* polarity; clause* binary; // A temporary binary clause lbool* tags; // @@ -148,6 +150,8 @@ struct sat_solver_t veci order; // Variable order. (heap) (contains: var) veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) veci model; // If problem is solved, this vector contains the model (contains: lbool). + veci conf_final; // If problem is unsatisfiable (possibly under assumptions), + // this vector represent the final conflict clause expressed in the assumptions. int root_level; // Level of first proper decision. int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. @@ -156,7 +160,7 @@ struct sat_solver_t double progress_estimate; int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - stats stats; + stats_t stats; ABC_INT64_T nConfLimit; // external limit on the number of conflicts ABC_INT64_T nInsLimit; // external limit on the number of implications @@ -210,4 +214,8 @@ static void sat_solver_compress(sat_solver* s) } } + + +ABC_NAMESPACE_HEADER_END + #endif diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c index fff8a836..ac74c4a6 100644 --- a/src/sat/bsat/satStore.c +++ b/src/sat/bsat/satStore.c @@ -26,6 +26,9 @@ #include "satStore.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -185,6 +188,7 @@ int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd ) // get memory for the clause nSize = sizeof(Sto_Cls_t) + sizeof(lit) * (pEnd - pBeg); + nSize = (nSize / sizeof(char*) + ((nSize % sizeof(char*)) > 0)) * sizeof(char*); // added by Saurabh on Sep 3, 2009 pClause = (Sto_Cls_t *)Sto_ManMemoryFetch( p, nSize ); memset( pClause, 0, sizeof(Sto_Cls_t) ); @@ -192,6 +196,7 @@ int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd ) pClause->Id = p->nClauses++; pClause->nLits = pEnd - pBeg; memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) ); +// assert( pClause->pLits[0] >= 0 ); // add the clause to the list if ( p->pHead == NULL ) @@ -461,3 +466,5 @@ Sto_Man_t * Sto_ManLoadClauses( char * pFileName ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h index ea11f46a..0293aea7 100644 --- a/src/sat/bsat/satStore.h +++ b/src/sat/bsat/satStore.h @@ -21,6 +21,7 @@ #ifndef __SAT_STORE_H__ #define __SAT_STORE_H__ + /* The trace of SAT solving contains the original clauses of the problem along with the learned clauses derived during SAT solving. @@ -38,9 +39,7 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif +ABC_NAMESPACE_HEADER_START #ifdef _WIN32 #define inline __inline // compatible with MS VS 6.0 @@ -116,8 +115,10 @@ extern int Sto_ManMemoryReport( Sto_Man_t * p ); extern void Sto_ManMarkRoots( Sto_Man_t * p ); extern void Sto_ManMarkClausesA( Sto_Man_t * p ); extern void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName ); +extern int Sto_ManChangeLastClause( Sto_Man_t * p ); extern Sto_Man_t * Sto_ManLoadClauses( char * pFileName ); + /*=== satInter.c ==========================================================*/ typedef struct Int_Man_t_ Int_Man_t; extern Int_Man_t * Int_ManAlloc(); @@ -143,9 +144,11 @@ extern Intp_Man_t * Intp_ManAlloc(); extern void Intp_ManFree( Intp_Man_t * p ); extern void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose ); -#ifdef __cplusplus -} -#endif + + +ABC_NAMESPACE_HEADER_END + + #endif diff --git a/src/sat/bsat/satTrace.c b/src/sat/bsat/satTrace.c index 08cfadf6..ae701ce9 100644 --- a/src/sat/bsat/satTrace.c +++ b/src/sat/bsat/satTrace.c @@ -20,6 +20,9 @@ #include "satSolver.h" +ABC_NAMESPACE_IMPL_START + + /* The trace of SAT solving contains the original clause of the problem along with the learned clauses derived during SAT solving. @@ -105,3 +108,5 @@ void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 5f8008bb..0ce40acd 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -22,6 +22,9 @@ #include <assert.h> #include "satSolver.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -35,7 +38,7 @@ struct clause_t static inline int clause_size( clause* c ) { return c->size_learnt >> 1; } static inline lit* clause_begin( clause* c ) { return c->lits; } -static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ); +static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -78,13 +81,13 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe nClauses = p->clauses.size; pClauses = p->clauses.ptr; for ( i = 0; i < nClauses; i++ ) - Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars ); + Sat_SolverClauseWriteDimacs( pFile, (clause *)pClauses[i], incrementVars ); // write the learned clauses nClauses = p->learnts.size; pClauses = p->learnts.ptr; for ( i = 0; i < nClauses; i++ ) - Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars ); + Sat_SolverClauseWriteDimacs( pFile, (clause *)pClauses[i], incrementVars ); // write zero-level assertions for ( i = 0; i < p->size; i++ ) @@ -119,14 +122,14 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe SeeAlso [] ***********************************************************************/ -void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ) +void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement ) { lit * pLits = clause_begin(pC); int nLits = clause_size(pC); int i; for ( i = 0; i < nLits; i++ ) - fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""), lit_var(pLits[i]) + (int)(fIncrement>0) ); + fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""), lit_var(pLits[i]) + (fIncrement>0) ); if ( fIncrement ) fprintf( pFile, "0" ); fprintf( pFile, "\n" ); @@ -169,7 +172,7 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ) { int * pModel; int i; - pModel = ABC_ALLOC( int, nVars+1 ); + pModel = ABC_CALLOC( int, nVars+1 ); for ( i = 0; i < nVars; i++ ) { assert( pVars[i] >= 0 && pVars[i] < p->size ); @@ -213,7 +216,7 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar ) nClauses = vecp_size(&p->clauses); for ( c = 0; c < nClauses; c++ ) { - pClause = p->clauses.ptr[c]; + pClause = (clause *)p->clauses.ptr[c]; nLits = clause_size(pClause); pLits = clause_begin(pClause); for ( v = 0; v < nLits; v++ ) @@ -231,3 +234,5 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h index f017c90b..4c3763e3 100644 --- a/src/sat/bsat/satVec.h +++ b/src/sat/bsat/satVec.h @@ -2,7 +2,7 @@ MiniSat -- Copyright (c) 2005, Niklas Sorensson http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ -Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is @@ -22,6 +22,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef satVec_h #define satVec_h +#include "abc_global.h" + +ABC_NAMESPACE_HEADER_START + + // vector of 32-bit intergers (added for 64-bit portability) struct veci_t { int size; @@ -78,4 +83,8 @@ static inline void vecp_push (vecp* v, void* e) } + + +ABC_NAMESPACE_HEADER_END + #endif diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index ecad9d37..d49f75c0 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -19,6 +19,11 @@ #include "abc.h" #include "fraig.h" #include "csat_apis.h" +#include "stmm.h" +#include "main.h" + +ABC_NAMESPACE_IMPL_START + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -56,7 +61,7 @@ extern void Abc_Start(); extern void Abc_Stop(); // some external procedures -extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); +extern int Io_WriteBench( Abc_Ntk_t * pNtk, const char * FileName ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -215,51 +220,51 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha case CSAT_CONST: if ( nofi != 0 ) { printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; } - pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc ); + pSop = Abc_SopCreateConst1( (Extra_MmFlex_t *)mng->pNtk->pManFunc ); break; case CSAT_BAND: if ( nofi < 1 ) { printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; } - pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL ); + pSop = Abc_SopCreateAnd( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi, NULL ); break; case CSAT_BNAND: if ( nofi < 1 ) { printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; } - pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi ); + pSop = Abc_SopCreateNand( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi ); break; case CSAT_BOR: if ( nofi < 1 ) { printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; } - pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL ); + pSop = Abc_SopCreateOr( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi, NULL ); break; case CSAT_BNOR: if ( nofi < 1 ) { printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; } - pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi ); + pSop = Abc_SopCreateNor( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi ); break; case CSAT_BXOR: if ( nofi < 1 ) { printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; } if ( nofi > 2 ) { printf( "ABC_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; } - pSop = Abc_SopCreateXor( mng->pNtk->pManFunc, nofi ); + pSop = Abc_SopCreateXor( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi ); break; case CSAT_BXNOR: if ( nofi < 1 ) { printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; } if ( nofi > 2 ) { printf( "ABC_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; } - pSop = Abc_SopCreateNxor( mng->pNtk->pManFunc, nofi ); + pSop = Abc_SopCreateNxor( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi ); break; case CSAT_BINV: if ( nofi != 1 ) { printf( "ABC_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } - pSop = Abc_SopCreateInv( mng->pNtk->pManFunc ); + pSop = Abc_SopCreateInv( (Extra_MmFlex_t *)mng->pNtk->pManFunc ); break; case CSAT_BBUF: if ( nofi != 1 ) { printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } - pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc ); + pSop = Abc_SopCreateBuf( (Extra_MmFlex_t *)mng->pNtk->pManFunc ); break; default : break; @@ -675,7 +680,7 @@ CSAT_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID ) void ABC_Dump_Bench_File( ABC_Manager mng ) { Abc_Ntk_t * pNtkTemp, * pNtkAig; - char * pFileName; + const char * pFileName; // derive the netlist pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0, 0 ); @@ -769,3 +774,5 @@ char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index 337056a3..a6c1b18a 100644 --- a/src/sat/csat/csat_apis.h +++ b/src/sat/csat/csat_apis.h @@ -19,6 +19,7 @@ #ifndef __ABC_APIS_H__ #define __ABC_APIS_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -27,9 +28,10 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif + + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// @@ -211,9 +213,11 @@ extern void ABC_TargetResFree( CSAT_Target_ResultT * p ); extern void CSAT_SetCaller(ABC_Manager mng, enum CSAT_CallerT caller); -#ifdef __cplusplus -} -#endif + + +ABC_NAMESPACE_HEADER_END + + #endif diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index ce686cef..2b499967 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -19,6 +19,7 @@ #ifndef __FRAIG_H__ #define __FRAIG_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -27,9 +28,10 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif + + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// @@ -249,8 +251,10 @@ extern Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fSt /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -} -#endif + + +ABC_NAMESPACE_HEADER_END + + #endif diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c index 79a7c224..6e0ab959 100644 --- a/src/sat/fraig/fraigApi.c +++ b/src/sat/fraig/fraigApi.c @@ -18,6 +18,9 @@ #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -295,3 +298,5 @@ void Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t * pNodeOld, Fraig_Nod //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c index 89bc924f..47539db2 100644 --- a/src/sat/fraig/fraigCanon.c +++ b/src/sat/fraig/fraigCanon.c @@ -19,6 +19,9 @@ #include <limits.h> #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -216,3 +219,5 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_ //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigChoice.c b/src/sat/fraig/fraigChoice.c index 896e5d2d..21d4fe10 100644 --- a/src/sat/fraig/fraigChoice.c +++ b/src/sat/fraig/fraigChoice.c @@ -18,6 +18,9 @@ #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -239,3 +242,5 @@ Fraig_ManCheckConsistency( pMan ); //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigFanout.c b/src/sat/fraig/fraigFanout.c index 789bffca..0e6c86f8 100644 --- a/src/sat/fraig/fraigFanout.c +++ b/src/sat/fraig/fraigFanout.c @@ -18,6 +18,9 @@ #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + #ifdef FRAIG_ENABLE_FANOUTS //////////////////////////////////////////////////////////////////////// @@ -173,3 +176,5 @@ int Fraig_NodeGetFanoutNum( Fraig_Node_t * pNode ) #endif +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c index 7977824d..47f946e1 100644 --- a/src/sat/fraig/fraigFeed.c +++ b/src/sat/fraig/fraigFeed.c @@ -18,6 +18,9 @@ #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -736,7 +739,7 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p ) // signatures remain without changes } - // replace the manager to ABC_FREE up some memory + // replace the manager to free up some memory Fraig_MemFixedStop( p->mmSims, 0 ); p->mmSims = mmSimsNew; @@ -906,3 +909,5 @@ printf( "\n" ); //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index ac6ea873..7cc2194a 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -19,6 +19,7 @@ #ifndef __FRAIG_INT_H__ #define __FRAIG_INT_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -33,6 +34,9 @@ #include "fraig.h" #include "msat.h" +ABC_NAMESPACE_HEADER_START + + //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// @@ -57,9 +61,9 @@ #define FRAIG_MAX_PRIMES 1024 // the maximum number of primes used for hashing // this parameter determines when simulation info is extended -// it will be extended when the ABC_FREE storage in the dynamic simulation +// it will be extended when the free storage in the dynamic simulation // info is less or equal to this number of words (FRAIG_WORDS_STORE) -// this is done because if the ABC_FREE storage for dynamic simulation info +// this is done because if the free storage for dynamic simulation info // is not sufficient, computation becomes inefficient #define FRAIG_WORDS_STORE 5 @@ -419,6 +423,10 @@ extern int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig /*=== fraigVec.c ===============================================================*/ extern void Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p ); + + +ABC_NAMESPACE_HEADER_END + #endif //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index b71262d8..ba08d793 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -18,6 +18,9 @@ #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -42,7 +45,7 @@ int timeAssign; ***********************************************************************/ void Prove_ParamsSetDefault( Prove_Params_t * pParams ) { - // clean the parameter structure + // clean the parameter structure memset( pParams, 0, sizeof(Prove_Params_t) ); // general parameters pParams->fUseFraiging = 1; // enables fraiging @@ -52,7 +55,7 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams ) // iterations pParams->nItersMax = 6; // the number of iterations // mitering - pParams->nMiteringLimitStart = 300; // starting mitering limit + pParams->nMiteringLimitStart = 5000; // starting mitering limit pParams->nMiteringLimitMulti = 2.0; // multiplicative coefficient to increase the limit in each iteration // rewriting (currently not used) pParams->nRewritingLimitStart = 3; // the number of rewriting iterations @@ -382,7 +385,7 @@ void Fraig_ManPrintStats( Fraig_Man_t * p ) SeeAlso [] ***********************************************************************/ -Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean ) +Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, int fClean ) { Fraig_NodeVec_t * vInfo; unsigned * pUnsigned; @@ -538,3 +541,5 @@ void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes ) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigMem.c b/src/sat/fraig/fraigMem.c index 1cc99790..ef52765e 100644 --- a/src/sat/fraig/fraigMem.c +++ b/src/sat/fraig/fraigMem.c @@ -18,6 +18,9 @@ #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -29,7 +32,7 @@ struct Fraig_MemFixed_t_ int nEntriesAlloc; // the total number of entries allocated int nEntriesUsed; // the number of entries in use int nEntriesMax; // the max number of entries in use - char * pEntriesFree; // the linked list of ABC_FREE entries + char * pEntriesFree; // the linked list of free entries // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -130,7 +133,7 @@ char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_t * p ) char * pTemp; int i; - // check if there are still ABC_FREE entries + // check if there are still free entries if ( p->nEntriesUsed == p->nEntriesAlloc ) { // need to allocate more entries assert( p->pEntriesFree == NULL ); @@ -159,7 +162,7 @@ char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_t * p ) p->nEntriesUsed++; if ( p->nEntriesMax < p->nEntriesUsed ) p->nEntriesMax = p->nEntriesUsed; - // return the first entry in the ABC_FREE entry list + // return the first entry in the free entry list pTemp = p->pEntriesFree; p->pEntriesFree = *((char **)pTemp); return pTemp; @@ -180,7 +183,7 @@ void Fraig_MemFixedEntryRecycle( Fraig_MemFixed_t * p, char * pEntry ) { // decrement the counter of used entries p->nEntriesUsed--; - // add the entry to the linked list of ABC_FREE entries + // add the entry to the linked list of free entries *((char **)pEntry) = p->pEntriesFree; p->pEntriesFree = pEntry; } @@ -214,7 +217,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p ) } // set the last link *((char **)pTemp) = NULL; - // set the ABC_FREE entry list + // set the free entry list p->pEntriesFree = p->pChunks[0]; // set the correct statistics p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; @@ -244,3 +247,5 @@ int Fraig_MemFixedReadMemUsage( Fraig_MemFixed_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c index 4cfe035d..9f95cd46 100644 --- a/src/sat/fraig/fraigNode.c +++ b/src/sat/fraig/fraigNode.c @@ -18,6 +18,9 @@ #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -311,3 +314,5 @@ void Fraig_NodeSimulate( Fraig_Node_t * pNode, int iWordStart, int iWordStop, in /// END OF FILE /// //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigPrime.c b/src/sat/fraig/fraigPrime.c index 127ad478..42a079fd 100644 --- a/src/sat/fraig/fraigPrime.c +++ b/src/sat/fraig/fraigPrime.c @@ -18,6 +18,9 @@ #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -142,3 +145,5 @@ unsigned int Cudd_PrimeFraig( unsigned int p) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index 084d1538..b96bc5a1 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -16,8 +16,12 @@ ***********************************************************************/ +#include <math.h> #include "fraigInt.h" -#include "math.h" +#include "msatInt.h" + +ABC_NAMESPACE_IMPL_START + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -36,8 +40,6 @@ static void Fraig_SupergateAddClausesMux( Fraig_Man_t * pMan, Fraig_Node_t * pNo static void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); static void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); -extern void * Msat_ClauseVecReadEntry( void * p, int i ); - // The lesson learned seems to be that variable should be in reverse topological order // from the output of the miter. The ordering of adjacency lists is very important. // The best way seems to be fanins followed by fanouts. Slight changes to this order @@ -318,7 +320,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * // nBTLimit /= 10; if ( nBTLimit <= 10 ) return 0; - nBTLimit = (int)sqrt(nBTLimit); + nBTLimit = (int)sqrt((double)nBTLimit); // fSwitch = 1; } @@ -907,7 +909,7 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t { // create the fanins of the supergate assert( pNode->fClauses == 0 ); - // detecting a fanout-ABC_FREE cone (experiment only) + // detecting a fanout-free cone (experiment only) // Fraig_DetectFanoutFreeCone( pMan, pNode ); if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) ) @@ -1453,3 +1455,5 @@ void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c index 55d92b4a..79ab7ffc 100644 --- a/src/sat/fraig/fraigTable.c +++ b/src/sat/fraig/fraigTable.c @@ -18,6 +18,9 @@ #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -655,3 +658,5 @@ int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEquiv ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c index 0930edbd..0d4cdfaf 100644 --- a/src/sat/fraig/fraigUtil.c +++ b/src/sat/fraig/fraigUtil.c @@ -19,6 +19,9 @@ #include "fraigInt.h" #include <limits.h> +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -237,7 +240,7 @@ int Fraig_CheckTfi2( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNe Description [This procedure collects the nodes reachable from the POs of the AIG and sets the type of fanout counter (none, one, or many) for each node. This procedure is useful to determine - fanout-ABC_FREE cones of AND-nodes, which is helpful for rebalancing + fanout-free cones of AND-nodes, which is helpful for rebalancing the AIG (see procedure Fraig_ManRebalance, or something like that).] SideEffects [] @@ -1032,3 +1035,5 @@ int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/fraig/fraigVec.c b/src/sat/fraig/fraigVec.c index b47c6a2f..25d50bf3 100644 --- a/src/sat/fraig/fraigVec.c +++ b/src/sat/fraig/fraigVec.c @@ -18,6 +18,9 @@ #include "fraigInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -543,3 +546,5 @@ void Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p ) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/lsat/solver.h b/src/sat/lsat/solver.h index 8d198cb2..a50c4abe 100644 --- a/src/sat/lsat/solver.h +++ b/src/sat/lsat/solver.h @@ -2,7 +2,7 @@ Copyright (c) 2008, Niklas Sorensson 2008, Koen Claessen -Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is @@ -21,6 +21,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_solver_h #define Minisat_solver_h + +ABC_NAMESPACE_HEADER_START + + // SolverTypes: // typedef struct solver_t solver; @@ -104,8 +108,8 @@ int solver_num_conflicts (solver *s); double random_seed; double restart_luby_start; // The factor with which the values of the luby sequence is multiplied to get the restart (default 100) double restart_luby_inc; // The constant that the luby sequence uses powers of (default 2) - bool expensive_ccmin; // FIXME: describe. - bool rnd_pol; // FIXME: describe. + int expensive_ccmin; // FIXME: describe. + int rnd_pol; // FIXME: describe. int restart_first; // The initial restart limit. (default 100) double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5) @@ -121,4 +125,8 @@ int solver_num_conflicts (solver *s); uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; */ + + +ABC_NAMESPACE_HEADER_END + #endif diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 2b28700c..6dc68cf8 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -21,6 +21,7 @@ #ifndef __MSAT_H__ #define __MSAT_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -29,22 +30,15 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif + + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#ifdef bool -#undef bool -#endif - -#ifndef __MVTYPES_H__ -typedef int bool; -#endif - typedef struct Msat_Solver_t_ Msat_Solver_t; // the vector of intergers and of clauses @@ -77,13 +71,13 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t; //////////////////////////////////////////////////////////////////////// /*=== satRead.c ============================================================*/ -extern bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ); +extern int Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ); /*=== satSolver.c ===========================================================*/ // adding vars, clauses, simplifying the database, and solving -extern bool Msat_SolverAddVar( Msat_Solver_t * p, int Level ); -extern bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits ); -extern bool Msat_SolverSimplifyDB( Msat_Solver_t * p ); -extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit ); +extern int Msat_SolverAddVar( Msat_Solver_t * p, int Level ); +extern int Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits ); +extern int Msat_SolverSimplifyDB( Msat_Solver_t * p ); +extern int Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit ); // printing stats, assignments, and clauses extern void Msat_SolverPrintStats( Msat_Solver_t * p ); extern void Msat_SolverPrintAssignment( Msat_Solver_t * p ); @@ -116,7 +110,7 @@ extern void Msat_SolverRemoveLearned( Msat_Solver_t * p ); extern void Msat_SolverRemoveMarked( Msat_Solver_t * p ); /*=== satSolverApi.c ===========================================================*/ // allocation, cleaning, and freeing the solver -extern Msat_Solver_t * Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, bool fVerbose ); +extern Msat_Solver_t * Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, int fVerbose ); extern void Msat_SolverResize( Msat_Solver_t * pMan, int nVarsAlloc ); extern void Msat_SolverClean( Msat_Solver_t * p, int nVars ); extern void Msat_SolverPrepare( Msat_Solver_t * pSat, Msat_IntVec_t * vVars ); @@ -161,9 +155,11 @@ extern int Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double Weigh extern int Msat_VarHeapReadMax( Msat_VarHeap_t * p ); extern int Msat_VarHeapGetMax( Msat_VarHeap_t * p ); -#ifdef __cplusplus -} -#endif + + +ABC_NAMESPACE_HEADER_END + + #endif diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c index 1cd795bd..6ac27e2c 100644 --- a/src/sat/msat/msatActivity.c +++ b/src/sat/msat/msatActivity.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -158,3 +161,5 @@ void Msat_SolverClaRescaleActivity( Msat_Solver_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c index ca698866..a464f23a 100644 --- a/src/sat/msat/msatClause.c +++ b/src/sat/msat/msatClause.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -52,7 +55,7 @@ struct Msat_Clause_t_ SeeAlso [] ***********************************************************************/ -bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, Msat_Clause_t ** pClause_out ) +int Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, int fLearned, Msat_Clause_t ** pClause_out ) { int * pAssigns = Msat_SolverReadAssignsArray(p); Msat_ClauseVec_t ** pvWatched; @@ -61,7 +64,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, int nLits, i, j; int nBytes; Msat_Var_t Var; - bool Sign; + int Sign; *pClause_out = NULL; @@ -217,7 +220,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, SeeAlso [] ***********************************************************************/ -void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched ) +void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, int fRemoveWatched ) { if ( fRemoveWatched ) { @@ -249,16 +252,16 @@ void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched SeeAlso [] ***********************************************************************/ -bool Msat_ClauseReadLearned( Msat_Clause_t * pC ) { return pC->fLearned; } +int Msat_ClauseReadLearned( Msat_Clause_t * pC ) { return pC->fLearned; } int Msat_ClauseReadSize( Msat_Clause_t * pC ) { return pC->nSize; } int * Msat_ClauseReadLits( Msat_Clause_t * pC ) { return pC->pData; } -bool Msat_ClauseReadMark( Msat_Clause_t * pC ) { return pC->fMark; } +int Msat_ClauseReadMark( Msat_Clause_t * pC ) { return pC->fMark; } int Msat_ClauseReadNum( Msat_Clause_t * pC ) { return pC->Num; } -bool Msat_ClauseReadTypeA( Msat_Clause_t * pC ) { return pC->fTypeA; } +int Msat_ClauseReadTypeA( Msat_Clause_t * pC ) { return pC->fTypeA; } -void Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark ) { pC->fMark = fMark; } +void Msat_ClauseSetMark( Msat_Clause_t * pC, int fMark ) { pC->fMark = fMark; } void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num ) { pC->Num = Num; } -void Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ) { pC->fTypeA = fTypeA; } +void Msat_ClauseSetTypeA( Msat_Clause_t * pC, int fTypeA ) { pC->fTypeA = fTypeA; } /**Function************************************************************* @@ -272,10 +275,10 @@ void Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ) { pC->fTypeA = fTy SeeAlso [] ***********************************************************************/ -bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC ) +int Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC ) { Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p ); - return (bool)(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC); + return (int )(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC); } /**Function************************************************************* @@ -326,7 +329,7 @@ void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num ) SeeAlso [] ***********************************************************************/ -bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out ) +int Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out ) { // make sure the false literal is pC->pData[1] Msat_Lit_t LitF = MSAT_LITNOT(Lit); @@ -365,7 +368,7 @@ bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, M SeeAlso [] ***********************************************************************/ -bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns ) +int Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns ) { Msat_Var_t Var; int i, j; @@ -485,7 +488,7 @@ void Msat_ClausePrint( Msat_Clause_t * pC ) SeeAlso [] ***********************************************************************/ -void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement ) +void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, int fIncrement ) { int i; for ( i = 0; i < (int)pC->nSize; i++ ) @@ -527,3 +530,5 @@ void Msat_ClausePrintSymbols( Msat_Clause_t * pC ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c index f29de389..71895711 100644 --- a/src/sat/msat/msatClauseVec.c +++ b/src/sat/msat/msatClauseVec.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -230,3 +233,5 @@ Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index b6759a0f..b4b5ff77 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -21,6 +21,7 @@ #ifndef __MSAT_INT_H__ #define __MSAT_INT_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -31,9 +32,13 @@ #include <assert.h> #include <time.h> #include <math.h> + #include "abc_global.h" #include "msat.h" +ABC_NAMESPACE_HEADER_START + + //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// @@ -120,7 +125,7 @@ struct Msat_Solver_t_ double dRandSeed; // For the internal random number generator (makes solver deterministic over different platforms). - bool fVerbose; // the verbosity flag + int fVerbose; // the verbosity flag double dProgress; // Set by 'search()'. // the variable cone and variable connectivity @@ -197,10 +202,10 @@ extern void Msat_SolverClausesIncrementL( Msat_Solver_t * p ); extern void Msat_SolverClausesDecrementL( Msat_Solver_t * p ); extern void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit ); extern void Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC ); -extern bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ); +extern int Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ); extern double Msat_SolverProgressEstimate( Msat_Solver_t * p ); /*=== satSolverSearch.c ===========================================================*/ -extern bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ); +extern int Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ); extern Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p ); extern void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level ); extern Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars ); @@ -222,29 +227,29 @@ extern void Msat_OrderVarAssigned( Msat_Order_t * p, int Var ); extern void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ); extern void Msat_OrderUpdate( Msat_Order_t * p, int Var ); /*=== satClause.c ===========================================================*/ -extern bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearnt, Msat_Clause_t ** pClause_out ); +extern int Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, int fLearnt, Msat_Clause_t ** pClause_out ); extern Msat_Clause_t * Msat_ClauseCreateFake( Msat_Solver_t * p, Msat_IntVec_t * vLits ); extern Msat_Clause_t * Msat_ClauseCreateFakeLit( Msat_Solver_t * p, Msat_Lit_t Lit ); -extern bool Msat_ClauseReadLearned( Msat_Clause_t * pC ); +extern int Msat_ClauseReadLearned( Msat_Clause_t * pC ); extern int Msat_ClauseReadSize( Msat_Clause_t * pC ); extern int * Msat_ClauseReadLits( Msat_Clause_t * pC ); -extern bool Msat_ClauseReadMark( Msat_Clause_t * pC ); -extern void Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark ); +extern int Msat_ClauseReadMark( Msat_Clause_t * pC ); +extern void Msat_ClauseSetMark( Msat_Clause_t * pC, int fMark ); extern int Msat_ClauseReadNum( Msat_Clause_t * pC ); extern void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num ); -extern bool Msat_ClauseReadTypeA( Msat_Clause_t * pC ); -extern void Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ); -extern bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC ); +extern int Msat_ClauseReadTypeA( Msat_Clause_t * pC ); +extern void Msat_ClauseSetTypeA( Msat_Clause_t * pC, int fTypeA ); +extern int Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC ); extern float Msat_ClauseReadActivity( Msat_Clause_t * pC ); extern void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num ); -extern void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched ); -extern bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out ); -extern bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns ); +extern void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, int fRemoveWatched ); +extern int Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out ); +extern int Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns ); extern void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out ); extern void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC ); extern void Msat_ClausePrint( Msat_Clause_t * pC ); extern void Msat_ClausePrintSymbols( Msat_Clause_t * pC ); -extern void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement ); +extern void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, int fIncrement ); extern unsigned Msat_ClauseComputeTruth( Msat_Solver_t * p, Msat_Clause_t * pC ); /*=== satSort.c ===========================================================*/ extern void Msat_SolverSortDB( Msat_Solver_t * p ); @@ -284,4 +289,8 @@ extern int Msat_MmStepReadMemUsage( Msat_MmStep_t * p ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_HEADER_END + #endif diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c index 439661f4..7e0dc0dd 100644 --- a/src/sat/msat/msatMem.c +++ b/src/sat/msat/msatMem.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -31,7 +34,7 @@ struct Msat_MmFixed_t_ int nEntriesAlloc; // the total number of entries allocated int nEntriesUsed; // the number of entries in use int nEntriesMax; // the max number of entries in use - char * pEntriesFree; // the linked list of ABC_FREE entries + char * pEntriesFree; // the linked list of free entries // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -48,8 +51,8 @@ struct Msat_MmFlex_t_ { // information about individual entries int nEntriesUsed; // the number of entries allocated - char * pCurrent; // the current pointer to ABC_FREE memory - char * pEnd; // the first entry outside the ABC_FREE memory + char * pCurrent; // the current pointer to free memory + char * pEnd; // the first entry outside the free memory // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -160,7 +163,7 @@ char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p ) char * pTemp; int i; - // check if there are still ABC_FREE entries + // check if there are still free entries if ( p->nEntriesUsed == p->nEntriesAlloc ) { // need to allocate more entries assert( p->pEntriesFree == NULL ); @@ -189,7 +192,7 @@ char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p ) p->nEntriesUsed++; if ( p->nEntriesMax < p->nEntriesUsed ) p->nEntriesMax = p->nEntriesUsed; - // return the first entry in the ABC_FREE entry list + // return the first entry in the free entry list pTemp = p->pEntriesFree; p->pEntriesFree = *((char **)pTemp); return pTemp; @@ -210,7 +213,7 @@ void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry ) { // decrement the counter of used entries p->nEntriesUsed--; - // add the entry to the linked list of ABC_FREE entries + // add the entry to the linked list of free entries *((char **)pEntry) = p->pEntriesFree; p->pEntriesFree = pEntry; } @@ -244,7 +247,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p ) } // set the last link *((char **)pTemp) = NULL; - // set the ABC_FREE entry list + // set the free entry list p->pEntriesFree = p->pChunks[0]; // set the correct statistics p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; @@ -346,7 +349,7 @@ void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose ) char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes ) { char * pTemp; - // check if there are still ABC_FREE entries + // check if there are still free entries if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd ) { // need to allocate more entries if ( p->nChunks == p->nChunksAlloc ) @@ -527,3 +530,5 @@ int Msat_MmStepReadMemUsage( Msat_MmStep_t * p ) nMemTotal += p->pMems[i]->nMemoryAlloc; return nMemTotal; } +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c index 7d8484d5..2904607f 100644 --- a/src/sat/msat/msatOrderH.c +++ b/src/sat/msat/msatOrderH.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -403,3 +406,5 @@ void Msat_HeapPercolateDown( Msat_Order_t * p, int i ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c index 4db7ff7b..2be6b47b 100644 --- a/src/sat/msat/msatOrderJ.c +++ b/src/sat/msat/msatOrderJ.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + /* The J-boundary (justification boundary) is defined as a set of unassigned variables belonging to the cone of interest, such that for each of them, @@ -470,3 +473,5 @@ void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c index 0bcaf6b2..f025920b 100644 --- a/src/sat/msat/msatQueue.c +++ b/src/sat/msat/msatQueue.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -155,3 +158,5 @@ void Msat_QueueClear( Msat_Queue_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c index ba33278c..b2cae898 100644 --- a/src/sat/msat/msatRead.c +++ b/src/sat/msat/msatRead.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -133,7 +136,7 @@ static void skipLine( char ** pIn ) static int Msat_ReadInt( char ** pIn ) { int val = 0; - bool neg = 0; + int neg = 0; Msat_ReadWhitespace( pIn ); if ( **pIn == '-' ) @@ -194,7 +197,7 @@ static void Msat_ReadClause( char ** pIn, Msat_Solver_t * p, Msat_IntVec_t * pLi SeeAlso [] ***********************************************************************/ -static bool Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, bool fVerbose ) +static int Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, int fVerbose ) { Msat_Solver_t * p = NULL; // Suppress "might be used uninitialized" Msat_IntVec_t * pLits = NULL; // Suppress "might be used uninitialized" @@ -251,10 +254,10 @@ static bool Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, bool fVerbose ) SeeAlso [] ***********************************************************************/ -bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ) +int Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ) { char * pText; - bool Value; + int Value; pText = Msat_FileRead( pFile ); Value = Msat_ReadDimacs( pText, p, fVerbose ); ABC_FREE( pText ); @@ -266,3 +269,5 @@ bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index 6a518212..622e94aa 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -47,7 +50,7 @@ int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); } int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; } Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; } -Msat_Lit_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; } +Msat_Type_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return (Msat_Type_t)p->pAssigns[Var]; } Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; } Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; } int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; } @@ -151,7 +154,7 @@ Msat_IntVec_t * Msat_SolverReadVarsUsed( Msat_Solver_t * p ) Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, - bool fVerbose ) + int fVerbose ) { Msat_Solver_t * p; int i; @@ -498,3 +501,5 @@ void Msat_SolverSetupTruthTables( unsigned uTruths[][2] ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index 0462f11b..3312c23d 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -39,7 +42,7 @@ SeeAlso [] ***********************************************************************/ -bool Msat_SolverAddVar( Msat_Solver_t * p, int Level ) +int Msat_SolverAddVar( Msat_Solver_t * p, int Level ) { if ( p->nVars == p->nVarsAlloc ) Msat_SolverResize( p, 2 * p->nVarsAlloc ); @@ -59,10 +62,10 @@ bool Msat_SolverAddVar( Msat_Solver_t * p, int Level ) SeeAlso [] ***********************************************************************/ -bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * vLits ) +int Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * vLits ) { Msat_Clause_t * pC; - bool Value; + int Value; Value = Msat_ClauseCreate( p, vLits, 0, &pC ); if ( pC != NULL ) Msat_ClauseVecPush( p->vClauses, pC ); @@ -132,7 +135,7 @@ void Msat_SolverPrintStats( Msat_Solver_t * p ) SeeAlso [] ***********************************************************************/ -bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit ) +int Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit ) { Msat_SearchParams_t Params = { 0.95, 0.999 }; double nConflictsLimit, nLearnedLimit; @@ -208,3 +211,5 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatSolverIo.c b/src/sat/msat/msatSolverIo.c index 05b7f6a9..38610b4d 100644 --- a/src/sat/msat/msatSolverIo.c +++ b/src/sat/msat/msatSolverIo.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -175,3 +178,5 @@ char * Msat_TimeStamp() //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c index 11a6540c..b3190e39 100644 --- a/src/sat/msat/msatSolverSearch.c +++ b/src/sat/msat/msatSolverSearch.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -45,7 +48,7 @@ static void Msat_SolverReduceDB( Msat_Solver_t * p ); SeeAlso [] ***********************************************************************/ -bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ) +int Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ) { assert( Msat_QueueReadSize(p->pQueue) == 0 ); if ( p->fVerbose ) @@ -167,7 +170,7 @@ Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits ) SeeAlso [] ***********************************************************************/ -bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ) +int Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ) { Msat_Var_t Var = MSAT_LIT2VAR(Lit); @@ -276,7 +279,7 @@ Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p ) SeeAlso [] ***********************************************************************/ -bool Msat_SolverSimplifyDB( Msat_Solver_t * p ) +int Msat_SolverSimplifyDB( Msat_Solver_t * p ) { Msat_ClauseVec_t * vClauses; Msat_Clause_t ** pClauses; @@ -627,3 +630,5 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatSort.c b/src/sat/msat/msatSort.c index 3b89d102..a4b34030 100644 --- a/src/sat/msat/msatSort.c +++ b/src/sat/msat/msatSort.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -171,3 +174,5 @@ void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c index 3716dbf7..7144b213 100644 --- a/src/sat/msat/msatVec.c +++ b/src/sat/msat/msatVec.c @@ -20,6 +20,9 @@ #include "msatInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -493,3 +496,5 @@ int Msat_IntVecSortCompare2( int * pp1, int * pp2 ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c index a951071a..0da16eaf 100644 --- a/src/sat/proof/pr.c +++ b/src/sat/proof/pr.c @@ -23,10 +23,14 @@ #include <string.h> #include <assert.h> #include <time.h> + //#include "vec.h" #include "abc_global.h" #include "pr.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -186,7 +190,7 @@ void Pr_ManResize( Pr_Man_t * p, int nVarsNew ) p->pVarTypes = ABC_REALLOC(char, p->pVarTypes, p->nVarsAlloc ); p->pReasons = ABC_REALLOC(Pr_Cls_t *, p->pReasons, p->nVarsAlloc ); p->pWatches = ABC_REALLOC(Pr_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); - // clean the ABC_FREE space + // clean the free space memset( p->pAssigns + nVarsAllocOld, 0xff, sizeof(lit) * (p->nVarsAlloc - nVarsAllocOld) ); memset( p->pSeens + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) ); memset( p->pVarTypes + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) ); @@ -649,10 +653,10 @@ void Pr_ManProofWriteOne( Pr_Man_t * p, Pr_Cls_t * pClause ) if ( p->fProofWrite ) { int v; - fprintf( p->pManProof, "%d", (int)pClause->pProof ); + fprintf( (FILE *)p->pManProof, "%d", (int)pClause->pProof ); for ( v = 0; v < (int)pClause->nLits; v++ ) - fprintf( p->pManProof, " %d", lit_print(pClause->pLits[v]) ); - fprintf( p->pManProof, " 0 0\n" ); + fprintf( (FILE *)p->pManProof, " %d", lit_print(pClause->pLits[v]) ); + fprintf( (FILE *)p->pManProof, " 0 0\n" ); } } @@ -718,7 +722,7 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal ) assert( pReason->pProof > 0 ); p->Counter++; if ( p->fProofWrite ) - fprintf( p->pManProof, "%d * %d %d 0\n", p->Counter, PrevId, (int)pReason->pProof ); + fprintf( (FILE *)p->pManProof, "%d * %d %d 0\n", p->Counter, PrevId, (int)pReason->pProof ); PrevId = p->Counter; if ( p->nClausesA ) @@ -1086,7 +1090,7 @@ int Pr_ManProofWrite( Pr_Man_t * p ) // stop the proof if ( p->fProofWrite ) { - fclose( p->pManProof ); + fclose( (FILE *)p->pManProof ); p->pManProof = NULL; } return RetValue; @@ -1162,7 +1166,7 @@ Pr_Man_t * Pr_ManProofRead( char * pFileName ) for ( ; *pCur && *pCur != ' '; pCur++ ); } // add the clause - if ( !Pr_ManAddClause( p, pArray, pArray + nNumbers, Counter < nRoots, Counter < nClausesA ) ) + if ( !Pr_ManAddClause( p, (unsigned *)pArray, (unsigned *)pArray + nNumbers, Counter < nRoots, Counter < nClausesA ) ) { printf( "Bad clause number %d.\n", Counter ); return NULL; @@ -1204,7 +1208,7 @@ int Pr_ManProofCount_rec( Pr_Cls_t * pClause ) pClause->fVisit = 1; // count the number of visited clauses Counter = 1; - Vec_PtrForEachEntry( pClause->pAntis, pNext, i ) + Vec_PtrForEachEntry( Pr_Cls_t *, pClause->pAntis, pNext, i ) Counter += Pr_ManProofCount_rec( pNext ); return Counter; } @@ -1258,3 +1262,5 @@ p->timeTotal = clock() - clkTotal; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/proof/pr.h b/src/sat/proof/pr.h index bc55e016..9088c89b 100644 --- a/src/sat/proof/pr.h +++ b/src/sat/proof/pr.h @@ -21,6 +21,7 @@ #ifndef __PR_H__ #define __PR_H__ + #ifdef _WIN32 #define inline __inline // compatible with MS VS 6.0 #endif @@ -33,9 +34,10 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif + + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -53,9 +55,11 @@ typedef struct Pr_Man_t_ Pr_Man_t; /*=== pr.c ==========================================================*/ -#ifdef __cplusplus -} -#endif + + +ABC_NAMESPACE_HEADER_END + + #endif diff --git a/src/sat/psat/m114p.h b/src/sat/psat/m114p.h index 5050cb4b..9319d918 100644 --- a/src/sat/psat/m114p.h +++ b/src/sat/psat/m114p.h @@ -3,8 +3,12 @@ #ifndef m114p_h #define m114p_h + #include "m114p_types.h" +ABC_NAMESPACE_HEADER_START + + // SAT solver APIs extern M114p_Solver_t M114p_SolverNew( int fRecordProof ); extern void M114p_SolverDelete( M114p_Solver_t s ); @@ -36,4 +40,8 @@ extern int M114p_SolverGetNextChain( M114p_Solver_t s, int ** ppClaus for ( i = 0, nVars = M114p_SolverGetFirstChain(s, ppClauses, ppVars); nVars; \ i++, nVars = M114p_SolverGetNextChain(s, ppClauses, ppVars) ) + + +ABC_NAMESPACE_HEADER_END + #endif
\ No newline at end of file diff --git a/src/sat/psat/m114p_types.h b/src/sat/psat/m114p_types.h index 54a20c5c..29d70a87 100644 --- a/src/sat/psat/m114p_types.h +++ b/src/sat/psat/m114p_types.h @@ -3,7 +3,11 @@ #ifndef m114p_types_h #define m114p_types_h + +ABC_NAMESPACE_HEADER_START + typedef int M114p_Solver_t; -typedef int lit; -#endif
\ No newline at end of file +ABC_NAMESPACE_HEADER_END + +#endif |