mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Moving skolems to lemma

Browse source
This commit is contained in:
Yakir Vizel 2017-12-18 09:14:38 -05:00 • committed by Arie Gurfinkel
parent ea73acef45
commit f51c07adf6
2 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -40,7 +40,7 @@ Notes:
#include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_util.h"
#include "ast/proofs/proof_checker.h"
#include "ast/proof_checker/proof_checker.h"
#include "smt/smt_value_sort.h"
#include "ast/scoped_proof.h"
#include "muz/spacer/spacer_qe_project.h"
@ -1177,7 +1177,7 @@ void pred_transformer::inherit_properties(pred_transformer& other)
lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
m_ref_count(0), m(manager),
m_body(body, m), m_cube(m),
m_bindings(m), m_lvl(lvl),
m_bindings(m), m_zks(m), m_lvl(lvl),
m_pob(nullptr), m_new_pob(false) {
SASSERT(m_body);
normalize(m_body, m_body);
@ -1186,16 +1186,17 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
lemma::lemma(pob_ref const &p) :
m_ref_count(0), m(p->get_ast_manager()),
m_body(m), m_cube(m),
m_bindings(m), m_lvl(p->level()),
m_pob(p), m_new_pob(m_pob) {SASSERT(m_pob);}
m_bindings(m), m_zks(m), m_lvl(p->level()),
m_pob(p), m_new_pob(m_pob) {SASSERT(m_pob); m_pob->get_skolems(m_zks);}
lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) :
m_ref_count(0),
m(p->get_ast_manager()),
m_body(m), m_cube(m),
m_bindings(m), m_lvl(p->level()),
m_bindings(m), m_zks(m), m_lvl(p->level()),
m_pob(p), m_new_pob(m_pob)
{
m_pob->get_skolems(m_zks);
update_cube(p, cube);
set_level(lvl);
}
@ -1210,9 +1211,9 @@ void lemma::mk_expr_core() {
m_body = ::push_not(::mk_and(m_cube));
normalize(m_body, m_body);
if (!m_pob->is_ground() && has_zk_const(m_body)) {
if (!m_zks.empty() && has_zk_const(m_body)) {
app_ref_vector zks(m);
m_pob->get_skolems(zks);
zks.append(m_zks);
zks.reverse();
expr_abstract(m, 0,
zks.size(), (expr* const*)zks.c_ptr(), m_body,
@ -2163,8 +2164,8 @@ bool context::validate()
expr_ref_vector refs(m);
expr_ref tmp(m);
model_ref model;
model_converter_ref mc;
vector<relation_info> rs;
model_converter_ref mc;
get_level_property(m_inductive_lvl, refs, rs);
inductive_property ex(m, mc, rs);
ex.to_model(model);

2
src/muz/spacer/spacer_context.h
View file

@ -111,6 +111,7 @@ class lemma {
expr_ref m_body;
expr_ref_vector m_cube;
app_ref_vector m_bindings;
app_ref_vector m_zks;
unsigned m_lvl;
pob_ref m_pob;
bool m_new_pob;
@ -133,6 +134,7 @@ public:
pob_ref &get_pob() {return m_pob;}
inline unsigned weakness();
void set_skolems(app_ref_vector &zks) { m_zks.append(zks); }
unsigned level () const {return m_lvl;}
void set_level (unsigned lvl) {m_lvl = lvl;}
app_ref_vector& get_bindings() {return m_bindings;}