diff options
Diffstat (limited to 'src/sat/bsat')
-rw-r--r-- | src/sat/bsat/module.make | 1 | ||||
-rw-r--r-- | src/sat/bsat/satInter.c | 2 | ||||
-rw-r--r-- | src/sat/bsat/satInterA.c | 970 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 1 | ||||
-rw-r--r-- | src/sat/bsat/satStore.h | 39 |
5 files changed, 997 insertions, 16 deletions
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make index 563c8dfc..1e52cc0a 100644 --- a/src/sat/bsat/module.make +++ b/src/sat/bsat/module.make @@ -1,5 +1,6 @@ SRC += src/sat/bsat/satMem.c \ src/sat/bsat/satInter.c \ + src/sat/bsat/satInterA.c \ src/sat/bsat/satSolver.c \ src/sat/bsat/satStore.c \ src/sat/bsat/satTrace.c \ diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c index 8759aa09..8e07e9f6 100644 --- a/src/sat/bsat/satInter.c +++ b/src/sat/bsat/satInter.c @@ -99,7 +99,7 @@ static inline void Int_ManProofSet( Int_Man_t * p, Sto_Cls_t * pCls, int n SeeAlso [] ***********************************************************************/ -Int_Man_t * Int_ManAlloc( int nVarsAlloc ) +Int_Man_t * Int_ManAlloc() { Int_Man_t * p; // allocate the manager diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c new file mode 100644 index 00000000..513a9044 --- /dev/null +++ b/src/sat/bsat/satInterA.c @@ -0,0 +1,970 @@ +/**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" + +//////////////////////////////////////////////////////////////////////// +/// 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))); } + +// 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 *)malloc( sizeof(Inta_Man_t) ); + memset( p, 0, sizeof(Inta_Man_t) ); + // verification + p->nResLitsAlloc = (1<<16); + p->pResLits = malloc( sizeof(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 = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); + p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); + p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); + p->pVarTypes = (int *) realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc ); + p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc ); + p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * 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 = (int *) realloc( p->pProofNums, sizeof(int) * 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 = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * 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" ); +PRT( "BCP ", p->timeBcp ); +PRT( "Trace ", p->timeTrace ); +PRT( "TOTAL ", p->timeTotal ); +*/ + free( p->pInters ); + free( p->pProofNums ); + free( p->pTrail ); + free( p->pAssigns ); + free( p->pSeens ); + free( p->pVarTypes ); + free( p->pReasons ); + free( p->pWatches ); + free( p->pResLits ); + 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_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 ) // var of A + Inta_ManAigOr( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) ); + else + Inta_ManAigAnd( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) ); + } + + // 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; + 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 ) + { + 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; + } + + Aig_ObjCreatePo( pRes, *Inta_ManAigRead( p, p->pCnf->pTail ) ); + Aig_ManCleanup( pRes ); + + p->pAig = NULL; + return pRes; + +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index ca2954d2..c1bf32a7 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -71,6 +71,7 @@ static inline int lit_var (lit l) { return l >> 1; } static inline int lit_sign (lit l) { return l & 1; } static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } +static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } //================================================================================================= diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h index 346b59df..b66abc8f 100644 --- a/src/sat/bsat/satStore.h +++ b/src/sat/bsat/satStore.h @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [pr.h] + FileName [satStore.h] SystemName [ABC: Logic synthesis and verification system.] @@ -18,11 +18,13 @@ ***********************************************************************/ -#ifndef __PR_H__ -#define __PR_H__ +#ifndef __SAT_STORE_H__ +#define __SAT_STORE_H__ + +#include "satSolver.h" /* - The trace of SAT solving contains the original clause of the problem + The trace of SAT solving contains the original clauses of the problem along with the learned clauses derived during SAT solving. The first line of the resulting file contains 3 numbers instead of 2: c <num_vars> <num_all_clauses> <num_root_clauses> @@ -54,7 +56,18 @@ extern "C" { /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// +/* typedef unsigned lit; +// variable/literal conversions (taken from MiniSat) +static inline lit toLit (int v) { return v + v; } +static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } +static inline lit lit_neg (lit l) { return l ^ 1; } +static inline int lit_var (lit l) { return l >> 1; } +static inline int lit_sign (lit l) { return l & 1; } +static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } +static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } +static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } +*/ typedef struct Sto_Cls_t_ Sto_Cls_t; struct Sto_Cls_t_ @@ -87,16 +100,6 @@ struct Sto_Man_t_ char * pChunkLast; // the last memory chunk }; -// variable/literal conversions (taken from MiniSat) -static inline lit toLit (int v) { return v + v; } -static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } -static inline lit lit_neg (lit l) { return l ^ 1; } -static inline int lit_var (lit l) { return l >> 1; } -static inline int lit_sign (lit l) { return l & 1; } -static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } -static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } -static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } - // iterators through the clauses #define Sto_ManForEachClause( p, pCls ) for( pCls = p->pHead; pCls; pCls = pCls->pNext ) #define Sto_ManForEachClauseRoot( p, pCls ) for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext ) @@ -121,10 +124,16 @@ extern Sto_Man_t * Sto_ManLoadClauses( char * pFileName ); /*=== satInter.c ==========================================================*/ typedef struct Int_Man_t_ Int_Man_t; -extern Int_Man_t * Int_ManAlloc( int nVarsAlloc ); +extern Int_Man_t * Int_ManAlloc(); extern void Int_ManFree( Int_Man_t * p ); extern int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult ); +/*=== satInterA.c ==========================================================*/ +typedef struct Inta_Man_t_ Inta_Man_t; +extern Inta_Man_t * Inta_ManAlloc(); +extern void Inta_ManFree( Inta_Man_t * p ); +extern void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose ); + #ifdef __cplusplus } #endif |