Alt-Ergo

zero

• Overview
• Download
  • Sources
  • Installation instructions
• Documentation
• Example
• Contact

Overview

Alt-Ergo Zero is an OCaml library for an SMT solver. This SMT solver is derived from Alt-Ergo. It uses an efficient SAT solver and supports the following quantifier free theories:

• Equality and uninterpreted functions
• Arithmetic (linear, non-linear, integer, real)
• Enumerated data-types

This API makes heavy use of hash consing, in particular hash-consed strings.

Download

Sources

Alt-Ergo Zero is distributed under the Apache licence.

You can download the sources of the latest version of Alt-Ergo Zero here.

Installation instructions

To compile Alt-Ergo Zero you will need OCaml version 3.11 (or newer).

Uncompress the archive and do:
$ cd aez-0.3
$ ./configure
$ make

then with superuser rigths:
# make install

Documentation

The API is documented with ocamldoc here.

Example

You can construct the following problem and check its validity with the code given afterwards.

type t

f : int → t

∀ x, y : int. ∀ u, w : t.
    (f(x + 3) = u ∧  f(y + 2) = w ∧  x = y - 1 ∧  f(x + y) = u) ⇒ u = w

To run this example in the toplevel you must give ocaml (or ocamlc) the options -I +alt-ergo-zero unix.cma nums.cma aez.cma. To compile natively you must use -I +alt-ergo-zero unix.cmxa nums.cmxa aez.cmxa.

open Aez
open Smt
module T = Term
module F = Formula
module Solver = Make (struct end)

let type_t = Hstring.make "t";;
let f = Hstring.make "f";;
let x = Hstring.make "x";;
let y = Hstring.make "y";;
let u = Hstring.make "u";;
let w = Hstring.make "w";;

Type.declare type_t [];;
Symbol.declare f [Type.type_int] type_t;;
Symbol.declare x [] Type.type_int;;
Symbol.declare y [] Type.type_int;;
Symbol.declare u [] type_t;;
Symbol.declare w [] type_t;;

let tx = T.make_app x [];;
let ty = T.make_app y [];;
let tu = T.make_app u [];;
let tw = T.make_app w [];;
let t3 = T.make_int (Num.Int 3);;
let t2 = T.make_int (Num.Int 2);;
let t1 = T.make_int (Num.Int 1);;
let fx3 = T.make_app f [T.make_arith T.Plus tx t3];;
let fy2 = T.make_app f [T.make_arith T.Plus ty t2];;
let ty = T.make_app y [];;

let f1 = F.make_lit F.Eq [fx3; tu];;                          (* f(x + 3) = u *)
let f2 = F.make_lit F.Eq [fy2; tw];;                          (* f(y + 2) = w *)
let f3 = F.make_lit F.Eq [tx; (T.make_arith T.Minus ty t1)];; (* x = y - 1 *)
let neg_goal = F.make F.Not [F.make_lit F.Eq [tu; tw]];;      (* not (u = w) *)

try
  Solver.clear ();
  Solver.assume ~id:1 f1;
  Solver.assume ~id:2 f2;
  Solver.assume ~id:3 f3;
  Solver.assume ~id:4 neg_goal;
  Solver.check ();
  print_endline "not valid"
with Unsat _ ->
  print_endline "valid";;