Norn is a solver for string constraints, i.e. word equations over (unbounded length) string variables together with length and membership constraints.
+model
.examples/horn-ab.smt2
./norn -timeout=15 +model examples/reglang-sat.smt2
.In this example, we assert that X belongs to two regular languages, and is of length 21. Norn constructs a length constraint from the intersection of the languages, and concludes that the problem is unsatisfiable. If the constant in the last assertion is changed to 20, the problem is satisfiable.
(set-logic QF_S)
(declare-fun X () String)
(assert (str.in.re X (re.++ (re.* (str.to.re "ab")) (re.* (str.to.re "dd")))))
(assert (str.in.re X (re.++ (re.* (str.to.re "abab")) (re.* (str.to.re "ddd")))))
(assert (= (str.len X) 21))
(check-sat)
A simple example showing how the interaction between language, equality and length constraints can make a set of constraints unsatisfiable. If the last assertion is removed, the problem is satisfiable.
(set-logic QF_S)
(declare-fun A () String)
(declare-fun B () String)
(declare-fun C () String)
(declare-fun D () String)
(assert (str.in.re A (re.* (str.to.re "a"))))
(assert (str.in.re B (re.* (str.to.re "b"))))
(assert (str.in.re C (re.* (str.to.re "a"))))
(assert (str.in.re D (re.* (str.to.re "b"))))
(assert (= (str.++ A B) (str.++ C D)))
(assert (not (= (str.len A) (str.len C))))
(check-sat)
We have evaluated Norn on two sets of benchmarks:
For any questions or bug reports, please contact jari.stenman at it.uu.se
.