CODEWITHSUNDEEP
c++z3
alphacarrot
alphacarrot

Reputation: 3

How to define a piecewise function in z3

I am trying to define a very simple piecewise linear function in Z3 with the following C++ code:

context c;
sort I = c.int_sort();
expr x = c.int_const("x");
func_decl f = function("f", I, I);
solver s(c);
s.add(forall(x, f(x) == ite(x <= 2, x, x + 1)));
s.add(f(x) == 2);
std::cout << s.check() << std::endl;

This generates the following code in SMTLib format:

(declare-fun f (Int) Int)
(declare-fun x () Int)
(assert (forall ((x Int)) (! (= (f x) (ite (<= x 2) x (+ x 1))) :weight 0)))
(assert (= (f x) 2))
(check-sat)

The obvious answer is x=2. However, during execution, Z3 seems to have entered an infinite loop and stops responding entirely.

Why does this happen, and how should I properly define a piecewise function in Z3?

Upvotes: 0

Views: 246

Answers (2)

alias
alias

Reputation: 30428

Malte described some of the issues that crop up often in handling quantifiers. It's almost always a bad idea to use quantifiers to define functions like this: It unnecessarily invokes procedures that can easily lead the solver to never-ending e-matching loops. The classic (and "official") way to define such a function is to simply use the define-fun construct:

(declare-fun x () Int)
(define-fun f ((x Int)) Int (ite (<= x 2) x (+ x 1)))
(assert (= (f x) 2))
(check-sat)

With this input, I get:

sat

immediately.

There's much to say about quantifiers in SMT solving, and here's a good set of slides to go through: http://homepage.divms.uiowa.edu/~ajreynol/pres-dagstuhl15.pdf

But, long story short, avoid quantifiers unless you absolutely need them. For regular first-order problems like the one you have you don't need quantifiers.

(Note that when you program using the C++, or any other higher-level API, you usually do not define these sorts of functions. Instead, you simply define a function in the host language, and call it with a "symbolic" variable, which generates the right-hand-side for each instantiation. In a sense, you "inline" the definitions at each call site. This avoids unnecessary complexity and is usually sufficient for most modeling problems.)

Upvotes: 1

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

Since SMT problems are often undecidable (depending on which theories the problem involves), it is in general to be expected that Z3 won't terminate (in reasonable time) for certain problems. Quantifiers and non-linear integer arithmetic are, e.g. common causes.

By default, Z3 analysis the problem it was given and configures (e.g. chooses subsolvers) itself accordingly. If you'd like to disable this, e.g. because you want to configure Z3 yourself. use (set-option :auto_config false).

Turning to your example:

  • Using Z3 4.8.7 x64, I immediately get sat for the SMT-LIB snippet you provided. Which Z3 version are you using?

  • If I disable MBQI (Z3 has different subsolvers for quantifiers) via (set-option :smt.mbqi true), then I immediately get unknown. This is not terribly surprising because MBQI is great for finding models for (non-recursive) functions, such your f.

  • Why did you set :weigh 0? It is used to prevent infinite quantifier instantiation chains (matching loops), so explicitly setting a weight of 0 seems risky. Although your quantifier does not give rise to a matching loop anyway.

Upvotes: 1

Related Questions