mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
Merge pull request #1737 from Nils-Becker/master
Equality Explanation Logging
This commit is contained in:
Nikolaj Bjorner
GitHub
commit
a2d078f6f5
11 changed files with 166 additions and 26 deletions
|
|
@ -1847,7 +1847,10 @@ namespace smt {
|
|||
enode * m_n2;
|
||||
enode * m_app;
|
||||
const bind * m_b;
|
||||
ptr_vector<enode> m_used_enodes;
|
||||
|
||||
// equalities used for pattern match. The first element of the tuple gives the argument (or null) of some term that was matched against some higher level
|
||||
// structure of the trigger, the second element gives the term that argument is replaced with in order to match the trigger. Used for logging purposes only.
|
||||
vector<std::tuple<enode *, enode *>> m_used_enodes;
|
||||
unsigned m_curr_used_enodes_size;
|
||||
ptr_vector<enode> m_pattern_instances; // collect the pattern instances... used for computing min_top_generation and max_top_generation
|
||||
unsigned_vector m_min_top_generation, m_max_top_generation;
|
||||
|
|
@ -1864,11 +1867,11 @@ namespace smt {
|
|||
m_pool.recycle(v);
|
||||
}
|
||||
|
||||
void update_max_generation(enode * n) {
|
||||
void update_max_generation(enode * n, enode * prev) {
|
||||
m_max_generation = std::max(m_max_generation, n->get_generation());
|
||||
|
||||
if (m_ast_manager.has_trace_stream())
|
||||
m_used_enodes.push_back(n);
|
||||
m_used_enodes.push_back(std::make_tuple(prev, n));
|
||||
}
|
||||
|
||||
// We have to provide the number of expected arguments because we have flat-assoc applications such as +.
|
||||
|
|
@ -1877,7 +1880,7 @@ namespace smt {
|
|||
enode * first = curr;
|
||||
do {
|
||||
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
|
||||
update_max_generation(curr);
|
||||
update_max_generation(curr, first);
|
||||
return curr;
|
||||
}
|
||||
curr = curr->get_next();
|
||||
|
|
@ -1890,7 +1893,7 @@ namespace smt {
|
|||
curr = curr->get_next();
|
||||
while (curr != first) {
|
||||
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
|
||||
update_max_generation(curr);
|
||||
update_max_generation(curr, first);
|
||||
return curr;
|
||||
}
|
||||
curr = curr->get_next();
|
||||
|
|
@ -1914,7 +1917,7 @@ namespace smt {
|
|||
do {
|
||||
if (n->get_decl() == f &&
|
||||
n->get_arg(0)->get_root() == m_args[0]) {
|
||||
update_max_generation(n);
|
||||
update_max_generation(n, first);
|
||||
return true;
|
||||
}
|
||||
n = n->get_next();
|
||||
|
|
@ -1929,7 +1932,7 @@ namespace smt {
|
|||
if (n->get_decl() == f &&
|
||||
n->get_arg(0)->get_root() == m_args[0] &&
|
||||
n->get_arg(1)->get_root() == m_args[1]) {
|
||||
update_max_generation(n);
|
||||
update_max_generation(n, first);
|
||||
return true;
|
||||
}
|
||||
n = n->get_next();
|
||||
|
|
@ -1949,7 +1952,7 @@ namespace smt {
|
|||
break;
|
||||
}
|
||||
if (i == num_args) {
|
||||
update_max_generation(n);
|
||||
update_max_generation(n, first);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
@ -2196,7 +2199,7 @@ namespace smt {
|
|||
if (bp.m_it == bp.m_end)
|
||||
return nullptr;
|
||||
m_top++;
|
||||
update_max_generation(*(bp.m_it));
|
||||
update_max_generation(*(bp.m_it), nullptr);
|
||||
return *(bp.m_it);
|
||||
}
|
||||
|
||||
|
|
@ -2277,7 +2280,7 @@ namespace smt {
|
|||
|
||||
if (m_ast_manager.has_trace_stream()) {
|
||||
m_used_enodes.reset();
|
||||
m_used_enodes.push_back(n);
|
||||
m_used_enodes.push_back(std::make_tuple(nullptr, n)); // null indicates that n was matched against the trigger at the top-level
|
||||
}
|
||||
|
||||
m_pc = t->get_root();
|
||||
|
|
@ -2382,6 +2385,10 @@ namespace smt {
|
|||
SASSERT(m_n2 != 0);
|
||||
if (m_n1->get_root() != m_n2->get_root())
|
||||
goto backtrack;
|
||||
|
||||
// we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log
|
||||
m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
|
||||
|
||||
m_pc = m_pc->m_next;
|
||||
goto main_loop;
|
||||
|
||||
|
|
@ -2776,7 +2783,7 @@ namespace smt {
|
|||
m_pattern_instances.pop_back();
|
||||
m_pattern_instances.push_back(m_app);
|
||||
// continue succeeded
|
||||
update_max_generation(m_app);
|
||||
update_max_generation(m_app, nullptr); // null indicates a top-level match
|
||||
TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager););
|
||||
m_num_args = c->m_num_args;
|
||||
m_oreg = c->m_oreg;
|
||||
|
|
@ -3878,7 +3885,7 @@ namespace smt {
|
|||
}
|
||||
#endif
|
||||
|
||||
void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) override {
|
||||
void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) override {
|
||||
TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";);
|
||||
#ifdef Z3DEBUG
|
||||
if (m_check_missing_instances) {
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ Revision History:
|
|||
|
||||
#include "ast/ast.h"
|
||||
#include "smt/smt_types.h"
|
||||
#include <tuple>
|
||||
|
||||
namespace smt {
|
||||
/**
|
||||
|
|
@ -57,7 +58,7 @@ namespace smt {
|
|||
|
||||
virtual void display(std::ostream& out) = 0;
|
||||
|
||||
virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) = 0;
|
||||
virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) = 0;
|
||||
|
||||
virtual bool is_shared(enode * n) const = 0;
|
||||
|
||||
|
|
|
|||
|
|
@ -562,6 +562,7 @@ namespace smt {
|
|||
invert_trans(n1);
|
||||
n1->m_trans.m_target = n2;
|
||||
n1->m_trans.m_justification = js;
|
||||
n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
|
||||
SASSERT(r1->trans_reaches(n1));
|
||||
// ---------------
|
||||
// r1 -> .. -> n1 -> n2 -> ... -> r2
|
||||
|
|
@ -741,12 +742,14 @@ namespace smt {
|
|||
eq_justification js = n->m_trans.m_justification;
|
||||
prev->m_trans.m_target = nullptr;
|
||||
prev->m_trans.m_justification = null_eq_justification;
|
||||
prev->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
|
||||
while (curr != nullptr) {
|
||||
SASSERT(prev->trans_reaches(n));
|
||||
enode * new_curr = curr->m_trans.m_target;
|
||||
eq_justification new_js = curr->m_trans.m_justification;
|
||||
curr->m_trans.m_target = prev;
|
||||
curr->m_trans.m_justification = js;
|
||||
curr->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
|
||||
prev = curr;
|
||||
js = new_js;
|
||||
curr = new_curr;
|
||||
|
|
@ -1040,6 +1043,7 @@ namespace smt {
|
|||
SASSERT(r1->trans_reaches(n1));
|
||||
n1->m_trans.m_target = nullptr;
|
||||
n1->m_trans.m_justification = null_eq_justification;
|
||||
n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
|
||||
invert_trans(r1);
|
||||
// ---------------
|
||||
// n1 -> ... -> r1
|
||||
|
|
@ -1786,7 +1790,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
|
||||
unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes) {
|
||||
unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode *>> & used_enodes) {
|
||||
return m_qmanager->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -49,6 +49,7 @@ Revision History:
|
|||
#include "util/timer.h"
|
||||
#include "util/statistics.h"
|
||||
#include "solver/progress_callback.h"
|
||||
#include <tuple>
|
||||
|
||||
// there is a significant space overhead with allocating 1000+ contexts in
|
||||
// the case that each context only references a few expressions.
|
||||
|
|
@ -970,7 +971,7 @@ namespace smt {
|
|||
bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
|
||||
|
||||
bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
|
||||
unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes);
|
||||
unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
|
||||
|
||||
void set_global_generation(unsigned generation) { m_generation = generation; }
|
||||
|
||||
|
|
|
|||
|
|
@ -577,7 +577,7 @@ namespace smt {
|
|||
case b_justification::BIN_CLAUSE: {
|
||||
literal l2 = j.get_literal();
|
||||
out << "bin-clause ";
|
||||
display_literal_verbose(out, l2);
|
||||
display_literal(out, l2);
|
||||
break;
|
||||
}
|
||||
case b_justification::CLAUSE: {
|
||||
|
|
@ -590,7 +590,7 @@ namespace smt {
|
|||
out << "justification " << j.get_justification()->get_from_theory() << ": ";
|
||||
literal_vector lits;
|
||||
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
|
||||
display_literals_verbose(out, lits);
|
||||
display_literals(out, lits);
|
||||
break;
|
||||
}
|
||||
default:
|
||||
|
|
|
|||
|
|
@ -47,6 +47,7 @@ namespace smt {
|
|||
n->m_cgc_enabled = cgc_enabled;
|
||||
n->m_iscope_lvl = iscope_lvl;
|
||||
n->m_lbl_hash = -1;
|
||||
n->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
|
||||
unsigned num_args = n->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
enode * arg = app2enode[owner->get_arg(i)->get_id()];
|
||||
|
|
|
|||
|
|
@ -38,6 +38,15 @@ namespace smt {
|
|||
}
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Indicates whether the proof for membership in an equivalence class is already logged.
|
||||
*/
|
||||
enum logged_status {
|
||||
NOT_LOGGED, //!< Proof is not logged or logged information is not up-to-date.
|
||||
BEING_LOGGED, //!< We are currently in the process of logging all relevant information. This is used to prevent looping when logging congruence steps.
|
||||
LOGGED //!< Proof is logged and logged information is still up-to-date.
|
||||
};
|
||||
|
||||
/** \ brief Use sparse maps in SMT solver.
|
||||
|
||||
Define this to use hash maps rather than vectors over ast
|
||||
|
|
@ -105,6 +114,7 @@ namespace smt {
|
|||
enode_vector m_parents; //!< Parent enodes of the equivalence class.
|
||||
theory_var_list m_th_var_list; //!< List of theories that 'care' about this enode.
|
||||
trans_justification m_trans; //!< A justification for the enode being equal to its root.
|
||||
logged_status m_proof_logged_status; //!< Indicates that the proof for the enode being equal to its root is in the log.
|
||||
signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern
|
||||
approx_set m_lbls;
|
||||
approx_set m_plbls;
|
||||
|
|
@ -113,6 +123,7 @@ namespace smt {
|
|||
friend class context;
|
||||
friend class euf_manager;
|
||||
friend class conflict_resolution;
|
||||
friend class quantifier_manager;
|
||||
|
||||
|
||||
theory_var_list * get_th_var_list() {
|
||||
|
|
@ -361,6 +372,10 @@ namespace smt {
|
|||
|
||||
theory_var get_th_var(theory_id th_id) const;
|
||||
|
||||
trans_justification get_trans_justification() {
|
||||
return m_trans;
|
||||
}
|
||||
|
||||
unsigned get_generation() const {
|
||||
return m_generation;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -33,6 +33,7 @@ Revision History:
|
|||
#include "smt/smt_context.h"
|
||||
#include "smt/smt_model_finder.h"
|
||||
#include "model/model_pp.h"
|
||||
#include <tuple>
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
|
@ -518,7 +519,7 @@ namespace smt {
|
|||
void model_checker::assert_new_instances() {
|
||||
TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";);
|
||||
ptr_buffer<enode> bindings;
|
||||
ptr_vector<enode> dummy;
|
||||
vector<std::tuple<enode *, enode *>> dummy;
|
||||
for (instance const& inst : m_new_instances) {
|
||||
quantifier * q = inst.m_q;
|
||||
if (m_context->b_internalized(q)) {
|
||||
|
|
|
|||
|
|
@ -104,6 +104,90 @@ namespace smt {
|
|||
return m_plugin->is_shared(n);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its
|
||||
equivalence class are in the log and up-to-date.
|
||||
*/
|
||||
void log_justification_to_root(std::ostream & log, enode *en) {
|
||||
enode *root = en->get_root();
|
||||
for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
|
||||
if (it->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
|
||||
it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
|
||||
log_single_justification(log, it);
|
||||
it->m_proof_logged_status = smt::logged_status::LOGGED;
|
||||
} else if (it->m_proof_logged_status != smt::logged_status::BEING_LOGGED && it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
|
||||
|
||||
// When the justification of an argument changes m_proof_logged_status is not reset => We need to check if the proofs of all arguments are logged.
|
||||
it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
|
||||
const unsigned num_args = it->get_num_args();
|
||||
enode *target = it->get_trans_justification().m_target;
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
log_justification_to_root(log, it->get_arg(i));
|
||||
log_justification_to_root(log, target->get_arg(i));
|
||||
}
|
||||
it->m_proof_logged_status = smt::logged_status::LOGGED;
|
||||
}
|
||||
}
|
||||
if (root->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
|
||||
log << "[eq-expl] #" << root->get_owner_id() << " root\n";
|
||||
root->m_proof_logged_status = smt::logged_status::LOGGED;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log
|
||||
equalities needed by the step (e.g. argument equalities for congruence steps).
|
||||
*/
|
||||
void log_single_justification(std::ostream & out, enode *en) {
|
||||
smt::literal lit;
|
||||
unsigned num_args;
|
||||
enode *target = en->get_trans_justification().m_target;
|
||||
theory_id th_id;
|
||||
|
||||
switch (en->get_trans_justification().m_justification.get_kind()) {
|
||||
case smt::eq_justification::kind::EQUATION:
|
||||
lit = en->get_trans_justification().m_justification.get_literal();
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " lit #" << m_context.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
case smt::eq_justification::kind::AXIOM:
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
case smt::eq_justification::kind::CONGRUENCE:
|
||||
if (!en->get_trans_justification().m_justification.used_commutativity()) {
|
||||
num_args = en->get_num_args();
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
log_justification_to_root(out, en->get_arg(i));
|
||||
log_justification_to_root(out, target->get_arg(i));
|
||||
}
|
||||
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " cg";
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")";
|
||||
}
|
||||
out << " ; #" << target->get_owner_id() << "\n";
|
||||
|
||||
break;
|
||||
} else {
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
}
|
||||
case smt::eq_justification::kind::JUSTIFICATION:
|
||||
th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory();
|
||||
if (th_id != null_theory_id) {
|
||||
symbol const theory = m().get_family_name(th_id);
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n";
|
||||
} else {
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
|
||||
}
|
||||
break;
|
||||
default:
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
bool add_instance(quantifier * q, app * pat,
|
||||
unsigned num_bindings,
|
||||
enode * const * bindings,
|
||||
|
|
@ -111,7 +195,7 @@ namespace smt {
|
|||
unsigned max_generation,
|
||||
unsigned min_top_generation,
|
||||
unsigned max_top_generation,
|
||||
ptr_vector<enode> & used_enodes) {
|
||||
vector<std::tuple<enode *, enode *>> & used_enodes) {
|
||||
max_generation = std::max(max_generation, get_generation(q));
|
||||
if (m_num_instances > m_params.m_qi_max_instances) {
|
||||
return false;
|
||||
|
|
@ -121,15 +205,39 @@ namespace smt {
|
|||
if (f) {
|
||||
if (has_trace_stream()) {
|
||||
std::ostream & out = trace_stream();
|
||||
out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id();
|
||||
|
||||
// In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables
|
||||
// is used. We need to make sure that all of these equalities appear in the log.
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
log_justification_to_root(out, bindings[i]);
|
||||
}
|
||||
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig != nullptr) {
|
||||
log_justification_to_root(out, orig);
|
||||
log_justification_to_root(out, substituted);
|
||||
}
|
||||
}
|
||||
|
||||
// At this point all relevant equalities for the match are logged.
|
||||
out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id() << " #" << pat->get_id();
|
||||
for (unsigned i = 0; i < num_bindings; i++) {
|
||||
// I don't want to use mk_pp because it creates expressions for pretty printing.
|
||||
// This nasty side-effect may change the behavior of Z3.
|
||||
out << " #" << bindings[i]->get_owner_id();
|
||||
}
|
||||
out << " ;";
|
||||
for (enode* n : used_enodes)
|
||||
out << " #" << n->get_owner_id();
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig == nullptr)
|
||||
out << " #" << substituted->get_owner_id();
|
||||
else {
|
||||
out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";
|
||||
}
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
|
||||
|
|
@ -296,12 +404,12 @@ namespace smt {
|
|||
unsigned max_generation,
|
||||
unsigned min_top_generation,
|
||||
unsigned max_top_generation,
|
||||
ptr_vector<enode> & used_enodes) {
|
||||
vector<std::tuple<enode *, enode *>> & used_enodes) {
|
||||
return m_imp->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_generation, used_enodes);
|
||||
}
|
||||
|
||||
bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation) {
|
||||
ptr_vector<enode> tmp;
|
||||
vector<std::tuple<enode *, enode *>> tmp;
|
||||
return add_instance(q, nullptr, num_bindings, bindings, def, generation, generation, generation, tmp);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -23,6 +23,7 @@ Revision History:
|
|||
#include "util/statistics.h"
|
||||
#include "util/params.h"
|
||||
#include "smt/smt_types.h"
|
||||
#include <tuple>
|
||||
|
||||
class proto_model;
|
||||
struct smt_params;
|
||||
|
|
@ -58,7 +59,7 @@ namespace smt {
|
|||
unsigned max_generation,
|
||||
unsigned min_top_generation,
|
||||
unsigned max_top_generation,
|
||||
ptr_vector<enode> & used_enodes);
|
||||
vector<std::tuple<enode *, enode *>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
|
||||
bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation = 0);
|
||||
|
||||
void init_search_eh();
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@ Revision History:
|
|||
#include "smt/smt_context.h"
|
||||
#include "smt/smt_quick_checker.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include <tuple>
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
|
@ -197,7 +198,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool quick_checker::process_candidates(quantifier * q, bool unsat) {
|
||||
ptr_vector<enode> empty_used_enodes;
|
||||
vector<std::tuple<enode *, enode *>> empty_used_enodes;
|
||||
buffer<unsigned> szs;
|
||||
buffer<unsigned> it;
|
||||
for (unsigned i = 0; i < m_num_bindings; i++) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue