mirror of
https://github.com/Z3Prover/z3
synced 2025-07-25 13:47:01 +00:00
consolidate throttling
This commit is contained in:
parent
f32066762c
commit
832cfb3c41
5 changed files with 148 additions and 0 deletions
24
src/math/lp/nla_throttle.cpp
Normal file
24
src/math/lp/nla_throttle.cpp
Normal file
|
@ -0,0 +1,24 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Author:
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
--*/
|
||||
#include "math/lp/nla_throttle.h"
|
||||
#include "util/trace.h"
|
||||
|
||||
namespace nla {
|
||||
|
||||
bool nla_throttle::insert_new_impl(const signature& sig) {
|
||||
if (m_seen.contains(sig)) {
|
||||
TRACE(nla_solver, tout << "throttled lemma generation\n";);
|
||||
return true; // Already seen, throttle
|
||||
}
|
||||
|
||||
m_seen.insert(sig);
|
||||
m_trail.push(insert_map(m_seen, sig));
|
||||
return false; // New, don't throttle
|
||||
}
|
||||
|
||||
} // namespace nla
|
Loading…
Add table
Add a link
Reference in a new issue