CODEWITHSUNDEEP
z3smt
Manjeet Dahiya
Manjeet Dahiya

Reputation: 505

Validation query formulation, SMT solver, Z3, STP

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.

Upvotes: 1

Views: 392

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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)

Upvotes: 1

Related Questions