merging from master

bin/medley

@@ -97,7 +97,7 @@ def main():
         "--seed",
         help="random seed",
         type=int,
-        default=0
+        default=hash("Go bears!") % 2**32
     )
 
     global_parser.add_argument(
@@ -147,6 +147,15 @@ def main():
         type=int,
         default=20
     )
+
+    global_parser.add_argument(
+        "--feature_setting",
+        "-f",
+        help="choose how queries are featurized",
+        type=str,
+        choices=["bow", "probes", "both"], 
+        default="both"
+    )
 
     args = global_parser.parse_args()
 
@@ -159,13 +168,14 @@ def main():
     problems = glob.glob(args.input + "/**.smt2", recursive=True)
     problems = sorted([p for p in problems if p.endswith(".smt2")])
 
+    np.random.shuffle(problems)
     if args.sample:
         problems = np.random.choice(problems, size=min(args.sample, len(problems)), replace=False)
 
     if args.timeout_manager == "expo":
         if not args.set_lambda:
             args.set_lambda = 1 / (args.timeout / len(SOLVERS))
-        timeout_manager = Exponential(args.set_lambda, args.confidence)
+        timeout_manager = Exponential(args.set_lambda, args.confidence, args.timeout)
     elif args.timeout_manager == "const":
         if not args.set_const:
             args.set_const = args.timeout // len(SOLVERS)
@@ -201,7 +211,7 @@ def main():
         with open(args.load_classifier, "rb") as f:
             classifier = dill.load(f)
 
-    execute(problems, args.output, classifier, timeout_manager, args.timeout, args.extra)
+    execute(problems, args.output, classifier, timeout_manager, args.timeout, args.feature_setting, args.extra)
 
     if args.save_classifier:
         classifier.save(args.save_classifier)

medleysolver/classifiers.py

@@ -22,7 +22,7 @@ def save(self, filename):
 class Random(ClassifierInterface):
     def get_ordering(self, point, count):
         order = list(SOLVERS.keys())
-        random.shuffle(order)
+        np.random.shuffle(order)
         return order
 
     def update(self, solved_prob, rewards):
@@ -65,7 +65,7 @@ def get_ordering(self, point, count):
             candidate = sorted(self.solved, key=lambda entry: np.linalg.norm(entry.datapoint - point))
             order = list(OrderedDict((x.solve_method, True) for x in candidate).keys())
             remaining = [x for x in SOLVERS.keys() if x not in order]
-            random.shuffle(remaining)
+            np.random.shuffle(remaining)
             order = order + remaining
 
         return list(unique_everseen(order))
@@ -107,7 +107,7 @@ def get_ordering(self, point, count):
         else: 
             order = []
         remaining = [x for x in SOLVERS.keys() if x not in order]
-        random.shuffle(remaining)
+        np.random.shuffle(remaining)
         order = order + remaining
         return list(unique_everseen(order))
 
@@ -172,7 +172,7 @@ def get_ordering(self, point, count):
 
         ps = [thetas[i].T @ point + beta.T @ point + self.alpha * np.sqrt(sigmas[i]) for i in range(len(SOLVERS))]
         ss = list(range(len(ps)))
-        random.shuffle(ss)
+        np.random.shuffle(ss)
         i_order = sorted(ss, key=lambda x: -1 * ps[x])
         order = [list(SOLVERS.keys())[int(choice)] for choice in i_order]
         return list(unique_everseen(order))
@@ -215,16 +215,14 @@ def get_nearby_times(self, point, count):
         return positions
 
     def get_ordering(self, point, count):
-        # if np.random.rand() >= self.epsilon * (self.decay ** count) and self.solved:
-        candidates = sorted(self.solved, key=lambda entry: np.linalg.norm(entry.datapoint - point))[:self.k]
-        methods = [x.solve_method for x in candidates]
-        ss = list(SOLVERS.keys())
-        random.shuffle(ss)
-        order = sorted(ss, key= lambda x: methods.count(x), reverse=True)
-        # else:
-        #     order = Random.get_ordering(self, point, count)
-
-        return list(unique_everseen(order))
+        if np.random.rand() >= self.epsilon * (self.decay ** count) and self.solved:
+            candidates = sorted(self.solved, key=lambda entry: np.linalg.norm(entry.datapoint - point))[:self.k]
+            methods = [x.solve_method for x in candidates]
+            ss = list(SOLVERS.keys())
+            np.random.shuffle(ss)
+            order = sorted(ss, key= lambda x: -1 * methods.count(x))
+        else:
+            order = Random.get_ordering(self, point, count)
 
     def update(self, solved_prob, rewards):
         #TODO: Implement pruning

medleysolver/compute_features.py

@@ -48,19 +48,23 @@ def get_syntactic_count_features(file_path):
     return features
 
 cache = {}
-def get_features(file_path,logic="",track=""):
+def get_features(file_path, feature_setting, logic="",track=""):
     if file_path not in cache:
         cache[file_path] = {}
     if logic not in cache[file_path]:
         cache[file_path][logic] = {}
     if track not in cache[file_path][logic]:
         cache[file_path][logic][track] = {}
-
-    features = get_syntactic_count_features(file_path)
-    g = z3.Goal()
-    g.add(z3.parse_smt2_file(file_path))
-    results = [z3.Probe(x)(g) for x in PROBES]
-    features = features + results
+    if feature_setting == "bow":
+        features = get_syntactic_count_features(file_path)
+    elif feature_setting == "probes":
+        g = z3.Goal()
+        g.add(z3.parse_smt2_file(file_path))
+        features = [z3.Probe(x)(g) for x in PROBES]
+    else:
+        g = z3.Goal()
+        g.add(z3.parse_smt2_file(file_path))
+        features = get_syntactic_count_features(file_path) + [z3.Probe(x)(g) for x in PROBES]
 
     cache[file_path][logic][track] = features
     return features

medleysolver/distributions.py

@@ -2,12 +2,13 @@
 import numpy as np
 
 class ExponentialDist:
-    def __init__(self, lamb, conf):
+    def __init__(self, lamb, conf, T):
         self.lamb = lamb
         self.count = 0
         self.total = 0
         self.confidence = conf
         self.naughtylist = False
+        self.T = T
 
     def add_sample(self, sample):
         self.total += sample
@@ -24,7 +25,7 @@ def add_error(self):
     def get_cutoff(self):
         if self.naughtylist:
             return 0
-        return log(1 - self.confidence) / (-1 * self.lamb)
+        return log(1 - self.confidence + np.exp(-1 * self.lamb * self.T)) / (-1 * self.lamb)
 
 class ThompsonDist(object):
     def __init__(self, n, init_a=1, init_b=1):

medleysolver/runner.py

@@ -6,13 +6,13 @@
 from medleysolver.distributions import ExponentialDist
 from medleysolver.dispatch import run_problem
 
-def execute(problems, output, classifier, time_manager, timeout, extra_time_to_first):
+def execute(problems, output, classifier, time_manager, timeout, feature_setting, extra_time_to_first):
     mean = 0
     writer = csv.writer(open(output, 'w'))
 
     for c, prob in tqdm.tqdm(enumerate(problems, 1)): 
         start = time.time()
-        point = np.array(get_features(prob))
+        point = np.array(get_features(prob, feature_setting))
         #normalizing point
         mean = (c - 1) / c * mean + 1 / c * point
         point = point / (mean+1e-9)

medleysolver/timers.py

@@ -19,8 +19,8 @@ def update(self, solver, time, timeout, success, error):
         pass
 
 class Exponential(TimerInterface):
-    def __init__(self, init_lambda, confidence):
-        self.timers = {solver:ExponentialDist(init_lambda, confidence) for solver in SOLVERS}
+    def __init__(self, init_lambda, confidence, T):
+        self.timers = {solver:ExponentialDist(init_lambda, confidence, T) for solver in SOLVERS}
 
     def get_timeout(self, solver, position):
         return self.timers[solver].get_cutoff()