; encoding of the formula ((P -> Q) /\ (Q -> R)) -> (P -> R) in smtlib2
; this option is necessary for the get-model and get-valuation commands
(set-option :produce-models true)
; right now, for us any logic suffices because we only need pure propositional logic
; we choose the fragment of first-order logic with uninterpreted functions and
; without quantifiers
(set-logic QF_UF)
; every non-logical symbol has to be declared, non-quantified variables are modelled as
; constants which are modelled as nullary functions
; so propositional variables can be modelled as nullary boolean functions
; (predicates are modelled by boolean functions)
(declare-fun P () Bool)
(declare-fun Q () Bool)
(declare-fun R () Bool)
; implication is symbolized by "=>", biimplication/equivalence by "=",
; "and", "or" and "not" are written out,
; everything is written prefix-style
(assert (=> (and (=> P Q) (=> Q R)) (=> P R)))
; check whether all assertions that have been made until now are satisfiable in conjunction
(check-sat)
; if check-sat was succesful, we can retrieve the values of the fulfilling valuation which
; has been discovered
(get-value (P Q R))