Generate BMC style functional equivalence checking queries

[FedericoAureliano]

The clever generator simulates bounded model checker client-specific equivalence queries. In particular, the generator produces:

• a client that calls a library n times
• two different versions of the library
• an assertion that is violated if the client calling the old library differs from the client calling the new library

The three functions are trees of IfThenElseNodes of configurable depth. Leafs of the tree are non-IfThenElse-expressions of configurable depth.

See the example below.

stringfuzzg clever --client-depth 2 --lib-depth 2 --expr-depth 1
;BEGIN STRINGFUZZ STATS
; max_client_depth 2
; num_client_vars 3
; max_lib_depth 2
; num_lib_vars 2
; num_lib_calls 1
; max_expr_depth 1
; lowest_lib_call_depth 1
;END STRINGFUZZ STATS
(declare-fun var0 () Bool)
(declare-fun var1 () Int)
(declare-fun var2 () Int)
(define-fun old_lib ((arg3 Int) (arg4 String)) Int (ite (> 5 arg3) (ite (<= 1 arg3) (str.len arg4) (str.len arg4)) (ite (> arg3 arg3) (str.indexof arg4 arg4 arg3) (str.len "P{\\=0;""Gv~"))))
(define-fun new_lib ((arg3 Int) (arg4 String)) Int (ite (or true true) (str.indexof arg4 arg4 arg3) (str.len arg4)))
(define-fun client_old ((arg0 Bool) (arg1 Int) (arg2 Int)) Int (ite (> arg1 arg2) (str.indexof "]gj4a`(^O{" "%ur].R-zV""" arg2) (old_lib (str.indexof "9?CITn7#X5" "`OpxJ~Y+l`" arg1) (str.replace "wf/U\\m1Y^Q" "$D@JN[wj*_" "aG5(zhuZJ;"))))
(define-fun client_new ((arg0 Bool) (arg1 Int) (arg2 Int)) Int (ite (> arg1 arg2) (str.indexof "]gj4a`(^O{" "%ur].R-zV""" arg2) (new_lib (str.indexof "9?CITn7#X5" "`OpxJ~Y+l`" arg1) (str.replace "wf/U\\m1Y^Q" "$D@JN[wj*_" "aG5(zhuZJ;"))))
(assert (not (= (client_old var0 var1 var2) (client_new var0 var1 var2))))
(check-sat)

[dblotsky]

@FedericoAureliano heyoo, is this PR still relevant?

[FedericoAureliano]

This was useful for an experiment I ran. It is no longer useful. We can delete.