mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
commit
618e1bee5b
|
@ -2039,6 +2039,7 @@ namespace z3 {
|
|||
expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
|
||||
expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
|
||||
expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
|
||||
expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
|
||||
expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
|
||||
friend std::ostream & operator<<(std::ostream & out, solver const & s);
|
||||
|
||||
|
|
|
@ -6646,6 +6646,11 @@ class Solver(Z3PPObject):
|
|||
"""
|
||||
return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
|
||||
|
||||
def non_units(self):
|
||||
"""Return an AST vector containing all atomic formulas in solver state that are not units.
|
||||
"""
|
||||
return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
|
||||
|
||||
def statistics(self):
|
||||
"""Return statistics for the last `check()`.
|
||||
|
||||
|
|
|
@ -262,25 +262,27 @@ expr_ref_vector solver::get_non_units(ast_manager& m) {
|
|||
get_assertions(fmls);
|
||||
family_id bfid = m.get_basic_family_id();
|
||||
expr_mark marked;
|
||||
unsigned sz0 = fmls.size();
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
expr* f = fmls.get(i);
|
||||
if (marked.is_marked(f)) continue;
|
||||
marked.mark(f);
|
||||
if (!is_app(f)) {
|
||||
result.push_back(f);
|
||||
if (i >= sz0) result.push_back(f);
|
||||
continue;
|
||||
}
|
||||
app* _f = to_app(f);
|
||||
if (_f->get_family_id() == bfid) {
|
||||
// basic objects are true/false/and/or/not/=/distinct and proof objects (that are not Boolean)
|
||||
if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) {
|
||||
fmls.append(_f->get_num_args(), _f->get_args());
|
||||
}
|
||||
else if (m.is_eq(f) || m.is_distinct(f)) {
|
||||
result.push_back(f);
|
||||
if (i >= sz0) result.push_back(f);
|
||||
}
|
||||
}
|
||||
else {
|
||||
result.push_back(f);
|
||||
if (i >= sz0) result.push_back(f);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
|
|
Loading…
Reference in a new issue