diff options
| author | Nguyễn Gia Phong <cnx@loang.net> | 2025-10-16 18:27:38 +0900 |
|---|---|---|
| committer | Nguyễn Gia Phong <cnx@loang.net> | 2025-10-16 18:27:38 +0900 |
| commit | d8090bb73f404a9abff5b7cc9cfdd8cdb1ee4d5f (patch) | |
| tree | f61d4bf27654b153329dc75459bbcd8022fff577 /synth.py | |
| parent | 6090724f0b2d7a577c2662cddb639e036e275e4f (diff) | |
| download | taosc-d8090bb73f404a9abff5b7cc9cfdd8cdb1ee4d5f.tar.gz | |
Read values from files
Diffstat (limited to 'synth.py')
| -rw-r--r-- | synth.py | 59 |
1 files changed, 0 insertions, 59 deletions
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 <https://www.gnu.org/licenses/>. - -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() |
