diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c2d4a2e7ddac324bee0e1c70f56379e1db201899..cb83c6d68fc2860665b0043da1f5d43c8c05941a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -2,13 +2,20 @@
 SET(sources imagine-planner.cpp types.cpp)
 # application header files
 SET(headers imagine-planner.h types.h)
+# Boost
 FIND_PACKAGE(Boost COMPONENTS system filesystem unit_test_framework REQUIRED)
+# Swi-pl
+include(FindPkgConfig)
+pkg_check_modules(SWIPL REQUIRED swipl)
 # locate the necessary dependencies
 # add the necessary include directories
-INCLUDE_DIRECTORIES(. ${Boost_INCLUDE_DIR})
+INCLUDE_DIRECTORIES(. ${Boost_INCLUDE_DIR} ${SWIPL_INCLUDE_DIRS})
+LINK_DIRECTORIES(${SWIPL_LIBRARY_DIRS})
 # create the shared library
 ADD_LIBRARY(imagine-planner SHARED ${sources})
 # link necessary libraries
+TARGET_LINK_LIBRARIES(imagine-planner ${SWIPL_LIBRARIES})
+
 INSTALL(TARGETS imagine-planner
         RUNTIME DESTINATION bin
         LIBRARY DESTINATION lib/iridrivers
diff --git a/src/examples/CMakeLists.txt b/src/examples/CMakeLists.txt
index d08b3af03a73b8a9cc33f48f363d0b7536bca6a9..aed90f64b128b57131728ed8ee67b73211bae976 100644
--- a/src/examples/CMakeLists.txt
+++ b/src/examples/CMakeLists.txt
@@ -10,3 +10,10 @@ TARGET_LINK_LIBRARIES(types_test
                       ${Boost_SYSTEM_LIBRARY}
                       ${Boost_UNIT_TEST_FRAMEWORK_LIBRARY})
 
+ADD_EXECUTABLE(query_test query_test.cpp)
+TARGET_LINK_LIBRARIES(query_test
+                      imagine-planner
+                      ${Boost_FILESYSTEM_LIBRARY}
+                      ${Boost_SYSTEM_LIBRARY}
+                      ${Boost_UNIT_TEST_FRAMEWORK_LIBRARY})
+
diff --git a/src/examples/query_test.cpp b/src/examples/query_test.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..1de2d48244d8106681206d118f12b692e57c59fd
--- /dev/null
+++ b/src/examples/query_test.cpp
@@ -0,0 +1,46 @@
+#include "types.h"
+#include <iostream>
+using namespace imagine_planner;
+
+#if 0 // Set to 1 if __PRETTY_FUNCTION__ macro is not available
+#define __PRETTY_FUNCTION__ __func__
+#endif
+
+#if 1
+#define INFO(x)\
+  std::cout << "\e[1m\e[32m\e[4m" <<  __PRETTY_FUNCTION__ << " [" << __LINE__ << "]" << "\e[24m: " << x << "\e[0m" << std::endl;
+#else
+#define INFO(x)
+#endif
+
+void test()
+{
+  PlanState state{Predicate("at", "lettuce", "east"),
+                  Predicate("at", "wolf", "east"),
+                  Predicate("at", "bunny", "east"),
+                  Predicate("at", "boat", "east"),
+                  Predicate("side", "east"),
+                  Predicate("side", "west"),
+                  Predicate("forbidden", "wolf", "bunny"),
+                  Predicate("forbidden", "lettuce", "bunny")};
+  PlCall("assertz((load_pre(Side,What):-at(boat,Side),at(What,Side),What\\==boat,side(Side),\\+loaded(_)))");
+  StateQuery query(state, create_term_v("Side", "What"), "load_pre");
+  //while (query.next_solution())
+  //{
+    //INFO("Side=" << query.get_values()[0] << ", What=" << query.get_values()[1]);
+  //}
+}
+
+int main(int argc, char* argv[])
+{
+  PlEngine pl(argc, argv);
+  //PlTermv av(1);
+  //PlQuery q("current_module", av);
+  //while (q.next_solution())
+  //{
+    //std::cout << (char*)av[0] << std::endl;
+  //}
+  test();
+
+
+}
diff --git a/src/examples/types_test.cpp b/src/examples/types_test.cpp
index 39642ce89491ed90aebe5bc09bbb5a7df7d10d42..1bcd862a309974d36454d63f6fd18973f6e05eab 100644
--- a/src/examples/types_test.cpp
+++ b/src/examples/types_test.cpp
@@ -8,6 +8,10 @@
 #include <unordered_set>
 using namespace imagine_planner;
 
+#if 0 // Set to 1 if __PRETTY_FUNCTION__ macro is not available
+#define __PRETTY_FUNCTION__ __func__
+#endif
+
 #if 1
 #define INFO(x)\
   std::cout << "\e[1m\e[32m\e[4m" <<  __PRETTY_FUNCTION__ << " [" << __LINE__ << "]" << "\e[24m: " << x << "\e[0m" << std::endl;
@@ -27,12 +31,6 @@ using namespace imagine_planner;
   os << '}';\
   return os;
 
-AtomFactory A;
-NumberFactory N;
-VariableFactory V;
-TermVFactory L;
-PredicateFactory P;
-
 const char* b2s(bool b)
 {
   return b? "true" : "false";
@@ -43,218 +41,172 @@ std::ostream& operator<<(std::ostream& os, const std::set<Predicate>& ctn)
   CONTAINER_TO_STREAM(ctn, os);
 }
 
-std::ostream& operator<<(std::ostream& os, const std::unordered_set<Predicate, std::hash<Term>>& ctn)
+std::ostream& operator<<(std::ostream& os, const std::unordered_set<Predicate,
+    std::hash<Hashable>>& ctn)
 {
   CONTAINER_TO_STREAM(ctn, os);
 }
 
-BOOST_AUTO_TEST_CASE(atom_test)
+BOOST_AUTO_TEST_CASE(literal_test)
 {
-  auto atom1 = A("atom1");
-  auto atom1_ = A("atom1");
-  auto atom2 = A("atom2");
-  INFO("atom1=" << *atom1);
-  INFO("atom1_=" << *atom1_);
-  INFO("atom2=" << *atom2);
-  // Check name method
-  BOOST_CHECK_EQUAL(atom1->name(), "atom1");
-  // Check == operator
-  BOOST_CHECK_EQUAL(*atom1, *atom1_);
-  BOOST_CHECK_NE(*atom1, *atom2);
-  // Check < operator
-  BOOST_CHECK_LT(*atom1, *atom2);
-  BOOST_CHECK(not(*atom2 < *atom1));
-  // Check hash correctness
-  BOOST_CHECK_EQUAL(atom1->hash(), atom1_->hash());
-  BOOST_CHECK_NE(atom1->hash(), atom2->hash());
+  TermWrapper l1("atom1");
+  TermWrapper l1_("atom1");
+  TermWrapper l2("atom2");
+  TermWrapper l3("Var1");
+  TermWrapper l4("_");
+  INFO("l1=" << l1);
+  INFO("l1_=" << l1_);
+  INFO("l2=" << l2);
+  INFO("l3=" << l3);
+  BOOST_CHECK_EQUAL(l1, l1_);
+  BOOST_CHECK_LE(l1, l1_);
+  BOOST_CHECK_NE(l1, l2);
+  BOOST_CHECK_LT(l1, l2);
+  BOOST_CHECK_LE(l1, l2);
+  BOOST_CHECK_GT(l2, l1);
+  BOOST_CHECK_GE(l2, l1);
+  BOOST_CHECK(l1.is_ground());
+  BOOST_CHECK(l2.is_ground());
+  BOOST_CHECK(not l3.is_ground());
+  BOOST_CHECK(not l4.is_ground());
+  BOOST_CHECK_EQUAL(l1.hash(), l1_.hash());
+  BOOST_WARN_NE(l1.hash(), l2.hash()); // Very likely the hashes are different
 }
 
 BOOST_AUTO_TEST_CASE(number_test)
 {
-  auto number1 = N(0.5);
-  auto number1_ = N(0.5+2e-10);
-  auto number1__ = N(0.5+5e-9);
-  auto number2 = N(1);
-  auto number2_ = N(1+2e-10);
-  auto number2__ = N(1+5e-9);
-  INFO("number1=" << *number1);
-  INFO("number1_=" << *number1_);
-  INFO("number1__=" << *number1__);
-  INFO("number2=" << *number2);
-  INFO("number2_=" << *number2_);
-  INFO("number2__=" << *number2__);
+  TermWrapper n1(0.5);
+  TermWrapper n1_(0.5+2e-10);
+  TermWrapper n1__(0.5+5e-9);
+  TermWrapper n2(1);
+  TermWrapper n2_(1+2e-10);
+  TermWrapper n2__(1+5e-9);
+  INFO("n1=" << n1);
+  INFO("n1_=" << n1_);
+  INFO("n1__=" << n1__);
+  INFO("n2=" << n2);
+  INFO("n2_=" << n2_);
+  INFO("n2__=" << n2__);
   // Check number specific method's
-  BOOST_CHECK_CLOSE(number1->number(), 0.5, 0.00001);
-  BOOST_CHECK_CLOSE(number2->number(), 1, 0.00001);
-  BOOST_CHECK(not number1->is_int());
-  BOOST_CHECK(number2->is_int());
-  BOOST_CHECK(not number2__->is_int());
-  // Check == operator
-  BOOST_CHECK_EQUAL(*number1, *number1_);
-  BOOST_CHECK_EQUAL(*number2, *number2_);
-  BOOST_CHECK_NE(*number1, *number1__);
-  BOOST_CHECK_NE(*number2, *number2__);
-  // Check < operator
-  BOOST_CHECK_LT(*number1, *number2);
-  BOOST_CHECK_LT(*number1, *number1__);
-  BOOST_CHECK(not(*number1 < *number1_));
-  BOOST_CHECK(not(*number2 < *number1));
-  // Check hash correctness
-  BOOST_CHECK_EQUAL(number1->hash(), number1__->hash()); // non-ints should have the same hash
-  BOOST_CHECK_EQUAL(number2->hash(), number2_->hash());
-  BOOST_CHECK_NE(number2->hash(), number2__->hash());
-}
-
-BOOST_AUTO_TEST_CASE(variable_test)
-{
-  auto variable1 = V("variable1");
-  auto variable1_ = V("variable1");
-  auto variable2 = V("variable2");
-  INFO("variable1=" << *variable1);
-  INFO("variable1_=" << *variable1_);
-  INFO("variable2=" << *variable2);
-  // Check name method
-  BOOST_CHECK_EQUAL(variable1->name(), "variable1");
+  BOOST_CHECK_CLOSE(n1.get_number_term()->get_number(), 0.5, 0.00001);
+  BOOST_CHECK_CLOSE(n2.get_number_term()->get_number(), 1, 0.00001);
+  BOOST_CHECK(not n1.get_number_term()->is_int());
+  BOOST_CHECK(not n2__.get_number_term()->is_int());
+  BOOST_CHECK(n2.get_number_term()->is_int());
+  BOOST_CHECK(n2_.get_number_term()->is_int());
   // Check == operator
-  BOOST_CHECK_EQUAL(*variable1, *variable1_);
-  BOOST_CHECK_NE(*variable1, *variable2);
+  BOOST_CHECK_EQUAL(n1, n1_);
+  BOOST_CHECK_EQUAL(n2, n2_);
+  BOOST_CHECK_NE(n1, n1__);
+  BOOST_CHECK_NE(n2, n2__);
+  BOOST_CHECK_NE(n1, n2);
   // Check < operator
-  BOOST_CHECK_LT(*variable1, *variable2);
-  BOOST_CHECK(not(*variable2 < *variable1));
+  BOOST_CHECK_LT(n1, n2);
+  BOOST_CHECK_LT(n1, n1__);
+  BOOST_CHECK_GE(n1_, n1);
+  BOOST_CHECK_GT(n2, n1);
   // Check hash correctness
-  BOOST_CHECK_EQUAL(variable1->hash(), variable1_->hash());
-  BOOST_CHECK_NE(variable1->hash(), variable2->hash());
+  BOOST_CHECK_EQUAL(n1.hash(), n1.hash()); // non-ints should have the same hash
+  BOOST_CHECK_EQUAL(n2.hash(), n2_.hash());
+  BOOST_WARN_NE(n2.hash(), n2__.hash()); // Very likely the hashes are
+                                              // different
 }
 
-BOOST_AUTO_TEST_CASE(term_v_test)
+BOOST_AUTO_TEST_CASE(mixed_test)
 {
-  auto term_v_1 = L(A("a"), N(1), V("X"));
-  auto term_v_1_ = L(A("a"), N(1), V("X"));
-  auto term_v_2 = L(A("a"), N(1), A("x"));
-  auto term_v_3 = L(A("a"), A("x"));
-  auto term_v_4 = L(A("a"), A("y"));
-  auto term_v_5 = L(A("y"), A("a"));
-  INFO("term_v_1=" << *term_v_1);
-  INFO("term_v_1_=" << *term_v_1_);
-  INFO("term_v_2=" << *term_v_2);
-  INFO("term_v_3=" << *term_v_3);
-  INFO("term_v_4=" << *term_v_4);
-  INFO("term_v_5=" << *term_v_5);
-  // Check size, at, and iterators
-  BOOST_CHECK_EQUAL(term_v_1->size(), 3);
-  BOOST_CHECK_EQUAL(*term_v_1->at(0), *A("a"));
-  BOOST_CHECK_EQUAL(*term_v_1->at(1), *N(1));
-  BOOST_CHECK_EQUAL(*term_v_1->at(2), *V("X"));
-  auto it = term_v_1->begin();
-  BOOST_CHECK_EQUAL(**it, *A("a"));
-  it += 3;
-  BOOST_CHECK(it == term_v_1->end());
-  // Check is_ground
-  //BOOST_CHECK(term_v_2->is_ground());
-  //BOOST_CHECK(not ẗerm_v_1->is_ground());
-  // Check == operator
-  BOOST_CHECK_EQUAL(*term_v_1, *term_v_1_);
-  BOOST_CHECK_NE(*term_v_1, *term_v_2);
-  BOOST_CHECK_NE(*term_v_1, *term_v_3);
-  BOOST_CHECK_NE(*term_v_4, *term_v_5);
-  // Check < operator
-  BOOST_CHECK_LT(*term_v_2, *term_v_1);
-  BOOST_CHECK_LT(*term_v_3, *term_v_2);
-  BOOST_CHECK_LT(*term_v_3, *term_v_4);
-  // Check hash correctness
-  BOOST_CHECK_EQUAL(term_v_1->hash(), term_v_1_->hash());
-  BOOST_CHECK_NE(term_v_4->hash(), term_v_5->hash());
-  // Check to_str
-  BOOST_CHECK_EQUAL(term_v_4->to_str(), "a,y");
+  TermWrapper t1(0);
+  TermWrapper t2("atom");
+  INFO("t1=" << t1);
+  INFO("t2=" << t2);
+  BOOST_CHECK_NE(t1, t2);
+  BOOST_CHECK_LT(t2, t1);
+  BOOST_WARN_NE(t1.hash(), t2.hash());
 }
 
 BOOST_AUTO_TEST_CASE(predicate_test)
 {
-  auto pred1 = P("p", A("x"), A("y"));
-  auto pred1_ = P("p", A("x"), A("y"));
-  auto pred2 = P("q", A("x"), A("y"));
-  auto pred3 = P("p", A("x"));
-  INFO("pred1=" << *pred1);
-  INFO("pred1_=" << *pred1_);
-  INFO("pred2=" << *pred2);
-  INFO("pred3=" << *pred3);
-  // Check == operator
-  BOOST_CHECK_EQUAL(*pred1, *pred1_);
-  BOOST_CHECK_NE(*pred1, *pred2);
-  BOOST_CHECK_NE(*pred1, *pred3);
-  // CHECK <  OPERATOR
-  BOOST_CHECK_LT(*pred1, *pred2);
-  BOOST_CHECK_LT(*pred3, *pred1);
-  BOOST_CHECK(not(*pred1 < *pred3));
-  // Check to_str
-  BOOST_CHECK_EQUAL(pred1->to_str(), "p(x,y)");
+  Predicate p1("p", "x", "y");
+  Predicate p1_("p", "x", "y");
+  Predicate p1__("p", "y", "x");
+  Predicate p2("p", "X", "y");
+  Predicate p3("q", "x");
+  Predicate p4("q", 1);
+  Predicate p5("r");
+  INFO("p1=" << p1);
+  INFO("p1_=" << p1_);
+  INFO("p1__=" << p1__);
+  INFO("p2=" << p2);
+  INFO("p3=" << p3);
+  INFO("p4=" << p4);
+  INFO("p5=" << p5);
+  // Check ==, < operators
+  BOOST_CHECK_EQUAL(p1, p1_);
+  BOOST_CHECK_NE(p1, p1__);
+  BOOST_CHECK_NE(p1, p2);
+  BOOST_CHECK_NE(p1, p3);
+  BOOST_CHECK_NE(p1, p5);
+  BOOST_CHECK_LT(p1, p3);
+  BOOST_CHECK_LT(p3, p4);
+  // Hash correctness
+  BOOST_CHECK_EQUAL(p1.hash(), p1_.hash());
+  BOOST_WARN_NE(p1.hash(), p1__.hash());
+  BOOST_WARN_NE(p1.hash(), p5.hash());
+  // Ground?
+  BOOST_CHECK(p1.is_ground());
+  BOOST_CHECK(not p2.is_ground());
+  BOOST_CHECK(p5.is_ground());
+  // spec
+  BOOST_CHECK_EQUAL(p1.get_specification(), "p/2");
+  BOOST_CHECK_EQUAL(p1__.get_specification(), "p/2");
+  BOOST_CHECK_EQUAL(p3.get_specification(), "q/1");
+  BOOST_CHECK_EQUAL(p5.get_specification(), "r/0");
 }
 
-BOOST_AUTO_TEST_CASE(substitution_test)
+template <class Set>
+void set_test_aux()
 {
-  Substitution sigma{{"X", A("a")}, {"Y", N(0)}};
-  INFO("sigma=" << sigma);
-  auto pred1 = P("p", V("X"), V("Y"));
-  auto pred2 = P("q", A("a"), V("Z"), V("X"));
-  auto pred1_ = sigma(pred1);
-  auto pred2_ = sigma(pred2);
-  BOOST_CHECK_EQUAL(*pred1_, *P("p", A("a"), N(0)));
-  BOOST_CHECK_EQUAL(*pred2_, *P("q", A("a"), V("Z"), A("a")));
+  // Further check the correctness of the < and == operators via set operations.
+  Predicate p1("p", "x", "y");
+  Predicate p1_("p", "x", "y");
+  Predicate p2("p", "X", 5);
+  Predicate p3("q", 0);
+  Predicate p4("r");
+  Set set{p1, p1_, p2, p3, p4};
+  INFO("Ordered set (on creation): " << set);
+  BOOST_CHECK_EQUAL(set.size(), 4);
+  set.erase(p1);
+  INFO("Ordered set (after removing p(x,y)): " << set);
+  BOOST_CHECK_EQUAL(set.size(), 3);
+  set.erase(Predicate("q", 5e-9));
+  INFO("Ordered set (after trying to remove non-existent number): " << set);
+  BOOST_CHECK_EQUAL(set.size(), 3);
+  set.erase(Predicate("q", 5e-10));
+  INFO("Ordered set (after removing existent number): " << set);
+  BOOST_CHECK_EQUAL(set.size(), 2);
+  set.insert(Predicate("r"));
+  INFO("Ordered set (after trying to insert existent predicate): " << set);
+  BOOST_CHECK_EQUAL(set.size(), 2);
+  set.insert(Predicate("s", 7));
+  INFO("Ordered set (after inserting non-existent predicate): " << set);
+  BOOST_CHECK_EQUAL(set.size(), 3);
 }
 
 BOOST_AUTO_TEST_CASE(ordered_set_test)
 {
-  // Further check the correctness of the < and == operators via set operations.
-  Predicate p1("p", {A("x"), A("y")});
-  Predicate p1_("p", {A("x"), A("y")});
-  Predicate p2("p", {V("X"), N(5)});
-  Predicate p3("q", {N(0)});
-  Predicate p4("r", {});
-  std::set<Predicate> o_set{p1, p1_, p2, p3, p4};
-  INFO("Ordered set (on creation): " << o_set);
-  BOOST_CHECK_EQUAL(o_set.size(), 4);
-  o_set.erase(p1);
-  INFO("Ordered set (after removing p(x,y)): " << o_set);
-  BOOST_CHECK_EQUAL(o_set.size(), 3);
-  o_set.erase(Predicate("q", {N(5e-9)}));
-  INFO("Ordered set (after trying to remove non-existent number): " << o_set);
-  BOOST_CHECK_EQUAL(o_set.size(), 3);
-  o_set.erase(Predicate("q", {N(5e-10)}));
-  INFO("Ordered set (after removing existent number): " << o_set);
-  BOOST_CHECK_EQUAL(o_set.size(), 2);
-  o_set.insert(Predicate("r", {}));
-  INFO("Ordered set (after trying to insert existent predicate): " << o_set);
-  BOOST_CHECK_EQUAL(o_set.size(), 2);
-  o_set.insert(Predicate("s", {N(7)}));
-  INFO("Ordered set (after inserting non-existent predicate): " << o_set);
-  BOOST_CHECK_EQUAL(o_set.size(), 3);
+  typedef std::set<Predicate,std::less<Predicate>,std::allocator<Predicate>>
+    Set;
+  set_test_aux<Set>();
 }
 
 BOOST_AUTO_TEST_CASE(unordered_set_test)
 {
-  // Further check the correctness of the hash and == methods via set operations.
-  Predicate p1("p", {A("x"), A("y")});
-  Predicate p1_("p", {A("x"), A("y")});
-  Predicate p2("p", {V("X"), N(5)});
-  Predicate p3("q", {N(0)});
-  Predicate p4("r", {});
-  std::unordered_set<Predicate, std::hash<Term>> u_set{p1, p1_, p2, p3, p4};
-  INFO("Unordered set (on creation): " << u_set);
-  BOOST_CHECK_EQUAL(u_set.size(), 4);
-  u_set.erase(p1);
-  INFO("Unordered set (after removing p(x,y)): " << u_set);
-  BOOST_CHECK_EQUAL(u_set.size(), 3);
-  u_set.erase(Predicate("q", {N(5e-9)}));
-  INFO("Unordered set (after trying to remove non-existent number): " << u_set);
-  BOOST_CHECK_EQUAL(u_set.size(), 3);
-  u_set.erase(Predicate("q", {N(5e-10)}));
-  INFO("Unordered set (after removing existent number): " << u_set);
-  BOOST_CHECK_EQUAL(u_set.size(), 2);
-  u_set.insert(Predicate("r", {}));
-  INFO("Unordered set (after trying to insert existent predicate): " << u_set);
-  BOOST_CHECK_EQUAL(u_set.size(), 2);
-  u_set.insert(Predicate("s", {N(7)}));
-  INFO("Unordered set (after inserting non-existent predicate): " << u_set);
-  BOOST_CHECK_EQUAL(u_set.size(), 3);
+  typedef std::unordered_set<Predicate,std::hash<Hashable>,
+          std::equal_to<Predicate>,std::allocator<Predicate>> Set;
+  set_test_aux<Set>();
+}
+
+BOOST_AUTO_TEST_CASE(state_query_test)
+{
+
 }
 
diff --git a/src/types.cpp b/src/types.cpp
index 749e10e8cfb4b88493a913ab36e4b025ce91575e..30cf5c6593b9a43c13d0b85c79b1e485e673264f 100644
--- a/src/types.cpp
+++ b/src/types.cpp
@@ -1,311 +1,251 @@
 #include "types.h"
+#include <iostream>
 #include <cmath>
 #include <sstream>
 
 namespace imagine_planner
 {
 
-// Implementation of Atom's methods
+// LiteralTerm
 
-Atom::Atom(const std::string& name) : name_(name) {}
+LiteralTerm::LiteralTerm(const std::string& literal) : literal_(literal) {}
 
-bool Atom::operator==(const Term& other) const
+std::size_t LiteralTerm::hash() const
 {
-  if (const Atom* c_other = dynamic_cast<const Atom*>(&other))
-  {
-    return this->name_ == c_other->name_;
-  }
-  return false;
-}
-
-bool Atom::operator<(const Term& other) const
-{
-  if (const Atom* c_other = dynamic_cast<const Atom*>(&other))
-  {
-    return this->name_ < c_other->name_;
-  }
-  return this->type() < other.type();
+  std::hash<std::string> h;
+  return h(literal_);
 }
 
-std::size_t Atom::hash() const
+bool LiteralTerm::is_ground() const
 {
-  std::hash<std::string> h;
-  return h(name_);
+  if (literal_.empty()) return false;
+  if (literal_[0] == '_') return false;
+  if (literal_[0] >= 'A' and literal_[0] <= 'Z') return false;
+  return true;
 }
 
-// Implementation of Number's methods
-
-double Number::EPSILON_ = 1E-9;
-
-Number::Number(double number) : number_(number) {}
-
-bool Number::operator==(const Term& other) const
+bool LiteralTerm::operator==(const Term& term) const
 {
-  if (const Number* c_other = dynamic_cast<const Number*>(&other))
+  if (auto other = dynamic_cast<const LiteralTerm*>(&term))
   {
-    return std::fabs(this->number_ - c_other->number_) < EPSILON_;
+    return this->literal_ == other->literal_;
   }
   return false;
 }
 
-bool Number::operator<(const Term& other) const
+bool LiteralTerm::operator<(const Term& term) const
 {
-  if (const Number* c_other = dynamic_cast<const Number*>(&other))
+  if (auto other = dynamic_cast<const LiteralTerm*>(&term))
   {
-    return c_other->number_ - this->number_ >= EPSILON_;
+    return this->literal_ < other->literal_;
   }
-  return this->type() < other.type();
+  return type() < term.type();
 }
 
-std::size_t Number::hash() const
+// NumberTerm
+
+double NumberTerm::EPSILON_ = 1E-9;
+
+NumberTerm::NumberTerm(double number) : number_(number) {}
+
+std::size_t NumberTerm::hash() const
 {
   std::hash<int> h;
-  // Return 0 for non-integer values to avoid problems in maps and sets
-  // (non-integer quantities would be assigned to the same bucket).
-  return is_int()? h(std::round(number_)) : 0;
+  return is_int()? h((int)std::round(number_)) : 0;
 }
 
-bool Number::is_int() const
+bool NumberTerm::is_int() const
 {
   return std::fabs(number_ - std::round(number_)) < EPSILON_;
 }
 
-// Implementation of Variable's methods
-
-Variable::Variable(const std::string& name) : name_(name) {}
-
-bool Variable::operator==(const Term& other) const
+bool NumberTerm::operator==(const Term& term) const
 {
-  if (const Variable* c_other = dynamic_cast<const Variable*>(&other))
+  if (auto other = dynamic_cast<const NumberTerm*>(&term))
   {
-    return this->name_ == c_other->name_;
+    return std::fabs(this->number_ - other->number_) < EPSILON_;
   }
   return false;
 }
 
-bool Variable::operator<(const Term& other) const
+bool NumberTerm::operator<(const Term& term) const
 {
-  if (const Variable* c_other = dynamic_cast<const Variable*>(&other))
+  if (auto other = dynamic_cast<const NumberTerm*>(&term))
   {
-    return this->name_ < c_other->name_;
+    return other->number_ - this->number_ >= EPSILON_;
   }
-  return this->type() < other.type();
-}
-
-std::size_t Variable::hash() const
-{
-  std::hash<std::string> h;
-  return h(name_);
+  return type() < term.type();
 }
 
-// Implementation of TermV's methods
+// TermWrapper
 
-TermV::TermV() {}
+TermWrapper::TermWrapper(const TermWrapper& term) : term_(term.term_->clone()) {}
 
-TermV::TermV(const std::vector<Term::Ptr>& term_v) : term_v_(term_v) {}
+TermWrapper::TermWrapper(const std::string& literal) :
+  term_(new LiteralTerm(literal)) {}
 
-TermV::TermV(const std::initializer_list<Term::Ptr>& il) : term_v_(il) {}
+TermWrapper::TermWrapper(double number) : term_(new NumberTerm(number)) {}
 
-std::string TermV::to_str() const
+const LiteralTerm* TermWrapper::get_literal_term() const
 {
-  std::ostringstream oss;
-  bool first = true;
-  for (auto term : term_v_)
-  {
-    if (not first) oss << ',';
-    oss << *term;
-    first = false;
-  }
-  return oss.str();
+  return dynamic_cast<const LiteralTerm*>(term_);
 }
 
-bool TermV::is_ground() const
+const NumberTerm* TermWrapper::get_number_term() const
 {
-  for (auto term : term_v_)
-  {
-    if (not term->is_ground()) return false;
-  }
-  return true;
+  return dynamic_cast<const NumberTerm*>(term_);
 }
 
-bool TermV::operator==(const Term& other) const
+TermWrapper& TermWrapper::operator=(const TermWrapper& term)
 {
-  if (const TermV* c_other = dynamic_cast<const TermV*>(&other))
-  {
-    if (this->size() != c_other->size()) return false;
-    for (int idx = 0; idx < this->size(); ++idx)
-    {
-      if (*(this->at(idx)) != *(c_other->at(idx))) return false;
-    }
-    return true;
-  }
-  return false;
+  delete term_;
+  term_ = term.term_->clone();
+  return *this;
 }
 
-bool TermV::operator<(const Term& other) const
+TermWrapper::~TermWrapper()
 {
-  if (const TermV* c_other = dynamic_cast<const TermV*>(&other))
-  {
-    if (this->size() < c_other->size()) return true;
-    if (this->size() > c_other->size()) return false;
-    for (int idx = 0; idx < this->size(); ++idx)
-    {
-      if (*(this->at(idx)) < *(c_other->at(idx))) return true;
-      if (*(c_other->at(idx)) < *(this->at(idx))) return false;
-    }
-    return false;
-  }
-  return this->type() < other.type();
+  delete term_;
 }
 
-std::size_t TermV::hash() const
+// Predicate
+
+Predicate::Predicate(const std::string& name, const TermV& arguments) :
+  name_(name), arguments_(arguments) {}
+
+bool Predicate::is_ground() const
 {
-  size_t ret = 0;
-  std::hash<Term> h;
-  for (auto term : term_v_)
+  for (const TermWrapper& term : arguments_)
   {
-    ret ^= h(*term) + 0x9e3779b9 + (ret << 6) + (ret >> 2);
+    if (not term.is_ground()) return false;
   }
-  return ret;
+  return true;
 }
 
-// Implementation of Predicate's methods
-
-Predicate::Predicate(const std::string& name, const TermV& arguments) :
-  name_(name), arguments_(arguments) {}
-
-std::string Predicate::to_str() const
+std::string Predicate::get_specification() const
 {
   std::ostringstream oss;
-  oss << name_ << '(' << arguments_ << ')';
+  oss << name_ << '/' << arguments_.size();
   return oss.str();
 }
 
-bool Predicate::operator==(const Term& other) const
+std::string Predicate::to_str() const
 {
-  if (const Predicate* c_other = dynamic_cast<const Predicate*>(&other))
+  std::ostringstream oss;
+  oss << name_ << '(';
+  bool first = true;
+  for (const TermWrapper& term : arguments_)
   {
-    return this->name_ == c_other->name_ and
-           this->arguments_ == c_other->arguments_;
+    if (not first) oss << ',';
+    oss << term;
+    first = false;
   }
-  return false;
+  oss << ')';
+  return oss.str();
 }
 
-bool Predicate::operator<(const Term& other) const
+std::size_t Predicate::hash() const
 {
-  if (const Predicate* c_other = dynamic_cast<const Predicate*>(&other))
+  std::hash<std::string> hasher_s;
+  std::hash<Hashable> hasher_h;
+  std::size_t acc = hasher_s(name_);
+  for (const TermWrapper& term : arguments_)
   {
-    if (this->name_ < c_other->name_) return true;
-    if (c_other->name_ < this->name_) return false;
-    return this->arguments_ < c_other->arguments_;
+    acc ^= hasher_h(term) + 0x9e3779b9 + (acc<<6) + (acc>>2);
   }
-  return this->type() < other.type();
+  return acc;
 }
 
-std::size_t Predicate::hash() const
+bool Predicate::operator==(const Predicate& predicate) const
 {
-  std::hash<std::string> h;
-  return h(name_)^(arguments_.hash());
+  if (name_ != predicate.name_) return false;
+  if (arguments_.size() != predicate.arguments_.size()) return false;
+  for (std::size_t idx = 0; idx < arguments_.size(); ++idx)
+  {
+    if (arguments_[idx] != predicate.arguments_[idx]) return false;
+  }
+  return true;
 }
 
-// Implementation of Substitution's methods
-
-Substitution::Substitution(std::initializer_list<Entry> il) : map_(il) {}
-
-std::string Substitution::to_str() const
+bool Predicate::operator<(const Predicate& predicate) const
 {
-  std::ostringstream oss;
-  oss << "{";
-  bool first = true;
-  for (auto entry : map_)
+  if (name_ < predicate.name_) return true;
+  if (name_ > predicate.name_) return false;
+  if (arguments_.size() < predicate.arguments_.size()) return true;
+  if (arguments_.size() > predicate.arguments_.size()) return false;
+  for (std::size_t idx = 0; idx < arguments_.size(); ++idx)
   {
-    if (not first) oss << ',';
-    oss << "\n  " << entry.first << " -> " << *entry.second;
-    first = false;
+    if (arguments_[idx] < predicate.arguments_[idx]) return true;
+    if (arguments_[idx] > predicate.arguments_[idx]) return false;
   }
-  if (not first) oss << '\n';
-  oss << '}';
-  return oss.str();
+  return false;
 }
 
-Term::Ptr Substitution::get(const std::string& key, Term::Ptr default_) const
-{
-  auto it = map_.find(key);
-  return it == map_.end()? default_ : it->second;
-}
+// Implementation of PlanState
+
+PlanState::PlanState() {}
 
-void Substitution::put(const std::string& key, Term::Ptr term)
+PlanState::PlanState(std::initializer_list<Predicate> il) : predicates_(il) {}
+
+// Implementation of StateQuery
+
+void add_predicate_to_pl(const Predicate& predicate)
 {
-  map_[key] = term;
+  std::size_t arity = predicate.arity();
+  const TermV& arguments = predicate.get_arguments();
+  PlTermv pl_termv(arity);
+  for (std::size_t idx = 0; idx < arity; ++idx)
+  {
+    if (auto casted = arguments[idx].get_literal_term())
+    {
+      pl_termv[idx] = casted->get_literal().c_str();
+    }
+    else if (auto casted = arguments[idx].get_number_term())
+    {
+      pl_termv[idx] = (long)casted->get_number();
+    }
+  }
+  PlCompound pl_pred(predicate.get_name().c_str(), pl_termv);
+  std::cout << "Adding " << predicate << std::endl;
+  PlCall("assertz", pl_pred);
+  std::cout << "Added " << predicate << std::endl;
 }
 
-void Substitution::remove(const std::string& key)
+StateQuery::StateQuery(const PlanState& state, const TermV& parameters,
+    const std::string& query) :
+  state_(state), parameters_(parameters), values_(parameters),
+  pl_values_(parameters.size()), query_(new PlQuery(query.c_str(), pl_values_))
 {
-  map_.erase(key);
+  for (const Predicate& predicate : state_)
+  {
+    add_predicate_to_pl(predicate);
+  }
 }
 
-Predicate::Ptr Substitution::operator()(Predicate::Ptr input) const
+bool StateQuery::next_solution()
 {
-  std::vector<Term::Ptr> arguments;
-  for (auto term : input->arguments())
+  if (query_->next_solution())
   {
-    if (auto var = std::dynamic_pointer_cast<const Variable>(term))
-    {
-      arguments.push_back(get(var->name(), var));
-    }
-    else
+    for (std::size_t idx = 0; idx < parameters_.size(); ++idx)
     {
-      arguments.push_back(term);
+      if (pl_values_[idx].type() == PL_ATOM)
+      {
+        values_[idx] = TermWrapper((char*)pl_values_[idx]);
+      }
+      else if (pl_values_[idx].type() == PL_INTEGER)
+      {
+        values_[idx] = TermWrapper((long)pl_values_[idx]);
+      }
     }
+    return true;
   }
-  return Predicate::Ptr(new Predicate(input->name(), arguments));
+  return false;
 }
 
-// Implementation of State's methods
-
-// Implementation of StateQuery's method
-
-//void StateQuery::reset(const Substitution& sigma_0)
-//{
-  //sigma_0_ = sigma_0;
-  //cur_predicate_ = predicate_range_.first;
-  //if (child != nullptr) child->reset(sigma_0);
-//}
-
-//StateQuery::StateQuery(const State& state, const Predicate* query,
-    //int query_size, const Substitution& sigma_0) :
-  //state_(state), query_(query), query_size_(query_size), child_(nullptr),
-  //done_(false), sigma_0_(sigma_0)
-//{
-  //if (query_ != nullptr and query_size_ != 0)
-  //{
-    //child_ = StateQuery(state_, query_+sizeof(Predicate), query_size_-1,
-        //sigma_0_);
-  //}
-  //predicate_range_ = state_.predicates(query->name());
-  //cur_predicate_ = predicate_range_.first;
-//}
-
-//bool StateQuery::next_solution()
-//{
-  //if (query_size_ == 0)
-  //{
-    //if (done_) return false;
-    //done_ = true;
-    //return true;
-  //}
-
-//}
-
-//const Substitution& StateQuery::get_substitution() const
-//{
-  //return query_size_ == 0? sigma_0_ : child_->get_substitution();
-//}
-
-//StateQuery::~StateQuery()
-//{
-  //if (child_ != nullptr) delete child_;
-//}
+StateQuery::~StateQuery()
+{
+  /* TO-DO: retract all facts */
+}
 
 // Implementation of stream operator
 
@@ -319,11 +259,11 @@ std::ostream& operator<<(std::ostream& os, const Stringifiable& strable)
 namespace std
 {
 
-std::size_t hash<imagine_planner::Term>::operator()(
-    const imagine_planner::Term& term) const
+std::size_t hash<imagine_planner::Hashable>::operator()(
+    const imagine_planner::Hashable& hashable) const
 {
-  return term.hash();
+  return hashable.hash();
 }
 
-}
+} /* end std namespace */
 
diff --git a/src/types.h b/src/types.h
index 1ac8aadaa80f213316844a9834d167850ad916a8..23cb5039c4aac451cfc0167f5bfc9df246483e50 100644
--- a/src/types.h
+++ b/src/types.h
@@ -4,23 +4,23 @@
 // Let's group some functions and typedefs that are common to all the Types
 // defined here in a macro for convenience.
 #define TYPES_COMMON(Class)\
-    typedef std::shared_ptr<const Class> Ptr;\
     virtual std::string type() const override { return #Class; }\
+    virtual Term* clone() const override { return new Class(*this); };
 
 #include <functional>
 #include <memory>
 #include <ostream>
 #include <string>
 #include <vector>
-#include <map>
+#include <set>
+#include <SWI-cpp.h>
 
 namespace imagine_planner
 {
 
-
 /** 
  * @brief Abstract class (interface-like) that simply declares the to_str
- * method (to be implemented by specific types).
+ * method (to be implemented by concrete classes).
  */
 class Stringifiable
 {
@@ -36,503 +36,268 @@ class Stringifiable
     virtual ~Stringifiable() {}
 };
 
-/** 
- * @brief Generic Term class.
- *
- * Declares the == and < operators and the hash function so they can be used
- * with both unordered and ordered sets/maps. The class is abstract.
- * Functionality is given by this class descendants (Atom, Number, TermV and
- * Predicate). Terms are immutable.
- */
-class Term : public Stringifiable
+class Hashable
 {
   public:
-
-    /** Terms are immutable, so only pointers to const types are considered. */
-    typedef std::shared_ptr<const Term> Ptr;
-    
-    /** 
-     * @brief Tells whether the term has a nested unground variable.
-     * 
-     * @return true if the term is an unground variable or contains one.
-     */
-    virtual bool is_ground() const =0;
-
-    /** 
-     * @brief true for atomic terms (i.e. numbers and atoms).
-     * 
-     * @return true if the term is atomic.
-     */
-    virtual bool is_atomic() const =0;
-
-    /** 
-     * @brief Equality operator. Each type of Term is responsible to implement
-     * one that works for its own type.
-     * 
-     * @param other Another term
-     * 
-     * @return true if the two terms are equal.
-     */
-    virtual bool operator==(const Term& other) const =0;
-
-    /** 
-     * @brief Simple inequality operator implemented as the negation of the
-     * result given by operator==.
-     * 
-     * @param other Another term
-     * 
-     * @return true if the two terms are not equal.
-     */
-    virtual bool operator!=(const Term& other) const
-    {
-      return not(*this == other);
-    }
-
-    /** 
-     * @brief LT operator. Included in the Term interface so terms can be used
-     * in ordered sets and maps.
-     * 
-     * @param other Another term
-     * 
-     * @return true if this term is smaller than the other.
-     */
-    virtual bool operator<(const Term& other) const =0;
-
-    /** 
-     * @brief Hash method, specified so terms can be used in unordered sets
-     * and maps.
-     * 
-     * @return hash integer
-     */
     virtual std::size_t hash() const =0;
 
-    /** 
-     * @brief Gives the type (class) of this term, so it can be used in
-     * heterogeneous comparisons (e.g. comparing Atoms with Numbers).
-     *
-     * It is not necessary to implement this method manually since it is
-     * automatically introduced by the TYPES_COMMON macro.
-     * 
-     * @return the stringified class name.
-     */
-    virtual std::string type() const =0;
-
-    /** 
-     * @brief Virtual destructor.
-     */
-    virtual ~Term() {}
+    virtual ~Hashable() {}
 };
 
-
-/** 
- * @brief This Term can be used to represent qualitative concepts like names.
- *
- * It essentially contains a string: the name of the atom.
- */
-class Atom : public Term
+class Term : public Stringifiable,
+             public Hashable
 {
-  private:
-
-    std::string name_;
-
   public:
 
-    TYPES_COMMON(Atom);
-
-    /** 
-     * @brief Creates an Atom with a certain name.
-     * 
-     * @param name Name (label) of the atom.
-     */
-    Atom(const std::string& name);
-
-    /** 
-     * @brief The representation consists simply in the Atom's name.
-     * 
-     * @return Atom's name
-     */
-    virtual std::string to_str() const override { return name_; }
-
-    /** 
-     * @brief Always returns true.
-     * 
-     * @return true.
-     */
-    virtual bool is_ground() const override { return true; }
-
-    /** 
-     * @brief Always returns true.
-     * 
-     * @return true.
-     */
-    virtual bool is_atomic() const override { return true; }
-
-    /** 
-     * @brief A term is equal to an Atom iff it is also an Atom and has the
-     * same name.
-     * 
-     * @param other Another Term.
-     * 
-     * @return true if both terms are Atoms and have the same name.
-     */
-    virtual bool operator==(const Term& other) const override;
-
-    /** 
-     * @brief Tells whether this Atom is lexicographically smaller than another
-     * given one.
-     *
-     * If both terms are Atoms, the method uses the Atoms' names to establish
-     * the lexicographical order. Otherwise, it uses the Term's types.
-     * 
-     * @param other Another Term.
-     * 
-     * @return true if this term is lexicographically smaller.
-     */
-    virtual bool operator<(const Term& other) const override;
-
-    /** 
-     * @brief Standard string hash is applied to name.
-     * 
-     * @return name's hash.
-     */
-    virtual std::size_t hash() const override;
-
-    /** 
-     * @brief Gives Atom's name.
-     *
-     * This is a class specific method (i.e. not present in Term).
-     * 
-     * @return Atom's name.
-     */
-    virtual std::string name() const { return name_; }
-
-};
-
-
-class Number : public Term
-{
-  private:
-
-    static double EPSILON_;
-
-    double number_;
+    virtual std::string type() const =0;
 
-  public:
+    virtual bool is_ground() const =0;
 
-    TYPES_COMMON(Number);
+    virtual bool operator==(const Term& term) const =0;
 
-    Number(double number);
+    virtual bool operator<(const Term& term) const =0;
 
-    virtual std::string to_str() const override
+    virtual bool operator<=(const Term& term) const
     {
-      return std::to_string(number_);
+      return *this < term or *this == term;
     }
 
-    virtual bool is_ground() const override { return true; }
-
-    virtual bool is_atomic() const override { return true; }
-
-    virtual bool operator==(const Term& other) const override;
-
-    virtual bool operator<(const Term& other) const override;
+    virtual bool operator!=(const Term& term) const
+    {
+      return not(*this == term);
+    }
 
-    virtual std::size_t hash() const override;
+    virtual bool operator>(const Term& term) const { return term < *this; }
 
-    bool is_int() const;
+    virtual bool operator>=(const Term& term) const { return term <= *this; }
 
-    double number() const { return number_; }
+    virtual Term* clone() const =0;
 
+    virtual ~Term() {}
 };
 
-
-/** 
- * @brief 
- */
-class Variable : public Term
+class LiteralTerm : public Term
 {
   private:
-
-    std::string name_;
+    std::string literal_;
 
   public:
+    LiteralTerm(const std::string& literal);
 
-    TYPES_COMMON(Variable);
-
-    Variable(const std::string& name);
-
-    virtual std::string to_str() const override { return name_; }
+    virtual std::string to_str() const override { return literal_; }
 
-    virtual bool is_ground() const override { return false; }
+    virtual std::size_t hash() const override;
 
-    virtual bool is_atomic() const override { return false; }
+    const std::string& get_literal() const { return literal_; }
 
-    virtual bool operator==(const Term& other) const override;
+    virtual bool is_ground() const override;
 
-    virtual bool operator<(const Term& other) const override;
+    virtual bool operator==(const Term& term) const override;
 
-    virtual std::size_t hash() const override;
+    virtual bool operator<(const Term& term) const override;
 
-    const std::string& name() const { return name_; }
+    TYPES_COMMON(LiteralTerm)
 
 };
 
-class TermV : public Term
+class NumberTerm : public Term
 {
   private:
-
-    std::vector<Term::Ptr> term_v_;
+    static double EPSILON_;
+    double number_;
 
   public:
+    NumberTerm(double number);
 
-    typedef std::vector<Term::Ptr>::const_iterator CIter;
-
-    TYPES_COMMON(TermV);
-
-    TermV();
-
-    TermV(const std::vector<Term::Ptr>& term_v);
-
-    TermV(const std::initializer_list<Term::Ptr>& il);
-
-    virtual std::string to_str() const override;
-
-    virtual bool is_ground() const override;
-
-    virtual bool is_atomic() const override { return false; }
-
-    virtual bool operator==(const Term& other) const override;
-
-    virtual bool operator<(const Term& other) const override;
+    std::string to_str() const override { return std::to_string(number_); }
 
     virtual std::size_t hash() const override;
 
-    int size() const { return term_v_.size(); }
+    bool is_int() const;
+
+    double get_number() const { return number_; }
 
-    const Term::Ptr at(int idx) const { return term_v_.at(idx); }
+    virtual bool is_ground() const override { return true; }
 
-    CIter begin() const { return term_v_.begin(); }
+    virtual bool operator==(const Term& term) const override;
 
-    CIter end() const { return term_v_.end(); }
+    virtual bool operator<(const Term& term) const override;
 
+    TYPES_COMMON(NumberTerm)
 };
 
-
-class Predicate : public Term
+class TermWrapper : public Stringifiable,
+                    public Hashable
 {
   private:
-
-    std::string name_;
-    TermV arguments_;
+    const Term* term_;
 
   public:
 
-    TYPES_COMMON(Predicate);
+    TermWrapper(const TermWrapper& term);
 
-    Predicate(const std::string& name, const TermV& arguments=TermV());
+    TermWrapper(const std::string& literal);
 
-    virtual std::string to_str() const override;
-
-    virtual bool is_ground() const override { return arguments_.is_ground(); }
-
-    virtual bool is_atomic() const override { return false; }
+    TermWrapper(double number);
 
-    virtual bool operator==(const Term& other) const override;
+    const LiteralTerm* get_literal_term() const;
 
-    virtual bool operator<(const Term& other) const override;
+    const NumberTerm* get_number_term() const;
 
-    virtual std::size_t hash() const override;
-
-    const std::string& name() const { return name_; }
+    bool is_ground() const { return term_->is_ground(); }
 
-    const TermV& arguments() const { return arguments_; }
+    virtual std::string to_str() const override { return term_->to_str(); }
 
-};
+    virtual std::size_t hash() const override { return term_->hash(); }
 
+    TermWrapper& operator=(const TermWrapper& term);
 
-class AtomFactory
-{
-  public:
-    
-    Atom::Ptr operator()(const std::string& name) const
+    bool operator==(const TermWrapper& term) const
     {
-      return Atom::Ptr(new Atom(name));
+      return *term_ == *(term.term_);
     }
-};
-
-
-class NumberFactory
-{
-  public:
 
-    Number::Ptr operator()(double number) const
+    bool operator<(const TermWrapper& term) const
     {
-      return Number::Ptr(new Number(number));
+      return *term_ < *(term.term_);
     }
-};
-
-
-class VariableFactory
-{
-  public:
 
-    Variable::Ptr operator()(const std::string& name) const
+    bool operator<=(const TermWrapper& term) const
     {
-      return Variable::Ptr(new Variable(name));
+      return *term_ <= *(term.term_);
     }
-};
-
-
-class TermVFactory
-{
-  private:
 
-    std::vector<Term::Ptr> gen_term_v() const
+    bool operator!=(const TermWrapper& term) const
     {
-      return std::vector<Term::Ptr>();
+      return *term_ != *(term.term_);
     }
 
-    template<typename... Args>
-    std::vector<Term::Ptr> gen_term_v(Term::Ptr term, Args... args) const
+    bool operator>(const TermWrapper& term) const
     {
-      auto term_v = gen_term_v(args...);
-      term_v.insert(term_v.begin(), term);
-      return term_v;
+      return *term_ > *(term.term_);
     }
 
-  public:
-
-    template<typename... Args>
-    TermV::Ptr operator()(Args... args) const
+    bool operator>=(const TermWrapper& term) const
     {
-      return TermV::Ptr(new TermV(gen_term_v(args...)));
+      return *term_ >= *(term.term_);
     }
 
+    ~TermWrapper();
 };
 
+typedef std::vector<TermWrapper> TermV;
 
-class PredicateFactory
-{
-  public:
+TermV create_term_v() { return TermV(); }
 
-   template<typename... Args>
-   Predicate::Ptr operator()(const std::string& name, Args... args) const
-   {
-     TermVFactory L;
-     return Predicate::Ptr(new Predicate(name, *L(args...)));
-   }
-};
+template <typename First, typename... Args>
+TermV create_term_v(const First& fst, Args... args)
+{
+  TermV term_v{TermWrapper(fst)};
+  TermV tail = create_term_v(args...);
+  term_v.insert(term_v.end(), tail.begin(), tail.end());
+  return term_v;
+}
 
+bool is_ground(const TermV& term_v);
 
-class Substitution : public Stringifiable
+class Predicate : public Stringifiable,
+                  public Hashable
 {
   private:
-
-    typedef std::map<std::string, Term::Ptr> Map;
-
-    Map map_;
+    std::string name_;
+    TermV arguments_;
 
   public:
+    template <typename... Args>
+    Predicate(const std::string& name, Args... args) :
+      name_(name), arguments_(create_term_v(args...)) {}
 
-    typedef std::pair<const std::string, Term::Ptr> Entry;
+    Predicate(const std::string& name, const TermV& arguments);
 
-    Substitution(std::initializer_list<Entry> il);
+    bool is_ground() const;
 
-    virtual std::string to_str() const override;
+    int arity() const { return arguments_.size(); }
 
-    Term::Ptr get(const std::string& key, Term::Ptr default_=nullptr) const;
+    const std::string& get_name() const { return name_; }
 
-    void put(const std::string& key, Term::Ptr term);
+    const TermV& get_arguments() const { return arguments_; }
 
-    void remove(const std::string& key);
+    virtual std::string get_specification() const;
 
-    Predicate::Ptr operator()(Predicate::Ptr input) const;
+    virtual std::string to_str() const override;
 
-    int size() const { return map_.size(); }
+    virtual std::size_t hash() const override;
 
-    Map::const_iterator begin() const { return map_.begin(); }
+    bool operator==(const Predicate& predicate) const;
 
-    Map::const_iterator end() const { return map_.begin(); }
+    bool operator<(const Predicate& predicate) const;
 
 };
 
-
-class StateQuery;
-
-
-class State : public Stringifiable
+class PlanState
 {
   private:
+    typedef std::set<Predicate> Container;
 
-    //typedef std::unordered_multiset<Predicate, std::hash<Predicate>> Set;
-    typedef std::multimap<std::string, Predicate> Map;
-
-    Map predicates_;
-    std::size_t hash_;
+    Container predicates_;
 
   public:
+    typedef Container::const_iterator CIter;
 
-    typedef std::pair<const std::string, Predicate> Entry;
-    typedef Map::const_iterator CIter;
-    typedef std::pair<CIter, CIter> Range;
-
-    State();
+    PlanState();
 
-    State(std::initializer_list<Entry> il);
+    PlanState(std::initializer_list<Predicate> il);
 
-    Range predicates(const std::string& type) const;
+    template <typename InputIterator>
+    PlanState(InputIterator begin, InputIterator end) :
+      predicates_(begin, end) {}
 
     CIter begin() const { return predicates_.begin(); }
 
     CIter end() const { return predicates_.end(); }
-    
-};
 
+};
 
 class StateQuery
 {
   private:
 
-    const State& state_;
-    const Predicate* query_;
-    int query_size_;
-    Substitution sigma_0_;
-
-    State::Range predicate_range_;
-    State::CIter cur_predicate_;
-    StateQuery* child_;
-    bool done_;
-
-    void reset();
-
-  protected:
-
-    StateQuery(const State& state, const Predicate* query=nullptr,
-        int query_size=0, const Substitution& sigma_0=Substitution{});
+    const PlanState& state_;
+    TermV parameters_, values_;
+    PlTermv pl_values_;
+    PlQuery* query_;
 
   public:
 
+    StateQuery(const PlanState& state, const TermV& parameters,
+        const std::string& query);
+
     bool next_solution();
 
-    const Substitution& get_substitution() const;
+    const TermV& get_values() const { return values_; }
 
     ~StateQuery();
-
-
 };
 
-//class State::Query
+//class Operator
 //{
   //private:
 
-    //const State& state_;
-    //Substitution substitution_;
+    //TermV parameters_, values_;
+    //std::string name_, pre_, post_;
 
   //public:
 
+    //Operator(TermV parameters_, const std::string& pre,
+        //const std::string& post);
 
+    //bool is_ground() const;
+
+    //int arity() const { return parameters_.size(); }
 
 //};
 
+
 /** 
  * @brief Stream operator that conveniently puts a Stringifiable object into
  * an output stream.
@@ -555,9 +320,9 @@ namespace std
  * unordered sets or maps.
  */
 template<>
-struct hash<imagine_planner::Term>
+struct hash<imagine_planner::Hashable>
 {
-  std::size_t operator()(const imagine_planner::Term& term) const;
+  std::size_t operator()(const imagine_planner::Hashable& hashable) const;
 };
 
 }