mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
add API for fixing tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e5541bad17
commit
d795792304
|
@ -364,6 +364,7 @@ namespace pdr {
|
|||
}
|
||||
vector<unsigned_vector> transversal;
|
||||
while (l_true == ctx.check()) {
|
||||
IF_VERBOSE(0, ctx.display(verbose_stream()););
|
||||
model_ref md;
|
||||
ctx.get_model(md);
|
||||
expr_ref_vector lits(m);
|
||||
|
|
|
@ -105,6 +105,11 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
lbool rel_context::saturate() {
|
||||
scoped_query sq(m_context);
|
||||
return saturate(sq);
|
||||
}
|
||||
|
||||
lbool rel_context::saturate(scoped_query& sq) {
|
||||
m_context.ensure_closed();
|
||||
bool time_limit = m_context.soft_timeout()!=0;
|
||||
|
|
|
@ -48,6 +48,8 @@ namespace datalog {
|
|||
|
||||
void reset_tables();
|
||||
|
||||
lbool saturate(scoped_query& sq);
|
||||
|
||||
public:
|
||||
rel_context(context& ctx);
|
||||
|
||||
|
@ -109,7 +111,7 @@ namespace datalog {
|
|||
|
||||
void display_profile(std::ostream& out);
|
||||
|
||||
lbool saturate(scoped_query& sq);
|
||||
lbool saturate();
|
||||
|
||||
};
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue