remove and add some TODOs
This commit is contained in:
parent
5e1547ba78
commit
869d513c1a
@ -99,21 +99,20 @@ LeafNode::weight (void) const
|
|||||||
ct.project (lvs);
|
ct.project (lvs);
|
||||||
nrGroundings = ct.size();
|
nrGroundings = ct.size();
|
||||||
}
|
}
|
||||||
// TODO this only works for one counted log var
|
// cout << "calc weight for " << clauses().front() << endl;
|
||||||
cout << "calc weight for " << clauses().front() << endl;
|
|
||||||
if (c.positiveCountedLogVars().empty() == false) {
|
if (c.positiveCountedLogVars().empty() == false) {
|
||||||
cout << " -> nr pos = " << SetOrNode::nrPositives() << endl;
|
// cout << " -> nr pos = " << SetOrNode::nrPositives() << endl;
|
||||||
nrGroundings *= std::pow (SetOrNode::nrPositives(),
|
nrGroundings *= std::pow (SetOrNode::nrPositives(),
|
||||||
c.nrPositiveCountedLogVars());
|
c.nrPositiveCountedLogVars());
|
||||||
}
|
}
|
||||||
if (c.negativeCountedLogVars().empty() == false) {
|
if (c.negativeCountedLogVars().empty() == false) {
|
||||||
cout << " -> nr neg = " << SetOrNode::nrNegatives() << endl;
|
//cout << " -> nr neg = " << SetOrNode::nrNegatives() << endl;
|
||||||
nrGroundings *= std::pow (SetOrNode::nrNegatives(),
|
nrGroundings *= std::pow (SetOrNode::nrNegatives(),
|
||||||
c.nrNegativeCountedLogVars());
|
c.nrNegativeCountedLogVars());
|
||||||
}
|
}
|
||||||
cout << " -> nr groundings = " << nrGroundings << endl;
|
// cout << " -> nr groundings = " << nrGroundings << endl;
|
||||||
cout << " -> lit weight = " << weight << endl;
|
// cout << " -> lit weight = " << weight << endl;
|
||||||
cout << " -> ret weight = " << std::pow (weight, nrGroundings) << endl;
|
// cout << " -> ret weight = " << std::pow (weight, nrGroundings) << endl;
|
||||||
return Globals::logDomain
|
return Globals::logDomain
|
||||||
? weight * nrGroundings
|
? weight * nrGroundings
|
||||||
: std::pow (weight, nrGroundings);
|
: std::pow (weight, nrGroundings);
|
||||||
@ -124,7 +123,6 @@ LeafNode::weight (void) const
|
|||||||
double
|
double
|
||||||
SmoothNode::weight (void) const
|
SmoothNode::weight (void) const
|
||||||
{
|
{
|
||||||
// TODO and what happens if smoothing contains ipg or counted lvs ?
|
|
||||||
Clauses cs = clauses();
|
Clauses cs = clauses();
|
||||||
double totalWeight = LogAware::multIdenty();
|
double totalWeight = LogAware::multIdenty();
|
||||||
for (size_t i = 0; i < cs.size(); i++) {
|
for (size_t i = 0; i < cs.size(); i++) {
|
||||||
@ -140,26 +138,26 @@ SmoothNode::weight (void) const
|
|||||||
ct.project (lvs);
|
ct.project (lvs);
|
||||||
nrGroundings = ct.size();
|
nrGroundings = ct.size();
|
||||||
}
|
}
|
||||||
cout << "calc smooth weight for " << cs[i] << endl;
|
// cout << "calc smooth weight for " << cs[i] << endl;
|
||||||
if (cs[i].positiveCountedLogVars().empty() == false) {
|
if (cs[i].positiveCountedLogVars().empty() == false) {
|
||||||
cout << " -> nr pos = " << SetOrNode::nrPositives() << endl;
|
// cout << " -> nr pos = " << SetOrNode::nrPositives() << endl;
|
||||||
nrGroundings *= std::pow (SetOrNode::nrPositives(),
|
nrGroundings *= std::pow (SetOrNode::nrPositives(),
|
||||||
cs[i].nrPositiveCountedLogVars());
|
cs[i].nrPositiveCountedLogVars());
|
||||||
}
|
}
|
||||||
if (cs[i].negativeCountedLogVars().empty() == false) {
|
if (cs[i].negativeCountedLogVars().empty() == false) {
|
||||||
cout << " -> nr neg = " << SetOrNode::nrNegatives() << endl;
|
// cout << " -> nr neg = " << SetOrNode::nrNegatives() << endl;
|
||||||
nrGroundings *= std::pow (SetOrNode::nrNegatives(),
|
nrGroundings *= std::pow (SetOrNode::nrNegatives(),
|
||||||
cs[i].nrNegativeCountedLogVars());
|
cs[i].nrNegativeCountedLogVars());
|
||||||
}
|
}
|
||||||
cout << " -> pos+neg = " << posWeight + negWeight << endl;
|
// cout << " -> pos+neg = " << posWeight + negWeight << endl;
|
||||||
cout << " -> nrgroun = " << nrGroundings << endl;
|
// cout << " -> nrgroun = " << nrGroundings << endl;
|
||||||
if (Globals::logDomain) {
|
if (Globals::logDomain) {
|
||||||
// TODO i think i have to do log on nrGrounginds here!
|
totalWeight += (Util::logSum (posWeight, negWeight)
|
||||||
totalWeight += (Util::logSum (posWeight, negWeight) * nrGroundings);
|
* std::log (nrGroundings));
|
||||||
} else {
|
} else {
|
||||||
totalWeight *= std::pow (posWeight + negWeight, nrGroundings);
|
totalWeight *= std::pow (posWeight + negWeight, nrGroundings);
|
||||||
}
|
}
|
||||||
cout << " -> smooth weight = " << totalWeight << endl;
|
// cout << " -> smooth weight = " << totalWeight << endl;
|
||||||
}
|
}
|
||||||
return totalWeight;
|
return totalWeight;
|
||||||
}
|
}
|
||||||
@ -337,7 +335,7 @@ LiftedCircuit::tryIndependence (
|
|||||||
if (clauses.size() == 1) {
|
if (clauses.size() == 1) {
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
// TODO this independence is a little weak
|
// TODO compare all subsets with all subsets
|
||||||
for (size_t i = 0; i < clauses.size(); i++) {
|
for (size_t i = 0; i < clauses.size(); i++) {
|
||||||
bool indep = true;
|
bool indep = true;
|
||||||
TinySet<LiteralId> lids1 = clauses[i].lidSet();
|
TinySet<LiteralId> lids1 = clauses[i].lidSet();
|
||||||
@ -407,6 +405,7 @@ LiftedCircuit::tryInclusionExclusion (
|
|||||||
CircuitNode** follow,
|
CircuitNode** follow,
|
||||||
Clauses& clauses)
|
Clauses& clauses)
|
||||||
{
|
{
|
||||||
|
// TODO compare all subsets with all subsets
|
||||||
for (size_t i = 0; i < clauses.size(); i++) {
|
for (size_t i = 0; i < clauses.size(); i++) {
|
||||||
const Literals& literals = clauses[i].literals();
|
const Literals& literals = clauses[i].literals();
|
||||||
for (size_t j = 0; j < literals.size(); j++) {
|
for (size_t j = 0; j < literals.size(); j++) {
|
||||||
@ -420,8 +419,7 @@ LiftedCircuit::tryInclusionExclusion (
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (indep) {
|
if (indep) {
|
||||||
// TODO i am almost sure that this will
|
// TODO this should be have to be count normalized too
|
||||||
// have to be count normalized too!
|
|
||||||
ConstraintTree really = clauses[i].constr();
|
ConstraintTree really = clauses[i].constr();
|
||||||
Clause c1 (really.projectedCopy (
|
Clause c1 (really.projectedCopy (
|
||||||
literals[j].logVars()));
|
literals[j].logVars()));
|
||||||
@ -489,6 +487,7 @@ LiftedCircuit::tryIndepPartialGroundingAux (
|
|||||||
ConstraintTree& ct,
|
ConstraintTree& ct,
|
||||||
vector<unsigned>& lvIndices)
|
vector<unsigned>& lvIndices)
|
||||||
{
|
{
|
||||||
|
// TODO check if the ipg log vars appears in the same positions
|
||||||
for (size_t j = 1; j < clauses.size(); j++) {
|
for (size_t j = 1; j < clauses.size(); j++) {
|
||||||
LogVarSet lvs2 = clauses[j].ipgCandidates();
|
LogVarSet lvs2 = clauses[j].ipgCandidates();
|
||||||
for (size_t k = 0; k < lvs2.size(); k++) {
|
for (size_t k = 0; k < lvs2.size(); k++) {
|
||||||
@ -516,15 +515,16 @@ LiftedCircuit::tryAtomCounting (
|
|||||||
for (size_t i = 0; i < clauses.size(); i++) {
|
for (size_t i = 0; i < clauses.size(); i++) {
|
||||||
Literals literals = clauses[i].literals();
|
Literals literals = clauses[i].literals();
|
||||||
for (size_t j = 0; j < literals.size(); j++) {
|
for (size_t j = 0; j < literals.size(); j++) {
|
||||||
if (literals[j].logVars().size() == 1) {
|
if (literals[j].logVars().size() == 1
|
||||||
// TODO check if not already in ipg and countedlvs
|
&& ! clauses[i].isIpgLogVar (literals[j].logVars().front())
|
||||||
|
&& ! clauses[i].isCountedLogVar (literals[j].logVars().front())) {
|
||||||
unsigned nrGroundings = clauses[i].constr().projectedCopy (
|
unsigned nrGroundings = clauses[i].constr().projectedCopy (
|
||||||
literals[j].logVars()).size();
|
literals[j].logVars()).size();
|
||||||
SetOrNode* setOrNode = new SetOrNode (nrGroundings, clauses);
|
SetOrNode* setOrNode = new SetOrNode (nrGroundings, clauses);
|
||||||
Clause c1 (clauses[i].constr().projectedCopy (literals[j].logVars()));
|
Clause c1 (clauses[i].constr().projectedCopy (literals[j].logVars()));
|
||||||
Clause c2 (clauses[i].constr().projectedCopy (literals[j].logVars()));
|
Clause c2 (clauses[i].constr().projectedCopy (literals[j].logVars()));
|
||||||
c1.addLiteral (literals[j]);
|
c1.addLiteral (literals[j]);
|
||||||
c2.addAndNegateLiteral (literals[j]);
|
c2.addLiteralNegated (literals[j]);
|
||||||
c1.addPositiveCountedLogVar (literals[j].logVars().front());
|
c1.addPositiveCountedLogVar (literals[j].logVars().front());
|
||||||
c2.addNegativeCountedLogVar (literals[j].logVars().front());
|
c2.addNegativeCountedLogVar (literals[j].logVars().front());
|
||||||
clauses.push_back (c1);
|
clauses.push_back (c1);
|
||||||
@ -737,7 +737,9 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
createSmoothNode (missingLids, casted->follow());
|
createSmoothNode (missingLids, casted->follow());
|
||||||
// TODO change propagLits to full lvs
|
for (size_t i = 0; i < propagLits.size(); i++) {
|
||||||
|
propagLits[i].setAllFullLogVars();
|
||||||
|
}
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -794,7 +796,7 @@ LiftedCircuit::createSmoothNode (
|
|||||||
c.addNegativeCountedLogVar (X);
|
c.addNegativeCountedLogVar (X);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
c.addAndNegateLiteral (c.literals()[0]);
|
c.addLiteralNegated (c.literals()[0]);
|
||||||
clauses.push_back (c);
|
clauses.push_back (c);
|
||||||
}
|
}
|
||||||
SmoothNode* smoothNode = new SmoothNode (clauses, *lwcnf_);
|
SmoothNode* smoothNode = new SmoothNode (clauses, *lwcnf_);
|
||||||
|
@ -193,6 +193,15 @@ Clause::isNegativeCountedLogVar (LogVar X) const
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
bool
|
||||||
|
Clause::isIpgLogVar (LogVar X) const
|
||||||
|
{
|
||||||
|
assert (constr_.logVarSet().contains (X));
|
||||||
|
return ipgLogVars_.contains (X);
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
TinySet<LiteralId>
|
TinySet<LiteralId>
|
||||||
Clause::lidSet (void) const
|
Clause::lidSet (void) const
|
||||||
{
|
{
|
||||||
@ -331,12 +340,12 @@ LiftedWCNF::LiftedWCNF (const ParfactorList& pfList)
|
|||||||
|
|
||||||
Clause c1 (names);
|
Clause c1 (names);
|
||||||
c1.addLiteral (Literal (0, LogVars() = {0}));
|
c1.addLiteral (Literal (0, LogVars() = {0}));
|
||||||
c1.addAndNegateLiteral (Literal (1, {0,1}));
|
c1.addLiteralNegated (Literal (1, {0,1}));
|
||||||
clauses_.push_back(c1);
|
clauses_.push_back(c1);
|
||||||
|
|
||||||
Clause c2 (names);
|
Clause c2 (names);
|
||||||
c2.addLiteral (Literal (0, LogVars()={0}));
|
c2.addLiteral (Literal (0, LogVars()={0}));
|
||||||
c2.addAndNegateLiteral (Literal (1, {1,0}));
|
c2.addLiteralNegated (Literal (1, {1,0}));
|
||||||
clauses_.push_back(c2);
|
clauses_.push_back(c2);
|
||||||
|
|
||||||
addWeight (0, 3.0, 4.0);
|
addWeight (0, 3.0, 4.0);
|
||||||
@ -415,8 +424,8 @@ LiftedWCNF::addIndicatorClauses (const ParfactorList& pfList)
|
|||||||
ConstraintTree tempConstr2 = *(*it)->constr();
|
ConstraintTree tempConstr2 = *(*it)->constr();
|
||||||
tempConstr2.project (formulas[i].logVars());
|
tempConstr2.project (formulas[i].logVars());
|
||||||
Clause clause2 (tempConstr2);
|
Clause clause2 (tempConstr2);
|
||||||
clause2.addAndNegateLiteral (Literal (clause.literals()[j]));
|
clause2.addLiteralNegated (Literal (clause.literals()[j]));
|
||||||
clause2.addAndNegateLiteral (Literal (clause.literals()[k]));
|
clause2.addLiteralNegated (Literal (clause.literals()[k]));
|
||||||
clauses_.push_back (clause2);
|
clauses_.push_back (clause2);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -451,12 +460,12 @@ LiftedWCNF::addParameterClauses (const ParfactorList& pfList)
|
|||||||
for (unsigned i = 0; i < groups.size(); i++) {
|
for (unsigned i = 0; i < groups.size(); i++) {
|
||||||
LiteralId lid = getLiteralId (groups[i], indexer[i]);
|
LiteralId lid = getLiteralId (groups[i], indexer[i]);
|
||||||
|
|
||||||
clause1.addAndNegateLiteral (
|
clause1.addLiteralNegated (
|
||||||
Literal (lid, (*it)->argument(i).logVars()));
|
Literal (lid, (*it)->argument(i).logVars()));
|
||||||
|
|
||||||
ConstraintTree ct = *(*it)->constr();
|
ConstraintTree ct = *(*it)->constr();
|
||||||
Clause tempClause (ct);
|
Clause tempClause (ct);
|
||||||
tempClause.addAndNegateLiteral (Literal (
|
tempClause.addLiteralNegated (Literal (
|
||||||
paramVarLid, (*it)->constr()->logVars()));
|
paramVarLid, (*it)->constr()->logVars()));
|
||||||
tempClause.addLiteral (Literal (lid, (*it)->argument(i).logVars()));
|
tempClause.addLiteral (Literal (lid, (*it)->argument(i).logVars()));
|
||||||
clauses_.push_back (tempClause);
|
clauses_.push_back (tempClause);
|
||||||
|
@ -68,8 +68,7 @@ class Clause
|
|||||||
|
|
||||||
void addLiteral (const Literal& l) { literals_.push_back (l); }
|
void addLiteral (const Literal& l) { literals_.push_back (l); }
|
||||||
|
|
||||||
// TODO kill me
|
void addLiteralNegated (const Literal& l)
|
||||||
void addAndNegateLiteral (const Literal& l)
|
|
||||||
{
|
{
|
||||||
literals_.push_back (l);
|
literals_.push_back (l);
|
||||||
literals_.back().negate();
|
literals_.back().negate();
|
||||||
@ -116,6 +115,8 @@ class Clause
|
|||||||
bool isPositiveCountedLogVar (LogVar X) const;
|
bool isPositiveCountedLogVar (LogVar X) const;
|
||||||
|
|
||||||
bool isNegativeCountedLogVar (LogVar X) const;
|
bool isNegativeCountedLogVar (LogVar X) const;
|
||||||
|
|
||||||
|
bool isIpgLogVar (LogVar X) const;
|
||||||
|
|
||||||
TinySet<LiteralId> lidSet (void) const;
|
TinySet<LiteralId> lidSet (void) const;
|
||||||
|
|
||||||
@ -165,6 +166,9 @@ class LiteralLvTypes
|
|||||||
LiteralId lid (void) const { return lid_; }
|
LiteralId lid (void) const { return lid_; }
|
||||||
|
|
||||||
const LogVarTypes& logVarTypes (void) const { return lvTypes_; }
|
const LogVarTypes& logVarTypes (void) const { return lvTypes_; }
|
||||||
|
|
||||||
|
void setAllFullLogVars (void) {
|
||||||
|
lvTypes_ = LogVarTypes (lvTypes_.size(), LogVarType::FULL_LV); }
|
||||||
|
|
||||||
private:
|
private:
|
||||||
LiteralId lid_;
|
LiteralId lid_;
|
||||||
|
Reference in New Issue
Block a user