Polish a tad HEAD main

1 files changed, 57 insertions, 0 deletions

diff --git a/synth.py b/synth.py
new file mode 100644
index 0000000..c35fb84
--- /dev/null
+++ b/synth.py
@@ -0,0 +1,57 @@
+#!/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 argparse import ArgumentParser
+from cProfile import run
+from functools import partial
+from pathlib import Path
+
+from pacfix import learn
+from pacfix.invariant import INVARIANT_MAP, InvariantType
+from pacfix.utils import get_live_vars, get_valuations, parse_valuation
+
+write = partial(print, end='')
+
+
+def write_invariant(inv):
+    if inv.inv_type == InvariantType.VAR:
+        write('v')
+        write(inv.data)
+    elif inv.inv_type == InvariantType.CONST:
+        write('n' if inv.data < 0 else 'p')
+        write(abs(inv.data))
+    else:
+        write(INVARIANT_MAP[inv.inv_type])
+        write_invariant(inv.left)
+        write_invariant(inv.right)
+
+
+arg_parser = ArgumentParser(prog='taosc-synth')
+arg_parser.add_argument('input', help='input directory', type=Path)
+arg_parser.add_argument('delta', help='PAC delta', type=float,
+                        nargs='?', default=0.01)
+args = arg_parser.parse_args()
+
+with open(args.input / 'list') as f: live_vars = get_live_vars(f)
+vals_neg, vals_pos = parse_valuation(get_valuations(args.input / 'neg'),
+                                     get_valuations(args.input / 'pos'))
+result = learn(live_vars, vals_neg, vals_pos, args.delta)
+for i in result.inv_mgr.invs:
+    write_invariant(i)
+    print()