microsoft / microsoft/z3guide

Add an example that illustrates set_on_model for Optimize

Open
#207 1 comment 1 reaction 1 assignee View on GitHub

Nobody has claimed this yet.

Dominant language
JavaScript
Stars
123
Forks
34
Avg merge
3h 48m
Merged PRs (30d)
4

Description

Here is a bare bones example:

from z3 import *
import sys

opt = Optimize()

def on_model(m):
print("model", m)
sys.stdout.flush()

opt.set_on_model(on_model)

#opt.set("maxsat_engine","wmax")
opt.set("enable_lns", True)
opt.from_file("../smtlib.txt")

set_option(verbose=2)

opt.set(timeout=3000)
opt.check()
print(opt.model())

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.