summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bsat/satProof2.h326
-rw-r--r--src/sat/bsat/satSolver2.c89
-rw-r--r--src/sat/bsat/satSolver2.h8
3 files changed, 393 insertions, 30 deletions
diff --git a/src/sat/bsat/satProof2.h b/src/sat/bsat/satProof2.h
new file mode 100644
index 00000000..82ed9264
--- /dev/null
+++ b/src/sat/bsat/satProof2.h
@@ -0,0 +1,326 @@
+/**CFile****************************************************************
+
+ FileName [satProof2.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT solver.]
+
+ Synopsis [Proof logging.]
+
+ Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - January 1, 2004.]
+
+ Revision [$Id: satProof2.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__sat__bsat__satProof2_h
+#define ABC__sat__bsat__satProof2_h
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "misc/vec/vec.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// STRUCTURE DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Prf_Man_t_ Prf_Man_t;
+struct Prf_Man_t_
+{
+ int iFirst; // first learned clause with proof
+ int iFirst2; // first learned clause with proof
+ int nWords; // the number of proof words
+ word * pInfo; // pointer to the current proof
+ Vec_Wrd_t * vInfo; // proof information
+ Vec_Int_t * vSaved; // IDs of saved clauses
+ Vec_Int_t * vId2Pr; // mapping proof IDs of problem clauses into bitshifts (user's array)
+};
+
+////////////////////////////////////////////////////////////////////////
+/// GLOBAL VARIABLES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Prf_BitWordNum( int nWidth ) { return (nWidth >> 6) + ((nWidth & 63) > 0); }
+static inline int Prf_ManSize( Prf_Man_t * p ) { return Vec_WrdSize( p->vInfo ) / p->nWords; }
+static inline void Prf_ManClearNewInfo( Prf_Man_t * p ) { int w; for ( w = 0; w < p->nWords; w++ ) Vec_WrdPush( p->vInfo, 0 ); }
+static inline word * Prf_ManClauseInfo( Prf_Man_t * p, int Id ) { return Vec_WrdEntryP( p->vInfo, Id * p->nWords ); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Prf_Man_t * Prf_ManAlloc()
+{
+ Prf_Man_t * p;
+ p = ABC_CALLOC( Prf_Man_t, 1 );
+ p->iFirst = -1;
+ p->iFirst2 = -1;
+ p->vInfo = Vec_WrdAlloc( 1000 );
+ p->vSaved = Vec_IntAlloc( 1000 );
+ return p;
+}
+static inline void Prf_ManStop( Prf_Man_t * p )
+{
+ if ( p == NULL )
+ return;
+ Vec_IntFree( p->vSaved );
+ Vec_WrdFree( p->vInfo );
+ ABC_FREE( p );
+}
+static inline void Prf_ManStopP( Prf_Man_t ** p )
+{
+ Prf_ManStop( *p );
+ *p = NULL;
+}
+static inline double Prf_ManMemory( Prf_Man_t * p )
+{
+ return Vec_WrdMemory(p->vInfo) + Vec_IntMemory(p->vSaved) + sizeof(Prf_Man_t);
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Prf_ManRestart( Prf_Man_t * p, Vec_Int_t * vId2Pr, int iFirst, int nWidth )
+{
+ assert( p->iFirst == -1 );
+ p->iFirst = iFirst;
+ p->nWords = Prf_BitWordNum( nWidth );
+ p->vId2Pr = vId2Pr;
+ p->pInfo = NULL;
+ Vec_WrdClear( p->vInfo );
+}
+static inline void Prf_ManGrow( Prf_Man_t * p, int nWidth )
+{
+ Vec_Wrd_t * vInfoNew;
+ int i, w, nSize, nWordsNew;
+ assert( p->iFirst >= 0 );
+ assert( p->pInfo == NULL );
+ if ( nWidth < 64 * p->nWords )
+ return;
+ // get word count after resizing
+ nWordsNew = Abc_MaxInt( Prf_BitWordNum(nWidth), 2 * p->nWords );
+ // remap the entries
+ nSize = Prf_ManSize( p );
+ vInfoNew = Vec_WrdAlloc( (nSize + 1000) * nWordsNew );
+ for ( i = 0; i < nSize; i++ )
+ {
+ p->pInfo = Prf_ManClauseInfo( p, i );
+ for ( w = 0; w < p->nWords; w++ )
+ Vec_WrdPush( vInfoNew, p->pInfo[w] );
+ for ( ; w < nWordsNew; w++ )
+ Vec_WrdPush( vInfoNew, 0 );
+ }
+ Vec_WrdFree( p->vInfo );
+ p->vInfo = vInfoNew;
+ p->nWords = nWordsNew;
+ p->pInfo = NULL;
+
+}
+static inline void Prf_ManShrink( Prf_Man_t * p, int iClause )
+{
+ assert( p->iFirst >= 0 );
+ assert( iClause - p->iFirst >= 0 );
+ assert( iClause - p->iFirst < Prf_ManSize(p) );
+ Vec_WrdShrink( p->vInfo, (iClause - p->iFirst) * p->nWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Prf_ManAddSaved( Prf_Man_t * p, int i, int iNew )
+{
+ assert( p->iFirst >= 0 );
+ if ( i < p->iFirst )
+ return;
+ if ( Vec_IntSize(p->vSaved) == 0 )
+ {
+ assert( p->iFirst2 == -1 );
+ p->iFirst2 = iNew;
+ }
+ Vec_IntPush( p->vSaved, i );
+}
+static inline void Prf_ManCompact( Prf_Man_t * p, int iNew )
+{
+ int i, w, k = 0, Entry, nSize;
+ assert( p->iFirst >= 0 );
+ assert( p->pInfo == NULL );
+ nSize = Prf_ManSize( p );
+ Vec_IntForEachEntry( p->vSaved, Entry, i )
+ {
+ assert( Entry - p->iFirst >= 0 && Entry - p->iFirst < nSize );
+ p->pInfo = Prf_ManClauseInfo( p, Entry - p->iFirst );
+ for ( w = 0; w < p->nWords; w++ )
+ Vec_WrdWriteEntry( p->vInfo, k++, p->pInfo[w] );
+ }
+ Vec_WrdShrink( p->vInfo, k );
+ Vec_IntClear( p->vSaved );
+ p->pInfo = NULL;
+ // update first
+ if ( p->iFirst2 == -1 )
+ p->iFirst = iNew;
+ else
+ p->iFirst = p->iFirst2;
+ p->iFirst2 = -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Prf_ManChainResolve( Prf_Man_t * p, clause * c )
+{
+ assert( p->iFirst >= 0 );
+ assert( p->pInfo != NULL );
+ // add to proof info
+ if ( c->lrn ) // learned clause
+ {
+ if ( clause_id(c) >= p->iFirst )
+ {
+ word * pProofStart;
+ int w;
+ assert( clause_id(c) - p->iFirst >= 0 );
+ assert( clause_id(c) - p->iFirst < Prf_ManSize(p) );
+ pProofStart = Prf_ManClauseInfo( p, clause_id(c) - p->iFirst );
+ for ( w = 0; w < p->nWords; w++ )
+ p->pInfo[w] |= pProofStart[w];
+ }
+ }
+ else // problem clause
+ {
+ if ( clause_id(c) ) // has proof ID
+ {
+ int Entry;
+ if ( p->vId2Pr == NULL )
+ Entry = clause_id(c);
+ else
+ Entry = Vec_IntEntry( p->vId2Pr, clause_id(c) );
+ if ( Entry >= 0 )
+ {
+ assert( Entry < 64 * p->nWords );
+ Abc_InfoSetBit( (unsigned *)p->pInfo, Entry );
+ }
+ }
+ }
+}
+static inline void Prf_ManChainStart( Prf_Man_t * p, clause * c )
+{
+ assert( p->iFirst >= 0 );
+ // prepare info for new clause
+ Prf_ManClearNewInfo( p );
+ // get pointer to the proof
+ assert( p->pInfo == NULL );
+ p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
+ // add to proof info
+ Prf_ManChainResolve( p, c );
+}
+static inline int Prf_ManChainStop( Prf_Man_t * p )
+{
+ assert( p->pInfo != NULL );
+ p->pInfo = NULL;
+ return 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Vec_Int_t * Prf_ManUnsatCore( Prf_Man_t * p )
+{
+ Vec_Int_t * vCore;
+ int i, Entry;
+ assert( p->iFirst >= 0 );
+ assert( p->pInfo == NULL );
+ vCore = Vec_IntAlloc( 64 * p->nWords );
+ p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
+ if ( p->vId2Pr == NULL )
+ {
+ for ( i = 0; i < 64 * p->nWords; i++ )
+ if ( Abc_InfoHasBit( (unsigned *)p->pInfo, i ) )
+ Vec_IntPush( vCore, i );
+ }
+ else
+ {
+ Vec_IntForEachEntry( p->vId2Pr, Entry, i )
+ {
+ if ( Entry < 0 )
+ continue;
+ assert( Entry < 64 * p->nWords );
+ if ( Abc_InfoHasBit( (unsigned *)p->pInfo, Entry ) )
+ Vec_IntPush( vCore, i );
+ }
+ }
+ p->pInfo = NULL;
+ Vec_IntSort( vCore, 1 );
+ return vCore;
+}
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index b84f5a5f..6662eca5 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -161,7 +161,11 @@ static inline veci* solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l
static inline void proof_chain_start( sat_solver2* s, clause* c )
{
- if ( s->fProofLogging )
+ if ( !s->fProofLogging )
+ return;
+ if ( s->pPrf2 )
+ Prf_ManChainStart( s->pPrf2, c );
+ if ( s->pPrf1 )
{
int ProofId = clause2_proofid(s, c, 0);
assert( (ProofId >> 2) > 0 );
@@ -174,7 +178,14 @@ static inline void proof_chain_start( sat_solver2* s, clause* c )
static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
{
- if ( s->fProofLogging )
+ if ( !s->fProofLogging )
+ return;
+ if ( s->pPrf2 )
+ {
+ clause* c = cls ? cls : var_unit_clause( s, Var );
+ Prf_ManChainResolve( s->pPrf2, c );
+ }
+ if ( s->pPrf1 )
{
clause* c = cls ? cls : var_unit_clause( s, Var );
int ProofId = clause2_proofid(s, c, var_is_partA(s,Var));
@@ -185,11 +196,15 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
static inline int proof_chain_stop( sat_solver2* s )
{
- if ( s->fProofLogging )
+ if ( !s->fProofLogging )
+ return 0;
+ if ( s->pPrf2 )
+ Prf_ManChainStop( s->pPrf2 );
+ if ( s->pPrf1 )
{
extern void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts );
- int h = Vec_SetAppend( &s->Proofs, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
- Proof_ClauseSetEnts( &s->Proofs, h, veci_size(&s->temp_proof) - 2 );
+ int h = Vec_SetAppend( s->pPrf1, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
+ Proof_ClauseSetEnts( s->pPrf1, h, veci_size(&s->temp_proof) - 2 );
return h;
}
return 0;
@@ -371,7 +386,7 @@ static inline int sat_clause_compute_lbd( sat_solver2* s, clause* c )
return lbd;
}
-static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id)
+static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id )
{
clause* c;
int h, size = end - begin;
@@ -385,11 +400,11 @@ static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt,
c = clause2_read( s, h );
if (learnt)
{
- if ( s->fProofLogging )
+ if ( s->pPrf1 )
assert( proof_id );
c->lbd = sat_clause_compute_lbd( s, c );
assert( clause_id(c) == veci_size(&s->act_clas) );
- if ( proof_id )
+ if ( s->pPrf1 )
veci_push(&s->claProofs, proof_id);
// veci_push(&s->act_clas, (1<<10));
veci_push(&s->act_clas, 0);
@@ -674,7 +689,8 @@ static int solver2_lit_removable(sat_solver2* s, int x)
while (veci_size(&s->stack))
{
x = veci_pop(&s->stack);
- if ( s->fProofLogging ){
+ if ( s->fProofLogging )
+ {
if ( x & 1 ){
if ( var_tag(s,x >> 1) & 1 )
veci_push(&s->min_lit_order, x >> 1 );
@@ -910,7 +926,8 @@ clause* solver2_propagate(sat_solver2* s)
// Did not find watch -- clause is unit under assignment:
Lit = lits[0];
- if (s->fProofLogging && solver2_dlevel(s) == 0){
+ if ( s->fProofLogging && solver2_dlevel(s) == 0 )
+ {
int k, x, proof_id, Cid, Var = lit_var(Lit);
int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit));
// Log production of top-level unit clause:
@@ -990,7 +1007,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
s->stats.conflicts++; conflictC++;
if (solver2_dlevel(s) <= s->root_level){
proof_id = solver2_analyze_final(s, confl, 0);
- assert( proof_id > 0 );
+ if ( s->pPrf1 )
+ assert( proof_id > 0 );
s->hProofLast = proof_id;
veci_delete(&learnt_clause);
return l_False;
@@ -1112,12 +1130,11 @@ sat_solver2* sat_solver2_new(void)
veci_new(&s->min_lit_order);
veci_new(&s->min_step_order);
// veci_new(&s->learnt_live);
-
Sat_MemAlloc_( &s->Mem, 14 );
veci_new(&s->act_clas);
+ // proof-logging
veci_new(&s->claProofs);
- if ( s->fProofLogging )
- Vec_SetAlloc_( &s->Proofs, 20 );
+// s->pPrf1 = Vec_SetAlloc( 20 );
// initialize clause pointers
s->hLearntLast = -1; // the last learnt clause
@@ -1218,7 +1235,8 @@ void sat_solver2_delete(sat_solver2* s)
// veci_delete(&s->lrns);
Sat_MemFree_( &s->Mem );
// veci_delete(&s->proofs);
- Vec_SetFree_( &s->Proofs );
+ Vec_SetFree( s->pPrf1 );
+ Prf_ManStop( s->pPrf2 );
// delete arrays
if (s->vi != 0){
@@ -1424,7 +1442,7 @@ void sat_solver2_reducedb(sat_solver2* s)
// mark learned clauses to remove
Counter = j = 0;
- pClaProofs = s->fProofLogging ? veci_begin(&s->claProofs) : NULL;
+ pClaProofs = veci_size(&s->claProofs) ? veci_begin(&s->claProofs) : NULL;
Sat_MemForEachLearned( pMem, c, i, k )
{
assert( c->mark == 0 );
@@ -1432,7 +1450,9 @@ void sat_solver2_reducedb(sat_solver2* s)
{
pSortValues[j] = pSortValues[clause_id(c)];
if ( pClaProofs )
- pClaProofs[j] = pClaProofs[clause_id(c)];
+ pClaProofs[j] = pClaProofs[clause_id(c)];
+ if ( s->pPrf2 )
+ Prf_ManAddSaved( s->pPrf2, clause_id(c), j );
j++;
}
else // delete
@@ -1443,13 +1463,15 @@ void sat_solver2_reducedb(sat_solver2* s)
}
}
ABC_FREE( pSortValues );
+ if ( s->pPrf2 )
+ Prf_ManCompact( s->pPrf2, j );
// if ( j == nLearnedOld )
// return;
assert( s->stats.learnts == (unsigned)j );
assert( Counter == nLearnedOld );
veci_resize(&s->act_clas,j);
- if ( s->fProofLogging )
+ if ( veci_size(&s->claProofs) )
veci_resize(&s->claProofs,j);
// update ID of each clause to be its new handle
@@ -1508,8 +1530,8 @@ void sat_solver2_reducedb(sat_solver2* s)
assert( Counter == (int)s->stats.learnts );
// compact proof (compacts 'proofs' and update 'claProofs')
- if ( s->fProofLogging )
- s->hProofPivot = Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
+ if ( s->pPrf1 )
+ s->hProofPivot = Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
// report the results
@@ -1531,7 +1553,7 @@ void sat_solver2_rollback( sat_solver2* s )
Count++;
assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
- assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(&s->Proofs) );
+ assert( s->pPrf1 == NULL || (s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(s->pPrf1)) );
// reset implication queue
solver2_canceluntil_rollback( s, s->iTrailPivot );
// update order
@@ -1568,14 +1590,17 @@ void sat_solver2_rollback( sat_solver2* s )
// resize learned arrays
veci_resize(&s->act_clas, s->stats.learnts);
- if ( s->fProofLogging )
+ if ( s->pPrf1 )
{
veci_resize(&s->claProofs, s->stats.learnts);
// Vec_SetShrink(&s->Proofs, s->hProofPivot);
// some weird bug here, which shows only on 64-bits!
// temporarily, perform more general proof reduction
- Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
+ Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
}
+ assert( s->pPrf2 == NULL );
+// if ( s->pPrf2 )
+// Prf_ManShrink( s->pPrf2, s->stats.learnts );
// initialize other vars
s->size = s->iVarPivot;
@@ -1641,8 +1666,6 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
#else
Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );
#endif
-// if ( s->factors )
-// Mem += s->cap * sizeof(double); // ABC_FREE(s->factors );
Mem += s->cap * sizeof(lit); // ABC_FREE(s->trail );
Mem += s->cap * sizeof(int); // ABC_FREE(s->orderpos );
Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons );
@@ -1659,12 +1682,15 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
Mem += s->min_step_order.cap * sizeof(int);
Mem += s->temp_proof.cap * sizeof(int);
Mem += Sat_MemMemoryAll( &s->Mem );
-// Mem += Vec_ReportMemory( &s->Proofs );
+// Mem += Vec_ReportMemory( s->pPrf1 );
return Mem;
}
double sat_solver2_memory_proof( sat_solver2* s )
{
- return Vec_ReportMemory( &s->Proofs );
+ double Mem = s->dPrfMemory;
+ if ( s->pPrf1 )
+ Mem += Vec_ReportMemory( s->pPrf1 );
+ return Mem;
}
@@ -1911,7 +1937,14 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
void * Sat_ProofCore( sat_solver2 * s )
{
extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot );
- return Proof_DeriveCore( &s->Proofs, s->hProofLast );
+ if ( s->pPrf1 )
+ return Proof_DeriveCore( s->pPrf1, s->hProofLast );
+ if ( s->pPrf2 )
+ {
+ s->dPrfMemory = Abc_MaxDouble( s->dPrfMemory, Prf_ManMemory(s->pPrf2) );
+ return Prf_ManUnsatCore( s->pPrf2 );
+ }
+ return NULL;
}
ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 81ecea76..1682ab6e 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -31,6 +31,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "satVec.h"
#include "satClause.h"
#include "misc/vec/vecSet.h"
+#include "satProof2.h"
ABC_NAMESPACE_HEADER_START
@@ -147,10 +148,12 @@ struct sat_solver2_t
veci learnt_live; // remaining clauses after reduce DB
// proof logging
- Vec_Set_t Proofs; // sequence of proof records
+ Vec_Set_t * pPrf1; // sequence of proof records
veci temp_proof; // temporary place to store proofs
int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
+ Prf_Man_t * pPrf2; // another proof manager
+ double dPrfMemory; // memory used by the proof-logger
// statistics
stats_t stats;
@@ -234,7 +237,8 @@ static inline void sat_solver2_bookmark(sat_solver2* s)
assert( s->qhead == s->qtail );
s->iVarPivot = s->size;
s->iTrailPivot = s->qhead;
- s->hProofPivot = Vec_SetHandCurrent(&s->Proofs);
+ if ( s->pPrf1 )
+ s->hProofPivot = Vec_SetHandCurrent(s->pPrf1);
Sat_MemBookMark( &s->Mem );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 17:27:51 +0000