(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))
- Constraint-System
=
mathend000# eine prädikatenlogische Formel F
mathend000#
- Lösung =
mathend000# Modell von F
mathend000# (=
mathend000# Strukur M
mathend000#,
in der F
mathend000# wahr ist)
- CP ist eine Form der deklarativen Programmierung.
- Vorteil: Benutzung von allgemeinen Suchverfahren
(bereichs-, aber nicht anwendungsspezifisch).
2014-03-31