search

dblotsky / stringfuzz

Fuzzer and generator for string and regex problems in SMT-LIB 2.x format.
Other
20 stars 9 forks source link

adding merge transformer #29

Closed FedericoAureliano closed 6 years ago

FedericoAureliano commented 6 years ago

Example without renaming

stringfuzzg concats > 1.smt
stringfuzzg concats | stringfuzzx rotate | stringfuzzx merge -f2 1.smt

(set-logic QF_S) (declare-fun var4 () String) (declare-fun var6 () String) (declare-fun var2 () String) (declare-fun var1 () String) (declare-fun var0 () String) (declare-fun var5 () String) (declare-fun var3 () String) (assert (= var0 (str.++ var6 (str.++ var5 (str.++ var4 (str.++ var3 (str.++ var2 var1))))))) (assert (= var0 (str.++ var2 (str.++ (str.++ (str.++ (str.++ var1 var3) var4) var5) var6)))) (check-sat)

Example with renaming

stringfuzzg concats > 1.smt
stringfuzzg concats | stringfuzzx rotate | stringfuzzx merge -f2 1.smt --rename

(set-logic QF_S) (declare-fun var01 () String) (declare-fun var21 () String) (declare-fun var42 () String) (declare-fun var31 () String) (declare-fun var62 () String) (declare-fun var52 () String) (declare-fun var22 () String) (declare-fun var41 () String) (declare-fun var32 () String) (declare-fun var12 () String) (declare-fun var02 () String) (declare-fun var61 () String) (declare-fun var51 () String) (declare-fun var11 () String) (assert (= var01 (str.++ var21 (str.++ (str.++ (str.++ (str.++ var11 var31) var41) var51) var61)))) (assert (= var02 (str.++ var62 (str.++ var52 (str.++ var42 (str.++ var32 (str.++ var22 var12))))))) (check-sat)

dblotsky commented 6 years ago

@FedericoAureliano we describe this tool as a separate script, called stringmerge. Would it be a lot of work to split it off into a separate script? Alternatively, I can merge this in, and then split it off into a separate script. Which of those two would you prefer?

FedericoAureliano commented 6 years ago

That's probably way better! I'll split it into a separate script inside this branch and have you review it here.

FedericoAureliano commented 6 years ago

I'm closing this branch and making a new one so that I can use the most recent changes to master, and mostly because the changes i'm going to make are really big so theres no point of it being the same branch.

dblotsky commented 6 years ago

@FedericoAureliano sounds good!