clean up
This commit is contained in:
parent
6877be897e
commit
bfa9648067
@ -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
|
bool
|
||||||
shatterCountedLogVars (Clauses& clauses, size_t idx1, size_t idx2)
|
shatterCountedLogVars (Clauses& clauses, size_t idx1, size_t idx2)
|
||||||
@ -312,14 +295,12 @@ LiftedCircuit::tryUnitPropagation (
|
|||||||
if (clauses[i].literals()[0].isPositive()) {
|
if (clauses[i].literals()[0].isPositive()) {
|
||||||
if (clauses[j].containsPositiveLiteral (lid, types) == false) {
|
if (clauses[j].containsPositiveLiteral (lid, types) == false) {
|
||||||
Clause newClause = clauses[j];
|
Clause newClause = clauses[j];
|
||||||
cout << "removing negative literals on " << newClause << endl;
|
|
||||||
newClause.removeNegativeLiterals (lid, types);
|
newClause.removeNegativeLiterals (lid, types);
|
||||||
newClauses.push_back (newClause);
|
newClauses.push_back (newClause);
|
||||||
}
|
}
|
||||||
} else if (clauses[i].literals()[0].isNegative()) {
|
} else if (clauses[i].literals()[0].isNegative()) {
|
||||||
if (clauses[j].containsNegativeLiteral (lid, types) == false) {
|
if (clauses[j].containsNegativeLiteral (lid, types) == false) {
|
||||||
Clause newClause = clauses[j];
|
Clause newClause = clauses[j];
|
||||||
cout << "removing negative literals on " << newClause << endl;
|
|
||||||
newClause.removePositiveLiterals (lid, types);
|
newClause.removePositiveLiterals (lid, types);
|
||||||
newClauses.push_back (newClause);
|
newClauses.push_back (newClause);
|
||||||
}
|
}
|
||||||
@ -330,7 +311,6 @@ LiftedCircuit::tryUnitPropagation (
|
|||||||
explanation << " UP on" << clauses[i].literals()[0];
|
explanation << " UP on" << clauses[i].literals()[0];
|
||||||
AndNode* andNode = new AndNode (clauses, explanation.str());
|
AndNode* andNode = new AndNode (clauses, explanation.str());
|
||||||
Clauses leftClauses = {clauses[i]};
|
Clauses leftClauses = {clauses[i]};
|
||||||
cout << "new clauses: " << newClauses << endl;
|
|
||||||
compile (andNode->leftBranch(), leftClauses);
|
compile (andNode->leftBranch(), leftClauses);
|
||||||
compile (andNode->rightBranch(), newClauses);
|
compile (andNode->rightBranch(), newClauses);
|
||||||
(*follow) = andNode;
|
(*follow) = andNode;
|
||||||
|
@ -81,7 +81,7 @@ class AndNode : public CircuitNode
|
|||||||
|
|
||||||
double weight (void) const;
|
double weight (void) const;
|
||||||
|
|
||||||
CircuitNode** leftBranch (void) { return &leftBranch_; }
|
CircuitNode** leftBranch (void) { return &leftBranch_; }
|
||||||
CircuitNode** rightBranch (void) { return &rightBranch_; }
|
CircuitNode** rightBranch (void) { return &rightBranch_; }
|
||||||
private:
|
private:
|
||||||
CircuitNode* leftBranch_;
|
CircuitNode* leftBranch_;
|
||||||
@ -134,6 +134,7 @@ class IncExcNode : public CircuitNode
|
|||||||
CircuitNode** plus1Branch (void) { return &plus1Branch_; }
|
CircuitNode** plus1Branch (void) { return &plus1Branch_; }
|
||||||
CircuitNode** plus2Branch (void) { return &plus2Branch_; }
|
CircuitNode** plus2Branch (void) { return &plus2Branch_; }
|
||||||
CircuitNode** minusBranch (void) { return &minusBranch_; }
|
CircuitNode** minusBranch (void) { return &minusBranch_; }
|
||||||
|
|
||||||
private:
|
private:
|
||||||
CircuitNode* plus1Branch_;
|
CircuitNode* plus1Branch_;
|
||||||
CircuitNode* plus2Branch_;
|
CircuitNode* plus2Branch_;
|
||||||
@ -172,7 +173,6 @@ class TrueNode : public CircuitNode
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
class CompilationFailedNode : public CircuitNode
|
class CompilationFailedNode : public CircuitNode
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
|
@ -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<LiteralId>
|
|
||||||
Clause::lidSet (void) const
|
|
||||||
{
|
|
||||||
TinySet<LiteralId> lidSet;
|
|
||||||
for (size_t i = 0; i < literals_.size(); i++) {
|
|
||||||
lidSet.insert (literals_[i].lid());
|
|
||||||
}
|
|
||||||
return lidSet;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
bool
|
bool
|
||||||
Clause::isCountedLogVar (LogVar X) const
|
Clause::isCountedLogVar (LogVar X) const
|
||||||
{
|
{
|
||||||
@ -222,13 +187,37 @@ Clause::isNegativeCountedLogVar (LogVar X) const
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
void
|
TinySet<LiteralId>
|
||||||
Clause::removeLiteral (size_t idx)
|
Clause::lidSet (void) const
|
||||||
{
|
{
|
||||||
LogVarSet lvs (literals_[idx].logVars());
|
TinySet<LiteralId> lidSet;
|
||||||
lvs -= getLogVarSetExcluding (idx);
|
for (size_t i = 0; i < literals_.size(); i++) {
|
||||||
constr_.remove (lvs);
|
lidSet.insert (literals_[i].lid());
|
||||||
literals_.erase (literals_.begin() + idx);
|
}
|
||||||
|
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
|
void
|
||||||
Clause::printClauses (const Clauses& clauses)
|
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)
|
std::ostream& operator<< (ostream &os, const Clause& clause)
|
||||||
{
|
{
|
||||||
for (unsigned i = 0; i < clause.literals_.size(); i++) {
|
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)
|
LiftedWCNF::LiftedWCNF (const ParfactorList& pfList)
|
||||||
: pfList_(pfList), freeLiteralId_(0)
|
: pfList_(pfList), freeLiteralId_(0)
|
||||||
{
|
{
|
||||||
|
@ -65,6 +65,7 @@ class Literal
|
|||||||
typedef vector<Literal> Literals;
|
typedef vector<Literal> Literals;
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
class Clause
|
class Clause
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
@ -74,28 +75,15 @@ class Clause
|
|||||||
|
|
||||||
void addLiteral (const Literal& l) { literals_.push_back (l); }
|
void addLiteral (const Literal& l) { literals_.push_back (l); }
|
||||||
|
|
||||||
|
// TODO kill me
|
||||||
void addAndNegateLiteral (const Literal& l)
|
void addAndNegateLiteral (const Literal& l)
|
||||||
{
|
{
|
||||||
literals_.push_back (l);
|
literals_.push_back (l);
|
||||||
literals_.back().negate();
|
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<Literal>& literals (void) const { return literals_; }
|
const vector<Literal>& literals (void) const { return literals_; }
|
||||||
|
|
||||||
void removeLiteralByIndex (size_t idx) { literals_.erase (literals_.begin() + idx); }
|
|
||||||
|
|
||||||
const ConstraintTree& constr (void) const { return constr_; }
|
const ConstraintTree& constr (void) const { return constr_; }
|
||||||
|
|
||||||
ConstraintTree constr (void) { return constr_; }
|
ConstraintTree constr (void) { return constr_; }
|
||||||
@ -110,9 +98,17 @@ class Clause
|
|||||||
|
|
||||||
void addNegativeCountedLogVar (LogVar X) { negCountedLvs_.insert (X); }
|
void addNegativeCountedLogVar (LogVar X) { negCountedLvs_.insert (X); }
|
||||||
|
|
||||||
LogVarSet ipgCandidates (void) const;
|
bool containsLiteral (LiteralId lid) const;
|
||||||
|
|
||||||
TinySet<LiteralId> lidSet (void) 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 isCountedLogVar (LogVar X) const;
|
||||||
|
|
||||||
@ -120,16 +116,19 @@ class Clause
|
|||||||
|
|
||||||
bool isNegativeCountedLogVar (LogVar X) const;
|
bool isNegativeCountedLogVar (LogVar X) const;
|
||||||
|
|
||||||
friend std::ostream& operator<< (ostream &os, const Clause& clause);
|
TinySet<LiteralId> lidSet (void) const;
|
||||||
|
|
||||||
void removeLiteral (size_t idx);
|
LogVarSet ipgCandidates (void) const;
|
||||||
|
|
||||||
LogVarTypes logVarTypes (size_t litIdx) const;
|
LogVarTypes logVarTypes (size_t litIdx) const;
|
||||||
|
|
||||||
|
void removeLiteral (size_t litIdx);
|
||||||
|
|
||||||
static void printClauses (const vector<Clause>& clauses);
|
static void printClauses (const vector<Clause>& clauses);
|
||||||
|
|
||||||
private:
|
friend std::ostream& operator<< (ostream &os, const Clause& clause);
|
||||||
|
|
||||||
|
private:
|
||||||
LogVarSet getLogVarSetExcluding (size_t idx) const;
|
LogVarSet getLogVarSetExcluding (size_t idx) const;
|
||||||
|
|
||||||
vector<Literal> literals_;
|
vector<Literal> literals_;
|
||||||
@ -139,8 +138,6 @@ class Clause
|
|||||||
ConstraintTree constr_;
|
ConstraintTree constr_;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
typedef vector<Clause> Clauses;
|
typedef vector<Clause> Clauses;
|
||||||
|
|
||||||
|
|
||||||
|
Reference in New Issue
Block a user