mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

make get_consequence call skip check-sat if a model is already there

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-30 18:05:19 -08:00
parent 8dde60f634
commit a4d5c4a00a
3 changed files with 15 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/sat/sat_solver.cpp
View file

@ -123,6 +123,7 @@ namespace sat {
// -----------------------
bool_var solver::mk_var(bool ext, bool dvar) {
m_model_is_current = false;
m_stats.m_mk_var++;
bool_var v = m_level.size();
m_watches.push_back(watch_list());
@ -148,6 +149,7 @@ namespace sat {
}
void solver::mk_clause(unsigned num_lits, literal * lits) {
m_model_is_current = false;
DEBUG_CODE({
for (unsigned i = 0; i < num_lits; i++)
SASSERT(m_eliminated[lits[i].var()] == false);
@ -3118,7 +3120,11 @@ namespace sat {
lbool solver::get_consequences(literal_vector const& asms, bool_var_vector const& vars, vector<literal_vector>& conseq) {
literal_vector lits;
lbool is_sat = check(asms.size(), asms.c_ptr());
lbool is_sat = l_true;
if (!m_model_is_current) {
is_sat = check(asms.size(), asms.c_ptr());
}
if (is_sat != l_true) {
return is_sat;
}
@ -3212,6 +3218,12 @@ namespace sat {
<< " unfixed: " << lits.size() - conseq.size() - vars.size()
<< ")\n";);
if (!vars.empty() &&
m_config.m_restart_max != 0 &&
m_config.m_restart_max <= num_iterations) {
return l_undef;
}
}
return l_true;
}

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -257,7 +257,7 @@ public:
r = internalize_vars(vars, bvars);
r = m_solver.get_consequences(m_asms, bvars, lconseq);
if (r != l_true) return r;
if (r == l_false) return r;
// build map from bound variables to
// the consequences that cover them.

2
src/smt/theory_pb.cpp
View file

@ -1752,7 +1752,7 @@ namespace smt {
// verbose_stream() << "(pb.conflict min size: " << l_size << ")\n";
// s_min_l_size = l_size;
//}
//IF_VERBOSE(1, verbose_stream() << "(pb.conflict " << m_ineq_literals.size() << " " << m_lemma.size() << "\n";);
IF_VERBOSE(1, verbose_stream() << "(pb.conflict " << m_ineq_literals.size() << " " << m_lemma.size() << ")\n";);
switch(is_true) {
case l_true:
UNREACHABLE();