Constraint-Programmierung (Bsp: SMT)

(satisfiability modulo theory)

Programm (Constraint-System)

(set-logic QF_NIA)(set-option :produce-models true)
(declare-fun P () Int) (declare-fun Q () Int)
(declare-fun R () Int) (declare-fun S () Int)
(assert (and (< 0 P) (<= 0 Q) (< 0 R) (<= 0 S)))
(assert (> (+ (* P S) Q) (+ (* R Q) S)))
(check-sat)(get-value (P Q R S))
(ausf├╝hren mit z3 p.smt2)

Antwort (erf├╝llende Belegung):

sat
((P 14)  (Q 9) (R 11)  (S 7))
siehe http://z3.codeplex.com/wikipage?title=Publications



Johannes Waldmann 2014-03-31