dReal SMT 솔버 반경

Question

dReal SMT 솔버가 반례를 반환합니까? 나는 produce-models은 사실이지만 반례를 생성하는 방법을 모른다. 또한 dReach 도구에는 --visualize 옵션이 있으므로 dReal이 일부 모델 정보를 생성해야하는 것처럼 보일 수 있습니다. 그러나 .smt2 파일을 실행할 때 반증을 볼 방법을 찾을 수 없습니다.

Answer 1

O.k. 그것은 사소한 것입니다. :) dReal은 (get-model)을 사용하는 일반적인 .smt2 규칙을 따르지 않지만 명령 행 옵션 - model을 사용하여 모델을 얻을 수 있습니다.

예 : dReal - 모델 마이크로파 1.smt2