lifted kc: when not debuging don't keep track of the origin clauses
This commit is contained in:
Tiago Gomes
parent
ee1b7dcd21
commit
73b3594c97
@ -77,9 +77,8 @@ IncExcNode::weight (void) const
|
||||
double
|
||||
LeafNode::weight (void) const
|
||||
{
|
||||
assert (clauses().size() == 1);
|
||||
assert (clauses()[0].isUnit());
|
||||
Clause c = clauses()[0];
|
||||
assert (clause_.isUnit());
|
||||
Clause c = clause_;
|
||||
double weight = c.literals()[0].isPositive()
|
||||
? lwcnf_.posWeight (c.literals().front().lid())
|
||||
: lwcnf_.negWeight (c.literals().front().lid());
|
||||
@ -261,7 +260,11 @@ LiftedCircuit::compile (
|
||||
return;
|
||||
}
|
||||
|
||||
*follow = new CompilationFailedNode (clauses);
|
||||
*follow = new CompilationFailedNode();
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[*follow] = clauses;
|
||||
explanationMap_[*follow] = "" ;
|
||||
}
|
||||
compilationSucceeded_ = false;
|
||||
}
|
||||
|
||||
@ -272,6 +275,9 @@ LiftedCircuit::tryUnitPropagation (
|
||||
CircuitNode** follow,
|
||||
Clauses& clauses)
|
||||
{
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = clauses;
|
||||
}
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
if (clauses[i].isUnit()) {
|
||||
Clauses newClauses;
|
||||
@ -294,9 +300,13 @@ LiftedCircuit::tryUnitPropagation (
|
||||
}
|
||||
}
|
||||
}
|
||||
stringstream explanation;
|
||||
explanation << " UP on" << clauses[i].literals()[0];
|
||||
AndNode* andNode = new AndNode (clauses, explanation.str());
|
||||
AndNode* andNode = new AndNode();
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[andNode] = backupClauses_;
|
||||
stringstream explanation;
|
||||
explanation << " UP on>" << clauses[i].literals()[0];
|
||||
explanationMap_[andNode] = explanation.str();
|
||||
}
|
||||
Clauses leftClauses = {clauses[i]};
|
||||
compile (andNode->leftBranch(), leftClauses);
|
||||
compile (andNode->rightBranch(), newClauses);
|
||||
@ -317,6 +327,9 @@ LiftedCircuit::tryIndependence (
|
||||
if (clauses.size() == 1) {
|
||||
return false;
|
||||
}
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = clauses;
|
||||
}
|
||||
Clauses depClauses = { clauses[0] };
|
||||
Clauses indepClauses (clauses.begin() + 1, clauses.end());
|
||||
bool finish = false;
|
||||
@ -332,7 +345,11 @@ LiftedCircuit::tryIndependence (
|
||||
}
|
||||
}
|
||||
if (indepClauses.empty() == false) {
|
||||
AndNode* andNode = new AndNode (clauses, " Independence");
|
||||
AndNode* andNode = new AndNode ();
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[andNode] = backupClauses_;
|
||||
explanationMap_[andNode] = " Independence" ;
|
||||
}
|
||||
compile (andNode->leftBranch(), depClauses);
|
||||
compile (andNode->rightBranch(), indepClauses);
|
||||
(*follow) = andNode;
|
||||
@ -348,6 +365,9 @@ LiftedCircuit::tryShannonDecomp (
|
||||
CircuitNode** follow,
|
||||
Clauses& clauses)
|
||||
{
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = clauses;
|
||||
}
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
const Literals& literals = clauses[i].literals();
|
||||
for (size_t j = 0; j < literals.size(); j++) {
|
||||
@ -364,9 +384,13 @@ LiftedCircuit::tryShannonDecomp (
|
||||
Clauses rightClauses = { c2 };
|
||||
leftClauses.insert (leftClauses.end(), clauses.begin(), clauses.end());
|
||||
rightClauses.insert (rightClauses.end(), clauses.begin(), clauses.end());
|
||||
stringstream explanation;
|
||||
explanation << " SD on " << literals[j];
|
||||
OrNode* orNode = new OrNode (clauses, explanation.str());
|
||||
OrNode* orNode = new OrNode();
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[orNode] = backupClauses_;
|
||||
stringstream explanation;
|
||||
explanation << " SD on " << literals[j];
|
||||
explanationMap_[orNode] = explanation.str();
|
||||
}
|
||||
compile (orNode->leftBranch(), leftClauses);
|
||||
compile (orNode->rightBranch(), rightClauses);
|
||||
(*follow) = orNode;
|
||||
@ -384,6 +408,9 @@ LiftedCircuit::tryInclusionExclusion (
|
||||
CircuitNode** follow,
|
||||
Clauses& clauses)
|
||||
{
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = clauses;
|
||||
}
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
Literals depLits = { clauses[i].literals().front() };
|
||||
Literals indepLits (clauses[i].literals().begin() + 1,
|
||||
@ -433,9 +460,13 @@ LiftedCircuit::tryInclusionExclusion (
|
||||
plus2Clauses.push_back (c2);
|
||||
minusClauses.push_back (c1);
|
||||
minusClauses.push_back (c2);
|
||||
stringstream explanation;
|
||||
explanation << " IncExc on clause nº " << i + 1;
|
||||
IncExcNode* ieNode = new IncExcNode (clauses, explanation.str());
|
||||
IncExcNode* ieNode = new IncExcNode();
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[ieNode] = backupClauses_;
|
||||
stringstream explanation;
|
||||
explanation << " IncExc on clause nº " << i + 1;
|
||||
explanationMap_[ieNode] = explanation.str();
|
||||
}
|
||||
compile (ieNode->plus1Branch(), plus1Clauses);
|
||||
compile (ieNode->plus2Branch(), plus2Clauses);
|
||||
compile (ieNode->minusBranch(), minusClauses);
|
||||
@ -455,6 +486,9 @@ LiftedCircuit::tryIndepPartialGrounding (
|
||||
{
|
||||
// assumes that all literals have logical variables
|
||||
// else, shannon decomp was possible
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = clauses;
|
||||
}
|
||||
LogVars rootLogVars;
|
||||
LogVarSet lvs = clauses[0].ipgCandidates();
|
||||
for (size_t i = 0; i < lvs.size(); i++) {
|
||||
@ -466,9 +500,13 @@ LiftedCircuit::tryIndepPartialGrounding (
|
||||
for (size_t j = 0; j < clauses.size(); j++) {
|
||||
newClauses[j].addIpgLogVar (rootLogVars[j]);
|
||||
}
|
||||
SetAndNode* node = new SetAndNode (ct.size(), clauses);
|
||||
*follow = node;
|
||||
compile (node->follow(), newClauses);
|
||||
SetAndNode* setAndNode = new SetAndNode (ct.size());
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[setAndNode] = backupClauses_;
|
||||
explanationMap_[setAndNode] = " IPG" ;
|
||||
}
|
||||
*follow = setAndNode;
|
||||
compile (setAndNode->follow(), newClauses);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
@ -531,6 +569,9 @@ LiftedCircuit::tryAtomCounting (
|
||||
return false;
|
||||
}
|
||||
}
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = clauses;
|
||||
}
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
Literals literals = clauses[i].literals();
|
||||
for (size_t j = 0; j < literals.size(); j++) {
|
||||
@ -539,7 +580,11 @@ LiftedCircuit::tryAtomCounting (
|
||||
&& ! clauses[i].isCountedLogVar (literals[j].logVars().front())) {
|
||||
unsigned nrGroundings = clauses[i].constr().projectedCopy (
|
||||
literals[j].logVars()).size();
|
||||
SetOrNode* setOrNode = new SetOrNode (nrGroundings, clauses);
|
||||
SetOrNode* setOrNode = new SetOrNode (nrGroundings);
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[setOrNode] = backupClauses_;
|
||||
explanationMap_[setOrNode] = " AC" ;
|
||||
}
|
||||
Clause c1 (clauses[i].constr().projectedCopy (literals[j].logVars()));
|
||||
Clause c2 (clauses[i].constr().projectedCopy (literals[j].logVars()));
|
||||
c1.addLiteral (literals[j]);
|
||||
@ -734,9 +779,10 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
||||
}
|
||||
|
||||
case CircuitNodeType::LEAF_NODE: {
|
||||
LeafNode* casted = dynamic_cast<LeafNode*>(node);
|
||||
propagLits.insert (LitLvTypes (
|
||||
node->clauses()[0].literals()[0].lid(),
|
||||
node->clauses()[0].logVarTypes(0)));
|
||||
casted->clause().literals()[0].lid(),
|
||||
casted->clause().logVarTypes(0)));
|
||||
}
|
||||
|
||||
default:
|
||||
@ -754,6 +800,10 @@ LiftedCircuit::createSmoothNode (
|
||||
CircuitNode** prev)
|
||||
{
|
||||
if (missingLits.empty() == false) {
|
||||
if (Globals::verbosity > 1) {
|
||||
// assert (Util::contains (originClausesMap_, prev));
|
||||
backupClauses_ = originClausesMap_[*prev];
|
||||
}
|
||||
Clauses clauses;
|
||||
for (size_t i = 0; i < missingLits.size(); i++) {
|
||||
LiteralId lid = missingLits[i].lid();
|
||||
@ -771,8 +821,11 @@ LiftedCircuit::createSmoothNode (
|
||||
clauses.push_back (c);
|
||||
}
|
||||
SmoothNode* smoothNode = new SmoothNode (clauses, *lwcnf_);
|
||||
*prev = new AndNode ((*prev)->clauses(), smoothNode,
|
||||
*prev, " Smoothing");
|
||||
*prev = new AndNode (smoothNode, *prev);
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[*prev] = backupClauses_;
|
||||
explanationMap_[*prev] = " Smoothing" ;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -879,7 +932,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||
|
||||
os << auxNode << " [" << opStyle << "label=\"∨\"]" << endl;
|
||||
os << escapeNode (node) << " -> " << auxNode;
|
||||
os << " [label=\"" << node->explanation() << "\"]" ;
|
||||
os << " [label=\"" << getExplanationString (node) << "\"]" ;
|
||||
os << endl;
|
||||
|
||||
os << auxNode << " -> " ;
|
||||
@ -903,7 +956,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||
|
||||
os << auxNode << " [" << opStyle << "label=\"∧\"]" << endl;
|
||||
os << escapeNode (node) << " -> " << auxNode;
|
||||
os << " [label=\"" << node->explanation() << "\"]" ;
|
||||
os << " [label=\"" << getExplanationString (node) << "\"]" ;
|
||||
os << endl;
|
||||
|
||||
os << auxNode << " -> " ;
|
||||
@ -927,7 +980,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||
|
||||
os << auxNode << " [" << opStyle << "label=\"∨(X)\"]" << endl;
|
||||
os << escapeNode (node) << " -> " << auxNode;
|
||||
os << " [label=\"" << node->explanation() << "\"]" ;
|
||||
os << " [label=\"" << getExplanationString (node) << "\"]" ;
|
||||
os << endl;
|
||||
|
||||
os << auxNode << " -> " ;
|
||||
@ -945,7 +998,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||
|
||||
os << auxNode << " [" << opStyle << "label=\"∧(X)\"]" << endl;
|
||||
os << escapeNode (node) << " -> " << auxNode;
|
||||
os << " [label=\"" << node->explanation() << "\"]" ;
|
||||
os << " [label=\"" << getExplanationString (node) << "\"]" ;
|
||||
os << endl;
|
||||
|
||||
os << auxNode << " -> " ;
|
||||
@ -964,7 +1017,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||
os << auxNode << " [" << opStyle << "label=\"+ - +\"]" ;
|
||||
os << endl;
|
||||
os << escapeNode (node) << " -> " << auxNode;
|
||||
os << " [label=\"" << node->explanation() << "\"]" ;
|
||||
os << " [label=\"" << getExplanationString (node) << "\"]" ;
|
||||
os << endl;
|
||||
|
||||
os << auxNode << " -> " ;
|
||||
@ -1027,14 +1080,31 @@ LiftedCircuit::escapeNode (const CircuitNode* node) const
|
||||
|
||||
|
||||
|
||||
string
|
||||
LiftedCircuit::getExplanationString (CircuitNode* node)
|
||||
{
|
||||
return Util::contains (explanationMap_, node)
|
||||
? explanationMap_[node]
|
||||
: "" ;
|
||||
}
|
||||
|
||||
|
||||
|
||||
void
|
||||
LiftedCircuit::printClauses (
|
||||
const CircuitNode* node,
|
||||
CircuitNode* node,
|
||||
ofstream& os,
|
||||
string extraOptions)
|
||||
{
|
||||
const Clauses& clauses = node->clauses();
|
||||
if (node->clauses().empty() == false) {
|
||||
Clauses clauses;
|
||||
if (Util::contains (originClausesMap_, node)) {
|
||||
clauses = originClausesMap_[node];
|
||||
} else if (getCircuitNodeType (node) == CircuitNodeType::LEAF_NODE) {
|
||||
clauses = { (dynamic_cast<LeafNode*>(node))->clause() } ;
|
||||
} else if (getCircuitNodeType (node) == CircuitNodeType::SMOOTH_NODE) {
|
||||
clauses = (dynamic_cast<SmoothNode*>(node))->clauses();
|
||||
}
|
||||
if (clauses.empty() == false) {
|
||||
os << escapeNode (node);
|
||||
os << " [shape=box," << extraOptions << "label=\"" ;
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
@ -1043,6 +1113,8 @@ LiftedCircuit::printClauses (
|
||||
}
|
||||
os << "\"]" ;
|
||||
os << endl;
|
||||
} else {
|
||||
os << " [shape=box]" << endl;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@ -23,20 +23,9 @@ enum CircuitNodeType {
|
||||
class CircuitNode
|
||||
{
|
||||
public:
|
||||
CircuitNode (const Clauses& clauses, string explanation = "")
|
||||
: clauses_(clauses), explanation_(explanation) { }
|
||||
|
||||
const Clauses& clauses (void) const { return clauses_; }
|
||||
|
||||
Clauses clauses (void) { return clauses_; }
|
||||
CircuitNode (void) { }
|
||||
|
||||
virtual double weight (void) const = 0;
|
||||
|
||||
string explanation (void) const { return explanation_; }
|
||||
|
||||
private:
|
||||
Clauses clauses_;
|
||||
string explanation_;
|
||||
};
|
||||
|
||||
|
||||
@ -44,9 +33,7 @@ class CircuitNode
|
||||
class OrNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
OrNode (const Clauses& clauses, string explanation = "")
|
||||
: CircuitNode (clauses, explanation),
|
||||
leftBranch_(0), rightBranch_(0) { }
|
||||
OrNode (void) : CircuitNode(), leftBranch_(0), rightBranch_(0) { }
|
||||
|
||||
CircuitNode** leftBranch (void) { return &leftBranch_; }
|
||||
CircuitNode** rightBranch (void) { return &rightBranch_; }
|
||||
@ -63,24 +50,10 @@ class OrNode : public CircuitNode
|
||||
class AndNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
AndNode (const Clauses& clauses, string explanation = "")
|
||||
: CircuitNode (clauses, explanation),
|
||||
leftBranch_(0), rightBranch_(0) { }
|
||||
AndNode (void) : CircuitNode(), leftBranch_(0), rightBranch_(0) { }
|
||||
|
||||
AndNode (
|
||||
const Clauses& clauses,
|
||||
CircuitNode* leftBranch,
|
||||
CircuitNode* rightBranch,
|
||||
string explanation = "")
|
||||
: CircuitNode (clauses, explanation),
|
||||
leftBranch_(leftBranch), rightBranch_(rightBranch) { }
|
||||
|
||||
AndNode (
|
||||
CircuitNode* leftBranch,
|
||||
CircuitNode* rightBranch,
|
||||
string explanation = "")
|
||||
: CircuitNode ({}, explanation),
|
||||
leftBranch_(leftBranch), rightBranch_(rightBranch) { }
|
||||
AndNode (CircuitNode* leftBranch, CircuitNode* rightBranch)
|
||||
: CircuitNode(), leftBranch_(leftBranch), rightBranch_(rightBranch) { }
|
||||
|
||||
CircuitNode** leftBranch (void) { return &leftBranch_; }
|
||||
CircuitNode** rightBranch (void) { return &rightBranch_; }
|
||||
@ -97,9 +70,8 @@ class AndNode : public CircuitNode
|
||||
class SetOrNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
SetOrNode (unsigned nrGroundings, const Clauses& clauses)
|
||||
: CircuitNode (clauses, " AC"), follow_(0),
|
||||
nrGroundings_(nrGroundings) { }
|
||||
SetOrNode (unsigned nrGroundings)
|
||||
: CircuitNode(), follow_(0), nrGroundings_(nrGroundings) { }
|
||||
|
||||
CircuitNode** follow (void) { return &follow_; }
|
||||
|
||||
@ -121,9 +93,8 @@ class SetOrNode : public CircuitNode
|
||||
class SetAndNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
SetAndNode (unsigned nrGroundings, const Clauses& clauses)
|
||||
: CircuitNode (clauses, " IPG"), follow_(0),
|
||||
nrGroundings_(nrGroundings) { }
|
||||
SetAndNode (unsigned nrGroundings)
|
||||
: CircuitNode(), follow_(0), nrGroundings_(nrGroundings) { }
|
||||
|
||||
CircuitNode** follow (void) { return &follow_; }
|
||||
|
||||
@ -139,9 +110,8 @@ class SetAndNode : public CircuitNode
|
||||
class IncExcNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
IncExcNode (const Clauses& clauses, string explanation)
|
||||
: CircuitNode (clauses, explanation), plus1Branch_(0),
|
||||
plus2Branch_(0), minusBranch_(0) { }
|
||||
IncExcNode (void)
|
||||
: CircuitNode(), plus1Branch_(0), plus2Branch_(0), minusBranch_(0) { }
|
||||
|
||||
CircuitNode** plus1Branch (void) { return &plus1Branch_; }
|
||||
CircuitNode** plus2Branch (void) { return &plus2Branch_; }
|
||||
@ -161,11 +131,16 @@ class LeafNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
LeafNode (const Clause& clause, const LiftedWCNF& lwcnf)
|
||||
: CircuitNode (Clauses() = {clause}), lwcnf_(lwcnf) { }
|
||||
: CircuitNode(), clause_(clause), lwcnf_(lwcnf) { }
|
||||
|
||||
const Clause& clause (void) const { return clause_; }
|
||||
|
||||
Clause& clause (void) { return clause_; }
|
||||
|
||||
double weight (void) const;
|
||||
|
||||
private:
|
||||
Clause clause_;
|
||||
const LiftedWCNF& lwcnf_;
|
||||
};
|
||||
|
||||
@ -175,11 +150,16 @@ class SmoothNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
SmoothNode (const Clauses& clauses, const LiftedWCNF& lwcnf)
|
||||
: CircuitNode (clauses), lwcnf_(lwcnf) { }
|
||||
: CircuitNode(), clauses_(clauses), lwcnf_(lwcnf) { }
|
||||
|
||||
const Clauses& clauses (void) const { return clauses_; }
|
||||
|
||||
Clauses clauses (void) { return clauses_; }
|
||||
|
||||
double weight (void) const;
|
||||
|
||||
private:
|
||||
Clauses clauses_;
|
||||
const LiftedWCNF& lwcnf_;
|
||||
};
|
||||
|
||||
@ -188,7 +168,7 @@ class SmoothNode : public CircuitNode
|
||||
class TrueNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
TrueNode (void) : CircuitNode ({}) { }
|
||||
TrueNode (void) : CircuitNode() { }
|
||||
|
||||
double weight (void) const;
|
||||
};
|
||||
@ -198,8 +178,7 @@ class TrueNode : public CircuitNode
|
||||
class CompilationFailedNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
CompilationFailedNode (const Clauses& clauses)
|
||||
: CircuitNode (clauses) { }
|
||||
CompilationFailedNode (void) : CircuitNode() { }
|
||||
|
||||
double weight (void) const;
|
||||
};
|
||||
@ -261,13 +240,19 @@ class LiftedCircuit
|
||||
|
||||
void exportToGraphViz (CircuitNode* node, ofstream&);
|
||||
|
||||
void printClauses (const CircuitNode* node, ofstream&,
|
||||
void printClauses (CircuitNode* node, ofstream&,
|
||||
string extraOptions = "");
|
||||
|
||||
string escapeNode (const CircuitNode* node) const;
|
||||
|
||||
string getExplanationString (CircuitNode* node);
|
||||
|
||||
CircuitNode* root_;
|
||||
const LiftedWCNF* lwcnf_;
|
||||
|
||||
Clauses backupClauses_;
|
||||
unordered_map<CircuitNode*, Clauses> originClausesMap_;
|
||||
unordered_map<CircuitNode*, string> explanationMap_;
|
||||
bool compilationSucceeded_;
|
||||
};
|
||||
|
||||
|
||||
Reference in New Issue
Block a user