Merge pull request #1233 from diffblue/buechi-sequence_first_match

SVA->Buechi: implement `first_match(...)` sequence operator

Author: tautschnig

regression/ebmc-spot/sva-buechi/sequence_first_match1.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence_first_match1.sv
+--buechi --k-induction --bound 1
+^\[.*\] first_match\(main\.x == 0\): PROVED$
+^\[.*\] first_match\(main\.x == 0, main\.x\+\+\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_first_match1.k.desc

@@ -1,13 +1,12 @@
 CORE
 ../../verilog/SVA/sequence_first_match2.sv
---buechi --bound 5
-^error: failed to convert sva_sequence_first_match$
-^EXIT=6$
-^SIGNAL=0$
---
+--buechi --k-induction --bound 2
 ^\[.*\] \(\(##1 1\) or \(##2 1\)\) \|-> main.x == 1: REFUTED$
-^\[.*\] first_match\(\(##1 1\) or \(##2 1\)\) \|-> main\.x == 1: PROVED up to bound 5$
+^\[.*\] first_match\(\(##1 1\) or \(##2 1\)\) \|-> main\.x == 1: PROVED$
 ^\[.*\] \(1 or \(##1 1\)\) \|-> main\.x == 0: REFUTED$
-^\[.*\] first_match\(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED up to bound 5$
+^\[.*\] first_match\(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
 ^warning: ignoring
 --

…ot/sva-buechi/sequence_first_match2.desc …/sva-buechi/sequence_first_match2.k.descregression/ebmc-spot/sva-buechi/sequence_first_match2.desc renamed to regression/ebmc-spot/sva-buechi/sequence_first_match2.k.desc regression/ebmc-spot/sva-buechi/sequence_first_match2.desc renamed to regression/ebmc-spot/sva-buechi/sequence_first_match2.k.desc

@@ -541,6 +541,13 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
       DATA_INVARIANT(
         false, "unexpected sva_sequence_non_consecutive_repetition");
   }
+  else if(expr.id() == ID_sva_sequence_first_match) // first_match(...)
+  {
+    PRECONDITION(mode == SVA_SEQUENCE);
+    auto &sequence = to_sva_sequence_first_match_expr(expr).sequence();
+    auto op_rec = rec(sequence, SVA_SEQUENCE);
+    return resultt{precedencet::ATOM, "first_match(" + op_rec.s + ')'};
+  }
   else if(!is_temporal_operator(expr))
   {
     auto number = atoms.number(expr);