string sort performance

[komalb007]

Hi NikolajBjorner,

I was using using 4.4.1 version before which was not supporting String sort so we converted that to integer internally in our code and passed as Integer sort Now we have upgraded to 4.8.4 and passing string asserts as String sort itself.

But I am seeing some serious performance issue. Is it expected to see performance difference between Integer and string sort? If yes what % of regression are we talking about here?

Thank,

[NikolajBjorner]

Not sure what to make of this: do you have a specific instance that really requires string reasoning? Or if it doesn't you use strings in a benign way, but Z3 does not treat it as benign. This could be a case where the solver could be tuned to such benign cases, but generally don't use strings if you don't really require them.

[chauhansantosh17]

Hello Nikolaj,

Komalb007 and me are colleage.

Let me add more background for the problem that Komalb007 reported above.

Our requirement to have mutually exclusive relation between string values. For example, consider a string variable with Color which can have three possible values - Red, Green and Blue. Let's say we have one constraint that says enforce Color=Red whenever a certain condition is met. In this discussion lets represent that condition by input1 Boolean flag With this data, input expression "input1 AND Color=Blue" should be invalid however, "input1 OR Color=Blue" should be valid.

With Z3 version 4.4.1, the above requirement was modeled using Int sort and some book keeping in local environment.

smt2 representation of our modeling with Z3 version 4.4.1

(declare-const color Int) (declare-const input1 Bool) (assert (or (= color 1) (= color 2) (= color 3))) (assert (implies input1 (= color 1))) ; this simulates a business rule which say if input1 is true then enforce Color=1(Red) (push) (assert (and input1 (= color 3))) (check-sat) ; this gives unsat because Int color can have only one value (pop) (push) (assert (or input1 (= color 2))) (check-sat) ; this gives sat by assigning 1 to color Int (pop)

The above constraint modeling solves our problem, but it requires us to local book-keeping. The book-keeping is mapping which says color=Red is modelled as color=1 in z3 solver. The z3 model contains integer 1,2,3 and these integers are mapped back to string value by our integration code for our consumers.

With Z3 version 4.8.4, we have string sort support. With this support we are trying to get rid of the book-keeping in local integration code and get the required result directly from z3 model. smt2 representation

(declare-const color String) (declare-const input1 Bool) (assert (or (= color "Red") (= color "Green") (= color "Blue"))) (assert (implies input1 (= color "Red"))) ; this simulates a business rule which say if input1 is true then enforce Color=Red (push) (assert (and input1 (= color "Blue"))) (check-sat) ; this gives unsat because Int color can have only one value (pop) (push) (assert (or input1 (= color "Blue"))) (check-sat) ; this gives sat by assigning Red to color Int (pop)

Our observation is the above two modeling of same problem yeilds functionaly same results, however perfromance wise modeling with z3 version 4.8.4 is slower than the modeling with 4.4.1. Do you see some reasons for this slow performance?

[NikolajBjorner]

Thanks for the example. Yes, the string solver is extremely naive compared to the other solvers. You can use algebraic data-types (which let you create an enumeration sort) for what you do. It is a better fit, or use integers. There is nothing in your constraints that say you have to use strings. Z3's string solver doesn't recognize that the constraints are easily solvable over the base cases "Red", "Green", "Blue" and it tries a brute force method to find solutions to "color".