support smoothing in inclusion-exclusion nodes
This commit is contained in:
parent
b31a047635
commit
77ef7b87cd
@ -498,32 +498,8 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
|||||||
TinySet<LiteralId> lids2 = smoothCircuit (*casted->rightBranch());
|
TinySet<LiteralId> lids2 = smoothCircuit (*casted->rightBranch());
|
||||||
TinySet<LiteralId> missingLeft = lids2 - lids1;
|
TinySet<LiteralId> missingLeft = lids2 - lids1;
|
||||||
TinySet<LiteralId> missingRight = lids1 - lids2;
|
TinySet<LiteralId> missingRight = lids1 - lids2;
|
||||||
if (missingLeft.empty() == false) {
|
createSmoothNode (missingLeft, casted->leftBranch());
|
||||||
Clauses clauses;
|
createSmoothNode (missingRight, casted->rightBranch());
|
||||||
for (size_t i = 0; i < missingLeft.size(); i++) {
|
|
||||||
Clause c = lwcnf_->createClauseForLiteral (missingLeft[i]);
|
|
||||||
c.addAndNegateLiteral (c.literals()[0]);
|
|
||||||
clauses.push_back (c);
|
|
||||||
}
|
|
||||||
SmoothNode* smoothNode = new SmoothNode (clauses);
|
|
||||||
CircuitNode** prev = casted->leftBranch();
|
|
||||||
AndNode* andNode = new AndNode ((*prev)->clauses(),
|
|
||||||
smoothNode, *prev, " Smoothing");
|
|
||||||
*prev = andNode;
|
|
||||||
}
|
|
||||||
if (missingRight.empty() == false) {
|
|
||||||
Clauses clauses;
|
|
||||||
for (size_t i = 0; i < missingRight.size(); i++) {
|
|
||||||
Clause c = lwcnf_->createClauseForLiteral (missingRight[i]);
|
|
||||||
c.addAndNegateLiteral (c.literals()[0]);
|
|
||||||
clauses.push_back (c);
|
|
||||||
}
|
|
||||||
SmoothNode* smoothNode = new SmoothNode (clauses);
|
|
||||||
CircuitNode** prev = casted->rightBranch();
|
|
||||||
AndNode* andNode = new AndNode ((*prev)->clauses(), smoothNode,
|
|
||||||
*prev, " Smoothing");
|
|
||||||
*prev = andNode;
|
|
||||||
}
|
|
||||||
propagatingLids |= lids1;
|
propagatingLids |= lids1;
|
||||||
propagatingLids |= lids2;
|
propagatingLids |= lids2;
|
||||||
break;
|
break;
|
||||||
@ -549,7 +525,15 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
|||||||
}
|
}
|
||||||
|
|
||||||
case CircuitNodeType::INC_EXC_NODE: {
|
case CircuitNodeType::INC_EXC_NODE: {
|
||||||
// TODO
|
IncExcNode* casted = dynamic_cast<IncExcNode*>(node);
|
||||||
|
TinySet<LiteralId> lids1 = smoothCircuit (*casted->plus1Branch());
|
||||||
|
TinySet<LiteralId> lids2 = smoothCircuit (*casted->plus2Branch());
|
||||||
|
TinySet<LiteralId> missingPlus1 = lids2 - lids1;
|
||||||
|
TinySet<LiteralId> missingPlus2 = lids1 - lids2;
|
||||||
|
createSmoothNode (missingPlus1, casted->plus1Branch());
|
||||||
|
createSmoothNode (missingPlus2, casted->plus2Branch());
|
||||||
|
propagatingLids |= lids1;
|
||||||
|
propagatingLids |= lids2;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -570,6 +554,26 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
void
|
||||||
|
LiftedCircuit::createSmoothNode (
|
||||||
|
const TinySet<LiteralId>& missingLids,
|
||||||
|
CircuitNode** prev)
|
||||||
|
{
|
||||||
|
if (missingLids.empty() == false) {
|
||||||
|
Clauses clauses;
|
||||||
|
for (size_t i = 0; i < missingLids.size(); i++) {
|
||||||
|
Clause c = lwcnf_->createClauseForLiteral (missingLids[i]);
|
||||||
|
c.addAndNegateLiteral (c.literals()[0]);
|
||||||
|
clauses.push_back (c);
|
||||||
|
}
|
||||||
|
SmoothNode* smoothNode = new SmoothNode (clauses);
|
||||||
|
*prev = new AndNode ((*prev)->clauses(), smoothNode,
|
||||||
|
*prev, " Smoothing");
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
CircuitNodeType
|
CircuitNodeType
|
||||||
LiftedCircuit::getCircuitNodeType (const CircuitNode* node) const
|
LiftedCircuit::getCircuitNodeType (const CircuitNode* node) const
|
||||||
{
|
{
|
||||||
@ -600,16 +604,6 @@ LiftedCircuit::getCircuitNodeType (const CircuitNode* node) const
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
string
|
|
||||||
LiftedCircuit::escapeNode (const CircuitNode* node) const
|
|
||||||
{
|
|
||||||
stringstream ss;
|
|
||||||
ss << "\"" << node << "\"" ;
|
|
||||||
return ss.str();
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
void
|
void
|
||||||
LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||||
{
|
{
|
||||||
@ -754,6 +748,16 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
string
|
||||||
|
LiftedCircuit::escapeNode (const CircuitNode* node) const
|
||||||
|
{
|
||||||
|
stringstream ss;
|
||||||
|
ss << "\"" << node << "\"" ;
|
||||||
|
return ss.str();
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
void
|
void
|
||||||
LiftedCircuit::printClauses (
|
LiftedCircuit::printClauses (
|
||||||
const CircuitNode* node,
|
const CircuitNode* node,
|
||||||
|
@ -209,14 +209,17 @@ class LiftedCircuit
|
|||||||
|
|
||||||
TinySet<LiteralId> smoothCircuit (CircuitNode* node);
|
TinySet<LiteralId> smoothCircuit (CircuitNode* node);
|
||||||
|
|
||||||
CircuitNodeType getCircuitNodeType (const CircuitNode* node) const;
|
void createSmoothNode (const TinySet<LiteralId>& lids,
|
||||||
|
CircuitNode** prev);
|
||||||
string escapeNode (const CircuitNode* node) const;
|
|
||||||
|
|
||||||
|
CircuitNodeType getCircuitNodeType (const CircuitNode* node) const;
|
||||||
|
|
||||||
void exportToGraphViz (CircuitNode* node, ofstream&);
|
void exportToGraphViz (CircuitNode* node, ofstream&);
|
||||||
|
|
||||||
void printClauses (const CircuitNode* node, ofstream&,
|
void printClauses (const CircuitNode* node, ofstream&,
|
||||||
string extraOptions = "");
|
string extraOptions = "");
|
||||||
|
|
||||||
|
string escapeNode (const CircuitNode* node) const;
|
||||||
|
|
||||||
CircuitNode* root_;
|
CircuitNode* root_;
|
||||||
const LiftedWCNF* lwcnf_;
|
const LiftedWCNF* lwcnf_;
|
||||||
|
Reference in New Issue
Block a user