diff --git a/packages/CLPBN/horus/LiftedCircuit.cpp b/packages/CLPBN/horus/LiftedCircuit.cpp index baa058170..06ebbae3e 100644 --- a/packages/CLPBN/horus/LiftedCircuit.cpp +++ b/packages/CLPBN/horus/LiftedCircuit.cpp @@ -217,23 +217,6 @@ LiftedCircuit::compile ( } -void -LiftedCircuit::propagate ( - const Clause& c, - const Clause& unitClause, - Clauses& newClauses) -{ -/* - Literals literals = c.literals(); - for (size_t i = 0; i < literals.size(); i++) { - if (literals_[i].lid() == lid && literals[i].isPositive()) { - - return true; - } - } -*/ -} - bool shatterCountedLogVars (Clauses& clauses, size_t idx1, size_t idx2) @@ -312,14 +295,12 @@ LiftedCircuit::tryUnitPropagation ( if (clauses[i].literals()[0].isPositive()) { if (clauses[j].containsPositiveLiteral (lid, types) == false) { Clause newClause = clauses[j]; - cout << "removing negative literals on " << newClause << endl; newClause.removeNegativeLiterals (lid, types); newClauses.push_back (newClause); } } else if (clauses[i].literals()[0].isNegative()) { if (clauses[j].containsNegativeLiteral (lid, types) == false) { Clause newClause = clauses[j]; - cout << "removing negative literals on " << newClause << endl; newClause.removePositiveLiterals (lid, types); newClauses.push_back (newClause); } @@ -330,7 +311,6 @@ LiftedCircuit::tryUnitPropagation ( explanation << " UP on" << clauses[i].literals()[0]; AndNode* andNode = new AndNode (clauses, explanation.str()); Clauses leftClauses = {clauses[i]}; - cout << "new clauses: " << newClauses << endl; compile (andNode->leftBranch(), leftClauses); compile (andNode->rightBranch(), newClauses); (*follow) = andNode; diff --git a/packages/CLPBN/horus/LiftedCircuit.h b/packages/CLPBN/horus/LiftedCircuit.h index a89821c84..060d66376 100644 --- a/packages/CLPBN/horus/LiftedCircuit.h +++ b/packages/CLPBN/horus/LiftedCircuit.h @@ -81,7 +81,7 @@ class AndNode : public CircuitNode double weight (void) const; - CircuitNode** leftBranch (void) { return &leftBranch_; } + CircuitNode** leftBranch (void) { return &leftBranch_; } CircuitNode** rightBranch (void) { return &rightBranch_; } private: CircuitNode* leftBranch_; @@ -128,12 +128,13 @@ class IncExcNode : public CircuitNode IncExcNode (const Clauses& clauses) : CircuitNode (clauses), plus1Branch_(0), plus2Branch_(0), minusBranch_(0) { } - + double weight (void) const; - + CircuitNode** plus1Branch (void) { return &plus1Branch_; } CircuitNode** plus2Branch (void) { return &plus2Branch_; } CircuitNode** minusBranch (void) { return &minusBranch_; } + private: CircuitNode* plus1Branch_; CircuitNode* plus2Branch_; @@ -172,7 +173,6 @@ class TrueNode : public CircuitNode - class CompilationFailedNode : public CircuitNode { public: diff --git a/packages/CLPBN/horus/LiftedWCNF.cpp b/packages/CLPBN/horus/LiftedWCNF.cpp index 29affb2ac..527035d08 100644 --- a/packages/CLPBN/horus/LiftedWCNF.cpp +++ b/packages/CLPBN/horus/LiftedWCNF.cpp @@ -159,41 +159,6 @@ Clause::removeNegativeLiterals ( -LogVarSet -Clause::ipgCandidates (void) const -{ - LogVarSet candidates; - LogVarSet allLvs = constr_.logVarSet(); - allLvs -= ipgLogVars_; - for (size_t i = 0; i < allLvs.size(); i++) { - bool valid = true; - for (size_t j = 0; j < literals_.size(); j++) { - if (Util::contains (literals_[j].logVars(), allLvs[i]) == false) { - valid = false; - break; - } - } - if (valid) { - candidates.insert (allLvs[i]); - } - } - return candidates; -} - - - -TinySet -Clause::lidSet (void) const -{ - TinySet lidSet; - for (size_t i = 0; i < literals_.size(); i++) { - lidSet.insert (literals_[i].lid()); - } - return lidSet; -} - - - bool Clause::isCountedLogVar (LogVar X) const { @@ -222,13 +187,37 @@ Clause::isNegativeCountedLogVar (LogVar X) const -void -Clause::removeLiteral (size_t idx) +TinySet +Clause::lidSet (void) const { - LogVarSet lvs (literals_[idx].logVars()); - lvs -= getLogVarSetExcluding (idx); - constr_.remove (lvs); - literals_.erase (literals_.begin() + idx); + TinySet lidSet; + for (size_t i = 0; i < literals_.size(); i++) { + lidSet.insert (literals_[i].lid()); + } + return lidSet; +} + + + +LogVarSet +Clause::ipgCandidates (void) const +{ + LogVarSet candidates; + LogVarSet allLvs = constr_.logVarSet(); + allLvs -= ipgLogVars_; + for (size_t i = 0; i < allLvs.size(); i++) { + bool valid = true; + for (size_t j = 0; j < literals_.size(); j++) { + if (Util::contains (literals_[j].logVars(), allLvs[i]) == false) { + valid = false; + break; + } + } + if (valid) { + candidates.insert (allLvs[i]); + } + } + return candidates; } @@ -252,6 +241,18 @@ Clause::logVarTypes (size_t litIdx) const +void +Clause::removeLiteral (size_t litIdx) +{ + // TODO maybe we need to clean up pos/neg/ipg lvs too + LogVarSet lvs (literals_[litIdx].logVars()); + lvs -= getLogVarSetExcluding (litIdx); + constr_.remove (lvs); + literals_.erase (literals_.begin() + litIdx); +} + + + void Clause::printClauses (const Clauses& clauses) { @@ -262,20 +263,6 @@ Clause::printClauses (const Clauses& clauses) -LogVarSet -Clause::getLogVarSetExcluding (size_t idx) const -{ - LogVarSet lvs; - for (size_t i = 0; i < literals_.size(); i++) { - if (i != idx) { - lvs |= literals_[i].logVars(); - } - } - return lvs; -} - - - std::ostream& operator<< (ostream &os, const Clause& clause) { for (unsigned i = 0; i < clause.literals_.size(); i++) { @@ -293,6 +280,20 @@ std::ostream& operator<< (ostream &os, const Clause& clause) +LogVarSet +Clause::getLogVarSetExcluding (size_t idx) const +{ + LogVarSet lvs; + for (size_t i = 0; i < literals_.size(); i++) { + if (i != idx) { + lvs |= literals_[i].logVars(); + } + } + return lvs; +} + + + LiftedWCNF::LiftedWCNF (const ParfactorList& pfList) : pfList_(pfList), freeLiteralId_(0) { diff --git a/packages/CLPBN/horus/LiftedWCNF.h b/packages/CLPBN/horus/LiftedWCNF.h index 079c07a11..260de8170 100644 --- a/packages/CLPBN/horus/LiftedWCNF.h +++ b/packages/CLPBN/horus/LiftedWCNF.h @@ -65,71 +65,70 @@ class Literal typedef vector Literals; + class Clause { public: Clause (const ConstraintTree& ct) : constr_(ct) { } - + Clause (vector> names) : constr_(ConstraintTree (names)) { } - + void addLiteral (const Literal& l) { literals_.push_back (l); } - + + // TODO kill me void addAndNegateLiteral (const Literal& l) { literals_.push_back (l); literals_.back().negate(); } - bool containsLiteral (LiteralId lid) const; - - bool containsPositiveLiteral (LiteralId lid, const LogVarTypes&) const; - - bool containsNegativeLiteral (LiteralId lid, const LogVarTypes&) const; - - void removeLiterals (LiteralId lid); - - void removePositiveLiterals (LiteralId lid, const LogVarTypes&); - - void removeNegativeLiterals (LiteralId lid, const LogVarTypes&); - const vector& literals (void) const { return literals_; } - - void removeLiteralByIndex (size_t idx) { literals_.erase (literals_.begin() + idx); } - + const ConstraintTree& constr (void) const { return constr_; } - + ConstraintTree constr (void) { return constr_; } - + bool isUnit (void) const { return literals_.size() == 1; } - + LogVarSet ipgLogVars (void) const { return ipgLogVars_; } - + void addIpgLogVar (LogVar X) { ipgLogVars_.insert (X); } - + void addPositiveCountedLogVar (LogVar X) { posCountedLvs_.insert (X); } void addNegativeCountedLogVar (LogVar X) { negCountedLvs_.insert (X); } - - LogVarSet ipgCandidates (void) const; + + bool containsLiteral (LiteralId lid) const; + + bool containsPositiveLiteral (LiteralId lid, const LogVarTypes&) const; + + bool containsNegativeLiteral (LiteralId lid, const LogVarTypes&) const; + + void removeLiterals (LiteralId lid); + + void removePositiveLiterals (LiteralId lid, const LogVarTypes&); + + void removeNegativeLiterals (LiteralId lid, const LogVarTypes&); + + bool isCountedLogVar (LogVar X) const; + + bool isPositiveCountedLogVar (LogVar X) const; + + bool isNegativeCountedLogVar (LogVar X) const; TinySet lidSet (void) const; + + LogVarSet ipgCandidates (void) const; + + LogVarTypes logVarTypes (size_t litIdx) const; - bool isCountedLogVar (LogVar X) const; - - bool isPositiveCountedLogVar (LogVar X) const; - - bool isNegativeCountedLogVar (LogVar X) const; + void removeLiteral (size_t litIdx); + + static void printClauses (const vector& clauses); friend std::ostream& operator<< (ostream &os, const Clause& clause); - void removeLiteral (size_t idx); - - LogVarTypes logVarTypes (size_t litIdx) const; - - static void printClauses (const vector& clauses); - private: - LogVarSet getLogVarSetExcluding (size_t idx) const; vector literals_; @@ -139,8 +138,6 @@ class Clause ConstraintTree constr_; }; - - typedef vector Clauses;