EBMC: tautology checker

This adds a property tautology check ask the first step to the engine
selection.

While it should be rare that this pass proves a property, the fact that it
does may suggest that the property is unintentionally vacuous.

Author: kroening

src/ebmc/Makefile

@@ -36,6 +36,7 @@ SRC = \
       show_formula_solver.cpp \
       show_properties.cpp \
       show_trans.cpp \
+      tautology_check.cpp \
       transition_system.cpp \
       waveform.cpp \
       #empty line

src/ebmc/property_checker.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include "netlist.h"
 #include "output_file.h"
 #include "report_results.h"
+#include "tautology_check.h"
 
 #include <chrono>
 #include <iostream>
@@ -382,7 +383,22 @@ property_checker_resultt engine_heuristic(
   message.status() << "No engine given, attempting heuristic engine selection"
                    << messaget::eom;
 
-  // First check whether we have a low completenes threshold
+  // First check if we can tell that the property is a tautology
+  message.status() << "Tautology check" << messaget::eom;
+
+  auto tautology_check_result =
+    tautology_check(cmdline, properties, solver_factory, message_handler);
+
+  properties.properties = tautology_check_result.properties;
+
+  if(!properties.has_unfinished_property())
+    return tautology_check_result; // done
+
+  properties.reset_failure();
+  properties.reset_inconclusive();
+  properties.reset_unsupported();
+
+  // Check whether we have a low completenes threshold
   message.status() << "Attempting completeness threshold" << messaget::eom;
 
   auto completeness_threshold_result = completeness_threshold(