Will add unit tests for Properties such as hasXEqualsY and onlyExistsForallPrefix (a draft for now)

Test/SyntaxSugar.hpp

@@ -26,6 +26,7 @@
 #include "Lib/Environment.hpp"
 #include "Kernel/Inference.hpp"
 #include "Kernel/Clause.hpp"
+#include "Kernel/FormulaUnit.hpp"
 #include "Kernel/SortHelper.hpp"
 #include "Kernel/NumTraits.hpp"
 #include "Kernel/ApplicativeHelper.hpp"
@@ -720,6 +721,9 @@ inline Stack<Clause*> clauses(std::initializer_list<std::initializer_list<Lit>>
   return out;
 }
 
+inline FormulaUnit* formula(Lit lit)
+{ return new FormulaUnit(new AtomicFormula(lit), Inference(Kernel::NonspecificInference0(UnitInputType::ASSUMPTION, InferenceRule::INPUT))); }
+
 inline void createTermAlgebra(SortSugar sort, std::initializer_list<FuncSugar> fs) {
   // avoid redeclaration
   if (env.signature->isTermAlgebraSort(sort.sugaredExpr())) {

UnitTests/tProperty.cpp

@@ -0,0 +1,38 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+
+#include "Test/UnitTesting.hpp"
+#include "Test/SyntaxSugar.hpp"
+
+#include "Shell/Property.hpp"
+
+using namespace Shell;
+
+/**
+ * NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses.
+ * See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available
+ */
+#define MY_SYNTAX_SUGAR                                                                    \
+  DECL_DEFAULT_VARS                                                                        \
+  DECL_SORT(s)                                                                             \
+  DECL_FUNC(f, {s}, s)                                                                     \
+  DECL_CONST(c, s)                                                                         \
+  DECL_PRED(p, {s})                                                                        \
+
+TEST_FUN(test01) {
+  __ALLOW_UNUSED(MY_SYNTAX_SUGAR);
+
+  auto units = UnitList::empty();
+  UnitList::push(clause({ f(c) == c, ~p(x) }), units);
+  UnitList::push(formula(f(c) != c), units);
+
+  auto prop = Property::scan(units);
+  ASS_EQ(prop->category(), Property::NEQ);
+}

cmake/sources.cmake

@@ -67,6 +67,7 @@ set(UNIT_TESTS
     UnitTests/tList.cpp
     UnitTests/tOption.cpp
     UnitTests/tOptionConstraints.cpp
+    UnitTests/tProperty.cpp
     UnitTests/tPushUnaryMinus.cpp
     UnitTests/tQKbo.cpp
     UnitTests/tQuotientE.cpp