summaryrefslogtreecommitdiffstats
path: root/src/opt/fxu/fxuInt.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/fxu/fxuInt.h')
-rw-r--r--src/opt/fxu/fxuInt.h12
1 files changed, 5 insertions, 7 deletions
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index ea85cb79..59b2df6d 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -23,6 +23,7 @@
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
+#include "util.h"
#include "extra.h"
#include "vec.h"
@@ -172,8 +173,6 @@ struct FxuMatrix // ~ 30 words
// the single cube divisors
Fxu_ListSingle lSingles; // the linked list of single cube divisors
Fxu_HeapSingle * pHeapSingle; // the heap of variables by the number of literals in the matrix
- int nWeightLimit;// the limit on weight of single cube divisors collected
- int nSingleTotal;// the total number of single cube divisors
// storage for cube pairs
Fxu_Pair *** pppPairs;
Fxu_Pair ** ppPairs;
@@ -273,7 +272,7 @@ struct FxuSingle // 7 words
};
////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
+/// MACRO DEFITIONS ///
////////////////////////////////////////////////////////////////////////
// minimum/maximum
@@ -431,7 +430,7 @@ extern void Fxu_MatrixRingVarsUnmark( Fxu_Matrix * p );
#endif
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/*===== fxu.c ====================================================*/
@@ -461,7 +460,7 @@ extern void Fxu_PairClearStorage( Fxu_Cube * pCube );
extern Fxu_Pair * Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
extern void Fxu_PairAdd( Fxu_Pair * pPair );
/*===== fxuSingle.c ====================================================*/
-extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax );
+extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p );
extern void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar );
extern int Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 );
/*===== fxuMatrix.c ====================================================*/
@@ -531,9 +530,8 @@ extern int Fxu_HeapSingleReadMaxWeight( Fxu_HeapSingle * p );
extern Fxu_Single * Fxu_HeapSingleReadMax( Fxu_HeapSingle * p );
extern Fxu_Single * Fxu_HeapSingleGetMax( Fxu_HeapSingle * p );
-#endif
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+#endif