2013-02-07 17:50:02 +00:00
|
|
|
#ifndef YAP_PACKAGES_CLPBN_HORUS_CONSTRAINTTREE_H_
|
|
|
|
#define YAP_PACKAGES_CLPBN_HORUS_CONSTRAINTTREE_H_
|
2012-05-23 14:56:01 +01:00
|
|
|
|
|
|
|
#include <cassert>
|
|
|
|
|
2013-02-07 20:09:10 +00:00
|
|
|
#include <vector>
|
|
|
|
#include <algorithm>
|
|
|
|
#include <string>
|
2012-05-23 14:56:01 +01:00
|
|
|
|
|
|
|
#include "TinySet.h"
|
|
|
|
#include "LiftedUtils.h"
|
|
|
|
|
|
|
|
|
2013-02-08 21:12:46 +00:00
|
|
|
namespace Horus {
|
2013-02-07 23:53:13 +00:00
|
|
|
|
2012-05-23 14:56:01 +01:00
|
|
|
class CTNode;
|
|
|
|
class ConstraintTree;
|
2013-02-07 22:37:45 +00:00
|
|
|
|
|
|
|
|
2013-02-08 01:11:18 +00:00
|
|
|
typedef std::vector<CTNode*> CTNodes;
|
|
|
|
typedef std::vector<ConstraintTree*> ConstraintTrees;
|
2012-05-23 14:56:01 +01:00
|
|
|
|
|
|
|
|
2013-03-09 19:41:17 +00:00
|
|
|
struct CmpSymbol {
|
|
|
|
bool operator() (const CTNode* n1, const CTNode* n2) const;
|
2012-05-23 14:56:01 +01:00
|
|
|
};
|
|
|
|
|
|
|
|
|
2013-03-09 19:41:17 +00:00
|
|
|
typedef TinySet<CTNode*, CmpSymbol> CTChilds;
|
2013-02-06 00:24:02 +00:00
|
|
|
|
|
|
|
|
2013-02-13 14:26:47 +00:00
|
|
|
class ConstraintTree {
|
2012-05-23 14:56:01 +01:00
|
|
|
public:
|
|
|
|
ConstraintTree (unsigned);
|
|
|
|
|
|
|
|
ConstraintTree (const LogVars&);
|
|
|
|
|
|
|
|
ConstraintTree (const LogVars&, const Tuples&);
|
2012-12-17 18:39:42 +00:00
|
|
|
|
2013-02-07 13:37:15 +00:00
|
|
|
ConstraintTree (std::vector<std::vector<std::string>> names);
|
2012-05-23 14:56:01 +01:00
|
|
|
|
|
|
|
ConstraintTree (const ConstraintTree&);
|
|
|
|
|
2013-02-06 00:24:02 +00:00
|
|
|
ConstraintTree (const CTChilds& rootChilds, const LogVars& logVars);
|
2012-05-23 14:56:01 +01:00
|
|
|
|
2013-02-28 19:45:37 +00:00
|
|
|
~ConstraintTree();
|
2012-05-23 14:56:01 +01:00
|
|
|
|
2013-02-28 19:45:37 +00:00
|
|
|
CTNode* root() const { return root_; }
|
2012-12-17 18:39:42 +00:00
|
|
|
|
2013-03-09 19:41:17 +00:00
|
|
|
bool empty() const;
|
2012-05-23 14:56:01 +01:00
|
|
|
|
2013-02-28 19:45:37 +00:00
|
|
|
const LogVars& logVars() const;
|
2012-05-23 14:56:01 +01:00
|
|
|
|
2013-02-28 19:45:37 +00:00
|
|
|
const LogVarSet& logVarSet() const;
|
2012-12-17 18:39:42 +00:00
|
|
|
|
2013-02-28 19:45:37 +00:00
|
|
|
size_t nrLogVars() const;
|
2012-12-17 18:39:42 +00:00
|
|
|
|
2012-05-23 14:56:01 +01:00
|
|
|
void addTuple (const Tuple&);
|
2012-12-17 18:39:42 +00:00
|
|
|
|
2012-05-23 14:56:01 +01:00
|
|
|
bool containsTuple (const Tuple&);
|
2012-12-17 18:39:42 +00:00
|
|
|
|
2012-05-23 14:56:01 +01:00
|
|
|
void moveToTop (const LogVars&);
|
|
|
|
|
|
|
|
void moveToBottom (const LogVars&);
|
|
|
|
|
|
|
|
void join (ConstraintTree*, bool oneTwoOne = false);
|
|
|
|
|
|
|
|
unsigned getLevel (LogVar) const;
|
|
|
|
|
|
|
|
void rename (LogVar, LogVar);
|
|
|
|
|
|
|
|
void applySubstitution (const Substitution&);
|
|
|
|
|
|
|
|
void project (const LogVarSet&);
|
2012-12-17 18:39:42 +00:00
|
|
|
|
2012-10-29 21:37:58 +00:00
|
|
|
ConstraintTree projectedCopy (const LogVarSet&);
|
2012-05-23 14:56:01 +01:00
|
|
|
|
|
|
|
void remove (const LogVarSet&);
|
|
|
|
|
|
|
|
bool isSingleton (LogVar);
|
|
|
|
|
2013-02-28 19:45:37 +00:00
|
|
|
LogVarSet singletons();
|
2012-05-23 14:56:01 +01:00
|
|
|
|
|
|
|
TupleSet tupleSet (unsigned = 0) const;
|
|
|
|
|
|
|
|
TupleSet tupleSet (const LogVars&);
|
|
|
|
|
2013-02-28 19:45:37 +00:00
|
|
|
unsigned size() const;
|
2012-05-23 14:56:01 +01:00
|
|
|
|
|
|
|
unsigned nrSymbols (LogVar);
|
|
|
|
|
|
|
|
void exportToGraphViz (const char*, bool = false) const;
|
|
|
|
|
|
|
|
bool isCountNormalized (const LogVarSet&);
|
|
|
|
|
|
|
|
unsigned getConditionalCount (const LogVarSet&);
|
|
|
|
|
|
|
|
TinySet<unsigned> getConditionalCounts (const LogVarSet&);
|
|
|
|
|
|
|
|
bool isCartesianProduct (const LogVarSet&);
|
|
|
|
|
|
|
|
std::pair<ConstraintTree*, ConstraintTree*> split (const Tuple&);
|
|
|
|
|
|
|
|
std::pair<ConstraintTree*, ConstraintTree*> split (
|
|
|
|
const LogVars&, ConstraintTree*, const LogVars&);
|
|
|
|
|
|
|
|
ConstraintTrees countNormalize (const LogVarSet&);
|
|
|
|
|
|
|
|
ConstraintTrees jointCountNormalize (
|
|
|
|
ConstraintTree*, ConstraintTree*, LogVar, LogVar, LogVar);
|
|
|
|
|
|
|
|
LogVars expand (LogVar);
|
|
|
|
|
|
|
|
ConstraintTrees ground (LogVar);
|
|
|
|
|
2012-12-18 23:51:51 +00:00
|
|
|
void cloneLogVar (LogVar, LogVar);
|
2012-12-17 18:39:42 +00:00
|
|
|
|
2012-10-30 00:15:40 +00:00
|
|
|
ConstraintTree& operator= (const ConstraintTree& ct);
|
2012-12-17 18:39:42 +00:00
|
|
|
|
2012-05-23 14:56:01 +01:00
|
|
|
private:
|
|
|
|
unsigned countTuples (const CTNode*) const;
|
|
|
|
|
|
|
|
CTNodes getNodesBelow (CTNode*) const;
|
|
|
|
|
|
|
|
CTNodes getNodesAtLevel (unsigned) const;
|
|
|
|
|
|
|
|
unsigned nrNodes (const CTNode* n) const;
|
|
|
|
|
|
|
|
void appendOnBottom (CTNode* n1, const CTChilds&);
|
|
|
|
|
|
|
|
void swapLogVar (LogVar);
|
|
|
|
|
2012-05-24 22:55:20 +01:00
|
|
|
bool join (CTNode*, const Tuple&, size_t, CTNode*);
|
2012-05-23 14:56:01 +01:00
|
|
|
|
|
|
|
void getTuples (CTNode*, Tuples, unsigned, Tuples&, CTNodes&) const;
|
|
|
|
|
2013-02-07 13:37:15 +00:00
|
|
|
std::vector<std::pair<CTNode*, unsigned>> countNormalize (
|
2012-05-23 14:56:01 +01:00
|
|
|
const CTNode*, unsigned);
|
|
|
|
|
2013-02-13 14:26:47 +00:00
|
|
|
static void split (CTNode*, CTNode*, CTChilds&, CTChilds&, unsigned);
|
2012-05-23 14:56:01 +01:00
|
|
|
|
|
|
|
CTNode* root_;
|
|
|
|
LogVars logVars_;
|
|
|
|
LogVarSet logVarSet_;
|
|
|
|
};
|
|
|
|
|
|
|
|
|
2013-02-06 00:24:02 +00:00
|
|
|
|
|
|
|
inline const LogVars&
|
2013-02-28 19:45:37 +00:00
|
|
|
ConstraintTree::logVars() const
|
2013-02-06 00:24:02 +00:00
|
|
|
{
|
|
|
|
assert (LogVarSet (logVars_) == logVarSet_);
|
|
|
|
return logVars_;
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
inline const LogVarSet&
|
2013-02-28 19:45:37 +00:00
|
|
|
ConstraintTree::logVarSet() const
|
2013-02-06 00:24:02 +00:00
|
|
|
{
|
|
|
|
assert (LogVarSet (logVars_) == logVarSet_);
|
|
|
|
return logVarSet_;
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
inline size_t
|
2013-02-28 19:45:37 +00:00
|
|
|
ConstraintTree::nrLogVars() const
|
2013-02-06 00:24:02 +00:00
|
|
|
{
|
|
|
|
assert (LogVarSet (logVars_) == logVarSet_);
|
2013-02-13 23:47:00 +00:00
|
|
|
return logVars_.size();
|
2013-02-06 00:24:02 +00:00
|
|
|
}
|
|
|
|
|
2013-02-08 21:12:46 +00:00
|
|
|
} // namespace Horus
|
2013-02-07 23:53:13 +00:00
|
|
|
|
2013-02-08 00:20:01 +00:00
|
|
|
#endif // YAP_PACKAGES_CLPBN_HORUS_CONSTRAINTTREE_H_
|
2012-05-23 14:56:01 +01:00
|
|
|
|