3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

duality fix plus mbqi option

This commit is contained in:
Ken McMillan 2014-03-04 18:38:08 -08:00
parent 19dbd02e13
commit 83a774ac79
5 changed files with 25 additions and 2 deletions

View file

@ -2847,7 +2847,12 @@ namespace Duality {
}
void RPFP::InterpolateByCases(Node *root, Node *node){
timer_start("InterpolateByCases");
bool axioms_added = false;
hash_set<ast> axioms_needed;
const std::vector<expr> &theory = ls->get_axioms();
for(unsigned i = 0; i < theory.size(); i++)
axioms_needed.insert(theory[i]);
aux_solver.push();
AddEdgeToSolver(node->Outgoing);
node->Annotation.SetEmpty();
@ -2869,7 +2874,17 @@ namespace Duality {
check_result foo = Check(root);
if(foo != unsat)
throw "should be unsat";
AddToProofCore(*core);
std::vector<expr> assumps, axioms_to_add;
slvr().get_proof().get_assumptions(assumps);
for(unsigned i = 0; i < assumps.size(); i++){
(*core).insert(assumps[i]);
if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
axioms_to_add.push_back(assumps[i]);
axioms_needed.erase(assumps[i]);
}
}
// AddToProofCore(*core);
Transformer old_annot = node->Annotation;
SolveSingleNode(root,node);
@ -2882,6 +2897,9 @@ namespace Duality {
node->Annotation.Formula = node->Annotation.Formula.simplify();
}
for(unsigned i = 0; i < axioms_to_add.size(); i++)
aux_solver.add(axioms_to_add[i]);
if(node->Annotation.IsEmpty()){
if(!axioms_added){
// add the axioms in the off chance they are useful
@ -2906,6 +2924,7 @@ namespace Duality {
delete proof_core; // shouldn't happen
proof_core = core;
aux_solver.pop(1);
timer_stop("InterpolateByCases");
}
void RPFP::Generalize(Node *root, Node *node){

View file

@ -43,7 +43,8 @@ namespace Duality {
if(models)
p.set_bool("model", true);
p.set_bool("unsat_core", true);
p.set_bool("mbqi",true);
bool mbqi = c.get_config().get().get_bool("mbqi",true);
p.set_bool("mbqi",mbqi); // just to test
p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants
p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants
if(true || extensional)

View file

@ -182,6 +182,7 @@ namespace Duality {
void set(char const * param, char const * value) { m_config.set(param,value); }
void set(char const * param, bool value) { m_config.set(param,value); }
void set(char const * param, int value) { m_config.set(param,value); }
config &get_config() {return m_config;}
symbol str_symbol(char const * s);
symbol int_symbol(int n);

View file

@ -74,6 +74,7 @@ def_module_params('fixedpoint',
('stratified_inlining', BOOL, False, 'DUALITY: Use stratified inlining'),
('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'),
('profile', BOOL, False, 'DUALITY: profile run time'),
('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'),
('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
))

View file

@ -141,6 +141,7 @@ lbool dl_interface::query(::expr * query) {
// make a new problem and solver
_d = alloc(duality_data,m_ctx.get_manager());
_d->ctx.set("mbqi",m_ctx.get_params().mbqi());
_d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx);
_d->rpfp = alloc(RPFP,_d->ls);