michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/tactic): clean up try_for

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-22 15:51:17 -08:00
parent 9fd594533d
commit df96068caa
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/tactic/tactic.cpp
View file

@ -131,13 +131,13 @@ tactic try_for(tactic t, unsigned ms, unsigned check_ms) {
try {
auto start = std::chrono::steady_clock::now();
std::chrono::milliseconds d(ms);
std::chrono::milliseconds one(1);
std::chrono::milliseconds small(check_ms);
while (!done) {
auto curr = std::chrono::steady_clock::now();
if (std::chrono::duration_cast<std::chrono::milliseconds>(curr - start) > d)
break;
check_interrupted();
std::this_thread::sleep_for(one);
std::this_thread::sleep_for(small);
}
th.request_interrupt();
th.join();

3
src/library/tactic/tactic.h
View file

@ -9,7 +9,6 @@ Author: Leonardo de Moura
#include <utility>
#include <memory>
#include <mutex>
#include "util/interrupt.h"
#include "util/lazy_list.h"
#include "library/io_state.h"
#include "library/tactic/proof_state.h"
@ -63,6 +62,6 @@ tactic now_tactic();
tactic assumption_tactic();
tactic then(tactic t1, tactic t2);
tactic orelse(tactic t1, tactic t2);
tactic try_for(tactic t, unsigned ms, unsigned check_ms = g_small_sleep);
tactic try_for(tactic t, unsigned ms, unsigned check_ms = 1);
tactic repeat(tactic t1);
}