mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

finish consequence fast path code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-28 20:15:47 -07:00
parent 4958edeb42
commit 5c99405db3
2 changed files with 30 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/python/z3.py
View file

@ -6127,8 +6127,14 @@ class Solver(Z3PPObject):
return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
def consequences(self, assumptions, variables):
"""Determine fixed values for the variables based on the solver state and assumptions.
documentation TBD
"""Determine fixed values for the variables based on the solver state and assumptions.
>>> s = Solver()
>>> a, b, c, d = Bools('a b c d')
>>> s.add(Implies(a,b), Implies(b, c))
>>> s.consequences([a],[b,c,d])
(sat, [Implies(a, b), Implies(a, c)])
>>> s.consequences([Not(c),d],[a,b,c,d])
(sat, [Implies(Not(c), Not(a)), Implies(Not(c), Not(b)), Implies(True, Not(c)), Implies(True, d)])
"""
if isinstance(assumptions, list):
_asms = AstVector(None, self.ctx)

35
src/smt/smt_consequences.cpp
View file

@ -66,11 +66,14 @@ namespace smt {
case b_justification::AXIOM: {
break;
}
case b_justification::JUSTIFICATION:
justification* j = js.get_justification();
// warning_msg("TODO: extract antecedents from theory justification");
// std::cout << "TODO: justification\n";
case b_justification::JUSTIFICATION: {
literal_vector literals;
m_conflict_resolution->justification2literals(js.get_justification(), literals);
for (unsigned j = 0; j < literals.size(); ++j) {
s |= m_antecedents.find(literals[j].var());
}
break;
}
}
}
m_antecedents.insert(lit.var(), s);
@ -100,6 +103,7 @@ namespace smt {
lbool context::get_consequences(expr_ref_vector const& assumptions,
expr_ref_vector const& vars, expr_ref_vector& conseq) {
m_antecedents.reset();
lbool is_sat = check(assumptions.size(), assumptions.c_ptr());
if (is_sat != l_true) {
return is_sat;
@ -111,19 +115,20 @@ namespace smt {
}
model_ref mdl;
get_model(mdl);
expr_ref_vector trail(m_manager);
ast_manager& m = m_manager;
expr_ref_vector trail(m);
model_evaluator eval(*mdl.get());
expr_ref val(m_manager);
expr_ref val(m);
for (unsigned i = 0; i < vars.size(); ++i) {
eval(vars[i], val);
if (m_manager.is_value(val)) {
if (m.is_value(val)) {
trail.push_back(val);
var2val.insert(vars[i], val);
}
}
extract_fixed_consequences(0, var2val, _assumptions, conseq);
unsigned num_units = assigned_literals().size();
app_ref eq(m_manager);
app_ref eq(m);
TRACE("context",
tout << "vars: " << vars.size() << "\n";
tout << "lits: " << num_units << "\n";);
@ -136,8 +141,8 @@ namespace smt {
unsigned current_level = m_scope_lvl;
literal lit;
if (m_manager.is_bool(e)) {
lit = literal(get_bool_var(e), m_manager.is_true(val));
if (m.is_bool(e)) {
lit = literal(get_bool_var(e), m.is_true(val));
}
else {
eq = mk_eq_atom(e, val);
@ -163,17 +168,21 @@ namespace smt {
var2val.erase(e);
}
else if (get_assign_level(lit) > get_search_level()) {
TRACE("context", tout << "Retry fixing: " << mk_pp(e, m_manager) << "\n";);
TRACE("context", tout << "Retry fixing: " << mk_pp(e, m) << "\n";);
pop_to_search_lvl();
continue;
}
else {
TRACE("context", tout << "Fixed: " << mk_pp(e, m_manager) << "\n";);
TRACE("context", tout << "Fixed: " << mk_pp(e, m) << "\n";);
}
extract_fixed_consequences(num_units, var2val, _assumptions, conseq);
num_units = assigned_literals().size();
if (var2val.contains(e)) {
TRACE("context", tout << "TBD: Fixed value to " << mk_pp(e, m_manager) << " was not retrieved\n";);
TRACE("context", tout << "Fixed value to " << mk_pp(e, m) << " was not processed\n";);
expr_ref fml(m);
fml = m.mk_eq(e, var2val.find(e));
fml = m.mk_implies(antecedent2fml(m_antecedents[lit.var()]), fml);
conseq.push_back(fml);
var2val.erase(e);
SASSERT(get_assignment(lit) == l_false);
}