diff --git a/.gitignore b/.gitignore index 8e488f4..4648327 100644 --- a/.gitignore +++ b/.gitignore @@ -238,8 +238,7 @@ $RECYCLE.BIN/ build/ coverage.* -libs/logic/include/cynthia/logic/parser/*.yy.cc -libs/logic/include/cynthia/logic/parser/*.hh -libs/logic/include/cynthia/logic/parser/*.tab.cc -libs/logic/include/cynthia/logic/parser/*.tab.hh -libs/logic/include/cynthia/logic/parser/*.hh +libs/parser/include/cynthia/parser/*.yy.cc +libs/parser/include/cynthia/parser/*.hh +libs/parser/include/cynthia/parser/*.tab.cc +libs/parser/include/cynthia/parser/*.tab.hh diff --git a/libs/logic/include/cynthia/logic/base.hpp b/libs/logic/include/cynthia/logic/base.hpp index 45c1b36..e182c58 100644 --- a/libs/logic/include/cynthia/logic/base.hpp +++ b/libs/logic/include/cynthia/logic/base.hpp @@ -29,29 +29,54 @@ namespace cynthia { namespace logic { class Context; -typedef std::shared_ptr context_ptr; class AstNode : public Visitable, public Hashable, public Comparable { private: Context* m_ctx_; public: - explicit AstNode(Context* ctx) : m_ctx_{ctx} {} + explicit AstNode(Context& ctx) : m_ctx_{&ctx} {} Context& ctx() const { return *m_ctx_; } friend void check_context(AstNode const& a, AstNode const& b) { assert(a.m_ctx_ == b.m_ctx_); }; }; -typedef std::shared_ptr ast_ptr; - class Context { private: std::unique_ptr table_; + 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); + ltlf_ptr make_equivalent(const vec_ptr& arg); + ltlf_ptr make_xor(const vec_ptr& arg); + ltlf_ptr make_next(const ltlf_ptr& arg); + ltlf_ptr make_weak_next(const ltlf_ptr& arg); + ltlf_ptr make_until(const vec_ptr& args); + ltlf_ptr make_release(const vec_ptr& args); + ltlf_ptr make_eventually(const ltlf_ptr& args); + ltlf_ptr make_always(const ltlf_ptr& args); }; } // namespace logic diff --git a/libs/logic/include/cynthia/logic/comparable.hpp b/libs/logic/include/cynthia/logic/comparable.hpp index 15d3a26..b4c5237 100644 --- a/libs/logic/include/cynthia/logic/comparable.hpp +++ b/libs/logic/include/cynthia/logic/comparable.hpp @@ -30,10 +30,16 @@ enum TypeID { t_Symbol, t_LTLfTrue, t_LTLfFalse, + t_LTLfPropTrue, + t_LTLfPropFalse, t_LTLfAtom, + t_LTLfPropNot, + t_LTLfNot, t_LTLfAnd, t_LTLfOr, - t_LTLfNot, + t_LTLfImplies, + t_LTLfEquivalent, + t_LTLfXor, t_LTLfNext, t_LTLfWeakNext, t_LTLfUntil, diff --git a/libs/logic/include/cynthia/logic/hashable.hpp b/libs/logic/include/cynthia/logic/hashable.hpp index d6c49b0..50e6302 100644 --- a/libs/logic/include/cynthia/logic/hashable.hpp +++ b/libs/logic/include/cynthia/logic/hashable.hpp @@ -84,7 +84,7 @@ inline void hash_combine_impl( } inline void hash_combine_impl(hash_t& seed, const std::string& s) { - for (const char& c : s) { + for (const auto& c : s) { hash_combine(seed, static_cast(c)); } } diff --git a/libs/logic/include/cynthia/logic/hashtable.hpp b/libs/logic/include/cynthia/logic/hashtable.hpp index cecc879..4d59696 100644 --- a/libs/logic/include/cynthia/logic/hashtable.hpp +++ b/libs/logic/include/cynthia/logic/hashtable.hpp @@ -17,38 +17,25 @@ */ #include +#include #include #include namespace cynthia { namespace logic { -struct Deref { - struct Hash { - template - std::size_t operator()(std::shared_ptr const& p) const { - return std::hash()(*p); - } - }; - - struct Compare { - template - size_t operator()(std::shared_ptr const& a, - std::shared_ptr const& b) const { - return *a == *b; - } - }; -}; /* * A hash table for AST nodes based on STL unordered_set. */ class HashTable { private: - std::unordered_set m_table_; + std::unordered_set + m_table_; public: explicit HashTable() { - m_table_ = std::unordered_set{}; + m_table_ = std::unordered_set{}; } template diff --git a/libs/logic/include/cynthia/logic/ltlf.hpp b/libs/logic/include/cynthia/logic/ltlf.hpp index dc0b1af..178506d 100644 --- a/libs/logic/include/cynthia/logic/ltlf.hpp +++ b/libs/logic/include/cynthia/logic/ltlf.hpp @@ -16,6 +16,7 @@ * along with Cynthia. If not, see . */ +#include #include #include #include @@ -23,21 +24,342 @@ namespace cynthia { namespace logic { +inline bool is_propositional(const ltlf_ptr& arg); + class Symbol : public AstNode { private: const std::string name_; public: const static TypeID type_code_id = TypeID::t_Symbol; - explicit Symbol(Context& ctx, const std::string& name) - : AstNode(&ctx), name_{name} {} + Symbol(Context& ctx, const std::string& name) : AstNode(ctx), name_{name} {} + + 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 LTLfFormula : public AstNode { +public: + explicit LTLfFormula(Context& c) : AstNode(c) {} +}; + +class LTLfTrue : public LTLfFormula { +public: + const static TypeID type_code_id = TypeID::t_LTLfTrue; + explicit LTLfTrue(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 LTLfFalse : public LTLfFormula { +public: + const static TypeID type_code_id = TypeID::t_LTLfFalse; + explicit LTLfFalse(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 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; + const static TypeID type_code_id = TypeID::t_LTLfAtom; + LTLfAtom(Context& ctx, const std::string& name) + : LTLfFormula(ctx), name{name} {} 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 LTLfUnaryOp : public LTLfFormula { +public: + const ltlf_ptr arg; + LTLfUnaryOp(Context& ctx, ltlf_ptr arg) + : LTLfFormula(ctx), arg{std::move(arg)} {} + + inline hash_t compute_hash_() const override; + bool is_equal(const Comparable& o) const override; + 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; + LTLfNot(Context& ctx, ltlf_ptr arg) : LTLfUnaryOp(ctx, std::move(arg)) {} + + void accept(Visitor* visitor) const override; inline TypeID get_type_code() const override; +}; + +class BooleanBinaryOp { +public: + bool const (&fun)(bool, bool); + + BooleanBinaryOp(bool const (&fun)(bool, bool)) : fun{fun} {} +}; + +class LTLfBinaryOp : public LTLfFormula { +public: + const vec_ptr args; + + LTLfBinaryOp(Context& ctx, vec_ptr args) : LTLfFormula(ctx), args{args} {} + + inline hash_t compute_hash_() const override; bool is_equal(const Comparable& o) const override; int compare_(const Comparable& o) const override; }; +class LTLfCommutativeBinaryOp : public LTLfBinaryOp { +public: + LTLfCommutativeBinaryOp(Context& ctx, vec_ptr args) + : LTLfBinaryOp(ctx, utils::setify(args)) {} +}; + +class LTLfAnd : public LTLfCommutativeBinaryOp, public BooleanBinaryOp { +private: + static inline bool const and_(bool b1, bool b2) { return b1 and b2; } + +public: + const static TypeID type_code_id = TypeID::t_LTLfAnd; + LTLfAnd(Context& ctx, vec_ptr args) + : LTLfCommutativeBinaryOp(ctx, std::move(args)), BooleanBinaryOp(and_) {} + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +class LTLfOr : public LTLfCommutativeBinaryOp, public BooleanBinaryOp { +private: + static inline bool const or_(bool b1, bool b2) { return b1 or b2; } + +public: + const static TypeID type_code_id = TypeID::t_LTLfOr; + LTLfOr(Context& ctx, vec_ptr args) + : LTLfCommutativeBinaryOp(ctx, std::move(args)), BooleanBinaryOp(or_) {} + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +class LTLfImplies : public LTLfBinaryOp, public BooleanBinaryOp { +private: + static inline bool const implies_(bool b1, bool b2) { return not b1 or b2; } + +public: + const static TypeID type_code_id = TypeID::t_LTLfImplies; + LTLfImplies(Context& ctx, vec_ptr args) + : LTLfBinaryOp(ctx, std::move(args)), BooleanBinaryOp(implies_) {} + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +class LTLfEquivalent : public LTLfBinaryOp, public BooleanBinaryOp { +private: + static inline bool const equivalent_(bool b1, bool b2) { + return (b1 and b2) or (not b1 and not b2); + } + +public: + const static TypeID type_code_id = TypeID::t_LTLfEquivalent; + LTLfEquivalent(Context& ctx, vec_ptr args) + : LTLfBinaryOp(ctx, utils::sort(std::move(args))), + BooleanBinaryOp(equivalent_) {} + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +class LTLfXor : public LTLfBinaryOp, public BooleanBinaryOp { +private: + static inline bool const xor_(bool b1, bool b2) { return b1 xor b2; } + +public: + const static TypeID type_code_id = TypeID::t_LTLfXor; + LTLfXor(Context& ctx, vec_ptr args) + : LTLfBinaryOp(ctx, utils::sort(std::move(args))), BooleanBinaryOp(xor_) { + } + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +class LTLfNext : public LTLfUnaryOp { +public: + const static TypeID type_code_id = TypeID::t_LTLfNext; + LTLfNext(Context& ctx, ltlf_ptr arg) : LTLfUnaryOp(ctx, std::move(arg)) {} + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +class LTLfWeakNext : public LTLfUnaryOp { +public: + const static TypeID type_code_id = TypeID::t_LTLfWeakNext; + LTLfWeakNext(Context& ctx, ltlf_ptr arg) : LTLfUnaryOp(ctx, std::move(arg)) {} + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +class LTLfUntil : public LTLfBinaryOp { + +public: + const static TypeID type_code_id = TypeID::t_LTLfUntil; + LTLfUntil(Context& ctx, vec_ptr args) : LTLfBinaryOp(ctx, std::move(args)) {} + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +class LTLfRelease : public LTLfBinaryOp { +public: + const static TypeID type_code_id = TypeID::t_LTLfRelease; + LTLfRelease(Context& ctx, vec_ptr args) + : LTLfBinaryOp(ctx, std::move(args)) {} + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +class LTLfEventually : public LTLfUnaryOp { +public: + const static TypeID type_code_id = TypeID::t_LTLfEventually; + LTLfEventually(Context& ctx, ltlf_ptr arg) + : LTLfUnaryOp(ctx, std::move(arg)) {} + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +class LTLfAlways : public LTLfUnaryOp { +public: + const static TypeID type_code_id = TypeID::t_LTLfAlways; + LTLfAlways(Context& ctx, ltlf_ptr arg) : LTLfUnaryOp(ctx, std::move(arg)) {} + + void accept(Visitor* visitor) const override; + inline TypeID get_type_code() const override; +}; + +inline bool is_propositional(const ltlf_ptr& arg) { + return is_a(*arg) || is_a(*arg) || + is_a(*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 \ No newline at end of file diff --git a/libs/logic/include/cynthia/logic/types.hpp b/libs/logic/include/cynthia/logic/types.hpp index dc428a7..ed69d1e 100644 --- a/libs/logic/include/cynthia/logic/types.hpp +++ b/libs/logic/include/cynthia/logic/types.hpp @@ -18,6 +18,7 @@ #include #include +#include namespace cynthia { namespace logic { @@ -29,6 +30,7 @@ typedef std::size_t hash_t; typedef std::shared_ptr ast_ptr; typedef std::shared_ptr symbol_ptr; typedef std::shared_ptr ltlf_ptr; +typedef std::vector vec_ptr; } // namespace logic } // namespace cynthia diff --git a/libs/logic/include/cynthia/logic/visitor.hpp b/libs/logic/include/cynthia/logic/visitor.hpp index 43b083a..d89fdf2 100644 --- a/libs/logic/include/cynthia/logic/visitor.hpp +++ b/libs/logic/include/cynthia/logic/visitor.hpp @@ -21,9 +21,30 @@ namespace cynthia { namespace logic { +/* + * Abstract visitor class. + */ class Visitor { public: - virtual void visit(const Symbol& symbol) = 0; + 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; + virtual void visit(const LTLfEquivalent&) = 0; + virtual void visit(const LTLfXor&) = 0; + virtual void visit(const LTLfNext&) = 0; + virtual void visit(const LTLfWeakNext&) = 0; + virtual void visit(const LTLfUntil&) = 0; + virtual void visit(const LTLfRelease&) = 0; + virtual void visit(const LTLfEventually&) = 0; + virtual void visit(const LTLfAlways&) = 0; }; } // namespace logic diff --git a/libs/logic/src/base.cpp b/libs/logic/src/base.cpp index d3d21ca..e3f917f 100644 --- a/libs/logic/src/base.cpp +++ b/libs/logic/src/base.cpp @@ -15,16 +15,141 @@ * along with Cynthia. If not, see . */ +//#include +#include #include +// TODO instead of make_shared, use "signature" of object to instantiate +// so to avoid heap allocation. + namespace cynthia { namespace logic { -Context::Context() { table_ = utils::make_unique(); } +Context::Context() { + table_ = utils::make_unique(); + + tt = std::make_shared(*this); + table_->insert_if_not_available(tt); + + ff = std::make_shared(*this); + table_->insert_if_not_available(ff); + + true_ = std::make_shared(*this); + table_->insert_if_not_available(true_); + + false_ = std::make_shared(*this); + table_->insert_if_not_available(false_); + + end = std::make_shared(*this, ff); + table_->insert_if_not_available(end); + + last = std::make_shared(*this, ff); + table_->insert_if_not_available(last); +} symbol_ptr Context::make_symbol(const std::string& name) { symbol_ptr symbol = std::make_shared(*this, name); symbol_ptr result = table_->insert_if_not_available(symbol); return result; } +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(); +} + +ltlf_ptr Context::make_atom(const std::string& name) { + auto atom = std::make_shared(*this, name); + auto actual_atom = table_->insert_if_not_available(atom); + return actual_atom; +} + +ltlf_ptr Context::make_not(const ltlf_ptr& arg) { + auto negation = std::make_shared(*this, arg); + auto actual = table_->insert_if_not_available(negation); + return actual; +} + +ltlf_ptr Context::make_prop_not(const ltlf_ptr& arg) { + // !(!a) = a + if (is_a(*arg)) { + return table_->insert_if_not_available( + std::static_pointer_cast(arg)->arg); + } + // argument must be an atom + auto negation = std::make_shared(*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(*this, args); + auto actual = table_->insert_if_not_available(and_); + return actual; +} + +ltlf_ptr Context::make_or(const vec_ptr& args) { + auto or_ = std::make_shared(*this, args); + auto actual = table_->insert_if_not_available(or_); + return actual; +} + +ltlf_ptr Context::make_implies(const vec_ptr& args) { + auto implies = std::make_shared(*this, args); + auto actual = table_->insert_if_not_available(implies); + return actual; +} + +ltlf_ptr Context::make_equivalent(const vec_ptr& args) { + auto equivalent = std::make_shared(*this, args); + auto actual = table_->insert_if_not_available(equivalent); + return actual; +} + +ltlf_ptr Context::make_xor(const vec_ptr& args) { + auto equivalent = std::make_shared(*this, args); + auto actual = table_->insert_if_not_available(equivalent); + return actual; +} + +ltlf_ptr Context::make_next(const ltlf_ptr& arg) { + auto next = std::make_shared(*this, arg); + auto actual = table_->insert_if_not_available(next); + return actual; +} + +ltlf_ptr Context::make_weak_next(const ltlf_ptr& arg) { + auto next = std::make_shared(*this, arg); + auto actual = table_->insert_if_not_available(next); + return actual; +} + +ltlf_ptr Context::make_until(const vec_ptr& args) { + auto until = std::make_shared(*this, args); + auto actual = table_->insert_if_not_available(until); + return actual; +} + +ltlf_ptr Context::make_release(const vec_ptr& args) { + auto release = std::make_shared(*this, args); + auto actual = table_->insert_if_not_available(release); + return actual; +} + +ltlf_ptr Context::make_eventually(const ltlf_ptr& arg) { + auto eventually = std::make_shared(*this, arg); + auto actual = table_->insert_if_not_available(eventually); + return actual; +} + +ltlf_ptr Context::make_always(const ltlf_ptr& arg) { + auto always = std::make_shared(*this, arg); + auto actual = table_->insert_if_not_available(always); + return actual; +} + } // namespace logic } // namespace cynthia \ No newline at end of file diff --git a/libs/logic/src/ltlf.cpp b/libs/logic/src/ltlf.cpp index 11209c7..4366af5 100644 --- a/libs/logic/src/ltlf.cpp +++ b/libs/logic/src/ltlf.cpp @@ -17,18 +17,11 @@ #include #include +#include namespace cynthia { namespace logic { -void Symbol::accept(Visitor* visitor) const { visitor->visit(*this); } -inline hash_t Symbol::compute_hash_() const { - hash_t h1 = get_type_code(); - auto h2 = std::hash()(name_); - hash_combine(h1, h2); - return h1; -} -inline TypeID Symbol::get_type_code() const { return TypeID::t_Symbol; } bool Symbol::is_equal(const Comparable& o) const { if (is_a(o)) return name_ == dynamic_cast(o).name_; @@ -42,5 +35,88 @@ int Symbol::compare_(const Comparable& o) const { return name_ < s.name_ ? -1 : 1; } +bool LTLfTrue::is_equal(const Comparable& o) const { return is_a(o); } +int LTLfTrue::compare_(const Comparable& o) const { + assert(is_a(o)); + return 0; +} + +bool LTLfFalse::is_equal(const Comparable& o) const { + return is_a(o); +} +int LTLfFalse::compare_(const Comparable& o) const { + assert(is_a(o)); + return 0; +} + +bool LTLfPropTrue::is_equal(const Comparable& o) const { + return is_a(o); +} +int LTLfPropTrue::compare_(const Comparable& o) const { + assert(is_a(o)); + return 0; +} + +bool LTLfPropFalse::is_equal(const Comparable& o) const { + return is_a(o); +} +int LTLfPropFalse::compare_(const Comparable& o) const { + assert(is_a(o)); + return 0; +} + +bool LTLfAtom::is_equal(const Comparable& o) const { + return is_a(o) and name == dynamic_cast(o).name; +} +int LTLfAtom::compare_(const Comparable& o) const { + assert(is_a(o)); + auto n1 = this->name; + auto n2 = dynamic_cast(o).name; + return n1 == n2 ? 0 : n1 < n2 ? -1 : 1; +} + +bool LTLfUnaryOp::is_equal(const Comparable& o) const { + return get_type_code() == o.get_type_code() and + arg->is_equal(*dynamic_cast(o).arg); +} +int LTLfUnaryOp::compare_(const Comparable& o) const { + assert(get_type_code() == o.get_type_code()); + return this->arg->compare(*dynamic_cast(o).arg); +} + +bool LTLfBinaryOp::is_equal(const Comparable& o) const { + return get_type_code() == o.get_type_code() and + std::equal(args.begin(), args.end(), + dynamic_cast(o).args.begin(), + utils::Deref::Compare()); +} +int LTLfBinaryOp::compare_(const Comparable& o) const { + assert(this->get_type_code() == o.get_type_code()); + return utils::ordered_compare(this->args, + dynamic_cast(o).args); +} + +void Symbol::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfTrue::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfFalse::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfPropTrue::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfPropFalse::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfAtom::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfNot::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfPropositionalNot::accept(Visitor* visitor) const { + visitor->visit(*this); +} +void LTLfAnd::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfOr::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfImplies::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfEquivalent::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfXor::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfNext::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfWeakNext::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfUntil::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfRelease::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfEventually::accept(Visitor* visitor) const { visitor->visit(*this); } +void LTLfAlways::accept(Visitor* visitor) const { visitor->visit(*this); } + } // namespace logic } // namespace cynthia \ No newline at end of file diff --git a/libs/logic/tests/unit/test_ltlf.cpp b/libs/logic/tests/unit/test_ltlf.cpp index 8a8efc1..c7e7714 100644 --- a/libs/logic/tests/unit/test_ltlf.cpp +++ b/libs/logic/tests/unit/test_ltlf.cpp @@ -34,6 +34,287 @@ TEST_CASE("Test Symbol", "[logic][ltlf]") { // different value, different pointer REQUIRE(s1 != s2); } + +TEST_CASE("tt", "[logic][ltlf]") { + auto context = Context(); + + auto tt1 = context.make_tt(); + auto tt2 = context.make_bool(true); + + REQUIRE(tt1 == tt2); + REQUIRE(*tt1 == *tt2); +} + +TEST_CASE("ff", "[logic][ltlf]") { + auto context = Context(); + + auto ff1 = context.make_ff(); + auto ff2 = context.make_bool(false); + + REQUIRE(ff1 == ff2); + REQUIRE(*ff1 == *ff2); +} + +TEST_CASE("true", "[logic][ltlf]") { + auto context = Context(); + + auto prop_true1 = context.make_prop_true(); + auto prop_true2 = context.make_prop_true(); + + REQUIRE(prop_true1 == prop_true2); + REQUIRE(*prop_true1 == *prop_true2); +} + +TEST_CASE("false", "[logic][ltlf]") { + auto context = Context(); + + auto prop_false1 = context.make_prop_false(); + auto prop_false2 = context.make_prop_false(); + + REQUIRE(prop_false1 == prop_false2); + REQUIRE(*prop_false1 == *prop_false2); +} + +TEST_CASE("atom", "[logic][ltlf]") { + auto context = Context(); + + auto expected_atom2 = context.make_atom("a"); + auto expected_atom1 = context.make_atom("a"); + REQUIRE(expected_atom1 == expected_atom2); + REQUIRE(*expected_atom1 == *expected_atom2); +} + +TEST_CASE("logical negation of literals", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto atom2 = context.make_atom("a"); + SECTION("Same pointer") { + auto expected1 = context.make_not(atom1); + auto expected2 = context.make_not(atom2); + REQUIRE(expected1 == expected2); + REQUIRE(*expected1 == *expected2); + } +} + +TEST_CASE("propositional negation of literals", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto atom2 = context.make_atom("a"); + SECTION("Same pointer") { + auto expected1 = context.make_prop_not(atom1); + auto expected2 = context.make_prop_not(atom2); + REQUIRE(expected1 == expected2); + REQUIRE(*expected1 == *expected2); + } + + SECTION("Prop. negation of prop. negation of a is a") { + auto actual = context.make_prop_not(context.make_prop_not(atom1)); + const auto& expected = atom1; + REQUIRE(actual == expected); + REQUIRE(*actual == *expected); + } + + SECTION("Propositional negation of a non-atom raises exception") { + REQUIRE_THROWS_AS(context.make_prop_not(context.make_not(atom1)), + std::invalid_argument); + } +} + +TEST_CASE("conjunction", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto atom2 = context.make_atom("a"); + auto atom3 = context.make_atom("b"); + auto atom4 = context.make_atom("b"); + auto expected1 = context.make_and(vec_ptr{atom1, atom2, atom3}); + auto expected2 = context.make_and(vec_ptr{atom1, atom3, atom4}); + REQUIRE(expected1 == expected2); + REQUIRE(*expected1 == *expected2); +} + +TEST_CASE("disjunction", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto atom2 = context.make_atom("a"); + auto atom3 = context.make_atom("b"); + auto atom4 = context.make_atom("b"); + auto expected1 = context.make_or(vec_ptr{atom1, atom2, atom3}); + auto expected2 = context.make_or(vec_ptr{atom1, atom3, atom4}); + REQUIRE(expected1 == expected2); + REQUIRE(*expected1 == *expected2); +} + +TEST_CASE("implication", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto atom2 = context.make_atom("a"); + auto atom3 = context.make_atom("b"); + auto atom4 = context.make_atom("b"); + auto aab1 = context.make_implies(vec_ptr{atom1, atom2, atom4}); + auto aab2 = context.make_implies(vec_ptr{atom1, atom2, atom3}); + auto abb = context.make_implies(vec_ptr{atom1, atom3, atom4}); + REQUIRE(aab1 == aab2); + REQUIRE(*aab1 == *aab2); + + REQUIRE(aab1 != abb); + REQUIRE(*aab1 != *abb); +} + +TEST_CASE("equivalence", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto atom2 = context.make_atom("a"); + auto atom3 = context.make_atom("b"); + auto atom4 = context.make_atom("b"); + auto aa = context.make_equivalent(vec_ptr{atom1, atom2}); + auto bb = context.make_equivalent(vec_ptr{atom3, atom4}); + SECTION("Test equal") { + REQUIRE(aa != bb); + REQUIRE(*aa != *bb); + + REQUIRE(aa == aa); + REQUIRE(*aa == *aa); + } + + SECTION("Test arguments are sorted") { + auto aa_bb = context.make_equivalent(vec_ptr{aa, bb}); + auto bb_aa = context.make_equivalent(vec_ptr{bb, aa}); + REQUIRE(aa_bb == bb_aa); + REQUIRE(*aa_bb == *bb_aa); + } +} + +TEST_CASE("xor", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto atom2 = context.make_atom("a"); + auto atom3 = context.make_atom("b"); + auto atom4 = context.make_atom("b"); + auto aa = context.make_xor(vec_ptr{atom1, atom2}); + auto bb = context.make_xor(vec_ptr{atom3, atom4}); + + SECTION("Test equal") { + REQUIRE(aa != bb); + REQUIRE(*aa != *bb); + + REQUIRE(aa == aa); + REQUIRE(*aa == *aa); + } + + SECTION("Test arguments are sorted") { + auto aa_bb = context.make_xor(vec_ptr{aa, bb}); + auto bb_aa = context.make_xor(vec_ptr{bb, aa}); + REQUIRE(aa_bb == bb_aa); + REQUIRE(*aa_bb == *bb_aa); + } +} + +TEST_CASE("next", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto expected1 = context.make_next(atom1); + + auto atom2 = context.make_atom("a"); + auto expected2 = context.make_next(atom2); + REQUIRE(expected1 == expected2); + REQUIRE(*expected1 == *expected2); +} +TEST_CASE("weak_next", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto expected1 = context.make_weak_next(atom1); + + auto atom2 = context.make_atom("a"); + auto expected2 = context.make_weak_next(atom2); + REQUIRE(expected1 == expected2); + REQUIRE(*expected1 == *expected2); +} + +TEST_CASE("until", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto atom2 = context.make_atom("a"); + auto atom3 = context.make_atom("b"); + auto atom4 = context.make_atom("b"); + auto aab1 = context.make_until(vec_ptr{atom1, atom2, atom4}); + auto aab2 = context.make_until(vec_ptr{atom1, atom2, atom3}); + auto abb = context.make_until(vec_ptr{atom1, atom3, atom4}); + REQUIRE(aab1 == aab2); + REQUIRE(*aab1 == *aab2); + + REQUIRE(aab1 != abb); + REQUIRE(*aab1 != *abb); +} + +TEST_CASE("release", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto atom2 = context.make_atom("a"); + auto atom3 = context.make_atom("b"); + auto atom4 = context.make_atom("b"); + auto aab1 = context.make_release(vec_ptr{atom1, atom2, atom4}); + auto aab2 = context.make_release(vec_ptr{atom1, atom2, atom3}); + auto abb = context.make_release(vec_ptr{atom1, atom3, atom4}); + REQUIRE(aab1 == aab2); + REQUIRE(*aab1 == *aab2); + + REQUIRE(aab1 != abb); + REQUIRE(*aab1 != *abb); +} + +TEST_CASE("eventually", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto expected1 = context.make_eventually(atom1); + + auto atom2 = context.make_atom("a"); + auto expected2 = context.make_eventually(atom2); + REQUIRE(expected1 == expected2); + REQUIRE(*expected1 == *expected2); +} + +TEST_CASE("always", "[logic][ltlf]") { + auto context = Context(); + + auto atom1 = context.make_atom("a"); + auto expected1 = context.make_always(atom1); + + auto atom2 = context.make_atom("a"); + auto expected2 = context.make_always(atom2); + REQUIRE(expected1 == expected2); + REQUIRE(*expected1 == *expected2); +} + +TEST_CASE("end", "[logic][ltlf]") { + auto context = Context(); + + auto actual_end = context.make_end(); + auto expected_end = context.make_always(context.make_ff()); + REQUIRE(actual_end == expected_end); + REQUIRE(*actual_end == *expected_end); +} + +TEST_CASE("last", "[logic][ltlf]") { + auto context = Context(); + + auto actual_last = context.make_last(); + auto expected_last = context.make_weak_next(context.make_ff()); + REQUIRE(actual_last == expected_last); + REQUIRE(*actual_last == *expected_last); +} + } // namespace Test } // namespace logic } // namespace cynthia \ No newline at end of file diff --git a/libs/parser/CMakeLists.txt b/libs/parser/CMakeLists.txt index a644701..e135b17 100644 --- a/libs/parser/CMakeLists.txt +++ b/libs/parser/CMakeLists.txt @@ -35,6 +35,7 @@ ADD_FLEX_BISON_DEPENDENCY(LTLfLexer LTLfParser) #set includes include_directories (${CYNTHIA_PARSER_INCLUDE_PATH} ${THIRD_PARTY_INCLUDE_PATH}) +include_directories (${CYNTHIA_LOGIC_INCLUDE_PATH} ${CYNTHIA_UTILS_INCLUDE_PATH}) include_directories (${CMAKE_CURRENT_BINARY_DIR} ${CMAKE_CURRENT_SOURCE_DIR}) #set sources diff --git a/libs/parser/include/cynthia/parser/abstract_driver.hpp b/libs/parser/include/cynthia/parser/abstract_driver.hpp index ddd8643..01ee7ef 100644 --- a/libs/parser/include/cynthia/parser/abstract_driver.hpp +++ b/libs/parser/include/cynthia/parser/abstract_driver.hpp @@ -16,16 +16,19 @@ * along with Cynthia. If not, see . */ +#include +#include + namespace cynthia { namespace parser { class AbstractDriver { public: - // std::shared_ptr context = nullptr; - // AbstractDriver() : context{std::make_shared()} {} - // AbstractDriver(std::shared_ptr c) : context{std::move(c)} {} + std::shared_ptr context = nullptr; + AbstractDriver() : context{std::make_shared()} {} + AbstractDriver(std::shared_ptr c) : context{std::move(c)} {} virtual void parse(const char* const filename) = 0; virtual void parse(std::istream& iss) = 0; - // virtual ldlf_ptr get_result() = 0; + virtual logic::ltlf_ptr get_result() = 0; }; } // namespace parser } // namespace cynthia diff --git a/libs/parser/include/cynthia/parser/driver.hpp b/libs/parser/include/cynthia/parser/driver.hpp index 982d628..0ed5347 100644 --- a/libs/parser/include/cynthia/parser/driver.hpp +++ b/libs/parser/include/cynthia/parser/driver.hpp @@ -18,9 +18,11 @@ #include #include +#include #include #include +#include #include #include #include @@ -37,15 +39,15 @@ class LTLfDriver : public AbstractDriver { LTLfScanner* scanner = nullptr; public: - // ldlf_ptr result; + logic::ltlf_ptr result; LTLfDriver() : AbstractDriver() {} - // explicit LTLfDriver(std::shared_ptr c) : AbstractDriver(c) {} + explicit LTLfDriver(std::shared_ptr c) : AbstractDriver(c) {} virtual ~LTLfDriver(); - // ldlf_ptr get_result() override { return result; } + logic::ltlf_ptr get_result() override { return result; } /** * parse - parse from a file @@ -57,9 +59,36 @@ class LTLfDriver : public AbstractDriver { * parse - parse from a c++ input stream * @param is - std::istream&, valid input stream */ - void parse(std::istream& iss); + void parse(std::istream& iss) override; std::ostream& print(std::ostream& stream) const; + + logic::ltlf_ptr add_LTLfTrue() const; + logic::ltlf_ptr add_LTLfFalse() const; + logic::ltlf_ptr add_LTLfPropTrue() const; + logic::ltlf_ptr add_LTLfPropFalse() const; + logic::ltlf_ptr add_LTLfEnd() const; + logic::ltlf_ptr add_LTLfLast() const; + logic::ltlf_ptr add_LTLfAtom(const std::string& name) const; + logic::ltlf_ptr add_LTLfNot(const logic::ltlf_ptr& arg) const; + logic::ltlf_ptr add_LTLfAnd(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const; + logic::ltlf_ptr add_LTLfOr(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const; + logic::ltlf_ptr add_LTLfEquivalent(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const; + logic::ltlf_ptr add_LTLfImplies(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const; + logic::ltlf_ptr add_LTLfXor(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const; + logic::ltlf_ptr add_LTLfNext(const logic::ltlf_ptr& arg) const; + logic::ltlf_ptr add_LTLfWeakNext(const logic::ltlf_ptr& arg) const; + logic::ltlf_ptr add_LTLfUntil(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const; + logic::ltlf_ptr add_LTLfRelease(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const; + logic::ltlf_ptr add_LTLfEventually(const logic::ltlf_ptr& arg) const; + logic::ltlf_ptr add_LTLfAlways(const logic::ltlf_ptr& arg) const; }; } // namespace ltlf diff --git a/libs/parser/include/cynthia/parser/lexer.l b/libs/parser/include/cynthia/parser/lexer.l index 6789d73..0301bb5 100644 --- a/libs/parser/include/cynthia/parser/lexer.l +++ b/libs/parser/include/cynthia/parser/lexer.l @@ -44,6 +44,7 @@ using token = cynthia::parser::ltlf::LTLfParser::token; "F" { return token::EVENTUALLY; } "G" { return token::ALWAYS; } +"^" { return token::XOR; } "<=>"|"<->" { return token::EQUIVALENCE; } "=>"|"->" { return token::IMPLICATION; } diff --git a/libs/parser/include/cynthia/parser/lexer.yy.cc b/libs/parser/include/cynthia/parser/lexer.yy.cc deleted file mode 100644 index 27ba688..0000000 --- a/libs/parser/include/cynthia/parser/lexer.yy.cc +++ /dev/null @@ -1,2007 +0,0 @@ -#line 2 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.yy.cc" - -#line 4 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.yy.cc" - -#define YY_INT_ALIGNED short int - -/* A lexical scanner generated by flex */ - -/* %not-for-header */ -/* %if-c-only */ -/* %if-not-reentrant */ -/* %endif */ -/* %endif */ -/* %ok-for-header */ - -#define FLEX_SCANNER -#define YY_FLEX_MAJOR_VERSION 2 -#define YY_FLEX_MINOR_VERSION 6 -#define YY_FLEX_SUBMINOR_VERSION 4 -#if YY_FLEX_SUBMINOR_VERSION > 0 -#define FLEX_BETA -#endif - -/* %if-c++-only */ -/* The c++ scanner is a mess. The FlexLexer.h header file relies on the - * following macro. This is required in order to pass the c++-multiple-scanners - * test in the regression suite. We get reports that it breaks inheritance. - * We will address this in a future release of flex, or omit the C++ scanner - * altogether. - */ -#define yyFlexLexer ltlfFlexLexer -/* %endif */ - -/* %if-c-only */ -/* %endif */ - -#ifdef yyalloc -#define ltlfalloc_ALREADY_DEFINED -#else -#define yyalloc ltlfalloc -#endif - -#ifdef yyrealloc -#define ltlfrealloc_ALREADY_DEFINED -#else -#define yyrealloc ltlfrealloc -#endif - -#ifdef yyfree -#define ltlffree_ALREADY_DEFINED -#else -#define yyfree ltlffree -#endif - -/* %if-c-only */ -/* %endif */ - -/* First, we deal with platform-specific or compiler-specific issues. */ - -/* begin standard C headers. */ -/* %if-c-only */ -/* %endif */ - -/* %if-tables-serialization */ -/* %endif */ -/* end standard C headers. */ - -/* %if-c-or-c++ */ -/* flex integer type definitions */ - -#ifndef FLEXINT_H -#define FLEXINT_H - -/* C99 systems have . Non-C99 systems may or may not. */ - -#if defined(__STDC_VERSION__) && __STDC_VERSION__ >= 199901L - -/* C99 says to define __STDC_LIMIT_MACROS before including stdint.h, - * if you want the limit (max/min) macros for int types. - */ -#ifndef __STDC_LIMIT_MACROS -#define __STDC_LIMIT_MACROS 1 -#endif - -#include -typedef int8_t flex_int8_t; -typedef uint8_t flex_uint8_t; -typedef int16_t flex_int16_t; -typedef uint16_t flex_uint16_t; -typedef int32_t flex_int32_t; -typedef uint32_t flex_uint32_t; -#else -typedef signed char flex_int8_t; -typedef short int flex_int16_t; -typedef int flex_int32_t; -typedef unsigned char flex_uint8_t; -typedef unsigned short int flex_uint16_t; -typedef unsigned int flex_uint32_t; - -/* Limits of integral types. */ -#ifndef INT8_MIN -#define INT8_MIN (-128) -#endif -#ifndef INT16_MIN -#define INT16_MIN (-32767 - 1) -#endif -#ifndef INT32_MIN -#define INT32_MIN (-2147483647 - 1) -#endif -#ifndef INT8_MAX -#define INT8_MAX (127) -#endif -#ifndef INT16_MAX -#define INT16_MAX (32767) -#endif -#ifndef INT32_MAX -#define INT32_MAX (2147483647) -#endif -#ifndef UINT8_MAX -#define UINT8_MAX (255U) -#endif -#ifndef UINT16_MAX -#define UINT16_MAX (65535U) -#endif -#ifndef UINT32_MAX -#define UINT32_MAX (4294967295U) -#endif - -#ifndef SIZE_MAX -#define SIZE_MAX (~(size_t)0) -#endif - -#endif /* ! C99 */ - -#endif /* ! FLEXINT_H */ - -/* %endif */ - -/* begin standard C++ headers. */ -/* %if-c++-only */ -#include -#include -#include -#include -#include -/* end standard C++ headers. */ -/* %endif */ - -/* TODO: this is always defined, so inline it */ -#define yyconst const - -#if defined(__GNUC__) && __GNUC__ >= 3 -#define yynoreturn __attribute__((__noreturn__)) -#else -#define yynoreturn -#endif - -/* %not-for-header */ -/* Returned upon end-of-file. */ -#define YY_NULL 0 -/* %ok-for-header */ - -/* %not-for-header */ -/* Promotes a possibly negative, possibly signed char to an - * integer in range [0..255] for use as an array index. - */ -#define YY_SC_TO_UI(c) ((YY_CHAR)(c)) -/* %ok-for-header */ - -/* %if-reentrant */ -/* %endif */ - -/* %if-not-reentrant */ - -/* %endif */ - -/* Enter a start condition. This macro really ought to take a parameter, - * but we do it the disgusting crufty way forced on us by the ()-less - * definition of BEGIN. - */ -#define BEGIN (yy_start) = 1 + 2 * -/* Translate the current start state into a value that can be later handed - * to BEGIN to return to the state. The YYSTATE alias is for lex - * compatibility. - */ -#define YY_START (((yy_start)-1) / 2) -#define YYSTATE YY_START -/* Action number for EOF rule of a given start state. */ -#define YY_STATE_EOF(state) (YY_END_OF_BUFFER + state + 1) -/* Special action meaning "start processing a new file". */ -#define YY_NEW_FILE yyrestart(yyin) -#define YY_END_OF_BUFFER_CHAR 0 - -/* Size of default input buffer. */ -#ifndef YY_BUF_SIZE -#ifdef __ia64__ -/* On IA-64, the buffer size is 16k, not 8k. - * Moreover, YY_BUF_SIZE is 2*YY_READ_BUF_SIZE in the general case. - * Ditto for the __ia64__ case accordingly. - */ -#define YY_BUF_SIZE 32768 -#else -#define YY_BUF_SIZE 16384 -#endif /* __ia64__ */ -#endif - -/* The state buf must be large enough to hold one state per character in the - * main buffer. - */ -#define YY_STATE_BUF_SIZE ((YY_BUF_SIZE + 2) * sizeof(yy_state_type)) - -#ifndef YY_TYPEDEF_YY_BUFFER_STATE -#define YY_TYPEDEF_YY_BUFFER_STATE -typedef struct yy_buffer_state* YY_BUFFER_STATE; -#endif - -#ifndef YY_TYPEDEF_YY_SIZE_T -#define YY_TYPEDEF_YY_SIZE_T -typedef size_t yy_size_t; -#endif - -/* %if-not-reentrant */ -extern int yyleng; -/* %endif */ - -/* %if-c-only */ -/* %if-not-reentrant */ -/* %endif */ -/* %endif */ - -#define EOB_ACT_CONTINUE_SCAN 0 -#define EOB_ACT_END_OF_FILE 1 -#define EOB_ACT_LAST_MATCH 2 - -#define YY_LESS_LINENO(n) -#define YY_LINENO_REWIND_TO(ptr) - -/* Return all but the first "n" matched characters back to the input stream. */ -#define yyless(n) \ - do { \ - /* Undo effects of setting up yytext. */ \ - int yyless_macro_arg = (n); \ - YY_LESS_LINENO(yyless_macro_arg); \ - *yy_cp = (yy_hold_char); \ - YY_RESTORE_YY_MORE_OFFSET(yy_c_buf_p) = yy_cp = \ - yy_bp + yyless_macro_arg - YY_MORE_ADJ; \ - YY_DO_BEFORE_ACTION; /* set up yytext again */ \ - } while (0) -#define unput(c) yyunput(c, (yytext_ptr)) - -#ifndef YY_STRUCT_YY_BUFFER_STATE -#define YY_STRUCT_YY_BUFFER_STATE -struct yy_buffer_state { - /* %if-c-only */ - /* %endif */ - - /* %if-c++-only */ - std::streambuf* yy_input_file; - /* %endif */ - - char* yy_ch_buf; /* input buffer */ - char* yy_buf_pos; /* current position in input buffer */ - - /* Size of input buffer in bytes, not including room for EOB - * characters. - */ - int yy_buf_size; - - /* Number of characters read into yy_ch_buf, not including EOB - * characters. - */ - int yy_n_chars; - - /* Whether we "own" the buffer - i.e., we know we created it, - * and can realloc() it to grow it, and should free() it to - * delete it. - */ - int yy_is_our_buffer; - - /* Whether this is an "interactive" input source; if so, and - * if we're using stdio for input, then we want to use getc() - * instead of fread(), to make sure we stop fetching input after - * each newline. - */ - int yy_is_interactive; - - /* Whether we're considered to be at the beginning of a line. - * If so, '^' rules will be active on the next match, otherwise - * not. - */ - int yy_at_bol; - - int yy_bs_lineno; /**< The line count. */ - int yy_bs_column; /**< The column count. */ - - /* Whether to try to fill the input buffer when we reach the - * end of it. - */ - int yy_fill_buffer; - - int yy_buffer_status; - -#define YY_BUFFER_NEW 0 -#define YY_BUFFER_NORMAL 1 - /* When an EOF's been seen but there's still some text to process - * then we mark the buffer as YY_EOF_PENDING, to indicate that we - * shouldn't try reading from the input source any more. We might - * still have a bunch of tokens to match, though, because of - * possible backing-up. - * - * When we actually see the EOF, we change the status to "new" - * (via yyrestart()), so that the user can continue scanning by - * just pointing yyin at a new input file. - */ -#define YY_BUFFER_EOF_PENDING 2 -}; -#endif /* !YY_STRUCT_YY_BUFFER_STATE */ - -/* %if-c-only Standard (non-C++) definition */ -/* %not-for-header */ -/* %if-not-reentrant */ -/* %endif */ -/* %ok-for-header */ - -/* %endif */ - -/* We provide macros for accessing buffer states in case in the - * future we want to put the buffer states in a more general - * "scanner state". - * - * Returns the top of the stack, or NULL. - */ -#define YY_CURRENT_BUFFER \ - ((yy_buffer_stack) ? (yy_buffer_stack)[(yy_buffer_stack_top)] : NULL) -/* Same as previous macro, but useful when we know that the buffer stack is not - * NULL or when we need an lvalue. For internal use only. - */ -#define YY_CURRENT_BUFFER_LVALUE (yy_buffer_stack)[(yy_buffer_stack_top)] - -/* %if-c-only Standard (non-C++) definition */ -/* %if-not-reentrant */ -/* %not-for-header */ -/* %ok-for-header */ - -/* %endif */ -/* %endif */ - -void* yyalloc(yy_size_t); -void* yyrealloc(void*, yy_size_t); -void yyfree(void*); - -#define yy_new_buffer yy_create_buffer -#define yy_set_interactive(is_interactive) \ - { \ - if (!YY_CURRENT_BUFFER) { \ - yyensure_buffer_stack(); \ - YY_CURRENT_BUFFER_LVALUE = yy_create_buffer(yyin, YY_BUF_SIZE); \ - } \ - YY_CURRENT_BUFFER_LVALUE->yy_is_interactive = is_interactive; \ - } -#define yy_set_bol(at_bol) \ - { \ - if (!YY_CURRENT_BUFFER) { \ - yyensure_buffer_stack(); \ - YY_CURRENT_BUFFER_LVALUE = yy_create_buffer(yyin, YY_BUF_SIZE); \ - } \ - YY_CURRENT_BUFFER_LVALUE->yy_at_bol = at_bol; \ - } -#define YY_AT_BOL() (YY_CURRENT_BUFFER_LVALUE->yy_at_bol) - -/* %% [1.0] yytext/yyin/yyout/yy_state_type/yylineno etc. def's & init go here - */ -/* Begin user sect3 */ -#define YY_SKIP_YYWRAP - -#define FLEX_DEBUG -typedef flex_uint8_t YY_CHAR; - -#define yytext_ptr yytext -#define YY_INTERACTIVE - -#include - -int yyFlexLexer::yywrap() { return 1; } -int yyFlexLexer::yylex() { - LexerError("yyFlexLexer::yylex invoked but %option yyclass used"); - return 0; -} - -#define YY_DECL int cynthia::parser::ltlf::LTLfScanner::yylex() - -/* %% [1.5] DFA */ - -/* %if-c-only Standard (non-C++) definition */ -/* %endif */ - -/* Done after the current pattern has been matched and before the - * corresponding action - sets up yytext. - */ -#define YY_DO_BEFORE_ACTION \ - (yytext_ptr) = yy_bp; \ - /* %% [2.0] code to fiddle yytext and yyleng for yymore() goes here \ */ \ - yyleng = (int)(yy_cp - yy_bp); \ - (yy_hold_char) = *yy_cp; \ - *yy_cp = '\0'; \ - /* %% [3.0] code to copy yytext_ptr to yytext[] goes here, if %array \ */ \ - (yy_c_buf_p) = yy_cp; -/* %% [4.0] data tables for the DFA and the user's section 1 definitions go here - */ -#define YY_NUM_RULES 23 -#define YY_END_OF_BUFFER 24 -/* This struct is not used in this scanner, - but its presence is necessary. */ -struct yy_trans_info { - flex_int32_t yy_verify; - flex_int32_t yy_nxt; -}; -static const flex_int16_t yy_accept[53] = { - 0, 0, 0, 24, 23, 22, 21, 13, 11, 1, 2, 23, 23, 23, 7, 8, 6, 5, - 4, 20, 20, 20, 20, 20, 20, 12, 22, 11, 10, 0, 0, 0, 20, 20, 20, 15, - 20, 20, 14, 20, 12, 9, 0, 19, 20, 20, 20, 3, 20, 18, 16, 17, 0}; - -static const YY_CHAR yy_ec[256] = { - 0, 1, 1, 1, 1, 1, 1, 1, 1, 2, 3, 1, 1, 2, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 4, 1, 1, 1, 1, - 5, 1, 6, 7, 1, 8, 1, 9, 1, 1, 10, 10, 10, 10, 10, 10, 10, 10, 10, - 10, 1, 1, 11, 12, 13, 1, 1, 1, 1, 1, 1, 1, 14, 15, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 16, 1, 1, 17, 18, 1, 19, 1, 1, 20, 1, 21, 1, - 22, 1, 23, 22, 22, 24, - - 25, 26, 22, 22, 22, 22, 22, 27, 22, 28, 22, 22, 22, 29, 30, 31, 32, 22, 33, - 22, 22, 22, 1, 34, 1, 35, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, - - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1}; - -static const YY_CHAR yy_meta[36] = {0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1}; - -static const flex_int16_t yy_base[54] = { - 0, 0, 0, 69, 70, 34, 36, 70, 63, 70, 70, 54, 31, 53, 70, 70, 70, 70, - 45, 0, 36, 18, 40, 16, 54, 27, 46, 70, 70, 47, 46, 54, 0, 33, 29, 0, - 25, 22, 0, 70, 70, 70, 32, 0, 22, 20, 25, 70, 21, 0, 0, 0, 70, 40}; - -static const flex_int16_t yy_def[54] = { - 0, 52, 1, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, - 52, 53, 53, 53, 53, 53, 53, 52, 52, 52, 52, 52, 52, 52, 53, 53, 53, 53, - 53, 53, 53, 52, 52, 52, 52, 53, 53, 53, 53, 52, 53, 53, 53, 53, 0, 52}; - -static const flex_int16_t yy_nxt[106] = { - 0, 4, 5, 6, 7, 8, 9, 10, 4, 11, 4, 12, 13, 4, 14, 15, 16, - 17, 16, 18, 4, 4, 19, 19, 19, 20, 21, 22, 19, 19, 19, 23, 19, 24, - 25, 7, 26, 26, 26, 26, 29, 34, 32, 30, 35, 37, 51, 38, 26, 26, 50, - 49, 48, 47, 46, 45, 44, 43, 42, 41, 41, 40, 39, 36, 33, 31, 28, 28, - 27, 52, 3, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, - 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, - - 52, 52, 52, 52, 52}; - -static const flex_int16_t yy_chk[106] = { - 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 5, 5, 6, 6, 12, 21, 53, 12, 21, 23, 48, 23, 26, 26, 46, - 45, 44, 42, 37, 36, 34, 33, 31, 30, 29, 25, 24, 22, 20, 18, 13, 11, - 8, 3, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, - 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, 52, - - 52, 52, 52, 52, 52}; - -static const flex_int16_t yy_rule_linenum[23] = {0, 38, 39, 41, 42, 43, 44, 45, - 46, 48, 49, 51, 52, 54, 56, 57, - 59, 60, 62, 63, 65, 70, 75}; - -/* The intent behind this definition is that it'll catch - * any uses of REJECT which flex missed. - */ -#define REJECT reject_used_but_not_detected -#define yymore() yymore_used_but_not_detected -#define YY_MORE_ADJ 0 -#define YY_RESTORE_YY_MORE_OFFSET -#line 1 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" -#line 8 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" -/* C++ string header, for string ops below */ -#include - -/* Implementation of yyFlexLTLfScanner */ -#include "cynthia/parser/scanner_internal.hpp" -#undef YY_DECL -#define YY_DECL \ - int cynthia::parser::ltlf::LTLfScanner::yylex( \ - cynthia::parser::ltlf::LTLf_YYSTYPE* lval, \ - cynthia::parser::ltlf::LTLfParser::location_type* loc) - -/* typedef to make the returns for the tokens shorter */ -using token = cynthia::parser::ltlf::LTLfParser::token; - -/* define yyterminate as this instead of NULL */ -#define yyterminate() return (token::END_OF_FILE) - -/* msvc2010 requires that we exclude this header file. */ -#define YY_NO_UNISTD_H - -/* update location on matching */ -#define YY_USER_ACTION \ - loc->step(); \ - loc->columns(yyleng); - -#line 563 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.yy.cc" -#line 564 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.yy.cc" - -#define INITIAL 0 - -#ifndef YY_NO_UNISTD_H -/* Special case for "unistd.h", since it is non-ANSI. We include it way - * down here because we want the user's section 1 to have been scanned first. - * The user has a chance to override it with an option. - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -#include -/* %endif */ -#endif - -#ifndef YY_EXTRA_TYPE -#define YY_EXTRA_TYPE void* -#endif - -/* %if-c-only Reentrant structure and macros (non-C++). */ -/* %if-reentrant */ -/* %if-c-only */ -/* %endif */ -/* %if-reentrant */ -/* %endif */ -/* %endif End reentrant structures and macros. */ -/* %if-bison-bridge */ -/* %endif */ -/* %not-for-header */ -/* %ok-for-header */ - -/* %endif */ - -#ifndef yytext_ptr -static void yy_flex_strncpy(char*, const char*, int); -#endif - -#ifdef YY_NEED_STRLEN -static int yy_flex_strlen(const char*); -#endif - -#ifndef YY_NO_INPUT -/* %if-c-only Standard (non-C++) definition */ -/* %not-for-header */ -/* %ok-for-header */ - -/* %endif */ -#endif - -/* %if-c-only */ -/* %endif */ - -/* Amount of stuff to slurp up with each read. */ -#ifndef YY_READ_BUF_SIZE -#ifdef __ia64__ -/* On IA-64, the buffer size is 16k, not 8k */ -#define YY_READ_BUF_SIZE 16384 -#else -#define YY_READ_BUF_SIZE 8192 -#endif /* __ia64__ */ -#endif - -/* Copy whatever the last rule matched to the standard output. */ -#ifndef ECHO -/* %if-c-only Standard (non-C++) definition */ -/* %endif */ -/* %if-c++-only C++ definition */ -#define ECHO LexerOutput(yytext, yyleng) -/* %endif */ -#endif - -/* Gets input and stuffs it into "buf". number of characters read, or YY_NULL, - * is returned in "result". - */ -#ifndef YY_INPUT -#define YY_INPUT(buf, result, max_size) \ - /* %% [5.0] fread()/read() definition of YY_INPUT goes here unless we're \ - * doing C++ \ */ \ - \ - /* %if-c++-only C++ definition \ */ \ - if ((int)(result = LexerInput((char*)buf, max_size)) < 0) \ - YY_FATAL_ERROR("input in flex scanner failed"); -/* %endif */ - -#endif - -/* No semi-colon after return; correct usage is to write "yyterminate();" - - * we don't want an extra ';' after the "return" because that will cause - * some compilers to complain about unreachable statements. - */ -#ifndef yyterminate -#define yyterminate() return YY_NULL -#endif - -/* Number of entries by which start-condition stack grows. */ -#ifndef YY_START_STACK_INCR -#define YY_START_STACK_INCR 25 -#endif - -/* Report a fatal error. */ -#ifndef YY_FATAL_ERROR -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -#define YY_FATAL_ERROR(msg) LexerError(msg) -/* %endif */ -#endif - -/* %if-tables-serialization structures and prototypes */ -/* %not-for-header */ -/* %ok-for-header */ - -/* %not-for-header */ -/* %tables-yydmap generated elements */ -/* %endif */ -/* end tables serialization structures and prototypes */ - -/* %ok-for-header */ - -/* Default declaration of generated scanner - a define so the user can - * easily add parameters. - */ -#ifndef YY_DECL -#define YY_DECL_IS_OURS 1 -/* %if-c-only Standard (non-C++) definition */ -/* %endif */ -/* %if-c++-only C++ definition */ -#define YY_DECL int yyFlexLexer::yylex() -/* %endif */ -#endif /* !YY_DECL */ - -/* Code executed at the beginning of each rule, after yytext and yyleng - * have been set up. - */ -#ifndef YY_USER_ACTION -#define YY_USER_ACTION -#endif - -/* Code executed at the end of each rule. */ -#ifndef YY_BREAK -#define YY_BREAK /*LINTED*/ break; -#endif - -/* %% [6.0] YY_RULE_SETUP definition goes here */ -#define YY_RULE_SETUP YY_USER_ACTION - -/* %not-for-header */ -/** The main scanner function which does all the work. - */ -YY_DECL { - yy_state_type yy_current_state; - char *yy_cp, *yy_bp; - int yy_act; - - if (!(yy_init)) { - (yy_init) = 1; - -#ifdef YY_USER_INIT - YY_USER_INIT; -#endif - - if (!(yy_start)) - (yy_start) = 1; /* first start state */ - - if (!yyin) - /* %if-c-only */ - /* %endif */ - /* %if-c++-only */ - yyin.rdbuf(std::cin.rdbuf()); - /* %endif */ - - if (!yyout) - /* %if-c-only */ - /* %endif */ - /* %if-c++-only */ - yyout.rdbuf(std::cout.rdbuf()); - /* %endif */ - - if (!YY_CURRENT_BUFFER) { - yyensure_buffer_stack(); - YY_CURRENT_BUFFER_LVALUE = yy_create_buffer(yyin, YY_BUF_SIZE); - } - - yy_load_buffer_state(); - } - - { -/* %% [7.0] user's declarations go here */ -#line 31 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - - /** Code executed at the beginning of yylex **/ -#line 35 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - yylval = lval; - -#line 764 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.yy.cc" - - while (/*CONSTCOND*/ 1) /* loops until end-of-file is reached */ - { - /* %% [8.0] yymore()-related code goes here */ - yy_cp = (yy_c_buf_p); - - /* Support of yytext. */ - *yy_cp = (yy_hold_char); - - /* yy_bp points to the position in yy_ch_buf of the start of - * the current run. - */ - yy_bp = yy_cp; - - /* %% [9.0] code to set up and find next match goes here */ - yy_current_state = (yy_start); - yy_match: - do { - YY_CHAR yy_c = yy_ec[YY_SC_TO_UI(*yy_cp)]; - if (yy_accept[yy_current_state]) { - (yy_last_accepting_state) = yy_current_state; - (yy_last_accepting_cpos) = yy_cp; - } - while (yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state) { - yy_current_state = (int)yy_def[yy_current_state]; - if (yy_current_state >= 53) - yy_c = yy_meta[yy_c]; - } - yy_current_state = yy_nxt[yy_base[yy_current_state] + yy_c]; - ++yy_cp; - } while (yy_base[yy_current_state] != 70); - - yy_find_action: - /* %% [10.0] code to find the action number goes here */ - yy_act = yy_accept[yy_current_state]; - if (yy_act == 0) { /* have to back up */ - yy_cp = (yy_last_accepting_cpos); - yy_current_state = (yy_last_accepting_state); - yy_act = yy_accept[yy_current_state]; - } - - YY_DO_BEFORE_ACTION; - - /* %% [11.0] code for yylineno update goes here */ - - do_action: /* This label is used only to access EOF actions. */ - - /* %% [12.0] debug code goes here */ - if (yy_flex_debug) { - if (yy_act == 0) - std::cerr << "--scanner backing up\n"; - else if (yy_act < 23) - std::cerr << "--accepting rule at line " << yy_rule_linenum[yy_act] - << "(\"" << yytext << "\")\n"; - else if (yy_act == 23) - std::cerr << "--accepting default rule (\"" << yytext << "\")\n"; - else if (yy_act == 24) - std::cerr << "--(end of buffer or a NUL)\n"; - else - std::cerr << "--EOF (start condition " << YY_START << ")\n"; - } - - switch (yy_act) { /* beginning of action switch */ - /* %% [13.0] actions go here */ - case 0: /* must back up */ - /* undo the effects of YY_DO_BEFORE_ACTION */ - *yy_cp = (yy_hold_char); - yy_cp = (yy_last_accepting_cpos); - yy_current_state = (yy_last_accepting_state); - goto yy_find_action; - - case 1: - YY_RULE_SETUP -#line 38 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::LPAR; - } - YY_BREAK - case 2: - YY_RULE_SETUP -#line 39 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::RPAR; - } - YY_BREAK - case 3: - YY_RULE_SETUP -#line 41 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::NEXT; - } - YY_BREAK - case 4: - YY_RULE_SETUP -#line 42 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::WEAK_NEXT; - } - YY_BREAK - case 5: - YY_RULE_SETUP -#line 43 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::UNTIL; - } - YY_BREAK - case 6: - YY_RULE_SETUP -#line 44 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::RELEASE; - } - YY_BREAK - case 7: - YY_RULE_SETUP -#line 45 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::EVENTUALLY; - } - YY_BREAK - case 8: - YY_RULE_SETUP -#line 46 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::ALWAYS; - } - YY_BREAK - case 9: - YY_RULE_SETUP -#line 48 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::EQUIVALENCE; - } - YY_BREAK - case 10: - YY_RULE_SETUP -#line 49 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::IMPLICATION; - } - YY_BREAK - case 11: - YY_RULE_SETUP -#line 51 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::AND; - } - YY_BREAK - case 12: - YY_RULE_SETUP -#line 52 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::OR; - } - YY_BREAK - case 13: - YY_RULE_SETUP -#line 54 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::NOT; - } - YY_BREAK - case 14: - YY_RULE_SETUP -#line 56 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::TT; - } - YY_BREAK - case 15: - YY_RULE_SETUP -#line 57 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::FF; - } - YY_BREAK - case 16: - YY_RULE_SETUP -#line 59 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::TRUE_; - } - YY_BREAK - case 17: - YY_RULE_SETUP -#line 60 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::FALSE_; - } - YY_BREAK - case 18: - YY_RULE_SETUP -#line 62 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::LAST; - } - YY_BREAK - case 19: - YY_RULE_SETUP -#line 63 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - return token::END; - } - YY_BREAK - case 20: - YY_RULE_SETUP -#line 65 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - yylval->symbol_name = yytext; - return token::SYMBOL; - } - YY_BREAK - case 21: - /* rule 21 can match eol */ - YY_RULE_SETUP -#line 70 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - // Update line number - loc->lines(); - return token::NEWLINE; - } - YY_BREAK - case 22: - /* rule 22 can match eol */ - YY_RULE_SETUP -#line 75 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - { - ; - } - YY_BREAK - case 23: - YY_RULE_SETUP -#line 77 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" - ECHO; - YY_BREAK -#line 967 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.yy.cc" - case YY_STATE_EOF(INITIAL): - yyterminate(); - - case YY_END_OF_BUFFER: { - /* Amount of text matched not including the EOB char. */ - int yy_amount_of_matched_text = (int)(yy_cp - (yytext_ptr)) - 1; - - /* Undo the effects of YY_DO_BEFORE_ACTION. */ - *yy_cp = (yy_hold_char); - YY_RESTORE_YY_MORE_OFFSET - - if (YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_NEW) { - /* We're scanning a new file or input source. It's - * possible that this happened because the user - * just pointed yyin at a new source and called - * yylex(). If so, then we have to assure - * consistency between YY_CURRENT_BUFFER and our - * globals. Here is the right place to do so, because - * this is the first action (other than possibly a - * back-up) that will match for the new input source. - */ - (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars; - /* %if-c-only */ - /* %endif */ - /* %if-c++-only */ - YY_CURRENT_BUFFER_LVALUE->yy_input_file = yyin.rdbuf(); - /* %endif */ - YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_NORMAL; - } - - /* Note that here we test for yy_c_buf_p "<=" to the position - * of the first EOB in the buffer, since yy_c_buf_p will - * already have been incremented past the NUL character - * (since all states make transitions on EOB to the - * end-of-buffer state). Contrast this with the test - * in input(). - */ - if ((yy_c_buf_p) <= - &YY_CURRENT_BUFFER_LVALUE - ->yy_ch_buf[(yy_n_chars)]) { /* This was really a NUL. */ - yy_state_type yy_next_state; - - (yy_c_buf_p) = (yytext_ptr) + yy_amount_of_matched_text; - - yy_current_state = yy_get_previous_state(); - - /* Okay, we're now positioned to make the NUL - * transition. We couldn't have - * yy_get_previous_state() go ahead and do it - * for us because it doesn't know how to deal - * with the possibility of jamming (and we don't - * want to build jamming into it because then it - * will run more slowly). - */ - - yy_next_state = yy_try_NUL_trans(yy_current_state); - - yy_bp = (yytext_ptr) + YY_MORE_ADJ; - - if (yy_next_state) { - /* Consume the NUL. */ - yy_cp = ++(yy_c_buf_p); - yy_current_state = yy_next_state; - goto yy_match; - } - - else { - /* %% [14.0] code to do back-up for compressed tables and set up - * yy_cp goes here */ - yy_cp = (yy_c_buf_p); - goto yy_find_action; - } - } - - else - switch (yy_get_next_buffer()) { - case EOB_ACT_END_OF_FILE: { - (yy_did_buffer_switch_on_eof) = 0; - - if (yywrap()) { - /* Note: because we've taken care in - * yy_get_next_buffer() to have set up - * yytext, we can now set up - * yy_c_buf_p so that if some total - * hoser (like flex itself) wants to - * call the scanner after we return the - * YY_NULL, it'll still work - another - * YY_NULL will get returned. - */ - (yy_c_buf_p) = (yytext_ptr) + YY_MORE_ADJ; - - yy_act = YY_STATE_EOF(YY_START); - goto do_action; - } - - else { - if (!(yy_did_buffer_switch_on_eof)) - YY_NEW_FILE; - } - break; - } - - case EOB_ACT_CONTINUE_SCAN: - (yy_c_buf_p) = (yytext_ptr) + yy_amount_of_matched_text; - - yy_current_state = yy_get_previous_state(); - - yy_cp = (yy_c_buf_p); - yy_bp = (yytext_ptr) + YY_MORE_ADJ; - goto yy_match; - - case EOB_ACT_LAST_MATCH: - (yy_c_buf_p) = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)]; - - yy_current_state = yy_get_previous_state(); - - yy_cp = (yy_c_buf_p); - yy_bp = (yytext_ptr) + YY_MORE_ADJ; - goto yy_find_action; - } - break; - } - - default: - YY_FATAL_ERROR("fatal flex scanner internal error--no action found"); - } /* end of action switch */ - } /* end of scanning one token */ - } /* end of user's declarations */ -} /* end of yylex */ -/* %ok-for-header */ - -/* %if-c++-only */ -/* %not-for-header */ -/* The contents of this function are C++ specific, so the () macro is not used. - * This constructor simply maintains backward compatibility. - * DEPRECATED - */ -yyFlexLexer::yyFlexLexer(std::istream* arg_yyin, std::ostream* arg_yyout) - : yyin(arg_yyin ? arg_yyin->rdbuf() : std::cin.rdbuf()), - yyout(arg_yyout ? arg_yyout->rdbuf() : std::cout.rdbuf()) { - ctor_common(); -} - -/* The contents of this function are C++ specific, so the () macro is not used. - */ -yyFlexLexer::yyFlexLexer(std::istream& arg_yyin, std::ostream& arg_yyout) - : yyin(arg_yyin.rdbuf()), yyout(arg_yyout.rdbuf()) { - ctor_common(); -} - -/* The contents of this function are C++ specific, so the () macro is not used. - */ -void yyFlexLexer::ctor_common() { - yy_c_buf_p = 0; - yy_init = 0; - yy_start = 0; - yy_flex_debug = 0; - yylineno = 1; // this will only get updated if %option yylineno - - yy_did_buffer_switch_on_eof = 0; - - yy_looking_for_trail_begin = 0; - yy_more_flag = 0; - yy_more_len = 0; - yy_more_offset = yy_prev_more_offset = 0; - - yy_start_stack_ptr = yy_start_stack_depth = 0; - yy_start_stack = NULL; - - yy_buffer_stack = NULL; - yy_buffer_stack_top = 0; - yy_buffer_stack_max = 0; - - yy_state_buf = 0; -} - -/* The contents of this function are C++ specific, so the () macro is not used. - */ -yyFlexLexer::~yyFlexLexer() { - delete[] yy_state_buf; - yyfree(yy_start_stack); - yy_delete_buffer(YY_CURRENT_BUFFER); - yyfree(yy_buffer_stack); -} - -/* The contents of this function are C++ specific, so the () macro is not used. - */ -void yyFlexLexer::switch_streams(std::istream& new_in, std::ostream& new_out) { - // was if( new_in ) - yy_delete_buffer(YY_CURRENT_BUFFER); - yy_switch_to_buffer(yy_create_buffer(new_in, YY_BUF_SIZE)); - - // was if( new_out ) - yyout.rdbuf(new_out.rdbuf()); -} - -/* The contents of this function are C++ specific, so the () macro is not used. - */ -void yyFlexLexer::switch_streams(std::istream* new_in, std::ostream* new_out) { - if (!new_in) { - new_in = &yyin; - } - - if (!new_out) { - new_out = &yyout; - } - - switch_streams(*new_in, *new_out); -} - -#ifdef YY_INTERACTIVE -int yyFlexLexer::LexerInput(char* buf, int /* max_size */) -#else -int yyFlexLexer::LexerInput(char* buf, int max_size) -#endif -{ - if (yyin.eof() || yyin.fail()) - return 0; - -#ifdef YY_INTERACTIVE - yyin.get(buf[0]); - - if (yyin.eof()) - return 0; - - if (yyin.bad()) - return -1; - - return 1; - -#else - (void)yyin.read(buf, max_size); - - if (yyin.bad()) - return -1; - else - return yyin.gcount(); -#endif -} - -void yyFlexLexer::LexerOutput(const char* buf, int size) { - (void)yyout.write(buf, size); -} -/* %ok-for-header */ - -/* %endif */ - -/* yy_get_next_buffer - try to read in a new buffer - * - * Returns a code representing an action: - * EOB_ACT_LAST_MATCH - - * EOB_ACT_CONTINUE_SCAN - continue scanning from current position - * EOB_ACT_END_OF_FILE - end of file - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -int yyFlexLexer::yy_get_next_buffer() -/* %endif */ -{ - char* dest = YY_CURRENT_BUFFER_LVALUE->yy_ch_buf; - char* source = (yytext_ptr); - int number_to_move, i; - int ret_val; - - if ((yy_c_buf_p) > &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1]) - YY_FATAL_ERROR("fatal flex scanner internal error--end of buffer missed"); - - if (YY_CURRENT_BUFFER_LVALUE->yy_fill_buffer == - 0) { /* Don't try to fill the buffer, so this is an EOF. */ - if ((yy_c_buf_p) - (yytext_ptr)-YY_MORE_ADJ == 1) { - /* We matched a single character, the EOB, so - * treat this as a final EOF. - */ - return EOB_ACT_END_OF_FILE; - } - - else { - /* We matched some text prior to the EOB, first - * process it. - */ - return EOB_ACT_LAST_MATCH; - } - } - - /* Try to read more data. */ - - /* First move last chars to start of buffer. */ - number_to_move = (int)((yy_c_buf_p) - (yytext_ptr)-1); - - for (i = 0; i < number_to_move; ++i) - *(dest++) = *(source++); - - if (YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_EOF_PENDING) - /* don't do the read, it's not guaranteed to return an EOF, - * just force an EOF - */ - YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars) = 0; - - else { - int num_to_read = - YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1; - - while (num_to_read <= 0) { /* Not enough room in the buffer - grow it. */ - - /* just a shorter name for the current buffer */ - YY_BUFFER_STATE b = YY_CURRENT_BUFFER_LVALUE; - - int yy_c_buf_p_offset = (int)((yy_c_buf_p)-b->yy_ch_buf); - - if (b->yy_is_our_buffer) { - int new_size = b->yy_buf_size * 2; - - if (new_size <= 0) - b->yy_buf_size += b->yy_buf_size / 8; - else - b->yy_buf_size *= 2; - - b->yy_ch_buf = (char*) - /* Include room in for 2 EOB chars. */ - yyrealloc((void*)b->yy_ch_buf, (yy_size_t)(b->yy_buf_size + 2)); - } else - /* Can't grow it, we don't own it. */ - b->yy_ch_buf = NULL; - - if (!b->yy_ch_buf) - YY_FATAL_ERROR("fatal error - scanner input buffer overflow"); - - (yy_c_buf_p) = &b->yy_ch_buf[yy_c_buf_p_offset]; - - num_to_read = YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1; - } - - if (num_to_read > YY_READ_BUF_SIZE) - num_to_read = YY_READ_BUF_SIZE; - - /* Read in more data. */ - YY_INPUT((&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]), - (yy_n_chars), num_to_read); - - YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars); - } - - if ((yy_n_chars) == 0) { - if (number_to_move == YY_MORE_ADJ) { - ret_val = EOB_ACT_END_OF_FILE; - yyrestart(yyin); - } - - else { - ret_val = EOB_ACT_LAST_MATCH; - YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_EOF_PENDING; - } - } - - else - ret_val = EOB_ACT_CONTINUE_SCAN; - - if (((yy_n_chars) + number_to_move) > YY_CURRENT_BUFFER_LVALUE->yy_buf_size) { - /* Extend the array by 50%, plus the number we really need. */ - int new_size = (yy_n_chars) + number_to_move + ((yy_n_chars) >> 1); - YY_CURRENT_BUFFER_LVALUE->yy_ch_buf = (char*)yyrealloc( - (void*)YY_CURRENT_BUFFER_LVALUE->yy_ch_buf, (yy_size_t)new_size); - if (!YY_CURRENT_BUFFER_LVALUE->yy_ch_buf) - YY_FATAL_ERROR("out of dynamic memory in yy_get_next_buffer()"); - /* "- 2" to take care of EOB's */ - YY_CURRENT_BUFFER_LVALUE->yy_buf_size = (int)(new_size - 2); - } - - (yy_n_chars) += number_to_move; - YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] = YY_END_OF_BUFFER_CHAR; - YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] = YY_END_OF_BUFFER_CHAR; - - (yytext_ptr) = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[0]; - - return ret_val; -} - -/* yy_get_previous_state - get the state just before the EOB char was reached */ - -/* %if-c-only */ -/* %not-for-header */ -/* %endif */ -/* %if-c++-only */ -yy_state_type yyFlexLexer::yy_get_previous_state() -/* %endif */ -{ - yy_state_type yy_current_state; - char* yy_cp; - - /* %% [15.0] code to get the start state into yy_current_state goes here */ - yy_current_state = (yy_start); - - for (yy_cp = (yytext_ptr) + YY_MORE_ADJ; yy_cp < (yy_c_buf_p); ++yy_cp) { - /* %% [16.0] code to find the next state goes here */ - YY_CHAR yy_c = (*yy_cp ? yy_ec[YY_SC_TO_UI(*yy_cp)] : 1); - if (yy_accept[yy_current_state]) { - (yy_last_accepting_state) = yy_current_state; - (yy_last_accepting_cpos) = yy_cp; - } - while (yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state) { - yy_current_state = (int)yy_def[yy_current_state]; - if (yy_current_state >= 53) - yy_c = yy_meta[yy_c]; - } - yy_current_state = yy_nxt[yy_base[yy_current_state] + yy_c]; - } - - return yy_current_state; -} - -/* yy_try_NUL_trans - try to make a transition on the NUL character - * - * synopsis - * next_state = yy_try_NUL_trans( current_state ); - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -yy_state_type yyFlexLexer::yy_try_NUL_trans(yy_state_type yy_current_state) -/* %endif */ -{ - int yy_is_jam; - /* %% [17.0] code to find the next state, and perhaps do backing up, goes here - */ - char* yy_cp = (yy_c_buf_p); - - YY_CHAR yy_c = 1; - if (yy_accept[yy_current_state]) { - (yy_last_accepting_state) = yy_current_state; - (yy_last_accepting_cpos) = yy_cp; - } - while (yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state) { - yy_current_state = (int)yy_def[yy_current_state]; - if (yy_current_state >= 53) - yy_c = yy_meta[yy_c]; - } - yy_current_state = yy_nxt[yy_base[yy_current_state] + yy_c]; - yy_is_jam = (yy_current_state == 52); - - return yy_is_jam ? 0 : yy_current_state; -} - -#ifndef YY_NO_UNPUT -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yyunput(int c, char* yy_bp) -/* %endif */ -{ - char* yy_cp; - - yy_cp = (yy_c_buf_p); - - /* undo effects of setting up yytext */ - *yy_cp = (yy_hold_char); - - if (yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + - 2) { /* need to shift things up to make room */ - /* +2 for EOB chars. */ - int number_to_move = (yy_n_chars) + 2; - char* dest = &YY_CURRENT_BUFFER_LVALUE - ->yy_ch_buf[YY_CURRENT_BUFFER_LVALUE->yy_buf_size + 2]; - char* source = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]; - - while (source > YY_CURRENT_BUFFER_LVALUE->yy_ch_buf) - *--dest = *--source; - - yy_cp += (int)(dest - source); - yy_bp += (int)(dest - source); - YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars) = - (int)YY_CURRENT_BUFFER_LVALUE->yy_buf_size; - - if (yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2) - YY_FATAL_ERROR("flex scanner push-back overflow"); - } - - *--yy_cp = (char)c; - - /* %% [18.0] update yylineno here */ - - (yytext_ptr) = yy_bp; - (yy_hold_char) = *yy_cp; - (yy_c_buf_p) = yy_cp; -} -/* %if-c-only */ -/* %endif */ -#endif - -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -int yyFlexLexer::yyinput() -/* %endif */ -{ - int c; - - *(yy_c_buf_p) = (yy_hold_char); - - if (*(yy_c_buf_p) == YY_END_OF_BUFFER_CHAR) { - /* yy_c_buf_p now points to the character we want to return. - * If this occurs *before* the EOB characters, then it's a - * valid NUL; if not, then we've hit the end of the buffer. - */ - if ((yy_c_buf_p) < &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)]) - /* This was really a NUL. */ - *(yy_c_buf_p) = '\0'; - - else { /* need more input */ - int offset = (int)((yy_c_buf_p) - (yytext_ptr)); - ++(yy_c_buf_p); - - switch (yy_get_next_buffer()) { - case EOB_ACT_LAST_MATCH: - /* This happens because yy_g_n_b() - * sees that we've accumulated a - * token and flags that we need to - * try matching the token before - * proceeding. But for input(), - * there's no matching to consider. - * So convert the EOB_ACT_LAST_MATCH - * to EOB_ACT_END_OF_FILE. - */ - - /* Reset buffer status. */ - yyrestart(yyin); - - /*FALLTHROUGH*/ - - case EOB_ACT_END_OF_FILE: { - if (yywrap()) - return 0; - - if (!(yy_did_buffer_switch_on_eof)) - YY_NEW_FILE; -#ifdef __cplusplus - return yyinput(); -#else - return input(); -#endif - } - - case EOB_ACT_CONTINUE_SCAN: - (yy_c_buf_p) = (yytext_ptr) + offset; - break; - } - } - } - - c = *(unsigned char*)(yy_c_buf_p); /* cast for 8-bit char's */ - *(yy_c_buf_p) = '\0'; /* preserve yytext */ - (yy_hold_char) = *++(yy_c_buf_p); - - /* %% [19.0] update BOL and yylineno */ - - return c; -} -/* %if-c-only */ -/* %endif */ - -/** Immediately switch to a different input stream. - * @param input_file A readable stream. - * - * @note This function does not reset the start condition to @c INITIAL . - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yyrestart(std::istream& input_file) -/* %endif */ -{ - - if (!YY_CURRENT_BUFFER) { - yyensure_buffer_stack(); - YY_CURRENT_BUFFER_LVALUE = yy_create_buffer(yyin, YY_BUF_SIZE); - } - - yy_init_buffer(YY_CURRENT_BUFFER, input_file); - yy_load_buffer_state(); -} - -/* %if-c++-only */ -/** Delegate to the new version that takes an istream reference. - * @param input_file A readable stream. - * - * @note This function does not reset the start condition to @c INITIAL . - */ -void yyFlexLexer::yyrestart(std::istream* input_file) { - if (!input_file) { - input_file = &yyin; - } - yyrestart(*input_file); -} -/* %endif */ - -/** Switch to a different input buffer. - * @param new_buffer The new input buffer. - * - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yy_switch_to_buffer(YY_BUFFER_STATE new_buffer) -/* %endif */ -{ - - /* TODO. We should be able to replace this entire function body - * with - * yypop_buffer_state(); - * yypush_buffer_state(new_buffer); - */ - yyensure_buffer_stack(); - if (YY_CURRENT_BUFFER == new_buffer) - return; - - if (YY_CURRENT_BUFFER) { - /* Flush out information for old buffer. */ - *(yy_c_buf_p) = (yy_hold_char); - YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p); - YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars); - } - - YY_CURRENT_BUFFER_LVALUE = new_buffer; - yy_load_buffer_state(); - - /* We don't actually know whether we did this switch during - * EOF (yywrap()) processing, but the only time this flag - * is looked at is after yywrap() is called, so it's safe - * to go ahead and always set it. - */ - (yy_did_buffer_switch_on_eof) = 1; -} - -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yy_load_buffer_state() -/* %endif */ -{ - (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars; - (yytext_ptr) = (yy_c_buf_p) = YY_CURRENT_BUFFER_LVALUE->yy_buf_pos; - /* %if-c-only */ - /* %endif */ - /* %if-c++-only */ - yyin.rdbuf(YY_CURRENT_BUFFER_LVALUE->yy_input_file); - /* %endif */ - (yy_hold_char) = *(yy_c_buf_p); -} - -/** Allocate and initialize an input buffer state. - * @param file A readable stream. - * @param size The character buffer size in bytes. When in doubt, use @c - * YY_BUF_SIZE. - * - * @return the allocated buffer state. - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -YY_BUFFER_STATE yyFlexLexer::yy_create_buffer(std::istream& file, int size) -/* %endif */ -{ - YY_BUFFER_STATE b; - - b = (YY_BUFFER_STATE)yyalloc(sizeof(struct yy_buffer_state)); - if (!b) - YY_FATAL_ERROR("out of dynamic memory in yy_create_buffer()"); - - b->yy_buf_size = size; - - /* yy_ch_buf has to be 2 characters longer than the size given because - * we need to put in 2 end-of-buffer characters. - */ - b->yy_ch_buf = (char*)yyalloc((yy_size_t)(b->yy_buf_size + 2)); - if (!b->yy_ch_buf) - YY_FATAL_ERROR("out of dynamic memory in yy_create_buffer()"); - - b->yy_is_our_buffer = 1; - - yy_init_buffer(b, file); - - return b; -} - -/* %if-c++-only */ -/** Delegate creation of buffers to the new version that takes an istream - * reference. - * @param file A readable stream. - * @param size The character buffer size in bytes. When in doubt, use @c - * YY_BUF_SIZE. - * - * @return the allocated buffer state. - */ -YY_BUFFER_STATE yyFlexLexer::yy_create_buffer(std::istream* file, int size) { - return yy_create_buffer(*file, size); -} -/* %endif */ - -/** Destroy the buffer. - * @param b a buffer created with yy_create_buffer() - * - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yy_delete_buffer(YY_BUFFER_STATE b) -/* %endif */ -{ - - if (!b) - return; - - if (b == YY_CURRENT_BUFFER) /* Not sure if we should pop here. */ - YY_CURRENT_BUFFER_LVALUE = (YY_BUFFER_STATE)0; - - if (b->yy_is_our_buffer) - yyfree((void*)b->yy_ch_buf); - - yyfree((void*)b); -} - -/* Initializes or reinitializes a buffer. - * This function is sometimes called more than once on the same buffer, - * such as during a yyrestart() or at EOF. - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yy_init_buffer(YY_BUFFER_STATE b, std::istream& file) -/* %endif */ - -{ - int oerrno = errno; - - yy_flush_buffer(b); - - /* %if-c-only */ - /* %endif */ - /* %if-c++-only */ - b->yy_input_file = file.rdbuf(); - /* %endif */ - b->yy_fill_buffer = 1; - - /* If b is the current buffer, then yy_init_buffer was _probably_ - * called from yyrestart() or through yy_get_next_buffer. - * In that case, we don't want to reset the lineno or column. - */ - if (b != YY_CURRENT_BUFFER) { - b->yy_bs_lineno = 1; - b->yy_bs_column = 0; - } - - /* %if-c-only */ - /* %endif */ - /* %if-c++-only */ - b->yy_is_interactive = 0; - /* %endif */ - errno = oerrno; -} - -/** Discard all buffered characters. On the next scan, YY_INPUT will be called. - * @param b the buffer state to be flushed, usually @c YY_CURRENT_BUFFER. - * - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yy_flush_buffer(YY_BUFFER_STATE b) -/* %endif */ -{ - if (!b) - return; - - b->yy_n_chars = 0; - - /* We always need two end-of-buffer characters. The first causes - * a transition to the end-of-buffer state. The second causes - * a jam in that state. - */ - b->yy_ch_buf[0] = YY_END_OF_BUFFER_CHAR; - b->yy_ch_buf[1] = YY_END_OF_BUFFER_CHAR; - - b->yy_buf_pos = &b->yy_ch_buf[0]; - - b->yy_at_bol = 1; - b->yy_buffer_status = YY_BUFFER_NEW; - - if (b == YY_CURRENT_BUFFER) - yy_load_buffer_state(); -} - -/* %if-c-or-c++ */ -/** Pushes the new state onto the stack. The new state becomes - * the current state. This function will allocate the stack - * if necessary. - * @param new_buffer The new state. - * - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yypush_buffer_state(YY_BUFFER_STATE new_buffer) -/* %endif */ -{ - if (new_buffer == NULL) - return; - - yyensure_buffer_stack(); - - /* This block is copied from yy_switch_to_buffer. */ - if (YY_CURRENT_BUFFER) { - /* Flush out information for old buffer. */ - *(yy_c_buf_p) = (yy_hold_char); - YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p); - YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars); - } - - /* Only push if top exists. Otherwise, replace top. */ - if (YY_CURRENT_BUFFER) - (yy_buffer_stack_top)++; - YY_CURRENT_BUFFER_LVALUE = new_buffer; - - /* copied from yy_switch_to_buffer. */ - yy_load_buffer_state(); - (yy_did_buffer_switch_on_eof) = 1; -} -/* %endif */ - -/* %if-c-or-c++ */ -/** Removes and deletes the top of the stack, if present. - * The next element becomes the new top. - * - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yypop_buffer_state(void) -/* %endif */ -{ - if (!YY_CURRENT_BUFFER) - return; - - yy_delete_buffer(YY_CURRENT_BUFFER); - YY_CURRENT_BUFFER_LVALUE = NULL; - if ((yy_buffer_stack_top) > 0) - --(yy_buffer_stack_top); - - if (YY_CURRENT_BUFFER) { - yy_load_buffer_state(); - (yy_did_buffer_switch_on_eof) = 1; - } -} -/* %endif */ - -/* %if-c-or-c++ */ -/* Allocates the stack if it does not exist. - * Guarantees space for at least one push. - */ -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yyensure_buffer_stack(void) -/* %endif */ -{ - yy_size_t num_to_alloc; - - if (!(yy_buffer_stack)) { - - /* First allocation is just for 2 elements, since we don't know if this - * scanner will even need a stack. We use 2 instead of 1 to avoid an - * immediate realloc on the next call. - */ - num_to_alloc = 1; /* After all that talk, this was set to 1 anyways... */ - (yy_buffer_stack) = (struct yy_buffer_state**)yyalloc( - num_to_alloc * sizeof(struct yy_buffer_state*)); - if (!(yy_buffer_stack)) - YY_FATAL_ERROR("out of dynamic memory in yyensure_buffer_stack()"); - - memset((yy_buffer_stack), 0, - num_to_alloc * sizeof(struct yy_buffer_state*)); - - (yy_buffer_stack_max) = num_to_alloc; - (yy_buffer_stack_top) = 0; - return; - } - - if ((yy_buffer_stack_top) >= ((yy_buffer_stack_max)) - 1) { - - /* Increase the buffer to prepare for a possible push. */ - yy_size_t grow_size = 8 /* arbitrary grow size */; - - num_to_alloc = (yy_buffer_stack_max) + grow_size; - (yy_buffer_stack) = (struct yy_buffer_state**)yyrealloc( - (yy_buffer_stack), num_to_alloc * sizeof(struct yy_buffer_state*)); - if (!(yy_buffer_stack)) - YY_FATAL_ERROR("out of dynamic memory in yyensure_buffer_stack()"); - - /* zero only the new slots.*/ - memset((yy_buffer_stack) + (yy_buffer_stack_max), 0, - grow_size * sizeof(struct yy_buffer_state*)); - (yy_buffer_stack_max) = num_to_alloc; - } -} -/* %endif */ - -/* %if-c-only */ -/* %endif */ - -/* %if-c-only */ -/* %endif */ - -/* %if-c-only */ -/* %endif */ - -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yy_push_state(int _new_state) -/* %endif */ -{ - if ((yy_start_stack_ptr) >= (yy_start_stack_depth)) { - yy_size_t new_size; - - (yy_start_stack_depth) += YY_START_STACK_INCR; - new_size = (yy_size_t)(yy_start_stack_depth) * sizeof(int); - - if (!(yy_start_stack)) - (yy_start_stack) = (int*)yyalloc(new_size); - - else - (yy_start_stack) = (int*)yyrealloc((void*)(yy_start_stack), new_size); - - if (!(yy_start_stack)) - YY_FATAL_ERROR("out of memory expanding start-condition stack"); - } - - (yy_start_stack)[(yy_start_stack_ptr)++] = YY_START; - - BEGIN(_new_state); -} - -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::yy_pop_state() -/* %endif */ -{ - if (--(yy_start_stack_ptr) < 0) - YY_FATAL_ERROR("start-condition stack underflow"); - - BEGIN((yy_start_stack)[(yy_start_stack_ptr)]); -} - -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -int yyFlexLexer::yy_top_state() -/* %endif */ -{ - return (yy_start_stack)[(yy_start_stack_ptr)-1]; -} - -#ifndef YY_EXIT_FAILURE -#define YY_EXIT_FAILURE 2 -#endif - -/* %if-c-only */ -/* %endif */ -/* %if-c++-only */ -void yyFlexLexer::LexerError(const char* msg) { - std::cerr << msg << std::endl; - exit(YY_EXIT_FAILURE); -} -/* %endif */ - -/* Redefine yyless() so it works in section 3 code. */ - -#undef yyless -#define yyless(n) \ - do { \ - /* Undo effects of setting up yytext. */ \ - int yyless_macro_arg = (n); \ - YY_LESS_LINENO(yyless_macro_arg); \ - yytext[yyleng] = (yy_hold_char); \ - (yy_c_buf_p) = yytext + yyless_macro_arg; \ - (yy_hold_char) = *(yy_c_buf_p); \ - *(yy_c_buf_p) = '\0'; \ - yyleng = yyless_macro_arg; \ - } while (0) - -/* Accessor methods (get/set functions) to struct members. */ - -/* %if-c-only */ -/* %if-reentrant */ -/* %endif */ -/* %if-reentrant */ -/* %endif */ -/* %endif */ - -/* %if-reentrant */ -/* %if-bison-bridge */ -/* %endif */ -/* %endif if-c-only */ - -/* %if-c-only */ -/* %endif */ - -/* %if-c-only SNIP! this currently causes conflicts with the c++ scanner */ -/* %if-reentrant */ -/* %endif */ -/* %endif */ - -/* - * Internal utility routines. - */ - -#ifndef yytext_ptr -static void yy_flex_strncpy(char* s1, const char* s2, int n) { - - int i; - for (i = 0; i < n; ++i) - s1[i] = s2[i]; -} -#endif - -#ifdef YY_NEED_STRLEN -static int yy_flex_strlen(const char* s) { - int n; - for (n = 0; s[n]; ++n) - ; - - return n; -} -#endif - -void* yyalloc(yy_size_t size) { return malloc(size); } - -void* yyrealloc(void* ptr, yy_size_t size) { - - /* The cast to (char *) in the following accommodates both - * implementations that use char* generic pointers, and those - * that use void* generic pointers. It works with the latter - * because both ANSI C and C++ allow castless assignment from - * any pointer type to void*, and deal with argument conversions - * as though doing an assignment. - */ - return realloc(ptr, size); -} - -void yyfree(void* ptr) { - free((char*)ptr); /* see yyrealloc() for (char *) cast */ -} - -/* %if-tables-serialization definitions */ -/* %define-yytables The name for this specific scanner's tables. */ -#define YYTABLES_NAME "yytables" -/* %endif */ - -/* %ok-for-header */ - -#line 77 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/lexer.l" diff --git a/libs/parser/include/cynthia/parser/location.hh b/libs/parser/include/cynthia/parser/location.hh deleted file mode 100644 index bc265f7..0000000 --- a/libs/parser/include/cynthia/parser/location.hh +++ /dev/null @@ -1,269 +0,0 @@ -// A Bison parser, made by GNU Bison 3.5.1. - -// Locations for Bison parsers in C++ - -// Copyright (C) 2002-2015, 2018-2020 Free Software Foundation, Inc. - -// This program is free software: you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation, either version 3 of the License, or -// (at your option) any later version. - -// This program is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. - -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -// As a special exception, you may create a larger work that contains -// part or all of the Bison parser skeleton and distribute that work -// under terms of your choice, so long as that work isn't itself a -// parser generator using the skeleton or a modified version thereof -// as a parser skeleton. Alternatively, if you modify or redistribute -// the parser skeleton itself, you may (at your option) remove this -// special exception, which will cause the skeleton and the resulting -// Bison output files to be licensed under the GNU General Public -// License without this special exception. - -// This special exception was added by the Free Software Foundation in -// version 2.2 of Bison. - -/** - ** \file - * /home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/location.hh - ** Define the cynthia::parser::ltlf::location class. - */ - -#ifndef YY_LTLF_HOME_MARCOFAVORITO_WORKFOLDER_CYNTHIA_LIBS_PARSER_INCLUDE_CYNTHIA_PARSER_LOCATION_HH_INCLUDED -#define YY_LTLF_HOME_MARCOFAVORITO_WORKFOLDER_CYNTHIA_LIBS_PARSER_INCLUDE_CYNTHIA_PARSER_LOCATION_HH_INCLUDED - -#include -#include - -#ifndef YY_NULLPTR -#if defined __cplusplus -#if 201103L <= __cplusplus -#define YY_NULLPTR nullptr -#else -#define YY_NULLPTR 0 -#endif -#else -#define YY_NULLPTR ((void*)0) -#endif -#endif - -#line 6 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" -namespace cynthia { -namespace parser { -namespace ltlf { -#line 59 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/location.hh" - -/// A point in a source file. -class position { -public: - /// Type for line and column numbers. - typedef int counter_type; - - /// Construct a position. - explicit position(std::string* f = YY_NULLPTR, counter_type l = 1, - counter_type c = 1) - : filename(f), line(l), column(c) {} - - /// Initialization. - void initialize(std::string* fn = YY_NULLPTR, counter_type l = 1, - counter_type c = 1) { - filename = fn; - line = l; - column = c; - } - - /** \name Line and Column related manipulators - ** \{ */ - /// (line related) Advance to the COUNT next lines. - void lines(counter_type count = 1) { - if (count) { - column = 1; - line = add_(line, count, 1); - } - } - - /// (column related) Advance to the COUNT next columns. - void columns(counter_type count = 1) { column = add_(column, count, 1); } - /** \} */ - - /// File name to which this position refers. - std::string* filename; - /// Current line number. - counter_type line; - /// Current column number. - counter_type column; - -private: - /// Compute max (min, lhs+rhs). - static counter_type add_(counter_type lhs, counter_type rhs, - counter_type min) { - return lhs + rhs < min ? min : lhs + rhs; - } -}; - -/// Add \a width columns, in place. -inline position& operator+=(position& res, position::counter_type width) { - res.columns(width); - return res; -} - -/// Add \a width columns. -inline position operator+(position res, position::counter_type width) { - return res += width; -} - -/// Subtract \a width columns, in place. -inline position& operator-=(position& res, position::counter_type width) { - return res += -width; -} - -/// Subtract \a width columns. -inline position operator-(position res, position::counter_type width) { - return res -= width; -} - -/// Compare two position objects. -inline bool operator==(const position& pos1, const position& pos2) { - return ( - pos1.line == pos2.line && pos1.column == pos2.column && - (pos1.filename == pos2.filename || - (pos1.filename && pos2.filename && *pos1.filename == *pos2.filename))); -} - -/// Compare two position objects. -inline bool operator!=(const position& pos1, const position& pos2) { - return !(pos1 == pos2); -} - -/** \brief Intercept output stream redirection. - ** \param ostr the destination output stream - ** \param pos a reference to the position to redirect - */ -template -std::basic_ostream& operator<<(std::basic_ostream& ostr, - const position& pos) { - if (pos.filename) - ostr << *pos.filename << ':'; - return ostr << pos.line << '.' << pos.column; -} - -/// Two points in a source file. -class location { -public: - /// Type for line and column numbers. - typedef position::counter_type counter_type; - - /// Construct a location from \a b to \a e. - location(const position& b, const position& e) : begin(b), end(e) {} - - /// Construct a 0-width location in \a p. - explicit location(const position& p = position()) : begin(p), end(p) {} - - /// Construct a 0-width location in \a f, \a l, \a c. - explicit location(std::string* f, counter_type l = 1, counter_type c = 1) - : begin(f, l, c), end(f, l, c) {} - - /// Initialization. - void initialize(std::string* f = YY_NULLPTR, counter_type l = 1, - counter_type c = 1) { - begin.initialize(f, l, c); - end = begin; - } - - /** \name Line and Column related manipulators - ** \{ */ -public: - /// Reset initial location to final location. - void step() { begin = end; } - - /// Extend the current location to the COUNT next columns. - void columns(counter_type count = 1) { end += count; } - - /// Extend the current location to the COUNT next lines. - void lines(counter_type count = 1) { end.lines(count); } - /** \} */ - -public: - /// Beginning of the located region. - position begin; - /// End of the located region. - position end; -}; - -/// Join two locations, in place. -inline location& operator+=(location& res, const location& end) { - res.end = end.end; - return res; -} - -/// Join two locations. -inline location operator+(location res, const location& end) { - return res += end; -} - -/// Add \a width columns to the end position, in place. -inline location& operator+=(location& res, location::counter_type width) { - res.columns(width); - return res; -} - -/// Add \a width columns to the end position. -inline location operator+(location res, location::counter_type width) { - return res += width; -} - -/// Subtract \a width columns to the end position, in place. -inline location& operator-=(location& res, location::counter_type width) { - return res += -width; -} - -/// Subtract \a width columns to the end position. -inline location operator-(location res, location::counter_type width) { - return res -= width; -} - -/// Compare two location objects. -inline bool operator==(const location& loc1, const location& loc2) { - return loc1.begin == loc2.begin && loc1.end == loc2.end; -} - -/// Compare two location objects. -inline bool operator!=(const location& loc1, const location& loc2) { - return !(loc1 == loc2); -} - -/** \brief Intercept output stream redirection. - ** \param ostr the destination output stream - ** \param loc a reference to the location to redirect - ** - ** Avoid duplicate information. - */ -template -std::basic_ostream& operator<<(std::basic_ostream& ostr, - const location& loc) { - location::counter_type end_col = 0 < loc.end.column ? loc.end.column - 1 : 0; - ostr << loc.begin; - if (loc.end.filename && - (!loc.begin.filename || *loc.begin.filename != *loc.end.filename)) - ostr << '-' << loc.end.filename << ':' << loc.end.line << '.' << end_col; - else if (loc.begin.line < loc.end.line) - ostr << '-' << loc.end.line << '.' << end_col; - else if (loc.begin.column < end_col) - ostr << '-' << end_col; - return ostr; -} - -#line 6 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" -} // namespace ltlf -} // namespace parser -} // namespace cynthia -#line 333 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/location.hh" - -#endif // !YY_LTLF_HOME_MARCOFAVORITO_WORKFOLDER_CYNTHIA_LIBS_PARSER_INCLUDE_CYNTHIA_PARSER_LOCATION_HH_INCLUDED diff --git a/libs/parser/include/cynthia/parser/parser.tab.cc b/libs/parser/include/cynthia/parser/parser.tab.cc deleted file mode 100644 index 92f5979..0000000 --- a/libs/parser/include/cynthia/parser/parser.tab.cc +++ /dev/null @@ -1,917 +0,0 @@ -// A Bison parser, made by GNU Bison 3.5.1. - -// Skeleton implementation for Bison LALR(1) parsers in C++ - -// Copyright (C) 2002-2015, 2018-2020 Free Software Foundation, Inc. - -// This program is free software: you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation, either version 3 of the License, or -// (at your option) any later version. - -// This program is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. - -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -// As a special exception, you may create a larger work that contains -// part or all of the Bison parser skeleton and distribute that work -// under terms of your choice, so long as that work isn't itself a -// parser generator using the skeleton or a modified version thereof -// as a parser skeleton. Alternatively, if you modify or redistribute -// the parser skeleton itself, you may (at your option) remove this -// special exception, which will cause the skeleton and the resulting -// Bison output files to be licensed under the GNU General Public -// License without this special exception. - -// This special exception was added by the Free Software Foundation in -// version 2.2 of Bison. - -// Undocumented macros, especially those whose name start with YY_, -// are private implementation details. Do not rely on them. - -// Take the name prefix into account. -#define yylex ltlflex - -#include "parser.tab.hh" - -// Unqualified %code blocks. -#line 37 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - -#include -#include -#include - -/* include for all driver functions */ -#include "cynthia/parser/driver.hpp" -#include "cynthia/parser/scanner.hpp" - -#undef yylex -#define yylex scanner.ltlflex - -#line 60 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - -#ifndef YY_ -#if defined YYENABLE_NLS && YYENABLE_NLS -#if ENABLE_NLS -#include // FIXME: INFRINGES ON USER NAME SPACE. -#define YY_(msgid) dgettext("bison-runtime", msgid) -#endif -#endif -#ifndef YY_ -#define YY_(msgid) msgid -#endif -#endif - -// Whether we are compiled with exception support. -#ifndef YY_EXCEPTIONS -#if defined __GNUC__ && !defined __EXCEPTIONS -#define YY_EXCEPTIONS 0 -#else -#define YY_EXCEPTIONS 1 -#endif -#endif - -#define YYRHSLOC(Rhs, K) ((Rhs)[K].location) -/* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N]. - If N is 0, then set CURRENT to the empty location which ends - the previous symbol: RHS[0] (always defined). */ - -#ifndef YYLLOC_DEFAULT -#define YYLLOC_DEFAULT(Current, Rhs, N) \ - do \ - if (N) { \ - (Current).begin = YYRHSLOC(Rhs, 1).begin; \ - (Current).end = YYRHSLOC(Rhs, N).end; \ - } else { \ - (Current).begin = (Current).end = YYRHSLOC(Rhs, 0).end; \ - } \ - while (false) -#endif - -// Enable debugging if requested. -#if LTLFDEBUG - -// A pseudo ostream that takes yydebug_ into account. -#define YYCDEBUG \ - if (yydebug_) \ - (*yycdebug_) - -#define YY_SYMBOL_PRINT(Title, Symbol) \ - do { \ - if (yydebug_) { \ - *yycdebug_ << Title << ' '; \ - yy_print_(*yycdebug_, Symbol); \ - *yycdebug_ << '\n'; \ - } \ - } while (false) - -#define YY_REDUCE_PRINT(Rule) \ - do { \ - if (yydebug_) \ - yy_reduce_print_(Rule); \ - } while (false) - -#define YY_STACK_PRINT() \ - do { \ - if (yydebug_) \ - yystack_print_(); \ - } while (false) - -#else // !LTLFDEBUG - -#define YYCDEBUG \ - if (false) \ - std::cerr -#define YY_SYMBOL_PRINT(Title, Symbol) YYUSE(Symbol) -#define YY_REDUCE_PRINT(Rule) static_cast(0) -#define YY_STACK_PRINT() static_cast(0) - -#endif // !LTLFDEBUG - -#define yyerrok (yyerrstatus_ = 0) -#define yyclearin (yyla.clear()) - -#define YYACCEPT goto yyacceptlab -#define YYABORT goto yyabortlab -#define YYERROR goto yyerrorlab -#define YYRECOVERING() (!!yyerrstatus_) - -#line 6 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" -namespace cynthia { -namespace parser { -namespace ltlf { -#line 152 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - -/// Build a parser object. -LTLfParser::LTLfParser(LTLfScanner& scanner_yyarg, LTLfDriver& d_yyarg) -#if LTLFDEBUG - : yydebug_(false), yycdebug_(&std::cerr), -#else - : -#endif - scanner(scanner_yyarg), d(d_yyarg) { -} - -LTLfParser::~LTLfParser() {} - -LTLfParser::syntax_error::~syntax_error() YY_NOEXCEPT YY_NOTHROW {} - -/*---------------. -| Symbol types. | -`---------------*/ - -// basic_symbol. -#if 201103L <= YY_CPLUSPLUS -template -LTLfParser::basic_symbol::basic_symbol(basic_symbol&& that) - : Base(std::move(that)), value(std::move(that.value)), - location(std::move(that.location)) {} -#endif - -template -LTLfParser::basic_symbol::basic_symbol(const basic_symbol& that) - : Base(that), value(that.value), location(that.location) {} - -/// Constructor for valueless symbols. -template -LTLfParser::basic_symbol::basic_symbol(typename Base::kind_type t, - YY_MOVE_REF(location_type) l) - : Base(t), value(), location(l) {} - -template -LTLfParser::basic_symbol::basic_symbol(typename Base::kind_type t, - YY_RVREF(semantic_type) v, - YY_RVREF(location_type) l) - : Base(t), value(YY_MOVE(v)), location(YY_MOVE(l)) {} - -template -bool LTLfParser::basic_symbol::empty() const YY_NOEXCEPT { - return Base::type_get() == empty_symbol; -} - -template -void LTLfParser::basic_symbol::move(basic_symbol& s) { - super_type::move(s); - value = YY_MOVE(s.value); - location = YY_MOVE(s.location); -} - -// by_type. -LTLfParser::by_type::by_type() : type(empty_symbol) {} - -#if 201103L <= YY_CPLUSPLUS -LTLfParser::by_type::by_type(by_type&& that) : type(that.type) { that.clear(); } -#endif - -LTLfParser::by_type::by_type(const by_type& that) : type(that.type) {} - -LTLfParser::by_type::by_type(token_type t) : type(yytranslate_(t)) {} - -void LTLfParser::by_type::clear() { type = empty_symbol; } - -void LTLfParser::by_type::move(by_type& that) { - type = that.type; - that.clear(); -} - -int LTLfParser::by_type::type_get() const YY_NOEXCEPT { return type; } - -// by_state. -LTLfParser::by_state::by_state() YY_NOEXCEPT : state(empty_state) {} - -LTLfParser::by_state::by_state(const by_state& that) YY_NOEXCEPT - : state(that.state) {} - -void LTLfParser::by_state::clear() YY_NOEXCEPT { state = empty_state; } - -void LTLfParser::by_state::move(by_state& that) { - state = that.state; - that.clear(); -} - -LTLfParser::by_state::by_state(state_type s) YY_NOEXCEPT : state(s) {} - -LTLfParser::symbol_number_type -LTLfParser::by_state::type_get() const YY_NOEXCEPT { - if (state == empty_state) - return empty_symbol; - else - return yystos_[+state]; -} - -LTLfParser::stack_symbol_type::stack_symbol_type() {} - -LTLfParser::stack_symbol_type::stack_symbol_type(YY_RVREF(stack_symbol_type) - that) - : super_type(YY_MOVE(that.state), YY_MOVE(that.value), - YY_MOVE(that.location)) { -#if 201103L <= YY_CPLUSPLUS - // that is emptied. - that.state = empty_state; -#endif -} - -LTLfParser::stack_symbol_type::stack_symbol_type(state_type s, - YY_MOVE_REF(symbol_type) that) - : super_type(s, YY_MOVE(that.value), YY_MOVE(that.location)) { - // that is emptied. - that.type = empty_symbol; -} - -#if YY_CPLUSPLUS < 201103L -LTLfParser::stack_symbol_type& -LTLfParser::stack_symbol_type::operator=(const stack_symbol_type& that) { - state = that.state; - value = that.value; - location = that.location; - return *this; -} - -LTLfParser::stack_symbol_type& -LTLfParser::stack_symbol_type::operator=(stack_symbol_type& that) { - state = that.state; - value = that.value; - location = that.location; - // that is emptied. - that.state = empty_state; - return *this; -} -#endif - -template -void LTLfParser::yy_destroy_(const char* yymsg, - basic_symbol& yysym) const { - if (yymsg) - YY_SYMBOL_PRINT(yymsg, yysym); - - // User destructor. - YYUSE(yysym.type_get()); -} - -#if LTLFDEBUG -template -void LTLfParser::yy_print_(std::ostream& yyo, - const basic_symbol& yysym) const { - std::ostream& yyoutput = yyo; - YYUSE(yyoutput); - symbol_number_type yytype = yysym.type_get(); -#if defined __GNUC__ && !defined __clang__ && !defined __ICC && \ - __GNUC__ * 100 + __GNUC_MINOR__ <= 408 - // Avoid a (spurious) G++ 4.8 warning about "array subscript is - // below array bounds". - if (yysym.empty()) - std::abort(); -#endif - yyo << (yytype < yyntokens_ ? "token" : "nterm") << ' ' << yytname_[yytype] - << " (" << yysym.location << ": "; - YYUSE(yytype); - yyo << ')'; -} -#endif - -void LTLfParser::yypush_(const char* m, YY_MOVE_REF(stack_symbol_type) sym) { - if (m) - YY_SYMBOL_PRINT(m, sym); - yystack_.push(YY_MOVE(sym)); -} - -void LTLfParser::yypush_(const char* m, state_type s, - YY_MOVE_REF(symbol_type) sym) { -#if 201103L <= YY_CPLUSPLUS - yypush_(m, stack_symbol_type(s, std::move(sym))); -#else - stack_symbol_type ss(s, sym); - yypush_(m, ss); -#endif -} - -void LTLfParser::yypop_(int n) { yystack_.pop(n); } - -#if LTLFDEBUG -std::ostream& LTLfParser::debug_stream() const { return *yycdebug_; } - -void LTLfParser::set_debug_stream(std::ostream& o) { yycdebug_ = &o; } - -LTLfParser::debug_level_type LTLfParser::debug_level() const { - return yydebug_; -} - -void LTLfParser::set_debug_level(debug_level_type l) { yydebug_ = l; } -#endif // LTLFDEBUG - -LTLfParser::state_type LTLfParser::yy_lr_goto_state_(state_type yystate, - int yysym) { - int yyr = yypgoto_[yysym - yyntokens_] + yystate; - if (0 <= yyr && yyr <= yylast_ && yycheck_[yyr] == yystate) - return yytable_[yyr]; - else - return yydefgoto_[yysym - yyntokens_]; -} - -bool LTLfParser::yy_pact_value_is_default_(int yyvalue) { - return yyvalue == yypact_ninf_; -} - -bool LTLfParser::yy_table_value_is_error_(int yyvalue) { - return yyvalue == yytable_ninf_; -} - -int LTLfParser::operator()() { return parse(); } - -int LTLfParser::parse() { - int yyn; - /// Length of the RHS of the rule being reduced. - int yylen = 0; - - // Error handling. - int yynerrs_ = 0; - int yyerrstatus_ = 0; - - /// The lookahead symbol. - symbol_type yyla; - - /// The locations where the error started and ended. - stack_symbol_type yyerror_range[3]; - - /// The return value of parse (). - int yyresult; - -#if YY_EXCEPTIONS - try -#endif // YY_EXCEPTIONS - { - YYCDEBUG << "Starting parse\n"; - - /* Initialize the stack. The initial state will be set in - yynewstate, since the latter expects the semantical and the - location values to have been already stored, initialize these - stacks with a primary value. */ - yystack_.clear(); - yypush_(YY_NULLPTR, 0, YY_MOVE(yyla)); - - /*-----------------------------------------------. - | yynewstate -- push a new symbol on the stack. | - `-----------------------------------------------*/ - yynewstate: - YYCDEBUG << "Entering state " << int(yystack_[0].state) << '\n'; - - // Accept? - if (yystack_[0].state == yyfinal_) - YYACCEPT; - - goto yybackup; - - /*-----------. - | yybackup. | - `-----------*/ - yybackup: - // Try to take a decision without lookahead. - yyn = yypact_[+yystack_[0].state]; - if (yy_pact_value_is_default_(yyn)) - goto yydefault; - - // Read a lookahead token. - if (yyla.empty()) { - YYCDEBUG << "Reading a token: "; -#if YY_EXCEPTIONS - try -#endif // YY_EXCEPTIONS - { - yyla.type = yytranslate_(yylex(&yyla.value, &yyla.location)); - } -#if YY_EXCEPTIONS - catch (const syntax_error& yyexc) { - YYCDEBUG << "Caught exception: " << yyexc.what() << '\n'; - error(yyexc); - goto yyerrlab1; - } -#endif // YY_EXCEPTIONS - } - YY_SYMBOL_PRINT("Next token is", yyla); - - /* If the proper action on seeing token YYLA.TYPE is to reduce or - to detect an error, take that action. */ - yyn += yyla.type_get(); - if (yyn < 0 || yylast_ < yyn || yycheck_[yyn] != yyla.type_get()) { - goto yydefault; - } - - // Reduce or error. - yyn = yytable_[yyn]; - if (yyn <= 0) { - if (yy_table_value_is_error_(yyn)) - goto yyerrlab; - yyn = -yyn; - goto yyreduce; - } - - // Count tokens shifted since error; after three, turn off error status. - if (yyerrstatus_) - --yyerrstatus_; - - // Shift the lookahead token. - yypush_("Shifting", state_type(yyn), YY_MOVE(yyla)); - goto yynewstate; - - /*-----------------------------------------------------------. - | yydefault -- do the default action for the current state. | - `-----------------------------------------------------------*/ - yydefault: - yyn = yydefact_[+yystack_[0].state]; - if (yyn == 0) - goto yyerrlab; - goto yyreduce; - - /*-----------------------------. - | yyreduce -- do a reduction. | - `-----------------------------*/ - yyreduce: - yylen = yyr2_[yyn]; - { - stack_symbol_type yylhs; - yylhs.state = yy_lr_goto_state_(yystack_[yylen].state, yyr1_[yyn]); - /* If YYLEN is nonzero, implement the default value of the - action: '$$ = $1'. Otherwise, use the top of the stack. - - Otherwise, the following line sets YYLHS.VALUE to garbage. - This behavior is undocumented and Bison users should not rely - upon it. */ - if (yylen) - yylhs.value = yystack_[yylen - 1].value; - else - yylhs.value = yystack_[0].value; - - // Default location. - { - stack_type::slice range(yystack_, yylen); - YYLLOC_DEFAULT(yylhs.location, range, yylen); - yyerror_range[1].location = yylhs.location; - } - - // Perform the reduction. - YY_REDUCE_PRINT(yyn); -#if YY_EXCEPTIONS - try -#endif // YY_EXCEPTIONS - { - switch (yyn) { - case 2: -#line 88 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - (yylhs.value.formula) = (yystack_[0].value.formula); - } -#line 608 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 3: -#line 91 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 614 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 4: -#line 92 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 620 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 5: -#line 93 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 626 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 6: -#line 94 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 632 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 7: -#line 95 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 638 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 8: -#line 96 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 644 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 9: -#line 97 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 650 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 10: -#line 98 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 656 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 11: -#line 99 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 662 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 12: -#line 100 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 668 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 13: -#line 101 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 674 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 14: -#line 102 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 680 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 15: -#line 103 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 686 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 16: -#line 104 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 692 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 17: -#line 105 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 698 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 18: -#line 106 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 704 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 19: -#line 107 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 710 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 20: -#line 108 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - } -#line 716 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - - case 21: -#line 111 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - { - (yylhs.value.formula) = (yystack_[1].value.formula); - } -#line 722 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - break; - -#line 726 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - - default: - break; - } - } -#if YY_EXCEPTIONS - catch (const syntax_error& yyexc) { - YYCDEBUG << "Caught exception: " << yyexc.what() << '\n'; - error(yyexc); - YYERROR; - } -#endif // YY_EXCEPTIONS - YY_SYMBOL_PRINT("-> $$ =", yylhs); - yypop_(yylen); - yylen = 0; - YY_STACK_PRINT(); - - // Shift the result of the reduction. - yypush_(YY_NULLPTR, YY_MOVE(yylhs)); - } - goto yynewstate; - - /*--------------------------------------. - | yyerrlab -- here on detecting error. | - `--------------------------------------*/ - yyerrlab: - // If not already recovering from an error, report this error. - if (!yyerrstatus_) { - ++yynerrs_; - error(yyla.location, yysyntax_error_(yystack_[0].state, yyla)); - } - - yyerror_range[1].location = yyla.location; - if (yyerrstatus_ == 3) { - /* If just tried and failed to reuse lookahead token after an - error, discard it. */ - - // Return failure if at end of input. - if (yyla.type_get() == yyeof_) - YYABORT; - else if (!yyla.empty()) { - yy_destroy_("Error: discarding", yyla); - yyla.clear(); - } - } - - // Else will try to reuse lookahead token after shifting the error token. - goto yyerrlab1; - - /*---------------------------------------------------. - | yyerrorlab -- error raised explicitly by YYERROR. | - `---------------------------------------------------*/ - yyerrorlab: - /* Pacify compilers when the user code never invokes YYERROR and - the label yyerrorlab therefore never appears in user code. */ - if (false) - YYERROR; - - /* Do not reclaim the symbols of the rule whose action triggered - this YYERROR. */ - yypop_(yylen); - yylen = 0; - goto yyerrlab1; - - /*-------------------------------------------------------------. - | yyerrlab1 -- common code for both syntax error and YYERROR. | - `-------------------------------------------------------------*/ - yyerrlab1: - yyerrstatus_ = 3; // Each real token shifted decrements this. - { - stack_symbol_type error_token; - for (;;) { - yyn = yypact_[+yystack_[0].state]; - if (!yy_pact_value_is_default_(yyn)) { - yyn += yy_error_token_; - if (0 <= yyn && yyn <= yylast_ && yycheck_[yyn] == yy_error_token_) { - yyn = yytable_[yyn]; - if (0 < yyn) - break; - } - } - - // Pop the current state because it cannot handle the error token. - if (yystack_.size() == 1) - YYABORT; - - yyerror_range[1].location = yystack_[0].location; - yy_destroy_("Error: popping", yystack_[0]); - yypop_(); - YY_STACK_PRINT(); - } - - yyerror_range[2].location = yyla.location; - YYLLOC_DEFAULT(error_token.location, yyerror_range, 2); - - // Shift the error token. - error_token.state = state_type(yyn); - yypush_("Shifting", YY_MOVE(error_token)); - } - goto yynewstate; - - /*-------------------------------------. - | yyacceptlab -- YYACCEPT comes here. | - `-------------------------------------*/ - yyacceptlab: - yyresult = 0; - goto yyreturn; - - /*-----------------------------------. - | yyabortlab -- YYABORT comes here. | - `-----------------------------------*/ - yyabortlab: - yyresult = 1; - goto yyreturn; - - /*-----------------------------------------------------. - | yyreturn -- parsing is finished, return the result. | - `-----------------------------------------------------*/ - yyreturn: - if (!yyla.empty()) - yy_destroy_("Cleanup: discarding lookahead", yyla); - - /* Do not reclaim the symbols of the rule whose action triggered - this YYABORT or YYACCEPT. */ - yypop_(yylen); - while (1 < yystack_.size()) { - yy_destroy_("Cleanup: popping", yystack_[0]); - yypop_(); - } - - return yyresult; - } -#if YY_EXCEPTIONS - catch (...) { - YYCDEBUG << "Exception caught: cleaning lookahead and stack\n"; - // Do not try to display the values of the reclaimed symbols, - // as their printers might throw an exception. - if (!yyla.empty()) - yy_destroy_(YY_NULLPTR, yyla); - - while (1 < yystack_.size()) { - yy_destroy_(YY_NULLPTR, yystack_[0]); - yypop_(); - } - throw; - } -#endif // YY_EXCEPTIONS -} - -void LTLfParser::error(const syntax_error& yyexc) { - error(yyexc.location, yyexc.what()); -} - -// Generate an error message. -std::string LTLfParser::yysyntax_error_(state_type, const symbol_type&) const { - return YY_("syntax error"); -} - -const signed char LTLfParser::yypact_ninf_ = -13; - -const signed char LTLfParser::yytable_ninf_ = -1; - -const signed char LTLfParser::yypact_[] = { - 10, 10, -13, -13, -13, -13, -13, -13, -13, 10, 10, 10, - 10, 10, 7, -12, 24, -13, -13, -13, -13, -13, -13, 10, - 10, 10, 10, 10, 10, -13, 29, 29, 18, 31, -4, -13}; - -const signed char LTLfParser::yydefact_[] = { - 0, 0, 19, 18, 14, 15, 16, 17, 20, 0, 0, 0, 0, 0, 0, 2, 0, 10, - 9, 12, 11, 13, 1, 0, 0, 0, 0, 0, 0, 21, 3, 4, 6, 5, 7, 8}; - -const signed char LTLfParser::yypgoto_[] = {-13, -13, -1}; - -const signed char LTLfParser::yydefgoto_[] = {-1, 14, 15}; - -const signed char LTLfParser::yytable_[] = { - 16, 23, 24, 25, 26, 27, 28, 22, 17, 18, 19, 20, 21, 1, 28, 2, 3, - 4, 5, 6, 7, 8, 30, 31, 32, 33, 34, 35, 29, 9, 10, 11, 12, 13, - 26, 27, 28, 23, 24, 25, 26, 27, 28, 24, 25, 26, 27, 28, 27, 28}; - -const signed char LTLfParser::yycheck_[] = { - 1, 13, 14, 15, 16, 17, 18, 0, 9, 10, 11, 12, 13, 3, 18, 5, 6, - 7, 8, 9, 10, 11, 23, 24, 25, 26, 27, 28, 4, 19, 20, 21, 22, 23, - 16, 17, 18, 13, 14, 15, 16, 17, 18, 14, 15, 16, 17, 18, 17, 18}; - -const signed char LTLfParser::yystos_[] = { - 0, 3, 5, 6, 7, 8, 9, 10, 11, 19, 20, 21, 22, 23, 25, 26, 26, 26, - 26, 26, 26, 26, 0, 13, 14, 15, 16, 17, 18, 4, 26, 26, 26, 26, 26, 26}; - -const signed char LTLfParser::yyr1_[] = {0, 24, 25, 26, 26, 26, 26, 26, - 26, 26, 26, 26, 26, 26, 26, 26, - 26, 26, 26, 26, 26, 26}; - -const signed char LTLfParser::yyr2_[] = {0, 2, 1, 3, 3, 3, 3, 3, 3, 2, 2, - 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 3}; - -#if LTLFDEBUG -// YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM. -// First, the terminals, then, starting at \a yyntokens_, nonterminals. -const char* const LTLfParser::yytname_[] = { - "END_OF_FILE", "error", "$undefined", "LPAR", "RPAR", - "TRUE_", "FALSE_", "TT", "FF", "END", - "LAST", "SYMBOL", "NEWLINE", "EQUIVALENCE", "IMPLICATION", - "UNTIL", "RELEASE", "OR", "AND", "EVENTUALLY", - "ALWAYS", "NEXT", "WEAK_NEXT", "NOT", "$accept", - "input", "ltlf_formula", YY_NULLPTR}; - -const signed char LTLfParser::yyrline_[] = { - 0, 88, 88, 91, 92, 93, 94, 95, 96, 97, 98, - 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 111}; - -// Print the state stack on the debug stream. -void LTLfParser::yystack_print_() { - *yycdebug_ << "Stack now"; - for (stack_type::const_iterator i = yystack_.begin(), i_end = yystack_.end(); - i != i_end; ++i) - *yycdebug_ << ' ' << int(i->state); - *yycdebug_ << '\n'; -} - -// Report on the debug stream that the rule \a yyrule is going to be reduced. -void LTLfParser::yy_reduce_print_(int yyrule) { - int yylno = yyrline_[yyrule]; - int yynrhs = yyr2_[yyrule]; - // Print the symbols being reduced, and their result. - *yycdebug_ << "Reducing stack by rule " << yyrule - 1 << " (line " << yylno - << "):\n"; - // The symbols being reduced. - for (int yyi = 0; yyi < yynrhs; yyi++) - YY_SYMBOL_PRINT(" $" << yyi + 1 << " =", yystack_[(yynrhs) - (yyi + 1)]); -} -#endif // LTLFDEBUG - -LTLfParser::token_number_type LTLfParser::yytranslate_(int t) { - // YYTRANSLATE[TOKEN-NUM] -- Symbol number corresponding to - // TOKEN-NUM as returned by yylex. - static const token_number_type translate_table[] = { - 0, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 3, 4, - 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23}; - const int user_token_number_max_ = 278; - - if (t <= 0) - return yyeof_; - else if (t <= user_token_number_max_) - return translate_table[t]; - else - return yy_undef_token_; -} - -#line 6 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" -} // namespace ltlf -} // namespace parser -} // namespace cynthia -#line 1087 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.cc" - -#line 113 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - -void cynthia::parser::ltlf::LTLfParser::error(const location_type& l, - const std::string& err_message) { - std::cerr << "Error: " << err_message << " at " << l << "\n"; -} diff --git a/libs/parser/include/cynthia/parser/parser.tab.hh b/libs/parser/include/cynthia/parser/parser.tab.hh deleted file mode 100644 index 57652df..0000000 --- a/libs/parser/include/cynthia/parser/parser.tab.hh +++ /dev/null @@ -1,665 +0,0 @@ -// A Bison parser, made by GNU Bison 3.5.1. - -// Skeleton interface for Bison LALR(1) parsers in C++ - -// Copyright (C) 2002-2015, 2018-2020 Free Software Foundation, Inc. - -// This program is free software: you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation, either version 3 of the License, or -// (at your option) any later version. - -// This program is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. - -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -// As a special exception, you may create a larger work that contains -// part or all of the Bison parser skeleton and distribute that work -// under terms of your choice, so long as that work isn't itself a -// parser generator using the skeleton or a modified version thereof -// as a parser skeleton. Alternatively, if you modify or redistribute -// the parser skeleton itself, you may (at your option) remove this -// special exception, which will cause the skeleton and the resulting -// Bison output files to be licensed under the GNU General Public -// License without this special exception. - -// This special exception was added by the Free Software Foundation in -// version 2.2 of Bison. - -/** - ** \file - * /home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.hh - ** Define the cynthia::parser::ltlf::parser class. - */ - -// C++ LALR(1) parser skeleton written by Akim Demaille. - -// Undocumented macros, especially those whose name start with YY_, -// are private implementation details. Do not rely on them. - -#ifndef YY_LTLF_HOME_MARCOFAVORITO_WORKFOLDER_CYNTHIA_LIBS_PARSER_INCLUDE_CYNTHIA_PARSER_PARSER_TAB_HH_INCLUDED -#define YY_LTLF_HOME_MARCOFAVORITO_WORKFOLDER_CYNTHIA_LIBS_PARSER_INCLUDE_CYNTHIA_PARSER_PARSER_TAB_HH_INCLUDED -// "%code requires" blocks. -#line 15 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" - -//#include "cynthia/logic/base.hpp" -#include "cynthia/parser/parser_stype.h" -namespace cynthia::parser::ltlf { -class LTLfDriver; -class LTLfScanner; -} // namespace cynthia::parser::ltlf - -// The following definitions is missing when %locations isn't used -#ifndef YY_NULLPTR -#if defined __cplusplus && 201103L <= __cplusplus -#define YY_NULLPTR nullptr -#else -#define YY_NULLPTR 0 -#endif -#endif - -#line 67 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.hh" - -#include -#include // std::abort -#include -#include -#include -#include - -#if defined __cplusplus -#define YY_CPLUSPLUS __cplusplus -#else -#define YY_CPLUSPLUS 199711L -#endif - -// Support move semantics when possible. -#if 201103L <= YY_CPLUSPLUS -#define YY_MOVE std::move -#define YY_MOVE_OR_COPY move -#define YY_MOVE_REF(Type) Type&& -#define YY_RVREF(Type) Type&& -#define YY_COPY(Type) Type -#else -#define YY_MOVE -#define YY_MOVE_OR_COPY copy -#define YY_MOVE_REF(Type) Type& -#define YY_RVREF(Type) const Type& -#define YY_COPY(Type) const Type& -#endif - -// Support noexcept when possible. -#if 201103L <= YY_CPLUSPLUS -#define YY_NOEXCEPT noexcept -#define YY_NOTHROW -#else -#define YY_NOEXCEPT -#define YY_NOTHROW throw() -#endif - -// Support constexpr when possible. -#if 201703 <= YY_CPLUSPLUS -#define YY_CONSTEXPR constexpr -#else -#define YY_CONSTEXPR -#endif -#include "location.hh" - -#ifndef YY_ATTRIBUTE_PURE -#if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__) -#define YY_ATTRIBUTE_PURE __attribute__((__pure__)) -#else -#define YY_ATTRIBUTE_PURE -#endif -#endif - -#ifndef YY_ATTRIBUTE_UNUSED -#if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__) -#define YY_ATTRIBUTE_UNUSED __attribute__((__unused__)) -#else -#define YY_ATTRIBUTE_UNUSED -#endif -#endif - -/* Suppress unused-variable warnings by "using" E. */ -#if !defined lint || defined __GNUC__ -#define YYUSE(E) ((void)(E)) -#else -#define YYUSE(E) /* empty */ -#endif - -#if defined __GNUC__ && !defined __ICC && 407 <= __GNUC__ * 100 + __GNUC_MINOR__ -/* Suppress an incorrect diagnostic about yylval being uninitialized. */ -#define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \ - _Pragma("GCC diagnostic push") \ - _Pragma("GCC diagnostic ignored \"-Wuninitialized\"") \ - _Pragma("GCC diagnostic ignored \"-Wmaybe-uninitialized\"") -#define YY_IGNORE_MAYBE_UNINITIALIZED_END _Pragma("GCC diagnostic pop") -#else -#define YY_INITIAL_VALUE(Value) Value -#endif -#ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN -#define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN -#define YY_IGNORE_MAYBE_UNINITIALIZED_END -#endif -#ifndef YY_INITIAL_VALUE -#define YY_INITIAL_VALUE(Value) /* Nothing. */ -#endif - -#if defined __cplusplus && defined __GNUC__ && !defined __ICC && 6 <= __GNUC__ -#define YY_IGNORE_USELESS_CAST_BEGIN \ - _Pragma("GCC diagnostic push") \ - _Pragma("GCC diagnostic ignored \"-Wuseless-cast\"") -#define YY_IGNORE_USELESS_CAST_END _Pragma("GCC diagnostic pop") -#endif -#ifndef YY_IGNORE_USELESS_CAST_BEGIN -#define YY_IGNORE_USELESS_CAST_BEGIN -#define YY_IGNORE_USELESS_CAST_END -#endif - -#ifndef YY_CAST -#ifdef __cplusplus -#define YY_CAST(Type, Val) static_cast(Val) -#define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast(Val) -#else -#define YY_CAST(Type, Val) ((Type)(Val)) -#define YY_REINTERPRET_CAST(Type, Val) ((Type)(Val)) -#endif -#endif -#ifndef YY_NULLPTR -#if defined __cplusplus -#if 201103L <= __cplusplus -#define YY_NULLPTR nullptr -#else -#define YY_NULLPTR 0 -#endif -#else -#define YY_NULLPTR ((void*)0) -#endif -#endif - -/* Debug traces. */ -#ifndef LTLFDEBUG -#if defined YYDEBUG -#if YYDEBUG -#define LTLFDEBUG 1 -#else -#define LTLFDEBUG 0 -#endif -#else /* ! defined YYDEBUG */ -#define LTLFDEBUG 1 -#endif /* ! defined YYDEBUG */ -#endif /* ! defined LTLFDEBUG */ - -#line 6 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" -namespace cynthia { -namespace parser { -namespace ltlf { -#line 205 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.hh" - -/// A Bison parser. -class LTLfParser { -public: -#ifndef LTLFSTYPE - /// Symbol semantic values. - typedef struct cynthia::parser::ltlf::LTLf_YYSTYPE semantic_type; -#else - typedef LTLFSTYPE semantic_type; -#endif - /// Symbol locations. - typedef location location_type; - - /// Syntax errors thrown from user actions. - struct syntax_error : std::runtime_error { - syntax_error(const location_type& l, const std::string& m) - : std::runtime_error(m), location(l) {} - - syntax_error(const syntax_error& s) - : std::runtime_error(s.what()), location(s.location) {} - - ~syntax_error() YY_NOEXCEPT YY_NOTHROW; - - location_type location; - }; - - /// Tokens. - struct token { - enum yytokentype { - END_OF_FILE = 0, - LPAR = 258, - RPAR = 259, - TRUE_ = 260, - FALSE_ = 261, - TT = 262, - FF = 263, - END = 264, - LAST = 265, - SYMBOL = 266, - NEWLINE = 267, - EQUIVALENCE = 268, - IMPLICATION = 269, - UNTIL = 270, - RELEASE = 271, - OR = 272, - AND = 273, - EVENTUALLY = 274, - ALWAYS = 275, - NEXT = 276, - WEAK_NEXT = 277, - NOT = 278 - }; - }; - - /// (External) token type, as returned by yylex. - typedef token::yytokentype token_type; - - /// Symbol type: an internal symbol number. - typedef int symbol_number_type; - - /// The symbol type number to denote an empty symbol. - enum { empty_symbol = -2 }; - - /// Internal symbol number for tokens (subsumed by symbol_number_type). - typedef signed char token_number_type; - - /// A complete symbol. - /// - /// Expects its Base type to provide access to the symbol type - /// via type_get (). - /// - /// Provide access to semantic value and location. - template struct basic_symbol : Base { - /// Alias to Base. - typedef Base super_type; - - /// Default constructor. - basic_symbol() : value(), location() {} - -#if 201103L <= YY_CPLUSPLUS - /// Move constructor. - basic_symbol(basic_symbol&& that); -#endif - - /// Copy constructor. - basic_symbol(const basic_symbol& that); - /// Constructor for valueless symbols. - basic_symbol(typename Base::kind_type t, YY_MOVE_REF(location_type) l); - - /// Constructor for symbols with semantic value. - basic_symbol(typename Base::kind_type t, YY_RVREF(semantic_type) v, - YY_RVREF(location_type) l); - - /// Destroy the symbol. - ~basic_symbol() { clear(); } - - /// Destroy contents, and record that is empty. - void clear() { Base::clear(); } - - /// Whether empty. - bool empty() const YY_NOEXCEPT; - - /// Destructive move, \a s is emptied into this. - void move(basic_symbol& s); - - /// The semantic value. - semantic_type value; - - /// The location. - location_type location; - - private: -#if YY_CPLUSPLUS < 201103L - /// Assignment operator. - basic_symbol& operator=(const basic_symbol& that); -#endif - }; - - /// Type access provider for token (enum) based symbols. - struct by_type { - /// Default constructor. - by_type(); - -#if 201103L <= YY_CPLUSPLUS - /// Move constructor. - by_type(by_type&& that); -#endif - - /// Copy constructor. - by_type(const by_type& that); - - /// The symbol type as needed by the constructor. - typedef token_type kind_type; - - /// Constructor from (external) token numbers. - by_type(kind_type t); - - /// Record that this symbol is empty. - void clear(); - - /// Steal the symbol type from \a that. - void move(by_type& that); - - /// The (internal) type number (corresponding to \a type). - /// \a empty when empty. - symbol_number_type type_get() const YY_NOEXCEPT; - - /// The symbol type. - /// \a empty_symbol when empty. - /// An int, not token_number_type, to be able to store empty_symbol. - int type; - }; - - /// "External" symbols: returned by the scanner. - struct symbol_type : basic_symbol {}; - - /// Build a parser object. - LTLfParser(LTLfScanner& scanner_yyarg, LTLfDriver& d_yyarg); - virtual ~LTLfParser(); - - /// Parse. An alias for parse (). - /// \returns 0 iff parsing succeeded. - int operator()(); - - /// Parse. - /// \returns 0 iff parsing succeeded. - virtual int parse(); - -#if LTLFDEBUG - /// The current debugging stream. - std::ostream& debug_stream() const YY_ATTRIBUTE_PURE; - /// Set the current debugging stream. - void set_debug_stream(std::ostream&); - - /// Type for debugging levels. - typedef int debug_level_type; - /// The current debugging level. - debug_level_type debug_level() const YY_ATTRIBUTE_PURE; - /// Set the current debugging level. - void set_debug_level(debug_level_type l); -#endif - - /// Report a syntax error. - /// \param loc where the syntax error is found. - /// \param msg a description of the syntax error. - virtual void error(const location_type& loc, const std::string& msg); - - /// Report a syntax error. - void error(const syntax_error& err); - -private: - /// This class is not copyable. - LTLfParser(const LTLfParser&); - LTLfParser& operator=(const LTLfParser&); - - /// Stored state numbers (used for stacks). - typedef signed char state_type; - - /// Generate an error message. - /// \param yystate the state where the error occurred. - /// \param yyla the lookahead token. - virtual std::string yysyntax_error_(state_type yystate, - const symbol_type& yyla) const; - - /// Compute post-reduction state. - /// \param yystate the current state - /// \param yysym the nonterminal to push on the stack - static state_type yy_lr_goto_state_(state_type yystate, int yysym); - - /// Whether the given \c yypact_ value indicates a defaulted state. - /// \param yyvalue the value to check - static bool yy_pact_value_is_default_(int yyvalue); - - /// Whether the given \c yytable_ value indicates a syntax error. - /// \param yyvalue the value to check - static bool yy_table_value_is_error_(int yyvalue); - - static const signed char yypact_ninf_; - static const signed char yytable_ninf_; - - /// Convert a scanner token number \a t to a symbol number. - /// In theory \a t should be a token_type, but character literals - /// are valid, yet not members of the token_type enum. - static token_number_type yytranslate_(int t); - - // Tables. - // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing - // STATE-NUM. - static const signed char yypact_[]; - - // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM. - // Performed when YYTABLE does not specify something else to do. Zero - // means the default is an error. - static const signed char yydefact_[]; - - // YYPGOTO[NTERM-NUM]. - static const signed char yypgoto_[]; - - // YYDEFGOTO[NTERM-NUM]. - static const signed char yydefgoto_[]; - - // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If - // positive, shift that token. If negative, reduce the rule whose - // number is the opposite. If YYTABLE_NINF, syntax error. - static const signed char yytable_[]; - - static const signed char yycheck_[]; - - // YYSTOS[STATE-NUM] -- The (internal number of the) accessing - // symbol of state STATE-NUM. - static const signed char yystos_[]; - - // YYR1[YYN] -- Symbol number of symbol that rule YYN derives. - static const signed char yyr1_[]; - - // YYR2[YYN] -- Number of symbols on the right hand side of rule YYN. - static const signed char yyr2_[]; - -#if LTLFDEBUG - /// For a symbol, its name in clear. - static const char* const yytname_[]; - - // YYRLINE[YYN] -- Source line where rule number YYN was defined. - static const signed char yyrline_[]; - /// Report on the debug stream that the rule \a r is going to be reduced. - virtual void yy_reduce_print_(int r); - /// Print the state stack on the debug stream. - virtual void yystack_print_(); - - /// Debugging level. - int yydebug_; - /// Debug stream. - std::ostream* yycdebug_; - - /// \brief Display a symbol type, value and location. - /// \param yyo The output stream. - /// \param yysym The symbol. - template - void yy_print_(std::ostream& yyo, const basic_symbol& yysym) const; -#endif - - /// \brief Reclaim the memory associated to a symbol. - /// \param yymsg Why this token is reclaimed. - /// If null, print nothing. - /// \param yysym The symbol. - template - void yy_destroy_(const char* yymsg, basic_symbol& yysym) const; - -private: - /// Type access provider for state based symbols. - struct by_state { - /// Default constructor. - by_state() YY_NOEXCEPT; - - /// The symbol type as needed by the constructor. - typedef state_type kind_type; - - /// Constructor. - by_state(kind_type s) YY_NOEXCEPT; - - /// Copy constructor. - by_state(const by_state& that) YY_NOEXCEPT; - - /// Record that this symbol is empty. - void clear() YY_NOEXCEPT; - - /// Steal the symbol type from \a that. - void move(by_state& that); - - /// The (internal) type number (corresponding to \a state). - /// \a empty_symbol when empty. - symbol_number_type type_get() const YY_NOEXCEPT; - - /// The state number used to denote an empty symbol. - /// We use the initial state, as it does not have a value. - enum { empty_state = 0 }; - - /// The state. - /// \a empty when empty. - state_type state; - }; - - /// "Internal" symbol: element of the stack. - struct stack_symbol_type : basic_symbol { - /// Superclass. - typedef basic_symbol super_type; - /// Construct an empty symbol. - stack_symbol_type(); - /// Move or copy construction. - stack_symbol_type(YY_RVREF(stack_symbol_type) that); - /// Steal the contents from \a sym to build this. - stack_symbol_type(state_type s, YY_MOVE_REF(symbol_type) sym); -#if YY_CPLUSPLUS < 201103L - /// Assignment, needed by push_back by some old implementations. - /// Moves the contents of that. - stack_symbol_type& operator=(stack_symbol_type& that); - - /// Assignment, needed by push_back by other implementations. - /// Needed by some other old implementations. - stack_symbol_type& operator=(const stack_symbol_type& that); -#endif - }; - - /// A stack with random access from its top. - template > class stack { - public: - // Hide our reversed order. - typedef typename S::reverse_iterator iterator; - typedef typename S::const_reverse_iterator const_iterator; - typedef typename S::size_type size_type; - typedef typename std::ptrdiff_t index_type; - - stack(size_type n = 200) : seq_(n) {} - - /// Random access. - /// - /// Index 0 returns the topmost element. - const T& operator[](index_type i) const { - return seq_[size_type(size() - 1 - i)]; - } - - /// Random access. - /// - /// Index 0 returns the topmost element. - T& operator[](index_type i) { return seq_[size_type(size() - 1 - i)]; } - - /// Steal the contents of \a t. - /// - /// Close to move-semantics. - void push(YY_MOVE_REF(T) t) { - seq_.push_back(T()); - operator[](0).move(t); - } - - /// Pop elements from the stack. - void pop(std::ptrdiff_t n = 1) YY_NOEXCEPT { - for (; 0 < n; --n) - seq_.pop_back(); - } - - /// Pop all elements from the stack. - void clear() YY_NOEXCEPT { seq_.clear(); } - - /// Number of elements on the stack. - index_type size() const YY_NOEXCEPT { return index_type(seq_.size()); } - - std::ptrdiff_t ssize() const YY_NOEXCEPT { return std::ptrdiff_t(size()); } - - /// Iterator on top of the stack (going downwards). - const_iterator begin() const YY_NOEXCEPT { return seq_.rbegin(); } - - /// Bottom of the stack. - const_iterator end() const YY_NOEXCEPT { return seq_.rend(); } - - /// Present a slice of the top of a stack. - class slice { - public: - slice(const stack& stack, index_type range) - : stack_(stack), range_(range) {} - - const T& operator[](index_type i) const { return stack_[range_ - i]; } - - private: - const stack& stack_; - index_type range_; - }; - - private: - stack(const stack&); - stack& operator=(const stack&); - /// The wrapped container. - S seq_; - }; - - /// Stack type. - typedef stack stack_type; - - /// The stack. - stack_type yystack_; - - /// Push a new state on the stack. - /// \param m a debug message to display - /// if null, no trace is output. - /// \param sym the symbol - /// \warning the contents of \a s.value is stolen. - void yypush_(const char* m, YY_MOVE_REF(stack_symbol_type) sym); - - /// Push a new look ahead token on the state on the stack. - /// \param m a debug message to display - /// if null, no trace is output. - /// \param s the state - /// \param sym the symbol (for its value and location). - /// \warning the contents of \a sym.value is stolen. - void yypush_(const char* m, state_type s, YY_MOVE_REF(symbol_type) sym); - - /// Pop \a n symbols from the stack. - void yypop_(int n = 1); - - /// Some specific tokens. - static const token_number_type yy_error_token_ = 1; - static const token_number_type yy_undef_token_ = 2; - - /// Constants. - enum { - yyeof_ = 0, - yylast_ = 49, ///< Last index in yytable_. - yynnts_ = 3, ///< Number of nonterminal symbols. - yyfinal_ = 22, ///< Termination state number. - yyntokens_ = 24 ///< Number of tokens. - }; - - // User arguments. - LTLfScanner& scanner; - LTLfDriver& d; -}; - -#line 6 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.yy" -} // namespace ltlf -} // namespace parser -} // namespace cynthia -#line 740 "/home/marcofavorito/workfolder/cynthia/libs/parser/include/cynthia/parser/parser.tab.hh" - -#endif // !YY_LTLF_HOME_MARCOFAVORITO_WORKFOLDER_CYNTHIA_LIBS_PARSER_INCLUDE_CYNTHIA_PARSER_PARSER_TAB_HH_INCLUDED diff --git a/libs/parser/include/cynthia/parser/parser.yy b/libs/parser/include/cynthia/parser/parser.yy index 9a1ab92..3575194 100644 --- a/libs/parser/include/cynthia/parser/parser.yy +++ b/libs/parser/include/cynthia/parser/parser.yy @@ -13,7 +13,7 @@ %define api.parser.class {LTLfParser} %code requires{ - //#include "cynthia/logic/base.hpp" + #include "cynthia/logic/base.hpp" #include "cynthia/parser/parser_stype.h" namespace cynthia::parser::ltlf { class LTLfDriver; @@ -66,12 +66,13 @@ namespace cynthia::parser::ltlf { %token NEWLINE %token END_OF_FILE 0 -%left EQUIVALENCE +%right EQUIVALENCE %right IMPLICATION -%left UNTIL -%left RELEASE +%right XOR %left OR %left AND +%left UNTIL +%left RELEASE %right EVENTUALLY %right ALWAYS %right NEXT @@ -85,27 +86,28 @@ namespace cynthia::parser::ltlf { %% -input: ltlf_formula { $$ = $1; }; - //d.result = $$; }; - -ltlf_formula: ltlf_formula EQUIVALENCE ltlf_formula { } - | ltlf_formula IMPLICATION ltlf_formula { } - | ltlf_formula RELEASE ltlf_formula { } - | ltlf_formula UNTIL ltlf_formula { } - | ltlf_formula OR ltlf_formula { } - | ltlf_formula AND ltlf_formula { } - | ALWAYS ltlf_formula { } - | EVENTUALLY ltlf_formula { } - | WEAK_NEXT ltlf_formula { } - | NEXT ltlf_formula { } - | NOT ltlf_formula { } - | TT { } - | FF { } - | END { } - | LAST { } - | FALSE_ { } - | TRUE_ { } - | SYMBOL { } +input: ltlf_formula { $$ = $1; + d.result = $$; }; + +ltlf_formula: ltlf_formula EQUIVALENCE ltlf_formula { $$ = d.add_LTLfEquivalent($1, $3); } + | ltlf_formula IMPLICATION ltlf_formula { $$ = d.add_LTLfImplies($1, $3); } + | ltlf_formula XOR ltlf_formula { $$ = d.add_LTLfXor($1, $3); } + | ltlf_formula OR ltlf_formula { $$ = d.add_LTLfOr($1, $3); } + | ltlf_formula AND ltlf_formula { $$ = d.add_LTLfAnd($1, $3); } + | ltlf_formula RELEASE ltlf_formula { $$ = d.add_LTLfRelease($1, $3); } + | ltlf_formula UNTIL ltlf_formula { $$ = d.add_LTLfUntil($1, $3); } + | ALWAYS ltlf_formula { $$ = d.add_LTLfAlways($2); } + | EVENTUALLY ltlf_formula { $$ = d.add_LTLfEventually($2); } + | WEAK_NEXT ltlf_formula { $$ = d.add_LTLfWeakNext($2); } + | NEXT ltlf_formula { $$ = d.add_LTLfNext($2); } + | NOT ltlf_formula { $$ = d.add_LTLfNot($2); } + | TT { $$ = d.add_LTLfTrue(); } + | FF { $$ = d.add_LTLfFalse(); } + | END { $$ = d.add_LTLfEnd(); } + | LAST { $$ = d.add_LTLfLast(); } + | FALSE_ { $$ = d.add_LTLfPropFalse(); } + | TRUE_ { $$ = d.add_LTLfPropTrue(); } + | SYMBOL { $$ = d.add_LTLfAtom($1); } ; ltlf_formula: LPAR ltlf_formula RPAR { $$ = $2; }; diff --git a/libs/parser/include/cynthia/parser/parser_stype.h b/libs/parser/include/cynthia/parser/parser_stype.h index de185e8..994fc67 100644 --- a/libs/parser/include/cynthia/parser/parser_stype.h +++ b/libs/parser/include/cynthia/parser/parser_stype.h @@ -23,8 +23,7 @@ namespace parser { namespace ltlf { struct LTLf_YYSTYPE { - // ldlf_ptr formula; - void* formula; + logic::ltlf_ptr formula; std::string symbol_name; // Constructor diff --git a/libs/parser/include/cynthia/parser/position.hh b/libs/parser/include/cynthia/parser/position.hh deleted file mode 100644 index bf34c1c..0000000 --- a/libs/parser/include/cynthia/parser/position.hh +++ /dev/null @@ -1,11 +0,0 @@ -// A Bison parser, made by GNU Bison 3.5.1. - -// Starting with Bison 3.2, this file is useless: the structure it -// used to define is now defined in "location.hh". -// -// To get rid of this file: -// 1. add '%require "3.2"' (or newer) to your grammar file -// 2. remove references to this file from your build system -// 3. if you used to include it, include "location.hh" instead. - -#include "location.hh" diff --git a/libs/parser/include/cynthia/parser/stack.hh b/libs/parser/include/cynthia/parser/stack.hh deleted file mode 100644 index c15d84c..0000000 --- a/libs/parser/include/cynthia/parser/stack.hh +++ /dev/null @@ -1,8 +0,0 @@ -// A Bison parser, made by GNU Bison 3.5.1. - -// Starting with Bison 3.2, this file is useless: the structure it -// used to define is now defined with the parser itself. -// -// To get rid of this file: -// 1. add '%require "3.2"' (or newer) to your grammar file -// 2. remove references to this file from your build system. diff --git a/libs/parser/src/driver.cpp b/libs/parser/src/driver.cpp index 013f85e..7531ca2 100644 --- a/libs/parser/src/driver.cpp +++ b/libs/parser/src/driver.cpp @@ -18,6 +18,7 @@ #include #include +#include #include namespace cynthia { @@ -71,127 +72,96 @@ void LTLfDriver::parse_helper(std::istream& stream) { } } -// ldlf_ptr LTLfDriver::add_LTLfTrue() const { -// auto prop_true = context->makePropRegex(context->makeTrue()); -// auto logical_true = context->makeLdlfTrue(); -// return context->makeLdlfDiamond(prop_true, logical_true); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfFalse() const { -// auto prop_true = context->makePropRegex(context->makeFalse()); -// auto logical_true = context->makeLdlfTrue(); -// return context->makeLdlfDiamond(prop_true, logical_true); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfAtom(std::string s) const { -// auto prop_atom = context->makePropRegex(context->makePropAtom(s)); -// auto logical_true = context->makeLdlfTrue(); -// return context->makeLdlfDiamond(prop_atom, logical_true); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfAnd(ldlf_ptr& lhs, ldlf_ptr& rhs) const { -// auto children = set_formulas({lhs, rhs}); -// return context->makeLdlfAnd(children); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfOr(ldlf_ptr& lhs, ldlf_ptr& rhs) const { -// auto children = set_formulas({lhs, rhs}); -// return context->makeLdlfOr(children); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfNot(ldlf_ptr& formula) const { -// return context->makeLdlfNot(formula); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfNext(ldlf_ptr& formula) const { -// auto not_end = context->makeLdlfNot(context->makeLdlfEnd()); -// auto formula_and_not_end = context->makeLdlfAnd({formula, not_end}); -// return context->makeLdlfDiamond(context->makePropRegex(context->makeTrue()), -// formula_and_not_end); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfWeakNext(ldlf_ptr& formula) const { -// auto end = context->makeLdlfEnd(); -// auto formula_or_end = context->makeLdlfOr({formula, end}); -// return context->makeLdlfBox(context->makePropRegex(context->makeTrue()), -// formula_or_end); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfEventually(ldlf_ptr& formula) const { -// auto not_end = context->makeLdlfNot(context->makeLdlfEnd()); -// auto formula_and_not_end = context->makeLdlfAnd({formula, not_end}); -// auto true_star = -// context->makeStarRegex(context->makePropRegex(context->makeTrue())); -// return context->makeLdlfDiamond(true_star, formula_and_not_end); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfAlways(ldlf_ptr& formula) const { -// auto end = context->makeLdlfEnd(); -// auto formula_or_end = context->makeLdlfOr({formula, end}); -// auto true_star = -// context->makeStarRegex(context->makePropRegex(context->makeTrue())); -// return context->makeLdlfBox(true_star, formula_or_end); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfUntil(ldlf_ptr& lhs, ldlf_ptr& rhs) const { -// auto not_end = context->makeLdlfNot(context->makeLdlfEnd()); -// auto formula_and_not_end = context->makeLdlfAnd({rhs, not_end}); -// auto true_regex = context->makePropRegex(context->makeTrue()); -// auto formula_test = context->makeTestRegex(lhs); -// auto seq_star = -// context->makeStarRegex(context->makeSeqRegex({formula_test, -// true_regex})); -// return context->makeLdlfDiamond(seq_star, formula_and_not_end); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfRelease(ldlf_ptr& lhs, ldlf_ptr& rhs) const { -// auto end = context->makeLdlfEnd(); -// auto formula_or_end = context->makeLdlfOr({rhs, end}); -// auto true_regex = context->makePropRegex(context->makeTrue()); -// auto formula_test = context->makeTestRegex(lhs); -// auto seq_star = -// context->makeStarRegex(context->makeSeqRegex({formula_test, -// true_regex})); -// return context->makeLdlfBox(seq_star, formula_or_end); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfImplication(ldlf_ptr& lhs, ldlf_ptr& rhs) const -// { -// auto ptr_not_lhs = context->makeLdlfNot(lhs); -// auto children = set_formulas({ptr_not_lhs, rhs}); -// return context->makeLdlfOr(children); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfEquivalence(ldlf_ptr& lhs, ldlf_ptr& rhs) const -// { -// auto ptr_left_implication = this->add_LTLfImplication(lhs, rhs); -// auto ptr_right_implication = this->add_LTLfImplication(rhs, lhs); -// auto children = set_formulas({ptr_left_implication, ptr_right_implication}); -// return context->makeLdlfAnd(children); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfLast() const { -// return context->makeLdlfDiamond(context->makePropRegex(context->makeTrue()), -// context->makeLdlfEnd()); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfEnd() const { return context->makeLdlfEnd(); } -// -// ldlf_ptr LTLfDriver::add_LTLfPropTrue() const { -// return context->makeLdlfDiamond(context->makePropRegex(context->makeTrue()), -// context->makeLdlfTrue()); -//} -// -// ldlf_ptr LTLfDriver::add_LTLfPropFalse() const { -// return -// context->makeLdlfDiamond(context->makePropRegex(context->makeFalse()), -// context->makeLdlfTrue()); -//} +logic::ltlf_ptr LTLfDriver::add_LTLfTrue() const { return context->make_tt(); } + +logic::ltlf_ptr LTLfDriver::add_LTLfFalse() const { return context->make_ff(); } +logic::ltlf_ptr LTLfDriver::add_LTLfPropTrue() const { + return context->make_prop_true(); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfPropFalse() const { + return context->make_prop_false(); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfEnd() const { + return context->make_always(context->make_ff()); +} +logic::ltlf_ptr LTLfDriver::add_LTLfLast() const { + return context->make_weak_next(context->make_ff()); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfAtom(const std::string& name) const { + return context->make_atom(name); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfNot(const logic::ltlf_ptr& formula) const { + if (logic::is_a(*formula) || + logic::is_a(*formula)) { + return context->make_prop_not(formula); + } + return context->make_not(formula); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfAnd(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const { + return context->make_and(logic::vec_ptr{lhs, rhs}); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfOr(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const { + return context->make_or(logic::vec_ptr{lhs, rhs}); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfImplies(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const { + return context->make_implies(logic::vec_ptr{lhs, rhs}); +} + +logic::ltlf_ptr +LTLfDriver::add_LTLfEquivalent(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const { + return context->make_equivalent(logic::vec_ptr{lhs, rhs}); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfXor(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const { + return context->make_xor(logic::vec_ptr{lhs, rhs}); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfNext(const logic::ltlf_ptr& formula) const { + return context->make_next(formula); +} + +logic::ltlf_ptr +LTLfDriver::add_LTLfWeakNext(const logic::ltlf_ptr& formula) const { + return context->make_weak_next(formula); +} // -// std::ostream& LTLfDriver::print(std::ostream& stream) const { -// stream << this->result->str() << "\n"; -// return (stream); -//} +logic::ltlf_ptr +LTLfDriver::add_LTLfEventually(const logic::ltlf_ptr& formula) const { + return context->make_eventually(formula); +} + +logic::ltlf_ptr +LTLfDriver::add_LTLfAlways(const logic::ltlf_ptr& formula) const { + return context->make_always(formula); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfUntil(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const { + return context->make_until(logic::vec_ptr{lhs, rhs}); +} + +logic::ltlf_ptr LTLfDriver::add_LTLfRelease(const logic::ltlf_ptr& lhs, + const logic::ltlf_ptr& rhs) const { + return context->make_release(logic::vec_ptr{lhs, rhs}); +} + +std::ostream& LTLfDriver::print(std::ostream& stream) const { + // stream << this->result->str() << "\n"; + // TODO + return (stream); +} } // namespace ltlf } // namespace parser diff --git a/libs/parser/tests/unit/main.cpp b/libs/parser/tests/unit/main.cpp index 674d931..0d6d0e1 100644 --- a/libs/parser/tests/unit/main.cpp +++ b/libs/parser/tests/unit/main.cpp @@ -18,11 +18,213 @@ #define CATCH_CONFIG_MAIN // This tells Catch to provide a main() - only do this // in one cpp file #include +#include +#include namespace cynthia { namespace parser { namespace Test { -TEST_CASE("Example", "[example]") {} +TEST_CASE("Parsing tt", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto expected_formula = context->make_tt(); + std::istringstream fstring("tt"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing ff", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto expected_formula = context->make_ff(); + std::istringstream fstring("ff"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing true", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto expected_formula = context->make_prop_true(); + std::istringstream fstring("true"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing false", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto expected_formula = context->make_prop_false(); + std::istringstream fstring("false"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing atom", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto expected_formula = context->make_atom("a"); + std::istringstream fstring("a"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing not", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto atom = context->make_atom("a"); + auto next = context->make_next(atom); + auto actual_formula = context->make_not(next); + std::istringstream fstring("!X[!] a"); + driver.parse(fstring); + auto expected_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing propositional not", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + + SECTION("parse !a") { + auto atom = context->make_atom("a"); + auto expected_formula = context->make_prop_not(atom); + std::istringstream fstring("!a"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); + } + + SECTION("parse !!a = a") { + auto expected_formula = context->make_atom("a"); + std::istringstream fstring("!!a"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); + } +} +TEST_CASE("Parsing and", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto atom_1 = context->make_atom("a"); + auto atom_2 = context->make_atom("b"); + auto expected_formula = context->make_and(logic::vec_ptr{atom_1, atom_2}); + std::istringstream fstring("a & b"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing or", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto atom_1 = context->make_atom("a"); + auto atom_2 = context->make_atom("b"); + auto expected_formula = context->make_or(logic::vec_ptr{atom_1, atom_2}); + std::istringstream fstring("a | b"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing implies", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto atom_1 = context->make_atom("a"); + auto atom_2 = context->make_atom("b"); + auto atom_3 = context->make_atom("c"); + // right-associative + auto expected_formula = context->make_implies(logic::vec_ptr{ + atom_1, context->make_implies(logic::vec_ptr{atom_2, atom_3})}); + std::istringstream fstring("a -> b -> c"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing equivalent", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto atom_1 = context->make_atom("a"); + auto atom_2 = context->make_atom("b"); + auto atom_3 = context->make_atom("c"); + auto expected_formula = context->make_equivalent(logic::vec_ptr{ + atom_1, context->make_equivalent(logic::vec_ptr{atom_2, atom_3})}); + std::istringstream fstring("a <-> b <-> c"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing xor", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto atom_1 = context->make_atom("a"); + auto atom_2 = context->make_atom("b"); + auto atom_3 = context->make_atom("c"); + auto expected_formula = context->make_xor(logic::vec_ptr{ + atom_1, context->make_xor(logic::vec_ptr{atom_2, atom_3})}); + std::istringstream fstring("a ^ b ^ c"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing next", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto atom_1 = context->make_atom("a"); + auto expected_formula = context->make_next(atom_1); + std::istringstream fstring("X[!]a"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing weak next", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto atom_1 = context->make_atom("a"); + auto expected_formula = context->make_weak_next(atom_1); + std::istringstream fstring("X a"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing until", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto a = context->make_atom("a"); + auto b = context->make_atom("b"); + auto expected_formula = context->make_until(logic::vec_ptr{a, b}); + std::istringstream fstring("a U b"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing release", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto a = context->make_atom("a"); + auto b = context->make_atom("b"); + auto expected_formula = context->make_release(logic::vec_ptr{a, b}); + std::istringstream fstring("a R b"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing eventually", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto a = context->make_atom("a"); + auto expected_formula = context->make_eventually(a); + std::istringstream fstring("F a"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} +TEST_CASE("Parsing always", "[parser][ltlf]") { + auto context = std::make_shared(); + auto driver = ltlf::LTLfDriver(context); + auto a = context->make_atom("a"); + auto expected_formula = context->make_always(a); + std::istringstream fstring("G a"); + driver.parse(fstring); + auto actual_formula = driver.result; + REQUIRE(expected_formula == actual_formula); +} } // namespace Test } // namespace parser } // namespace cynthia \ No newline at end of file diff --git a/libs/utils/include/cynthia/utils.hpp b/libs/utils/include/cynthia/utils.hpp index c89e5a7..2ca5974 100644 --- a/libs/utils/include/cynthia/utils.hpp +++ b/libs/utils/include/cynthia/utils.hpp @@ -16,11 +16,33 @@ * along with Cynthia. If not, see . */ +#include #include +#include namespace cynthia { namespace utils { +/* + * Dereferenced versions of hashing and comparison. + */ +struct Deref { + struct Hash { + template + std::size_t operator()(std::shared_ptr const& p) const { + return std::hash()(*p); + } + }; + + struct Compare { + template + size_t operator()(std::shared_ptr const& a, + std::shared_ptr const& b) const { + return *a == *b; + } + }; +}; + /* * make_unique function, like the one in the standards >C++14. * In C++11, that is not included. @@ -29,5 +51,56 @@ template std::unique_ptr make_unique(Args&&... args) { return std::unique_ptr(new T(std::forward(args)...)); } + +/* + * Insert an element in a sorted vector. + */ +template +typename std::vector::iterator insert_sorted(std::vector& vec, + T const& item) { + return vec.insert(std::upper_bound(vec.begin(), vec.end(), item), item); +} + +/* + * Insert an element in a sorted vector by a specific predicate. + */ +template +typename std::vector::iterator insert_sorted(std::vector& vec, + T const& item, Pred pred) { + return vec.insert(std::upper_bound(vec.begin(), vec.end(), item, pred), item); +} + +template typename std::vector setify(std::vector vec) { + if (!std::is_sorted(vec.begin(), vec.end())) { + std::sort(vec.begin(), vec.end()); + } + auto last = std::unique(vec.begin(), vec.end()); + vec.erase(last, vec.end()); + return vec; +} +template typename std::vector sort(std::vector vec) { + if (!std::is_sorted(vec.begin(), vec.end())) { + std::sort(vec.begin(), vec.end()); + } + return vec; +} + +template inline int ordered_compare(const T& A, const T& B) { + // Can't be equal if # of entries differ: + if (A.size() != B.size()) + return A.size() < B.size() ? -1 : 1; + + // Loop over elements in "a" and "b": + auto a = A.begin(); + auto b = B.begin(); + for (; a != A.end(); ++a, ++b) { + auto eq = *a == *b; + if (!eq) { + return *a < *b ? -1 : 1; + } + } + return 0; +} + } // namespace utils } // namespace cynthia \ No newline at end of file diff --git a/libs/utils/tests/unit/main.cpp b/libs/utils/tests/unit/main.cpp index cc1ce01..40acdb2 100644 --- a/libs/utils/tests/unit/main.cpp +++ b/libs/utils/tests/unit/main.cpp @@ -24,10 +24,26 @@ namespace cynthia { namespace utils { namespace Test { -TEST_CASE("Make unique", "[example]") { +TEST_CASE("Make unique", "[utils]") { auto a1 = make_unique(1); REQUIRE(*a1.get()); } + +TEST_CASE("insert_sorted", "[utils]") { + auto v = std::vector{0, 1, 3}; + insert_sorted(v, 2); + REQUIRE(v.size() == 4); + REQUIRE(v.at(2) == 2); +} + +TEST_CASE("setify vector", "[utils]") { + std::vector v{1, 2, 1, 1, 3, 3, 3, 4, 5, 4}; + + std::vector expected{1, 2, 3, 4, 5}; + auto actual = setify(v); + REQUIRE(actual == expected); +} + } // namespace Test } // namespace utils } // namespace cynthia \ No newline at end of file