Z3 QFNRA 전술 사용 : 상호 작용 또는 인라이닝

Question

Non-linear arithmetic and uninterpreted functions에서 Leonardo de Moura는 qfnra-nlsat 전술이 아직 Z3의 나머지 부분과 완전히 통합되지 않았다고 말합니다. 나는 상황이 2 년 후에 바뀌 었다고 생각했다. 그러나 분명히 통합은 아직 완전하지 않다.

아래 예제에서는 데이터를 레코드로 구성하는 "소프트웨어 엔지니어링"용도로만 데이터 유형을 사용합니다.

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

: 나는 수동으로 인라인 모든 기능, Z3는 즉시 모델을 찾으면, 그러나

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

: 더 해석의 기능이 없다하더라도, Z3는 여전히 나에게 솔루션을 제공하는 데 실패 내 질문은

---

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

, 퍼가기하는 방법은 무엇입니까 그런 인라인은 자동으로 실행 되나요? 난 괜찮아와 하나 이러한 워크 플로우 중 하나.

1. 시작 Z3 인라인 먼저, 다음 qfnra-nlsat을 적용 난 그렇게 할 수있는 방법을 발견하지 않았습니다 "라는 전술로하지만, 어쩌면 내가보고되지 않았다 충분히.
Z3가. 인라인을 처음 호출의 결과에 Z3에게 (인라인 버전)을 두 번째로 시작하는 simplify의 일부 버전을 사용
2. 시작합니다.
즉

, 어떻게 qfnra-nlsat로 만들려면 튜플을 사용하여 작업 하시겠습니까?

고마워요!

Answer 1

맞습니다. NLSAT 해결자는 여전히 다른 이론과 통합되지 않습니다. 현재 실행하기 전에 모든 데이터 유형 (또는 다른 이론의 요소)을 제거하는 경우에만 사용할 수 있습니다. 나는 Z3의 내부에 유용한 전술이 존재하지 않는다고 생각한다. 그래서 이것은 미리 수행되어야 할 것이다.

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

을하지만 simplifier이 문제에 데이터 유형 상수를 제거 할만큼 강한되지 않습니다 : 일반적으로는 다음과 같이 예를 들면, 전술을 구성하기 어렵지 않다. 각 구현 파일은 datatype_rewriter.cpp 및 datatype_simplifier_plugin.cpp입니다.