For bool operations, does Z3 support three-valued logic?

[Flians]

There are three values of 0, 1, X in the circuit. Can Z3 support this situation？

[NikolajBjorner]

One way to encode it is using four elements, z, 0, 1, x, (where x is sometimes called *). You use two bits (two Booleans) to encode the 3 states. The combination z can be ruled out by the encoding and constraints on inputs. Using an enumeration sort with three elements is another approach or operations over -1, 0, 1, but the bit-encoding should map directly into adequately efficient SAT solving.

[Flians]

Thank you!

[Flians]

Hi @NikolajBjorner, Can you provide some C++ API about bitvector? Thank you!

[aytey]

@Flians is there a reason that https://github.com/Z3Prover/z3/blob/master/examples/c%2B%2B/example.cpp#L204 isn't good enough?

[Flians]

@andrewvaughanj
I want to create a conjecture dynamically, which consists of many parts. the method in the example is not very convenient.

[aytey]

If you need help, you'll need to provide a little bit more detail.

Here is the core of the C++ API: https://github.com/Z3Prover/z3/blob/master/src/api/c%2B%2B/z3%2B%2B.h

[Flians]

@andrewvaughanj I got it. But I dont know the function of each api, because it is not described.

[aytey]

Most of the BV operators start here: https://github.com/Z3Prover/z3/blob/master/src/api/c%2B%2B/z3%2B%2B.h#L1793

To work out what they do, you probably want to read here: http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml

[Flians]

@andrewvaughanj Thank you.

[Flians]

One way to encode it is using four elements, z, 0, 1, x, (where x is sometimes called *). You use two bits (two Booleans) to encode the 3 states. The combination z can be ruled out by the encoding and constraints on inputs. Using an enumeration sort with three elements is another approach or operations over -1, 0, 1, but the bit-encoding should map directly into adequately efficient SAT solving.

Hi, I have implemented my program with bitvector. But this solution is particularly poor. how can I set the parameters of Z3 to speed up the solution process?