SMT solvers allow one to reason with logical combinations of arithmetic statements. Z3 has the most flexible web-based interface, with a few extensions on the standard SMT-LIB 2 format that make the task of modeling your query easier. So, I'll show what one can enter here to model and reason about yor query.
;; Trace subset of unsatisfiable constraints
(set-option :produce-unsat-cores true)
;; Declare enumerated types.
(declare-datatypes () ((Risk None Low Medium High)))
(declare-datatypes () ((Index A1 A2 A3 S1 S2 S3 S4 S5 S6 S7 S8 S9)))
;; Declare the constant symbols of our model.
(declare-const amount Real)
(declare-const risklevel Risk)
(declare-const ind Index)
;; Assert constraints on the model. Named constraints can be traced.
(assert (! (or (< amount 20000) (and (<= 20000 amount) (= risklevel None)))
(assert (! (or
(= ind A1) (= ind A2) (= ind A3)
(= ind S1) (= ind S2) (= ind S9)) :named rightindex))
;; Sanity check: Are the constraints satisfiable?
(check-sat) ; expect 'sat'
;; See if we can simplify one of the constraints. (Not much.)
(simplify (or (< amount 20000) (and (<= 20000 amount) (= risklevel None))))
;; Get values of amount, risklevel, and ind that witness satisfiability.
(get-value (amount risklevel ind))
;; Start new context.
;; Do these choices satisfy the constraints?
(assert (! (and (= amount 100000) (= risklevel Medium)) :named example))
(check-sat) ; expect 'unsat'
;; Get explanation.
;; We can now check another example or simply say, 'That's all, folks!'
Running Z3 on this input produces:
(or (not (<= 20000.0 amount)) (and (<= 20000.0 amount) (= risklevel None)))
((amount 20000.0) (risklevel None) (ind A1))
The last line says that the unsatisfiability of the constraints depends on a conflict between the
example constraints. The
rightindex constraint has nothing to do with it.