mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

#7418 - circumvent use of timer threads to make WASM integration of z3 easier

Browse source 
The scoped_timer uses a std::therad. Spawning this thread fails in cases of WASM.
Instead of adapting builds and using async features at the level of WASM and the client, we expose a specialized version of z3 that doesn't use threads at all, neither for solvers nor for timers.
The tradeoff is that the periodic poll that checks for timeout directly queries the global clock each time.
We characterize it as based on polling.
This commit is contained in:
Nikolaj Bjorner 2024-11-21 11:20:05 -08:00
parent 94f0aff47f
commit 71bad7159b
8 changed files with 124 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -20,6 +20,7 @@ Notes:
#include "cmd_context/cmd_context.h"
#include "solver/combined_solver.h"
#include "solver/tactic2solver.h"
#include "tactic/tactical.h"
#include "tactic/smtlogics/qfbv_tactic.h"
#include "tactic/smtlogics/qflia_tactic.h"
#include "tactic/smtlogics/qfnia_tactic.h"
@ -67,27 +68,27 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
else if (logic=="QF_BV")
return mk_qfbv_tactic(m, p);
else if (logic=="QF_IDL")
return mk_qfidl_tactic(m, p);
return annotate_tactic("qfidl-tactic", mk_qfidl_tactic(m, p));
else if (logic=="QF_LIA")
return mk_qflia_tactic(m, p);
return annotate_tactic("qflia-tactic", mk_qflia_tactic(m, p));
else if (logic=="QF_LRA")
return mk_qflra_tactic(m, p);
return annotate_tactic("qflra-tactic", mk_qflra_tactic(m, p));
else if (logic=="QF_NIA")
return mk_qfnia_tactic(m, p);
return annotate_tactic("qfnia-tactic", mk_qfnia_tactic(m, p));
else if (logic=="QF_NRA")
return mk_qfnra_tactic(m, p);
return annotate_tactic("qfnra-tactic", mk_qfnra_tactic(m, p));
else if (logic=="QF_AUFLIA")
return mk_qfauflia_tactic(m, p);
return annotate_tactic("qfauflia-tactic", mk_qfauflia_tactic(m, p));
else if (logic=="QF_AUFBV")
return mk_qfaufbv_tactic(m, p);
return annotate_tactic("qfaufbv-tactic", mk_qfaufbv_tactic(m, p));
else if (logic=="QF_ABV")
return mk_qfaufbv_tactic(m, p);
return annotate_tactic("qfaufbv-tactic", mk_qfaufbv_tactic(m, p));
else if (logic=="QF_UFBV")
return mk_qfufbv_tactic(m, p);
return annotate_tactic("qfufbv-tactic", mk_qfufbv_tactic(m, p));
else if (logic=="AUFLIA")
return mk_auflia_tactic(m, p);
return annotate_tactic("auflia-tactic", mk_auflia_tactic(m, p));
else if (logic=="AUFLIRA")
return mk_auflira_tactic(m, p);
return annotate_tactic("auflira-tactic", mk_auflira_tactic(m, p));
else if (logic=="AUFNIRA")
return mk_aufnira_tactic(m, p);
else if (logic=="UFNIA")
@ -101,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
else if (logic=="LIA")
return mk_lia_tactic(m, p);
else if (logic=="UFBV")
return mk_ufbv_tactic(m, p);
return annotate_tactic("ufbv", mk_ufbv_tactic(m, p));
else if (logic=="BV")
return mk_ufbv_tactic(m, p);
else if (logic=="QF_FP")