Using Z3 QFNRA Tactics with Data Types: Interaction or Nesting

Question

In non-linear arithmetic and qfnra-nlsat functions , Leonardo de Mora argues that qfnra-nlsat are not yet fully integrated with the rest of Z3. I thought the situation changed two years later, but apparently the integration is still not very complete.

In the example below, I use data types solely for the purpose of "software development": to organize my data into records. Despite the fact that there are no uninterpreted functions, Z3 still does not 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 pl))) (check-sat-using qfnra-nlsat) (get-model) 

---

 > unknown (model ) 

However, if I manually entered all the functions, Z3 will instantly find the model:

 (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 (+ (* ax) (* by) 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 insert automatically? I am fine with one of these workflows:

• Launch Z3 with a tactic that says “Inline first, then apply qfnra-nlsat . I did not find a way to do this, but maybe I didn’t look good enough.
• Launch Z3 using some version of simplify to do inlining. Launch Z3 a second time after the first call (built-in version).

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

Thanks!

Answer 1

That's right, the NLSAT solver is still not integrated with other theories. At the moment, we can use it only if we exclude all data types (or elements of other theories) before launching it. I believe there is currently no useful existing tactic inside Z3, so this needs to be done in advance. In general, it’s easy to make tactics, for example:

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

but simplification is not enough to eliminate the data type constants in this task. (The corresponding implementation files are datatype_rewriter.cpp and datatype_simplifier_plugin.cpp .)