EUSolver for Nix

This repository contains a fork of the original EUSolver with a Nix derivation.

Supported platforms for this Nix derivation include:

• x86_64-linux
• aarch64-linux
• x86_64-darwin
• aarch64-darwin

Getting Started

Prerequisites

To use this fork of EUSolver, make sure you have Nix installed on your system. If not, follow the instructions provided in the Nix installation guide.

Building EUSolver

To build EUSolver using Nix, execute the following command:

nix build .

This will generate the executable in the ./result/bin/ directory.

Running EUSolver

After building, you can run EUSolver directly by specifying the path to a benchmark file. For example,

./result/bin/eusolver benchmarks/max/max_2.sl

This command should output the synthesized function similar to the following:

(define-fun max2 ((a0 Int) (a1 Int)) Int
     (ite (>= a0 a1) a0 a1))

Combining Build and Run

Alternatively, you can use nix run to build and immediately execute EUSolver with the desired benchmark:

nix run . -- benchmarks/max/max_2.sl