This is a program for executing algorithm specifications written in first-order predicate language with variables ranging over the integers and functions from the integers to the integers (which can model arrays). The solver then searches for a satisfying assignment of a given input formula. Downloads
|