choiceof expression

[Nuno Lopes]

Hi,

I've been coming across the need of a new "choiceof" expression several
times.
The idea is that given a list of pairs (value, condition), the expression
returns any of the values for which the condition holds. If none of the
conditions holds, the expression's value is undefined. The conditions don't
have to be disjoint.

For example:
(choiceof (x (= x y)) (3 (bvule x y)) (0 (= y 42)))

This expression may yield either x, 3, or 0. Or a subset of these depending
on whether the respective conditions hold in the model.

If I have something like:
(assert (= x (choiceof (x (= x y)) (3 (bvule x y)) (0 (= y 42)))))

Models that satisfy this constraints respect *at least one* of the following
constraints:
- (= x y)
- (= x 3) and (bvule x y)
- (= x 0) and (= y 42)

For now I've been encoding this with ite expressions plus a quantified
variable. I was wondering if any SMT solver out there has native support for
something similar?
Have others come across the necessity of a similar construct? (just
wondering if it would be useful to make it standard in smt-lib)

Thanks,
Nuno

[Tim King]

Double checking I understand the proposal:

> If none of the conditions holds, the expression's value is undefined. 

Wouldn't there be a 4th case for:

> (assert (= x (choiceof (x (= x y)) (3 (bvule x y)) (0 (= y 42)))))

- A "no matches" case where (not (= x y)), (not (bvule x y)), (not (= y 42)) and choiceof is undefined.

There is then a question of what the value of the choiceof is for the no matches case.

Given the syntax, I am guessing that the intention is for choiceof to be a function that goes from (A Bool)+ to A. Model assignments for this would need to be consistent. So I think there would also probably need to be some (= x <skolem>) condition where <skolem> is some type of skolem term for choiceof to handle congruence. (This is the div by 0 argument yet again.) Basically you need a consistent model assignment for the choiceof term so that:

  (assert (= x1 (choiceof (z1 b1))

  (assert (= x2 (choiceof (z2 b2))

  (assert (= z1 z2))

  (assert (= b1 b2))

  (assert (not (= x1 x2)))

is unsat.

Best,

Tim

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/000501d69b4a%24008a09e0%24019e1da0%24%40ist.utl.pt.

[Martin Nyx Brain]

On Mon, 2020-10-05 at 20:01 +0100, Nuno Lopes wrote:
> Hi,
>
> I've been coming across the need of a new "choiceof" expression
> several
> times.
> The idea is that given a list of pairs (value, condition), the
> expression
> returns any of the values for which the condition holds. If none of
> the
> conditions holds, the expression's value is undefined.

Undefined is not really a concept in SMT-LIB. Do you mean that if none
of the conditions hold then the result can be any value of the
appropriate sort?


<snip helpful example>

> For now I've been encoding this with ite expressions plus a
> quantified
> variable.

Is the semantics you want the same as this?

(ite (and NONDET_BOOL_1 (= x y)) x
(ite (and NONDET_BOOL_2 (bvule x y)) 3
(ite (and NONDET_BOOL_3 (= y 42)) 0
NONDET_VALUE_SORT)))

> I was wondering if any SMT solver out there has native support for
> something similar?

What kind of support do you want, just syntactic or is there something
specific you want solvers to do when given this construct?

Cheers,
- Martin

[Nuno Lopes]

> Double checking I understand the proposal:

>> If none of the conditions holds, the expression's value is undefined. 

> 

> Wouldn't there be a 4th case for:

> (assert (= x (choiceof (x (= x y)) (3 (bvule x y)) (0 (= y 42)))))

> - A "no matches" case where (not (= x y)), (not (bvule x y)), (not (= y 42)) and choiceof is undefined.

 

Right!

 

 

> There is then a question of what the value of the choiceof is for the no matches case.

 

For my case, it doesn’t matter, because the constraints guarantee that case isn’t observed. It can be any of the input values, for example.

BTW, since you mention udiv, I use Z3’s option to ignore the division by zero case, as it never happens with my constraints. I would rather get a warning from the solver saying I’m relying on the division by zero case (best effort) since that’s a bug in the encoding than having solving slowed down with that case being encoded with an UF internally (like Z3 does). I would be surprised if anyone relies on the SMT’s division by zero semantics.

 

 

> Given the syntax, I am guessing that the intention is for choiceof to be a function that goes from (A Bool)+ to A. Model assignments for this would need to be consistent. So I think there would also probably need to be some (= x <skolem>) condition where <skolem> is some type of skolem term for choiceof to handle congruence. (This is the div by 0 argument yet again.) Basically you need a consistent model assignment for the choiceof term so that:

>   (assert (= x1 (choiceof (z1 b1))

>   (assert (= x2 (choiceof (z2 b2))

>   (assert (= z1 z2))

>   (assert (= b1 b2))

>   (assert (not (= x1 x2)))

> is unsat.

 

Yes, exactly!

As I mentioned, I can encode this right now with a quantified variable + a couple of ITEs, but having a “choiceof” operator would allow the solver to preprocess the formula much more easily.

This is somewhat close to a UF, but where the expression may yield more than one value for the same input. This is important for applications that encode refinement rather than equivalence.

 

Thanks,

Nuno

 

 

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAJ3tPC67TYpFxk6cP1s2c3wP9DBZ1bqt-poUbEnM_R0fPmH3cg%40mail.gmail.com.

[Calvin Loncaric]

I have written a lot of tools that output SMT-LIB formulas, and the proposed "choiceof" construct would have simplified many of them.

That said, I DON'T think this construct should be added to SMT-LIB. First, it can be easily encoded without quantifiers, at the cost of a little complexity for whatever person or tool is writing the formula. For example, your assertion

(assert (= x (choiceof (x (= x y)) (3 (bvule x y)) (0 (= y 42)))))

could be written by introducing a new skolem variable (as Tim hinted):

(declare-const choice ...)

(assert (= x choice))

(assert (or

    (and (= choice x) (= x y))

    (and (= choice 3) (bvule x y))

    (and (= choice 0) (= y 42))

    (and (not (= x y)) (not (bvule x y)) (not (= y 42)))

))

Note that the last (or) case is there to say "there are no constraints on `choice` if none of the conditions hold".

I am fine with the extra complexity, since I think of SMT-LIB as an "assembly language" of sorts. I'm happy to let a computer program build complex constructs like that one for me when it has to.

Second, and more importantly, there are some very subtle problems associated with adding undefinedness to expressions. Tim touched on this. In SMT-LIB, it is always true that `(= E E)` for any expression E. But is it always true that `(= (choiceof (0 false)) (choiceof (0 false)))`? The expression `(choiceof (0 false))` is "undefined", and it isn't obvious if the first choiceof is allowed to choose something different than the second choiceof. If they can choose different things, then `(= E E)` might sometimes be false! Adding a fresh variable for every lexical occurrence of "choiceof" takes undefinedness out of the equation, and makes what is happening painfully explicit.

Note that today, no expressions in SMT-LIB are undefined. Even division by zero is defined! See the notes in the definition of the Reals theory (http://smtlib.cs.uiowa.edu/theories-Reals.shtml).

If you are interested in some reading, the closest thing I have seen is the "choose" operator in TLA+ (another formal language). TLA+'s "choose" is essentially Hilbert's epsilon operator in disguise. See also Epsilon Calculus (https://en.wikipedia.org/wiki/Epsilon_calculus). Lamport gives a great description of it in section 6.6 of Specifying Systems (https://lamport.azurewebsites.net/tla/book-02-08-08.pdf). In particular, he writes:

> People who do a lot of programming and not much mathematics often think that choose must be a nondeterministic operator. In mathematics, there  is no such thing as a nondeterministic operator or a nondeterministic function.

He clarifies formally how this is possible in section 16.1.2 by giving some axioms for "choose". However, the axioms of "choose" are incredibly difficult for solvers to work with. For a practical description of the challenges, see the 2016 tech report "Compiling Hilbert's Epsilon Operator" by Rustan Leino (https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml252.pdf)

--

Calvin

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAJ3tPC67TYpFxk6cP1s2c3wP9DBZ1bqt-poUbEnM_R0fPmH3cg%40mail.gmail.com.

[Nuno Lopes]

>> I've been coming across the need of a new "choiceof" expression
>> several times.
>> The idea is that given a list of pairs (value, condition), the
>> expression returns any of the values for which the condition holds. If
>> none of the conditions holds, the expression's value is undefined.
>
> Undefined is not really a concept in SMT-LIB. Do you mean that if none of the conditions hold then the result can be any value of the appropriate sort?

Yes.

> <snip helpful example>
>> For now I've been encoding this with ite expressions plus a quantified
>> variable.
>
> Is the semantics you want the same as this?
>
> (ite (and NONDET_BOOL_1 (= x y)) x
> (ite (and NONDET_BOOL_2 (bvule x y)) 3
> (ite (and NONDET_BOOL_3 (= y 42)) 0
> NONDET_VALUE_SORT)))

Not exactly. One of the input values whose conditions holds must be picked. This formula always allows the expression to take the value NONDET_VALUE_SORT.
But it's close to that, agreed.

>> I was wondering if any SMT solver out there has native support for
>> something similar?
>
> What kind of support do you want, just syntactic or is there something specific you want solvers to do when given this construct?

Can be syntactic, but hopefully a bit more. Dedicated pre-processing rules would be helpful.

Thanks,
Nuno

[Nuno Lopes]

Of course there’s a tradeoff between what SMT solvers should support and what’s the job of the application. SMT solver builders want the smallest possible language, while SMT solver users want the largest.. The truth is somewhere in between, but we need to make sure that it’s sufficiently large such that we don’t have everybody reinventing the wheel all the time in their applications.

 

I do run my fair share of SMT queries (many thousands every single day), and I feel there’s no forum where SMT solver builders & users can meet to discuss the SMT-LIB language. There are some parts of SMT-LIB that need improvement (e.g., FPA, arrays, UFs) and I don’t know where/if round tables between the different stakeholders occur.

 

Thanks,

Nuno

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CABf5HMjyXYDi98e7G8duDKYtBXRreVpDNy3FgUHJjiVKYvSDiA%40mail.gmail.com.

[Tim King]

> This is somewhat close to a UF, but where the expression may yield more than one value for the same input. This is important for applications that encode refinement rather than equivalence.

I don't think you will have much luck having choiceof be an (A Bool)+ -> A function (/family of functions) and not smuggle in congruence. As Calvin mentioned, `(= E E)` is the expectation for terms in SMT-LIB. (In particular, you are up against Definition 6 (Σ-structure) in SMT-LIB v2.6 having total functions.)

Here are alternatives that could plausibly get around this:

- Introduce a command (choose v (_ BitVec 8) ( (x (= x y)) (3 (bvule x y)) (0 (= y 42))) that is syntactic sugar for Calvin's suggestion:

(declare-const v (_ BitVec 8))

(assert (or

    (and (= v x) (= x y))

    (and (= v 3) (bvule x y))

    (and (= v 0) (= y 42))

    (and (not (= x y)) (not (bvule x y)) (not (= y 42)))

))

- Expand the signature with another argument say C to become C,(A Bool)+ -> A. C could be a new Sort with a numeral "constructor" (_ C n) that constructs distinct C values. You can then write `(choiceof (_ C 1) (x (= x y)) (3 (bvule x y)) (0 (= y 42))) `. Assigning a different n value at each location would make each choice flexible. Solver authors still need to handle congruence. If used against distinct constants, this should be cheap to solve in practice. (If C was instead parametric, one can also just use Int or BitVec constants. [You could also have a family of choiceof functions (_ choiceof n), but basically the same idea.])

- Make choiceof a macro that creates a fresh skolem constant at each location.

FWIW I am opposed to the last suggestion. It is going to introduce complexity to the standard and IMO be confusing. (= E E) might not hold pre-macro expansion while (= E' E') would hold post macro expansion. (Also E would not be a "term", but a "pre-term" or something?) This seems strictly more confusing than requiring in-order traversal to support :named. (Section 4.1.6 in the standard for those unfamiliar.) A higher level language could support macros like this though.

Best,

Tim

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/002a01d69da1%247891e0d0%2469b5a270%24%40ist.utl.pt.

[Martin Nyx Brain]

On Thu, 2020-10-08 at 19:33 +0100, Nuno Lopes wrote:
> Of course there’s a tradeoff between what SMT solvers should support
> and what’s the job of the application. SMT solver builders want the
> smallest possible language, while SMT solver users want the largest..

I'm not sure that builders want the smallest TBH...

> The truth is somewhere in between, but we need to make sure that it’s
> sufficiently large such that we don’t have everybody reinventing the
> wheel all the time in their applications.

Yes; that is definitely a design goal.

> I do run my fair share of SMT queries (many thousands every single
> day), and I feel there’s no forum where SMT solver builders & users
> can meet to discuss the SMT-LIB language.

That is a big part of the point of this mailing list. Please do post
what you think!

> There are some parts of SMT-LIB that need improvement (e.g., FPA,
> arrays, UFs) and I don’t know where/if round tables between the
> different stakeholders occur.

Back when we could be physically co-located, that was one of the aims
of the SMT workshop.

Cheers,
- Martin

[Calvin Loncaric]

Somebody just called to my attention that a "choose" operator is actually planned for SMT-LIB version 3:

http://smtlib.cs.uiowa.edu/version3.shtml

I am not sure if any of the standard authors have more up-to-date information about this, but would be an exciting addition.

--

Calvin

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/c2ff3ef215979713928cdbc5a77a3064c2a6d120.camel%40cs.ox.ac.uk.

[Nuno Lopes]

Nice to hear that, thanks for the pointer!
Nuno

-----Original Message-----
From: Calvin Loncaric
Sent: Wednesday, October 28, 2020 12:29 AM
To: smt...@googlegroups.com
Subject: Re: [smt-lib] choiceof expression

[Martin Nyx Brain]

On Tue, 2020-10-27 at 17:29 -0700, Calvin Loncaric wrote:
> Somebody just called to my attention that a "choose" operator is
> actually
> planned for SMT-LIB version 3:
> http://smtlib.cs.uiowa.edu/version3.shtml

There is but I am not sure that it has quite the semantics that was
originally desired.

> I am not sure if any of the standard authors have more up-to-date
> information about this, but would be an exciting addition.

As far as I know, that page is the most up-to-date information on SMT-
LIB 3.0.

Cheers,
- Martin