Skip to content

Commit

Permalink
feat: complete parser, add tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@marcofavorito
marcofavorito committed Aug 6, 2021
1 parent b420326 commit 4cf2daf
Show file tree
Hide file tree
Showing 13 changed files with 564 additions and 248 deletions.
9 changes: 9 additions & 0 deletions libs/logic/include/cynthia/logic/base.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,15 +48,24 @@ class Context {

ltlf_ptr tt;
ltlf_ptr ff;
ltlf_ptr true_;
ltlf_ptr false_;
ltlf_ptr end;
ltlf_ptr last;

public:
Context();
symbol_ptr make_symbol(const std::string& name);
ltlf_ptr make_tt();
ltlf_ptr make_ff();
ltlf_ptr make_prop_true();
ltlf_ptr make_prop_false();
ltlf_ptr make_end();
ltlf_ptr make_last();
ltlf_ptr make_bool(bool value);
ltlf_ptr make_atom(const std::string& name);
ltlf_ptr make_not(const ltlf_ptr& arg);
ltlf_ptr make_prop_not(const ltlf_ptr& arg);
ltlf_ptr make_and(const vec_ptr& args);
ltlf_ptr make_or(const vec_ptr& arg);
ltlf_ptr make_implies(const vec_ptr& arg);
Expand Down
3 changes: 3 additions & 0 deletions libs/logic/include/cynthia/logic/comparable.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,10 @@ enum TypeID {
t_Symbol,
t_LTLfTrue,
t_LTLfFalse,
t_LTLfPropTrue,
t_LTLfPropFalse,
t_LTLfAtom,
t_LTLfPropNot,
t_LTLfNot,
t_LTLfAnd,
t_LTLfOr,
Expand Down
115 changes: 113 additions & 2 deletions libs/logic/include/cynthia/logic/ltlf.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@
namespace cynthia {
namespace logic {

inline bool is_propositional(const ltlf_ptr& arg);

class Symbol : public AstNode {
private:
const std::string name_;
Expand Down Expand Up @@ -68,6 +70,30 @@ class LTLfFalse : public LTLfFormula {
int compare_(const Comparable& o) const override;
};

class LTLfPropTrue : public LTLfFormula {
public:
const static TypeID type_code_id = TypeID::t_LTLfPropTrue;
explicit LTLfPropTrue(Context& ctx) : LTLfFormula(ctx) {}

void accept(Visitor* visitor) const override;
inline TypeID get_type_code() const override;
inline hash_t compute_hash_() const override;
bool is_equal(const Comparable& o) const override;
int compare_(const Comparable& o) const override;
};

class LTLfPropFalse : public LTLfFormula {
public:
const static TypeID type_code_id = TypeID::t_LTLfPropFalse;
explicit LTLfPropFalse(Context& ctx) : LTLfFormula(ctx) {}

void accept(Visitor* visitor) const override;
inline TypeID get_type_code() const override;
inline hash_t compute_hash_() const override;
bool is_equal(const Comparable& o) const override;
int compare_(const Comparable& o) const override;
};

class LTLfAtom : public LTLfFormula {
public:
const std::string name;
Expand All @@ -93,6 +119,20 @@ class LTLfUnaryOp : public LTLfFormula {
int compare_(const Comparable& o) const override;
};

class LTLfPropositionalNot : public LTLfUnaryOp {
public:
const static TypeID type_code_id = TypeID::t_LTLfPropNot;
LTLfPropositionalNot(Context& ctx, ltlf_ptr arg)
: LTLfUnaryOp(ctx, std::move(arg)) {
if (!is_propositional(this->arg))
throw std::invalid_argument(
"PropositionalNot only accepts LTLfAtom as arguments.");
}

void accept(Visitor* visitor) const override;
inline TypeID get_type_code() const override;
};

class LTLfNot : public LTLfUnaryOp {
public:
const static TypeID type_code_id = TypeID::t_LTLfNot;
Expand Down Expand Up @@ -174,7 +214,8 @@ class LTLfEquivalent : public LTLfBinaryOp, public BooleanBinaryOp {
public:
const static TypeID type_code_id = TypeID::t_LTLfEquivalent;
LTLfEquivalent(Context& ctx, vec_ptr args)
: LTLfBinaryOp(ctx, std::move(args)), BooleanBinaryOp(equivalent_) {}
: LTLfBinaryOp(ctx, utils::sort(std::move(args))),
BooleanBinaryOp(equivalent_) {}

void accept(Visitor* visitor) const override;
inline TypeID get_type_code() const override;
Expand All @@ -187,7 +228,8 @@ class LTLfXor : public LTLfBinaryOp, public BooleanBinaryOp {
public:
const static TypeID type_code_id = TypeID::t_LTLfXor;
LTLfXor(Context& ctx, vec_ptr args)
: LTLfBinaryOp(ctx, std::move(args)), BooleanBinaryOp(xor_) {}
: LTLfBinaryOp(ctx, utils::sort(std::move(args))), BooleanBinaryOp(xor_) {
}

void accept(Visitor* visitor) const override;
inline TypeID get_type_code() const override;
Expand Down Expand Up @@ -250,5 +292,74 @@ class LTLfAlways : public LTLfUnaryOp {
inline TypeID get_type_code() const override;
};

inline bool is_propositional(const ltlf_ptr& arg) {
return is_a<LTLfAtom>(*arg) || is_a<LTLfPropTrue>(*arg) ||
is_a<LTLfPropFalse>(*arg);
}

inline hash_t Symbol::compute_hash_() const {
hash_t result = get_type_code();
hash_combine(result, name_);
return result;
}
inline hash_t LTLfTrue::compute_hash_() const { return type_code_id; }
inline hash_t LTLfFalse::compute_hash_() const { return type_code_id; }
inline hash_t LTLfPropTrue::compute_hash_() const { return type_code_id; }
inline hash_t LTLfPropFalse::compute_hash_() const { return type_code_id; }
inline hash_t LTLfAtom::compute_hash_() const {
hash_t result = type_code_id;
hash_combine(result, name);
return result;
}
inline hash_t LTLfUnaryOp::compute_hash_() const {
hash_t result = get_type_code();
hash_combine(result, arg->hash());
return result;
}

inline hash_t LTLfBinaryOp::compute_hash_() const {
hash_t result = get_type_code();
auto first = args.begin();
auto last = args.end();
for (; first < last; ++first) {
hash_combine(result, **first);
}
return result;
}

inline TypeID Symbol::get_type_code() const { return TypeID::t_Symbol; }
inline TypeID LTLfTrue::get_type_code() const { return TypeID::t_LTLfTrue; }
inline TypeID LTLfFalse::get_type_code() const { return TypeID::t_LTLfFalse; }
inline TypeID LTLfPropTrue::get_type_code() const {
return TypeID::t_LTLfPropTrue;
}
inline TypeID LTLfPropFalse::get_type_code() const {
return TypeID::t_LTLfPropFalse;
}
inline TypeID LTLfAtom::get_type_code() const { return TypeID::t_LTLfAtom; }
inline TypeID LTLfNot::get_type_code() const { return TypeID::t_LTLfNot; }
inline TypeID LTLfPropositionalNot::get_type_code() const {
return TypeID::t_LTLfPropNot;
}
inline TypeID LTLfAnd::get_type_code() const { return TypeID::t_LTLfAnd; }
inline TypeID LTLfOr::get_type_code() const { return TypeID::t_LTLfOr; }
inline TypeID LTLfImplies::get_type_code() const {
return TypeID::t_LTLfImplies;
}
inline TypeID LTLfEquivalent::get_type_code() const {
return TypeID::t_LTLfEquivalent;
}
inline TypeID LTLfXor::get_type_code() const { return TypeID::t_LTLfXor; }
inline TypeID LTLfNext::get_type_code() const { return TypeID::t_LTLfNext; }
inline TypeID LTLfWeakNext::get_type_code() const { return TypeID::t_LTLfNext; }
inline TypeID LTLfUntil::get_type_code() const { return TypeID::t_LTLfUntil; }
inline TypeID LTLfRelease::get_type_code() const {
return TypeID::t_LTLfRelease;
}
inline TypeID LTLfEventually::get_type_code() const {
return TypeID::t_LTLfEventually;
}
inline TypeID LTLfAlways::get_type_code() const { return TypeID::t_LTLfAlways; }

} // namespace logic
} // namespace cynthia
3 changes: 3 additions & 0 deletions libs/logic/include/cynthia/logic/visitor.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,11 @@ class Visitor {
virtual void visit(const Symbol&) = 0;
virtual void visit(const LTLfTrue&) = 0;
virtual void visit(const LTLfFalse&) = 0;
virtual void visit(const LTLfPropTrue&) = 0;
virtual void visit(const LTLfPropFalse&) = 0;
virtual void visit(const LTLfAtom&) = 0;
virtual void visit(const LTLfNot&) = 0;
virtual void visit(const LTLfPropositionalNot&) = 0;
virtual void visit(const LTLfAnd&) = 0;
virtual void visit(const LTLfOr&) = 0;
virtual void visit(const LTLfImplies&) = 0;
Expand Down
46 changes: 37 additions & 9 deletions libs/logic/src/base.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,18 @@ Context::Context() {

ff = std::make_shared<const LTLfFalse>(*this);
table_->insert_if_not_available(ff);

true_ = std::make_shared<const LTLfPropTrue>(*this);
table_->insert_if_not_available(true_);

false_ = std::make_shared<const LTLfPropFalse>(*this);
table_->insert_if_not_available(false_);

end = std::make_shared<const LTLfAlways>(*this, ff);
table_->insert_if_not_available(end);

last = std::make_shared<const LTLfWeakNext>(*this, ff);
table_->insert_if_not_available(last);
}

symbol_ptr Context::make_symbol(const std::string& name) {
Expand All @@ -41,6 +53,10 @@ symbol_ptr Context::make_symbol(const std::string& name) {
}
ltlf_ptr Context::make_tt() { return tt; }
ltlf_ptr Context::make_ff() { return ff; }
ltlf_ptr Context::make_prop_true() { return true_; }
ltlf_ptr Context::make_prop_false() { return false_; }
ltlf_ptr Context::make_end() { return end; }
ltlf_ptr Context::make_last() { return last; }
ltlf_ptr Context::make_bool(bool value) {
return value ? make_tt() : make_ff();
}
Expand All @@ -57,6 +73,18 @@ ltlf_ptr Context::make_not(const ltlf_ptr& arg) {
return actual;
}

ltlf_ptr Context::make_prop_not(const ltlf_ptr& arg) {
// !(!a) = a
if (is_a<LTLfPropositionalNot>(*arg)) {
return table_->insert_if_not_available(
std::static_pointer_cast<const LTLfPropositionalNot>(arg)->arg);
}
// argument must be an atom
auto negation = std::make_shared<const LTLfPropositionalNot>(*this, arg);
auto actual = table_->insert_if_not_available(negation);
return actual;
}

ltlf_ptr Context::make_and(const vec_ptr& args) {
auto and_ = std::make_shared<const LTLfAnd>(*this, args);
auto actual = table_->insert_if_not_available(and_);
Expand All @@ -82,7 +110,7 @@ ltlf_ptr Context::make_equivalent(const vec_ptr& args) {
}

ltlf_ptr Context::make_xor(const vec_ptr& args) {
auto equivalent = std::make_shared<const LTLfEquivalent>(*this, args);
auto equivalent = std::make_shared<const LTLfXor>(*this, args);
auto actual = table_->insert_if_not_available(equivalent);
return actual;
}
Expand All @@ -100,26 +128,26 @@ ltlf_ptr Context::make_weak_next(const ltlf_ptr& arg) {
}

ltlf_ptr Context::make_until(const vec_ptr& args) {
auto and_ = std::make_shared<const LTLfUntil>(*this, args);
auto actual = table_->insert_if_not_available(and_);
auto until = std::make_shared<const LTLfUntil>(*this, args);
auto actual = table_->insert_if_not_available(until);
return actual;
}

ltlf_ptr Context::make_release(const vec_ptr& args) {
auto and_ = std::make_shared<const LTLfRelease>(*this, args);
auto actual = table_->insert_if_not_available(and_);
auto release = std::make_shared<const LTLfRelease>(*this, args);
auto actual = table_->insert_if_not_available(release);
return actual;
}

ltlf_ptr Context::make_eventually(const ltlf_ptr& arg) {
auto next = std::make_shared<const LTLfEventually>(*this, arg);
auto actual = table_->insert_if_not_available(next);
auto eventually = std::make_shared<const LTLfEventually>(*this, arg);
auto actual = table_->insert_if_not_available(eventually);
return actual;
}

ltlf_ptr Context::make_always(const ltlf_ptr& arg) {
auto next = std::make_shared<const LTLfAlways>(*this, arg);
auto actual = table_->insert_if_not_available(next);
auto always = std::make_shared<const LTLfAlways>(*this, arg);
auto actual = table_->insert_if_not_available(always);
return actual;
}

Expand Down
Loading

0 comments on commit 4cf2daf

Please sign in to comment.