From 62836f9f37c0f9c21f317a51de5803e26d019d8b Mon Sep 17 00:00:00 2001 From: FedericoAureliano Date: Tue, 13 Oct 2020 15:01:32 -0700 Subject: [PATCH] 540 learning configurations. Need to pull gamma option in --- bin/medley | 10 +++++++++- clean.sh | 3 +++ full_test.sh | 9 --------- medleysolver/runner.py | 15 +++++++++++---- ordermisses.py | 2 +- process.py | 6 +++--- runmedley.sh | 43 +++++++++++++++++++++++++----------------- timemisses.py | 2 +- 8 files changed, 54 insertions(+), 36 deletions(-) create mode 100644 clean.sh delete mode 100755 full_test.sh diff --git a/bin/medley b/bin/medley index 936fafe..7dadba7 100755 --- a/bin/medley +++ b/bin/medley @@ -38,6 +38,14 @@ def main(): choices=["full", "single", "greedy"] ) + global_parser.add_argument( + "--reward", + help="the kind of reward to give", + type=str, + default="bump", + choices=["binary", "bump", "exp"] + ) + global_parser.add_argument( "--classifier", "-c", @@ -211,7 +219,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.feature_setting, args.extra) + execute(problems, args.output, classifier, timeout_manager, args.timeout, args.feature_setting, args.extra, args.reward) if args.save_classifier: classifier.save(args.save_classifier) diff --git a/clean.sh b/clean.sh new file mode 100644 index 0000000..2165f08 --- /dev/null +++ b/clean.sh @@ -0,0 +1,3 @@ +for learner in thompson neighbor nearest knearest random MLP linear exp3; do + rm $1/${learner}* +done \ No newline at end of file diff --git a/full_test.sh b/full_test.sh deleted file mode 100755 index c3d651c..0000000 --- a/full_test.sh +++ /dev/null @@ -1,9 +0,0 @@ -medley ./tmp/ nearest.csv -c neighbor -medley ./tmp/ random.csv -c random -medley ./tmp/ neural.csv -c MLP -medley ./tmp/ thompson.csv -c thompson -medley ./tmp/ linucb.csv -c linear -medley ./tmp/ z3.csv -c preset --preset Z3 -medley ./tmp/ cvc4.csv -c preset --preset CVC4 -medley ./tmp/ yices.csv -c preset --preset YICES -medley ./tmp/ boolector.csv -c preset --preset BOOLECTOR diff --git a/medleysolver/runner.py b/medleysolver/runner.py index 890df2c..fb3e322 100644 --- a/medleysolver/runner.py +++ b/medleysolver/runner.py @@ -6,7 +6,7 @@ from medleysolver.distributions import ExponentialDist from medleysolver.dispatch import run_problem -def execute(problems, output, classifier, time_manager, timeout, feature_setting, extra_time_to_first): +def execute(problems, output, classifier, time_manager, timeout, feature_setting, extra_time_to_first, reward): mean = 0 writer = csv.writer(open(output, 'w')) @@ -29,15 +29,16 @@ def execute(problems, output, classifier, time_manager, timeout, feature_setting writer.writerow(solved_prob) -def apply_ordering(problem, order, timeout, time_manager, extra_time_to_first, times): +def apply_ordering(problem, order, timeout, time_manager, extra_time_to_first, times, reward): elapsed = 0 rewards = [-1 for _ in SOLVERS] # negative rewards should be ignored. time_spent = [] + timeout = int(timeout) budgets = [int(time_manager.get_timeout(solver, times))+1 for solver in order] for i in range(len(budgets)): - budgets[i] = min(budgets[i], int(timeout - sum(budgets[:i]))) + budgets[i] = min(budgets[i], max(0, int(timeout - sum(budgets[:i])))) if sum(budgets) < timeout: if extra_time_to_first: @@ -54,7 +55,13 @@ def apply_ordering(problem, order, timeout, time_manager, extra_time_to_first, t time_for_solver = int(timeout - elapsed) + 1 if i == len(order) - 1 else budgets[i] res = run_problem(solver, SOLVERS[solver], problem, time_for_solver) - reward = 1 + ((1 - res.elapsed / timeout) ** 4) if is_solved(res.result) else 0 + if reward == "binary": + reward = 1 if is_solved(res.result) else 0 + elif reward == "bump": + reward = 1 + ((1 - res.elapsed / timeout) ** 4) if is_solved(res.result) else 0 + elif reward == "exp": + reward = (1 - res.elapsed / timeout) ** 4 if is_solved(res.result) else 0 + rewards[list(SOLVERS.keys()).index(solver)] = reward time_spent.append(res.elapsed) diff --git a/ordermisses.py b/ordermisses.py index 1859a63..b157a11 100755 --- a/ordermisses.py +++ b/ordermisses.py @@ -24,7 +24,7 @@ for row in spamreader: r = float(row[3]) if isinstance(row[3], str) else row[3] r = r if r < 60 else 60 - r = r if row[4] != "error" else 60 + r = r if row[4] != "error" and "timeout" not in row[4] else 60 cols[solver][row[0]] = r print("choice, answer, problem") diff --git a/process.py b/process.py index 692a722..d23c2ba 100755 --- a/process.py +++ b/process.py @@ -27,6 +27,6 @@ totaltimes = [str(sum(time)) for time in times] totalcount = [str(sum(map(lambda x: 1 if x == "sat" or x == "unsat" else 0, answer))) for answer in answers] -print(",".join(solvers)) -print(",".join(totaltimes)) -print(",".join(totalcount)) +print("solver, total time, total solved") +for i in range(len(solvers)): + print(",".join([str(solvers[i]), str(totaltimes[i]), str(totalcount[i])])) diff --git a/runmedley.sh b/runmedley.sh index 14a0c6c..a68f9b4 100644 --- a/runmedley.sh +++ b/runmedley.sh @@ -1,17 +1,26 @@ -medley ./$1/ ./$1/thompson.csv -c thompson -medley ./$1/ ./$1/nearest.csv -c neighbor -medley ./$1/ ./$1/knearest.csv -c knearest --k 10 -medley ./$1/ ./$1/random.csv -c random -medley ./$1/ ./$1/MLP.csv -c MLP -medley ./$1/ ./$1/linear.csv -c linear -medley ./$1/ ./$1/exp3.csv -c exp3 - -medley ./$1/ ./$1/thompson_only.csv -c thompson --timeout_manager const --set_const 60 -medley ./$1/ ./$1/nearest_only.csv -c neighbor --timeout_manager const --set_const 60 -medley ./$1/ ./$1/knearest_only.csv -c knearest --k 10 --timeout_manager const --set_const 60 -medley ./$1/ ./$1/random_only.csv -c random --timeout_manager const --set_const 60 -medley ./$1/ ./$1/MLP_only.csv -c MLP --timeout_manager const --set_const 60 -medley ./$1/ ./$1/linear_only.csv -c linear --timeout_manager const --set_const 60 -medley ./$1/ ./$1/exp3_only.csv -c exp3 --timeout_manager const --set_const 60 - -medley ./$1/ ./$1/timenearest.csv -c knearest --k 10 --timeout_manager nearest --time_k 20 \ No newline at end of file +for seed in 0 1; do + for learner in thompson neighbor knearest random MLP linear exp3a exp3b exp3c exp3d; do + if [ $learner == exp3a ] + then + learnconfig="exp3 --gamma 0.07" + elif [ $learner == exp3b ] + then + learnconfig="exp3 --gamma 0.1" + elif [ $learner == exp3c ] + then + learnconfig="exp3 --gamma 0.25" + elif [ $learner == exp3c ] + then + learnconfig="exp3 --gamma 0.5" + else + learnconfig=$learner + fi + for feature in both probes bow; do + for reward in binary bump exp; do + medley ./$1/ ./$1/${learner}_${feature}_${reward}_const_${seed}.csv --classifier $learnconfig --seed $seed --feature_setting $feature --reward $reward --timeout_manager const --set_const 60 + medley ./$1/ ./$1/${learner}_${feature}_${reward}_expo_${seed}.csv --classifier $learnconfig --seed $seed --feature_setting $feature --reward $reward --timeout_manager expo + medley ./$1/ ./$1/${learner}_${feature}_${reward}_nearest_${seed}.csv --classifier $learnconfig --seed $seed --feature_setting $feature --reward $reward --timeout_manager nearest --time_k 20 + done + done + done +done \ No newline at end of file diff --git a/timemisses.py b/timemisses.py index f1e05b2..cd11381 100755 --- a/timemisses.py +++ b/timemisses.py @@ -24,7 +24,7 @@ for row in spamreader: r = float(row[3]) if isinstance(row[3], str) else row[3] r = r if r < 60 else 60 - r = r if row[4] != "error" else 60 + r = r if row[4] != "error" and "timeout" not in row[4] else 60 cols[solver][row[0]] = r print("solver, answer, guess, problem")