Re: Substitution related query formulation

[Stephen McCamant]

MD> I have a boolean fourmula f(a, b, x, y). Where a and b are boolean
MD> expressions and x and y are bitvector expressions.

MD> I want to define the following query for validity:

MD> f(a, b, x, y) such that a = false && b = false
MD> ->
MD> f(a, b, x, y) such that a = true && b = false

MD> In a way, I need to substitute the values of a and b in the formula on
MD> both the sides of implication.

MD> Please advise how to create such a query.

I'm not sure I'm clear on what query you want to create. I'm guessing
that in the queries you're actually creating, "f" will be replaced by
some particular formula; perhaps you could give a simplified example
of one such f, and the context in which it arises, to help us
understand.

One interpretation that makes it pretty simple is that your "such
that" just means substitution, so that the formula you want to check
for validity looks like

f(false, false, x, y) => f(true, false, x, y)

This formula should certainly be queryable in STP if "f" is
expressible. The most reliable way would be to just expand the
definition of "f" twice. If your question is that you want to avoid
writing the definition of "f" twice, STP has partial support for
SMTLIB 2 function definitions that might be used in a case like
this. Suppose that "f" is

a && b && x == y

Then you can use the following query:

(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(declare-fun the_x () (_ BitVec 32))
(declare-fun the_y () (_ BitVec 32))
(define-fun f
((a (_ BitVec 1))
(b (_ BitVec 1))
(x (_ BitVec 32))
(y (_ BitVec 32)))
Bool
(and (= a #b1) (= b #b1) (= x y)))
(assert (not (=> (f #b0 #b0 the_x the_y) (f #b1 #b0 the_x the_y))))
(check-sat)
(exit)

which gives "unsat" (valid). Note that in SMTLIB mode STP is a
satisfiability checker, so I had to negate the assertion. Also
"define-fun" appears to only support bit-vector parameters, so I
represented false and true by the one-bit vectors #b0 and #b1. If you
change "f" to "!a && !b && x == y" then the formula is no longer
valid, and STP gives the counterexample x = y = 0x00000000.

However there are other interpretations of your query that would not
be so natural for STP. If "... such that" means "there exists ... such
that", then your formula has a there-exists quantifier inside the
for-all quantifier implied by validity checking, and so can't be made
quantifier-free. Another way of saying this is that STP only thinks
about one assignment to the free variables at a time, either looking
for one that makes the formula true, when it's a satisfiability
checker, or looking for one that makes the formula false, when it's a
validity checker. So if "a" is some particular boolean expression in
terms of other free variables, STP can't conceive of the possibility
of "a = true" and "a = false" at the same time.

Hope this helps,

-- Stephen

[Manjeet Dahiya]

Hello Stephen,

I have the second the second case. a is an expression in terms of b, x
and y. Can you suggest any other solver that may solve such queries?

Thanks!
Manjeet

[Stephen McCamant]

>>>>> "MD" == Manjeet Dahiya <manjee...@gmail.com> writes:

MD> I want to define the following query for validity:

MD> f(a, b, x, y) such that a = false && b = false
MD> ->
MD> f(a, b, x, y) such that a = true && b = false

MD> In a way, I need to substitute the values of a and b in the formula on
MD> both the sides of implication.

[...]
MD> I have the second the second case. a is an expression in terms of
MD> b, x and y. Can you suggest any other solver that may solve such
MD> queries?

Hmm. I'm still not fully clear on what your problem really looks
like. I think the clearest way to write your formula would be to
figure out what all the free variables are and what free variables all
the other parts are functions of, and then put in all the needed
quantifiers with their scopes. You'll have a much easier time solving
your problem if it's expressible without quantifier alternation
("there exists" inside "for all" or vice-versa), though perhaps you're
saying you think it can't be.

If you need quantifiers, your choice of tools becomes more
complicated: there's a wider variety of tools with narrower classes of
problems for which they work well.

The broader class of tools that are like STP are called SMT solvers;
some SMT solvers have some support for quantified formulas. In your
case you need one that supports both quantifiers and bit-vectors. You
can find a good list of SMT solvers at
http://www.smtlib.org/solvers.html , and their web pages or
documentation generally describe which theories they support. Most of
these should support the same SMTLIB input format, which should make
it easier to try different tools. Some you might try are CVC(3/4),
Yices, or Z3.

Further afield, there are at least a couple other classes of tools you
could consider. "First-order automated theorem provers" tend to focus
on proof techniques more like instantiating axioms: they might be
useful in your problem if you only need a few properties about
bit-vectors that you can express manually. "Quantified Boolean
formula" (QBF) solvers are generalizations of SAT solvers that allow
arbitrary combinations of quantifiers, but still only Boolean
variables: to use one you'd need to translate your whole formula into
a quantified CNF format.