1 files changed, 55 insertions, 0 deletions
diff --git a/synth b/synth
new file mode 100644
index 0000000..4594d0a
--- /dev/null
+++ b/synth
@@ -0,0 +1,55 @@
+#!/usr/bin/env python3
+# Patch's predicate synthesizer
+# Copyright (C) 2024  Nguyễn Gia Phong
+#
+# This file is part of taosc.
+#
+# Taosc is free software: you can redistribute it and/or modify
+# it under the terms of the GNU Affero General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# Taosc is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU Affero General Public License for more details.
+#
+# You should have received a copy of the GNU Affero General Public License
+# along with taosc.  If not, see <https://www.gnu.org/licenses/>.
+
+from contextlib import redirect_stderr
+from os import devnull
+from os.path import basename
+from pathlib import Path
+from sys import argv, stdout
+
+from pacfix import learn
+from pacfix.invariant import INVARIANT_MAP, InvariantType
+from pacfix.utils import get_live_vars, get_valuations, parse_valuation
+
+
+def encode(inv, file):
+    if inv.inv_type == InvariantType.VAR:
+        file.write(f"v{inv.data}")
+    elif inv.inv_type == InvariantType.CONST:
+        file.write(f"{'n' if inv.data < 0 else 'p'}{abs(inv.data)}")
+    else:
+        file.write(INVARIANT_MAP[inv.inv_type])
+        encode(inv.left, file)
+        encode(inv.right, file)
+
+
+if len(argv) != 3:
+    print(f'usage: taosc-synth input-dir delta')
+    exit(1)
+input_dir = Path(argv[1])
+delta = float(argv[2])
+
+with open(input_dir / 'vars') as f: live_vars = get_live_vars(f)
+vals_neg, vals_pos = parse_valuation(get_valuations(input_dir / "neg"),
+                                     get_valuations(input_dir / "pos"))
+with open(devnull, 'w') as f, redirect_stderr(f):
+    result = learn(live_vars, vals_neg, vals_pos, delta)
+for i in result.inv_mgr.invs:
+    encode(i, stdout)
+    print()