1 #ifndef __DIADES__SDMDL__FORMULA_HH 2 #define __DIADES__SDMDL__FORMULA_HH 5 #include <unordered_map> 28 using std::unordered_map;
69 return "Diades::Sdmdl::Formula";
123 _support(), _supportNotComputed(true), _value() {
134 _bdd(bdd), _dataIndex(index), _owner(&owner), _support(), _supportNotComputed(true), _value() {
149 void getModels(FormulaVector & models)
const;
245 void primes(FormulaVector & result)
const;
266 return !(*
this == f);
464 _box.push_back(formula);
468 return _box.back().get();
473 _box.push_back(formula);
573 void newCubeNode(
unsigned i);
582 _assignment.push_back(assignment);
592 _value.push_back(value);
602 if (_assignment.empty()) {
605 return _assignment[0];
615 if (_value.empty()) {
631 Pointer chain(
const vector<int> & cube,
632 unsigned lower,
unsigned upper);
642 if (_children.size() > i) {
655 return _children.size() > i && _children[i] !=
nullptr;
663 void print(
unsigned level)
const;
671 return "Diades::Sdmdl::FormulaFactory";
773 const Formula & newFormula(
int * cube);
805 void extractAssignments(
int * cube,
const Variable & var, FormulaVector & assignments)
const;
835 return _varSet[0].get().domain().front().get().
owner().
nullValue();
902 void printInfoFactory()
const;
914 BDD getBDD(
bool positive, BDD var)
const;
921 void increment(vector<bool> & encoding)
const;
931 void bddFormulaToDot(DdNode * rootNode,
const string & fileName)
const;
952 Variable & getVariable(
const string & name);
972 return this == &factory;
982 require(Exception, valid(),
"bddManager: invalid factory");
993 require(Exception, valid(),
"bddManager: invalid factory");
1004 return _mgr !=
nullptr;
1016 void addVariables(
const vector<unsigned> & indexes,
VariableVector & variables)
const;
1029 const BDD & getPositiveCube(
const Variable & var)
const;
1051 const Formula & createFormulaFromCube(
const vector<int> & cube,
1052 const vector<BDD> & newVars);
1072 void searchAssignments(
const int * cube,
const Variable & var,
1073 list<CubeNode::Pointer> & leaves)
const;
1124 template <Formula::BinaryOperator OP>
1129 return "Diades::Sdmdl::FormulaBinaryOperator";
1134 return f1.
apply(OP, f2);
1135 }
catch (exception & e) {
1136 throw (
Exception(
Msg(
"Failure to apply a binary operator between '%1%' and '%2%'.")
1145 template <Formula::UnaryOperator OP>
1150 return "Diades::Sdmdl::FormulaUnaryOperator";
1156 }
catch (exception & e) {
1157 throw (
Exception(
Msg(
"Failure to apply a unary operator on '%1%'.")
1166 template<Formula::UnaryOperator UnaryOp>
1169 for (
const Formula & f : formulas) {
1174 for (
const Formula & f : tmp) {
1175 formulas.push_back(unOp(f));
1187 inline FormulaVector &
notF(FormulaVector & formulas) {
1188 return applyUnaryOperator<Formula::UnaryOperator::NotOp>(formulas);
1193 template<Formula::BinaryOperator BinaryOp>
1196 for (
const Formula & f1 : formulas) {
1201 for (
const Formula & f1 : tmp) {
1202 formulas.push_back(binOp(f1, f2));
1216 inline FormulaVector &
andF(FormulaVector & formulas,
const Formula & f) {
1217 return applyBinaryOperator<Formula::BinaryOperator::AndOp>(formulas, f);
1228 inline FormulaVector &
orF(FormulaVector & formulas,
const Formula & f) {
1229 return applyBinaryOperator<Formula::BinaryOperator::OrOp>(formulas, f);
FormulaVector & notF(FormulaVector &formulas)
BddStateMachine & encode(const Diades::Automata::Experimental::StateMachine< StateProperty, FaultProperty > &component, Variable &stateVar, Variable &nextStateVar, Variable &event, BddStateMachine &result)
FormulaVector & orF(FormulaVector &formulas, const Formula &f)
FormulaVector & applyBinaryOperator(FormulaVector &formulas, const Formula &f2)
FormulaVector & andF(FormulaVector &formulas, const Formula &f)
Variable::VariableVector VariableVector
#define require(Exception, expr, message)
Namespace of the Diades project.
FormulaVector & applyUnaryOperator(FormulaVector &formulas)
Value::ValueVector ValueVector
const ValueFactory & owner() const
const Value & nullValue() const
void printFormula(const Formula &formula, ostream &os)