CODEWITHSUNDEEP
z3
Steven Woodhouse
Steven Woodhouse

Reputation: 23

Unsat core generation with .NET Z3 API

I'm trying to turn on unsat core generation, using Z3 4.3.0 and the .NET API.

Calling context.UpdateParamValue("unsat_core", "true") throws an exception with the message "Error setting 'unsat_core', reason: unknown option".

Checking context.SimplifyParameterDescriptions lists only these parameters:

(:ite-extra-rules, :flat, :elim-and, :local-ctx, :local-ctx-limit, :blast-distinct, :som, :som-blowup, :hoist-mul, :hoist-cmul, :algebraic-number-evaluator, :mul-to-power, :expand-power, :expand-tan, :max-degree, :eq2ineq, :sort-sums, :gcd-rounding, :arith-lhs, :elim-to-real, :push-to-real, :elim-rem, :udiv2mul, :split-concat-eq, :bit2bool, :blast-eq-value, :elim-sign-ext, :hi-div0, :mul2concat, :expand-select-store, :sort-store, :max-memory, :max-steps, :push-ite-arith, :push-ite-bv, :pull-cheap-ite, :cache-all)

This is related to a previously asked question which didn't seem to get a conclusive answer.

Upvotes: 2

Views: 205

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

The exact form the configuration needs to take depends on which parts of Z3, and which version is being used. The SimplifyParameterDescriptions are only for the simplifier (either calls to the Simplify tactic, or Expr.Simplify). Unsat-core generation needs to be enabled either on the Context (via it's constructor and option unsat_core), or via the parameters of a Goal (see Context.MkGoal).

I can't test it where I am right now, but I think the old version (master/4.3.0) used the same parameter name in upper case. Newer versions (i.e., the unstable branch) also have a function for setting global parameters in Global.SetParamValue. Sorry about the confusion, but the parameter setting infrastructure was completely replaced since the last master release.

Upvotes: 1

Related Questions