summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/asat/solver.h5
-rw-r--r--src/sat/fraig/fraigCanon.c4
-rw-r--r--src/sat/fraig/fraigSat.c22
-rw-r--r--src/sat/msat/msat.h1
-rw-r--r--src/sat/msat/msatClause.c5
-rw-r--r--src/sat/msat/msatInt.h1
-rw-r--r--src/sat/msat/msatSolverApi.c1
-rw-r--r--src/sat/msat/msatSolverCore.c20
8 files changed, 54 insertions, 5 deletions
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index b82601c4..9618603c 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -52,8 +52,9 @@ static const lbool l_Undef = 0;
static const lbool l_True = 1;
static const lbool l_False = -1;
-static inline lit neg (lit l) { return l ^ 1; }
-static inline lit toLit (int v) { return v + v; }
+static inline lit neg (lit l) { return l ^ 1; }
+static inline lit toLit (int v) { return v + v; }
+static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); }
//=================================================================================================
// Public interface:
diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c
index 97da413d..fab01368 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -68,7 +68,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
return p1;
return Fraig_Not(pMan->pConst1);
}
-
+/*
// check for less trivial cases
if ( Fraig_IsComplement(p1) )
{
@@ -125,7 +125,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
return Fraig_Not(pMan->pConst1);
}
}
-
+*/
// perform level-one structural hashing
if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found
{
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index bc60e4e9..13f6b50b 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -41,6 +41,8 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i );
// The best way seems to be fanins followed by fanouts. Slight changes to this order
// leads to big degradation in quality.
+static int nMuxes;
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -105,7 +107,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
}
if ( p->fVerboseP )
{
- PRT( "Final miter proof time", clock() - clk );
+// PRT( "Final miter proof time", clock() - clk );
}
}
@@ -195,6 +197,8 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
}
*/
+ nMuxes = 0;
+
// get the logic cone
clk = clock();
@@ -202,6 +206,9 @@ clk = clock();
// Fraig_PrepareCones( p, pOld, pNew );
p->timeTrav += clock() - clk;
+// printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) );
+// PRT( "Time", clock() - clk );
+
if ( fVerbose )
printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
@@ -226,6 +233,8 @@ clk = clock();
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += clock() - clk;
+Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
+
if ( RetValue1 == MSAT_FALSE )
{
//p->time1 += clock() - clk;
@@ -284,6 +293,7 @@ p->time3 += clock() - clk;
clk = clock();
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += clock() - clk;
+
if ( RetValue1 == MSAT_FALSE )
{
//p->time1 += clock() - clk;
@@ -552,6 +562,7 @@ void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t *
Fraig_PrepareCones_rec( pMan, pNew );
Fraig_PrepareCones_rec( pMan, pOld );
+
/*
nVars = Msat_IntVecReadSize( pMan->vVarsInt );
pVars = Msat_IntVecReadArray( pMan->vVarsInt );
@@ -715,6 +726,8 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t
Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
Fraig_SupergateAddClausesMux( pMan, pNode );
// Fraig_DetectFanoutFreeConeMux( pMan, pNode );
+
+ nMuxes++;
}
else
{
@@ -1057,6 +1070,12 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
// t + e + f'
// t' + e' + f
+ if ( VarT == VarE )
+ {
+// assert( fCompT == !fCompE );
+ return;
+ }
+
Msat_IntVecClear( p->vProj );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) );
@@ -1069,6 +1088,7 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) );
RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
assert( RetValue );
+
}
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 37e0bbeb..40028784 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -87,6 +87,7 @@ extern void Msat_SolverPrintClauses( Msat_Solver_t * p );
extern void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
// access to the solver internal data
extern int Msat_SolverReadVarNum( Msat_Solver_t * p );
+extern int Msat_SolverReadClauseNum( Msat_Solver_t * p );
extern int Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
extern int * Msat_SolverReadAssignsArray( Msat_Solver_t * p );
extern int * Msat_SolverReadModelArray( Msat_Solver_t * p );
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
index f944ed81..62b9ecad 100644
--- a/src/sat/msat/msatClause.c
+++ b/src/sat/msat/msatClause.c
@@ -82,6 +82,10 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
// nSeenId - 1 stands for negative
// nSeenId stands for positive
// Remove false literals
+
+ // there is a bug here!!!!
+ // when the same var in opposite polarities is given, it drops one polarity!!!
+
for ( i = j = 0; i < nLits; i++ ) {
// get the corresponding variable
Var = MSAT_LIT2VAR(pLits[i]);
@@ -190,6 +194,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
{
Msat_SolverVarBumpActivity( p, pLits[i] );
// Msat_SolverVarBumpActivity( p, pLits[i] );
+ p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
}
}
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index ef2375a7..3dfe2109 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -151,6 +151,7 @@ struct Msat_Solver_t_
int nSeenId; // the id of current seeing
Msat_IntVec_t * vReason; // the temporary array of literals
Msat_IntVec_t * vTemp; // the temporary array of literals
+ int * pFreq; // the number of times each var participated in conflicts
// the memory manager
Msat_MmStep_t * pMem;
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index dd3a5a43..4a721487 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -42,6 +42,7 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
***********************************************************************/
int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; }
+int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; }
int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc;}
int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); }
int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; }
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index ed228b33..5f13694b 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -140,6 +140,9 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
int64 nConflictsOld = p->Stats.nConflicts;
int64 nDecisionsOld = p->Stats.nDecisions;
+ p->pFreq = ALLOC( int, p->nVarsAlloc );
+ memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
+
if ( vAssumps )
{
int * pAssumps, nAssumps, i;
@@ -181,6 +184,23 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
}
Msat_SolverCancelUntil( p, 0 );
p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
+/*
+ PRT( "True solver runtime", clock() - timeStart );
+ // print the statistics
+ {
+ int i, Counter = 0;
+ for ( i = 0; i < p->nVars; i++ )
+ if ( p->pFreq[i] > 0 )
+ {
+ printf( "%d ", p->pFreq[i] );
+ Counter++;
+ }
+ if ( Counter )
+ printf( "\n" );
+ printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
+ PRT( "Time", clock() - timeStart );
+ }
+*/
return Status;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 20:31:29 +0000