Add minimal test with some syntax sugar

Author: mezpusz

Test/SyntaxSugar.hpp

@@ -27,6 +27,7 @@
 #include "Kernel/Inference.hpp"
 #include "Kernel/Clause.hpp"
 #include "Kernel/HOL/HOL.hpp"
+#include "Kernel/FormulaUnit.hpp"
 #include "Kernel/SortHelper.hpp"
 #include "Kernel/NumTraits.hpp"
 #include "Kernel/TypedTermList.hpp"
@@ -713,9 +714,20 @@ inline Clause* clause(Stack<Lit> ls, Inference inf) {
 inline Clause* clause(Stack<Lit> ls)
 { return clause(ls, Inference(Kernel::NonspecificInference0(UnitInputType::ASSUMPTION, InferenceRule::INPUT))); }
 
-inline Clause* clause(std::initializer_list<Lit> ls) 
+inline Clause* clause(std::initializer_list<Lit> ls)
 { return clause(Stack<Lit>(ls)); }
 
+inline Stack<Clause*> clauses(std::initializer_list<std::initializer_list<Lit>> cls) {
+  auto out = Stack<Clause*>();
+  for (auto cl : cls) {
+    out.push(clause(cl));
+  }
+  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

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