Optimizing an smt query about partial orders

[dwightguth]

I asked this question on Stace Overflow, but then I realized this venue existed and so I am cross posting it here because I'm not sure if everyone here would see it there.

I am working on trying to do type inference in Z3 for a compiler and the compiler generates a Z3 query over a fully defined partial order, and then attempts to find the maximal type for all the variables such that a fixed set of constraints is satisfied.

The query looks something like this:

(declare-datatypes () ((Sort
(|SortInt| )
(|SortExp| )
(|SortKItem| )
(|SortKLabel| )
(|SortK| )
)))
(define-fun <=Sort ((s1 Sort) (s2 Sort)) Bool (or
  (and (= s1 |SortKItem|) (= s2 |SortK|))
  (and (= s1 |SortExp|) (= s2 |SortKItem|))
  (and (= s1 |SortExp|) (= s2 |SortK|))
  (and (= s1 |SortInt|) (= s2 |SortKItem|))
  (and (= s1 |SortInt|) (= s2 |SortExp|))
  (and (= s1 |SortInt|) (= s2 |SortK|))
  (and (= s1 |SortKItem|) (= s2 |SortKItem|))
  (and (= s1 |SortKLabel|) (= s2 |SortKLabel|))
  (and (= s1 |SortExp|) (= s2 |SortExp|))
  (and (= s1 |SortK|) (= s2 |SortK|))
  (and (= s1 |SortInt|) (= s2 |SortInt|))
))
(define-fun <=SortSyntax ((s1 Sort) (s2 Sort)) Bool (or
  (and (= s1 |SortKItem|) (= s2 |SortK|))
  (and (= s1 |SortExp|) (= s2 |SortKItem|))
  (and (= s1 |SortExp|) (= s2 |SortK|))
  (and (= s1 |SortInt|) (= s2 |SortKItem|))
  (and (= s1 |SortInt|) (= s2 |SortExp|))
  (and (= s1 |SortInt|) (= s2 |SortK|))
  (and (= s1 |SortKItem|) (= s2 |SortKItem|))
  (and (= s1 |SortKLabel|) (= s2 |SortKLabel|))
  (and (= s1 |SortExp|) (= s2 |SortExp|))
  (and (= s1 |SortK|) (= s2 |SortK|))
  (and (= s1 |SortInt|) (= s2 |SortInt|))
))
(push)
(declare-const |FreshVarSort_6_8_6_36_#KRewrite| Sort)
(declare-const |VarA| Sort)
(declare-const |VarB| Sort)
(declare-const |VarC| Sort)
(declare-datatypes() ((SolutionVariables (SolVars (|Sol_VarA| Sort) (|Sol_VarB| Sort) (|Sol_VarC| Sort) ))))
(declare-datatypes() ((Solution (Sol (vars SolutionVariables) (|Sol_FreshVarSort_6_8_6_36_#KRewrite| Sort) ))))
(define-fun theSolution () Solution (Sol (SolVars |VarA| |VarB| |VarC| ) |FreshVarSort_6_8_6_36_#KRewrite| ))
(define-fun lt ((s1 Solution) (s2 Solution)) Bool (and true (<=SortSyntax (|Sol_VarA| (vars s1)) (|Sol_VarA| (vars s2))) (<=SortSyntax (|Sol_VarB| (vars s1)) (|Sol_VarB| (vars s2))) (<=SortSyntax (|Sol_VarC| (vars s1)) (|Sol_VarC| (vars s2)))  (distinct (vars s1) (vars s2))))
(assert (and true (distinct (|Sol_FreshVarSort_6_8_6_36_#KRewrite| theSolution) |SortKLabel|) ))
(define-fun |constraint4_SortExp| ((s Solution)) Bool (and true (<=Sort (|Sol_VarA| (vars s)) |SortExp|) ))
(define-fun |constraint6_SortExp| ((s Solution)) Bool (and true (<=Sort (|Sol_VarB| (vars s)) |SortExp|) ))
(define-fun |constraint3_SortExp| ((s Solution)) Bool (and true (<=Sort |SortExp| |SortExp|) (|constraint4_SortExp| s) (|constraint6_SortExp| s) ))
(define-fun |constraint8_SortExp| ((s Solution)) Bool (and true (<=Sort (|Sol_VarC| (vars s)) |SortExp|) ))
(define-fun |constraint2_(Sol_FreshVarSort_6_8_6_36_#KRewrite s)| ((s Solution)) Bool (and true (<=Sort |SortExp| (|Sol_FreshVarSort_6_8_6_36_#KRewrite| s)) (|constraint3_SortExp| s) (|constraint8_SortExp| s) ))
(define-fun |constraint12_SortInt| ((s Solution)) Bool (and true (<=Sort (|Sol_VarA| (vars s)) |SortInt|) ))
(define-fun |constraint14_SortInt| ((s Solution)) Bool (and true (<=Sort (|Sol_VarB| (vars s)) |SortInt|) ))
(define-fun |constraint11_SortInt| ((s Solution)) Bool (and true (<=Sort |SortInt| |SortInt|) (|constraint12_SortInt| s) (|constraint14_SortInt| s) ))
(define-fun |constraint16_SortInt| ((s Solution)) Bool (and true (<=Sort (|Sol_VarC| (vars s)) |SortInt|) ))
(define-fun |constraint10_(Sol_FreshVarSort_6_8_6_36_#KRewrite s)| ((s Solution)) Bool (and true (<=Sort |SortInt| (|Sol_FreshVarSort_6_8_6_36_#KRewrite| s)) (|constraint11_SortInt| s) (|constraint16_SortInt| s) ))
(define-fun |constraint1_Sort#RuleBody| ((s Solution)) Bool (and true (= (|Sol_FreshVarSort_6_8_6_36_#KRewrite| s) |SortK|) (|constraint2_(Sol_FreshVarSort_6_8_6_36_#KRewrite s)| s) (|constraint10_(Sol_FreshVarSort_6_8_6_36_#KRewrite s)| s) ))
(define-fun |constraint0_Sort#RuleContent| ((s Solution)) Bool (and true (|constraint1_Sort#RuleBody| s) ))
(define-fun |constraint21_SortExp| ((s Solution)) Bool (and true (<=Sort |SortExp| |SortExp|) (|constraint6_SortExp| s) (|constraint8_SortExp| s) ))
(define-fun |constraint20_(Sol_FreshVarSort_6_8_6_36_#KRewrite s)| ((s Solution)) Bool (and true (<=Sort |SortExp| (|Sol_FreshVarSort_6_8_6_36_#KRewrite| s)) (|constraint4_SortExp| s) (|constraint21_SortExp| s) ))
(define-fun |constraint19_Sort#RuleBody| ((s Solution)) Bool (and true (= (|Sol_FreshVarSort_6_8_6_36_#KRewrite| s) |SortK|) (|constraint20_(Sol_FreshVarSort_6_8_6_36_#KRewrite s)| s) (|constraint10_(Sol_FreshVarSort_6_8_6_36_#KRewrite s)| s) ))
(define-fun |constraint18_Sort#RuleContent| ((s Solution)) Bool (and true (|constraint19_Sort#RuleBody| s) ))
(define-fun amb0 ((s Solution)) Bool (or (|constraint0_Sort#RuleContent| s) (|constraint18_Sort#RuleContent| s) ))

(assert (amb0 theSolution))
(assert (not (exists ((s Solution)) (and (lt theSolution s) (amb0 s) (distinct (|Sol_FreshVarSort_6_8_6_36_#KRewrite| s) |SortKLabel|) ))))
(check-sat)
(get-model)
(assert (or false (distinct |VarA| |SortInt|) (distinct |VarB| |SortInt|) (distinct |VarC| |SortInt|) ))
(check-sat)
(pop)

This is a smaller query and runs fine. The problem is, when the number of sorts and variables and disjunctions in the constraints increases, z3 starts to take a significant amount of time to solve the constraints. Part of this is because the size of the relations is quadratic, and part of this is due to the existential quantifier being used to assert that the solution is maximal.

What I am wondering is, are there any specific tactics I could use or ways I could refactor the way the query is generated so queries of this type are faster on complex examples?

I can provide a larger query if it would be useful, but it's several hundred kilobytes.

[NikolajBjorner]

You are likely better of writing a user-propagator plugin to z3 that encodes the partial order.
It currently only supports values over Boolean and Bit-vectors so you would have to rewrite your enumeration data-type into bit-vectors.
The user-propagator can encode partial order constraints and enforce assignments.

https://github.com/Z3Prover/z3/tree/master/examples/userPropagator

[NikolajBjorner]

@CEisenhofer - we should add ADT enumeration sorts to supported value assignments.

[dwightguth]

I read the pdf you linked and I want to try to see if I understand what you are suggesting.

Essentially, I can use the user propagator for 3 different things in this example:

1. The blocking constraints added after the first (get-model) can be replaced with a conflict added during the final callback.
2. The maximality assertion can be replaced with a subquery in the final callback checking that the solution is maximal and either recording the solution or propagating the counterexample.
3. The partial order functions can be turned into user functions which we record via the created callback and then manually implement the behavior of via the fixed callback, adding conflicts if the values fixed for the function and its arguments don't match.

If we do all three of these, then the only assertions we actually have to add to the solver are the constraints themselves.

Is my understanding of how to use the user propagator accurate? Does this sound like what you had in mind?

[dwightguth]

Also, one other question: you said this is restricted to boolean and bit vector values. Does this mean that this whole approach would not be viable if our Sort type had parameters? This is not a significant restriction for us at this moment, but it could cause serious problems for us in the future.

[NikolajBjorner]

It is possible to use the user propagator (but not yet for quantifiers from Python) for your example. I may be able to create a sample as an illustration. It does not require the fixed callback and it does not require bit-vectors.

The approach is to

• register all constants and functions of sort "Sort".
• attached the equality event handler. You get callbacks when equalities between variables of type "Sort" are equal.
• create an incremental union-find to track equalities with constructors
• register the declarations for <=Sort and <=SortSyntax.
• When <=Sort, <=SortSyntax are assigned to true, add an edge to a graph. When assigned to false remember this on the side.
• Also, when assigned to true/false check if there is an immediate conflict with the union-find information about the arguments and the static graph that defines the partial order.

Before doing that, I would suggest trying out a different axiomatization:
replace (define-fun <=Sort ...) by (declare-fun <=Sort ... without the equations)
For each pair of enumeration constructors (s1, s2) of type Sort x Sort assert either

• <=Sort(s1, s2), or
• (not (<=Sort(s1,s2))
  You still get an O(n^2) overhead which the user propagator avoids, but at least you avoid O(n^2) equations for every occurrence of <=Sort.

[dwightguth]

So, I tried the axiomatization you suggested. It's actually a lot slower (on the example I profiled, it jumped from like 300 milliseconds to 40 seconds). I suspect the reason is that the number of sorts is very high (243 in the example I specifically profiled), but the number of edges in the graph is actually pretty small, so having to explicitly add an assertion between every two nodes that aren't connected increases the size of the state from like 2000 edges to something like 118k assertions. I'll try coming to grips with what you suggested for the user propagator, but I thought I'd share my results with your first suggestion in case you happen to know anything else that might help.

[NikolajBjorner]

I added a tutorial example

https://microsoft.github.io/z3guide/docs/Programming%20Z3/Using%20Z3%20from%20Python/User%20Propagator

[dwightguth]

Thanks! This is very helpful and definitely fills in the gaps of my understanding of the solution.