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

Move proof dot printing into iuc_proof

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-16 13:32:28 -07:00
parent 45500ff7d3
commit 07ad67ebad
4 changed files with 545 additions and 633 deletions
Download patch file Download diff file Expand all files Collapse all files

88
src/muz/spacer/spacer_iuc_proof.cpp
View file

@ -1,9 +1,12 @@
#include <unordered_map>
#include "ast/ast_pp_dot.h"
#include "muz/spacer/spacer_iuc_proof.h"
#include "ast/for_each_expr.h"
#include "ast/array_decl_plugin.h"
#include "ast/proofs/proof_utils.h"
#include "muz/spacer/spacer_proof_utils.h"
#include "muz/spacer/spacer_util.h"
namespace spacer {
/*
@ -191,4 +194,87 @@ void iuc_proof::dump_farkas_stats()
<< "\n total farkas lemmas " << fl_total
<< " farkas lemmas in lowest cut " << fl_lowcut << "\n";);
}
void iuc_proof::display_dot(std::ostream& out) {
out << "digraph proof { \n";
std::unordered_map<unsigned, unsigned> ids;
unsigned last_id = 0;
proof_post_order it(m_pr, m);
while (it.hasNext())
{
proof* curr = it.next();
SASSERT(ids.count(curr->get_id()) == 0);
ids.insert(std::make_pair(curr->get_id(), last_id));
std::string color = "white";
if (this->is_a_marked(curr) && !this->is_b_marked(curr))
color = "red";
else if(!this->is_a_marked(curr) && this->is_b_marked(curr))
color = "blue";
else if(this->is_a_marked(curr) && this->is_b_marked(curr) )
color = "purple";
// compute node label
std::ostringstream label_ostream;
label_ostream << mk_epp(m.get_fact(curr), m) << "\n";
std::string label = escape_dot(label_ostream.str());
// compute edge-label
std::string edge_label = "";
if (m.get_num_parents(curr) == 0) {
switch (curr->get_decl_kind())
{
case PR_ASSERTED:
edge_label = "asserted:";
break;
case PR_HYPOTHESIS:
edge_label = "hyp:";
color = "grey";
break;
case PR_TH_LEMMA:
if (is_farkas_lemma(m, curr))
edge_label = "th_axiom(farkas):";
else if (is_arith_lemma(m, curr))
edge_label = "th_axiom(arith):";
else
edge_label = "th_axiom:";
break;
default:
edge_label = "unknown axiom:";
}
}
else {
if (curr->get_decl_kind() == PR_LEMMA)
edge_label = "lemma:";
else if (curr->get_decl_kind() == PR_TH_LEMMA) {
if (is_farkas_lemma(m, curr))
edge_label = "th_lemma(farkas):";
else if (is_arith_lemma(m, curr))
edge_label = "th_lemma(arith):";
else
edge_label = "th_lemma(other):";
}
}
// generate entry for node in dot-file
out << "node_" << last_id << " " << "["
<< "shape=box,style=\"filled\","
<< "label=\"" << edge_label << " " << label << "\", "
<< "fillcolor=\"" << color << "\"" << "]\n";
// add entry for each edge to that node
for (unsigned i = m.get_num_parents(curr); i > 0 ; --i)
{
proof* premise = to_app(curr->get_arg(i-1));
unsigned pid = ids.at(premise->get_id());
out << "node_" << pid << " -> " << "node_" << last_id << ";\n";
}
++last_id;
}
out << "\n}" << std::endl;
}
}

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

@ -1,6 +1,7 @@
#ifndef IUC_PROOF_H_
#define IUC_PROOF_H_
#include <ostream>
#include "ast/ast.h"
namespace spacer {
@ -35,6 +36,7 @@ public:
return !is_h_marked (p) && is_core_pure(m.get_fact (p));
}
void display_dot(std::ostream &out);
// debug method
void dump_farkas_stats();
private:

207
src/muz/spacer/spacer_proof_utils.cpp
View file

@ -16,7 +16,6 @@ Revision History:
--*/
#include <unordered_map>
#include "util/params.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
@ -26,222 +25,40 @@ Revision History:
#include "ast/proofs/proof_utils.h"
#include "muz/spacer/spacer_proof_utils.h"
#include "muz/spacer/spacer_util.h"
namespace spacer {
// arithmetic lemma recognizer
bool is_arith_lemma(ast_manager& m, proof* pr)
{
// arith lemmas: second parameter specifies exact type of lemma,
// could be "farkas", "triangle-eq", "eq-propagate",
// "assign-bounds", maybe also something else
bool is_arith_lemma(ast_manager& m, proof* pr)
{
if (pr->get_decl_kind() == PR_TH_LEMMA)
{
if (pr->get_decl_kind() == PR_TH_LEMMA) {
func_decl* d = pr->get_decl();
symbol sym;
if (d->get_num_parameters() >= 1 &&
d->get_parameter(0).is_symbol(sym) && sym == "arith")
{
return true;
}
return d->get_num_parameters() >= 1 &&
d->get_parameter(0).is_symbol(sym) &&
sym == "arith";
}
return false;
}
// farkas lemma recognizer
bool is_farkas_lemma(ast_manager& m, proof* pr)
{
if (pr->get_decl_kind() == PR_TH_LEMMA)
{
func_decl* d = pr->get_decl();
symbol sym;
if (d->get_num_parameters() >= 2 && // the Farkas coefficients are saved in the parameters of step
d->get_parameter(0).is_symbol(sym) && sym == "arith" && // the first two parameters are "arith", "farkas",
d->get_parameter(1).is_symbol(sym) && sym == "farkas")
{
return true;
}
return d->get_num_parameters() >= 2 &&
d->get_parameter(0).is_symbol(sym) && sym == "arith" &&
d->get_parameter(1).is_symbol(sym) && sym == "farkas";
}
return false;
}
/*
* ====================================
* methods for dot printing
* ====================================
*/
void pp_proof_dot_to_stream(ast_manager& m, std::ofstream& dotstream, proof* pr, iuc_proof* iuc_pr = nullptr);
std::string escape_dot(const std::string &s);
void pp_proof_post_process_dot(std::string dot_filepath, std::ofstream &dotstream);
void pp_proof_dot(ast_manager& m, proof* pr, iuc_proof* iuc_pr)
{
// open temporary dot-file
std::string dotfile_path = "proof.dot";
std::ofstream dotstream(dotfile_path);
// dump dot representation to stream
pp_proof_dot_to_stream(m, dotstream, pr, iuc_pr);
// post process dot-file, TODO: factor this out to a different place
pp_proof_post_process_dot(dotfile_path,dotstream);
}
void pp_proof_dot_to_stream(ast_manager& m, std::ofstream& dotstream, proof* pr, iuc_proof* iuc_pr)
{
dotstream << "digraph proof { \n";
std::unordered_map<unsigned, unsigned> id_to_small_id;
unsigned counter = 0;
proof_post_order it2(pr, m);
while (it2.hasNext())
{
proof* currentNode = it2.next();
SASSERT(id_to_small_id.find(currentNode->get_id()) == id_to_small_id.end());
id_to_small_id.insert(std::make_pair(currentNode->get_id(), counter));
std::string color = "white";
if (iuc_pr != nullptr)
{
if (iuc_pr->is_a_marked(currentNode) && !iuc_pr->is_b_marked(currentNode))
{
color = "red";
}
else if(iuc_pr->is_b_marked(currentNode) && !iuc_pr->is_a_marked(currentNode))
{
color = "blue";
}
else if(iuc_pr->is_b_marked(currentNode) && iuc_pr->is_a_marked(currentNode))
{
color = "purple";
}
}
// compute label
params_ref p;
p.set_uint("max_depth", 4294967295u);
p.set_uint("min_alias_size", 4294967295u);
std::ostringstream label_ostream;
label_ostream << mk_pp(m.get_fact(currentNode),m,p) << "\n";
std::string label = escape_dot(label_ostream.str());
// compute edge-label
std::string edge_label = "";
if (m.get_num_parents(currentNode) == 0)
{
switch (currentNode->get_decl_kind())
{
case PR_ASSERTED:
edge_label = "asserted:";
break;
case PR_HYPOTHESIS:
edge_label = "hyp:";
color = "grey";
break;
case PR_TH_LEMMA:
if (is_farkas_lemma(m, currentNode))
{
edge_label = "th_axiom(farkas):";
}
else
{
edge_label = "th_axiom:";
}
break;
default:
edge_label = "unknown axiom-type:";
}
}
else
{
if (currentNode->get_decl_kind() == PR_LEMMA)
{
edge_label = "lemma:";
}
else if (currentNode->get_decl_kind() == PR_TH_LEMMA)
{
func_decl* d = currentNode->get_decl();
symbol sym;
if (d->get_num_parameters() >= 2 && // the Farkas coefficients are saved in the parameters of step
d->get_parameter(0).is_symbol(sym) && sym == "arith" && // the first two parameters are "arith", "farkas",
d->get_parameter(1).is_symbol(sym) && sym == "farkas")
{
edge_label = "th_lemma(farkas):";
}
else
{
edge_label = "th_lemma(other):";
}
}
}
// generate entry for node in dot-file
dotstream << "node_" << counter << " "
<< "["
<< "shape=box,style=\"filled\","
<< "label=\"" << edge_label << " " << label << "\", "
<< "fillcolor=\"" << color << "\""
<< "]\n";
// add entry for each edge to that node
for (unsigned i = m.get_num_parents(currentNode); i > 0 ; --i)
{
proof* premise = to_app(currentNode->get_arg(i-1));
unsigned premise_small_id = id_to_small_id[premise->get_id()];
dotstream << "node_" << premise_small_id
<< " -> "
<< "node_" << counter
<< ";\n";
}
++counter;
}
dotstream << "\n}" << std::endl;
}
std::string escape_dot(const std::string &s)
{
std::string res;
res.reserve(s.size()); // preallocate
for (auto c : s) {
if (c == '\n')
res.append("\\l");
else
res.push_back(c);
}
return res;
}
void pp_proof_post_process_dot(std::string dot_filepath, std::ofstream &dotstream)
{
// replace variables in the dotfiles with nicer descriptions (hack: hard coded replacement for now)
std::vector<std::vector<std::string> > predicates;
std::vector<std::string> l1 = {"L1","i","n","A"};
predicates.push_back(l1);
std::vector<std::string> l2 = {"L2","j","m","B"};
predicates.push_back(l2);
for(auto& predicate : predicates)
{
std::string predicate_name = predicate[0];
for (unsigned i=0; i+1 < predicate.size(); ++i)
{
std::string new_name = predicate[i+1];
std::string substring0 = predicate_name + "_" + std::to_string(i) + "_0";
std::string substringN = predicate_name + "_" + std::to_string(i) + "_n";
std::string command0 = "sed -i '.bak' 's/" + substring0 + "/" + new_name + "/g' " + dot_filepath;
verbose_stream() << command0 << std::endl;
system(command0.c_str());
std::string commandN = "sed -i '.bak' s/" + substringN + "/" + new_name + "\\'" + "/g " + dot_filepath;
verbose_stream() << commandN << std::endl;
system(commandN.c_str());
}
}
verbose_stream() << "end of postprocessing";
}
/*
* ====================================

45
src/muz/spacer/spacer_proof_utils.h
View file

@ -25,15 +25,7 @@ namespace spacer {
bool is_arith_lemma(ast_manager& m, proof* pr);
bool is_farkas_lemma(ast_manager& m, proof* pr);
/*
* prints the proof pr in dot representation to the file proof.dot
* if iuc_pr is not nullptr, then it is queried for coloring partitions
*/
class iuc_proof;
void pp_proof_dot(ast_manager& m, proof* pr, iuc_proof* iuc_pr = nullptr);
class theory_axiom_reducer
{
class theory_axiom_reducer {
public:
theory_axiom_reducer(ast_manager& m) : m(m), m_pinned(m) {}
@ -46,7 +38,8 @@ namespace spacer {
// tracking all created expressions
expr_ref_vector m_pinned;
// maps each proof of a clause to the transformed subproof of that clause
// maps each proof of a clause to the transformed subproof of
// that clause
obj_map<proof, proof*> m_cache;
void reset();
@ -66,18 +59,32 @@ namespace spacer {
ast_manager &m;
expr_ref_vector m_pinned; // tracking all created expressions
ptr_vector<proof_set> m_pinned_active_hyps; // tracking all created sets of active hypothesis
ptr_vector<expr_set> m_pinned_parent_hyps; // tracking all created sets of parent hypothesis
// created expressions
expr_ref_vector m_pinned;
obj_map<proof, proof*> m_cache; // maps each proof of a clause to the transformed subproof of that clause
obj_map<expr, proof*> m_units; // maps each unit literal to the subproof of that unit
obj_map<proof, proof_set*> m_active_hyps; // maps each proof of a clause to the set of proofs of active hypothesis' of the clause
obj_map<proof, expr_set*> m_parent_hyps; // maps each proof of a clause to the hypothesis-fact, which are transitive parents of that clause, needed to avoid creating cycles in the proof.
// created sets of active hypothesis
ptr_vector<proof_set> m_pinned_active_hyps;
// created sets of parent hypothesis
ptr_vector<expr_set> m_pinned_parent_hyps;
// maps a proof to the transformed proof
obj_map<proof, proof*> m_cache;
// maps a unit literal to its derivation
obj_map<expr, proof*> m_units;
// maps a proof to the set of proofs of active hypotheses
obj_map<proof, proof_set*> m_active_hyps;
// maps a proof to the hypothesis-fact that are transitive
// parents of that proof. Used for cycle detection and avoidance.
obj_map<proof, expr_set*> m_parent_hyps;
void reset();
void compute_hypsets(proof* pr); // compute active_hyps and parent_hyps for pr
void collect_units(proof* pr); // compute m_units
// compute active_hyps and parent_hyps for pr
void compute_hypsets(proof* pr);
// compute m_units
void collect_units(proof* pr);
proof* compute_transformed_proof(proof* pf);
proof* mk_lemma_core(proof *pf, expr *fact);