Using Z3 QFNRA tactic with datatypes: interaction or inlining

Question

In Non-linear arithmetic and uninterpreted functions, Leonardo de Moura states that the qfnra-nlsat tactic hasn't been fully integrated with the rest of Z3 yet. I thought that the situation has changed in two years, but apparently the integration is still not very complete.

In the example below, I use datatypes purely for "software engineering" purposes: to organize my data into records. Even though there are no uninterpreted functions, Z3 still fails to give me a solution:

(declare-datatypes () (
    (Point (point (point-x Real) (point-y Real)))
    (Line (line (line-a Real) (line-b Real) (line-c Real)))))

(define-fun point-line-subst ((p Point) (l Line)) Real
    (+ (* (line-a l) (point-x p)) (* (line-b l) (point-y p)) (line-c l)))

(declare-const p Point)
(declare-const l Line)

(assert (> (point-y p) 20.0))
(assert (= 0.0 (point-line-subst p l)))

(check-sat-using qfnra-nlsat)
(get-model)

---

> unknown
(model 
)

However, if I manually inline all the functions, Z3 finds a model instantly:

(declare-const x Real)
(declare-const y Real)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)

(assert (> y 20.0))
(assert (= 0.0 (+ (* a x) (* b y) c)))

(check-sat-using qfnra-nlsat)
(get-model)

---

> sat
(model 
  (define-fun y () Real
    21.0)
  (define-fun a () Real
    0.0)
  (define-fun x () Real
    0.0)
  (define-fun b () Real
    0.0)
  (define-fun c () Real
    0.0)
)

My question is, is there a way to perform such an inlining automatically? I'm fine with either one of these workflows:

1. Launch Z3 with a tactic that says "Inline first, then apply qfnra-nlsat. I haven't found a way to do so, but maybe I wasn't looking well enough.
2. Launch Z3 using some version of simplify to do the inlining. Launch Z3 the second time on the result of the first invocation (the inlined version).

In other words, how to make qfnra-nlsat work with tuples?

Thank you!

Answer 1

That's correct, the NLSAT solver is still not integrated with the other theories. At the moment, we can only use it if we eliminate all datatypes (or elements of other theories) before running it. I believe there is no useful existing tactic inside of Z3 at the moment though, so this would have to be done beforehand. In general it's not hard to compose tactics, e.g., like this:

(check-sat-using (and-then simplify qfnra-nlsat))

but the simplifier is not strong enough to eliminate the datatype constants in this problem. (The respective implementation files are datatype_rewriter.cpp and datatype_simplifier_plugin.cpp.)