Norn, a solver for string constraints

Norn is a solver for string constraints, i.e. word equations over (unbounded length) string variables together with length and membership constraints.

News

Usage

Examples

The following examples demonstrate some features of Norn:

reglang.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)
	

abcd.smt2

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)
	

Benchmarks

We have evaluated Norn on two sets of benchmarks:

People Involved

For any questions or bug reports, please contact jari.stenman at it.uu.se.