Verwenden von Z3 QFNRA Taktik mit Datentypen: Interaktion oder Inlining

Question

In Non-linear arithmetic and uninterpreted functions, Leonardo de Moura, dass die qfnra-nlsat Taktik wurde nicht vollständig in den Rest von Z3 integriert noch. Ich dachte, dass sich die Situation in zwei Jahren geändert hat, aber anscheinend ist die Integration noch nicht vollständig abgeschlossen.

Im folgenden Beispiel verwende ich Datentypen rein für "Software Engineering" Zwecke: um meine Daten in Datensätze zu organisieren. Auch wenn es keine uninterpretierte Funktionen sind nicht Z3 noch mir eine Lösung geben:

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

Wenn ich jedoch manuell inline alle Funktionen, Z3 sofort ein Modell findet:

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

Meine Frage ist, gibt es eine Möglichkeit, pe Ein solches Inlining automatisch gestalten? Ich bin fein mit einem dieses Workflows.

1. Einführung Z3 mit einer Taktik, die sagt: „Inline zuerst, dann qfnra-nlsat bewerbe ich mich nicht einen Weg, dies zu tun gefunden haben, aber vielleicht war ich nicht auf der Suche gut genug.
2. Einführung Z3 eine Version von simplify mit dem inlining zu tun. Starten Sie Z3 zum zweiten Mal auf dem Ergebnis des ersten Aufrufs (die inlined Version).

mit anderen Worten, wie qfnra-nlsat zu machen Arbeit mit Tupeln?

Vielen Dank!

Answer 1

Das stimmt, der NLSAT-Solver ist immer noch nicht mit den anderen Theorien integriert. Im Moment können wir es nur benutzen, wenn wir alle Datentypen (oder Elemente anderer Theorien) eliminieren, bevor wir es ausführen. Ich glaube, dass es momentan keine nützliche Taktik in Z3 gibt, also müsste dies vorher gemacht werden. Im Allgemeinen ist es nicht schwer Taktik zu komponieren, zum Beispiel wie folgt aus:

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

aber der Vereinfacher ist nicht stark genug, um den Datentyp Konstanten in dieses Problem zu beseitigen. (Die entsprechenden Implementierungsdateien sind datatype_rewriter.cpp und datatype_simplifier_plugin.cpp.)