-
Notifications
You must be signed in to change notification settings - Fork 274
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
520 changed files
with
177,651 additions
and
143,537 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,273 @@ | ||
//---------------------------------------------------------------------------------------------------------------------- | ||
// | ||
// BDD package (implementation of ROBDD) | ||
// | ||
// This file is part of libpm library | ||
// | ||
// Copyright (C) 1999, ..., 2023 Pierre Molinaro. | ||
// | ||
// e-mail : [email protected] | ||
// | ||
// This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General | ||
// Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) | ||
// any later version. | ||
// | ||
// This program is distributed in the hope it will be useful, but WITHOUT ANY WARRANTY; without even the implied | ||
// warranty of MERCHANDIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for | ||
// more details. | ||
// | ||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
#include "bdd/C_BDD.h" | ||
#include "utilities/F_GetPrime.h" | ||
#include "strings/C_String.h" | ||
#include "bdd/C_BDD-node.h" | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
#ifdef PRAGMA_MARK_ALLOWED | ||
#pragma mark Cache for AND Operation | ||
#endif | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
// | ||
// And computation cache | ||
// | ||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
class tStructANDOperationCacheEntry { | ||
public: uint64_t mOperands ; | ||
public: uint32_t mResult ; | ||
} ; | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
static const int32_t kANDOperationCacheInitialSize = 262145 ; | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
static uint64_t * gANDOperationCacheOperandMap ; | ||
static uint32_t * gANDOperationCacheResultMap ; | ||
static uint32_t gANDOperationMapSize ; | ||
static uint32_t gANDOperationCacheMapUsedEntryCount ; | ||
static uint64_t gANDOperationCacheTrivialOperationCount ; | ||
static bool gANDOperationCacheExpandable = true ; | ||
static uint32_t gANDOperationCacheMaxPowerOfTwoSize = 31 ; | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
uint32_t ANDCacheMemoryUsage (void) { | ||
return (gANDOperationMapSize * (uint32_t) (sizeof (uint32_t) + sizeof (uint64_t))) / 1000000 ; | ||
} | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
void releaseANDOperationCache (void) { | ||
gANDOperationCacheMapUsedEntryCount = 0 ; | ||
macroMyDeletePODArray (gANDOperationCacheOperandMap) ; | ||
macroMyDeletePODArray (gANDOperationCacheResultMap) ; | ||
gANDOperationMapSize = 0 ; | ||
gANDOperationCacheExpandable = true ; | ||
} | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
void clearANDOperationCache (void) { | ||
gANDOperationCacheMapUsedEntryCount = 0 ; | ||
for (uint32_t i=0 ; i<gANDOperationMapSize ; i++) { | ||
gANDOperationCacheOperandMap [i] = 0 ; | ||
} | ||
} | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
static inline uint64_t getOperands (const uint32_t inOperand1, | ||
const uint32_t inOperand2) { | ||
uint64_t operands = inOperand1 ; | ||
operands <<= 32 ; | ||
operands |= inOperand2 ; | ||
return operands ; | ||
} | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
static bool searchInANDOperationCache (const uint32_t inOperand1, | ||
const uint32_t inOperand2, | ||
uint32_t & outResult) { | ||
if (0 == gANDOperationMapSize) { | ||
gANDOperationMapSize = kANDOperationCacheInitialSize ; | ||
macroMyNewPODArray (gANDOperationCacheOperandMap, uint64_t, gANDOperationMapSize) ; | ||
macroMyNewPODArray (gANDOperationCacheResultMap, uint32_t, gANDOperationMapSize) ; | ||
clearANDOperationCache () ; | ||
if (C_BDD::displaysInformationMessages ()) { | ||
printf ("BDD package info: AND cache allocated to %u %03u %03u (%u MB)\n", | ||
gANDOperationMapSize / 1000000, | ||
(gANDOperationMapSize / 1000) % 1000, | ||
gANDOperationMapSize % 1000, | ||
(gANDOperationMapSize * (uint32_t) (sizeof (uint32_t) + sizeof (uint64_t))) / 1000000) ; | ||
} | ||
} | ||
const uint64_t operands = getOperands (inOperand1, inOperand2) ; | ||
const uint64_t idx = operands % gANDOperationMapSize ; | ||
const bool found = gANDOperationCacheOperandMap [idx] == operands ; | ||
if (found) { | ||
outResult = gANDOperationCacheResultMap [idx] ; | ||
} | ||
return found ; | ||
} | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
static void reallocANDOperationCache (const uint32_t inNewSize) { | ||
if (0 < inNewSize) { | ||
gANDOperationCacheMapUsedEntryCount = 0 ; | ||
uint64_t * newCache = nullptr ; | ||
macroMyNewPODArray (newCache, uint64_t, inNewSize) ; | ||
for (uint32_t i=0 ; i<inNewSize ; i++) { | ||
newCache [i] = 0 ; | ||
} | ||
uint32_t * newResult = nullptr ; | ||
macroMyNewPODArray (newResult, uint32_t, inNewSize) ; | ||
for (uint32_t i=0 ; i<gANDOperationMapSize ; i++) { | ||
if (gANDOperationCacheOperandMap [i] != 0) { | ||
const uint64_t newIndex = gANDOperationCacheOperandMap [i] % inNewSize ; | ||
gANDOperationCacheMapUsedEntryCount += newCache [newIndex] == 0 ; | ||
newCache [newIndex] = gANDOperationCacheOperandMap [i] ; | ||
newResult [newIndex] = gANDOperationCacheResultMap [i] ; | ||
} | ||
} | ||
macroMyDeletePODArray (gANDOperationCacheOperandMap) ; | ||
macroMyDeletePODArray (gANDOperationCacheResultMap) ; | ||
gANDOperationCacheOperandMap = newCache ; | ||
gANDOperationCacheResultMap = newResult ; | ||
gANDOperationMapSize = inNewSize ; | ||
if (C_BDD::displaysInformationMessages ()) { | ||
printf ("BDD package info: AND cache reallocated to %u %03u %03u (%u MB)\n", | ||
gANDOperationMapSize / 1000000, | ||
(gANDOperationMapSize / 1000) % 1000, | ||
gANDOperationMapSize % 1000, | ||
(gANDOperationMapSize * (uint32_t) (sizeof (uint32_t) + sizeof (uint64_t))) / 1000000) ; | ||
} | ||
} | ||
} | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
static void enterInANDOperationCache (const uint32_t inOperand1, | ||
const uint32_t inOperand2, | ||
const uint32_t inResult) { | ||
const uint64_t operands = getOperands (inOperand1, inOperand2) ; | ||
const uint64_t idx = operands % gANDOperationMapSize ; | ||
const bool entryWasUnused = gANDOperationCacheOperandMap [idx] == 0 ; | ||
gANDOperationCacheOperandMap [idx] = operands ; | ||
gANDOperationCacheResultMap [idx] = inResult ; | ||
//--- Realloc cache ? | ||
if (entryWasUnused) { | ||
gANDOperationCacheMapUsedEntryCount ++ ; | ||
if (gANDOperationCacheExpandable && | ||
((gANDOperationCacheMapUsedEntryCount + gANDOperationCacheMapUsedEntryCount / 4) > gANDOperationMapSize)) { | ||
const uint32_t newSize = getPrimeGreaterThan (gANDOperationMapSize + 1) ; | ||
if (newSize < (1U << gANDOperationCacheMaxPowerOfTwoSize)) { | ||
uint32_t newMemoryUsage = C_BDD::currentMemoryUsage () ; | ||
newMemoryUsage -= ANDCacheMemoryUsage () ; | ||
newMemoryUsage += (uint32_t) ((newSize * (sizeof (uint64_t) + sizeof (uint32_t))) / 1000000) ; | ||
if (newMemoryUsage < C_BDD::maximumMemoryUsage ()) { | ||
reallocANDOperationCache (newSize) ; | ||
}else{ | ||
gANDOperationCacheExpandable = false ; | ||
if (C_BDD::displaysInformationMessages ()) { | ||
printf ("BDD package info: AND cache reallocation to %u %03u %03u inhibited (max RAM usage reached)\n", | ||
newSize / 1000000, | ||
(newSize / 1000) % 1000, | ||
newSize % 1000) ; | ||
} | ||
} | ||
}else{ | ||
gANDOperationCacheExpandable = false ; | ||
if (C_BDD::displaysInformationMessages ()) { | ||
printf ("BDD package info: AND cache reallocation to %u %03u %03u inhibited (max size reached)\n", | ||
newSize / 1000000, | ||
(newSize / 1000) % 1000, | ||
newSize % 1000) ; | ||
} | ||
} | ||
} | ||
} | ||
} | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
void C_BDD::setANDOperationCacheMaxSize (const uint32_t inPowerOfTwo) { | ||
gANDOperationCacheMaxPowerOfTwoSize = inPowerOfTwo ; | ||
if (C_BDD::displaysInformationMessages ()) { | ||
printf ("BDD package info: AND cache max size limited < 2 ** %u\n", gANDOperationCacheMaxPowerOfTwoSize) ; | ||
} | ||
} | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
#ifdef PRAGMA_MARK_ALLOWED | ||
#pragma mark AND operation | ||
#endif | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- | ||
// | ||
// Operation AND | ||
// | ||
//---------------------------------------------------------------------------------------------------------------------- | ||
|
||
uint32_t internalANDoperation (const uint32_t opf, | ||
const uint32_t opg) { | ||
uint32_t result ; | ||
uint32_t f = opf ; | ||
uint32_t g = opg ; | ||
//--- Simplification 1 : si f > g, and (f, g) -> and (g, f) ; | ||
if (f > g) { | ||
const uint32_t tempo = g ; g = f ; f = tempo ; | ||
} | ||
//--- Test trivial 1 : and (0, g) -> 0 ; | ||
if (f == 0) { | ||
gANDOperationCacheTrivialOperationCount ++ ; | ||
result = 0 ; | ||
//--- Test trivial 2 : and (1, g) -> g ; | ||
}else if (f == 1) { | ||
gANDOperationCacheTrivialOperationCount ++ ; | ||
result = g ; | ||
//--- Test trivial 3 : and (f, f) -> f ; | ||
}else if (f == g) { | ||
gANDOperationCacheTrivialOperationCount ++ ; | ||
result = g ; | ||
//--- Test trivial 3 : and (f, ~f) -> 0 ; | ||
}else if ((f ^ g) == 1) { | ||
gANDOperationCacheTrivialOperationCount ++ ; | ||
result = 0 ; | ||
//--- Effectuer le calcul | ||
}else if (! searchInANDOperationCache (f, g, result)) { | ||
//--- Faire l'operation | ||
const uint32_t nodeF = nodeIndexForRoot (f COMMA_HERE) ; | ||
const uint32_t nodeG = nodeIndexForRoot (g COMMA_HERE) ; | ||
const uint32_t compF = f & 1 ; | ||
const uint32_t compG = g & 1 ; | ||
const uint32_t varF = gNodeArray [nodeF].mVariableIndex ; | ||
const uint32_t varG = gNodeArray [nodeG].mVariableIndex ; | ||
//--- Compute | ||
if (varF < varG) { | ||
result = find_or_add (varG, | ||
internalANDoperation (f, gNodeArray [nodeG].mELSE ^ compG), | ||
internalANDoperation (f, gNodeArray [nodeG].mTHEN ^ compG) COMMA_HERE) ; | ||
}else if (varF == varG) { | ||
result = find_or_add (varF, | ||
internalANDoperation (gNodeArray [nodeF].mELSE ^ compF, gNodeArray [nodeG].mELSE ^ compG), | ||
internalANDoperation (gNodeArray [nodeF].mTHEN ^ compF, gNodeArray [nodeG].mTHEN ^ compG) COMMA_HERE) ; | ||
}else{ // varF > varG | ||
result = find_or_add (varF, | ||
internalANDoperation (gNodeArray [nodeF].mELSE ^ compF, g), | ||
internalANDoperation (gNodeArray [nodeF].mTHEN ^ compF, g) COMMA_HERE) ; | ||
} | ||
//--- Insert result into cache | ||
enterInANDOperationCache (f, g, result) ; | ||
} | ||
return result ; | ||
} | ||
|
||
//---------------------------------------------------------------------------------------------------------------------- |
Oops, something went wrong.