Utilizzo tattica Z3 QFNRA con tipi di dati: interazione o interlining

Question

In Non-linear arithmetic and uninterpreted functions, Leonardo de Moura afferma che la tattica qfnra-nlsat non è stata ancora completamente integrata con il resto di Z3. Ho pensato che la situazione sia cambiata in due anni, ma a quanto pare l'integrazione non è ancora molto completa.

Nell'esempio seguente, utilizzo i tipi di dati esclusivamente per scopi di "ingegneria del software": per organizzare i miei dati in record. Anche se non ci sono funzioni non interpretati, Z3 non riesce ancora a darmi una soluzione:

(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 
) 

Tuttavia, se manualmente in linea tutte le funzioni, Z3 trova un modello immediatamente:

(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) 
) 

la mia domanda è: esiste un modo per pe rform un allineamento di questo tipo automaticamente? Io sto bene con uno di questi flussi di lavoro:.

1. lancio Z3 con una tattica che dice "in linea prima, quindi applicare qfnra-nlsat non ho trovato un modo per farlo, ma forse non ero alla ricerca abbastanza bene.
2. lancio Z3 utilizzando una qualche versione di simplify per fare la messa in linea. Avviare Z3 la seconda volta sul risultato della prima invocazione (la versione inline).

In altre parole, come fare qfnra-nlsat lavoro con le tuple?

Grazie!

Answer 1

Questo è corretto, il risolutore NLSAT non è ancora integrato con le altre teorie. Al momento, possiamo usarlo solo se eliminiamo tutti i tipi di dati (o elementi di altre teorie) prima di eseguirlo. Credo che al momento non ci sia alcuna tattica esistente valida all'interno di Z3, quindi questo dovrebbe essere fatto in anticipo. In generale, non è difficile comporre le tattiche, per esempio, in questo modo:

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

ma il semplificatore non è abbastanza forte per eliminare le costanti di tipo di dati di questo problema. (I rispettivi file di implementazione sono datatype_rewriter.cpp e datatype_simplifier_plugin.cpp.)