mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

build test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-31 20:49:53 -08:00
parent 4dfdabc80f
commit 20870c43ec
4 changed files with 13 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/sat/smt/q_ematch.cpp
View file

@ -52,9 +52,9 @@ namespace q {
m_qs(s), m_qs(s),
m(ctx.get_manager()), m(ctx.get_manager()),
m_eval(ctx), m_eval(ctx),
m_infer_patterns(m, ctx.get_config()), m_qstat_gen(m, ctx.get_region()),
m_inst_queue(*this, ctx), m_inst_queue(*this, ctx),
m_qstat_gen(m, ctx.get_region()) m_infer_patterns(m, ctx.get_config())
{ {
std::function<void(euf::enode*, euf::enode*)> _on_merge = std::function<void(euf::enode*, euf::enode*)> _on_merge =
[&](euf::enode* root, euf::enode* other) { [&](euf::enode* root, euf::enode* other) {
@ -229,10 +229,8 @@ namespace q {
TRACE("q", tout << "on-binding " << mk_pp(q, m) << "\n";); TRACE("q", tout << "on-binding " << mk_pp(q, m) << "\n";);
unsigned idx = m_q2clauses[q]; unsigned idx = m_q2clauses[q];
clause& c = *m_clauses[idx]; clause& c = *m_clauses[idx];
if (!propagate(_binding, max_generation, c)) { if (!propagate(_binding, max_generation, c))
add_binding(c, pat, _binding, max_generation, min_gen, max_gen); add_binding(c, pat, _binding, max_generation, min_gen, max_gen);
insert_clause_in_queue(idx);
}
} }
bool ematch::propagate(euf::enode* const* binding, unsigned max_generation, clause& c) { bool ematch::propagate(euf::enode* const* binding, unsigned max_generation, clause& c) {
@ -314,7 +312,6 @@ namespace q {
sat::literal ematch::instantiate(clause& c, euf::enode* const* binding, lit const& l) { sat::literal ematch::instantiate(clause& c, euf::enode* const* binding, lit const& l) {
expr_ref_vector _binding(m); expr_ref_vector _binding(m);
quantifier* q = c.q();
for (unsigned i = 0; i < c.num_decls(); ++i) for (unsigned i = 0; i < c.num_decls(); ++i)
_binding.push_back(binding[i]->get_expr()); _binding.push_back(binding[i]->get_expr());
var_subst subst(m); var_subst subst(m);
@ -349,7 +346,6 @@ namespace q {
} }
} }
/** /**
* basic clausifier, assumes q has been normalized. * basic clausifier, assumes q has been normalized.
*/ */

1
src/sat/smt/q_eval.cpp
View file

@ -14,7 +14,6 @@ Author:
Nikolaj Bjorner (nbjorner) 2021-01-24 Nikolaj Bjorner (nbjorner) 2021-01-24
--*/ --*/
#pragma once
#include "sat/smt/q_eval.h" #include "sat/smt/q_eval.h"
#include "sat/smt/euf_solver.h" #include "sat/smt/euf_solver.h"

15
src/sat/smt/q_queue.cpp
View file

@ -86,11 +86,9 @@ namespace q {
quantifier_stat * stat = f.c->m_stat; quantifier_stat * stat = f.c->m_stat;
quantifier* q = f.q(); quantifier* q = f.q();
app* pat = f.b->m_pattern; app* pat = f.b->m_pattern;
unsigned min_top_generation = f.b->m_min_top_generation;
unsigned max_top_generation = f.b->m_max_top_generation;
m_vals[COST] = cost; m_vals[COST] = cost;
m_vals[MIN_TOP_GENERATION] = static_cast<float>(min_top_generation); m_vals[MIN_TOP_GENERATION] = static_cast<float>(f.b->m_min_top_generation);
m_vals[MAX_TOP_GENERATION] = static_cast<float>(max_top_generation); m_vals[MAX_TOP_GENERATION] = static_cast<float>(f.b->m_max_top_generation);
m_vals[INSTANCES] = static_cast<float>(stat->get_num_instances_curr_branch()); m_vals[INSTANCES] = static_cast<float>(stat->get_num_instances_curr_branch());
m_vals[SIZE] = static_cast<float>(stat->get_size()); m_vals[SIZE] = static_cast<float>(stat->get_size());
m_vals[DEPTH] = static_cast<float>(stat->get_depth()); m_vals[DEPTH] = static_cast<float>(stat->get_depth());
@ -138,18 +136,17 @@ namespace q {
fingerprint & f = *ent.m_qb; fingerprint & f = *ent.m_qb;
quantifier * q = f.q(); quantifier * q = f.q();
unsigned num_bindings = f.size(); unsigned num_bindings = f.size();
euf::enode * const * bindings = f.nodes(); quantifier_stat * stat = f.c->m_stat;
q::quantifier_stat * stat = f.c->m_stat;
ent.m_instantiated = true; ent.m_instantiated = true;
unsigned gen = get_new_gen(f, ent.m_cost); unsigned gen = get_new_gen(f, ent.m_cost);
if (em.propagate(bindings, gen, *f.c)) if (em.propagate(f.nodes(), gen, *f.c))
return; return;
auto* ebindings = m_subst(q, num_bindings); auto* ebindings = m_subst(q, num_bindings);
for (unsigned i = 0; i < num_bindings; ++i) for (unsigned i = 0; i < num_bindings; ++i)
ebindings[i] = bindings[i]->get_expr(); ebindings[i] = f.nodes()[i]->get_expr();
expr_ref instance = m_subst(); expr_ref instance = m_subst();
ctx.get_rewriter()(instance); ctx.get_rewriter()(instance);
if (m.is_true(instance)) { if (m.is_true(instance)) {
@ -176,7 +173,7 @@ namespace q {
if (0 == since_last_check && ctx.resource_limits_exceeded()) if (0 == since_last_check && ctx.resource_limits_exceeded())
break; break;
fingerprint& f = *curr.m_qb; fingerprint& f = *curr.m_qb;
if (curr.m_cost <= m_eager_cost_threshold) if (curr.m_cost <= m_eager_cost_threshold)
instantiate(curr); instantiate(curr);

7
src/test/simple_parser.cpp
View file

@ -16,13 +16,14 @@ Author:
Revision History: Revision History:
--*/ --*/
#include "parsers/util/cost_parser.h" #include "util/warning.h"
#include "smt/cost_evaluator.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/well_sorted.h" #include "ast/well_sorted.h"
#include "util/warning.h" #include "ast/cost_evaluator.h"
#include "ast/reg_decl_plugins.h" #include "ast/reg_decl_plugins.h"
#include "parsers/util/cost_parser.h"
void tst_simple_parser() { void tst_simple_parser() {
ast_manager m; ast_manager m;