mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

add hook for induction

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-29 12:06:53 -07:00
parent fd911a5563
commit 9f6a733ff6
3 changed files with 20 additions and 11 deletions

24
src/smt/smt_context.cpp
View file

@ -270,18 +270,14 @@ namespace smt {
}
d.m_phase_available = true;
d.m_phase = !l.sign();
CTRACE("assign_core", l.var() == 13, tout << (decision?"decision: ":"propagating: ") << l << " ";
/*display_literal(tout, l);*/
tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n";
/*display(tout, j);*/
);
TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
display_literal_smt2(tout, l) << "\n";
tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n";
/*display(tout, j);*/
);
TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
CTRACE("relevancy", l.var() == 13,
tout << "is_atom: " << d.is_atom() << " is relevant: "
<< is_relevant_core(l) << " relevancy-lvl: " << relevancy_lvl() << "\n";);
if (d.is_atom() && (relevancy_lvl() == 0 || (relevancy_lvl() == 1 && !d.is_quantifier()) || is_relevant_core(l))) {
CTRACE("assign_core", l.var() == 13, tout << "propagation queue\n";);
m_atom_propagation_queue.push_back(l);
}
@ -1655,6 +1651,16 @@ namespace smt {
!m_th_diseq_propagation_queue.empty();
}
/**
\brief retrieve facilities for creating induction lemmas.
*/
induction& context::get_induction() {
if (!m_induction) {
m_induction = alloc(induction, *this, get_manager());
}
return *m_induction;
}
/**
\brief unit propagation.
Cancelation is not safe during propagation at base level because

6
src/smt/smt_context.h
View file

@ -34,6 +34,7 @@ Revision History:
#include "smt/smt_statistics.h"
#include "smt/smt_conflict_resolution.h"
#include "smt/smt_relevancy.h"
#include "smt/smt_induction.h"
#include "smt/smt_case_split_queue.h"
#include "smt/smt_almost_cg_table.h"
#include "smt/smt_failure.h"
@ -185,6 +186,7 @@ namespace smt {
unsigned m_simp_qhead;
int m_simp_counter; //!< can become negative
scoped_ptr<case_split_queue> m_case_split_queue;
scoped_ptr<induction> m_induction;
double m_bvar_inc;
bool m_phase_cache_on;
unsigned m_phase_counter; //!< auxiliary variable used to decide when to turn on/off phase caching
@ -848,7 +850,7 @@ namespace smt {
void remove_lit_occs(clause const& cls, unsigned num_bool_vars);
void add_lit_occs(clause const& cls);
public:
public:
void ensure_internalized(expr* e);
@ -1267,6 +1269,8 @@ namespace smt {
public:
bool can_propagate() const;
induction& get_induction();
// Retrieve arithmetic values.
bool get_arith_lo(expr* e, rational& lo, bool& strict);
bool get_arith_up(expr* e, rational& up, bool& strict);

1
src/smt/smt_induction.cpp
View file

@ -240,7 +240,6 @@ void create_induction_lemmas::create_lemmas(expr* t, expr* sk, abstraction& a, l
sort* s = m.get_sort(sk);
if (!m_dt.is_datatype(s))
return;
family_id fid = s->get_family_id();
expr_ref alpha = a.m_term;
auto const& eqs = a.m_eqs;
literal_vector common_literals;