diff --git a/cozy/main.py b/cozy/main.py index 29bbef60..620b6385 100755 --- a/cozy/main.py +++ b/cozy/main.py @@ -10,6 +10,8 @@ import datetime import pickle +from multiprocessing import Value + from cozy import parse from cozy import codegen from cozy import common @@ -55,6 +57,8 @@ def run(): args = parser.parse_args() opts.read(args) + improve_count = Value('i', 0) + if args.resume: with common.open_maybe_stdin(args.file or "-", mode="rb") as f: ast = pickle.load(f) @@ -138,7 +142,8 @@ def callback(impl): ast = synthesis.improve_implementation( ast, timeout = datetime.timedelta(seconds=args.timeout), - progress_callback = callback) + progress_callback = callback, + improve_count=improve_count) if server is not None: server.join() @@ -190,3 +195,5 @@ def callback(impl): f.write("share_info = {}\n".format(repr(share_info))) print("Implementation was dumped to {}".format(save_failed_codegen_inputs.value)) raise + + print("Number of improvements done: {}".format(improve_count.value)) diff --git a/cozy/synthesis/core.py b/cozy/synthesis/core.py index dab42c6b..16ae6818 100644 --- a/cozy/synthesis/core.py +++ b/cozy/synthesis/core.py @@ -16,6 +16,8 @@ import itertools from typing import Callable +from multiprocessing import Value + from cozy.syntax import ( INT, BOOL, TMap, Op, @@ -41,6 +43,8 @@ from .acceleration import try_optimize from .enumeration import Enumerator, Fingerprint, retention_policy +import threading + eliminate_vars = Option("eliminate-vars", bool, False) enable_blacklist = Option("enable-blacklist", bool, False, description='If enabled, skip expressions that have been ' + @@ -102,7 +106,8 @@ def improve( hints : [Exp] = (), examples : [{str:object}] = (), cost_model : CostModel = None, - ops : [Op] = ()): + ops : [Op] = (), + improve_count : Value = None): """Improve the target expression using enumerative synthesis. This function is a generator that yields increasingly better and better @@ -271,6 +276,10 @@ def improve( print("Now watching {} targets".format(len(watched_targets))) break + if improve_count is not None: + with improve_count.get_lock(): + improve_count.value += 1 + SearchInfo = namedtuple("SearchInfo", ( "context", "targets", diff --git a/cozy/synthesis/high_level_interface.py b/cozy/synthesis/high_level_interface.py index 9e0444c8..1edb6a5b 100644 --- a/cozy/synthesis/high_level_interface.py +++ b/cozy/synthesis/high_level_interface.py @@ -11,6 +11,7 @@ import sys import os from queue import Empty +from multiprocessing import Value from cozy.common import typechecked, OrderedSet, LINE_BUFFER_MODE from cozy.syntax import Query, Op, Exp, EVar, EAll @@ -43,7 +44,8 @@ def __init__(self, k, hints : [Exp] = [], freebies : [Exp] = [], - ops : [Op] = []): + ops : [Op] = [], + improve_count = None): super().__init__() self.state = state self.assumptions = assumptions @@ -55,6 +57,7 @@ def __init__(self, self.freebies = freebies self.ops = ops self.k = k + self.improve_count = improve_count def __str__(self): return "ImproveQueryJob[{}]".format(self.q.name) def run(self): @@ -82,7 +85,8 @@ def run(self): hints=self.hints, stop_callback=lambda: self.stop_requested, cost_model=cost_model, - ops=self.ops)): + ops=self.ops, + improve_count=self.improve_count)): new_rep, new_ret = unpack_representation(expr) self.k(new_rep, new_ret) @@ -94,7 +98,8 @@ def run(self): def improve_implementation( impl : Implementation, timeout : datetime.timedelta = datetime.timedelta(seconds=60), - progress_callback : Callable[[Implementation], Any] = None) -> Implementation: + progress_callback : Callable[[Implementation], Any] = None, + improve_count : Value = None) -> Implementation: """Improve an implementation. This function tries to synthesize a better version of the given @@ -142,7 +147,8 @@ def reconcile_jobs(): k=(lambda q: lambda new_rep, new_ret: solutions_q.put((q, new_rep, new_ret)))(q), hints=[EStateVar(c).with_type(c.type) for c in impl.concretization_functions.values()], freebies=[e for (v, e) in impl.concretization_functions.items() if EVar(v) in states_maintained_by_q], - ops=impl.op_specs)) + ops=impl.op_specs, + improve_count=improve_count)) # figure out what old jobs we can stop impl_query_names = set(q.name for q in impl.query_specs)