mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 09:35:32 +00:00
ensure limit children are safe for race conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f8a804ba56
commit
4132fc2d91
6 changed files with 51 additions and 33 deletions
|
@ -41,7 +41,6 @@ public:
|
|||
- parameter setting (updt_params)
|
||||
- statistics
|
||||
- results based on check_sat_result API
|
||||
- interruption (set_cancel)
|
||||
*/
|
||||
class solver : public check_sat_result {
|
||||
public:
|
||||
|
@ -105,14 +104,6 @@ public:
|
|||
*/
|
||||
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
|
||||
|
||||
/**
|
||||
\brief Interrupt this solver.
|
||||
*/
|
||||
//void cancel() { set_cancel(true); }
|
||||
/**
|
||||
\brief Reset the interruption.
|
||||
*/
|
||||
//void reset_cancel() { set_cancel(false); }
|
||||
|
||||
/**
|
||||
\brief Set a progress callback procedure that is invoked by this solver during check_sat.
|
||||
|
@ -156,9 +147,6 @@ public:
|
|||
~scoped_push() { if (!m_nopop) s.pop(1); }
|
||||
void disable_pop() { m_nopop = true; }
|
||||
};
|
||||
|
||||
protected:
|
||||
//virtual void set_cancel(bool f) = 0;
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue