mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

fixed interp api bug (github issue #47)

Browse source
This commit is contained in:
Ken McMillan 2015-04-20 12:30:15 -07:00
parent af444beb2e
commit 5f37b1d32f
2 changed files with 29 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/interp/iz3interp.cpp
View file

@ -398,10 +398,27 @@ public:
s.assert_expr(to_expr(cnsts[i].raw())); s.assert_expr(to_expr(cnsts[i].raw()));
} }
void get_proof_assumptions(z3pf proof, std::vector<ast> &cnsts, hash_set<ast> &memo){
if(memo.find(proof) != memo.end())return;
memo.insert(proof);
pfrule dk = pr(proof);
if(dk == PR_ASSERTED)
cnsts.push_back(conc(proof));
else {
unsigned nprems = num_prems(proof);
for(unsigned i = 0; i < nprems; i++){
z3pf arg = prem(proof,i);
get_proof_assumptions(arg,cnsts,memo);
}
}
}
iz3interp(ast_manager &_m_manager) iz3interp(ast_manager &_m_manager)
: iz3base(_m_manager) {} : iz3base(_m_manager) {}
}; };
void iz3interpolate(ast_manager &_m_manager, void iz3interpolate(ast_manager &_m_manager,
ast *proof, ast *proof,
const ptr_vector<ast> &cnsts, const ptr_vector<ast> &cnsts,
@ -475,6 +492,13 @@ void iz3interpolate(ast_manager &_m_manager,
_cnsts[i] = itp.cook(cnsts[i]); _cnsts[i] = itp.cook(cnsts[i]);
iz3mgr::ast _proof = itp.cook(proof); iz3mgr::ast _proof = itp.cook(proof);
iz3mgr::ast _tree = itp.cook(tree); iz3mgr::ast _tree = itp.cook(tree);
// if consts isn't provided, we can reconstruct it
if(_cnsts.empty()){
hash_set<iz3mgr::ast> memo;
itp.get_proof_assumptions(_proof,_cnsts,memo);
}
itp.proof_to_interpolant(_proof,_cnsts,_tree,_interps,options); itp.proof_to_interpolant(_proof,_cnsts,_tree,_interps,options);
interps.resize(_interps.size()); interps.resize(_interps.size());
for(unsigned i = 0; i < interps.size(); i++) for(unsigned i = 0; i < interps.size(); i++)

6
src/interp/iz3interp.h
View file

@ -67,7 +67,11 @@ void iz3interpolate(ast_manager &_m_manager,
interpolation_options_struct * options = 0); interpolation_options_struct * options = 0);
/* Compute an interpolant from a proof. This version uses the ast /* Compute an interpolant from a proof. This version uses the ast
representation, for compatibility with the new API. */ representation, for compatibility with the new API. Here, cnsts is
a vector of all the assertions in the proof. This can be
over-approximated by the set of all assertions in the
solver. However, if it is empty it will be reconstructed from the
proof, so it can be considered a hint. */
void iz3interpolate(ast_manager &_m_manager, void iz3interpolate(ast_manager &_m_manager,
ast *proof, ast *proof,