2012-03-22 11:33:24 +00:00
|
|
|
#ifndef HORUS_PROBFORMULA_H
|
|
|
|
#define HORUS_PROBFORMULA_H
|
|
|
|
|
|
|
|
#include <limits>
|
|
|
|
|
|
|
|
#include "ConstraintTree.h"
|
|
|
|
#include "LiftedUtils.h"
|
|
|
|
#include "Horus.h"
|
|
|
|
|
|
|
|
|
2012-03-31 23:27:37 +01:00
|
|
|
|
2012-03-22 11:33:24 +00:00
|
|
|
class ProbFormula
|
|
|
|
{
|
|
|
|
public:
|
|
|
|
ProbFormula (Symbol f, const LogVars& lvs, unsigned range)
|
|
|
|
: functor_(f), logVars_(lvs), range_(range),
|
2012-03-31 23:27:37 +01:00
|
|
|
countedLogVar_(), group_(Util::maxUnsigned()) { }
|
2012-03-22 11:33:24 +00:00
|
|
|
|
2012-03-31 23:27:37 +01:00
|
|
|
ProbFormula (Symbol f, unsigned r)
|
|
|
|
: functor_(f), range_(r), group_(Util::maxUnsigned()) { }
|
2012-03-22 11:33:24 +00:00
|
|
|
|
|
|
|
Symbol functor (void) const { return functor_; }
|
|
|
|
|
|
|
|
unsigned arity (void) const { return logVars_.size(); }
|
|
|
|
|
|
|
|
unsigned range (void) const { return range_; }
|
|
|
|
|
|
|
|
LogVars& logVars (void) { return logVars_; }
|
|
|
|
|
|
|
|
const LogVars& logVars (void) const { return logVars_; }
|
|
|
|
|
|
|
|
LogVarSet logVarSet (void) const { return LogVarSet (logVars_); }
|
|
|
|
|
2012-03-31 23:27:37 +01:00
|
|
|
unsigned group (void) const { return group_; }
|
2012-03-22 11:33:24 +00:00
|
|
|
|
2012-03-31 23:27:37 +01:00
|
|
|
void setGroup (unsigned g) { group_ = g; }
|
2012-03-22 11:33:24 +00:00
|
|
|
|
|
|
|
bool sameSkeletonAs (const ProbFormula&) const;
|
|
|
|
|
|
|
|
bool contains (LogVar) const;
|
|
|
|
|
|
|
|
bool contains (LogVarSet) const;
|
|
|
|
|
|
|
|
bool isAtom (void) const;
|
|
|
|
|
|
|
|
bool isCounting (void) const;
|
|
|
|
|
|
|
|
LogVar countedLogVar (void) const;
|
|
|
|
|
|
|
|
void setCountedLogVar (LogVar);
|
|
|
|
|
|
|
|
void rename (LogVar, LogVar);
|
|
|
|
|
2012-03-31 23:27:37 +01:00
|
|
|
static unsigned getNewGroup (void);
|
2012-03-22 11:33:24 +00:00
|
|
|
|
2012-03-31 23:27:37 +01:00
|
|
|
friend std::ostream& operator<< (ostream &os, const ProbFormula& f);
|
2012-03-22 11:33:24 +00:00
|
|
|
|
2012-03-31 23:27:37 +01:00
|
|
|
friend bool operator== (const ProbFormula& f1, const ProbFormula& f2);
|
2012-03-22 11:33:24 +00:00
|
|
|
|
|
|
|
private:
|
2012-03-31 23:27:37 +01:00
|
|
|
Symbol functor_;
|
|
|
|
LogVars logVars_;
|
|
|
|
unsigned range_;
|
|
|
|
LogVar countedLogVar_;
|
|
|
|
unsigned group_;
|
|
|
|
static int freeGroup_;
|
2012-03-22 11:33:24 +00:00
|
|
|
};
|
|
|
|
|
|
|
|
typedef vector<ProbFormula> ProbFormulas;
|
|
|
|
|
|
|
|
|
2012-03-31 23:27:37 +01:00
|
|
|
class ObservedFormula
|
|
|
|
{
|
|
|
|
public:
|
|
|
|
ObservedFormula (Symbol f, unsigned a, unsigned ev)
|
|
|
|
: functor_(f), arity_(a), evidence_(ev), constr_(a) { }
|
|
|
|
|
|
|
|
ObservedFormula (Symbol f, unsigned ev, const Tuple& tuple)
|
|
|
|
: functor_(f), arity_(tuple.size()), evidence_(ev), constr_(arity_)
|
|
|
|
{
|
|
|
|
constr_.addTuple (tuple);
|
|
|
|
}
|
|
|
|
|
|
|
|
Symbol functor (void) const { return functor_; }
|
|
|
|
|
|
|
|
unsigned arity (void) const { return arity_; }
|
|
|
|
|
|
|
|
unsigned evidence (void) const { return evidence_; }
|
|
|
|
|
|
|
|
ConstraintTree& constr (void) { return constr_; }
|
|
|
|
|
|
|
|
bool isAtom (void) const { return arity_ == 0; }
|
|
|
|
|
|
|
|
void addTuple (const Tuple& tuple) { constr_.addTuple (tuple); }
|
|
|
|
|
|
|
|
friend ostream& operator<< (ostream &os, const ObservedFormula& of);
|
|
|
|
|
|
|
|
private:
|
|
|
|
Symbol functor_;
|
|
|
|
unsigned arity_;
|
|
|
|
unsigned evidence_;
|
|
|
|
ConstraintTree constr_;
|
|
|
|
};
|
|
|
|
|
|
|
|
typedef vector<ObservedFormula> ObservedFormulas;
|
|
|
|
|
2012-03-22 11:33:24 +00:00
|
|
|
#endif // HORUS_PROBFORMULA_H
|
|
|
|
|