support model counting on atom couting nodes - still untested

This commit is contained in:
Tiago Gomes
2012-11-01 22:34:28 +00:00
parent d4912ea219
commit a1d0deb638
4 changed files with 91 additions and 56 deletions

View File

@@ -25,36 +25,36 @@ class Literal
public:
Literal (LiteralId lid, double w = -1.0) :
lid_(lid), weight_(w), negated_(false) { }
Literal (LiteralId lid, const LogVars& lvs, double w = -1.0) :
lid_(lid), logVars_(lvs), weight_(w), negated_(false) { }
Literal (const Literal& lit, bool negated) :
lid_(lit.lid_), logVars_(lit.logVars_), weight_(lit.weight_), negated_(negated) { }
LiteralId lid (void) const { return lid_; }
LogVars logVars (void) const { return logVars_; }
LogVarSet logVarSet (void) const { return LogVarSet (logVars_); }
// FIXME this is not log aware :(
double weight (void) const { return weight_ < 0.0 ? 1.0 : weight_; }
void negate (void) { negated_ = !negated_; }
bool isPositive (void) const { return negated_ == false; }
bool isNegative (void) const { return negated_; }
bool isGround (ConstraintTree constr, LogVarSet ipgLogVars) const;
string toString (LogVarSet ipgLogVars = LogVarSet(),
LogVarSet posCountedLvs = LogVarSet(),
LogVarSet negCountedLvs = LogVarSet()) const;
friend std::ostream& operator<< (ostream &os, const Literal& lit);
private:
LiteralId lid_;
LogVars logVars_;
@@ -81,7 +81,7 @@ class Clause
literals_.push_back (l);
literals_.back().negate();
}
const vector<Literal>& literals (void) const { return literals_; }
const ConstraintTree& constr (void) const { return constr_; }
@@ -98,6 +98,10 @@ class Clause
void addNegativeCountedLogVar (LogVar X) { negCountedLvs_.insert (X); }
LogVarSet positiveCountedLogVars (void) const { return posCountedLvs_; }
LogVarSet negativeCountedLogVars (void) const { return negCountedLvs_; }
bool containsLiteral (LiteralId lid) const;
bool containsPositiveLiteral (LiteralId lid, const LogVarTypes&) const;
@@ -115,26 +119,26 @@ class Clause
bool isPositiveCountedLogVar (LogVar X) const;
bool isNegativeCountedLogVar (LogVar X) const;
TinySet<LiteralId> lidSet (void) const;
LogVarSet ipgCandidates (void) const;
LogVarTypes logVarTypes (size_t litIdx) const;
void removeLiteral (size_t litIdx);
static void printClauses (const vector<Clause>& clauses);
friend std::ostream& operator<< (ostream &os, const Clause& clause);
private:
LogVarSet getLogVarSetExcluding (size_t idx) const;
vector<Literal> literals_;
LogVarSet ipgLogVars_;
LogVarSet posCountedLvs_;
LogVarSet negCountedLvs_;
LogVarSet negCountedLvs_;
ConstraintTree constr_;
};
@@ -146,19 +150,19 @@ class LiftedWCNF
{
public:
LiftedWCNF (const ParfactorList& pfList);
~LiftedWCNF (void);
const Clauses& clauses (void) const { return clauses_; }
Clause createClauseForLiteral (LiteralId lid) const;
void printFormulaIndicators (void) const;
void printWeights (void) const;
void printClauses (void) const;
private:
void addIndicatorClauses (const ParfactorList& pfList);
@@ -171,11 +175,11 @@ class LiftedWCNF
}
Clauses clauses_;
unordered_map<PrvGroup, vector<LiteralId>> map_;
const ParfactorList& pfList_;
LiteralId freeLiteralId_;
};