This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/packages/CLPBN/horus/LiftedWCNF.h

238 lines
5.8 KiB
C
Raw Normal View History

#ifndef HORUS_LIFTEDWCNF_H
#define HORUS_LIFTEDWCNF_H
#include "ParfactorList.h"
using namespace std;
typedef long LiteralId;
class ConstraintTree;
2012-10-31 23:43:39 +00:00
enum LogVarType
{
FULL_LV,
POS_LV,
NEG_LV
};
typedef vector<LogVarType> LogVarTypes;
2012-11-07 15:28:33 +00:00
class Literal
{
public:
Literal (LiteralId lid, const LogVars& lvs) :
lid_(lid), logVars_(lvs), negated_(false) { }
Literal (const Literal& lit, bool negated) :
lid_(lit.lid_), logVars_(lit.logVars_), negated_(negated) { }
LiteralId lid (void) const { return lid_; }
2012-10-24 21:22:49 +01:00
LogVars logVars (void) const { return logVars_; }
2012-12-17 18:39:42 +00:00
size_t nrLogVars (void) const { return logVars_.size(); }
2012-11-07 15:28:33 +00:00
LogVarSet logVarSet (void) const { return LogVarSet (logVars_); }
2012-12-17 18:39:42 +00:00
2012-11-07 15:28:33 +00:00
void complement (void) { negated_ = !negated_; }
bool isPositive (void) const { return negated_ == false; }
bool isNegative (void) const { return negated_; }
2012-12-17 18:39:42 +00:00
bool isGround (ConstraintTree constr, LogVarSet ipgLogVars) const;
2012-12-17 18:39:42 +00:00
size_t indexOfLogVar (LogVar X) const;
2012-10-31 23:43:39 +00:00
string toString (LogVarSet ipgLogVars = LogVarSet(),
LogVarSet posCountedLvs = LogVarSet(),
LogVarSet negCountedLvs = LogVarSet()) const;
2012-11-07 15:28:33 +00:00
friend std::ostream& operator<< (std::ostream &os, const Literal& lit);
private:
2012-11-07 15:28:33 +00:00
LiteralId lid_;
LogVars logVars_;
bool negated_;
};
typedef vector<Literal> Literals;
2012-10-31 23:58:07 +00:00
class Clause
{
public:
2012-11-07 18:43:13 +00:00
Clause (const ConstraintTree& ct = ConstraintTree({})) : constr_(ct) { }
2012-10-31 23:58:07 +00:00
2012-10-31 23:43:39 +00:00
Clause (vector<vector<string>> names) : constr_(ConstraintTree (names)) { }
2012-10-31 23:58:07 +00:00
void addLiteral (const Literal& l) { literals_.push_back (l); }
2012-10-31 23:58:07 +00:00
2012-11-07 15:28:33 +00:00
const Literals& literals (void) const { return literals_; }
2012-12-17 18:39:42 +00:00
Literals& literals (void) { return literals_; }
2012-12-17 18:39:42 +00:00
size_t nrLiterals (void) const { return literals_.size(); }
2012-10-31 23:58:07 +00:00
const ConstraintTree& constr (void) const { return constr_; }
2012-10-31 23:58:07 +00:00
ConstraintTree constr (void) { return constr_; }
2012-10-31 23:58:07 +00:00
bool isUnit (void) const { return literals_.size() == 1; }
2012-10-31 23:58:07 +00:00
LogVarSet ipgLogVars (void) const { return ipgLvs_; }
2012-10-31 23:58:07 +00:00
void addIpgLogVar (LogVar X) { ipgLvs_.insert (X); }
2012-10-31 23:58:07 +00:00
2012-11-07 15:28:33 +00:00
void addPosCountedLogVar (LogVar X) { posCountedLvs_.insert (X); }
2012-10-31 23:43:39 +00:00
2012-11-07 15:28:33 +00:00
void addNegCountedLogVar (LogVar X) { negCountedLvs_.insert (X); }
2012-10-31 23:58:07 +00:00
2012-11-07 15:28:33 +00:00
LogVarSet posCountedLogVars (void) const { return posCountedLvs_; }
2012-11-07 15:28:33 +00:00
LogVarSet negCountedLogVars (void) const { return negCountedLvs_; }
2012-11-07 15:28:33 +00:00
unsigned nrPosCountedLogVars (void) const { return posCountedLvs_.size(); }
2012-11-07 15:28:33 +00:00
unsigned nrNegCountedLogVars (void) const { return negCountedLvs_.size(); }
2012-12-17 18:39:42 +00:00
2012-11-07 15:28:33 +00:00
void addLiteralComplemented (const Literal& lit);
2012-10-31 23:58:07 +00:00
bool containsLiteral (LiteralId lid) const;
bool containsPositiveLiteral (LiteralId lid, const LogVarTypes&) const;
bool containsNegativeLiteral (LiteralId lid, const LogVarTypes&) const;
void removeLiterals (LiteralId lid);
void removePositiveLiterals (LiteralId lid, const LogVarTypes&);
void removeNegativeLiterals (LiteralId lid, const LogVarTypes&);
2012-10-31 23:43:39 +00:00
bool isCountedLogVar (LogVar X) const;
2012-10-31 23:58:07 +00:00
2012-10-31 23:43:39 +00:00
bool isPositiveCountedLogVar (LogVar X) const;
2012-12-17 18:39:42 +00:00
bool isNegativeCountedLogVar (LogVar X) const;
2012-11-06 15:56:52 +00:00
bool isIpgLogVar (LogVar X) const;
2012-10-31 23:58:07 +00:00
TinySet<LiteralId> lidSet (void) const;
LogVarSet ipgCandidates (void) const;
2012-10-31 23:43:39 +00:00
LogVarTypes logVarTypes (size_t litIdx) const;
2012-10-31 23:58:07 +00:00
void removeLiteral (size_t litIdx);
2012-12-17 18:39:42 +00:00
static bool independentClauses (Clause& c1, Clause& c2);
2012-12-17 18:39:42 +00:00
static vector<Clause*> copyClauses (const vector<Clause*>& clauses);
static void printClauses (const vector<Clause*>& clauses);
2012-12-17 18:39:42 +00:00
2012-10-31 23:58:07 +00:00
friend std::ostream& operator<< (ostream &os, const Clause& clause);
2012-10-30 00:21:10 +00:00
private:
LogVarSet getLogVarSetExcluding (size_t idx) const;
2012-11-07 15:28:33 +00:00
Literals literals_;
LogVarSet ipgLvs_;
2012-10-31 23:43:39 +00:00
LogVarSet posCountedLvs_;
LogVarSet negCountedLvs_;
ConstraintTree constr_;
};
typedef vector<Clause*> Clauses;
2012-11-07 15:28:33 +00:00
class LitLvTypes
{
public:
2012-11-07 15:28:33 +00:00
struct CompareLitLvTypes
{
bool operator() (
2012-11-07 15:28:33 +00:00
const LitLvTypes& types1,
const LitLvTypes& types2) const
{
if (types1.lid_ < types2.lid_) {
return true;
}
2012-12-10 19:37:41 +00:00
if (types1.lid_ == types2.lid_) {
return types1.lvTypes_ < types2.lvTypes_;
}
return false;
}
};
2012-12-17 18:39:42 +00:00
2012-11-07 15:28:33 +00:00
LitLvTypes (LiteralId lid, const LogVarTypes& lvTypes) :
lid_(lid), lvTypes_(lvTypes) { }
2012-12-17 18:39:42 +00:00
LiteralId lid (void) const { return lid_; }
2012-12-17 18:39:42 +00:00
const LogVarTypes& logVarTypes (void) const { return lvTypes_; }
2012-12-17 18:39:42 +00:00
2012-11-06 15:56:52 +00:00
void setAllFullLogVars (void) {
2012-11-07 15:28:33 +00:00
std::fill (lvTypes_.begin(), lvTypes_.end(), LogVarType::FULL_LV); }
2012-12-10 18:48:54 +00:00
friend std::ostream& operator<< (std::ostream &os, const LitLvTypes& lit);
private:
LiteralId lid_;
LogVarTypes lvTypes_;
};
2012-11-07 15:28:33 +00:00
typedef TinySet<LitLvTypes,LitLvTypes::CompareLitLvTypes> LitLvTypesSet;
class LiftedWCNF
{
public:
LiftedWCNF (const ParfactorList& pfList);
~LiftedWCNF (void);
const Clauses& clauses (void) const { return clauses_; }
void addWeight (LiteralId lid, double posW, double negW);
2012-11-07 15:28:33 +00:00
double posWeight (LiteralId lid) const;
2012-11-07 15:28:33 +00:00
double negWeight (LiteralId lid) const;
vector<LiteralId> prvGroupLiterals (PrvGroup prvGroup);
Clause* createClause (LiteralId lid) const;
void printFormulaIndicators (void) const;
void printWeights (void) const;
void printClauses (void) const;
private:
2012-11-07 15:28:33 +00:00
LiteralId getLiteralId (PrvGroup prvGroup, unsigned range);
void addIndicatorClauses (const ParfactorList& pfList);
void addParameterClauses (const ParfactorList& pfList);
2012-11-07 15:28:33 +00:00
Clauses clauses_;
LiteralId freeLiteralId_;
2012-12-17 18:39:42 +00:00
const ParfactorList& pfList_;
2012-11-07 15:28:33 +00:00
unordered_map<PrvGroup, vector<LiteralId>> map_;
unordered_map<LiteralId, std::pair<double,double>> weights_;
};
#endif // HORUS_LIFTEDWCNF_H
2012-10-24 21:22:49 +01:00