Add LTLf syntax support.

.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

libs/logic/include/cynthia/logic/base.hpp

@@ -29,29 +29,54 @@ namespace cynthia {
 namespace logic {
 
 class Context;
-typedef std::shared_ptr<Context> 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<const AstNode> ast_ptr;
-
 class Context {
 private:
   std::unique_ptr<HashTable> 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

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,

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<hash_t>(seed, static_cast<hash_t>(c));
   }
 }

libs/logic/include/cynthia/logic/hashtable.hpp

@@ -17,38 +17,25 @@
  */
 
 #include <cynthia/logic/types.hpp>
+#include <cynthia/utils.hpp>
 #include <memory>
 #include <unordered_set>
 
 namespace cynthia {
 namespace logic {
-struct Deref {
-  struct Hash {
-    template <typename T>
-    std::size_t operator()(std::shared_ptr<const T> const& p) const {
-      return std::hash<T>()(*p);
-    }
-  };
-
-  struct Compare {
-    template <typename T>
-    size_t operator()(std::shared_ptr<const T> const& a,
-                      std::shared_ptr<const T> const& b) const {
-      return *a == *b;
-    }
-  };
-};
 
 /*
  * A hash table for AST nodes based on STL unordered_set.
  */
 class HashTable {
 private:
-  std::unordered_set<ast_ptr, Deref::Hash, Deref::Compare> m_table_;
+  std::unordered_set<ast_ptr, utils::Deref::Hash, utils::Deref::Compare>
+      m_table_;
 
 public:
   explicit HashTable() {
-    m_table_ = std::unordered_set<ast_ptr, Deref::Hash, Deref::Compare>{};
+    m_table_ = std::unordered_set<ast_ptr, utils::Deref::Hash,
+                                  utils::Deref::Compare>{};
   }
 
   template <typename T>