CODEWITHSUNDEEP
z3
Markus Müller
Markus Müller

Reputation: 35

Z3/OCaml free constants

Out of curiosity, I wonder how I can add a free constant to a Z3 solver via the OCaml API, i.e., something corresponding to

(declare-const k!0 (_ BitVec 5))

The following attempt yields an invalid argument exception.

let cfg = [("model", "true"); ("proof", "false")] in
let ctx = mk_context cfg in
let solver = Solver.mk_solver ctx None in
  Solver.add solver [Expr.mk_const ctx (Symbol.mk_int ctx 0) (BitVector.mk_sort ctx 5)]

Is there a way to do this without adding a constraint which contains the constant and simplifies to true?

Upvotes: 1

Views: 182

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8402

Solver.add expects a term of Boolean sort, i.e., an assertion, but in this example a constant of bit-vector type is added, that's why it complains about an invalid argument.

In general, constants (or any other functions) do not need to be declared explicitly in a separate step via the API, they can be constructed and used in expressions/assertions without declaring them.

By default, such constants will be assumed to be existential, otherwise they'll have to be quantified explicitly (see the Quantifier module).

Upvotes: 2

Related Questions