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

output background model in duality counterexamples

Browse source
This commit is contained in:
Ken McMillan 2013-05-29 16:40:47 -07:00
parent ee4b9d46f1
commit dfae0c5109
4 changed files with 34 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/duality/duality.h
View file

@ -257,7 +257,9 @@ namespace Duality {
};
public:
model dualModel;
private:
literals dualLabels;
std::list<stack_entry> stack;
std::vector<Term> axioms; // only saved here for printing purposes

2
src/duality/duality_rpfp.cpp
View file

@ -248,6 +248,8 @@ namespace Duality {
RPFP::Term RPFP::Localize(Edge *e, const Term &t){
timer_start("Localize");
hash_map<ast,Term> memo;
if(e->F.IndParams.size() > 0 && e->varMap.empty())
SetEdgeMaps(e); // TODO: why is this needed?
Term res = LocalizeRec(e,memo,t);
timer_stop("Localize");
return res;

8
src/duality/duality_wrapper.h
View file

@ -688,10 +688,10 @@ namespace Duality {
void show() const;
unsigned num_consts() const;
unsigned num_funcs() const;
func_decl get_const_decl(unsigned i) const;
func_decl get_func_decl(unsigned i) const;
unsigned num_consts() const {return m_model.get()->get_num_constants();}
unsigned num_funcs() const {return m_model.get()->get_num_functions();}
func_decl get_const_decl(unsigned i) const {return func_decl(ctx(),m_model.get()->get_constant(i));}
func_decl get_func_decl(unsigned i) const {return func_decl(ctx(),m_model.get()->get_function(i));}
unsigned size() const;
func_decl operator[](unsigned i) const;

26
src/muz_qe/duality_dl_interface.cpp
View file

@ -35,6 +35,7 @@ Revision History:
#include "dl_mk_coalesce.h"
#include "expr_abstract.h"
#include "model_smt2_pp.h"
#include "model_v2_pp.h"
// template class symbol_table<family_id>;
@ -218,6 +219,8 @@ expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) {
void dl_interface::reset_statistics() {
}
static hash_set<func_decl> *local_func_decls;
static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexample &cex) {
context &ctx = d->dd()->ctx;
RPFP::Node &node = *cex.root;
@ -261,6 +264,8 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
symbol name = t.get_quantifier_bound_name(j);
expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
out << " (= " << skolem << " " << cex.tree->Eval(&edge,skolem) << ")\n";
expr local_skolem = cex.tree->Localize(&edge,skolem);
(*local_func_decls).insert(local_skolem.decl());
}
}
out << " )\n";
@ -298,8 +303,29 @@ void dl_interface::display_certificate(std::ostream& out) {
else if(_d->status == StatusRefutation){
out << "(derivation\n";
// negation of the query is the last clause -- prove it
hash_set<func_decl> locals;
local_func_decls = &locals;
print_proof(this,out,_d->cex);
out << ")\n";
out << "(model \n";
::model mod(m_ctx.get_manager());
model orig_model = _d->cex.tree->dualModel;
for(unsigned i = 0; i < orig_model.num_consts(); i++){
func_decl cnst = orig_model.get_const_decl(i);
if(locals.find(cnst) == locals.end()){
expr thing = orig_model.get_const_interp(cnst);
mod.register_decl(to_func_decl(cnst.raw()),to_expr(thing.raw()));
}
}
for(unsigned i = 0; i < orig_model.num_funcs(); i++){
func_decl cnst = orig_model.get_func_decl(i);
if(locals.find(cnst) == locals.end()){
func_interp thing = orig_model.get_func_interp(cnst);
mod.register_decl(to_func_decl(cnst.raw()),thing);
}
}
model_v2_pp(out,mod);
out << ")\n";
}
}