mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
another module level ifdef for #4382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d603bd7e3b
commit
c8c02060ee
|
@ -569,7 +569,6 @@ void seq_decl_plugin::init() {
|
|||
sort* str2TintT[3] = { strT, strT, intT };
|
||||
sort* seqAintT[2] = { seqA, intT };
|
||||
sort* seq3A[3] = { seqA, seqA, seqA };
|
||||
sort* charTcharT[2] = { m_char, m_char };
|
||||
m_sigs.resize(LAST_SEQ_OP);
|
||||
// TBD: have (par ..) construct and load parameterized signature from premable.
|
||||
m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA);
|
||||
|
@ -609,6 +608,7 @@ void seq_decl_plugin::init() {
|
|||
m_sigs[OP_STRING_CONST] = nullptr;
|
||||
#if _USE_UNICODE
|
||||
m_sigs[OP_CHAR_CONST] = nullptr;
|
||||
sort* charTcharT[2] = { m_char, m_char };
|
||||
m_sigs[OP_CHAR_LE] = alloc(psig, m, "char.<=", 0, 2, charTcharT, boolT);
|
||||
#endif
|
||||
m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
|
||||
|
|
|
@ -28,7 +28,7 @@ namespace smt {
|
|||
seq(m),
|
||||
dl(),
|
||||
m_qhead(0),
|
||||
m_nc_functor(*this),
|
||||
m_nc_functor(),
|
||||
m_var_value_hash(*this),
|
||||
m_var_value_eq(*this),
|
||||
m_var_value_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_var_value_hash, m_var_value_eq)
|
||||
|
|
|
@ -35,9 +35,8 @@ namespace smt {
|
|||
|
||||
class nc_functor {
|
||||
literal_vector m_literals;
|
||||
seq_unicode& m_super;
|
||||
public:
|
||||
nc_functor(seq_unicode& s): m_super(s) {}
|
||||
nc_functor() {}
|
||||
void operator()(literal const& l) {
|
||||
if (l != null_literal) m_literals.push_back(l);
|
||||
}
|
||||
|
|
|
@ -28,6 +28,14 @@ Notes:
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef SINGLE_THREAD
|
||||
|
||||
tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
|
||||
throw default_exception("parallel tactic is disabled in single threaded mode");
|
||||
}
|
||||
|
||||
#else
|
||||
|
||||
#include <thread>
|
||||
#include <mutex>
|
||||
#include <cmath>
|
||||
|
@ -795,3 +803,4 @@ tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
|
|||
return alloc(parallel_tactic, s, p);
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
Loading…
Reference in a new issue