Unit tests for trivial_sva(...)

unit/Makefile

@@ -8,6 +8,7 @@ SRC += smvlang/expr2smv.cpp \
        temporal-logic/ltl_sva_to_string.cpp \
        temporal-logic/sva_sequence_match.cpp \
        temporal-logic/nnf.cpp \
+       temporal-logic/trivial_sva.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I . -I $(CPROVER_DIR)/unit -I $(CPROVER_DIR)/src
@@ -20,7 +21,8 @@ include $(CPROVER_DIR)/src/common
 CXXFLAGS += -D'LOCAL_IREP_IDS=<hw_cbmc_irep_ids.h>'
 
 OBJ += ../src/smvlang/smvlang$(LIBEXT) \
-       ../src/temporal-logic/temporal-logic$(LIBEXT)
+       ../src/temporal-logic/temporal-logic$(LIBEXT) \
+       ../src/verilog/verilog$(LIBEXT)
 
 cprover.dir:
 	$(MAKE) $(MAKEARGS) -C ../src

unit/temporal-logic/trivial_sva.cpp

@@ -0,0 +1,60 @@
+/*******************************************************************\
+
+Module: Trivial SVA
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <temporal-logic/trivial_sva.h>
+#include <testing-utils/use_catch.h>
+#include <verilog/sva_expr.h>
+
+SCENARIO("Simplifying a trivial SVA formula")
+{
+  auto p = symbol_exprt{"p", bool_typet{}};
+  auto q = symbol_exprt{"q", bool_typet{}};
+  auto r = symbol_exprt{"r", bool_typet{}};
+
+  GIVEN("A trivial SVA formula with properties")
+  {
+    auto prop = [](exprt expr) {
+      return sva_boolean_exprt{std::move(expr), bool_typet{}};
+    };
+
+    REQUIRE(trivial_sva(sva_not_exprt{prop(p)}) == not_exprt{prop(p)});
+    REQUIRE(
+      trivial_sva(
+        sva_not_exprt{sva_and_exprt{prop(p), prop(q), bool_typet{}}}) ==
+      not_exprt{and_exprt{prop(p), prop(q)}});
+    REQUIRE(
+      trivial_sva(
+        sva_and_exprt{sva_not_exprt{prop(p)}, prop(q), bool_typet{}}) ==
+      and_exprt{not_exprt{prop(p)}, prop(q)});
+    REQUIRE(
+      trivial_sva(sva_and_exprt{
+        sva_or_exprt{prop(p), prop(q), bool_typet{}}, prop(r), bool_typet{}}) ==
+      and_exprt{or_exprt{prop(p), prop(q)}, prop(r)});
+  }
+
+  GIVEN("A trivial SVA formula with sequences")
+  {
+    auto sequence_type = verilog_sva_sequence_typet{};
+    auto seq = [](exprt expr) {
+      return sva_boolean_exprt{std::move(expr), verilog_sva_sequence_typet{}};
+    };
+
+    auto weak = [](const exprt &expr) {
+      return sva_weak_exprt{ID_sva_weak, expr};
+    };
+
+    REQUIRE(trivial_sva(weak(seq(p))) == p);
+
+    REQUIRE(
+      trivial_sva(weak(sva_and_exprt{
+        sva_and_exprt{seq(p), seq(q), sequence_type}})) == and_exprt{p, q});
+
+    // The below fails
+    // REQUIRE(trivial_sva(weak(sva_and_exprt{sva_and_exprt{p_seq, sva_or_exprt{q_seq, r_seq, sequence_type}, sequence_type}})) == and_exprt{p, or_exprt{q, r}});
+  }
+}