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

249 lines
6.0 KiB
C
Raw Normal View History

2013-02-07 17:50:02 +00:00
#ifndef YAP_PACKAGES_CLPBN_HORUS_LIFTEDWCNF_H_
#define YAP_PACKAGES_CLPBN_HORUS_LIFTEDWCNF_H_
2013-02-07 20:09:10 +00:00
#include <vector>
2012-12-27 12:54:58 +00:00
#include <unordered_map>
2013-02-07 20:09:10 +00:00
#include <string>
#include <ostream>
2012-12-27 12:54:58 +00:00
2013-02-08 12:12:45 +00:00
#include "ConstraintTree.h"
#include "ProbFormula.h"
#include "LiftedUtils.h"
namespace Horus {
2013-02-07 23:53:13 +00:00
2013-02-08 12:12:45 +00:00
class ParfactorList;
enum class LogVarType {
fullLvt,
posLvt,
negLvt
};
2012-10-31 23:43:39 +00:00
2013-02-07 13:37:15 +00:00
typedef long LiteralId;
typedef std::vector<LogVarType> LogVarTypes;
2012-11-07 15:28:33 +00:00
class Literal {
public:
2013-02-08 12:12:45 +00:00
Literal (LiteralId lid, const LogVars& lvs)
: lid_(lid), logVars_(lvs), negated_(false) { }
2013-02-08 12:12:45 +00:00
Literal (const Literal& lit, bool negated)
: lid_(lit.lid_), logVars_(lit.logVars_), negated_(negated) { }
LiteralId lid() const { return lid_; }
LogVars logVars() const { return logVars_; }
2012-12-17 18:39:42 +00:00
size_t nrLogVars() const { return logVars_.size(); }
LogVarSet logVarSet() const { return LogVarSet (logVars_); }
2012-12-17 18:39:42 +00:00
void complement() { negated_ = !negated_; }
bool isPositive() const { return negated_ == false; }
bool isNegative() const { return negated_; }
2012-12-17 18:39:42 +00:00
2013-02-08 12:12:45 +00:00
bool isGround (ConstraintTree constr, const LogVarSet& ipgLogVars) const;
2012-12-17 18:39:42 +00:00
size_t indexOfLogVar (LogVar X) const;
2013-02-08 12:12:45 +00:00
std::string toString (
LogVarSet ipgLogVars = LogVarSet(),
LogVarSet posCountedLvs = LogVarSet(),
LogVarSet negCountedLvs = LogVarSet()) const;
private:
friend std::ostream& operator<< (std::ostream&, const Literal&);
2012-11-07 15:28:33 +00:00
LiteralId lid_;
LogVars logVars_;
bool negated_;
};
2013-02-07 13:37:15 +00:00
typedef std::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
2013-02-07 13:37:15 +00:00
Clause (std::vector<std::vector<std::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
const Literals& literals() const { return literals_; }
2012-12-17 18:39:42 +00:00
Literals& literals() { return literals_; }
2012-12-17 18:39:42 +00:00
size_t nrLiterals() const { return literals_.size(); }
2012-10-31 23:58:07 +00:00
const ConstraintTree& constr() const { return constr_; }
2012-10-31 23:58:07 +00:00
ConstraintTree constr() { return constr_; }
2012-10-31 23:58:07 +00:00
bool isUnit() const { return literals_.size() == 1; }
2012-10-31 23:58:07 +00:00
LogVarSet ipgLogVars() 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
LogVarSet posCountedLogVars() const { return posCountedLvs_; }
LogVarSet negCountedLogVars() const { return negCountedLvs_; }
unsigned nrPosCountedLogVars() const { return posCountedLvs_.size(); }
unsigned nrNegCountedLogVars() 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;
TinySet<LiteralId> lidSet() const;
2012-10-31 23:58:07 +00:00
LogVarSet ipgCandidates() const;
2012-10-31 23:58:07 +00:00
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
2013-02-07 13:37:15 +00:00
static std::vector<Clause*> copyClauses (
const std::vector<Clause*>& clauses);
2013-02-07 13:37:15 +00:00
static void printClauses (const std::vector<Clause*>& clauses);
2012-12-17 18:39:42 +00:00
2013-02-07 13:37:15 +00:00
static void deleteClauses (std::vector<Clause*>& clauses);
2012-12-19 17:45:53 +00:00
2012-10-30 00:21:10 +00:00
private:
LogVarSet getLogVarSetExcluding (size_t idx) const;
friend std::ostream& operator<< (std::ostream&, const Clause&);
Literals literals_;
LogVarSet ipgLvs_;
LogVarSet posCountedLvs_;
LogVarSet negCountedLvs_;
ConstraintTree constr_;
2012-12-27 22:25:45 +00:00
DISALLOW_ASSIGN (Clause);
};
2013-02-07 13:37:15 +00:00
typedef std::vector<Clause*> Clauses;
class LitLvTypes {
public:
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() const { return lid_; }
2012-12-17 18:39:42 +00:00
const LogVarTypes& logVarTypes() const { return lvTypes_; }
2012-12-17 18:39:42 +00:00
void setAllFullLogVars();
private:
friend std::ostream& operator<< (std::ostream&, const LitLvTypes&);
LiteralId lid_;
LogVarTypes lvTypes_;
};
struct CmpLitLvTypes
{
2013-02-08 01:11:18 +00:00
bool operator() (
const LitLvTypes& types1,
const LitLvTypes& types2) const
{
if (types1.lid() < types2.lid()) {
return true;
}
if (types1.lid() == types2.lid()){
return types1.logVarTypes() < types2.logVarTypes();
}
return false;
}
};
typedef TinySet<LitLvTypes, CmpLitLvTypes> LitLvTypesSet;
class LiftedWCNF {
public:
LiftedWCNF (const ParfactorList& pfList);
~LiftedWCNF();
const Clauses& clauses() 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;
2013-02-07 13:37:15 +00:00
std::vector<LiteralId> prvGroupLiterals (PrvGroup prvGroup);
Clause* createClause (LiteralId lid) const;
void printFormulaIndicators() const;
void printWeights() const;
void printClauses() 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);
2013-02-07 13:37:15 +00:00
Clauses clauses_;
LiteralId freeLiteralId_;
const ParfactorList& pfList_;
std::unordered_map<PrvGroup, std::vector<LiteralId>> map_;
std::unordered_map<LiteralId, std::pair<double,double>> weights_;
2012-12-27 22:25:45 +00:00
DISALLOW_COPY_AND_ASSIGN (LiftedWCNF);
};
} // namespace Horus
2013-02-07 23:53:13 +00:00
2013-02-08 00:20:01 +00:00
#endif // YAP_PACKAGES_CLPBN_HORUS_LIFTEDWCNF_H_
2012-10-24 21:22:49 +01:00