Z3 해결사 차이 로직 파이썬 API를

내가 파이썬에서 이런 일을하려고했습니다 : 나는 솔버 (solver.set('smt.arith.solver', 1))을 위해 그것을 할 수있었습니다Z3 해결사 차이 로직 파이썬 API를

(set-option :smt.arith.solver 1) 
(declare-const x Int) 
(declare-const y Int) 
(assert (>= 10 x)) 
(assert (>= x (+ y 7))) 
(maximize (+ x y)) 
(check-sat)

하지만 함께 할 수 없습니다 클래스 최적화. 파이썬에서 위와 같은 것을 쓸 수 있습니까?

또한 일반 논리 선형 프로그램을 얻는다면 차이 논리로 설정된 솔버가 오류를 던집니까?

출처

2017-03-23 George

논리를 진술의 표준 방법은

을 설정할 필요가 없습니다 (https://z3prover.github.io/api/html/z3.html 참조) SolverFor() 공장을 사용하여, 당신은 해결사 인스턴스를 생성 논리의 SMT-LIB 이름을 제공하는 것입니다 논리가 Z3을 작동 시키므로 논리에 대해 걱정하지 않고도 문제의 작업 버전을 얻을 가치가 있습니다.

출처

2017-03-23 22:30:06 Marco

감사합니다. 최적화 문제와 유사한 점이 있습니까? 나는 문서에서 아무것도 발견하지 못했다. 나는 작동하는 버전을 가지고 있지만 성능이 떨어지고 있습니다. 그래서이 논리로 전환하는 것이 도움이되는지 확인하려고합니다. (실제로 문제를 설명하기 위해 차이 논리가 필요합니다.) – George

Z3 해결사 차이 로직 파이썬 API를

답변

관련 문제