diff --git a/.gitignore b/.gitignore index f0c5201c6..cbb424152 100644 --- a/.gitignore +++ b/.gitignore @@ -8,12 +8,6 @@ ReleaseExt/ _/ _TEST/ -_sandwich/ -_scripts/ -*.aig -*.vcproj -*.sh -*.v lib/abc* lib/m114* lib/bip* diff --git a/Makefile b/Makefile index 9a9f7abd5..0cc979b75 100644 --- a/Makefile +++ b/Makefile @@ -33,8 +33,7 @@ MODULES := \ src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \ src/proof/cec src/proof/acec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \ src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \ - src/aig/miniaig \ - src/sat/bsat2 + src/aig/miniaig all: $(PROG) default: $(PROG) diff --git a/abc.rc b/abc.rc new file mode 100644 index 000000000..a3efc0b09 --- /dev/null +++ b/abc.rc @@ -0,0 +1,148 @@ +# global parameters +set check # checks intermediate networks +#set checkfio # prints warnings when fanins/fanouts are duplicated +#unset checkread # does not check new networks after reading from file +#set backup # saves backup networks retrived by "undo" and "recall" +#set savesteps 1 # sets the maximum number of backup networks to save +#set progressbar # display the progress bar + +# program names for internal calls +set dotwin dot.exe +set dotunix dot +set gsviewwin gsview32.exe +set gsviewunix gv +set siswin sis.exe +set sisunix sis +set mvsiswin mvsis.exe +set mvsisunix mvsis +set capowin MetaPl-Capo10.1-Win32.exe +set capounix MetaPl-Capo10.1 +set gnuplotwin wgnuplot.exe +set gnuplotunix gnuplot + +# Niklas Een's commands +#load_plugin C:\_projects\abc\lib\bip_win.exe "BIP" + +# standard aliases +alias hi history +alias b balance +alias cg clockgate +alias cl cleanup +alias clp collapse +alias cs care_set +alias el eliminate +alias esd ext_seq_dcs +alias f fraig +alias fs fraig_sweep +alias fsto fraig_store +alias fres fraig_restore +alias fr fretime +alias ft fraig_trust +alias ic indcut +alias lp lutpack +alias pcon print_cone +alias pd print_dsd +alias pex print_exdc -d +alias pf print_factor +alias pfan print_fanio +alias pg print_gates +alias pl print_level +alias plat print_latch +alias pio print_io +alias pk print_kmap +alias pm print_miter +alias ps print_stats +alias psb print_stats -b +alias psu print_supp +alias psy print_symm +alias pun print_unate +alias q quit +alias r read +alias ra read_aiger +alias r3 retime -M 3 +alias r3f retime -M 3 -f +alias r3b retime -M 3 -b +alias ren renode +alias rh read_hie +alias ri read_init +alias rl read_blif +alias rb read_bench +alias ret retime +alias dret dretime +alias rp read_pla +alias rt read_truth +alias rv read_verilog +alias rvl read_verlib +alias rsup read_super mcnc5_old.super +alias rlib read_library +alias rlibc read_library cadence.genlib +alias rty read_liberty +alias rlut read_lut +alias rw rewrite +alias rwz rewrite -z +alias rf refactor +alias rfz refactor -z +alias re restructure +alias rez restructure -z +alias rs resub +alias rsz resub -z +alias sa set autoexec ps +alias scl scleanup +alias sif if -s +alias so source -x +alias st strash +alias sw sweep +alias ssw ssweep +alias tr0 trace_start +alias tr1 trace_check +alias trt "r c.blif; st; tr0; b; tr1" +alias u undo +alias w write +alias wa write_aiger +alias wb write_bench +alias wc write_cnf +alias wh write_hie +alias wl write_blif +alias wp write_pla +alias wv write_verilog + +# standard scripts +alias resyn "b; rw; rwz; b; rwz; b" +alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" +alias resyn2a "b; rw; b; rw; rwz; b; rwz; b" +alias resyn3 "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b" +alias compress "b -l; rw -l; rwz -l; b -l; rwz -l; b -l" +alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore" +alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore" +alias rwsat "st; rw -l; b -l; rw -l; rf -l" +alias drwsat2 "st; drw; b -l; drw; drf; ifraig -C 20; drw; b -l; drw; drf" +alias share "st; multi -m; sop; fx; resyn2" +alias addinit "read_init; undc; strash; zero" +alias blif2aig "undc; strash; zero" +alias v2p "&vta_gla; &ps; &gla_derive; &put; w 1.aig; pdr -v" +alias g2p "&ps; &gla_derive; &put; w 2.aig; pdr -v" +alias &sw_ "&put; sweep; st; &get" +alias &fx_ "&put; sweep; sop; fx; st; &get" +alias &dc3 "&b; &jf -K 6; &b; &jf -K 4; &b" +alias &dc4 "&b; &jf -K 7; &fx; &b; &jf -K 5; &fx; &b" + +# resubstitution scripts for the IWLS paper +alias src_rw "st; rw -l; rwz -l; rwz -l" +alias src_rs "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" +alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" +alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" +alias r2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" +alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" +alias c2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" + +# use this script to convert 1-valued and DC-valued flops for an AIG +alias fix_aig "logic; undc; strash; zero" + +# use this script to convert 1-valued and DC-valued flops for a logic network coming from BLIF +alias fix_blif "undc; strash; zero" + +# lazy man's synthesis +alias recadd3 "st; rec_add3; b; rec_add3; dc2; rec_add3; if -K 8; bidec; st; rec_add3; dc2; rec_add3; if -g -K 6; st; rec_add3" + + diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e0654afda..f12ab35df 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1793,19 +1793,26 @@ extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs ) /*=== giaBound.c ===========================================================*/ typedef struct Bnd_Man_t_ Bnd_Man_t; -extern Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl ); +extern Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose ); extern void Bnd_ManStop(); + +// getter +extern int Bnd_ManGetNInternal(); +extern int Bnd_ManGetNExtra(); + //for fraig extern void Bnd_ManMap( int iLit, int id, int spec ); extern void Bnd_ManMerge( int id1, int id2, int phaseDiff ); extern void Bnd_ManFinalizeMappings(); extern void Bnd_ManPrintMappings(); // for eco -extern int Bnd_ManCheckBound( Gia_Man_t *p ); +extern int Bnd_ManCheckBound( Gia_Man_t *p, int fVerbose ); extern void Bnd_ManFindBound( Gia_Man_t *p ); extern Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t *p ); extern Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t *p ); extern Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch ); +extern Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec ); +extern Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkiptStrash, int fVerbose ); extern void Bnd_ManSetEqOut( int eq ); extern void Bnd_ManSetEqRes( int eq ); extern void Bnd_ManPrintStats(); diff --git a/src/aig/gia/giaBound.c b/src/aig/gia/giaBound.c index 916ed8e1f..a420b818d 100644 --- a/src/aig/gia/giaBound.c +++ b/src/aig/gia/giaBound.c @@ -29,6 +29,7 @@ struct Bnd_Man_t_ int nNode_patched; int status; // 0: init 1: boundary found 2: out generated 3: patched generated + int fVerbose; int combLoop_spec; int combLoop_impl; @@ -57,7 +58,7 @@ struct Bnd_Man_t_ }; -Bnd_Man_t* pBnd; +Bnd_Man_t* pBnd = 0; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -78,7 +79,7 @@ void Bnd_ManSetEqRes( int eq ) { pBnd -> eq_res = eq;} ***********************************************************************/ -Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl ) +Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose ) { int i; Bnd_Man_t* p = ABC_CALLOC( Bnd_Man_t, 1 ); @@ -113,6 +114,8 @@ Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl ) p -> nNode_patched = 0; p -> status = 0; + p -> fVerbose = fVerbose; + p -> combLoop_spec = 0; p -> combLoop_impl = 0; p -> eq_out = 0; @@ -166,6 +169,8 @@ void Bnd_ManStop() ABC_FREE( pBnd ); } +int Bnd_ManGetNInternal() { assert(pBnd); return pBnd -> nInternal; } +int Bnd_ManGetNExtra() { assert(pBnd); return pBnd -> nExtra; } void Bnd_ManMap( int iLit, int id, int spec ) { @@ -370,23 +375,22 @@ void Bnd_ManPrintStats() Description [check if the given boundary is valid. Return 0 if the boundary is invalid. Return k if the boundary is valid and - there're k boundary inputs. ] + there're k boundary inputs. + Can be called even if Bnd_Man_t is not created] SideEffects [] SeeAlso [] ***********************************************************************/ -int Bnd_ManCheckBound( Gia_Man_t * p ) +int Bnd_ManCheckBound( Gia_Man_t * p, int fVerbose ) { int i; Gia_Obj_t *pObj; int valid = 1; - pBnd -> nBI = 0; - pBnd -> nBO = 0; - pBnd -> nInternal = 0; + int nBI = 0, nBO = 0, nInternal = 0; - printf( "Checking boundary... \n"); + if ( fVerbose ) printf( "Checking boundary... \n"); Vec_Int_t *vPath; vPath = Vec_IntAlloc( Gia_ManObjNum(p) ); @@ -417,7 +421,7 @@ int Bnd_ManCheckBound( Gia_Man_t * p ) if ( path == 1 ) // boundary input { // TODO: record BIs here since they may not be in the first n buffers - pBnd -> nBO ++; + nBO ++; } } else if ( Gia_ObjFaninNum( p, pObj ) >= 1 ) @@ -431,7 +435,7 @@ int Bnd_ManCheckBound( Gia_Man_t * p ) if ( path == 2 ) // inside boundary { // TODO: record BIs here since they may not be in the first n buffers - pBnd -> nInternal ++; + nInternal ++; } } else // PI or const, check validity @@ -445,20 +449,33 @@ int Bnd_ManCheckBound( Gia_Man_t * p ) } } - pBnd -> nBI = Gia_ManBufNum(p) - pBnd -> nBO; + nBI = Gia_ManBufNum(p) - nBO; if ( !valid ) { printf("invalid boundary\n"); return 0; } + else if ( nBI == 0 ) + { + printf("no boundary\n"); + return 0; + } else { - printf("valid boundary ("); - printf("#BI = %d\t#BO = %d\t", pBnd -> nBI, Gia_ManBufNum(p)- pBnd -> nBI); - printf("#Internal = %d)\n", pBnd -> nInternal ); - assert( pBnd -> nBI > 0 ); - return pBnd -> nBI; + if ( fVerbose ) + { + printf("valid boundary ("); + printf("#BI = %d\t#BO = %d\t", nBI, Gia_ManBufNum(p)- nBI); + printf("#Internal = %d)\n", nInternal ); + } + if ( pBnd ) + { + pBnd -> nBI = nBI; + pBnd -> nBO = nBO; + pBnd -> nInternal = nInternal; + } + return nBI; } } @@ -572,7 +589,7 @@ void Bnd_ManFindBound( Gia_Man_t * p ) { if ( cnt < pBnd -> nBI ) { - Vec_IntPush( vBI, Gia_ObjId(p, pObj) ); + Vec_IntPush( vBI, Gia_ObjId(p, Gia_ObjFanin0(pObj) ) ); } else { @@ -593,7 +610,7 @@ void Bnd_ManFindBound( Gia_Man_t * p ) Vec_IntPush(vEO_spec, id); } } - printf("%d BO doesn't match. ", Vec_PtrSize(vQ) ); + if ( pBnd -> fVerbose ) printf("%d BO doesn't match. ", Vec_PtrSize(vQ) ); pBnd -> nBO_miss = Vec_PtrSize(vQ); int cnt_extra = - Vec_PtrSize(vQ); @@ -622,7 +639,7 @@ void Bnd_ManFindBound( Gia_Man_t * p ) } } // printf("%d AO found with %d extra nodes\n", Vec_IntSize(vAO) , cnt_extra ); - printf("%d AO found\n", Vec_IntSize(vAO) ); + if ( pBnd -> fVerbose ) printf("%d AO found\n", Vec_IntSize(vAO) ); // mark TFOC of BO with flag 1 to prevent them from being selected into EI @@ -665,7 +682,7 @@ void Bnd_ManFindBound( Gia_Man_t * p ) Vec_IntPush(vEI_spec, id); } } - printf("%d BI doesn't match. ", Vec_PtrSize(vQ) ); + if ( pBnd -> fVerbose ) printf("%d BI doesn't match. ", Vec_PtrSize(vQ) ); pBnd -> nBI_miss = Vec_PtrSize(vQ); cnt_extra -= Vec_PtrSize(vQ); @@ -708,7 +725,7 @@ void Bnd_ManFindBound( Gia_Man_t * p ) Vec_IntSetEntry( vFlag, id, 2 ); } - printf("%d AI found with %d extra nodes in total\n", Vec_IntSize(vAI) , cnt_extra ); + if ( pBnd -> fVerbose ) printf("%d AI found with %d extra nodes in total\n", Vec_IntSize(vAI) , cnt_extra ); pBnd -> nExtra = cnt_extra; @@ -738,8 +755,11 @@ void Bnd_ManFindBound( Gia_Man_t * p ) // print pBnd -> status = 1; - printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra ); - Bnd_ManPrintBound(); + if ( pBnd -> fVerbose ) + { + printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra ); + Bnd_ManPrintBound(); + } // check boundary has comb loop if ( !Bnd_ManCheckExtBound( p, vEI_spec, vEO_spec ) ) @@ -869,42 +889,47 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec } -Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p ) +Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p ) { - printf("Generating spec_out with given boundary.\n"); + if ( pBnd -> fVerbose ) printf("Generating spec_out with given boundary.\n"); Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_spec, pBnd->vEO_spec, 0, 0 ); return pNew; } -Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p ) +Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p) { - printf("Generating impl_out with given boundary.\n"); + if ( pBnd -> fVerbose ) printf("Generating impl_out with given boundary.\n"); Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_impl, pBnd->vEO_impl, pBnd->vEI_phase, pBnd->vEO_phase ); if ( pNew ) pBnd -> status = 2; else pBnd -> combLoop_impl = 1; return pNew; } -void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj ) +void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj, int fSkipStrash ) { // TODO does this mean constant zero node? if ( pObj -> Value != ~0 ) return; for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ ) { - Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i) ); + Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i), fSkipStrash ); } if ( Gia_ObjIsAnd(pObj) ) { - pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( fSkipStrash ) + { + if ( Gia_ObjIsBuf(pObj) ) pObj -> Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + else pObj -> Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + else + { + pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } } else { - if ( Gia_ObjIsCi(pObj) ) - { - printf("Ci with value 0 encountered (id = %d)\n", Gia_ObjId(p, pObj) ); - } assert( Gia_ObjIsCo(pObj) ); + // if ( Gia_ObjIsCi(pObj) ) printf("Ci with value ~0 encountered (id = %d)\n", Gia_ObjId(p, pObj) ); pObj -> Value = Gia_ObjFanin0Copy(pObj); } } @@ -963,7 +988,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ ) { pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) ); - Bnd_AddNodeRec( pOut, pNew, pObj ); + Bnd_AddNodeRec( pOut, pNew, pObj, 0 ); // set Spec EI Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value; @@ -976,7 +1001,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat Vec_IntForEachEntry( pBnd -> vBI, id, i ) { pObj = Gia_ManObj( pSpec, id ); - Bnd_AddNodeRec( pSpec, pNew, pObj ); + Bnd_AddNodeRec( pSpec, pNew, pObj, 0 ); // set patch bi Gia_ManObj( pPatch, Vec_IntEntry( vBI_patch, i) ) -> Value = pObj -> Value; @@ -989,7 +1014,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat Vec_IntForEachEntry( vBO_patch, id, i ) { pObj = Gia_ManObj( pPatch, id ); - Bnd_AddNodeRec( pPatch, pNew, pObj ); + Bnd_AddNodeRec( pPatch, pNew, pObj, 0 ); // set spec bo Gia_ManObj( pSpec, Vec_IntEntry( pBnd -> vBO, i) ) -> Value = pObj -> Value; @@ -1002,7 +1027,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat Vec_IntForEachEntry( pBnd -> vEO_spec, id, i ) { pObj = Gia_ManObj( pSpec, id ); - Bnd_AddNodeRec( pSpec, pNew, pObj ); + Bnd_AddNodeRec( pSpec, pNew, pObj, 0 ); // set impl EO (PI) Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value; @@ -1015,7 +1040,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat for ( i = 0; i < Gia_ManCoNum(pSpec); i++ ) { pObj = Gia_ManCo( pOut, i ); - Bnd_AddNodeRec( pOut, pNew, pObj ); + Bnd_AddNodeRec( pOut, pNew, pObj, 0 ); Gia_ManAppendCo( pNew, pObj->Value ); // printf(" %d",pObj -> Value); } @@ -1036,8 +1061,186 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat return pNew; } +Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec ) +{ + + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, id; + + pNew = Gia_ManStart( Gia_ManObjNum(pOut) + Gia_ManObjNum( pSpec ) ); + pNew -> pName = ABC_ALLOC( char, strlen(pOut->pName)+3); + sprintf( pNew -> pName, "%s_p", pOut -> pName ); + + Gia_ManFillValue(pOut); + Gia_ManFillValue(pSpec); + Gia_ManConst0(pOut)->Value = 0; + Gia_ManConst0(pSpec)->Value = 0; + // add Impl (real) PI + for ( i = 0; i < Gia_ManCiNum(pSpec); i++ ) + { + pObj = Gia_ManCi(pOut, i); + pObj -> Value = Gia_ManAppendCi( pNew ); + } + + // add Impl EI to CI + // printf("adding EI to CI in Impl\n"); + for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ ) + { + pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) ); + Bnd_AddNodeRec( pOut, pNew, pObj, 1 ); + + // set Spec EI + Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + // add Spec EO to EI + // add BI -> BO -> EO to maintain the order of bufs + // Vec_IntForEachEntry( pBnd -> vBI, id, i ) + // { + // pObj = Gia_ManObj( pSpec, id ); + // Bnd_AddNodeRec( pSpec, pNew, pObj, 1 ); + // } + // Vec_IntForEachEntry( pBnd -> vBO, id, i ) + // { + // pObj = Gia_ManObj( pSpec, id ); + // Bnd_AddNodeRec( pSpec, pNew, pObj, 1 ); + // } + Gia_ManForEachBuf( pSpec, pObj, i ) + { + Bnd_AddNodeRec( pSpec, pNew, pObj, 1 ); + } + Vec_IntForEachEntry( pBnd -> vEO_spec, id, i ) + { + pObj = Gia_ManObj( pSpec, id ); + Bnd_AddNodeRec( pSpec, pNew, pObj, 1 ); + + // set impl EO (PI) + Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + // add Impl (real) PO to EO + // printf("adding CO to EO in Impl\n"); + for ( i = 0; i < Gia_ManCoNum(pSpec); i++ ) + { + pObj = Gia_ManCo( pOut, i ); + Bnd_AddNodeRec( pOut, pNew, pObj, 1 ); + Gia_ManAppendCo( pNew, pObj->Value ); + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + + // clean up + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + pBnd -> nNode_patched = Gia_ManAndNum( pNew ); + pBnd -> status = 3; + + return pNew; +} + +Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkipStrash, int fVerbose ) +{ + + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, nBI, nBI_patch, cnt; + Vec_Int_t* vLit; + + + // check boundary first + nBI = Bnd_ManCheckBound( pImpl, fVerbose ); + nBI_patch = Bnd_ManCheckBound( pPatch, fVerbose ); + if ( 0 == nBI_patch || Gia_ManBufNum(pImpl) != Gia_ManBufNum(pPatch) || nBI != nBI_patch ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" ); + return 0; + } + + // prepare new network + pNew = Gia_ManStart( Gia_ManObjNum(pImpl) + Gia_ManObjNum( pPatch ) ); + pNew -> pName = ABC_ALLOC( char, strlen(pImpl->pName)+3); + sprintf( pNew -> pName, "%s_p", pImpl -> pName ); + if ( !fSkipStrash ) + { + Gia_ManHashAlloc( pNew ); + } + Gia_ManFillValue(pImpl); + Gia_ManFillValue(pPatch); + Gia_ManConst0(pImpl)->Value = 0; + Gia_ManConst0(pPatch)->Value = 0; + + vLit = Vec_IntAlloc( Gia_ManBufNum(pImpl) ); + + // add Impl (real) CI + Gia_ManForEachCi( pImpl, pObj, i ) + { + pObj -> Value = Gia_ManAppendCi( pNew ); + } + + // add Impl BI to CI + cnt = 0; + Gia_ManForEachBuf( pImpl, pObj, i ) + { + Bnd_AddNodeRec( pImpl, pNew, pObj, fSkipStrash ); + Vec_IntPush( vLit, pObj -> Value ); + cnt ++; + if ( cnt >= nBI ) break; + } + + // set BI in patch + // add patch BO to BI + cnt = 0; + Gia_ManForEachBuf( pPatch, pObj, i ) + { + if ( cnt < nBI ) + { + pObj -> Value = Vec_IntEntry( vLit, cnt ); + } + else + { + Bnd_AddNodeRec( pPatch, pNew, pObj, fSkipStrash ); + Vec_IntPush( vLit, pObj -> Value ); + } + cnt ++; + if ( cnt == nBI ) Vec_IntClear( vLit ); + } + + // set BO in impl + cnt = 0; + Gia_ManForEachBuf( pImpl, pObj, i ) + { + cnt ++; + if ( cnt <= nBI) continue; + pObj -> Value = Vec_IntEntry( vLit, cnt-nBI-1 ); + } + + // add impl CO to BO + Gia_ManForEachCo( pImpl, pObj, i ) + { + Bnd_AddNodeRec( pImpl, pNew, pObj, fSkipStrash ); + Gia_ManAppendCo( pNew, pObj -> Value ); + } + + // clean up + if ( !fSkipStrash ) + { + Gia_ManHashStop( pNew ); + } + Vec_IntFree( vLit ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + return pNew; +} //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9a558c2da..d6363a0cc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -599,6 +599,7 @@ static int Abc_CommandAbc9ProdAdd ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9BMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9BRecover ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1381,6 +1382,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&addflop", Abc_CommandAbc9AddFlop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&brecover", Abc_CommandAbc9BRecover, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); @@ -52092,12 +52094,12 @@ usage: ***********************************************************************/ extern Bnd_Man_t* pBnd; -int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); extern void Cec4_ManSetParams( Cec_ParFra_t * pPars ); extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ); - Gia_Man_t *pImpl, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatch, *pPatched, *pTemp, *pBmiter;; + Gia_Man_t *pSpec, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatched = 0, *pTemp, *pBmiter; char * FileName = NULL; FILE * pFile = NULL; int c, fVerbose = 0, success = 1; @@ -52111,8 +52113,6 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) Cec4_ManSetParams( pParsFra ); pParsFra -> fBMiterInfo = 1; - // TODO: save return value and return at the end of the function - // parse options Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) @@ -52130,17 +52130,17 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9BRecover(): There is no AIG.\n" ); return 0; } - if ( argc != globalUtilOptind + 2 ) + if ( argc != globalUtilOptind + 1 ) { printf("%d\n", argc-globalUtilOptind); - Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" ); + Abc_Print( -1, "Abc_CommandAbc9BRecover(): AIG should be given on the command line.\n" ); return 0; } - // read impl + // read spec FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { @@ -52151,15 +52151,198 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } fclose( pFile ); - pImpl = Gia_AigerRead( FileName, 0, 0, 0 ); - if ( pImpl == NULL ) + pSpec = Gia_AigerRead( FileName, 0, 1, 0 ); + if ( pSpec == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" ); + Abc_Print( -1, "Abc_CommandAbc9BRecover(): Cannot read the file name on the command line.\n" ); + return 0; + } + if ( Gia_ManBufNum(pSpec) == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec should be hierarchical.\n" ); + Gia_ManStop(pSpec); return 0; } + // start boundary manager + pBnd = Bnd_ManStart( pSpec, pAbc->pGia, fVerbose ); + + // verify if spec eq impl + pMiter = Gia_ManMiter( pAbc->pGia, pSpec, 0, 1, 0, 0, 0 ); + if ( !Cec_ManVerify( pMiter, pParsCec ) ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec is not equivalent to current impl.\n" ); + success = 0; + } + Gia_ManStop(pMiter); + + // check boundary + if ( success ) + { + if ( 0 == Bnd_ManCheckBound( pSpec, fVerbose ) ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec has invalid boundary.\n" ); + success = 0; + } + } + + if ( success ) + { + // create bmiter, run fraig, record mapping + pBmiter = Gia_ManBoundaryMiter( pSpec, pAbc->pGia, 0 ); + pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra ); + Gia_ManStop(pBmiter); + Gia_ManStop(pTemp); + + // find + Bnd_ManFindBound( pSpec ); + + // create spec_out and + pSpec_out = Bnd_ManGenSpecOut( pSpec ); + if ( !pSpec_out ) success = 0; + pImpl_out = Bnd_ManGenImplOut( pAbc->pGia ); + if ( !pImpl_out ) success = 0; + + // Gia_AigerWrite( pSpec_out, "spec_out.aig", 0, 0, 0 ); + // Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 ); + // Gia_ManPrintStats( pSpec_out, pPars ); + // Gia_ManPrintStats( pImpl_out, pPars ); + } + + if ( !success ) + { + printf("Abc_CommandAbc9BRecover(): The generated boundary is invalid. The circuit is not changed.\n"); + } + else + { + + // check if spec_out and imnpl_out are equivalent + if ( fVerbose ) + { + printf("Checking the equivalence of spec_out and impl_out\n"); + pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 ); + Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) ); + Gia_ManStop( pMiter ); + } + + // generate patched impl + if ( fVerbose ) printf("Generating patched impl\n"); + pPatched = Bnd_ManGenPatched1( pImpl_out, pSpec ); + + // // generate patched spec just for debugging + // printf("Generating patched spec\n"); + // pTemp = Bnd_ManGenPatched( pSpec_out, pAbc->pGia, pPatch ); + // printf("Checking the equivalence of patched spec and patched impl\n"); + // pMiter = Gia_ManMiter( pTemp, pPatched, 0, 1, 0, 0, 0 ); + // Cec_ManVerify( pMiter, pParsCec ); + // Gia_ManStop( pMiter ); + // printf("Checking the equivalence of patched spec and patch\n"); + // pMiter = Gia_ManMiter( pTemp, pPatch, 0, 1, 0, 0, 0 ); + // Cec_ManVerify( pMiter, pParsCec ); + // Gia_ManStop( pMiter ); + + // Gia_ManStop( pTemp ); + + // check if patched is equiv to spec + if ( fVerbose ) printf("Checking the equivalence of patched impl and spec\n"); + pMiter = Gia_ManMiter( pSpec, pPatched, 0, 1, 0, 0, 0 ); + success = Cec_ManVerify( pMiter, pParsCec ); + Bnd_ManSetEqRes( success ); + if ( !success ) + { + printf("Failed. The generated AIG is not equivalent.\n"); + } + Gia_ManStop( pMiter ); + + } + + if ( fVerbose ) Bnd_ManPrintStats(); + + Gia_ManStop( pSpec ); + if ( pSpec_out ) Gia_ManStop( pSpec_out ); + if ( pImpl_out ) Gia_ManStop( pImpl_out ); + if ( success ) + { + printf("Success. The generated hierarchical impl is equivalent. (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() ); + } + if (pPatched) Abc_FrameUpdateGia( pAbc, pPatched ); + Bnd_ManStop(); + + return 0; + +usage: + Abc_Print( -2, "usage: &brecover -I [-vh] \n" ); + Abc_Print( -2, "\t recover boundary using SAT-Sweeping\n" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : the implementation aig. (should be equivalent to spec)\n"); + Abc_Print( -2, "\t : the modified spec. (should be a hierarchical AIG)\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); + extern void Cec4_ManSetParams( Cec_ParFra_t * pPars ); + Gia_Man_t *pMiter, *pPatch, *pPatched; + char * FileName = NULL; + FILE * pFile = NULL; + int c, success = 1; + int fVerbose = 0, fSkipStrash = 0; + + // params + Gps_Par_t Pars, * pPars = &Pars; + memset( pPars, 0, sizeof(Gps_Par_t) ); + Cec_ParCec_t ParsCec, *pParsCec = &ParsCec; + Cec_ManCecSetDefaultParams( pParsCec ); + Cec_ParFra_t ParsFra, *pParsFra = &ParsFra; + Cec4_ManSetParams( pParsFra ); + pParsFra -> fBMiterInfo = 1; + + // parse options + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vsh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 's': + fSkipStrash ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 1 ) + { + printf("%d\n", argc-globalUtilOptind); + Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" ); + return 0; + } + // read patch - FileName = argv[globalUtilOptind+1]; + FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); @@ -52176,98 +52359,29 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } - // start boundary manager - pBnd = Bnd_ManStart( pAbc->pGia, pImpl ); + // generate patched impl + if ( fVerbose ) printf("Generating patched impl\n"); + pPatched = Bnd_ManGenPatched2( pAbc->pGia, pPatch, fSkipStrash, fVerbose ); - // verify if spec eq impl - pMiter = Gia_ManMiter( pAbc->pGia, pImpl, 0, 1, 0, 0, 0 ); - if ( !Cec_ManVerify( pMiter, pParsCec ) ) + if ( pPatched ) { - Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given impl is not equivalent to spec.\n" ); - success = 0; - } - Gia_ManStop(pMiter); - - // check boundary - if ( success ) - { - if ( 0 == Bnd_ManCheckBound( pPatch ) || 0 == Bnd_ManCheckBound( pAbc -> pGia ) ) - { - Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" ); - success = 0; - } - } - - if ( success ) - { - // create bmiter, run fraig - pBmiter = Gia_ManBoundaryMiter( pAbc -> pGia, pImpl, 0 ); - pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra ); - Gia_ManStop(pBmiter); - Gia_ManStop(pTemp); - - // find - Bnd_ManFindBound( pAbc -> pGia ); - - // create spec_out and - pSpec_out = Bnd_ManGenSpecOut( pAbc -> pGia ); - if ( !pSpec_out ) success = 0; - pImpl_out = Bnd_ManGenImplOut( pImpl ); - if ( !pImpl_out ) success = 0; - - // Gia_AigerWrite( pSpec_out, "spec_out.aig", 0, 0, 0 ); - // Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 ); - // Gia_ManPrintStats( pSpec_out, pPars ); - // Gia_ManPrintStats( pImpl_out, pPars ); - - } - - if ( success ) - { - - // check if spec_out and imnpl_out are equivalent - printf("Checking the equivalence of spec_out and impl_out\n"); - pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 ); - Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) ); - Gia_ManStop( pMiter ); - - // generate patched impl - printf("Generating patched impl\n"); - pPatched = Bnd_ManGenPatched( pImpl_out, pAbc->pGia, pPatch ); - - // generate patched spec just for debugging - printf("Generating patched spec\n"); - pTemp = Bnd_ManGenPatched( pSpec_out, pAbc->pGia, pPatch ); - printf("Checking the equivalence of patched spec and patched impl\n"); - pMiter = Gia_ManMiter( pTemp, pPatched, 0, 1, 0, 0, 0 ); - Cec_ManVerify( pMiter, pParsCec ); - Gia_ManStop( pMiter ); - printf("Checking the equivalence of patched spec and patch\n"); - pMiter = Gia_ManMiter( pTemp, pPatch, 0, 1, 0, 0, 0 ); - Cec_ManVerify( pMiter, pParsCec ); - Gia_ManStop( pMiter ); - - Gia_ManStop( pTemp ); - // check if patched is equiv to patch - printf("Checking the equivalence of patched impl and patch\n"); + if ( fVerbose ) printf("Checking the equivalence of patched impl and patch\n"); pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 ); - Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) ); + success = Cec_ManVerify( pMiter, pParsCec ); + if( !success ) + { + printf("Failed. The patched circuit is not equivalent.\n"); + } Gia_ManStop( pMiter ); - - } - - Bnd_ManPrintStats(); - - Gia_ManStop( pImpl ); - Gia_ManStop( pPatch ); - if ( pSpec_out ) Gia_ManStop( pSpec_out ); - if ( pImpl_out ) Gia_ManStop( pImpl_out ); - if ( success ) - { Abc_FrameUpdateGia( pAbc, pPatched ); } - Bnd_ManStop(); + + Gia_ManStop( pPatch ); + if ( success ) + { + printf("Success. The patched circuit is equivalent.\n"); + } return 0; @@ -52275,6 +52389,7 @@ usage: Abc_Print( -2, "usage: &str_eco -I [-vh] \n" ); Abc_Print( -2, "\t SAT-sweeping-based ECO\n" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-s : toggles skipping structural hash [default = %s]\n", fSkipStrash? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : the implementation aig. (should be equivalent to spec)\n"); Abc_Print( -2, "\t : the modified spec. (should be a hierarchical AIG)\n"); diff --git a/src/sat/bsat2/Options.cpp b/src/sat/bsat2/Options.cpp index f14059f67..a0a3817d8 100644 --- a/src/sat/bsat2/Options.cpp +++ b/src/sat/bsat2/Options.cpp @@ -45,10 +45,12 @@ int Minisat::parseOptions(int& argc, char** argv, bool strict) } if (!parsed_ok) + { if (strict && match(argv[i], "-")) { fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()); return 0; } // exit(0); else argv[j++] = argv[i]; + } } } diff --git a/src/sat/bsat2/Options.h b/src/sat/bsat2/Options.h index 137b5a45e..00d46d352 100644 --- a/src/sat/bsat2/Options.h +++ b/src/sat/bsat2/Options.h @@ -62,7 +62,7 @@ class Option struct OptionLt { bool operator()(const Option* x, const Option* y) { int test1 = strcmp(x->category, y->category); - return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0; + return test1 < 0 || ( test1 == 0 && strcmp(x->type_name, y->type_name) < 0 ); } }; diff --git a/src/sat/bsat2/SimpSolver.cpp b/src/sat/bsat2/SimpSolver.cpp index 59952d154..c07ec5b97 100644 --- a/src/sat/bsat2/SimpSolver.cpp +++ b/src/sat/bsat2/SimpSolver.cpp @@ -230,10 +230,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& ou if (var(qs[i]) != v){ for (j = 0; j < ps.size(); j++) if (var(ps[j]) == var(qs[i])) + { if (ps[j] == ~qs[i]) return false; else goto next; + } out_clause.push(qs[i]); } next:; @@ -264,10 +266,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size) if (var(__qs[i]) != v){ for (int j = 0; j < ps.size(); j++) if (var(__ps[j]) == var(__qs[i])) + { if (__ps[j] == ~__qs[i]) return false; else goto next; + } size++; } next:; diff --git a/src/sat/bsat2/Solver.cpp b/src/sat/bsat2/Solver.cpp index 1c45a4538..602692a8b 100644 --- a/src/sat/bsat2/Solver.cpp +++ b/src/sat/bsat2/Solver.cpp @@ -211,7 +211,7 @@ void Solver::cancelUntil(int level) { for (int c = trail.size()-1; c >= trail_lim[level]; c--){ Var x = var(trail[c]); assigns [x] = l_Undef; - if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) + if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last())) polarity[x] = sign(trail[c]); insertVarOrder(x); } qhead = trail_lim[level]; @@ -659,7 +659,7 @@ lbool Solver::search(int nof_conflicts) }else{ // NO CONFLICT - if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ + if ( (nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){ // Reached bound on number of conflicts: progress_estimate = progressEstimate(); cancelUntil(0); diff --git a/src/sat/bsat2/Vec.h b/src/sat/bsat2/Vec.h index aade19f13..f5f5499ea 100644 --- a/src/sat/bsat2/Vec.h +++ b/src/sat/bsat2/Vec.h @@ -93,7 +93,6 @@ public: void moveTo(vec& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } }; - template void vec::capacity(int min_cap) { if (cap >= min_cap) return;