Stosowanie taktyki Z3 QFNRA z typami danych: interakcja lub podpowiedź

Question

W Non-linear arithmetic and uninterpreted functions, Leonardo de Moura twierdzi, że taktyka qfnra-nlsat nie została jeszcze w pełni zintegrowana z resztą Z3. Myślałem, że sytuacja zmieniła się za dwa lata, ale widocznie integracja wciąż nie jest kompletna.

W poniższym przykładzie używam typów danych wyłącznie do celów "inżynierii oprogramowania": do organizowania moich danych w zapisy. Nawet jeśli istnieją żadne funkcje zinterpretowane, Z3 wciąż nie daje mi rozwiązanie:

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

Jednak gdybym ręcznie inline wszystkie funkcje, Z3 znajdzie model natychmiast:

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

Moje pytanie brzmi, czy istnieje sposób do pE zmodyfikuj takie automatyczne wstawianie? Jestem w porządku z jednej z tych przepływów pracy.

1. Wprowadzenie Z3 z taktyką, która mówi „Inline pierwszy, a następnie zastosować qfnra-nlsat Nie znaleźli sposób, aby to zrobić, ale może ja nie szukałem wystarczająco dobrze.
2. Wprowadzenie Z3 stosując jakąś wersję simplify zrobić inline. Uruchom Z3 po raz drugi w wyniku pierwszej inwokacji (wersja inlined).

innymi słowy, jak zrobić qfnra-nlsat pracować z krotkami?

Dziękujemy!

Answer 1

Zgadza się, solwer NLSAT nadal nie jest zintegrowany z innymi teoriami. W tej chwili możemy go używać tylko wtedy, gdy usuniemy wszystkie typy danych (lub elementy innych teorii) przed uruchomieniem. Uważam jednak, że nie ma obecnie żadnej użytecznej taktyki wewnątrz Z3, więc trzeba to zrobić wcześniej. Na ogół nie jest to trudne do komponowania taktyki, na przykład, tak:

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

ale Simplifier nie jest wystarczająco silny, aby wyeliminować stałe typu danych w tym problemie. (Odpowiednimi plikami implementacji są datatype_rewriter.cpp i datatype_simplifier_plugin.cpp.)