summaryrefslogtreecommitdiffstats
path: root/src/sat/fraig/fraigInt.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/fraig/fraigInt.h')
-rw-r--r--src/sat/fraig/fraigInt.h6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 890af13c..8e016331 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -189,7 +189,8 @@ struct Fraig_ManStruct_t_
int nSatCalls; // the number of times equivalence checking was called
int nSatProof; // the number of times a proof was found
int nSatCounter; // the number of times a counter example was found
- int nSatFails; // the number of times the SAT solver failed to complete
+ int nSatFails; // the number of times the SAT solver failed to complete due to resource limit or prediction
+ int nSatFailsReal; // the number of times the SAT solver failed to complete due to resource limit
int nSatCallsImp; // the number of times equivalence checking was called
int nSatProofImp; // the number of times a proof was found
@@ -243,8 +244,9 @@ struct Fraig_NodeStruct_t_
unsigned fMark3 : 1; // the mark used for traversals
unsigned fFeedUse : 1; // the presence of the variable in the feedback
unsigned fFeedVal : 1; // the value of the variable in the feedback
+ unsigned fFailTfo : 1; // the node is in the TFO of the failed SAT run
unsigned nFanouts : 2; // the indicator of fanouts (none, one, or many)
- unsigned nOnes : 21; // the number of 1's in the random sim info
+ unsigned nOnes : 20; // the number of 1's in the random sim info
// the children of the node
Fraig_Node_t * p1; // the first child