mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

working on duality

Browse source
This commit is contained in:
Ken McMillan 2013-11-27 17:39:49 -08:00
parent a93f8b04e5
commit a3462ba6aa
11 changed files with 415 additions and 121 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/duality/duality.h
View file

@ -142,6 +142,7 @@ namespace Duality {
context *ctx; /** Z3 context for formulas */
solver *slvr; /** Z3 solver */
bool need_goals; /** Can the solver use the goal tree to optimize interpolants? */
solver aux_solver; /** For temporary use -- don't leave assertions here. */
/** Tree interpolation. This method assumes the formulas in TermTree
"assumptions" are currently asserted in the solver. The return
@ -178,6 +179,8 @@ namespace Duality {
/** Cancel, throw Canceled object if possible. */
virtual void cancel(){ }
LogicSolver(context &c) : aux_solver(c){}
virtual ~LogicSolver(){}
};
@ -215,7 +218,7 @@ namespace Duality {
}
#endif
iZ3LogicSolver(context &c){
iZ3LogicSolver(context &c) : LogicSolver(c) {
ctx = ictx = &c;
slvr = islvr = new interpolating_solver(*ictx);
need_goals = false;
@ -287,9 +290,9 @@ namespace Duality {
literals dualLabels;
std::list<stack_entry> stack;
std::vector<Term> axioms; // only saved here for printing purposes
solver aux_solver;
solver &aux_solver;
hash_set<ast> *proof_core;
public:
/** Construct an RPFP graph with a given interpolating prover context. It is allowed to
@ -299,13 +302,14 @@ namespace Duality {
inherit the axioms.
*/
RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(*(_ls->ctx))
RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver)
{
ls = _ls;
nodeCount = 0;
edgeCount = 0;
stack.push_back(stack_entry());
HornClauses = false;
proof_core = 0;
}
~RPFP();
@ -606,9 +610,13 @@ namespace Duality {
lbool Solve(Node *root, int persist);
/** Same as Solve, but annotates only a single node. */
lbool SolveSingleNode(Node *root, Node *node);
/** Get the constraint tree (but don't solve it) */
TermTree *GetConstraintTree(Node *root);
TermTree *GetConstraintTree(Node *root, Node *skip_descendant = 0);
/** Dispose of the dual model (counterexample) if there is one. */
@ -678,6 +686,12 @@ namespace Duality {
/** Pop a scope (see Push). Note, you cannot pop axioms. */
void Pop(int num_scopes);
/** Return true if the given edge is used in the proof of unsat.
Can be called only after Solve or Check returns an unsat result. */
bool EdgeUsedInProof(Edge *edge);
/** Convert a collection of clauses to Nodes and Edges in the RPFP.
@ -762,8 +776,19 @@ namespace Duality {
// int GetLabelsRec(hash_map<ast,int> *memo, const Term &f, std::vector<symbol> &labels, bool labpos);
/** Compute and save the proof core for future calls to
EdgeUsedInProof. You only need to call this if you will pop
the solver before calling EdgeUsedInProof.
*/
void ComputeProofCore();
private:
void ClearProofCore(){
if(proof_core)
delete proof_core;
proof_core = 0;
}
Term SuffixVariable(const Term &t, int n);
@ -779,10 +804,14 @@ namespace Duality {
Term ReducedDualEdge(Edge *e);
TermTree *ToTermTree(Node *root);
TermTree *ToTermTree(Node *root, Node *skip_descendant = 0);
TermTree *ToGoalTree(Node *root);
void CollapseTermTreeRec(TermTree *root, TermTree *node);
TermTree *CollapseTermTree(TermTree *node);
void DecodeTree(Node *root, TermTree *interp, int persist);
Term GetUpperBound(Node *n);

79
src/duality/duality_rpfp.cpp
View file

@ -185,6 +185,7 @@ namespace Duality {
return clone_quantifier(t,new_body);
}
RPFP::Term RPFP::LocalizeRec(Edge *e, hash_map<ast,Term> &memo, const Term &t)
{
std::pair<ast,Term> foo(t,expr(ctx));
@ -274,13 +275,15 @@ namespace Duality {
return implies(b, Localize(e, e->F.Formula));
}
TermTree *RPFP::ToTermTree(Node *root)
TermTree *RPFP::ToTermTree(Node *root, Node *skip_descendant)
{
if(skip_descendant && root == skip_descendant)
return new TermTree(ctx.bool_val(true));
Edge *e = root->Outgoing;
if(!e) return new TermTree(ctx.bool_val(true), std::vector<TermTree *>());
std::vector<TermTree *> children(e->Children.size());
for(unsigned i = 0; i < children.size(); i++)
children[i] = ToTermTree(e->Children[i]);
children[i] = ToTermTree(e->Children[i],skip_descendant);
// Term top = ReducedDualEdge(e);
Term top = e->dual.null() ? ctx.bool_val(true) : e->dual;
TermTree *res = new TermTree(top, children);
@ -623,6 +626,7 @@ namespace Duality {
TermTree *goals = NULL;
if(ls->need_goals)
goals = GetGoalTree(root);
ClearProofCore();
// if (dualModel != null) dualModel.Dispose();
// if (dualLabels != null) dualLabels.Dispose();
@ -644,11 +648,54 @@ namespace Duality {
return res;
}
void RPFP::CollapseTermTreeRec(TermTree *root, TermTree *node){
root->addTerm(node->getTerm());
std::vector<Term> &cnsts = node->getTerms();
for(unsigned i = 0; i < cnsts.size(); i++)
root->addTerm(cnsts[i]);
std::vector<TermTree *> &chs = node->getChildren();
for(unsigned i = 0; i < chs.size(); i++){
CollapseTermTreeRec(root,chs[i]);
}
}
TermTree *RPFP::CollapseTermTree(TermTree *node){
std::vector<TermTree *> &chs = node->getChildren();
for(unsigned i = 0; i < chs.size(); i++)
CollapseTermTreeRec(node,chs[i]);
for(unsigned i = 0; i < chs.size(); i++)
delete chs[i];
chs.clear();
return node;
}
lbool RPFP::SolveSingleNode(Node *root, Node *node)
{
timer_start("Solve");
TermTree *tree = CollapseTermTree(GetConstraintTree(root,node));
tree->getChildren().push_back(CollapseTermTree(ToTermTree(node)));
TermTree *interpolant = NULL;
ClearProofCore();
timer_start("interpolate_tree");
lbool res = ls->interpolate_tree(tree, interpolant, dualModel,0,true);
timer_stop("interpolate_tree");
if (res == l_false)
{
DecodeTree(node, interpolant->getChildren()[0], 0);
delete interpolant;
}
delete tree;
timer_stop("Solve");
return res;
}
/** Get the constraint tree (but don't solve it) */
TermTree *RPFP::GetConstraintTree(Node *root)
TermTree *RPFP::GetConstraintTree(Node *root, Node *skip_descendant)
{
return AddUpperBound(root, ToTermTree(root));
return AddUpperBound(root, ToTermTree(root,skip_descendant));
}
/** Dispose of the dual model (counterexample) if there is one. */
@ -677,6 +724,7 @@ namespace Duality {
check_result RPFP::Check(Node *root, std::vector<Node *> underapproxes, std::vector<Node *> *underapprox_core )
{
ClearProofCore();
// if (dualModel != null) dualModel.Dispose();
check_result res;
if(!underapproxes.size())
@ -713,6 +761,7 @@ namespace Duality {
check_result RPFP::CheckUpdateModel(Node *root, std::vector<expr> assumps){
// check_result temp1 = slvr.check(); // no idea why I need to do this
ClearProofCore();
check_result res = slvr.check_keep_model(assumps.size(),&assumps[0]);
dualModel = slvr.get_model();
return res;
@ -1760,9 +1809,9 @@ namespace Duality {
expr conj = ctx.make(And,conjuncts);
s.add(conj);
check_result res = s.check();
s.pop(1);
if(res != unsat)
throw "should be unsat";
s.pop(1);
for(unsigned i = 0; i < conjuncts.size(); ){
std::swap(conjuncts[i],conjuncts.back());
@ -2276,8 +2325,28 @@ namespace Duality {
}
void RPFP::ComputeProofCore(){
if(!proof_core){
std::vector<expr> assumps;
slvr.get_proof().get_assumptions(assumps);
proof_core = new hash_set<ast>;
for(unsigned i = 0; i < assumps.size(); i++)
proof_core->insert(assumps[i]);
}
}
bool RPFP::EdgeUsedInProof(Edge *edge){
ComputeProofCore();
if(!edge->dual.null() && proof_core->find(edge->dual) != proof_core->end())
return true;
for(unsigned i = 0; i < edge->constraints.size(); i++)
if(proof_core->find(edge->constraints[i]) != proof_core->end())
return true;
return false;
}
RPFP::~RPFP(){
ClearProofCore();
for(unsigned i = 0; i < nodes.size(); i++)
delete nodes[i];
for(unsigned i = 0; i < edges.size(); i++)

107
src/duality/duality_solver.cpp
View file

@ -184,7 +184,7 @@ namespace Duality {
best.insert(*it);
}
#else
virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority=false){
virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority=false, bool best_only=false){
if(high_priority) return;
int best_score = INT_MAX;
int worst_score = 0;
@ -194,13 +194,13 @@ namespace Duality {
best_score = std::min(best_score,score);
worst_score = std::max(worst_score,score);
}
int cutoff = best_score + (worst_score-best_score)/2;
int cutoff = best_only ? best_score : (best_score + (worst_score-best_score)/2);
for(std::set<Node *>::iterator it = choices.begin(), en = choices.end(); it != en; ++it)
if(scores[(*it)->map].updates <= cutoff)
best.insert(*it);
}
#endif
/** Called when done expanding a tree */
virtual void Done() {}
};
@ -1607,12 +1607,12 @@ namespace Duality {
heuristic->ChooseExpand(choices, best);
}
#else
void ExpansionChoicesFull(std::set<Node *> &best, bool high_priority){
void ExpansionChoicesFull(std::set<Node *> &best, bool high_priority, bool best_only = false){
std::set<Node *> choices;
for(std::list<RPFP::Node *>::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it)
if (high_priority || !tree->Empty(*it)) // if used in the counter-model
choices.insert(*it);
heuristic->ChooseExpand(choices, best, high_priority);
heuristic->ChooseExpand(choices, best, high_priority, best_only);
}
void ExpansionChoicesRec(std::vector <Node *> &unused_set, std::vector <Node *> &used_set,
@ -1650,9 +1650,9 @@ namespace Duality {
std::set<Node *> old_choices;
void ExpansionChoices(std::set<Node *> &best, bool high_priority){
void ExpansionChoices(std::set<Node *> &best, bool high_priority, bool best_only = false){
if(!underapprox || constrained || high_priority){
ExpansionChoicesFull(best, high_priority);
ExpansionChoicesFull(best, high_priority,best_only);
return;
}
std::vector <Node *> unused_set, used_set;
@ -1684,7 +1684,7 @@ namespace Duality {
timer_start("ExpandSomeNodes");
timer_start("ExpansionChoices");
std::set<Node *> choices;
ExpansionChoices(choices,high_priority);
ExpansionChoices(choices,high_priority,max != INT_MAX);
timer_stop("ExpansionChoices");
std::list<RPFP::Node *> leaves_copy = leaves; // copy so can modify orig
leaves.clear();
@ -1740,38 +1740,54 @@ namespace Duality {
if(slvr_level != stack.back().level)
throw "stacks out of sync!";
res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop
// res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop
check_result foo = tree->Check(top);
res = foo == unsat ? l_false : l_true;
if (res == l_false) {
if (stack.empty()) // should never happen
return false;
std::vector<Node *> &expansions = stack.back().expansions;
int update_count = 0;
for(unsigned i = 0; i < expansions.size(); i++){
tree->Generalize(expansions[i]);
if(RecordUpdate(expansions[i]))
update_count++;
}
if(update_count == 0)
std::cout << "backtracked without learning\n";
tree->Pop(1);
hash_set<Node *> leaves_to_remove;
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
// if(node != top)
// tree->ConstrainParent(node->Incoming[0],node);
std::vector<Node *> &cs = node->Outgoing->Children;
for(unsigned i = 0; i < cs.size(); i++){
leaves_to_remove.insert(cs[i]);
UnmapNode(cs[i]);
if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
throw "help!";
{
std::vector<Node *> &expansions = stack.back().expansions;
int update_count = 0;
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
tree->SolveSingleNode(top,node);
tree->Generalize(node);
if(RecordUpdate(node))
update_count++;
}
RemoveExpansion(node);
if(update_count == 0)
std::cout << "backtracked without learning\n";
}
RemoveLeaves(leaves_to_remove);
stack.pop_back();
tree->ComputeProofCore(); // need to compute the proof core before popping solver
while(1) {
std::vector<Node *> &expansions = stack.back().expansions;
bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop
tree->Pop(1);
hash_set<Node *> leaves_to_remove;
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
// if(node != top)
// tree->ConstrainParent(node->Incoming[0],node);
std::vector<Node *> &cs = node->Outgoing->Children;
for(unsigned i = 0; i < cs.size(); i++){
leaves_to_remove.insert(cs[i]);
UnmapNode(cs[i]);
if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
throw "help!";
}
RemoveExpansion(node);
}
RemoveLeaves(leaves_to_remove);
stack.pop_back();
if(prev_level_used || stack.size() == 1) break;
RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list
std::vector<Node *> &unused_ex = stack.back().expansions;
for(unsigned i = 0; i < unused_ex.size(); i++)
heuristic->Update(unused_ex[i]->map); // make it less likely to expand this node in future
}
HandleUpdatedNodes();
if(stack.size() == 1)
return false;
@ -1782,8 +1798,10 @@ namespace Duality {
for(unsigned i = 0; i < expansions.size(); i++){
tree->FixCurrentState(expansions[i]->Outgoing);
}
#if 0
if(tree->slvr.check() == unsat)
throw "help!";
#endif
stack.push_back(stack_entry());
stack.back().level = tree->slvr.get_scope_level();
if(ExpandSomeNodes(false,1)){
@ -1798,6 +1816,27 @@ namespace Duality {
}
}
bool LevelUsedInProof(unsigned level){
std::vector<Node *> &expansions = stack[level].expansions;
for(unsigned i = 0; i < expansions.size(); i++)
if(tree->EdgeUsedInProof(expansions[i]->Outgoing))
return true;
return false;
}
void RemoveUpdateNodesAtCurrentLevel() {
for(std::list<Node *>::iterator it = updated_nodes.begin(), en = updated_nodes.end(); it != en;){
Node *node = *it;
if(AtCurrentStackLevel(node->Incoming[0]->Parent)){
std::list<Node *>::iterator victim = it;
++it;
updated_nodes.erase(victim);
}
else
++it;
}
}
void RemoveLeaves(hash_set<Node *> &leaves_to_remove){
std::list<RPFP::Node *> leaves_copy;
leaves_copy.swap(leaves);
@ -2270,7 +2309,7 @@ namespace Duality {
return name;
}
virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority){
virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority, bool best_only){
if(!high_priority || !old_cex.tree){
Heuristic::ChooseExpand(choices,best,false);
return;

37
src/duality/duality_wrapper.cpp
View file

@ -481,9 +481,9 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
for(unsigned i = 0; i < theory.size(); i++)
_theory[i] = theory[i];
push();
if(!incremental){
push();
for(unsigned i = 0; i < linear_assumptions.size(); i++)
for(unsigned j = 0; j < linear_assumptions[i].size(); j++)
add(linear_assumptions[i][j]);
@ -522,7 +522,8 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
}
#endif
pop();
if(!incremental)
pop();
return (res == unsat) ? l_false : ((res == sat) ? l_true : l_undef);
@ -554,6 +555,29 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
return "";
}
static void get_assumptions_rec(stl_ext::hash_set<ast> &memo, const proof &pf, std::vector<expr> &assumps){
if(memo.find(pf) != memo.end())return;
memo.insert(pf);
pfrule dk = pf.rule();
if(dk == PR_ASSERTED){
expr con = pf.conc();
assumps.push_back(con);
}
else {
unsigned nprems = pf.num_prems();
for(unsigned i = 0; i < nprems; i++){
proof arg = pf.prem(i);
get_assumptions_rec(memo,arg,assumps);
}
}
}
void proof::get_assumptions(std::vector<expr> &assumps){
stl_ext::hash_set<ast> memo;
get_assumptions_rec(memo,*this,assumps);
}
void ast::show() const{
std::cout << mk_pp(raw(), m()) << std::endl;
@ -564,6 +588,15 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
std::cout << std::endl;
}
void solver::show() {
unsigned n = m_solver->get_num_assertions();
if(!n)
return;
ast_smt_pp pp(m());
for (unsigned i = 0; i < n-1; ++i)
pp.add_assumption(m_solver->get_assertion(i));
pp.display_smt2(std::cout, m_solver->get_assertion(n-1));
}
void include_ast_show(ast &a){
a.show();

37
src/duality/duality_wrapper.h
View file

@ -393,6 +393,7 @@ namespace Duality {
sort array_range() const;
};
class func_decl : public ast {
public:
func_decl() : ast() {}
@ -593,6 +594,36 @@ namespace Duality {
};
typedef ::decl_kind pfrule;
class proof : public ast {
public:
proof(context & c):ast(c) {}
proof(context & c, ::proof *s):ast(c, s) {}
proof(proof const & s):ast(s) {}
operator ::proof*() const { return to_app(raw()); }
proof & operator=(proof const & s) { return static_cast<proof&>(ast::operator=(s)); }
pfrule rule() const {
::func_decl *d = to_app(raw())->get_decl();
return d->get_decl_kind();
}
unsigned num_prems() const {
return to_app(raw())->get_num_args() - 1;
}
expr conc() const {
return ctx().cook(to_app(raw())->get_arg(num_prems()));
}
proof prem(unsigned i) const {
return proof(ctx(),to_app(to_app(raw())->get_arg(i)));
}
void get_assumptions(std::vector<expr> &assumps);
};
#if 0
#if Z3_MAJOR_VERSION > 4 || Z3_MAJOR_VERSION == 4 && Z3_MINOR_VERSION >= 3
@ -870,6 +901,12 @@ namespace Duality {
unsigned get_scope_level(){return m_solver->get_scope_level();}
void show();
proof get_proof(){
return proof(ctx(),m_solver->get_proof());
}
};
#if 0

2
src/interp/iz3interp.cpp
View file

@ -501,5 +501,3 @@ void interpolation_options_struct::apply(iz3base &b){
b.set_option((*it).first,(*it).second);
}

6
src/interp/iz3mgr.h
View file

@ -359,6 +359,12 @@ class iz3mgr {
return fid == m().get_basic_family_id() && k == BOOL_SORT;
}
bool is_array_type(type t){
family_id fid = to_sort(t)->get_family_id();
decl_kind k = to_sort(t)->get_decl_kind();
return fid == m_array_fid && k == ARRAY_SORT;
}
type get_range_type(symb s){
return to_func_decl(s)->get_range();
}

200
src/interp/iz3proof_itp.cpp
View file

@ -473,7 +473,12 @@ class iz3proof_itp_impl : public iz3proof_itp {
hash_map<ast,ast> simplify_memo;
ast simplify(const ast &t){
return simplify_rec(t);
ast res = normalize(simplify_rec(t));
#ifdef BOGUS_QUANTS
if(localization_vars.size())
res = add_quants(z3_simplify(res));
#endif
return res;
}
ast simplify_rec(const ast &e){
@ -550,11 +555,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
ast simplify_sum(std::vector<ast> &args){
ast cond = mk_true();
ast Aproves = mk_true(), Bproves = mk_true();
ast ineq = args[0];
if(!is_normal_ineq(ineq)) throw cannot_simplify();
sum_cond_ineq(ineq,cond,args[1],args[2]);
return my_implies(cond,ineq);
sum_cond_ineq(ineq,args[1],args[2],Aproves,Bproves);
return my_and(Aproves,my_implies(Bproves,ineq));
}
ast simplify_rotate_sum(const ast &pl, const ast &pf){
@ -567,38 +572,42 @@ class iz3proof_itp_impl : public iz3proof_itp {
return sym(chain) == concat;
}
ast ineq_from_chain(const ast &chain, ast &cond){
if(sym(chain) == normal)
throw "normalized inequalities not supported here";
if(is_rewrite_chain(chain)){
ast last = chain_last(chain);
ast rest = chain_rest(chain);
if(is_true(rest) && is_rewrite_side(LitA,last)
&& is_true(rewrite_lhs(last))){
cond = my_and(cond,rewrite_cond(last));
return rewrite_rhs(last);
}
if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last)))
return ineq_from_chain(rest,cond);
#if 0
ast ineq_from_chain_simple(const ast &chain, ast &cond){
if(is_true(chain))
return chain;
ast last = chain_last(chain);
ast rest = chain_rest(chain);
if(is_true(rest) && is_rewrite_side(LitA,last)
&& is_true(rewrite_lhs(last))){
cond = my_and(cond,rewrite_cond(last));
return rewrite_rhs(last);
}
if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last)))
return ineq_from_chain_simple(rest,cond);
return chain;
}
#endif
ast ineq_from_chain(const ast &chain, ast &Aproves, ast &Bproves){
if(is_rewrite_chain(chain))
return rewrite_chain_to_normal_ineq(chain,Aproves,Bproves);
return chain;
}
void sum_cond_ineq(ast &ineq, ast &cond, const ast &coeff2, const ast &ineq2){
void sum_cond_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){
opr o = op(ineq2);
if(o == Implies){
sum_cond_ineq(ineq,cond,coeff2,arg(ineq2,1));
cond = my_and(cond,arg(ineq2,0));
sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves);
Bproves = my_and(Bproves,arg(ineq2,0));
}
else {
if(sym(ineq) == normal || sym(ineq2) == normal){
ast Aproves = mk_true();
sum_normal_ineq(ineq,coeff2,ineq2,Aproves,cond);
if(!is_true(Aproves))
throw "Aproves not handled in sum_cond_ineq";
ast the_ineq = ineq_from_chain(ineq2,Aproves,Bproves);
if(sym(ineq) == normal || sym(the_ineq) == normal){
sum_normal_ineq(ineq,coeff2,the_ineq,Aproves,Bproves);
return;
}
ast the_ineq = ineq_from_chain(ineq2,cond);
if(is_ineq(the_ineq))
linear_comb(ineq,coeff2,the_ineq);
else
@ -621,10 +630,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast in1,in2,n1,n2;
destruct_normal(ineq,in1,n1);
destruct_normal(ineq2,in2,n2);
ast dummy;
sum_cond_ineq(in1,dummy,coeff2,in2);
ast dummy1, dummy2;
sum_cond_ineq(in1,coeff2,in2,dummy1,dummy2);
n1 = merge_normal_chains(n1,n2, Aproves, Bproves);
ineq = make(normal,in1,n1);
ineq = make_normal(in1,n1);
}
bool is_ineq(const ast &ineq){
@ -639,7 +648,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast in1,n1;
destruct_normal(ineq1,in1,n1);
in1 = idiv_ineq(in1,divisor);
return make(normal,in1,n1);
return make_normal(in1,n1);
}
if(divisor == make_int(rational(1)))
return ineq1;
@ -649,17 +658,23 @@ class iz3proof_itp_impl : public iz3proof_itp {
return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor));
}
ast rotate_sum_rec(const ast &pl, const ast &pf, ast &cond, ast &ineq){
ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){
if(pf == pl)
return my_implies(cond,simplify_ineq(ineq));
return my_implies(Bproves,simplify_ineq(ineq));
if(op(pf) == Uninterpreted && sym(pf) == sum){
if(arg(pf,2) == pl){
sum_cond_ineq(ineq,cond,make_int("1"),arg(pf,0));
ast Aproves = mk_true();
sum_cond_ineq(ineq,make_int("1"),arg(pf,0),Aproves,Bproves);
if(!is_true(Aproves))
throw "help!";
ineq = idiv_ineq(ineq,arg(pf,1));
return my_implies(cond,ineq);
return my_implies(Bproves,ineq);
}
sum_cond_ineq(ineq,cond,arg(pf,1),arg(pf,2));
return rotate_sum_rec(pl,arg(pf,0),cond,ineq);
ast Aproves = mk_true();
sum_cond_ineq(ineq,arg(pf,1),arg(pf,2),Aproves,Bproves);
if(!is_true(Aproves))
throw "help!";
return rotate_sum_rec(pl,arg(pf,0),Bproves,ineq);
}
throw cannot_simplify();
}
@ -669,28 +684,30 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast equality = arg(neg_equality,0);
ast x = arg(equality,0);
ast y = arg(equality,1);
ast cond1 = mk_true();
ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),cond1));
ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),cond1));
ast Aproves1 = mk_true(), Bproves1 = mk_true();
ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),Aproves1,Bproves1));
ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),Aproves1,Bproves1));
ast ineq1 = make(Leq,make_int("0"),make_int("0"));
sum_cond_ineq(ineq1,cond1,make_int("-1"),xleqy);
sum_cond_ineq(ineq1,cond1,make_int("-1"),yleqx);
cond1 = my_and(cond1,z3_simplify(ineq1));
ast cond2 = mk_true();
sum_cond_ineq(ineq1,make_int("-1"),xleqy,Aproves1,Bproves1);
sum_cond_ineq(ineq1,make_int("-1"),yleqx,Aproves1,Bproves1);
Bproves1 = my_and(Bproves1,z3_simplify(ineq1));
ast Aproves2 = mk_true(), Bproves2 = mk_true();
ast ineq2 = make(Leq,make_int("0"),make_int("0"));
sum_cond_ineq(ineq2,cond2,make_int("1"),xleqy);
sum_cond_ineq(ineq2,cond2,make_int("1"),yleqx);
cond2 = z3_simplify(ineq2);
sum_cond_ineq(ineq2,make_int("1"),xleqy,Aproves2,Bproves2);
sum_cond_ineq(ineq2,make_int("1"),yleqx,Aproves2,Bproves2);
Bproves2 = z3_simplify(ineq2);
if(!is_true(Aproves1) || !is_true(Aproves2))
throw "help!";
if(get_term_type(x) == LitA){
ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy)));
ast rewrite1 = make_rewrite(LitA,top_pos,cond1,make(Equal,x,iter));
ast rewrite2 = make_rewrite(LitB,top_pos,cond2,make(Equal,iter,y));
ast rewrite1 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,x,iter));
ast rewrite2 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,iter,y));
return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
}
if(get_term_type(y) == LitA){
ast iter = z3_simplify(make(Plus,y,get_ineq_rhs(yleqx)));
ast rewrite2 = make_rewrite(LitA,top_pos,cond1,make(Equal,iter,y));
ast rewrite1 = make_rewrite(LitB,top_pos,cond2,make(Equal,x,iter));
ast rewrite2 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,iter,y));
ast rewrite1 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,x,iter));
return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
}
throw cannot_simplify();
@ -723,7 +740,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
else {
ast itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
return make(normal,itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
return make_normal(itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
}
}
}
@ -852,7 +869,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast sub_chain = extract_rewrites(chain,pos);
if(is_true(sub_chain))
throw "bad inequality rewriting";
ast new_normal = make_normal(ineq2,ineq1,reverse_chain(sub_chain));
ast new_normal = make_normal_step(ineq2,ineq1,reverse_chain(sub_chain));
normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
}
}
@ -876,7 +893,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast mc = z3_simplify(chain_side_proves(LitA,pref));
Aproves = my_and(Aproves,mc);
}
return make(normal,itp,nc);
return make_normal(itp,nc);
}
/* Given a chain rewrite chain deriving not P and a rewrite chain deriving P, return an interpolant. */
@ -913,7 +930,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast interp;
if(is_normal_ineq(Q2)){ // inequalities are special
ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves);
sum_cond_ineq(nQ2,Bproves,make_int(rational(1)),Q2);
sum_cond_ineq(nQ2,make_int(rational(1)),Q2,Aproves,Bproves);
interp = normalize(nQ2);
}
else
@ -1549,7 +1566,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
return;
}
}
if(op(ineq) == Leq){
if(op(ineq) == Leq || op(ineq) == Geq){
lhs = srhs;
rhs = arg(ineq,1);
return;
@ -1604,7 +1621,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
ast normal_lhs(const ast &t){
return arg(arg(t,0),1);
return arg(arg(t,0),0);
}
ast normal_rhs(const ast &t){
@ -1615,16 +1632,22 @@ class iz3proof_itp_impl : public iz3proof_itp {
return arg(t,1);
}
ast make_normal(const ast &lhs, const ast &rhs, const ast &proof){
ast make_normal_step(const ast &lhs, const ast &rhs, const ast &proof){
return make(normal_step,make_equiv(lhs,rhs),proof);
}
ast make_normal(const ast &ineq, const ast &nrml){
if(!is_ineq(ineq))
throw "what?";
return make(normal,ineq,nrml);
}
ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){
LitType rhst = get_term_type(rhs);
if(rhst != LitMixed || ast_id(lhs) < ast_id(rhs))
return make_normal(lhs,rhs,proof);
return make_normal_step(lhs,rhs,proof);
else
return make_normal(rhs,lhs,reverse_chain(proof));
return make_normal_step(rhs,lhs,reverse_chain(proof));
}
ast chain_side_proves(LitType side, const ast &chain){
@ -1658,7 +1681,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
if(t1 == LitMixed && (t2 != LitMixed || tid2 > tid1)){
ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2);
new_normal = f2;
trans[rhs1] = make_normal(rhs1,rhs2,new_proof);
trans[rhs1] = make_normal_step(rhs1,rhs2,new_proof);
}
else if(t2 == LitMixed && (t1 != LitMixed || tid1 > tid2))
return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves);
@ -1671,7 +1694,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
Aproves = my_and(Aproves,mcB);
ast rep = apply_rewrite_chain(rhs1,Aproof);
new_proof = concat_rewrite_chain(pf1,Aproof);
new_normal = make_normal(rhs1,rep,new_proof);
new_normal = make_normal_step(rhs1,rep,new_proof);
}
else if(t1 == LitA && t2 == LitB)
return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves);
@ -1701,7 +1724,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
if(it != trans.end()){
const ast &f2 = it->second;
ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2));
new_normal = make_normal(normal_lhs(f),normal_rhs(f2),pf);
new_normal = make_normal_step(normal_lhs(f),normal_rhs(f2),pf);
}
else
new_normal = f;
@ -1715,9 +1738,36 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res;
}
ast normalize(const ast &t){
bool destruct_cond_ineq(ast t, ast &Aproves, ast &Bproves, ast&ineq){
if(op(t) == And){
Aproves = arg(t,0);
t = arg(t,1);
}
else
Aproves = mk_true();
if(op(t) == Implies){
Bproves = arg(t,0);
t = arg(t,1);
}
else
Bproves = mk_true();
if(is_normal_ineq(t)){
ineq = t;
return true;
}
return false;
}
ast cons_cond_ineq(const ast &Aproves, const ast &Bproves, const ast &ineq){
return my_and(Aproves,my_implies(Bproves,ineq));
}
ast normalize(const ast &ct){
ast Aproves,Bproves,t;
if(!destruct_cond_ineq(ct,Aproves,Bproves,t))
return ct;
if(sym(t) != normal)
return t;
return ct;
ast chain = arg(t,1);
hash_map<ast,ast> map;
for(ast c = chain; !is_true(c); c = normal_rest(c)){
@ -1727,7 +1777,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
map[lhs] = rhs;
}
ast res = subst(map,arg(t,0));
return res;
return cons_cond_ineq(Aproves,Bproves,res);
}
/** Make an assumption node. The given clause is assumed in the given frame. */
@ -1848,8 +1898,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
/** Make an axiom node. The conclusion must be an instance of an axiom. */
virtual node make_axiom(const std::vector<ast> &conclusion){
prover::range frng = pv->range_full();
virtual node make_axiom(const std::vector<ast> &conclusion, prover::range frng){
int nargs = conclusion.size();
std::vector<ast> largs(nargs);
std::vector<ast> eqs;
@ -1874,6 +1923,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
return itp;
}
virtual node make_axiom(const std::vector<ast> &conclusion){
return make_axiom(conclusion,pv->range_full());
}
/** Make a Contra node. This rule takes a derivation of the form
Gamma |- False and produces |- \/~Gamma. */
@ -2299,7 +2352,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
int nargs = num_args(e);
if(nargs > 0 /* && (!is_local(e) || flo <= hi || fhi >= lo) */){
prover::range frng = rng;
if(op(e) == Uninterpreted){
opr o = op(e);
if(o == Uninterpreted){
symb f = sym(e);
prover::range srng = pv->sym_range(f);
if(pv->ranges_intersect(srng,rng)) // localize to desired range if possible
@ -2307,6 +2361,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
else
frng = srng; // this term will be localized
}
else if(o == Plus || o == Times){ // don't want bound variables inside arith ops
frng = erng; // this term will be localized
}
std::vector<ast> largs(nargs);
std::vector<ast> eqs;
std::vector<ast> pfs;
@ -2333,6 +2390,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
if(pv->ranges_intersect(pv->ast_scope(e),rng))
return e; // this term occurs in range, so it's O.K.
if(is_array_type(get_type(e)))
throw "help!";
// choose a frame for the constraint that is close to range
int frame = pv->range_near(pv->ast_scope(e),rng);
@ -2362,7 +2422,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
/* Return an interpolant from a proof of false */
ast interpolate(const node &pf){
// proof of false must be a formula, with quantified symbols
#ifndef BOGUS_QUANTS
return add_quants(z3_simplify(pf));
#else
return z3_simplify(pf);
#endif
}
ast resolve_with_quantifier(const ast &pivot1, const ast &conj1,

3
src/interp/iz3proof_itp.h
View file

@ -70,6 +70,9 @@ class iz3proof_itp : public iz3mgr {
/** Make an axiom node. The conclusion must be an instance of an axiom. */
virtual node make_axiom(const std::vector<ast> &conclusion) = 0;
/** Make an axiom node. The conclusion must be an instance of an axiom. Localize axiom instance to range*/
virtual node make_axiom(const std::vector<ast> &conclusion, prover::range) = 0;
/** Make a Contra node. This rule takes a derivation of the form
Gamma |- False and produces |- \/~Gamma. */

20
src/interp/iz3translate.cpp
View file

@ -1364,6 +1364,18 @@ public:
return eq2;
}
bool get_store_array(const ast &t, ast &res){
if(op(t) == Store){
res = t;
return true;
}
int nargs = num_args(t);
for(int i = 0; i < nargs; i++)
if(get_store_array(arg(t,i),res))
return true;
return false;
}
// translate a Z3 proof term into interpolating proof system
Iproof::node translate_main(ast proof, bool expect_clause = true){
@ -1578,9 +1590,13 @@ public:
throw unsupported();
}
break;
case ArrayTheory: // nothing fancy for this
res = iproof->make_axiom(lits);
case ArrayTheory: {// nothing fancy for this
ast store_array;
if(!get_store_array(con,store_array))
throw unsupported();
res = iproof->make_axiom(lits,ast_scope(store_array));
break;
}
default:
throw unsupported();
}

2
src/muz/duality/duality_dl_interface.cpp
View file

@ -472,7 +472,7 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) {
expr conc = f(args);
::vector<proof *> pprems;
::vector< ::proof *> pprems;
for(unsigned i = 0; i < prems.size(); i++)
pprems.push_back(prems[i].get());