May a solver return "unsat" for this example involving the theory of arrays?

[Calvin Loncaric]

Hi everyone!

Here is an SMT-LIB 2 script that uses the theory of arrays:

(set-logic ALIA)
(declare-const a (Array Int Int))
(assert (forall ((i Int)) (= (select a i) i)))
(check-sat)

Is it legal for a solver to return "unsat" for this input? (I don't know of any solver that does; this is a question about the SMT-LIB standard and not a particular implementation.)

"Unsat" is the correct response if array values are constrained to (1) a "default" array that maps every integer to zero and (2) arrays that can be built using a finite number of applications of (store ...). Constraining arrays in that way is entirely consistent with (my very novice understanding of) the array theory definition and the SMT-LIB semantics.

I would like it to be the case that "sat" and "unknown" are the only legal outputs for this example, but I don't know what (if anything) in the theory of arrays or the SMT-LIB semantics forbids an "unsat" result.

[Clark Barrett]

It would be incorrect for a solver to answer "unsat." The correct
answer is based on the theory definition which does not limit models
to any particular construction. Rather, the theory definition is
axiomatic, and there do exist models for this assertion which satisfy
the array axioms.

-Clark

> --
> 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/5e4e319c-d0ae-42bb-9d86-86fc4e1f1083%40googlegroups.com.

[Calvin Loncaric]

Thanks for the quick response!

Martin Suda followed up with some interesting info as well, which I'm forwarding with permission. I have a followup question below as well.

Hi Calvin,

your example is SAT, because there exists a model of the theory of arrays with an object $a$ in it that behaves like the identity function. What is a bit confusing is that the "negation" (after we unskolemise $a$), i.e.

(set-logic ALIA)
(assert (forall (a (Array Int Int))) ( (exist ((i Int)) (not (= (select a i) i)))))

(check-sat)

is also SAT. In other words, the existence of such array is not guaranteed.

But even the simpler arrays (constant 0 and its finite modifications) you mentioned are not guaranteed to exists in every model of arrays. So even

(set-logic ALIA)
(assert (forall (a (Array Int Int))) ( (exist ((i Int)) (not (= (select a i) 0)))))

(check-sat)

is SAT. These forall claims, however, are much more "esoteric" questions for the current SMT solver technology and I wouldn't be surprised if most of them would time out on them.

P.S. It is never the case that SAT and UNS would both be legal answers!

A somewhat complex followup question:

I am writing a tool that generates proof obligations in SMT-LIB format. It plays a fairly standard trick where it inverts the proof obligation and interprets "unsat" to mean "valid". Proof obligations like "exists a, P(a)" turn into esoteric satisfiability questions just like the ones in Martin's text above, since "not (exists a, P(a)) <-> (forall a, not P(a))".

I would like the tool to have a richer set of array construction primitives than SMT-LIB supports. However, I am very worried that adding such primitives might make the tool unsound if:

• It is possible to prove "not (exists a, P(a))" using the SMT-LIB backend
  
• It is possible to prove "exists a, P(a)" using the richer array construction primitives

From this discussion, I am tentatively concluding that it should be fine, provided that the tool interprets "sat" to mean "not provable" rather than "definitely falsifiable". If the tool interprets "sat" to mean "definitely falsifiable", then it might be possible to prove "not (exists a, P(a))" by observing that "exists a, P(a)" is falsifiable.

Can safely I add additional array construction primitives to my tool?

[Clark Barrett]

Calvin,

I don't fully understand your question. I'm not sure what you mean by
"adding primitives to your tool." I assume you are talking about a
tool built on top of SMT solvers. So adding a primitive could mean
writing an axiom to constrain an uninterpreted function? In that case,
as long as the axioms you write don't introduce a logical
inconsistency, there should be no problem. But maybe you meant
something else?

As far as SMT solvers themselves go, I think you are making things
more complicated than necessary. From the solver's point of view,
there are no "esoteric" questions. Every formula has well-defined
semantics, and the solver will either answer sat, unsat, or unknown
(or not terminate which should also be interpreted as unknown). In no
case should a solver give a "sat" answer when there is not actually a
model or an "unsat" answer when there is a model (unless there is a
bug in the solver of course).

-Clark

> To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CABf5HMhTCxaSYQwFhAwJDWd_pYQbdgC_jThWX%3DGpwwojL-r-hQ%40mail.gmail.com.

[Martin Riener]

Hello everyone,

May I ask a closely related question about the satisfiability of array formulas?
I have the following SMT-lib problem:

(set-logic ALIA)
(assert (not (exists ((a (Array Int Int)))
(forall ((i Int)) (= (select a i) 0 )))))
(check-sat)

Calvin asks if there is a model for the identity array wheras I am asking if
ALIA has a model that does not contain the constant zero array. In my opinion
this should be the case (*) such that an SMT solver should return SAT (or
UNKNOWN) for this problem. Is this correct?

cheers,
Martin




(*) The model construction I have in mind is as follows:

We can use lambda terms to interpret arrays and use the interpretations

I(select)(a,i) = a i
I(store)(a,i,x) = λj. if i = j then x else a j

for the two update functions. Now I construct the domain for (Array Int Int) by
starting with the array λj.1 -- the constant array of 1 -- and close this set
under the three axioms of A. The domain for (Array Int Int) will be extended by
pointwise updates, some of them might be updates with 0.

But the sequence of updates is finite, so for an infinite domain like the
integers, each of such a constructed array a must have some index i such that
one of the values of our starting array appears, i.e. a i = 1 on that position.

Extensionality could put one of our arrays into a congruence with the constant
zero array. This is impossible because each domain element having a in index
that is one is a witness that this cannot be the zero array.

> --
> 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

> <mailto:smt-lib+u...@googlegroups.com>.

> To view this discussion on the web visit
> https://groups.google.com/d/msgid/smt-lib/5e4e319c-d0ae-42bb-9d86-86fc4e1f1083%40googlegroups.com

> <https://groups.google.com/d/msgid/smt-lib/5e4e319c-d0ae-42bb-9d86-86fc4e1f1083%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Calvin Loncaric]

Sorry, I definitely didn't explain my question well.

as long as the axioms you write don't introduce a logical inconsistency, there should be no problem

I am trying to figure out if one particular axiom in my tool could introduce a logical inconsistency. I want to axiomatize this second-order "array construction" primitive:

(assert

  (forall ((f Function))

    (exists ((a Array))

      (forall ((i Int)) (= (select a i) (f i))))))

This axiom is useful because it lets a programmer define all kinds of useful arrays, such as the "zero array" where every element is zero or the "identity array" where every element maps to itself.

Smt-lib doesn't have first-class functions, so the "array construction" axiom has to be instantiated as needed. Specifically, when a programmer writes "makeArray(f)" in the tool, it gets translated into:

(declare-const a Array)

(assert (forall ((i Int)) (= (select a i) (f i))))

However, this approach leads to a big surprise! (Or at least, a surprise for me.) The surprise is that adding those two lines to define "a"---even when the array "a" is not used elsewhere---can flip the solver's result from SAT to UNSAT. Consider:

(set-logic ALIA)

(define-fun f ((x Int)) Int ...)

; (declare-const a (Array Int Int))

; (assert (forall ((i Int)) (= (select a i) (f i))))

(assert (forall ((arr (Array Int Int))) (exists ((i Int)) (not (= (select arr i) (f i))))))
(check-sat)

If I am not mistaken, this query should be SAT without the commented lines, but UNSAT if they are included. I want to believe in my heart that my array construction axiom is true, but there is nothing in the smt-lib arrays theory that requires it.

Question 1: How should my tool interpret the solver's output, when the mere mention of "makeArray" changes the solver's output? The answer, I think, is:

• UNSAT means UNSAT. Adding more "makeArray" terms does will not make the problem satisfiable.
• SAT (from the solver) does not mean SAT (in the extended theory of the tool that includes my array construction axiom). SAT should be interpreted as "unknown". This makes sense: the tool believes in an array construction axiom that it is not able to communicate to the solver, so any model the solver finds may not satisfy the "hidden" array construction axiom.
  

Question 2: Does my array construction axiom create any inconsistencies? I have no idea how to approach this question. I think it does not, but I have no tools at my disposal to prove it.

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

[Clark Barrett]

See answers inline below:

On Thu, Apr 30, 2020 at 11:55 PM Calvin Loncaric <c.a.lo...@gmail.com> wrote:
>
> Sorry, I definitely didn't explain my question well.
>
>> as long as the axioms you write don't introduce a logical inconsistency, there should be no problem
>
>
> I am trying to figure out if one particular axiom in my tool could introduce a logical inconsistency. I want to axiomatize this second-order "array construction" primitive:
>
> (assert
> (forall ((f Function))
> (exists ((a Array))
> (forall ((i Int)) (= (select a i) (f i))))))
>
> This axiom is useful because it lets a programmer define all kinds of useful arrays, such as the "zero array" where every element is zero or the "identity array" where every element maps to itself.
>
> Smt-lib doesn't have first-class functions, so the "array construction" axiom has to be instantiated as needed. Specifically, when a programmer writes "makeArray(f)" in the tool, it gets translated into:
>
> (declare-const a Array)
> (assert (forall ((i Int)) (= (select a i) (f i))))

This seems very reasonable and should be fine, with one caveat - you
would need a fresh symbol "f" for each such array a, otherwise you
could indeed create an unexpected inconsistency.

> However, this approach leads to a big surprise! (Or at least, a surprise for me.) The surprise is that adding those two lines to define "a"---even when the array "a" is not used elsewhere---can flip the solver's result from SAT to UNSAT. Consider:
>
> (set-logic ALIA)
> (define-fun f ((x Int)) Int ...)
> ; (declare-const a (Array Int Int))
> ; (assert (forall ((i Int)) (= (select a i) (f i))))
> (assert (forall ((arr (Array Int Int))) (exists ((i Int)) (not (= (select arr i) (f i))))))
> (check-sat)
>
> If I am not mistaken, this query should be SAT without the commented lines, but UNSAT if they are included. I want to believe in my heart that my array construction axiom is true, but there is nothing in the smt-lib arrays theory that requires it.

That's correct, but why are you surprised? By adding an axiom, you
extend the theory (and thereby reduce the corresponding models), so
there will be some formulas that were satisfiable before but are not
any longer (specifically formulas that contradict your axiom as in the
example above).

> Question 1: How should my tool interpret the solver's output, when the mere mention of "makeArray" changes the solver's output? The answer, I think, is:
>
> UNSAT means UNSAT. Adding more "makeArray" terms does will not make the problem satisfiable.

That's right. Adding constraints can never make something UNSAT become SAT.

> SAT (from the solver) does not mean SAT (in the extended theory of the tool that includes my array construction axiom). SAT should be interpreted as "unknown". This makes sense: the tool believes in an array construction axiom that it is not able to communicate to the solver, so any model the solver finds may not satisfy the "hidden" array construction axiom.

Hmm, I don't think that is right. You *are* communicating the
relevant instances of your array construction axiom, so I think that
if you get SAT, it is really SAT. Even in the "extended theory of the
tool", you would just have one such axiom (with a unique function f)
for each array, and this should never introduce any inconsistency with
an existing formula, since the functions are fresh.

>
> Question 2: Does my array construction axiom create any inconsistencies? I have no idea how to approach this question. I think it does not, but I have no tools at my disposal to prove it.

Given any satisfiable formula, adding an instance of your axiom with a
fresh function symbol f cannot introduce an inconsistency. There is a
simple argument showing that a model for the first formula can be
extended to a model that includes f.

Hope that helps,

-Clark

[Calvin Loncaric]

Thanks for your response, Clark. I want to respond to one of your points, but thinking about these things takes me a while, so I've been slow to get back to you.

You *are* communicating the relevant instances of your array construction axiom, so I think that if you get SAT, it is really SAT.

I still don't think that's true, as demonstrated by the example in my previous email. Here it is again, minus some commented-out lines:

(set-logic ALIA)
(define-fun f ((x Int)) Int ...)

(assert (forall ((arr (Array Int Int))) (exists ((i Int)) (not (= (select arr i) (f i))))))
(check-sat)

If I understand correctly, this input is SAT in SMT-LIB, but it is not SAT if you believe in the second-order array construction axiom I proposed. In SMT-LIB, there might be a model of the arrays theory where no array matches the function f. But in my tool's theory, such an array must exist because of the array construction axiom.

If my tool gets a SAT response from the solver for a problem involving arrays, I think it has to assume that the solver might have produced a model that does not satisfy the array construction axiom. That being the case, I believe it needs to interpret SAT as UNKNOWN.

(This example is very similar to the one in Martin Riener's question from April 30. I'm not sure if anyone got back to him about it, but I'm curious about the answer, since it seems relevant here.)

Thanks!

 

--
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/CAFOm5sS3Vx3ceKDksmyY4dbG8KG_AFCBcK96gYPOC0J0MC5ydg%40mail.gmail.com.

[Clark Barrett]

On Thu, May 7, 2020 at 11:03 AM Calvin Loncaric <c.a.lo...@gmail.com> wrote:

You *are* communicating the relevant instances of your array construction axiom, so I think that if you get SAT, it is really SAT.

I still don't think that's true, as demonstrated by the example in my previous email. Here it is again, minus some commented-out lines:

(set-logic ALIA)
(define-fun f ((x Int)) Int ...)
(assert (forall ((arr (Array Int Int))) (exists ((i Int)) (not (= (select arr i) (f i))))))
(check-sat)

If I understand correctly, this input is SAT in SMT-LIB, but it is not SAT if you believe in the second-order array construction axiom I proposed. In SMT-LIB, there might be a model of the arrays theory where no array matches the function f. But in my tool's theory, such an array must exist because of the array construction axiom.

Ah OK.  I was assuming that you would generate an instance of your second-order axiom for every array variable in your formula (using a fresh function symbol as I described).  If you always do that, then I think you will never get an unexpected result.  Of course, if you don't tell the SMT solver anything about this second-order axiom, then naturally it may find a model that contradicts it.

 

[Calvin Loncaric]

Ah, I think I understand.

The problem is that I need to instantiate the axiom not for all arrays, but for all functions! (I did not explain "instantiated as needed" very well.) If the programmer has written "makeArray(f)", then we know what function to use to instantiate the axiom: for the function "f", there exists a corresponding array. If the programmer doesn't use any "makeArray" terms, then we have very little hope. We could easily require that every array in the formula behaves according to some function, but we can't require that for every function there exists some corresponding array.

...

--

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/CAFOm5sR5GHd%3D%2BC1GxJGS6XnpGP4mctANBm7kL6BM0JjH2aMXrQ%40mail.gmail.com.

[Clark Barrett]

On Thu, May 7, 2020 at 1:11 PM Calvin Loncaric <c.a.lo...@gmail.com> wrote:

Ah, I think I understand.

The problem is that I need to instantiate the axiom not for all arrays, but for all functions! (I did not explain "instantiated as needed" very well.) If the programmer has written "makeArray(f)", then we know what function to use to instantiate the axiom: for the function "f", there exists a corresponding array. If the programmer doesn't use any "makeArray" terms, then we have very little hope. We could easily require that every array in the formula behaves according to some function, but we can't require that for every function there exists some corresponding array.

Actually, you can do exactly that.  Every time you introduce a function symbol, you could also create a fresh array symbol and create the axiom that says that the array behaves like the function.  This should have the same effect as introducing a function symbol for every array.  Am I missing something?

[Calvin Loncaric]

Not every useful function will necessarily appear in the input. This was probably unclear because I expressed my array constraint using a function symbol. Here is a slightly different SMT-LIB input that asks a similar question about arrays without using a function symbol:

(set-logic ALIA)
(assert (forall ((arr (Array Int Int))) (exists ((i Int)) (not (and (>= (select arr i) 0) (<= (select arr i) 0))))))
(check-sat)

This question is SAT for a model where there is no constant-zero array.

For which functions should the tool instantiate the array construction axiom? The identity function (\x -> x) is not a useful choice, but the constant-zero function (\x -> 0) is. I don't think it is possible for the tool to decide which function symbols are useful and which aren't in cases like this one.

--

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/CAFOm5sTkeD435db6_5hba4W4xLk%2BN9e%3Dg4ScXRnsAkFfGo8RCg%40mail.gmail.com.

[Clark Barrett]

Ah - OK I think I finally understand.  You want to only consider models in which all possible arrays exist.  That does not seem to be first-order axiomatizable.  It is second-order axiomatizable, of course, and some SMT solvers (like CVC4) accept higher-order formulas, but I'm pretty sure you would never get a SAT answer as it is really beyond what these solvers can do - you would always get UNKNOWN if it's not UNSAT.  So, in that case, your best bet is to treat SAT as UNKNOWN as you suggested originally.

-Clark

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