SoP Satisfier

Kind of SMT solver with only Non-linear Natural Arithmetic.

Library with an SMTlib like interface to declare and assert SoP (kind of) expressions.

Interface:

• declare - to declare expression to the state
• assert - to assert that expression holds in the state
• unify - to get a list of expressions that need to hold for the given expression to hold (only equalities are supported)
• range - to get a range (a pair of minimum and maximum possible values) of expression