mirror of
https://github.com/Z3Prover/z3
synced 2025-04-11 11:43:36 +00:00
142 lines
4.5 KiB
C++
142 lines
4.5 KiB
C++
/*++
|
|
Copyright (c) 2020 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
q_ematch.h
|
|
|
|
Abstract:
|
|
|
|
E-matching quantifier instantiation plugin
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 2021-01-24
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "util/nat_set.h"
|
|
#include "ast/quantifier_stat.h"
|
|
#include "ast/pattern/pattern_inference.h"
|
|
#include "solver/solver.h"
|
|
#include "sat/smt/sat_th.h"
|
|
#include "sat/smt/q_mam.h"
|
|
#include "sat/smt/q_clause.h"
|
|
#include "sat/smt/q_fingerprint.h"
|
|
#include "sat/smt/q_queue.h"
|
|
#include "sat/smt/q_eval.h"
|
|
|
|
namespace euf {
|
|
class solver;
|
|
}
|
|
|
|
namespace q {
|
|
|
|
class solver;
|
|
|
|
class ematch {
|
|
struct stats {
|
|
unsigned m_num_instantiations;
|
|
unsigned m_num_propagations;
|
|
unsigned m_num_conflicts;
|
|
unsigned m_num_redundant;
|
|
|
|
stats() { reset(); }
|
|
|
|
void reset() {
|
|
memset(this, 0, sizeof(*this));
|
|
}
|
|
};
|
|
|
|
struct remove_binding;
|
|
struct insert_binding;
|
|
struct pop_clause;
|
|
struct scoped_mark_reset;
|
|
struct reset_in_queue;
|
|
|
|
|
|
euf::solver& ctx;
|
|
solver& m_qs;
|
|
ast_manager& m;
|
|
eval m_eval;
|
|
quantifier_stat_gen m_qstat_gen;
|
|
fingerprints m_fingerprints;
|
|
scoped_ptr<binding> m_tmp_binding;
|
|
unsigned m_tmp_binding_capacity { 0 };
|
|
queue m_inst_queue;
|
|
pattern_inference_rw m_infer_patterns;
|
|
scoped_ptr<q::mam> m_mam, m_lazy_mam;
|
|
ptr_vector<clause> m_clauses;
|
|
obj_map<quantifier, unsigned> m_q2clauses;
|
|
vector<unsigned_vector> m_watch; // expr_id -> clause-index*
|
|
stats m_stats;
|
|
expr_fast_mark1 m_mark;
|
|
unsigned m_generation_propagation_threshold{ 3 };
|
|
ptr_vector<app> m_ground;
|
|
bool m_in_queue_set{ false };
|
|
nat_set m_node_in_queue;
|
|
nat_set m_clause_in_queue;
|
|
unsigned m_qhead { 0 };
|
|
unsigned_vector m_clause_queue;
|
|
|
|
binding* alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top);
|
|
void add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top);
|
|
|
|
sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b);
|
|
|
|
void ensure_ground_enodes(expr* e);
|
|
void ensure_ground_enodes(clause const& c);
|
|
|
|
void instantiate(binding& b, clause& c);
|
|
sat::literal instantiate(clause& c, euf::enode* const* binding, lit const& l);
|
|
|
|
// register as callback into egraph.
|
|
void on_merge(euf::enode* root, euf::enode* other);
|
|
void insert_to_propagate(unsigned node_id);
|
|
void insert_clause_in_queue(unsigned idx);
|
|
|
|
void add_watch(euf::enode* root, unsigned clause_idx);
|
|
void init_watch(expr* e, unsigned clause_idx);
|
|
void init_watch(clause& c);
|
|
|
|
void attach_ground_pattern_terms(expr* pat);
|
|
clause* clausify(quantifier* q);
|
|
|
|
fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation);
|
|
void set_tmp_binding(fingerprint& fp);
|
|
|
|
public:
|
|
|
|
ematch(euf::solver& ctx, solver& s);
|
|
|
|
bool operator()();
|
|
|
|
bool propagate(bool flush);
|
|
|
|
void init_search();
|
|
|
|
void add(quantifier* q);
|
|
|
|
void collect_statistics(statistics& st) const;
|
|
|
|
void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing);
|
|
|
|
// callback from mam
|
|
void on_binding(quantifier* q, app* pat, euf::enode* const* binding, unsigned max_generation, unsigned min_gen, unsigned max_gen);
|
|
|
|
// callbacks from queue
|
|
lbool evaluate(euf::enode* const* binding, clause& c) { return m_eval(binding, c); }
|
|
|
|
void add_instantiation(clause& c, binding& b, sat::literal lit);
|
|
|
|
bool propagate(euf::enode* const* binding, unsigned max_generation, clause& c, bool& new_propagation);
|
|
|
|
std::ostream& display(std::ostream& out) const;
|
|
|
|
std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const;
|
|
|
|
};
|
|
|
|
}
|