/**CFile*********************************************************************** FileName [puresatArosat.c] PackageName [puresat] Synopsis [Abstraction refinement for large scale invariant checking.] Description [This file contains the functions to check invariant properties by the PureSAT abstraction refinement algorithm, which is entirely based on SAT solver, the input of which could be either CNF or AIG. It has several parts: * Localization-reduction base Abstraction * K-induction or interpolation to prove the truth of a property * Bounded Model Checking to find bugs * Incremental concretization based methods to verify abstract bugs * Incremental SAT solver to improve efficiency * UNSAT proof based method to obtain refinement * AROSAT to bring in only necessary latches into unsat proofs * Bridge abstraction to get compact coarse refinement * Refinement minization to guarrantee minimal refinements * Unsat proof-based refinement minimization to eliminate multiple candidate by on SAT test * Refinement prediction to decrease the number of refinement iterations * Dynamic switching to redistribute computional resources to improve efficiency For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", " Abstraction in symbolic model checking using satisfiability as the only decision procedure", "Efficient computation of small abstraction refinements", and "Efficient abstraction refinement in interpolation-based unbounded model checking"] Author [Bing Li] Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.] ******************************************************************************/ #include "puresatInt.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [comparing score for sorting] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ static int ScoreCompare( const void * node1, const void * node2) { int v1; int v2; int s1, s2; v1 = *(int *)(node1); v2 = *(int *)(node2); s1 = *((int *)(node1) + 1); s2 = *((int *)(node2) + 1); if(s1 == s2) { return(v1 > v2); } return(s1 < s2); } /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ typedef int (*ASIMPLY_FN) (satManager_t *cm, satLevel_t *d, long v, long left, long right); ASIMPLY_FN ASImplicationFN[64]= { AS_ImplyStop, /* 0 */ AS_ImplyConflict, /* 1 */ AS_ImplyLeftForward, /* 2 */ AS_ImplyLeftForward, /* 3 */ AS_ImplyStop, /* 4 */ AS_ImplyConflict, /* 5 */ AS_ImplyLeftForward, /* 6 */ AS_ImplyLeftForward, /* 7 */ AS_ImplySplit, /* 8 */ AS_ImplyConflict, /* 9 */ AS_ImplyLeftForward, /* 10 */ AS_ImplyLeftForward, /* 11 */ AS_ImplySplit, /* 12 */ AS_ImplyConflict, /* 13 */ AS_ImplyLeftForward, /* 14 */ AS_ImplyLeftForward, /* 15 */ AS_ImplyStop, /* 16 */ AS_ImplyConflict, /* 17 */ AS_ImplyRightForward, /* 18 */ AS_ImplyRightForward, /* 19 */ AS_ImplyConflict, /* 20 */ AS_ImplyStop, /* 21 */ AS_ImplyForwardOne, /* 22 */ AS_ImplyForwardOne, /* 23 */ AS_ImplyPropRight, /* 24 */ AS_ImplyPropRightOne, /* 25 */ AS_ImplyStop, /* 26 */ AS_ImplyStop, /* 27 */ AS_ImplyPropRight, /* 28 */ AS_ImplyPropRightOne, /* 29 */ AS_ImplyStop, /* 30 */ AS_ImplyStop, /* 31 */ AS_ImplySplit, /* 32 */ AS_ImplyConflict, /* 33 */ AS_ImplyRightForward, /* 34 */ AS_ImplyRightForward, /* 35 */ AS_ImplyPropLeft, /* 36 */ AS_ImplyPropLeftOne, /* 37 */ AS_ImplyStop, /* 38 */ AS_ImplyStop, /* 39 */ AS_ImplySplit, /* 40 */ AS_ImplyPropLeftRight, /* 41 */ AS_ImplyStop, /* 42 */ AS_ImplyStop, /* 43 */ AS_ImplySplit, /* 44 */ AS_ImplyPropLeftRight, /* 45 */ AS_ImplyStop, /* 46 */ AS_ImplyStop, /* 47 */ AS_ImplySplit, /* 48 */ AS_ImplyConflict, /* 49 */ AS_ImplyRightForward, /* 50 */ AS_ImplyRightForward, /* 51 */ AS_ImplyPropLeft, /* 52 */ AS_ImplyPropLeftOne, /* 53 */ AS_ImplyStop, /* 54 */ AS_ImplyStop, /* 55 */ AS_ImplySplit, /* 56 */ AS_ImplyPropLeftRight, /* 57 */ AS_ImplyStop, /* 58 */ AS_ImplyStop, /* 59 */ AS_ImplySplit, /* 60 */ AS_ImplyPropLeftRight, /* 61 */ AS_ImplyStop, /* 62 */ AS_ImplyStop, /* 63 */ }; /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [No further implcation when this function is called.] Description [No further implcation when this function is called. 0 0 0 1 | | | | --- --- --- --- / \ / \ / \ / \ 0 X X 0 0 0 1 1 ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyStop( satManager_t *cm, satLevel_t *d, long v, long left, long right) { return(0); } /**Function******************************************************************** Synopsis [No further implcation when this function is called.] Description [No further implcation when this function is called. and need split on output. 0 | --- / \ X X ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplySplit( satManager_t *cm, satLevel_t *d, long v, long left, long right) { return(0); } /**Function******************************************************************** Synopsis [The conflict happens.] Description [The conflict happens when 0 1 1 1 1 | | | | | --- --- --- --- --- / \ / \ / \ / \ / \ 1 1 X 0 0 X 1 0 0 1 ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyConflict( satManager_t *cm, satLevel_t *d, long v, long left, long right) { if(left != 2) { d->conflict = SATnormalNode(v); } return(0); } /**Function******************************************************************** Synopsis [A value implied to output due to left child.] Description [A value implied to output due to left child X X | | --- --- / \ / \ 0 1 0 X ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyLeftForward( satManager_t *cm, satLevel_t *d, long v, long left, long right) { if(sat_ASImp(cm,d,v,0)) return(0); v = SATnormalNode(v); left = SATnormalNode(left); SATvalue(v) = 0; SATmakeImplied(v, d); SATante(v) = left; sat_Enqueue(cm->queue, v); SATflags(v) |= InQueueMask; SATflags(v) |= (SATflags(left) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to output due to right child.] Description [A value implied to output due to right child X X | | --- --- / \ / \ 1 0 X 0 ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyRightForward( satManager_t *cm, satLevel_t *d, long v, long left, long right) { if(sat_ASImp(cm,d,v,0)) return(0); v = SATnormalNode(v); right = SATnormalNode(right); SATvalue(v) = 0; SATmakeImplied(v, d); SATante(v) = right; sat_Enqueue(cm->queue, v); SATflags(v) |= InQueueMask; SATflags(v) |= (SATflags(right) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to output due to both child.] Description [A value implied to output due to both child X | --- / \ 1 1 ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyForwardOne( satManager_t *cm, satLevel_t *d, long v, long left, long right) { if(sat_ASImp(cm,d,v,1)) return(0); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATvalue(v) = 1; SATmakeImplied(v, d); SATante(v) = right; SATante2(v) = left; sat_Enqueue(cm->queue, v); SATflags(v) |= InQueueMask; SATflags(v) |= (SATflags(right) & ObjMask); SATflags(v) |= (SATflags(left) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to right child due to both output and left.] Description [A value implied to right child due to both output and left 0 | --- / \ 1 X ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyPropRight( satManager_t *cm, satLevel_t *d, long v, long left, long right) { int isInverted; isInverted = SATisInverted(right); if(sat_ASImp(cm,d,right, isInverted)) return(0); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATmakeImplied(right, d); SATvalue(right) = isInverted; SATante(right) = left; SATante2(right) = v; sat_Enqueue(cm->queue, right); SATflags(right) |= InQueueMask; SATflags(right) |= (SATflags(left) & ObjMask); SATflags(right) |= (SATflags(v) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to right child due to both output and left.] Description [A value implied to right child due to both output and left 1 | --- / \ 1 X ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyPropRightOne( satManager_t *cm, satLevel_t *d, long v, long left, long right) { int isInverted; if(sat_ASImp(cm,d,right,!SATisInverted(right))) return(0); isInverted = SATisInverted(right); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATmakeImplied(right, d); SATante(right) = v; SATvalue(right) = !isInverted; sat_Enqueue(cm->queue, right); SATflags(right) |= InQueueMask; SATflags(right) |= (SATflags(v) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to left child due to both output and right.] Description [A value implied to left child due to both output and right 0 | --- / \ X 1 ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyPropLeft( satManager_t *cm, satLevel_t *d, long v, long left, long right) { int isInverted; if(sat_ASImp(cm,d,left,SATisInverted(left))) return(0); isInverted = SATisInverted(left); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATmakeImplied(left, d); SATante(left) = v; SATante2(left) = right; SATvalue(left) = isInverted; sat_Enqueue(cm->queue, left); SATflags(left) |= InQueueMask; SATflags(left) |= (SATflags(v) & ObjMask); SATflags(left) |= (SATflags(right) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to left child due to both output and right.] Description [A value implied to left child due to both output and right 1 | --- / \ X 1 ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyPropLeftOne( satManager_t *cm, satLevel_t *d, long v, long left, long right) { int isInverted; if(sat_ASImp(cm,d,left,!SATisInverted(left))) return(0); isInverted = SATisInverted(left); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); SATmakeImplied(left, d); SATante(left) = v; SATvalue(left) = !isInverted; sat_Enqueue(cm->queue, left); SATflags(left) |= InQueueMask; SATflags(left) |= (SATflags(v) & ObjMask); cm->each->nAigImplications++; return(0); } /**Function******************************************************************** Synopsis [A value implied to left and right child due to output.] Description [A value implied to left and right child due to output 1 | --- / \ X X ] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyPropLeftRight( satManager_t *cm, satLevel_t *d, long v, long left, long right) { int isLeftInverted; int isRightInverted; int lImp=1,rImp=1; if(left == right) return 1; if(sat_ASImp(cm,d,left,!SATisInverted(left))) lImp = 0; if(sat_ASImp(cm,d,right,!SATisInverted(right))) rImp = 0; isLeftInverted = SATisInverted(left); isRightInverted = SATisInverted(right); v = SATnormalNode(v); left = SATnormalNode(left); right = SATnormalNode(right); if(lImp){ SATmakeImplied(left, d); SATante(left) = v; SATvalue(left) = !isLeftInverted; sat_Enqueue(cm->queue, left); SATflags(left) |= InQueueMask; SATflags(left) |= (SATflags(v) & ObjMask); cm->each->nAigImplications ++; } if(rImp){ SATmakeImplied(right, d); SATante(right) = v; SATvalue(right) = !isRightInverted; sat_Enqueue(cm->queue, right); SATflags(right) |= InQueueMask; SATflags(right) |= (SATflags(v) & ObjMask); cm->each->nAigImplications ++; } return(0); } /**Function******************************************************************** Synopsis [erase previous assignments by arosat] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_Undo( satManager_t *cm, satLevel_t *d) { satArray_t *implied, *satisfied; int size, i; long *space, v; satVariable_t *var; int dfs; implied = d->implied; space = implied->space; size = implied->num; for(i=0; iscores[0]/SCOREUNIT; cm->assignedArray[dfs]--; #if DBG assert(cm->assignedArray[dfs]>=0); #endif } } cm->implicatedSoFar -= size; if(d->satisfied) { satisfied = d->implied; space = satisfied->space; size = satisfied->num; for(i=0; isatisfied->num = 0; } if(d->level > 0) { if((cm->decisionHead[d->level-1]).currentVarPos < cm->currentVarPos) cm->currentVarPos = (cm->decisionHead[d->level-1]).currentVarPos; } else cm->currentVarPos = d->currentVarPos; d->implied->num = 0; d->currentVarPos = 0; d->conflict = 0; } /**Function******************************************************************** Synopsis [implication for cnf] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_ImplyCNF( satManager_t *cm, satLevel_t *d, long v, satArray_t *wl) { int size, i, j; long *space; long lit, *plit, *tplit; int dir; long nv, tv, *oplit, *wlit; int isInverted, value; int tsize, inverted; long cur, clit; satStatistics_t *stats; satOption_t *option; satQueue_t *Q; satVariable_t *var; long tmpv; size = wl->num; space = wl->space; Q = cm->queue; stats = cm->each; option = cm->option; nv = 0; wlit = 0; for(i=0; iconflict = nv; wl->num = size; return; } else if(value > 1) { /** implication **/ if(sat_ASImp(cm,d,tmpv,!isInverted)) break; SATvalue(tv) = !isInverted; SATmakeImplied(tv, d); SATante(tv) = nv; if((SATflags(tv) & InQueueMask) == 0) { sat_Enqueue(Q, tv); SATflags(tv) |= InQueueMask; } stats->nCNFImplications++; /** to identify the objective dependent clause for incremental * SAT **/ if(option->incTraceObjective == 1) { tsize = SATnumLits(nv); for(j=0, tplit=(long*)SATfirstLit(nv); jwl[inverted]) { sat_ArrayInsert(var->wl[inverted], (long)oplit); } else { var->wl[inverted] = sat_ArrayAlloc(4); sat_ArrayInsert(var->wl[inverted], (long)oplit); } break; } } wl->num = size; } /**Function******************************************************************** Synopsis [implication for aig node and cnf ] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ImplyNode( satManager_t *cm, satLevel_t *d, long v) { long *fan, cur; int value; int i, size; long left, right; satVariable_t *var; satArray_t *wlArray; value = SATvalue(v) ^ 1; var = SATgetVariable(v); wlArray = var->wl[value]; /** implcation on CNF **/ if(wlArray && wlArray->size) { AS_ImplyCNF(cm, d, v, wlArray); } if(d->conflict) return(0); /** implication on AIG **/ fan = (long *)SATfanout(v); size = SATnFanout(v); for(i=0; i> 1; cur = SATnormalNode(cur); left = SATleftChild(cur); right = SATrightChild(cur); value = SATgetValue(left, right, cur); #if DBG assert(SATflags(SATnormalNode(left))&CoiMask); assert(SATflags(SATnormalNode(right))&CoiMask); #endif (ASImplicationFN[value])(cm, d, cur, left, right); if(d->conflict) return(0); } left = SATleftChild(v); right = SATrightChild(v); value = SATgetValue(left, right, v); #if DBG assert(left==bAig_NULL||SATflags(SATnormalNode(left))&CoiMask); assert(right==bAig_NULL||SATflags(SATnormalNode(right))&CoiMask); #endif (ASImplicationFN[value])(cm, d, v, left, right); if(d->conflict) return(0); return(1); } /**Function******************************************************************** Synopsis [The main procedure of implication propogation] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_ImplicationMain( satManager_t *cm, satLevel_t *d) { satQueue_t *Q, *BDDQ; long v; Q = cm->queue; BDDQ = cm->BDDQueue; while(1) { v = sat_Dequeue(Q); while(v && d->conflict == 0) { AS_ImplyNode(cm, d, v); SATflags(v) &= ResetInQueueMask; v = sat_Dequeue(Q); } if(d->conflict) break; if(cm->option->BDDImplication) { v = sat_Dequeue(Q); while(v && d->conflict == 0) { sat_ImplyBDD(cm, d, v); SATflags(v) &= ResetInQueueMask; v = sat_Dequeue(Q); } } if(Q->size == 0 && BDDQ->size == 0) break; } sat_CleanImplicationQueue(cm); cm->implicatedSoFar += d->implied->num; } /**Function******************************************************************** Synopsis [Implication for assertation in one array] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_ImplyArray( satManager_t *cm, satLevel_t *d, satArray_t *arr) { int i, size; long v; int inverted, value; satQueue_t *Q; satVariable_t *var; int dfs; if(arr == 0) return; if(cm->status)return; size = arr->num; Q = cm->queue; for(i=0; ispace[i]; inverted = SATisInverted(v); v = SATnormalNode(v); value = !inverted; if(SATvalue(v) < 2) { if(SATvalue(v) == value) continue; else { cm->status = SAT_UNSAT; d->conflict = v; return; } } var = SATgetVariable(v); dfs = var->scores[0]/SCOREUNIT; if(dfs==cm->LatchLevel){ if(!(SATflags(SATnormalNode(v))&AssignedMask)){ SATflags(SATnormalNode(v))|=AssignedMask; cm->assignedArray[dfs]++; #if DBG assert(cm->assignedArray[dfs]<=cm->numArray[dfs]); #endif if(cm->assignedArray[dfs]==cm->numArray[dfs]) sat_ASmergeLevel(cm); } } SATvalue(v) = value; SATmakeImplied(v, d); if(cm->option->coreGeneration){ st_insert(cm->anteTable,(char *)SATnormalNode(v),(char *)SATnormalNode(v)); } if((SATflags(v) & InQueueMask) == 0) { sat_Enqueue(Q, v); SATflags(v) |= InQueueMask; } } } /**Function******************************************************************** Synopsis [Preprocessing step for AROSAT] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_PreProcessing(satManager_t *cm) { satLevel_t *d; /** create implication queue **/ cm->queue = sat_CreateQueue(1024); cm->BDDQueue = sat_CreateQueue(1024); cm->unusedAigQueue = sat_CreateQueue(1024); /** create variable array : one can reduce size of variable array using mapping. for fanout free internal node.... **/ if(cm->variableArray == 0) { cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1); memset(cm->variableArray, 0, sizeof(satVariable_t) * (cm->initNumVariables+1)); } cm->auxArray = sat_ArrayAlloc(1024); cm->nonobjUnitLitArray = sat_ArrayAlloc(128); cm->objUnitLitArray = sat_ArrayAlloc(128); if(cm->option->AbRf == 0) sat_CompactFanout(cm); /*assign initial layer score to variables*/ sat_InitLayerScore(cm); /** create decision stack **/ if(cm->decisionHeadSize == 0) { cm->decisionHeadSize = 32; cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize); memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize); } cm->currentDecision = -1; /** to avoid purify warning **/ SATvalue(2) = 2; SATflags(0) = 0; cm->initNodesArraySize = cm->nodesArraySize; cm->beginConflict = cm->nodesArraySize; /** incremental SAT.... **/ if(cm->option->incTraceObjective) { sat_RestoreForwardedClauses(cm, 0); } else if(cm->option->incAll) { sat_RestoreForwardedClauses(cm, 1); } if(cm->option->incTraceObjective) { sat_MarkObjectiveFlagToArray(cm, cm->obj); sat_MarkObjectiveFlagToArray(cm, cm->objCNF); } /** Level 0 decision.... **/ d = sat_AllocLevel(cm); sat_ApplyForcedAssignmentMain(cm, d); if(cm->status == SAT_UNSAT) return; if(cm->option->coreGeneration){ cm->rm = ALLOC(RTManager_t, 1); memset(cm->rm,0,sizeof(RTManager_t)); } AS_ImplyArray(cm, d, cm->auxObj); AS_ImplyArray(cm, d, cm->obj); AS_ImplyArray(cm,d,cm->assertArray); AS_ImplicationMain(cm, d); if(d->conflict) { cm->status = SAT_UNSAT; } if(cm->status == 0) { if(cm->option->incDistill) { sat_IncrementalUsingDistill(cm); } } } /**Function******************************************************************** Synopsis [backtrack procedure for arosat] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_Backtrack( satManager_t *cm, int level) { satLevel_t *d; d = SATgetDecision(cm->currentDecision); while(1) { if(d->level <= level) break; AS_Undo(cm, d); cm->currentDecision--; if(cm->currentDecision == -1) break; d = SATgetDecision(cm->currentDecision); } return; } /**Function******************************************************************** Synopsis [procedure for updating score] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_UpdateScore( satManager_t *cm) { satArray_t *one, *tmp; satArray_t *ordered; satVariable_t *var; int size, i; long v; int value; int baseScore,realScore,newNum; ordered = cm->orderedVariableArray; one = sat_ArrayAlloc(ordered->num); tmp = sat_ArrayAlloc(ordered->num); size = ordered->num; for(i=0; ispace[i]; if(SATvalue(v) < 2 && SATlevel(v) == 0) continue; var = SATgetVariable(v); baseScore =(var->scores[0]/SCOREUNIT)*SCOREUNIT; realScore = var->scores[0]%SCOREUNIT; newNum = var->litsCount[0] - var->lastLitsCount[0]; var->scores[0] = baseScore + (realScore>>1) + newNum; baseScore =(var->scores[1]/SCOREUNIT)*SCOREUNIT; realScore = var->scores[1]%SCOREUNIT; newNum = var->litsCount[1] - var->lastLitsCount[1]; var->scores[1] = baseScore + (realScore>>1) + newNum; var->lastLitsCount[0] = var->litsCount[0]; var->lastLitsCount[1] = var->litsCount[1]; if((var->scores[0] + var->scores[1]) < 1) { sat_ArrayInsert(one, v); } else { value = (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1]; sat_ArrayInsert(tmp, v); sat_ArrayInsert(tmp, value); } } qsort(tmp->space, (tmp->num)>>1, sizeof(long)*2, ScoreCompare); ordered->num = 0; size = tmp->num; for(i=0; ispace[i]; sat_ArrayInsert(ordered, v); var = SATgetVariable(v); var->pos = (i>>1); i++; } size = one->num; for(i=0; ispace[i]; var = SATgetVariable(v); var->pos = ordered->num; sat_ArrayInsert(ordered, v); } sat_ArrayFree(one); sat_ArrayFree(tmp); cm->orderedVariableArray = ordered; cm->currentVarPos = 0; for(i=1; icurrentDecision; i++) { cm->decisionHead[i].currentVarPos = 0; } if(cm->option->verbose > 3) sat_PrintScore(cm); } /**Function******************************************************************** Synopsis [Periodically executed operations] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_PeriodicFunctions(satManager_t *cm) { satStatistics_t *stats; satOption_t *option; int nDecisions; int gap; stats = cm->each; option = cm->option; nDecisions = stats->nDecisions-stats->nShrinkDecisions; if(nDecisions && !(nDecisions % option->decisionAgeInterval)) { if(option->decisionAgeRestart) { gap = stats->nConflictCl-stats->nOldConflictCl; if(gap > option->decisionAgeInterval>>2) { AS_UpdateScore(cm); AS_Backtrack(cm, cm->lowestBacktrackLevel); cm->currentTopConflict = cm->literals->last-1; cm->currentTopConflictCount = 0; cm->lowestBacktrackLevel = MAXINT; } stats->nOldConflictCl = stats->nConflictCl; } else { AS_UpdateScore(cm); } } if(stats->nBacktracks > option->nextClauseDeletion) { option->nextClauseDeletion += option->clauseDeletionInterval; sat_ClauseDeletion(cm); } } /**Function******************************************************************** Synopsis [Decision procedure] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ satLevel_t * AS_MakeDecision(satManager_t *cm) { satLevel_t *d; int value; long v; satStatistics_t *stats; d = SATgetDecision(cm->currentDecision); if(cm->queue->size) return(d); d = sat_AllocLevel(cm); v = 0; v = sat_DecisionBasedOnBDD(cm, d); if(v == 0) v = sat_DecisionBasedOnScore(cm, d); if(v == 0) return(0); sat_ASDec(cm,d,v); stats = cm->each; stats->nDecisions++; value = !(SATisInverted(v)); v = SATnormalNode(v); d->decisionNode = v; if((SATgetVariable(v)->RecVal)!=0){ if(SATgetVariable(v)->RecVal==-1) value=0; else{ #if DBG assert(SATgetVariable(v)->RecVal==1); #endif value=1; } } SATvalue(v) = value; SATmakeImplied(v, d); #if DBG assert(SATflags(v)&CoiMask); #endif sat_Enqueue(cm->queue, v); SATflags(v) |= InQueueMask; return(d); } /**Function******************************************************************** Synopsis [Find UIP for generating conflict clauses] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_FindUIP( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit) { long conflicting; int nMarked, value; int first, i,j; long *space, v,left,right,inverted,result,*tmp; satArray_t *implied; satOption_t *option; RTnode_t tmprt; int size = 0; long *lp, *tmpIP,ante,ante2,node; RTManager_t * rm = cm->rm; conflicting = d->conflict; nMarked = 0; option = cm->option; if(option->incTraceObjective) *objectFlag = 0; else *objectFlag = ObjMask; (*objectFlag) |= (SATflags(conflicting) & ObjMask); /* find seed from conflicting clause to find unique implication point. * */ clauseArray->num = 0; sat_MarkNodeInConflict( cm, d, &nMarked, objectFlag, bLevel, clauseArray); /* Traverse implication graph backward */ first = 1; implied = d->implied; space = implied->space+implied->num-1; if(cm->option->coreGeneration){ /*if last conflict is CNF*/ if(SATflags(conflicting)&IsCNFMask){ /*is conflict CNF*/ if(SATflags(conflicting)&IsConflictMask){ if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){ fprintf(vis_stderr,"RTree node of conflict cnf %ld is not in RTreeTable\n",ante); exit(0); } else{ rm->root = tmprt; } } /*CNF but not conflict*/ else{ rm->root = RTCreateNode(rm); RT_oriClsIdx(rm->root) = conflicting; size = SATnumLits(conflicting); RT_fSize(rm->root) = size; } } /*if last conflict is AIG*/ else{ rm->root = RTCreateNode(rm); node = SATnormalNode(conflicting); left = SATleftChild(node); right = SATrightChild(node); result = PureSat_IdentifyConflict(cm,left,right,conflicting); inverted = SATisInverted(left); left = SATnormalNode(left); left = inverted ? SATnot(left) : left; inverted = SATisInverted(right); right = SATnormalNode(right); right = inverted ? SATnot(right) : right; j = node; if(result == 1){ tmp = ALLOC(long,3); tmp[0] = left; tmp[1] = SATnot(j); size = 2; } else if(result == 2){ tmp = ALLOC(long,3); tmp[0] = right; tmp[1] = SATnot(j); size = 2; } else if(result == 3){ tmp = ALLOC(long,4); tmp[0] = SATnot(left); tmp[1] = SATnot(right); tmp[2] = j; size = 3; } else{ fprintf(vis_stderr,"wrong returned result value, exit\n"); exit(0); } lp = tmp; sat_BuildRT(cm,rm->root, lp, tmpIP,size,1); FREE(tmp); } } for(i=implied->num-1; i>=0; i--, space--) { v = *space; if(SATflags(v) & VisitedMask) { SATflags(v) &= ResetVisitedMask; --nMarked; if(nMarked == 0 && (!first || i==0)) { value = SATvalue(v); *fdaLit = v^(!value); sat_ArrayInsert(clauseArray, *fdaLit); break; } if(cm->option->coreGeneration){ ante = SATante(v); if(ante==0){ if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v),&ante))){ fprintf(vis_stderr,"ante = 0 and is not in anteTable %ld\n",v); exit(0); } } /*build non-leaf node*/ tmprt = RTCreateNode(rm); RT_pivot(tmprt) = SATnormalNode(v); RT_right(tmprt) = rm->root; rm->root = tmprt; if((SATflags(ante)&IsConflictMask)&&(SATflags(ante)&IsCNFMask)){ if(!st_lookup(cm->RTreeTable,(char*)ante,&tmprt)){ fprintf(vis_stderr,"RTree node of conflict cnf %ld is not in RTreeTable\n",ante); exit(0); } else{ RT_left(rm->root) = tmprt; } } else{ /* if not conflict CNF*/ /*left */ tmprt = RTCreateNode(rm); RT_left(rm->root) = tmprt; /*left is AIG*/ if(!(SATflags(ante) & IsCNFMask)){ /*generate formula for left*/ tmp = ALLOC(long,3); value = SATvalue(v); node = SATnormalNode(v); node = value==1?node:SATnot(node); tmp[0] = node; size = 1; if(ante != SATnormalNode(v)){ value = SATvalue(ante); node = SATnormalNode(ante); node = value==1?SATnot(node):node; tmp[1] = node; size++; ante2 = SATante2(v); if(ante2){ value = SATvalue(ante2); node = SATnormalNode(ante2); node = value==1?SATnot(node):node; tmp[2] = node; size++; } } /*generate p1 and p2*/ lp = tmp; sat_BuildRT(cm,tmprt,lp,tmpIP,size,1); FREE(tmp); } /* left is CNF*/ else{ RT_oriClsIdx(tmprt) = ante; //generate p1 and p2 for left lp = (long*)SATfirstLit(ante); size = SATnumLits(ante); RT_fSize(tmprt) = size; } } /*else{ if not conflict CNF*/ }/*if(cm->option->coreGeneration){*/ sat_MarkNodeInImpliedNode( cm, d, v, &nMarked, objectFlag, bLevel, clauseArray); /*Bing:Important for EffIP*/ first = 0; } /* first = 0;*/ } /* Minimize conflict clause */ if(option->minimizeConflictClause) sat_MinimizeConflictClause(cm, clauseArray); else sat_ResetFlagForClauseArray(cm, clauseArray); return; } /**Function******************************************************************** Synopsis [Conflict analysis procedure] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ int AS_ConflictAnalysis( satManager_t *cm, satLevel_t *d) { satStatistics_t *stats; satOption_t *option; satArray_t *clauseArray; int objectFlag; int bLevel; long fdaLit, learned, conflicting; int inverted; RTManager_t * rm = cm->rm; conflicting = d->conflict; if(d->level == 0) { /** Bing : UNSAT core generation */ if(cm->option->coreGeneration) sat_ConflictAnalysisForCoreGen(cm, d); cm->currentDecision--; return (-1); } stats = cm->each; option = cm->option; stats->nBacktracks++; clauseArray = cm->auxArray; bLevel = 0; fdaLit = -1; clauseArray->num = 0; /* Find Unique Implication Point */ AS_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit); stats->nNonchonologicalBacktracks += (d->level - bLevel); if(clauseArray->num == 0) { sat_PrintImplicationGraph(cm, d); sat_PrintNode(cm, conflicting); } /* If we could find UIP then it is critical error... * at lease the decision node has to be detected as UIP. */ if(fdaLit == -1) { fprintf(vis_stdout, "%s ERROR : Illegal unit literal\n", cm->comment); fflush(vis_stdout); sat_PrintNode(cm, conflicting); sat_PrintImplicationGraph(cm, d); sat_PrintDotForConflict(cm, d, conflicting, 0); exit(0); } if(bLevel && cm->lowestBacktrackLevel > bLevel) cm->lowestBacktrackLevel = bLevel; inverted = SATisInverted(fdaLit); fdaLit = SATnormalNode(fdaLit); if(option->verbose > 2) { if(option->verbose > 4) sat_PrintNode(cm, conflicting); fprintf(vis_stdout, "conflict at %3d on %6ld bLevel %d UnitLit ", d->level, conflicting, bLevel); sat_PrintNodeAlone(cm, fdaLit); fprintf(vis_stdout, "\n"); } d->conflict = 0; /* unit literal conflict clause */ if(clauseArray->num == 1) { learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag); stats->nUnitConflictCl++; cm->currentTopConflict = cm->literals->last-1; cm->currentTopConflictCount = 0; AS_Backtrack(cm, 0); d = SATgetDecision(cm->currentDecision); cm->implicatedSoFar -= d->implied->num; SATante(fdaLit) = 0; if(!(SATflags(SATnormalNode(fdaLit))&AssignedMask)){ satVariable_t *var = SATgetVariable(fdaLit); int dfs = var->scores[0]/SCOREUNIT; #if DBG assert(dfs==cm->LatchLevel); #endif SATflags(SATnormalNode(fdaLit))|=AssignedMask; cm->assignedArray[dfs]++; if(cm->assignedArray[dfs]==cm->numArray[dfs]) sat_ASmergeLevel(cm); } SATvalue(fdaLit) = inverted; SATmakeImplied(fdaLit, d); if((SATflags(fdaLit) & InQueueMask) == 0) { sat_Enqueue(cm->queue, fdaLit); SATflags(fdaLit) |= InQueueMask; } clauseArray->num = 0; if(option->incTraceObjective && objectFlag == 0) sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit)); if(option->incDistill && objectFlag) sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit)); if(objectFlag) SATflags(fdaLit) |= ObjMask; /* Bing: UNSAT core generation */ if(cm->option->coreGeneration){ st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned); st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root); RT_oriClsIdx(rm->root) = learned; } return(bLevel); } /* add conflict learned clause */ learned = sat_AddConflictClause(cm, clauseArray, objectFlag); cm->currentTopConflict = cm->literals->last-1; cm->currentTopConflictCount = 0; /* Bing: UNSAT core generation */ if(cm->option->coreGeneration){ st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root); RT_oriClsIdx(rm->root) = learned; } if(option->verbose > 2) { sat_PrintNode(cm, learned); fflush(vis_stdout); } /* apply Deepest Variable Hike decision heuristic */ if(option->decisionHeuristic & DVH_DECISION) sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit); /* Backtrack and failure driven assertion */ AS_Backtrack(cm, bLevel); d = SATgetDecision(bLevel); cm->implicatedSoFar -= d->implied->num; if(!(SATflags(SATnormalNode(fdaLit))&AssignedMask)){ satVariable_t *var = SATgetVariable(fdaLit); int dfs = var->scores[0]/SCOREUNIT; #if DBG assert(dfs==cm->LatchLevel); #endif SATflags(SATnormalNode(fdaLit))|=AssignedMask; cm->assignedArray[dfs]++; if(cm->assignedArray[dfs]==cm->numArray[dfs]) sat_ASmergeLevel(cm); } SATante(fdaLit) = learned; SATvalue(fdaLit) = inverted; SATmakeImplied(fdaLit, d); if((SATflags(fdaLit) & InQueueMask) == 0) { sat_Enqueue(cm->queue, fdaLit); SATflags(fdaLit) |= InQueueMask; } clauseArray->num = 0; if(objectFlag) SATflags(fdaLit) |= ObjMask; return(bLevel); } /**Function******************************************************************** Synopsis [Main solving procedure] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_Solve(satManager_t *cm) { satLevel_t *d; satOption_t *option; satVariable_t *var; int level; d = SATgetDecision(0); cm->implicatedSoFar = d->implied->num; cm->currentTopConflict = 0; option = cm->option; if(option->BDDMonolithic) { sat_TryToBuildMonolithicBDD(cm); } if(cm->status == SAT_UNSAT) { AS_Undo(cm, SATgetDecision(0)); return; } while(1) { AS_PeriodicFunctions(cm); if(cm->currentDecision == 0) sat_BuildLevelZeroHyperImplicationGraph(cm); d = AS_MakeDecision(cm); if(d == 0) { cm->status = SAT_SAT; return; } while(1) { AS_ImplicationMain(cm, d); if(d->conflict == 0) { if(cm->option->verbose > 2) { var = SATgetVariable(d->decisionNode); fprintf(vis_stdout, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied %.3f %%\n", d->level, d->decisionNode, SATvalue(d->decisionNode), var->scores[0], var->scores[1], cm->each->nDecisions, d->implied->num, (double)cm->implicatedSoFar/(double)cm->initNumVariables * 100); fflush(vis_stdout); } break; } if(cm->option->verbose > 2) { var = SATgetVariable(d->decisionNode); fprintf(vis_stdout, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied %.3f %% Conflict\n", d->level, d->decisionNode, SATvalue(d->decisionNode), var->scores[0], var->scores[1], cm->each->nDecisions, d->implied->num, (double)cm->implicatedSoFar/(double)cm->initNumVariables * 100); fflush(vis_stdout); } level = AS_ConflictAnalysis(cm, d); if(cm->currentDecision == -1) { if(cm->option->incDistill) { sat_BuildTrieForDistill(cm); } AS_Undo(cm, SATgetDecision(0)); cm->status = SAT_UNSAT; return; } d = SATgetDecision(cm->currentDecision); } } } /**Function******************************************************************** Synopsis [The main procedure of AROSAT solver] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AS_Main(satManager_t *cm) { long btime, etime; btime = util_cpu_time(); AS_PreProcessing(cm); if(cm->status == 0) AS_Solve(cm); /** Bing: UNSAT core generation **/ if(cm->option->coreGeneration && cm->status == SAT_UNSAT){ sat_GenerateCore_All(cm); } sat_PostProcessing(cm); etime = util_cpu_time(); cm->each->satTime = (double)(etime - btime) / 1000.0 ; } /**Function******************************************************************** Synopsis [Create one layer for AROSAT] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatCreateOneLayer(Ntk_Network_t *network, PureSat_Manager_t *pm, satManager_t *cm, array_t * latchArray, int layer) { mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); MvfAig_Function_t *mvfAig; bAigTimeFrame_t * tf = manager->timeframeWOI; mAigMvar_t lmVar; mAigBvar_t bVar; array_t *bVarList,*mVarList; int i,j,k,lmAigId,index,index1; char * name; Ntk_Node_t * latch; bAigEdge_t node,v, *li, *bli; st_table *table = st_init_table(st_numcmp,st_numhash); bVarList = mAigReadBinVarList(manager); mVarList = mAigReadMulVarList(manager); arrayForEachItem(char*,latchArray,i,name){ latch = Ntk_NetworkFindNodeByName(network,name); st_lookup(node2MvfAigTable,latch,&mvfAig); for(j=0;jnum;j++){ int retVal; v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j)); if(v==bAig_Zero||v==bAig_One) continue; retVal = st_lookup(tf->li2index,(char *)v,&index); assert(retVal); for(k=1;k<=pm->Length;k++){ li = tf->latchInputs[k]; if(li[index]==bAig_Zero||li[index]==bAig_One) continue; node = bAig_NonInvertedEdge(li[index]); st_insert(table,(char*)node,(char*)(long)layer); } } lmAigId = Ntk_NodeReadMAigId(latch); lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId); for(j=0,index1=lmVar.bVars;jbli2index,(char *)bVar.node,&index); assert(retVal); for(k=1;k<=pm->Length;k++){ bli = tf->blatchInputs[k]; if(bli[index]==bAig_Zero||bli[index]==bAig_One) continue; node = bAig_NonInvertedEdge(bli[index]); st_insert(table,(char*)node,(char*)(long)layer); } } } st_insert(cm->layerTable,table,(char*)(long)layer); } /**Function******************************************************************** Synopsis [Create all the layers] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatCreateLayer(Ntk_Network_t *network, PureSat_Manager_t *pm, satManager_t *cm, array_t *absModel, array_t *sufArray) { int layer; char* name; int i,j,threshold; array_t *tmpArray; if(sufArray->num<4) layer = 1; else if(sufArray->num<6) layer = 2; else if(sufArray->num<10) layer = 3; else if(sufArray->num<20) layer = 5; else if(sufArray->num<50) layer = 8; else layer = 10; threshold = sufArray->num/layer; layer = array_n(sufArray)/threshold; layer = sufArray->num%threshold?layer+1:layer; cm->LatchLevel = layer; cm->OriLevel = layer; cm->layerTable = st_init_table(st_ptrcmp,st_ptrhash); layer = layer+1; for(i=0;i=array_n(sufArray)) break; name = array_fetch(char*,sufArray,i+j); array_insert_last(char*,tmpArray,name); } PureSatCreateOneLayer(network,pm,cm,tmpArray,layer); array_free(tmpArray); } assert(layer==1); cm->assignedArray = ALLOC(int,cm->LatchLevel+1); cm->numArray = ALLOC(int,cm->LatchLevel+1); }