Skip to content

Commit 7be604d

Browse files
mistzztmistzzt
committed
add eusolver
1 parent 1da2372 commit 7be604d

File tree

5 files changed

+185
-52
lines changed

5 files changed

+185
-52
lines changed

‎README.md

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@ We provide [`template.nix`](./template.nix), a minimal Nix flake template that d
1919

2020
## More Program Synthesis Tools with Nix Derivations
2121

22-
- EUSolver: https://github.com/mistzzt/EUSolver
2322
- Opera: https://github.com/utopia-group/Opera
2423

2524
If you're working with or developing a tool that you believe should be listed here, please reach out.

‎default.nix

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,4 +8,5 @@
88
AutoLifter = pkgs.callPackage ./pkgs/AutoLifter {};
99
parsynt = pkgs.callPackage ./pkgs/parsynt {};
1010
Synduce = pkgs.callPackage ./pkgs/Synduce {};
11+
eusolver = pkgs.callPackage ./pkgs/eusolver {};
1112
}

‎pkgs/eusolver/default.nix

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
{
2+
fetchFromBitbucket,
3+
lib,
4+
makeWrapper,
5+
stdenv,
6+
python311,
7+
cmake,
8+
}: let
9+
python = python311.withPackages (ps: with ps; [pyparsing z3]);
10+
src =
11+
fetchFromBitbucket
12+
{
13+
owner = "abhishekudupa";
14+
repo = "eusolver";
15+
rev = "cedce0c159996cafb14367ed400314d86b4832ad";
16+
sha256 = "pZXFRbq1XKn6eALFKobwKbjW7JzYpQhR1RrP9cdkWbI=";
17+
};
18+
19+
libeusolver = stdenv.mkDerivation {
20+
name = "libeusolver";
21+
version = "0-unstable-2020-06-15";
22+
inherit src;
23+
24+
sourceRoot = "${src.name}/thirdparty/libeusolver";
25+
buildInputs = [cmake python311];
26+
installPhase = ''
27+
mkdir -p $out
28+
cp eusolver.py $out
29+
cp libeusolver.* $out
30+
'';
31+
};
32+
in
33+
stdenv.mkDerivation rec {
34+
name = "eusolver";
35+
version = "0-unstable-2020-06-15";
36+
inherit src;
37+
patches = [./diff.patch];
38+
39+
nativeBuildInputs = [
40+
python
41+
libeusolver
42+
makeWrapper
43+
cmake
44+
];
45+
dontUseCmakeConfigure = true;
46+
47+
installPhase = ''
48+
mkdir -p $out/bin
49+
cp -r src $out/src
50+
cp -r benchmarks $out/benchmarks
51+
52+
makeWrapper ${python}/bin/python $out/bin/eusolver \
53+
--argv0 "eusolver" \
54+
--add-flags $out/src/benchmarks.py \
55+
--prefix PYTHONPATH : ${libeusolver}
56+
'';
57+
58+
meta = with lib; {
59+
description = "enumerative unification based solver";
60+
homepage = "https://bitbucket.org/abhishekudupa/eusolver";
61+
platforms = platforms.unix;
62+
};
63+
}

‎pkgs/eusolver/diff.patch

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
diff --git a/scripts/job_scheduler.py b/scripts/job_scheduler.py
2+
index 3feaceb..0ec4e33 100755
3+
--- a/scripts/job_scheduler.py
4+
+++ b/scripts/job_scheduler.py
5+
@@ -68,11 +68,11 @@ for process_id in range(num_concurrent_processes):
6+
7+
print('Starting %d worker processes, with %d jobs to run' % (num_concurrent_processes, len(job_list)))
8+
sys.stdout.flush()
9+
-begin_time = time.clock()
10+
+begin_time = time.process_time()
11+
for worker_process in worker_processes:
12+
worker_process.start()
13+
14+
for worker_process in worker_processes:
15+
worker_process.join()
16+
-end_time = time.clock()
17+
+end_time = time.process_time()
18+
print('Completed %d jobs in %f seconds, with %d worker processes' % (len(job_list), end_time - begin_time, num_concurrent_processes))
19+
diff --git a/src/core/solvers.py b/src/core/solvers.py
20+
index 6b079cf..e84d34c 100644
21+
--- a/src/core/solvers.py
22+
+++ b/src/core/solvers.py
23+
@@ -78,7 +78,7 @@ class Solver(object):
24+
def solve(self, generator_factory, term_solver, unifier, verifier, verify_term_solve=True):
25+
import time
26+
27+
- time_origin = time.clock()
28+
+ time_origin = time.process_time()
29+
30+
while (True):
31+
# print('________________')
32+
@@ -110,7 +110,7 @@ class Solver(object):
33+
sol_or_cex = cexs
34+
35+
if _is_expr(sol_or_cex):
36+
- solution_found_at = time.clock() - time_origin
37+
+ solution_found_at = time.process_time() - time_origin
38+
if self.report_additional_info:
39+
yield (sol_or_cex,
40+
unifier.last_dt_size,
41+
diff --git a/src/enumerators/enumerators.py b/src/enumerators/enumerators.py
42+
index 13f325b..7883b7f 100644
43+
--- a/src/enumerators/enumerators.py
44+
+++ b/src/enumerators/enumerators.py
45+
@@ -549,7 +549,7 @@ class StreamGenerator(GeneratorBase):
46+
# total_exps = 0
47+
# logging_enabled = self.enable_logging
48+
# if (logging_enabled):
49+
- # generation_start_time = time.clock()
50+
+ # generation_start_time = time.process_time()
51+
52+
max_size = self.max_size
53+
sub_generator_object = self.generator_object
54+
@@ -558,7 +558,7 @@ class StreamGenerator(GeneratorBase):
55+
total_of_current_size = 0
56+
sub_generator_object.set_size(current_size)
57+
# if (logging_enabled):
58+
- # current_size_start_time = time.clock()
59+
+ # current_size_start_time = time.process_time()
60+
61+
sub_generator_state = sub_generator_object.generate()
62+
while (True):
63+
@@ -568,7 +568,7 @@ class StreamGenerator(GeneratorBase):
64+
yield retval
65+
except StopIteration:
66+
# if (logging_enabled):
67+
- # current_size_end_time = time.clock()
68+
+ # current_size_end_time = time.process_time()
69+
# current_size_time = current_size_end_time - current_size_start_time
70+
# cumulative_size_time = current_size_end_time - generation_start_time
71+
# total_exps += total_of_current_size

‎pkgs/parsynt/default.nix

Lines changed: 50 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -5,60 +5,59 @@
55
ocaml-ng,
66
z3,
77
racket,
8-
}:
9-
let
8+
}: let
109
ocamlPackages = ocaml-ng.ocamlPackages_5_1;
1110
in
12-
ocamlPackages.buildDunePackage rec {
13-
pname = "Parsynt";
14-
version = "0-unstable-2021-12-15";
15-
duneVersion = "3";
16-
src =
17-
fetchFromGitHub
18-
{
19-
owner = "victornicolet";
20-
repo = "parsynt";
21-
rev = "b70635d199dfc47378b19d4140093b7d261d753e";
22-
sha256 = "cJnCGDFe7scnvlHN0G31Oi156iY0+DJnkZvgoQG3VRQ=";
23-
};
24-
patches = [./diff.patch];
25-
preConfigure = ''
26-
mkdir -p $out
27-
cp -r $src/src $out
11+
ocamlPackages.buildDunePackage rec {
12+
pname = "Parsynt";
13+
version = "0-unstable-2021-12-15";
14+
duneVersion = "3";
15+
src =
16+
fetchFromGitHub
17+
{
18+
owner = "victornicolet";
19+
repo = "parsynt";
20+
rev = "b70635d199dfc47378b19d4140093b7d261d753e";
21+
sha256 = "cJnCGDFe7scnvlHN0G31Oi156iY0+DJnkZvgoQG3VRQ=";
22+
};
23+
patches = [./diff.patch];
24+
preConfigure = ''
25+
mkdir -p $out
26+
cp -r $src/src $out
2827
29-
project_dir_src_path=$PWD/src/utils/Project_dir.ml
30-
rm $project_dir_src_path || true
31-
touch $project_dir_src_path
32-
echo "let base = \"$out\"" >> $project_dir_src_path
33-
echo "let src = \"$out/src/\"" >> $project_dir_src_path
34-
echo "let templates = \"$out/src/templates/\"" >> $project_dir_src_path
35-
echo "let racket = \"${racket}/bin/racket\"" >> $project_dir_src_path
36-
echo "let z3 = \"${z3}/bin/z3\"" >> $project_dir_src_path
37-
'';
28+
project_dir_src_path=$PWD/src/utils/Project_dir.ml
29+
rm $project_dir_src_path || true
30+
touch $project_dir_src_path
31+
echo "let base = \"$out\"" >> $project_dir_src_path
32+
echo "let src = \"$out/src/\"" >> $project_dir_src_path
33+
echo "let templates = \"$out/src/templates/\"" >> $project_dir_src_path
34+
echo "let racket = \"${racket}/bin/racket\"" >> $project_dir_src_path
35+
echo "let z3 = \"${z3}/bin/z3\"" >> $project_dir_src_path
36+
'';
3837

39-
nativeBuildInputs = with ocamlPackages; [menhir];
38+
nativeBuildInputs = with ocamlPackages; [menhir];
4039

41-
buildInputs = with ocamlPackages; [
42-
getopt
43-
sexplib
44-
fmt
45-
stdio
46-
ppx_sexp_conv
47-
ppx_let
48-
fileutils
49-
core
50-
lwt
51-
camlp-streams
52-
];
53-
strictDeps = true;
54-
preBuild = ''
55-
dune build Parsynt.opam
56-
'';
40+
buildInputs = with ocamlPackages; [
41+
getopt
42+
sexplib
43+
fmt
44+
stdio
45+
ppx_sexp_conv
46+
ppx_let
47+
fileutils
48+
core
49+
lwt
50+
camlp-streams
51+
];
52+
strictDeps = true;
53+
preBuild = ''
54+
dune build Parsynt.opam
55+
'';
5756

58-
meta = with lib; {
59-
description = "Automatic parallel divide-and-conquer programs synthesizer";
60-
homepage = "https://github.com/victornicolet/parsynt";
61-
license = licenses.gpl2;
62-
platforms = platforms.unix;
63-
};
64-
}
57+
meta = with lib; {
58+
description = "Automatic parallel divide-and-conquer programs synthesizer";
59+
homepage = "https://github.com/victornicolet/parsynt";
60+
license = licenses.gpl2;
61+
platforms = platforms.unix;
62+
};
63+
}

0 commit comments

Comments
 (0)