From d8090bb73f404a9abff5b7cc9cfdd8cdb1ee4d5f Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong Date: Thu, 16 Oct 2025 18:27:38 +0900 Subject: Read values from files --- synth.py | 59 ----------------------------------------------------------- 1 file changed, 59 deletions(-) delete mode 100644 synth.py (limited to 'synth.py') diff --git a/synth.py b/synth.py deleted file mode 100644 index 6779eb1..0000000 --- a/synth.py +++ /dev/null @@ -1,59 +0,0 @@ -#!/usr/bin/env python3 -# Patch's predicate synthesizer -# Copyright (C) 2024-2025 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 . - -from argparse import ArgumentParser -from cProfile import run -from functools import partial -from pathlib import Path -from sys import stderr - -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) -print('PAC epsilon:', result.pac_epsilon, file=stderr) -for i in result.inv_mgr.invs: - write_invariant(i) - print() -- cgit 1.4.1