small improvements
This commit is contained in:
parent
864f764391
commit
a75799b34f
@ -110,6 +110,17 @@ TrueNode::weight (void) const
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
double
|
||||||
|
CompilationFailedNode::weight (void) const
|
||||||
|
{
|
||||||
|
// we should not perform model counting
|
||||||
|
// in compilation failed nodes
|
||||||
|
abort();
|
||||||
|
return 0.0;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
LiftedCircuit::LiftedCircuit (const LiftedWCNF* lwcnf)
|
LiftedCircuit::LiftedCircuit (const LiftedWCNF* lwcnf)
|
||||||
: lwcnf_(lwcnf)
|
: lwcnf_(lwcnf)
|
||||||
{
|
{
|
||||||
@ -217,7 +228,7 @@ LiftedCircuit::compile (
|
|||||||
}
|
}
|
||||||
|
|
||||||
// assert (false);
|
// assert (false);
|
||||||
*follow = new FailNode (clauses);
|
*follow = new CompilationFailedNode (clauses);
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -237,14 +248,10 @@ LiftedCircuit::tryUnitPropagation (
|
|||||||
if (clauses[i].literals()[0].isPositive()) {
|
if (clauses[i].literals()[0].isPositive()) {
|
||||||
if (clauses[j].containsPositiveLiteral (lid) == false) {
|
if (clauses[j].containsPositiveLiteral (lid) == false) {
|
||||||
Clause newClause = clauses[j];
|
Clause newClause = clauses[j];
|
||||||
//cout << "new j : " << clauses[j] << endl;
|
|
||||||
//cout << "new clause: " << newClause << endl;
|
|
||||||
//cout << "clvs: " << clauses[j].constr()->logVars() << endl;
|
|
||||||
newClause.removeNegativeLiterals (lid);
|
newClause.removeNegativeLiterals (lid);
|
||||||
newClauses.push_back (newClause);
|
newClauses.push_back (newClause);
|
||||||
}
|
}
|
||||||
} else if (clauses[i].literals()[0].isNegative()) {
|
} else if (clauses[i].literals()[0].isNegative()) {
|
||||||
//cout << "unit prop of = " << clauses[i].literals()[0] << endl;
|
|
||||||
if (clauses[j].containsNegativeLiteral (lid) == false) {
|
if (clauses[j].containsNegativeLiteral (lid) == false) {
|
||||||
Clause newClause = clauses[j];
|
Clause newClause = clauses[j];
|
||||||
newClause.removePositiveLiterals (lid);
|
newClause.removePositiveLiterals (lid);
|
||||||
@ -254,7 +261,6 @@ LiftedCircuit::tryUnitPropagation (
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
stringstream explanation;
|
stringstream explanation;
|
||||||
explanation << " UP of " << clauses[i];
|
|
||||||
AndNode* andNode = new AndNode (clauses, explanation.str());
|
AndNode* andNode = new AndNode (clauses, explanation.str());
|
||||||
Clauses leftClauses = {clauses[i]};
|
Clauses leftClauses = {clauses[i]};
|
||||||
compile (andNode->leftBranch(), leftClauses);
|
compile (andNode->leftBranch(), leftClauses);
|
||||||
@ -551,7 +557,7 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
|||||||
|
|
||||||
// case CircuitNodeType::SMOOTH_NODE:
|
// case CircuitNodeType::SMOOTH_NODE:
|
||||||
// case CircuitNodeType::TRUE_NODE:
|
// case CircuitNodeType::TRUE_NODE:
|
||||||
// case CircuitNodeType::FAIL_NODE:
|
// case CircuitNodeType::COMPILATION_FAILED_NODE:
|
||||||
|
|
||||||
default:
|
default:
|
||||||
break;
|
break;
|
||||||
@ -571,8 +577,6 @@ LiftedCircuit::getCircuitNodeType (const CircuitNode* node) const
|
|||||||
} else if (dynamic_cast<const AndNode*>(node) != 0) {
|
} else if (dynamic_cast<const AndNode*>(node) != 0) {
|
||||||
type = CircuitNodeType::AND_NODE;
|
type = CircuitNodeType::AND_NODE;
|
||||||
} else if (dynamic_cast<const SetOrNode*>(node) != 0) {
|
} else if (dynamic_cast<const SetOrNode*>(node) != 0) {
|
||||||
// TODO
|
|
||||||
assert (false);
|
|
||||||
type = CircuitNodeType::SET_OR_NODE;
|
type = CircuitNodeType::SET_OR_NODE;
|
||||||
} else if (dynamic_cast<const SetAndNode*>(node) != 0) {
|
} else if (dynamic_cast<const SetAndNode*>(node) != 0) {
|
||||||
type = CircuitNodeType::SET_AND_NODE;
|
type = CircuitNodeType::SET_AND_NODE;
|
||||||
@ -584,8 +588,8 @@ LiftedCircuit::getCircuitNodeType (const CircuitNode* node) const
|
|||||||
type = CircuitNodeType::SMOOTH_NODE;
|
type = CircuitNodeType::SMOOTH_NODE;
|
||||||
} else if (dynamic_cast<const TrueNode*>(node) != 0) {
|
} else if (dynamic_cast<const TrueNode*>(node) != 0) {
|
||||||
type = CircuitNodeType::TRUE_NODE;
|
type = CircuitNodeType::TRUE_NODE;
|
||||||
} else if (dynamic_cast<const FailNode*>(node) != 0) {
|
} else if (dynamic_cast<const CompilationFailedNode*>(node) != 0) {
|
||||||
type = CircuitNodeType::FAIL_NODE;
|
type = CircuitNodeType::COMPILATION_FAILED_NODE;
|
||||||
} else {
|
} else {
|
||||||
assert (false);
|
assert (false);
|
||||||
}
|
}
|
||||||
@ -778,7 +782,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
|||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
|
||||||
case FAIL_NODE: {
|
case COMPILATION_FAILED_NODE: {
|
||||||
os << escapeNode (node);
|
os << escapeNode (node);
|
||||||
os << " [shape=box,style=filled,fillcolor=brown1,label=\"" ;
|
os << " [shape=box,style=filled,fillcolor=brown1,label=\"" ;
|
||||||
const Clauses& clauses = node->clauses();
|
const Clauses& clauses = node->clauses();
|
||||||
|
@ -13,7 +13,7 @@ enum CircuitNodeType {
|
|||||||
LEAF_NODE,
|
LEAF_NODE,
|
||||||
SMOOTH_NODE,
|
SMOOTH_NODE,
|
||||||
TRUE_NODE,
|
TRUE_NODE,
|
||||||
FAIL_NODE
|
COMPILATION_FAILED_NODE
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
||||||
@ -28,7 +28,7 @@ class CircuitNode
|
|||||||
|
|
||||||
Clauses clauses (void) { return clauses_; }
|
Clauses clauses (void) { return clauses_; }
|
||||||
|
|
||||||
virtual double weight (void) const { return 0; }
|
virtual double weight (void) const = 0;
|
||||||
|
|
||||||
string explanation (void) const { return explanation_; }
|
string explanation (void) const { return explanation_; }
|
||||||
|
|
||||||
@ -128,6 +128,8 @@ class IncExcNode : public CircuitNode
|
|||||||
IncExcNode (const Clauses& clauses)
|
IncExcNode (const Clauses& clauses)
|
||||||
: CircuitNode (clauses), plus1Branch_(0),
|
: CircuitNode (clauses), plus1Branch_(0),
|
||||||
plus2Branch_(0), minusBranch_(0) { }
|
plus2Branch_(0), minusBranch_(0) { }
|
||||||
|
|
||||||
|
double weight (void) const;
|
||||||
|
|
||||||
CircuitNode** plus1Branch (void) { return &plus1Branch_; }
|
CircuitNode** plus1Branch (void) { return &plus1Branch_; }
|
||||||
CircuitNode** plus2Branch (void) { return &plus2Branch_; }
|
CircuitNode** plus2Branch (void) { return &plus2Branch_; }
|
||||||
@ -171,10 +173,12 @@ class TrueNode : public CircuitNode
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
class FailNode : public CircuitNode
|
class CompilationFailedNode : public CircuitNode
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
FailNode (const Clauses& clauses) : CircuitNode (clauses) { }
|
CompilationFailedNode (const Clauses& clauses) : CircuitNode (clauses) { }
|
||||||
|
|
||||||
|
double weight (void) const;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
||||||
|
Reference in New Issue
Block a user