mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-08 03:48:38 -07:00
parent 7722bf1a55
commit bd59fceaec
2 changed files with 36 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/expr_abstract.h
View file

@ -33,7 +33,7 @@ public:
}; };
void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result); void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result);
inline expr_ref expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n) { expr_ref r(m); expr_abstract(m, base, num_bound, bound, n); return r; } inline expr_ref expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n) { expr_ref r(m); expr_abstract(m, base, num_bound, bound, n, r); return r; }
expr_ref mk_forall(ast_manager& m, unsigned num_bound, app* const* bound, expr* n); expr_ref mk_forall(ast_manager& m, unsigned num_bound, app* const* bound, expr* n);
expr_ref mk_exists(ast_manager& m, unsigned num_bound, app* const* bound, expr* n); expr_ref mk_exists(ast_manager& m, unsigned num_bound, app* const* bound, expr* n);

74
src/muz/spacer/spacer_context.cpp
View file

@ -24,35 +24,32 @@ Notes:
#include <sstream> #include <sstream>
#include <iomanip> #include <iomanip>
#include "muz/base/dl_util.h" #include "util/util.h"
#include "util/timeit.h"
#include "util/luby.h"
#include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter.h"
#include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
#include "util/util.h"
#include "muz/spacer/spacer_prop_solver.h"
#include "muz/spacer/spacer_context.h"
#include "muz/spacer/spacer_generalizers.h"
#include "ast/for_each_expr.h"
#include "muz/base/dl_rule_set.h"
#include "smt/tactic/unit_subsumption_tactic.h"
#include "model/model_smt2_pp.h"
#include "muz/transforms/dl_mk_rule_inliner.h"
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/proofs/proof_checker.h" #include "ast/proofs/proof_checker.h"
#include "smt/smt_value_sort.h" #include "ast/for_each_expr.h"
#include "ast/scoped_proof.h" #include "ast/scoped_proof.h"
#include "muz/spacer/spacer_qe_project.h"
#include "tactic/core/blast_term_ite_tactic.h"
#include "util/timeit.h"
#include "util/luby.h"
#include "ast/rewriter/expr_safe_replace.h" #include "ast/rewriter/expr_safe_replace.h"
#include "ast/expr_abstract.h" #include "ast/expr_abstract.h"
#include "model/model_smt2_pp.h"
#include "tactic/core/blast_term_ite_tactic.h"
#include "smt/tactic/unit_subsumption_tactic.h"
#include "smt/smt_value_sort.h"
#include "smt/smt_solver.h" #include "smt/smt_solver.h"
#include "muz/base/dl_util.h"
#include "muz/spacer/spacer_prop_solver.h"
#include "muz/spacer/spacer_context.h"
#include "muz/spacer/spacer_generalizers.h"
#include "muz/base/dl_rule_set.h"
#include "muz/transforms/dl_mk_rule_inliner.h"
#include "muz/spacer/spacer_qe_project.h"
#include "muz/spacer/spacer_sat_answer.h" #include "muz/spacer/spacer_sat_answer.h"
#define WEAKNESS_MAX 65535 #define WEAKNESS_MAX 65535
@ -441,8 +438,8 @@ derivation::premise::premise (pred_transformer &pt, unsigned oidx,
} }
if (aux_vars) if (aux_vars)
for (unsigned i = 0, sz = aux_vars->size (); i < sz; ++i) for (app* v : *aux_vars)
m_ovars.push_back(m.mk_const(sm.n2o(aux_vars->get(i)->get_decl(), m_oidx))); m_ovars.push_back(m.mk_const(sm.n2o(v->get_decl(), m_oidx)));
} }
derivation::premise::premise (const derivation::premise &p) : derivation::premise::premise (const derivation::premise &p) :
@ -466,9 +463,8 @@ void derivation::premise::set_summary (expr * summary, bool must,
{ m_ovars.push_back(m.mk_const(sm.o2o(m_pt.sig(i), 0, m_oidx))); } { m_ovars.push_back(m.mk_const(sm.o2o(m_pt.sig(i), 0, m_oidx))); }
if (aux_vars) if (aux_vars)
for (unsigned i = 0, sz = aux_vars->size (); i < sz; ++i) for (app* v : *aux_vars)
m_ovars.push_back (m.mk_const (sm.n2o (aux_vars->get (i)->get_decl (), m_ovars.push_back (m.mk_const (sm.n2o (v->get_decl (), m_oidx)));
m_oidx)));
} }
@ -541,25 +537,25 @@ void lemma::mk_expr_core() {
m_body = ::push_not(m_body); m_body = ::push_not(m_body);
if (!m_zks.empty() && has_zk_const(m_body)) { if (!m_zks.empty() && has_zk_const(m_body)) {
app_ref_vector zks(m); app_ref_vector zks(m);
zks.append(m_zks); zks.append(m_zks);
zks.reverse(); zks.reverse();
expr_abstract(m, 0, m_body = expr_abstract(m, 0,
zks.size(), (expr* const*)zks.c_ptr(), m_body, zks.size(), (expr* const*)zks.c_ptr(), m_body);
m_body); ptr_buffer<sort> sorts;
ptr_buffer<sort> sorts; svector<symbol> names;
svector<symbol> names; for (app* z : zks) {
for (unsigned i=0, sz=zks.size(); i < sz; ++i) { sorts.push_back(get_sort(z));
sorts.push_back(get_sort(zks.get(i))); names.push_back(z->get_decl()->get_name());
names.push_back(zks.get(i)->get_decl()->get_name()); }
} m_body = m.mk_quantifier(forall_k, zks.size(),
m_body = m.mk_quantifier(forall_k, zks.size(), sorts.c_ptr(),
sorts.c_ptr(), names.c_ptr(),
names.c_ptr(), m_body, 15, symbol(m_body->get_id()));
m_body, 15, symbol(m_body->get_id()));
} }
SASSERT(m_body); SASSERT(m_body);
} }
void lemma::mk_cube_core() { void lemma::mk_cube_core() {
if (!m_cube.empty()) {return;} if (!m_cube.empty()) {return;}
expr_ref cube(m); expr_ref cube(m);