Unit tests for trivial_sva(...)

This adds unit tests for the trivial_sva(expr) simplification.

Author: kroening

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,70 @@
+/*******************************************************************\
+
+Module: Trivial SVA
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+//#include <util/arith_tools.h>
+//#include <util/mathematical_types.h>
+
+//#include <temporal-logic/ltl.h>
+#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{}};
+    };
+
+    auto p_prop = prop(p);
+    auto q_prop = prop(q);
+    auto r_prop = prop(r);
+
+    REQUIRE(trivial_sva(sva_not_exprt{p_prop}) == not_exprt{p_prop});
+    REQUIRE(
+      trivial_sva(sva_not_exprt{sva_and_exprt{p_prop, q_prop, bool_typet{}}}) ==
+      not_exprt{and_exprt{p_prop, q_prop}});
+    REQUIRE(
+      trivial_sva(sva_and_exprt{sva_not_exprt{p_prop}, q_prop, bool_typet{}}) ==
+      and_exprt{not_exprt{p_prop}, q_prop});
+    REQUIRE(
+      trivial_sva(sva_and_exprt{
+        sva_or_exprt{p_prop, q_prop, bool_typet{}}, r_prop, bool_typet{}}) ==
+      and_exprt{or_exprt{p_prop, q_prop}, r_prop});
+  }
+
+  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 p_seq = seq(p);
+    auto q_seq = seq(q);
+    auto r_seq = seq(r);
+
+    auto weak = [](const exprt &expr) {
+      return sva_weak_exprt{ID_sva_weak, expr};
+    };
+
+    REQUIRE(trivial_sva(weak(p_seq)) == p);
+
+    REQUIRE(
+      trivial_sva(weak(sva_and_exprt{
+        sva_and_exprt{p_seq, q_seq, 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}});
+  }
+}