Ignore:
Timestamp:
Jul 7, 2015, 4:11:50 PM (4 years ago)
Author:
nmedfort
Message:

Fixed Multiplexing for new While structure/logic + Potential bug fix for PabloBuilder::Create.

Location:
icGREP/icgrep-devel/icgrep/pablo
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • icGREP/icgrep-devel/icgrep/pablo/builder.hpp

    r4641 r4646  
    1010public:
    1111
    12     explicit PabloBuilder(PabloBlock & block) : mPb(&block), mParent(nullptr) {}
     12    explicit PabloBuilder(PabloBlock & block) : mPb(&block), mParent(nullptr), mExprTable(nullptr) {}
    1313
    1414    explicit PabloBuilder(PabloBlock & block, PabloBuilder & parent) : mPb(&block), mParent(&parent), mExprTable(&(parent.mExprTable)) {}
    1515
    16     PabloBuilder(const PabloBuilder &) = default;
     16    PabloBuilder(PabloBuilder && builder) : mPb(builder.mPb), mParent(builder.mParent), mExprTable(std::move(builder.mExprTable)) {}
     17
     18    PabloBuilder & operator=(PabloBuilder) = delete;
    1719
    1820    PabloBuilder & operator=(PabloBuilder &) = delete;
    1921
    20     PabloBuilder & operator=(PabloBuilder &&) = default;
     22    PabloBuilder & operator=(PabloBuilder && builder) {
     23        mPb = builder.mPb;
     24        mParent = builder.mParent;
     25        mExprTable = std::move(builder.mExprTable);
     26        return *this;
     27    }
    2128
    22     inline static PabloBuilder && Create(PabloBuilder & parent) noexcept {
     29    inline static PabloBuilder Create(PabloBuilder & parent) noexcept {
    2330        return std::move(PabloBuilder(PabloBlock::Create(*(parent.mPb)), parent));
    2431    }
  • icGREP/icgrep-devel/icgrep/pablo/expression_map.hpp

    r4641 r4646  
    1313    typedef ExpressionMap<Args...> Type;
    1414    typedef std::tuple<PabloAST::ClassTypeId, Args...> Key;
     15    friend struct ExpressionTable;
    1516
    16     inline explicit ExpressionMap(Type * predecessor) : mPredecessor(predecessor) { }
     17    explicit ExpressionMap(Type * predecessor = nullptr) : mPredecessor(predecessor) { }
    1718
    18     ExpressionMap(const Type &) = default;
     19    explicit ExpressionMap(Type && other) noexcept
     20    : mPredecessor(other.mPredecessor)
     21    , mMap(std::move(other.mMap)) {
    1922
    20     ExpressionMap(Type &&) = default;
     23    }
     24
     25    ExpressionMap & operator=(Type && other) {
     26        mPredecessor = other.mPredecessor;
     27        mMap = std::move(other.mMap);
     28        return *this;
     29    }
    2130
    2231    template <class Functor, typename... Params>
     
    7988
    8089private:
    81     Type *                      mPredecessor;
     90    const Type *                mPredecessor;
    8291    std::map<Key, PabloAST *>   mMap;
    8392};
     
    8695struct ExpressionTable {
    8796
    88     ExpressionTable() noexcept
    89     : mUnary(nullptr)
    90     , mBinary(nullptr)
    91     , mTernary(nullptr) {
     97    explicit ExpressionTable(const ExpressionTable * predecessor = nullptr) noexcept {
     98        if (predecessor) {
     99            mUnary.mPredecessor = &(predecessor->mUnary);
     100            mBinary.mPredecessor = &(predecessor->mBinary);
     101            mTernary.mPredecessor = &(predecessor->mTernary);
     102        }
     103    }
     104
     105    explicit ExpressionTable(ExpressionTable & other) = delete;
     106
     107    explicit ExpressionTable(ExpressionTable && other) noexcept
     108    : mUnary(std::move(other.mUnary))
     109    , mBinary(std::move(other.mBinary))
     110    , mTernary(std::move(other.mTernary)) {
    92111
    93112    }
    94113
    95     explicit ExpressionTable(ExpressionTable * predecessor) noexcept
    96     : mUnary(predecessor ? &(predecessor->mUnary) : nullptr)
    97     , mBinary(predecessor ? &(predecessor->mBinary) : nullptr)
    98     , mTernary(predecessor ? &(predecessor->mTernary) : nullptr) {
    99 
     114    ExpressionTable & operator=(ExpressionTable && other) {
     115        mUnary = std::move(other.mUnary);
     116        mBinary = std::move(other.mBinary);
     117        mTernary = std::move(other.mTernary);
     118        return *this;
    100119    }
    101120
    102     ExpressionTable(const ExpressionTable &) = default;
    103 
    104     ExpressionTable(ExpressionTable &&) = default;
    105121
    106122    template <class Functor, typename... Params>
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_automultiplexing.cpp

    r4641 r4646  
    306306 * Scan through the program and iteratively compute the BDDs for each statement.
    307307 ** ------------------------------------------------------------------------------------------------------------- */
    308 void AutoMultiplexing::characterize(PabloBlock & block) {
     308void AutoMultiplexing::characterize(PabloBlock &block) {
    309309    for (Statement * stmt : block) {
    310310        if (LLVM_UNLIKELY(isa<If>(stmt) || isa<While>(stmt))) {
    311             // Set the next statement to be the first statement of the inner scope and push the
    312             // next statement of the current statement into the scope stack.
     311            const auto start = mRecentCharacterizations.size();
    313312            characterize(isa<If>(stmt) ? cast<If>(stmt)->getBody() : cast<While>(stmt)->getBody());
     313            assert (mRecentCharacterizations.size() >= start);
     314            if (isa<If>(stmt)) {
     315                const auto & defined = cast<const If>(stmt)->getDefined();
     316                for (auto pair = mRecentCharacterizations.begin() + start; pair != mRecentCharacterizations.end(); ++pair) {
     317                    const PabloAST * expr = nullptr;
     318                    DdNode * bdd = nullptr;
     319                    std::tie(expr, bdd) = *pair;
     320                    if (LLVM_UNLIKELY(isa<Assign>(expr))) {
     321                        if (LLVM_LIKELY(std::find(defined.begin(), defined.end(), expr) != defined.end())) {
     322                            continue;
     323                        }
     324                    }
     325                    mCharacterizationMap.erase(mCharacterizationMap.find(expr));
     326                    if (LLVM_UNLIKELY(Cudd_IsConstant(bdd))) {
     327                        continue;
     328                    }
     329                    Deref(bdd);
     330                }
     331            }
     332            else { // if isa<While>(stmt)
     333                const auto & variants = cast<const While>(stmt)->getVariants();
     334                for (auto pair = mRecentCharacterizations.begin() + start; pair != mRecentCharacterizations.end(); ++pair) {
     335                    const PabloAST * expr = nullptr;
     336                    DdNode * bdd = nullptr;
     337                    std::tie(expr, bdd) = *pair;
     338                    if (LLVM_UNLIKELY(isa<Next>(expr))) {
     339                        if (LLVM_LIKELY(std::find(variants.begin(), variants.end(), expr) != variants.end())) {
     340                            DdNode *& next = mCharacterizationMap[expr];
     341                            next = Or(next, bdd);
     342                            Ref(next);
     343                            continue;
     344                        }
     345                    }
     346                    mCharacterizationMap.erase(mCharacterizationMap.find(expr));
     347                    if (LLVM_UNLIKELY(Cudd_IsConstant(bdd))) {
     348                        continue;
     349                    }
     350                    Deref(bdd);
     351                }
     352            }
     353
     354            assert (Cudd_DebugCheck(mManager) == 0);
     355
     356            mRecentCharacterizations.erase(mRecentCharacterizations.begin() + start, mRecentCharacterizations.end());
    314357            continue;
    315358        }
    316         mCharacterizationMap[stmt] = characterize(stmt);
     359
     360        DdNode * var = characterize(stmt);
     361        mCharacterizationMap[stmt] = var;
     362        assert (Cudd_DebugCheck(mManager) == 0);
    317363    }
    318364}
     
    326372    // Map our operands to the computed BDDs
    327373    std::array<DdNode *, 3> input;
    328     for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
    329         PabloAST * const op = stmt->getOperand(i);
     374    unsigned count = 0;
     375    for (; count != stmt->getNumOperands(); ++count) {
     376        PabloAST * const op = stmt->getOperand(count);
    330377        if (LLVM_UNLIKELY(isa<Integer>(op) || isa<String>(op))) {
    331378            continue;
     
    335382            std::string tmp;
    336383            llvm::raw_string_ostream msg(tmp);
    337             msg << "Uncharacterized operand " << std::to_string(i);
     384            msg << "Uncharacterized operand " << std::to_string(count);
    338385            PabloPrinter::print(stmt, " of ", msg);
    339386            throw std::runtime_error(msg.str());
    340387        }
    341         input[i] = f->second;
     388        input[count] = f->second;
    342389    }
    343390
    344391    switch (stmt->getClassTypeId()) {
    345392        case PabloAST::ClassTypeId::Assign:
    346             return input[0];
     393        case PabloAST::ClassTypeId::Next:
     394            bdd = input[0];
     395            break;
    347396        case PabloAST::ClassTypeId::And:
    348397            bdd = And(input[0], input[1]);
     398            break;       
     399        case PabloAST::ClassTypeId::Or:
     400            bdd = Or(input[0], input[1]);
    349401            break;
    350         case PabloAST::ClassTypeId::Next:
    351         case PabloAST::ClassTypeId::Or:
    352             return Or(input[0], input[1]);
    353402        case PabloAST::ClassTypeId::Xor:
    354             return Xor(input[0], input[1]);
     403            bdd = Xor(input[0], input[1]);
     404            break;
    355405        case PabloAST::ClassTypeId::Not:
    356             return Not(input[0]);
     406            bdd = Not(input[0]);
     407            break;
    357408        case PabloAST::ClassTypeId::Sel:
    358409            bdd = Ite(input[0], input[1], input[2]);
     
    367418            }
    368419        case PabloAST::ClassTypeId::Call:
    369             return NewVar();
     420            bdd = NewVar();
     421            mRecentCharacterizations.emplace_back(stmt, bdd);
     422            return bdd;
    370423        case PabloAST::ClassTypeId::Advance:
     424            // This returns so that it doesn't mistakeningly replace the Advance with 0 or add it
     425            // to the list of recent characterizations.
    371426            return characterize(cast<Advance>(stmt), input[0]);
    372427        default:
     
    374429    }
    375430
     431
     432    Ref(bdd);
     433
     434    if (LLVM_UNLIKELY(NoSatisfyingAssignment(bdd))) {
     435        Deref(bdd);
     436        // If there is no satisfing assignment for this bdd, the statement will always produce
     437        // 0. If this is an Assign or Next node, replace the value with 0. Otherwise replace
     438        // the statement with 0.
     439        if (LLVM_UNLIKELY(isa<Assign>(stmt) || isa<Next>(stmt))) {
     440            stmt->setOperand(0, stmt->getParent()->createZeroes());
     441        }
     442        else {
     443            stmt->replaceWith(stmt->getParent()->createZeroes());
     444        }
     445        return Zero();
     446    }
     447
     448    mRecentCharacterizations.emplace_back(stmt, bdd);
    376449    return bdd;
    377450}
     
    380453 * @brief characterize
    381454 ** ------------------------------------------------------------------------------------------------------------- */
    382 inline DdNode * AutoMultiplexing::characterize(Advance * adv, DdNode * input) {
     455inline DdNode * AutoMultiplexing::characterize(Advance *adv, DdNode * input) {
    383456    DdNode * Ik, * Ck, * Nk;
    384457    if (LLVM_UNLIKELY(isZero(input))) {
     
    388461
    389462        Ik = input;
     463        Ref(input);
    390464        Ck = NewVar();
    391465        Nk = Not(Ck);
     
    405479            if ((adv->getOperand(1) == tmp->getOperand(1)) && (notTransitivelyDependant(i, k))) {
    406480                DdNode * Ii = std::get<1>(mAdvance[i]);
    407                 DdNode * Ni = std::get<2>(mAdvance[i]);
    408481                DdNode * const IiIk = And(Ik, Ii);
     482                Ref(IiIk);
    409483                // Is there any satisfying truth assignment? If not, these streams are mutually exclusive.
    410484                if (NoSatisfyingAssignment(IiIk)) {
     
    412486                    DdNode *& Ci = mCharacterizationMap[tmp];
    413487                    // Mark the i-th and k-th Advances as being mutually exclusive
    414                     Ck = And(Ck, Ni);
    415                     Ci = And(Ci, Nk);
     488                    DdNode * Ni = std::get<2>(mAdvance[i]);
     489                    Ck = And(Ck, Ni); Ref(Ck);
     490                    Ci = And(Ci, Nk); Ref(Ci);
    416491                    // If Ai ∩ Ak = âˆ
    417492 and Aj ⊂ Ai, Aj ∩ Ak = âˆ
     
    426501                            DdNode * Nj = std::get<2>(mAdvance[j]);
    427502                            // Mark the i-th and j-th Advances as being mutually exclusive
    428                             Ck = And(Ck, Nj);
    429                             Cj = And(Cj, Nk);
     503                            Ck = And(Ck, Nj); Ref(Ck);
     504                            Cj = And(Cj, Nk); Ref(Cj);
    430505                            unconstrained[j] = true;
    431506                        }
     
    459534                    unconstrained[i] = true;
    460535                }
    461                 Cudd_RecursiveDeref(mManager, IiIk);
     536                Deref(IiIk);
    462537            }
    463538        }
     
    475550
    476551    mAdvance.emplace_back(adv, Ik, Nk);
    477 
     552    Ref(Ck);
    478553    return Ck;
    479554}
     
    500575
    501576inline DdNode * AutoMultiplexing::NewVar() {
    502     return Cudd_bddIthVar(mManager, mVariables++);
     577    DdNode * var = Cudd_bddIthVar(mManager, mVariables++);
     578    return var;
    503579}
    504580
     
    508584
    509585inline DdNode * AutoMultiplexing::And(DdNode * const x, DdNode * const y) {
    510     DdNode * r = Cudd_bddAnd(mManager, x, y);
    511     Cudd_Ref(r);
    512     return r;
     586    DdNode * var = Cudd_bddAnd(mManager, x, y);
     587    return var;
    513588}
    514589
    515590inline DdNode * AutoMultiplexing::Or(DdNode * const x, DdNode * const y) {
    516     DdNode * r = Cudd_bddOr(mManager, x, y);
    517     Cudd_Ref(r);
    518     return r;
     591    DdNode * var = Cudd_bddOr(mManager, x, y);
     592    return var;
    519593}
    520594
    521595inline DdNode * AutoMultiplexing::Xor(DdNode * const x, DdNode * const y) {
    522     DdNode * r = Cudd_bddXor(mManager, x, y);
    523     Cudd_Ref(r);
    524     return r;
     596    DdNode * var = Cudd_bddXor(mManager, x, y);
     597    return var;
    525598}
    526599
    527600inline DdNode * AutoMultiplexing::Not(DdNode * const x) const {
    528     return Cudd_Not(x);
     601    DdNode * var = Cudd_Not(x);
     602    return var;
    529603}
    530604
    531605inline DdNode * AutoMultiplexing::Ite(DdNode * const x, DdNode * const y, DdNode * const z) {
    532     DdNode * r = Cudd_bddIte(mManager, x, y, z);
    533     Cudd_Ref(r);
    534     return r;
     606    DdNode * var = Cudd_bddIte(mManager, x, y, z);
     607    return var;
    535608}
    536609
    537610inline bool AutoMultiplexing::NoSatisfyingAssignment(DdNode * const x) {
    538611    return Cudd_bddLeq(mManager, x, Zero());
     612}
     613
     614inline void AutoMultiplexing::Ref(DdNode * const x) {
     615    assert (x);
     616    Cudd_Ref(x);
     617}
     618
     619inline void AutoMultiplexing::Deref(DdNode * const x) {
     620    assert (x);
     621    Cudd_RecursiveDeref(mManager, x);
    539622}
    540623
     
    859942
    860943                    // Gather the original users to this advance. We'll be manipulating it shortly.
    861                     Statement::Users U(adv->users());
     944                    std::vector<PabloAST *> U(adv->users().begin(), adv->users().end());
    862945
    863946                    // Add s to V and sort the list; it'll be closer to being in topological order.
     
    9991082                input[i - 1]->replaceWith(demuxed, true, true);
    10001083            }
    1001 
    1002             simplify(muxed, m, builder);
    1003         }
    1004     }
    1005 }
    1006 
    1007 
    1008 
    1009 /** ------------------------------------------------------------------------------------------------------------- *
    1010  * @brief simplify
    1011  ** ------------------------------------------------------------------------------------------------------------- */
    1012 void AutoMultiplexing::simplify(const std::vector<PabloAST *> & variables, const unsigned n, PabloBuilder & builder) const {
    1013 
    1014     std::queue<PabloAST *> Q;
    1015     llvm::DenseMap<PabloAST *, DdNode *> characterization;
    1016     flat_set<PabloAST *> uncharacterized;
    1017 
    1018     DdManager * manager = Cudd_Init(n + mBaseVariables.size(), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
    1019     Cudd_AutodynDisable(manager);
    1020 
    1021     unsigned i = 0;
    1022     for (; i != n; ++i) {
    1023         PabloAST * const var = variables[i];
    1024         Q.push(var);
    1025         characterization[var] = Cudd_bddIthVar(manager, i);
    1026     }
    1027 
    1028     for (Var * var : mBaseVariables) {
    1029         characterization[var] = Cudd_bddIthVar(manager, i++);
    1030     }
    1031 
    1032     std::array<DdNode *, 3> input;
    1033 
    1034     while (!Q.empty()) {
    1035         PabloAST * const var = Q.front(); Q.pop();
    1036         for (PabloAST * user : var->users()) {
    1037             Statement * stmt = nullptr;
    1038             // If this user is a boolean operation ...
    1039             switch (user->getClassTypeId()) {
    1040                 case PabloAST::ClassTypeId::And:
    1041                 case PabloAST::ClassTypeId::Or:
    1042                 case PabloAST::ClassTypeId::Not:
    1043                 case PabloAST::ClassTypeId::Xor:
    1044                 case PabloAST::ClassTypeId::Sel:
    1045                     // And it is within the same scope ...
    1046                     if ((stmt = cast<Statement>(user))->getParent() == builder.getPabloBlock()) {
    1047                         bool characterized = true;
    1048                         for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
    1049                             auto f = characterization.find(stmt->getOperand(i));
    1050                             if (f == characterization.end()) {
    1051                                 characterized = false;
    1052                                 break;
    1053                             }
    1054                             input[i] = f->second;
    1055                         }
    1056                         // And every input operand is characterizied ...
    1057                         if (characterized) {
    1058                             DdNode * bdd = nullptr;
    1059                             switch (user->getClassTypeId()) {
    1060                                 case PabloAST::ClassTypeId::And:
    1061                                     bdd = Cudd_bddAnd(manager, input[0], input[1]);
    1062                                     break;
    1063                                 case PabloAST::ClassTypeId::Or:
    1064                                     bdd = Cudd_bddOr(manager, input[0], input[1]);
    1065                                     break;
    1066                                 case PabloAST::ClassTypeId::Not:
    1067                                     bdd = Cudd_Not(input[0]);
    1068                                     break;
    1069                                 case PabloAST::ClassTypeId::Xor:
    1070                                     bdd = Cudd_bddXor(manager, input[0], input[1]);
    1071                                     break;
    1072                                 case PabloAST::ClassTypeId::Sel:
    1073                                     bdd = Cudd_bddIte(manager, input[0], input[1], input[2]);
    1074                                     break;
    1075                                 default: __builtin_unreachable();
    1076                             }
    1077                             characterization[stmt] = bdd;
    1078                             uncharacterized.erase(stmt);
    1079                             for (PabloAST * next : stmt->users()) {
    1080                                 if (characterization.count(next) == 0) {
    1081                                     Q.push(next);
    1082                                 }
    1083                             }
    1084                             break;
    1085                         }
    1086                     }
    1087                 default:
    1088                     // Otherwise we probably apply Quine McCluskey to one of this statements operands
    1089                     // presuming they aren't characterized properly later.
    1090                     uncharacterized.insert(user);
    1091                     break;
    1092             }
    1093         }
    1094     }
    1095     // Gether up the output statements from the characterized inputs of the uncharacterized statements
    1096     llvm::DenseMap<PabloAST *, DdNode *> outputs;
    1097     for (PabloAST * var : uncharacterized) {
    1098         Statement * stmt = cast<Statement>(var);
    1099         for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
    1100             auto f = characterization.find(stmt->getOperand(i));
    1101             if (f != characterization.end()) {
    1102                 outputs.insert(std::make_pair(f->first, f->second));
    1103             }
    1104         }
    1105     }
    1106 
    1107     circular_buffer<PabloAST *> S(n);
    1108 
    1109     CUDD_VALUE_TYPE value;
    1110     int * cube = nullptr;
    1111     for (auto itr : outputs) {
    1112 
    1113         // Look into doing some more analysis here to see if a Xor or Sel operation is possible.
    1114         DdGen * gen = Cudd_FirstCube(manager, itr.second, &cube, &value);
    1115         while (!Cudd_IsGenEmpty(gen)) {
    1116             // cube[0 ... n - 1] = {{ 0 : false, 1: true, 2: don't care }}
    1117             for (unsigned i = 0; i != n; ++i) {
    1118                 if (cube[i] == 0) {
    1119                     S.push_back(variables[i]);
    1120                 }
    1121             }
    1122 
    1123             if (S.size() > 0) {
    1124                 while(S.size() > 1) {
    1125                     PabloAST * A = S.front(); S.pop_front();
    1126                     PabloAST * B = S.front(); S.pop_front();
    1127                     S.push_back(builder.createOr(A, B));
    1128                 }
    1129                 PabloAST * C = S.front(); S.pop_front();
    1130                 S.push_back(builder.createNot(C));
    1131             }
    1132 
    1133             for (unsigned i = 0; i != n; ++i) {
    1134                 if (cube[i] == 1) {
    1135                     S.push_back(variables[i]);
    1136                 }
    1137             }
    1138 
    1139             while(S.size() > 1) {
    1140                 PabloAST * A = S.front(); S.pop_front();
    1141                 PabloAST * B = S.front(); S.pop_front();
    1142                 S.push_back(builder.createAnd(A, B));
    1143             }
    1144 
    1145             Q.push(S.front()); S.pop_front();
    1146 
    1147             Cudd_NextCube(gen, &cube, &value);
    1148         }
    1149         Cudd_GenFree(gen);
    1150 
    1151         while (Q.size() > 1) {
    1152             PabloAST * A = Q.front(); Q.pop();
    1153             PabloAST * B = Q.front(); Q.pop();
    1154             Q.push(builder.createOr(A, B));
    1155         }
    1156 
    1157         Statement * stmt = cast<Statement>(itr.first);
    1158         stmt->replaceWith(Q.front(), true, true);
    1159         Q.pop();
    1160     }
    1161     Cudd_Quit(manager);
    1162 
    1163 
    1164 }
    1165 
    1166 
     1084        }
     1085    }
     1086}
    11671087
    11681088/** ------------------------------------------------------------------------------------------------------------- *
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_automultiplexing.hpp

    r4639 r4646  
    3434    using AdvanceVector = std::vector<std::tuple<Advance *, DdNode *, DdNode *>>;
    3535    using IndependentSet = std::vector<ConstraintVertex>;
     36    using RecentCharacterizations = std::vector<std::pair<const PabloAST *, DdNode *>>;
    3637
    3738public:
     
    3940protected:
    4041    void initialize(PabloBlock & entry);
    41     void characterize(PabloBlock & block);
     42    void characterize(PabloBlock &block);
    4243    DdNode * characterize(Statement * const stmt);
    4344    DdNode * characterize(Advance * adv, DdNode * input);
     
    4849    void applySubsetConstraints();
    4950    void multiplexSelectedIndependentSets() const;
    50     void simplify(const std::vector<PabloAST *> & variables, const unsigned n, PabloBuilder & block) const;
    5151    void topologicalSort(PabloBlock & entry) const;
    5252    inline AutoMultiplexing(const std::vector<Var *> & vars)
     
    6767    DdNode * Ite(DdNode * const x, DdNode * const y, DdNode * const z);
    6868    DdNode * NewVar();
     69    void Ref(DdNode * const x);
     70    void Deref(DdNode * const x);
    6971    bool NoSatisfyingAssignment(DdNode * const x);
    7072    void Shutdown();
     
    8082    MultiplexSetGraph           mMultiplexSetGraph;
    8183    const std::vector<Var *> &  mBaseVariables;
     84    RecentCharacterizations     mRecentCharacterizations;
    8285};
    8386
Note: See TracChangeset for help on using the changeset viewer.