Validation query formulation, SMT solver, Z3, STP

Question

I have a boolean formula f(a, b, x, y). Where a and b are boolean expressions and x and y are bit vector expressions. a and b are boolean expressions possibly using expressions a, b, x and y.

I want to define the following query for validity:

f(a, b, x, y)* such that *a = false && b = false 

f(a, b, x, y)* such that *a = true && b = false

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

Please advise how to create such a query.

Answer 1

Why not create a fresh variable for a? you can then assert the following: (assert (not a)) (assert (not b)) (assert (f a b x y)) (assert a2) (assert (not (f a2 b x y))) (check-sat)

your query is valid if and only if the query above is unsatisfiable because the bindings are represented as assertions and the implication was negated ( and flattened into two assertions)