Speedup "substitute" function

[computereasy]

Dear all,

Sorry I closed issue #808 since after some profiling I figured out the dominator of the performance penalty is the substitute method. I pasted a screen capture of my profiling results, after running around 20 mins of our tool.

As you can see from the figure below, the com.microsoft.z3.Native.INTERNALsubstitute method takes almost 90% of the total execution time. Note that since our tool can actually run for hours or days, I can expect the substitute function would eventually takes almost 100% of the execution time..

So given a path condition (e.g, symbol1 * 4 + symbol2*2 + 12 > 0) what I am trying to do is 1) collect all the symbols in the formula (i.e., symbol1 and symbol2 for this case) 2) substitute each with a fresh symbol and produce a new formula (e.g., substitute sym into sym_new, and the sample formula would become symbol1_new * 4 + symbol2_new * 2 + 12 > 0) 3) put both original and the new formula into the solver to check the satisfiability regarding those symbols. Note that the number of path condition formulas could be over hundreds.

My Scala code for the above procedure is shown below: Note that variable sbl is the list of each symbol and corresponding fresh new symbol, for example, sbl = List(("symbol1", "symbol1_new"), ("symbol2, symbol2_new")). This list is built in the `build_symbol_pair' function.

 def add_path_conditions(m: Solver, pcs: List[BoolExpr], sbl:  List[(BitVecExpr, BitVecExpr)], en: Engine) = {
    pcs.foreach { (pc) =>
      m.add(pc.asInstanceOf[BoolExpr])
      val pc1: Expr = sbl.foldLeft(pc.asInstanceOf[Expr]) { (pc0, sb) => pc0.substitute(sb._1, sb._2) }
      m.add(pc1.asInstanceOf[BoolExpr])
    }
  }

def build_symbol_pair(en: Engine, kl: List[BitVecExpr]): List[(BitVecExpr, BitVecExpr)] = {
    kl.map(k =>
      (k, en.ctx_z3.mkBVConst(k.toString + "_new", k.getSortSize))
    )
 }

Conceptually, I don't see any obvious issue with the above code, besides each time substitute one symbol may not be the most efficient way. But it seems that currently the substitute function is just quite slow for some reason..

So I am writing to ask, given my situation (i.e., substitute one or multiple symbols), is there any way that can speed up the substitution process? I would really appreciate for any advice and suggestion. Thank you!

[computereasy]

I tried to "cache" the already substituted new formulas. The performance is improved. I paste the current profiling results after running our tool for around 25 mins.

As you can see, currently 75% of the processing time is from the substitution procedure above. Actually we have another usage of substitute method, and it takes around 5%. The check function of z3 takes another 5%. In sum, those three procedures together take around 85% of the processing time.

So besides caching the already substituted formulas, is there any way I can speedup the procedure? Thank you!

[wintersteiger]

Yes, calling substitute repeatedly with only one substitution to perform instead of many of them at the same time, will indeed be slower, so that's definitely worth trying.

Apart from that, you may want to consider building those terms bottom-up by yourself instead of using calls to Expr.substitute Every call to substitute will definitely take at least one traversal of the whole expression, while you may be able to build them incrementally, in smaller pieces.

To gauge the cost it may be helpful for you to take a look at our implementation of the substitution: it's in expr_safe_replace.cpp.

[nunoplopes]

You can also use index variables (numbered, no name) and do a replace over those (Z3_substitute_vars). It's much faster! (dunno id this API is exposed in .Net). Of course, you should still batch substitutions and do all of them in one go.

[computereasy]

@nunoplopes Thank you for your reply. So here is something I never figured out... How should I "batch" the substitutions? It seems to me that the substitute API replace one variable at a time...

[nunoplopes]

According to your stack trace, Java API exposes the substitute function taking arrays of Exprs. Maybe these are not exported to Scala.. But Z3 supports that. Also note the difference between the substitution of expr->expr and from integer->expr (what I mentioned in my previous comment).

[wintersteiger]

Yes, there is also SubstituteVars which implements the substitution in a different way. I wouldn't expect it to be generally more efficient though.

The Java API exposes these:

public Expr substitute(Expr[] from, Expr[] to)
public Expr substitute(Expr from, Expr to)
public Expr substituteVars(Expr[] to)

(scala uses the Java API)

[computereasy]

@wintersteiger @nunoplopes Thank you so much your your information. I tried with the "batched" solution and it works good in my situation.

Actually before the optimization, there are three bottlenecks in my tool:

1) collect symbols from a formula, I implemented a procedure similar to this one And my profiling results show that it consumes around 10% of the total processing time.

2) the substitute procedure above: it takes around 75% time of the total execution.

3) the check of z3: it takes around 1.5% of the total time.

After I employ the batched substitution, the overall performance is notably improved, and at this time:

1) collect symbols from a formula: takes around 47% of the total time.

2) substitute: around 12% of the total time.

3) check: 6%.

This results look good to me. I guess it's time to switch back on the functionality tests:)

Again, thank you so much for your help! Wish you all the best!!