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

2015-03-09: Added support for model generation. Use the flag +model.
2015-03-09: Added an example demonstrating Horn clause solving (see CAV'14 paper): examples/horn-ab.smt2

Usage

Norn together with all required libraries can be downloaded here.
Example: ./norn -timeout=15 +model examples/reglang-sat.smt2.

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:

The Kaluza benchmarks (~45000 benchmarks), translated to SMTLIB2 format by the CVC4 team.
A set of ~1000 benchmarks containing regular langauge constraints generated by a CEGAR based model checker for string programs. Also available in S3's format.

People Involved

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