From 48498af8189ef321ee876065d8947875cf711294 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 29 Dec 2021 13:08:32 -0800 Subject: Missing class name in the FreeBSD code. --- src/sat/glucose/System.cpp | 2 +- src/sat/glucose2/System2.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'src/sat') diff --git a/src/sat/glucose/System.cpp b/src/sat/glucose/System.cpp index 18f2d656..276eddb8 100644 --- a/src/sat/glucose/System.cpp +++ b/src/sat/glucose/System.cpp @@ -86,7 +86,7 @@ double Gluco::memUsed(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_maxrss / 1024; } -double memUsedPeak(void) { return memUsed(); } +double Gluco::memUsedPeak(void) { return memUsed(); } ABC_NAMESPACE_IMPL_END diff --git a/src/sat/glucose2/System2.cpp b/src/sat/glucose2/System2.cpp index 844220a0..bf16dcd1 100644 --- a/src/sat/glucose2/System2.cpp +++ b/src/sat/glucose2/System2.cpp @@ -86,7 +86,7 @@ double Gluco2::memUsed(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_maxrss / 1024; } -double memUsedPeak(void) { return memUsed(); } +double Gluco2::memUsedPeak(void) { return memUsed(); } ABC_NAMESPACE_IMPL_END -- cgit v1.2.3 From 554a1693ac2bd81169b28227ea718527136f5e7e Mon Sep 17 00:00:00 2001 From: Baruch Sterin Date: Fri, 21 Jan 2022 22:51:36 +0200 Subject: Move CI to GitHub Actions. Also, a few minor changes that are required to compile ABC under moder compilers. --- src/sat/msat/msatClause.c | 2 +- src/sat/msat/msatSolverSearch.c | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'src/sat') diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c index 6b1b9e98..3d1fa2fc 100644 --- a/src/sat/msat/msatClause.c +++ b/src/sat/msat/msatClause.c @@ -522,7 +522,7 @@ void Msat_ClausePrintSymbols( Msat_Clause_t * pC ) // if ( pC->fLearned ) // printf( "Act = %.4f ", Msat_ClauseReadActivity(pC) ); for ( i = 0; i < (int)pC->nSize; i++ ) - printf(" "L_LIT, L_lit(pC->pData[i])); + printf(" " L_LIT, L_lit(pC->pData[i])); } printf( "\n" ); } diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c index b3190e39..2eda5038 100644 --- a/src/sat/msat/msatSolverSearch.c +++ b/src/sat/msat/msatSolverSearch.c @@ -52,7 +52,7 @@ int Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ) { assert( Msat_QueueReadSize(p->pQueue) == 0 ); if ( p->fVerbose ) - printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(Lit)); + printf(L_IND "assume(" L_LIT ")\n", L_ind, L_lit(Lit)); Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) ); // assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 ); // assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars ); @@ -83,7 +83,7 @@ void Msat_SolverUndoOne( Msat_Solver_t * p ) Msat_OrderVarUnassigned( p->pOrder, Var ); if ( p->fVerbose ) - printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(Lit)); + printf(L_IND "unbind(" L_LIT")\n", L_ind, L_lit(Lit)); } /**Function************************************************************* @@ -107,7 +107,7 @@ void Msat_SolverCancel( Msat_Solver_t * p ) { Msat_Lit_t Lit; Lit = Msat_IntVecReadEntry( p->vTrail, Msat_IntVecReadEntryLast(p->vTrailLim) ); - printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(Lit)); + printf(L_IND "cancel(" L_LIT ")\n", L_ind, L_lit(Lit)); } } for ( c = Msat_IntVecReadSize(p->vTrail) - Msat_IntVecPop( p->vTrailLim ); c != 0; c-- ) @@ -188,7 +188,7 @@ int Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ) if ( p->fVerbose ) { // printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit)); - printf(L_IND"bind("L_LIT") ", L_ind, L_lit(Lit)); + printf(L_IND "bind(" L_LIT ") ", L_ind, L_lit(Lit)); Msat_ClausePrintSymbols( pC ); } p->pAssigns[Var] = Lit; @@ -513,7 +513,7 @@ void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * nReasonSize = Msat_IntVecReadSize( vLits_out ); pReasonArray = Msat_IntVecReadArray( vLits_out ); for ( j = 0; j < nReasonSize; j++ ) - printf(" "L_LIT, L_lit(pReasonArray[j])); + printf(" " L_LIT, L_lit(pReasonArray[j])); printf(" } at level %d\n", *pLevel_out); } } -- cgit v1.2.3 From 6097ac1d1aa67732a98caab517a510731fb2f0b1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 2 Feb 2022 17:21:30 -0800 Subject: Adding option to dump CNF after preprocessing in &glucose. --- src/sat/bsat2/Solver.cpp | 2 +- src/sat/glucose/AbcGlucose.cpp | 11 ++++++++++- src/sat/glucose/AbcGlucose.h | 2 +- src/sat/glucose/AbcGlucoseCmd.cpp | 11 ++++++++--- src/sat/glucose/Glucose.cpp | 2 +- src/sat/glucose2/Glucose2.cpp | 2 +- 6 files changed, 22 insertions(+), 8 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bsat2/Solver.cpp b/src/sat/bsat2/Solver.cpp index 451beed8..0f8b415a 100644 --- a/src/sat/bsat2/Solver.cpp +++ b/src/sat/bsat2/Solver.cpp @@ -820,7 +820,7 @@ void Solver::toDimacs(FILE* f, Clause& c, vec& map, Var& max) void Solver::toDimacs(const char *file, const vec& assumps) { - FILE* f = fopen(file, "wr"); + FILE* f = fopen(file, "wb"); if (f == NULL) fprintf(stderr, "could not open file %s\n", file), exit(1); toDimacs(f, assumps); diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index ad595ab9..9c23e0d0 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -818,7 +818,7 @@ void Glucose_ReadDimacs( char * pFileName, SimpSolver& s ) SeeAlso [] ***********************************************************************/ -void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars ) +void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars, int fDumpCnf ) { abctime clk = Abc_Clock(); @@ -844,6 +844,15 @@ void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars ) S.eliminate(true); printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + if ( fDumpCnf ) + { + char * pFileCnf = Extra_FileNameGenericAppend( pFileName, "_out.cnf" ); + S.toDimacs(pFileCnf); + printf( "Finished dumping CNF after preprocessing into file \"%s\".\n", pFileCnf ); + printf( "SAT solving is not performed.\n" ); + return; + } } vec dummy; diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h index 89a3652f..c73f9918 100644 --- a/src/sat/glucose/AbcGlucose.h +++ b/src/sat/glucose/AbcGlucose.h @@ -105,7 +105,7 @@ extern void bmcg_sat_solver_start_new_round( bmcg_sat_solver * s ); extern void bmcg_sat_solver_mark_cone( bmcg_sat_solver * s, int var ); -extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars ); +extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars, int fDumpCnf ); extern int Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars ); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/glucose/AbcGlucoseCmd.cpp b/src/sat/glucose/AbcGlucoseCmd.cpp index 2e819e49..bb957547 100644 --- a/src/sat/glucose/AbcGlucoseCmd.cpp +++ b/src/sat/glucose/AbcGlucoseCmd.cpp @@ -81,10 +81,11 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv ) int pre = 1; int verb = 0; int nConfls = 0; + int fDumpCnf = 0; Glucose_Pars pPars; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Cpdvh" ) ) != EOF ) { switch ( c ) { @@ -102,6 +103,9 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': pre ^= 1; break; + case 'd': + fDumpCnf ^= 1; + break; case 'v': verb ^= 1; break; @@ -116,7 +120,7 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( argc == globalUtilOptind + 1 ) { - Glucose_SolveCnf( argv[globalUtilOptind], &pPars ); + Glucose_SolveCnf( argv[globalUtilOptind], &pPars, fDumpCnf ); return 0; } @@ -132,10 +136,11 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &glucose [-C num] [-pvh] \n" ); + Abc_Print( -2, "usage: &glucose [-C num] [-pdvh] \n" ); Abc_Print( -2, "\t run Glucose 3.0 by Gilles Audemard and Laurent Simon\n" ); Abc_Print( -2, "\t-C num : conflict limit [default = %d]\n", nConfls ); Abc_Print( -2, "\t-p : enable preprocessing [default = %d]\n",pre); + Abc_Print( -2, "\t-d : enable dumping CNF after proprocessing [default = %d]\n",fDumpCnf); Abc_Print( -2, "\t-v : verbosity [default = %d]\n",verb); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : (optional) CNF file to solve\n"); diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp index c975c6ca..cfb388de 100644 --- a/src/sat/glucose/Glucose.cpp +++ b/src/sat/glucose/Glucose.cpp @@ -1330,7 +1330,7 @@ void Solver::toDimacs(FILE* f, Clause& c, vec& map, Var& max) void Solver::toDimacs(const char *file, const vec& assumps) { - FILE* f = fopen(file, "wr"); + FILE* f = fopen(file, "wb"); if (f == NULL) fprintf(stderr, "could not open file %s\n", file), exit(1); toDimacs(f, assumps); diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp index 7a8b265b..4b4c28e7 100644 --- a/src/sat/glucose2/Glucose2.cpp +++ b/src/sat/glucose2/Glucose2.cpp @@ -1535,7 +1535,7 @@ void Solver::toDimacs(FILE* f, Clause& c, vec& map, Var& max) void Solver::toDimacs(const char *file, const vec& assumps) { - FILE* f = fopen(file, "wr"); + FILE* f = fopen(file, "wb"); if (f == NULL) fprintf(stderr, "could not open file %s\n", file), exit(1); toDimacs(f, assumps); -- cgit v1.2.3 From 1f56f20e1bcd7528b526cf6d48776a606edf61fd Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 24 Apr 2022 09:29:52 -0700 Subject: Experiments with SAT sweeping. --- src/sat/glucose2/AbcGlucose2.cpp | 6 +++ src/sat/glucose2/CGlucoseCore.h | 79 ++++++++++++++++++++++++++++++++++++++++ src/sat/glucose2/Glucose2.cpp | 27 +++++++++----- src/sat/glucose2/Solver.h | 8 ++++ 4 files changed, 111 insertions(+), 9 deletions(-) (limited to 'src/sat') diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp index 9a8b97eb..c1d77587 100644 --- a/src/sat/glucose2/AbcGlucose2.cpp +++ b/src/sat/glucose2/AbcGlucose2.cpp @@ -1536,6 +1536,12 @@ int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars) return (ret == l_True ? 10 : ret == l_False ? 20 : 0); } +extern "C" { + void glucose2_markapprox( void * pSat, int v0, int v1, int nlim ){ + ((Gluco2::Solver*) pSat)->markApprox(v0, v1, nlim); + } +}; + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/glucose2/CGlucoseCore.h b/src/sat/glucose2/CGlucoseCore.h index c0f96fc4..22de92d2 100644 --- a/src/sat/glucose2/CGlucoseCore.h +++ b/src/sat/glucose2/CGlucoseCore.h @@ -613,6 +613,85 @@ inline void Solver::prelocate( int base_var_num ){ polarity .prelocate( base_var_num ); } + +inline void Solver::markTill( Var v, int nlim ){ + if( var2TravId[v] == travId ) + return; + + vMarked.push(v); + + if( vMarked.size() >= nlim ) + return; + if( var2TravId[v] == travId-1 || !isTwoFanin(v) ) + goto finalize; + + markTill( getFaninVar0(v), nlim ); + markTill( getFaninVar1(v), nlim ); +finalize: + var2TravId[v] = travId; +} + +inline void Solver::markApprox( Var v0, Var v1, int nlim ){ + int i; + if( travId <= 1 || nSkipMark>=4 || 0 == nlim ) + goto finalize; + + vMarked.shrink_( vMarked.size() ); + travId ++ ; // travId = t+1 + assert(travId>1); + + markTill(v0, nlim); + if( vMarked.size() >= nlim ) + goto finalize; + + markTill(v1, nlim); + if( vMarked.size() >= nlim ) + goto finalize; + + travId -- ; // travId = t + for(i = 0; i < vMarked.size(); i ++){ + var2TravId [ vMarked[i] ] = travId; // set new nodes to time t + var2NodeData[ vMarked[i] ].sort = 0; + } + nSkipMark ++ ; + return; +finalize: + + travId ++ ; + nSkipMark = 0; + markCone(v0); + markCone(v1); +} + +inline void Solver::loadJust_rec( Var v ){ + //assert( value(v) != l_Undef ); + if( var2TravId[v] == travId || value(v) == l_Undef ) + return; + assert( var2TravId[v] == travId-1 ); + var2TravId[v] = travId; + vMarked.push(v); + + if( !isTwoFanin(v) ){ + JustModel.push( mkLit( v, value(v) == l_False ) ); + return; + } + loadJust_rec( getFaninVar0(v) ); + loadJust_rec( getFaninVar1(v) ); +} +inline void Solver::loadJust(){ + int i; + travId ++ ; + JustModel.shrink_(JustModel.size()); + vMarked.shrink_(vMarked.size()); + JustModel.push(toLit(0)); + for(i = 0; i < assumptions.size(); i ++) + loadJust_rec( var(assumptions[i]) ); + JustModel[0] = toLit( JustModel.size()-1 ); + travId -- ; + for(i = 0; i < vMarked.size(); i ++) + var2TravId[ vMarked[i] ] = travId; +} + }; ABC_NAMESPACE_IMPL_END diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp index 4b4c28e7..d345cd0a 100644 --- a/src/sat/glucose2/Glucose2.cpp +++ b/src/sat/glucose2/Glucose2.cpp @@ -186,6 +186,7 @@ Solver::Solver() : itpc = ca.alloc(tmp); ca[itpc].shrink( ca[itpc].size() ); + nSkipMark = 0; #endif } @@ -1452,15 +1453,20 @@ printf("c ==================================[ Search Statistics (every %6d confl if (status == l_True){ if( justUsage() ){ - JustModel.shrink_(JustModel.size()); - assert(jheap.empty()); - //JustModel.growTo(nVars()); - int i = 0, j = 0; - JustModel.push(toLit(0)); - for (; i < trail.size(); i++) - if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) ) - JustModel.push(trail[i]), j++; - JustModel[0] = toLit(j); + if( nSkipMark ){ + loadJust(); + } else { + JustModel.shrink_(JustModel.size()); + assert(jheap.empty()); + //JustModel.growTo(nVars()); + int i = 0, j = 0; + JustModel.push(toLit(0)); + for (; i < trail.size(); i++) + if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) ) + JustModel.push(trail[i]), j++; + JustModel[0] = toLit(j); + } + } else { // Extend & copy model: model.shrink_(model.size()); @@ -1743,6 +1749,9 @@ void Solver::reset() itpc = ca.alloc(tmp); ca[itpc].shrink( ca[itpc].size() ); } + + vMarked.shrink_( vMarked.size() ); + nSkipMark = 0; #endif } diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h index b1d38d79..004fdc95 100644 --- a/src/sat/glucose2/Solver.h +++ b/src/sat/glucose2/Solver.h @@ -453,7 +453,15 @@ protected: Heap2 jheap; vec jlevel; vec jnext; + + int nSkipMark; + void loadJust_rec( Var v ); + void loadJust(); + vec vMarked; public: + void markTill( Var v0, int nlim ); + void markApprox( Var v0, Var v1, int nlim ); + void prelocate( int var_num ); void setVarFaninLits( Var v, Lit lit1, Lit lit2 ); void setVarFaninLits( int v, int lit1, int lit2 ){ setVarFaninLits( Var(v), toLit(lit1), toLit(lit2) ); } -- cgit v1.2.3 From 1abd0457abb9f522da48e24996545b155285bac9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 24 Apr 2022 10:25:46 -0700 Subject: Experiments with SAT sweeping. --- src/sat/glucose2/AbcGlucose2.cpp | 25 +++++++++++++++++++------ src/sat/glucose2/AbcGlucose2.h | 1 + 2 files changed, 20 insertions(+), 6 deletions(-) (limited to 'src/sat') diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp index c1d77587..99ca112a 100644 --- a/src/sat/glucose2/AbcGlucose2.cpp +++ b/src/sat/glucose2/AbcGlucose2.cpp @@ -132,6 +132,10 @@ void glucose2_solver_setstop(Gluco2::SimpSolver* S, int * pstop) S->pstop = pstop; } +void glucose2_markapprox( Gluco2::SimpSolver* S, int v0, int v1, int nlim ) +{ + S->markApprox(v0, v1, nlim); +} /**Function************************************************************* @@ -228,6 +232,11 @@ void bmcg2_sat_solver_set_stop(bmcg2_sat_solver* s, int * pstop) glucose2_solver_setstop((Gluco2::SimpSolver*)s, pstop); } +void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim) +{ + glucose2_markapprox((Gluco2::SimpSolver*)s, v0, v1, nlim); +} + abctime bmcg2_sat_solver_set_runtime_limit(bmcg2_sat_solver* s, abctime Limit) { abctime nRuntimeLimit = ((Gluco2::SimpSolver*)s)->nRuntimeLimit; @@ -474,6 +483,11 @@ void glucose2_solver_setstop(Gluco2::Solver* S, int * pstop) S->pstop = pstop; } +void glucose2_markapprox( Gluco2::Solver* S, int v0, int v1, int nlim ) +{ + S->markApprox(v0, v1, nlim); +} + /**Function************************************************************* @@ -570,6 +584,11 @@ void bmcg2_sat_solver_set_stop(bmcg2_sat_solver* s, int * pstop) glucose2_solver_setstop((Gluco2::Solver*)s, pstop); } +void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim) +{ + glucose2_markapprox((Gluco2::Solver*)s, v0, v1, nlim); +} + abctime bmcg2_sat_solver_set_runtime_limit(bmcg2_sat_solver* s, abctime Limit) { abctime nRuntimeLimit = ((Gluco2::Solver*)s)->nRuntimeLimit; @@ -1536,12 +1555,6 @@ int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars) return (ret == l_True ? 10 : ret == l_False ? 20 : 0); } -extern "C" { - void glucose2_markapprox( void * pSat, int v0, int v1, int nlim ){ - ((Gluco2::Solver*) pSat)->markApprox(v0, v1, nlim); - } -}; - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h index 9299d290..d1c15639 100644 --- a/src/sat/glucose2/AbcGlucose2.h +++ b/src/sat/glucose2/AbcGlucose2.h @@ -86,6 +86,7 @@ extern int bmcg2_sat_solver_elim_varnum(bmcg2_sat_solver* s); extern int * bmcg2_sat_solver_read_cex( bmcg2_sat_solver* s ); extern int bmcg2_sat_solver_read_cex_varvalue( bmcg2_sat_solver* s, int ); extern void bmcg2_sat_solver_set_stop( bmcg2_sat_solver* s, int * pstop ); +extern void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim); extern abctime bmcg2_sat_solver_set_runtime_limit( bmcg2_sat_solver* s, abctime Limit ); extern void bmcg2_sat_solver_set_conflict_budget( bmcg2_sat_solver* s, int Limit ); extern int bmcg2_sat_solver_varnum( bmcg2_sat_solver* s ); -- cgit v1.2.3