From d0174fcf02417cb495259190d85c54fd7ba901b1 Mon Sep 17 00:00:00 2001
From: Christoph Schwering <c.schwering@unsw.edu.au>
Date: Sun, 6 Aug 2017 07:03:55 +1000
Subject: [PATCH] Renamed kb.h to knowledge_base.h.

---
 CMakeLists.txt                       |  2 +-
 src/limbo/format/pdl/context.h       |  2 +-
 src/limbo/formula.h                  | 15 ++++++++++-----
 src/limbo/{kb.h => knowledge_base.h} |  6 +++---
 src/limbo/term.h                     |  6 +++---
 tests/CMakeLists.txt                 |  2 +-
 tests/{kb.cc => knowledge_base.cc}   |  2 +-
 7 files changed, 20 insertions(+), 15 deletions(-)
 rename src/limbo/{kb.h => knowledge_base.h} (99%)
 rename tests/{kb.cc => knowledge_base.cc} (99%)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index debd67f..95f0c5e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -4,7 +4,7 @@ project (limbo)
 include (CTest)
 
 set (CMAKE_BUILD_TYPE Release)
-set (CMAKE_BUILD_TYPE Debug)
+#set (CMAKE_BUILD_TYPE Debug)
 
 set (CMAKE_VERBOSE_MAKEFILE ON)
 
diff --git a/src/limbo/format/pdl/context.h b/src/limbo/format/pdl/context.h
index 6751a25..a172419 100644
--- a/src/limbo/format/pdl/context.h
+++ b/src/limbo/format/pdl/context.h
@@ -21,7 +21,7 @@
 
 #include <limbo/term.h>
 #include <limbo/formula.h>
-#include <limbo/kb.h>
+#include <limbo/knowledge_base.h>
 
 #include <limbo/format/output.h>
 
diff --git a/src/limbo/formula.h b/src/limbo/formula.h
index b96d735..14a37ba 100644
--- a/src/limbo/formula.h
+++ b/src/limbo/formula.h
@@ -2,12 +2,17 @@
 // Copyright 2014-2017 Christoph Schwering
 // Licensed under the MIT license. See LICENSE file in the project root.
 //
-// Basic first-order formulas without any syntactic sugar. The atomic entities
-// here are clauses, and the connectives are negation, disjunction, and
-// existential quantifier.
+// Basic first-order formulas. The atomic entities here are clauses, and the
+// connectives are negation, disjunction, existential, as well as modalities
+// for knowledge, contingency, conditional belief, consistency guarantee.
 //
-// NF() rectifies a formula (that is, renames variables to make sure no variable
-// occurs freely and bound or bound by two different quantifiers).
+// Some rewriting procedures are bundled in NF():
+// - Rectify() makes assigns a unique variable to every quantifier.
+// - Normalize() aims to turn disjunctions into clauses, removes redundant
+//   quantifiers and double negations, and redistributes knowledge and
+//   contingency operators over quantifiers.
+// - Flatten() pulls nested terms and terms on the right-hand side of literals
+//   out by generating a new clause.
 
 #ifndef LIMBO_FORMULA_H_
 #define LIMBO_FORMULA_H_
diff --git a/src/limbo/kb.h b/src/limbo/knowledge_base.h
similarity index 99%
rename from src/limbo/kb.h
rename to src/limbo/knowledge_base.h
index 6510377..be5a582 100644
--- a/src/limbo/kb.h
+++ b/src/limbo/knowledge_base.h
@@ -23,8 +23,8 @@
 // Queries are not subject to any syntactic restrictions. Technically, they are
 // evaluated using variants of Levesque's representation theorem.
 
-#ifndef LIMBO_KB_H_
-#define LIMBO_KB_H_
+#ifndef LIMBO_KNOWLEDGE_BASE_H_
+#define LIMBO_KNOWLEDGE_BASE_H_
 
 #include <cassert>
 
@@ -370,5 +370,5 @@ class KnowledgeBase {
 
 }  // namespace limbo
 
-#endif  // LIMBO_KB_H_
+#endif  // LIMBO_KNOWLEDGE_BASE_H_
 
diff --git a/src/limbo/term.h b/src/limbo/term.h
index 83fce43..07eb75b 100644
--- a/src/limbo/term.h
+++ b/src/limbo/term.h
@@ -69,6 +69,8 @@ class Symbol {
     bool operator==(const Sort s) const { return id_ == s.id_; }
     bool operator!=(const Sort s) const { return id_ != s.id_; }
 
+    internal::hash32_t hash() const { return internal::jenkins_hash(id_); }
+
     Id id() const { return id_; }
 
    private:
@@ -440,9 +442,7 @@ namespace std {
 
 template<>
 struct hash<limbo::Symbol::Sort> {
-  limbo::internal::hash32_t operator()(const limbo::Symbol::Sort s) const { return h(s.id()); }
- private:
-  std::hash<limbo::Symbol::Sort::Id> h;
+  limbo::internal::hash32_t operator()(const limbo::Symbol::Sort s) const { return s.hash(); }
 };
 
 template<>
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index cf5ad01..2000bea 100644
--- a/tests/CMakeLists.txt
+++ b/tests/CMakeLists.txt
@@ -2,7 +2,7 @@ add_subdirectory (googletest)
 enable_testing ()
 include_directories (${gtest_SOURCE_DIR}/include ${gtest_SOURCE_DIR})
 
-foreach (test hash iter intmap term bloom literal clause setup formula syntax grounder solver kb)
+foreach (test hash iter intmap term bloom literal clause setup formula syntax grounder solver knowledge_base)
     add_executable (${test} ${test}.cc)
     target_link_libraries (${test} LINK_PUBLIC limbo gtest gtest_main)
     add_test (NAME ${test} COMMAND ${test})
diff --git a/tests/kb.cc b/tests/knowledge_base.cc
similarity index 99%
rename from tests/kb.cc
rename to tests/knowledge_base.cc
index cc52b8b..8ee7fe8 100644
--- a/tests/kb.cc
+++ b/tests/knowledge_base.cc
@@ -3,7 +3,7 @@
 
 #include <gtest/gtest.h>
 
-#include <limbo/kb.h>
+#include <limbo/knowledge_base.h>
 #include <limbo/format/output.h>
 #include <limbo/format/cpp/syntax.h>
 
-- 
GitLab