Satisfiability modulo injectivity ?

[Claude Marché]

Hello SMTLIB list,

I wonder what would be the best practice for modeling in SMTLIB, and
efficiently solve, problems involving a function known to be injective.
That is something like

(declare-sort A B)
(declare-fun f (A) B)
(assert (forall ((x A) (y A)) (=> (= (f x) (f y)) (= x y)))

With a quick search on the web I found

https://rise4fun.com/Z3/tutorial/guide

where a trick is proposed to avoid a quadratic explosion of quantifier
instanciation, by introducing a converse function

(declare-fun g (B) A)
(assert (forall ((x A)) (= (g (f x)) x)))

I also found a paper about datatypes

https://www.ijcai.org/Proceedings/16/Papers/631.pdf

where the handling of injectivity of constructors is considered.

Generally speaking, it seems to me that an SMT solver could efficiently
handle injectivity if it was natively supported in its congruence
closure engine. Are there any theoretical studies about this?
implementations?


To be complete, my problem specifically concerns the modeling of finite
intervals of integers. Say if one wants to model the type of integers
between 17 and 42, one could write

(declare-sort I)
(declare-fun toint (I) Int)
(assert (forall ((x I)) (and (<= 17 (toint x)) (<= (toint y) 42)

but what would be the best way to express injectivity?

Thanks in advance for any advice

- Claude




--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex |

[Viktor Kunčak]

Dear Claude,

Since you are adding quantified axioms anyway, it looks like what you
need is understanding in terms of specific internal aspects of
solvers.
The solvers also need to be good in taking care of cardinalities of sorts.

I look forward to responses from people implementing SMT solvers.

Since you mention intervals, and I know this may not be what you are
looking for, but some theoretical analysis of specific decision
procedures of first-class intervals as sets was in a paper
accompanying my keynote, where there are intervals but you also have
their length as well as min and max (and Q.F. BAPA):

http://lara.epfl.ch/~kuncak/papers/KuncakETAL10OrderedSetsinCalculusofDataStructures.pdf
(Section 4)

We also wrote a prototype implementation of this decision procedure in
Scala somewhere. The case of only integers and only intervals should
be simpler than the logic in that paper where we tried to be as
general as we could while staying in NP.

An interval S is a subset of integers where not only

card(S) <= max(S) - min(S) + 1

but actually

card(S) == max(S) - min(S) + 1

This should give encoding into that logic.

Best regards,

Viktor

> --
> 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/12542a61-9103-0968-bbf4-24849c6edfbc%40inria.fr.
> For more options, visit https://groups.google.com/d/optout.

[Cesare Tinelli]

Hi Claude,

The best way to express injectivity of a user-defined function in SMT-LIB would be to add a qualifier to its declaration. To you use your example, something like:

  (declare-sort I)
  (declare-fun toint (I) Int :injective)

This way, it would be let to solver how to implement the injectivity constraint. However, adding qualifiers like above to function declarations is not allowed currently in the SMT-LIB standard. As I recall, there was some discussion a long time ago on this possible feature but no agreement. The main issue is that such qualifiers effectively make the problem a quantified one because EUF solvers typically do not have built-in support for injectivity or similar properties.

I agree that supporting injectivity constraints would not be too difficult in practice, but as usual there are trade-offs to consider when adding a new functionality. As I understand it, Z3's EUF solver does actually support injectivity constraints, at least internally, in order to reason about constructors of (algebraic) datatypes but it does not extend that to user-defined function symbols.

Z3's developers, please correct me if I am wrong.

The IJCAI paper you refer to describes a calculus and decision procedure for co-datatypes obtained as a modification of one for datatypes implemented in CVC4. In both cases (datatypes and co-datatypes), the procedure is implemented as a separate theory solver from the EUF solver. That said, many of CVC4's theory solvers (e.g., EUF, ADTs, strings, sets, relations) are actually built on top of the same core congruence closure library. So adding a theory of injective functions would not require a big effort in CVC4, at least for input sorts with no cardinality restrictions: it would amount to creating a solver that performs theory propagations of the form f(x) = f(y) ---> x = y to the CC core. In case of finite input sorts, however, one has also to take care of propagating finite cardinality constraints, as Viktor mentions in his reply, which gets a little trickier. This complication, however, is not specific to injective functions. For instance, it occurs also for arrays with finite index sort.

To come to your final question, the best way to express injectivity at the moment is probably to use the trick described in the Z3 tutorial because pretty much all SMT solvers that support quantifiers use some form of E-matching.

It'd be interesting to hear from other developers though.


Cesare