Skip to content

Commit

Permalink
Merge pull request #42 from whitemech/feature/ldlf
Browse files Browse the repository at this point in the history 
Add test regular expression.
  • Loading branch information
@marcofavorito
marcofavorito committed Apr 26, 2020
2 parents 3d3562a + a0e5f1f commit 390d891
Show file tree
Hide file tree
Showing 15 changed files with 333 additions and 58 deletions.
34 changes: 31 additions & 3 deletions lib/include/atom_visitor.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,30 @@ class AtomsVisitor : public Visitor {
public:
static Logger logger;

// callbacks for LDLf
void visit(const Symbol &) override{};
void visit(const LDLfBooleanAtom &) override{};
void visit(const LDLfAnd &) override{};
void visit(const LDLfOr &) override{};
void visit(const LDLfNot &) override{};
void visit(const LDLfDiamond<PropositionalRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfDiamond<TestRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfBox<PropositionalRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfBox<TestRegExp> &x) override {
this->visit_temporal(x);
};

// callbacks for regular expressions
void visit(const PropositionalRegExp &) override;
void visit(const TestRegExp &) override;

// callbacks for propositional logic
void visit(const PropositionalTrue &) override;
void visit(const PropositionalFalse &) override;
void visit(const PropositionalAtom &) override;
Expand All @@ -39,12 +63,16 @@ class AtomsVisitor : public Visitor {
void visit(const PropositionalNot &) override;

void visit(const QuotedFormula &) override{};
void visit(const Symbol &) override{};
void visit(const LDLfDiamond<PropositionalRegExp> &) override;
void visit(const LDLfBox<PropositionalRegExp> &) override;

template <class R> void inline visit_temporal(const LDLfTemporal<R> &x) {
result = apply(*x.get_regex());
auto y = apply(*x.get_formula());
result.insert(y.begin(), y.end());
}

set_atoms_ptr apply(const PropositionalFormula &b);
set_atoms_ptr apply(const LDLfFormula &b);
set_atoms_ptr apply(const RegExp &b);
};

set_atoms_ptr find_atoms(const LDLfFormula &);
Expand Down
1 change: 1 addition & 0 deletions lib/include/basic.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ enum TypeID {
t_LDLfDiamond,
t_LDLfBox,
t_PropositionalRegExp,
t_TestRegExp,
t_NFAState,
t_DFAState,
t_PropositionalTrue,
Expand Down
18 changes: 18 additions & 0 deletions lib/include/delta.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,13 +46,31 @@ class DeltaVisitor : public Visitor {
explicit DeltaVisitor(const set_atoms_ptr &prop_interpretation)
: prop_interpretation{prop_interpretation}, epsilon{false} {}

// callbacks for LDLf
void visit(const Symbol &) override{};
void visit(const LDLfBooleanAtom &) override;
void visit(const LDLfAnd &) override;
void visit(const LDLfOr &) override;
void visit(const LDLfNot &) override;
void visit(const LDLfDiamond<PropositionalRegExp> &x) override;
void visit(const LDLfDiamond<TestRegExp> &) override;
void visit(const LDLfBox<PropositionalRegExp> &x) override;
void visit(const LDLfBox<TestRegExp> &) override;
// TODO add all the combinations of temporal formulas + regular expression

// callbacks for regular expressions
void visit(const PropositionalRegExp &) override{};
void visit(const TestRegExp &) override{};

// callbacks for propositional logic
void visit(const PropositionalTrue &) override{};
void visit(const PropositionalFalse &) override{};
void visit(const PropositionalAtom &) override{};
void visit(const PropositionalAnd &) override{};
void visit(const PropositionalOr &) override{};
void visit(const PropositionalNot &) override{};

void visit(const QuotedFormula &) override{};

std::shared_ptr<const PropositionalFormula> apply(const LDLfFormula &b);
};
Expand Down
55 changes: 48 additions & 7 deletions lib/include/logic.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,11 @@ class LDLfNot : public LDLfFormula {

// TODO consider template check "enable_if_t" vs static_assert in constructor
// template <class T, class=std::enable_if_t<std::is_base_of_v<RegExp, T>>>
template <class T> class LDLfTemporal : public LDLfFormula {
// template <class T>
// template <typename T, typename = typename
// std::enable_if<std::is_base_of<RegExp, T>::value, T>::type>
// template <typename T, typename>
template <typename T> class LDLfTemporal : public LDLfFormula {
private:
const ldlf_ptr arg_;
const std::shared_ptr<const T> regex_;
Expand All @@ -123,6 +127,9 @@ template <class T> class LDLfTemporal : public LDLfFormula {
static_assert(std::is_base_of<RegExp, T>::value,
"concrete RegExp class not derived from RegExp");
}
explicit LDLfTemporal<T>(const std::shared_ptr<const RegExp> &regex,
const ldlf_ptr &formula)
: regex_{std::dynamic_pointer_cast<const T>(regex)}, arg_{formula} {}
ldlf_ptr get_formula() const { return arg_; };
std::shared_ptr<const T> get_regex() const { return regex_; };
hash_t compute_hash_() const override {
Expand All @@ -133,7 +140,11 @@ template <class T> class LDLfTemporal : public LDLfFormula {
};
};

template <class T> class LDLfDiamond : public LDLfTemporal<T> {
// template <class T>
// template <typename T, typename = typename
// std::enable_if<std::is_base_of<RegExp, T>::value, T>::type>
// template <typename T, typename>
template <typename T> class LDLfDiamond : public LDLfTemporal<T> {
public:
const static TypeID type_code_id = TypeID::t_LDLfDiamond;
bool is_canonical(const set_formulas &container_) const;
Expand All @@ -143,6 +154,11 @@ template <class T> class LDLfDiamond : public LDLfTemporal<T> {
: LDLfTemporal<T>(regex, formula) {
this->type_code_ = type_code_id;
}
explicit LDLfDiamond<T>(const std::shared_ptr<const RegExp> &regex,
const ldlf_ptr &formula)
: LDLfTemporal<T>(regex, formula) {
this->type_code_ = type_code_id;
}

bool is_equal(const Basic &o) const override {
return is_a<LDLfDiamond<T>>(o) and
Expand All @@ -160,12 +176,17 @@ template <class T> class LDLfDiamond : public LDLfTemporal<T> {
dynamic_cast<const LDLfDiamond &>(o).get_formula());
};
std::shared_ptr<const LDLfFormula> logical_not() const override {
return std::make_shared<LDLfBox<T>>(this->get_regex(),
this->get_formula()->logical_not());
// return std::make_shared<LDLfBox<T>>(this->get_regex(),
// this->get_formula()->logical_not());
return std::make_shared<LDLfDiamond<T>>(this->get_regex(),
this->get_formula()->logical_not());
};
};

template <class T> class LDLfBox : public LDLfTemporal<T> {
// template <typename T, typename = typename
// std::enable_if<std::is_base_of<RegExp, T>::value, T>::type>
// template <typename T, typename>
template <typename T> class LDLfBox : public LDLfTemporal<T> {
public:
const static TypeID type_code_id = TypeID::t_LDLfBox;
bool is_canonical(const set_formulas &container_) const;
Expand All @@ -175,6 +196,11 @@ template <class T> class LDLfBox : public LDLfTemporal<T> {
: LDLfTemporal<T>(regex, formula) {
this->type_code_ = type_code_id;
}
explicit LDLfBox<T>(const std::shared_ptr<const RegExp> &regex,
const ldlf_ptr &formula)
: LDLfTemporal<T>(regex, formula) {
this->type_code_ = type_code_id;
}

bool is_equal(const Basic &o) const override {
return is_a<LDLfBox<T>>(o) and
Expand Down Expand Up @@ -205,15 +231,30 @@ class PropositionalRegExp : public RegExp {

public:
const static TypeID type_code_id = TypeID::t_PropositionalRegExp;
void accept(Visitor &v) const override{};
void accept(Visitor &v) const override;
explicit PropositionalRegExp(std::shared_ptr<const PropositionalFormula> f);
bool is_canonical(const set_formulas &container_) const;
bool is_canonical(const PropositionalFormula &f) const;
hash_t compute_hash_() const override;
std::shared_ptr<const PropositionalFormula> get_arg() const;
bool is_equal(const Basic &o) const override;
int compare(const Basic &o) const override;
};

class TestRegExp : public RegExp {
private:
const std::shared_ptr<const LDLfFormula> arg_;

public:
const static TypeID type_code_id = TypeID::t_TestRegExp;
void accept(Visitor &v) const override;
explicit TestRegExp(std::shared_ptr<const LDLfFormula> f);
bool is_canonical(const LDLfFormula &f) const;
hash_t compute_hash_() const override;
std::shared_ptr<const LDLfFormula> get_arg() const;
bool is_equal(const Basic &o) const override;
int compare(const Basic &o) const override;
};

class QuotedFormula : public Basic {
private:
protected:
Expand Down
51 changes: 46 additions & 5 deletions lib/include/nnf.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,20 +26,61 @@ namespace lydia {
class NNFTransformer : public Visitor {
private:
protected:
std::shared_ptr<LDLfFormula> result;
// TODO split into several transformers?
std::shared_ptr<const LDLfFormula> result;
std::shared_ptr<const RegExp> regex_result;

public:
// callbacks for LDLf
void visit(const Symbol &) override{};
void visit(const LDLfBooleanAtom &) override;
void visit(const LDLfAnd &) override;
void visit(const LDLfOr &) override;
void visit(const LDLfNot &) override;
void visit(const LDLfDiamond<PropositionalRegExp> &x) override;
void visit(const LDLfBox<PropositionalRegExp> &x) override;
std::shared_ptr<LDLfFormula> apply(const LDLfFormula &b);
void visit(const LDLfDiamond<PropositionalRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfDiamond<TestRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfBox<PropositionalRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfBox<TestRegExp> &x) override {
this->visit_temporal(x);
};

// callbacks for regular expressions
void visit(const PropositionalRegExp &) override;
void visit(const TestRegExp &) override;

// callbacks for propositional logic
void visit(const PropositionalTrue &) override{};
void visit(const PropositionalFalse &) override{};
void visit(const PropositionalAtom &) override{};
void visit(const PropositionalAnd &) override{};
void visit(const PropositionalOr &) override{};
void visit(const PropositionalNot &) override{};

void visit(const QuotedFormula &) override{};

std::shared_ptr<const LDLfFormula> apply(const LDLfFormula &b);
std::shared_ptr<const RegExp> apply(const RegExp &b);

template <typename T, typename = typename std::enable_if<
std::is_base_of<RegExp, T>::value, T>::type>
void inline visit_temporal(const LDLfTemporal<T> &x) {
if (x.type_code_ == TypeID::t_LDLfDiamond) {
result = std::make_shared<LDLfDiamond<T>>(apply(*x.get_regex()),
apply(*x.get_formula()));
} else if (x.type_code_ == TypeID::t_LDLfBox) {
result = std::make_shared<LDLfBox<T>>(apply(*x.get_regex()),
apply(*x.get_formula()));
}
}
};

std::shared_ptr<LDLfFormula> to_nnf(const LDLfFormula &);
std::shared_ptr<const LDLfFormula> to_nnf(const LDLfFormula &);

} // namespace lydia
} // namespace whitemech
21 changes: 21 additions & 0 deletions lib/include/propositional_logic.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,12 +128,33 @@ class EvalVisitor : public Visitor {
public:
explicit EvalVisitor(const set_atoms_ptr &interpretation)
: interpretation{interpretation} {};

// callbacks for LDLf
void visit(const Symbol &) override{};
void visit(const LDLfBooleanAtom &) override{};
void visit(const LDLfAnd &) override{};
void visit(const LDLfOr &) override{};
void visit(const LDLfNot &) override{};
void visit(const LDLfDiamond<PropositionalRegExp> &) override{};
void visit(const LDLfDiamond<TestRegExp> &) override{};
void visit(const LDLfBox<PropositionalRegExp> &) override{};
void visit(const LDLfBox<TestRegExp> &) override{};
// TODO add all the combinations of temporal formulas + regular expression

// callbacks for regular expressions
void visit(const PropositionalRegExp &) override{};
void visit(const TestRegExp &) override{};

// callbacks for propositional logic
void visit(const PropositionalTrue &) override;
void visit(const PropositionalFalse &) override;
void visit(const PropositionalAtom &) override;
void visit(const PropositionalAnd &) override;
void visit(const PropositionalOr &) override;
void visit(const PropositionalNot &) override;

void visit(const QuotedFormula &) override{};

bool apply(const PropositionalFormula &b);
};

Expand Down
8 changes: 5 additions & 3 deletions lib/include/types.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,15 +29,17 @@ namespace lydia {

class Basic;
class Symbol;
class RegExp;
class LDLfFormula;
class LDLfBooleanAtom;
class LDLfAnd;
class LDLfOr;
class LDLfNot;
template <class T> class LDLfDiamond;
template <class T> class LDLfBox;
class RegExp;
class PropositionalRegExp;
class TestRegExp;
template <typename T> class LDLfTemporal;
template <typename T> class LDLfDiamond;
template <typename T> class LDLfBox;
class PropositionalFormula;
class PropositionalAtom;
class PropositionalTrue;
Expand Down
22 changes: 22 additions & 0 deletions lib/include/utils/print.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,12 +32,34 @@ class StrPrinter : public Visitor {
std::string result;

public:
// callbacks for LDLf
void visit(const Symbol &) override;
void visit(const LDLfBooleanAtom &) override;
void visit(const LDLfAnd &) override;
void visit(const LDLfOr &) override;
void visit(const LDLfNot &) override;
void visit(const LDLfDiamond<PropositionalRegExp> &) override{};
void visit(const LDLfDiamond<TestRegExp> &) override{};
void visit(const LDLfBox<PropositionalRegExp> &) override{};
void visit(const LDLfBox<TestRegExp> &) override{};
// TODO add all the combinations of temporal formulas + regular expression

// callbacks for regular expressions
void visit(const PropositionalRegExp &) override{};
void visit(const TestRegExp &) override{};

// callbacks for propositional logic
void visit(const PropositionalTrue &) override{};
void visit(const PropositionalFalse &) override{};
void visit(const PropositionalAtom &) override{};
void visit(const PropositionalAnd &) override{};
void visit(const PropositionalOr &) override{};
void visit(const PropositionalNot &) override{};

void visit(const QuotedFormula &) override{};

template <class T> void visit(const LDLfDiamond<T> &);

std::string apply(const vec_basic &v);
std::string apply(const set_formulas &v);
std::string apply(const Basic &b);
Expand Down
Loading

0 comments on commit 390d891

Please sign in to comment.