Skip to content

Commit

Permalink
CDCL Graph v2 (#86)
Browse files Browse the repository at this point in the history
* Parse cdcl

* Rename `Error as E`

* Mostly fix cdcl handling

* Fix remaining issues

* Handle missed case

* Fix `bool_lit` can be zero

* Finalize cdcl

* Undo multiple roots wording

* clippy, fmt

* Add cdcl filters

* Overflow info boxes
  • Loading branch information
JonasAlaif authored Dec 12, 2024
1 parent 760ca23 commit 98c9409
Show file tree
Hide file tree
Showing 37 changed files with 1,112 additions and 267 deletions.
1 change: 1 addition & 0 deletions axiom-profiler-GUI/assets/html/style.css
Original file line number Diff line number Diff line change
Expand Up @@ -386,6 +386,7 @@ li input.td-matcher, li input.td-formatter {
}
.summary .info-boxes {
display: flex;
overflow: auto;
}
.summary .info-box-row {
display: flex;
Expand Down
38 changes: 31 additions & 7 deletions axiom-profiler-GUI/src/screen/file/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,10 @@ use super::{
homepage::{FileInfo, ParseInfo, RcParser},
inst_graph::{
filter::{
DEFAULT_DISABLER_CHAIN, DEFAULT_FILTER_CHAIN, PROOF_DISABLER_CHAIN, PROOF_FILTER_CHAIN,
CDCL_DISABLER_CHAIN, CDCL_FILTER_CHAIN, DEFAULT_DISABLER_CHAIN, DEFAULT_FILTER_CHAIN,
PROOF_DISABLER_CHAIN, PROOF_FILTER_CHAIN,
},
GraphProps,
GraphMode, GraphProps,
},
manager::{NestedScreen, NestedScreenM},
maybe_rc::MaybeRc,
Expand Down Expand Up @@ -101,9 +102,10 @@ pub enum FileM {

pub enum ViewChoice {
Overview,
Graph,
Insts,
MatchingLoop,
Proofs,
Cdcl,
}

impl Screen for File {
Expand Down Expand Up @@ -175,7 +177,7 @@ impl Screen for File {
FileM::ChangeView(view) => {
let view = match view {
ViewChoice::Overview => ViewProps::Overview,
ViewChoice::Graph => {
ViewChoice::Insts => {
let Some(analysis) = self.analysis_or_error(link, 12) else {
return false;
};
Expand All @@ -185,7 +187,7 @@ impl Screen for File {
default_filters: DEFAULT_FILTER_CHAIN.to_vec(),
default_disablers: DEFAULT_DISABLER_CHAIN.to_vec(),
extra: None,
enable_proofs: false,
mode: GraphMode::Inst,
})
}
ViewChoice::MatchingLoop => {
Expand All @@ -208,7 +210,20 @@ impl Screen for File {
default_filters: PROOF_FILTER_CHAIN.to_vec(),
default_disablers: PROOF_DISABLER_CHAIN.to_vec(),
extra: None,
enable_proofs: true,
mode: GraphMode::Proof,
})
}
ViewChoice::Cdcl => {
let Some(analysis) = self.analysis_or_error(link, 14) else {
return false;
};
ViewProps::Graph(GraphProps {
parser: props.parser.clone(),
analysis: analysis.clone(),
default_filters: CDCL_FILTER_CHAIN.to_vec(),
default_disablers: CDCL_DISABLER_CHAIN.to_vec(),
extra: None,
mode: GraphMode::Cdcl,
})
}
};
Expand Down Expand Up @@ -343,7 +358,7 @@ impl File {
hover_text: Some("View with quantifier instantiation graph".to_string()),
disabled: true,
click: Action::MouseDown(
link.callback(|()| FileM::ChangeView(ViewChoice::Graph)),
link.callback(|()| FileM::ChangeView(ViewChoice::Insts)),
),
}),
ElementKind::Simple(SimpleButton {
Expand All @@ -364,6 +379,15 @@ impl File {
link.callback(|()| FileM::ChangeView(ViewChoice::Proofs)),
),
}),
ElementKind::Simple(SimpleButton {
icon: "sports_kabaddi",
text: "CDCL tree".to_string(),
hover_text: Some("View with conflict driven clause learning tree".to_string()),
disabled: props.parser.parser.borrow().proofs().is_empty(),
click: Action::MouseDown(
link.callback(|()| FileM::ChangeView(ViewChoice::Cdcl)),
),
}),
],
}
}
Expand Down
17 changes: 17 additions & 0 deletions axiom-profiler-GUI/src/screen/file/summary.rs
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,7 @@ pub fn Summary(props: &SummaryProps) -> Html {
});
let cost_proofs = html! {<div class="info-box">
<h2 title="The hypotheses which were the most expensive to contradict.">{ "Most expensive hypotheses" }</h2>
<i>{ "Try providing their negation directly." }</i>
<ul>
{ for proofs }
</ul>
Expand All @@ -116,6 +117,21 @@ pub fn Summary(props: &SummaryProps) -> Html {
{ cost_proofs }
</>}
});

let cdcl = props.parser.cdcl.uncut_assigns.iter().take(5);
let cdcl = cdcl.map(|&(p, c)| {
let p = format!("<code class=\"margin-left-half\">{}</code>", p.with(&ctxt));
let p = Html::from_html_unchecked(p.into());
html! { <li><div class="info-box-row">{ format!("{c}:") }{ p }</div></li> }
});
let cost_cdcl = html! {<div class="info-box">
<h2 title="The CDCL assignments which didn't lead to a conflict.">{ "Most common assignments" }</h2>
<i>{ "Try assigning the truth value directly." }</i>
<ul>
{ for cdcl }
</ul>
</div>};

let graph = props.analysis.clone().map(|analysis| {
let file = props.file.clone();
html! {
Expand All @@ -130,6 +146,7 @@ pub fn Summary(props: &SummaryProps) -> Html {
{ metrics }
{ most_quants }
{ analysis }
{ cost_cdcl }
</div>
{graph}
</div>}
Expand Down
57 changes: 49 additions & 8 deletions axiom-profiler-GUI/src/screen/graphviz.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@ use core::fmt;
use smt_log_parser::{
analysis::{
analysis::matching_loop::{MLGraphEdge, MLGraphNode, RecurrenceKind},
raw::{NodeKind, ProofReach},
raw::{CdclEdge, EdgeKind, NodeKind, ProofReach},
visible::VisibleEdge,
},
display_with::{DisplayCtxt, DisplayWithCtxt},
items::{ENodeIdx, MatchKind, QuantPat},
items::{CdclKind, ENodeIdx, MatchKind, QuantPat},
Z3Parser,
};

Expand Down Expand Up @@ -205,6 +205,13 @@ impl
let name = name.map(|n| &parser[n]).unwrap_or_default();
name.to_string()
}
Cdcl(cdcl) => match &parser[cdcl].kind {
CdclKind::Root => "root",
CdclKind::Empty(..) => "empty",
CdclKind::Decision(..) => "decision",
CdclKind::Conflict(..) => "cut",
}
.to_string(),
}
}

Expand All @@ -226,6 +233,10 @@ impl
"filled"
}
}
NodeKind::Cdcl(cdcl) => match &parser[cdcl].kind {
CdclKind::Root | CdclKind::Empty(..) => "filled,dashed",
_ => "filled",
},
_ => "filled",
}
}
Expand All @@ -238,9 +249,9 @@ impl
(Instantiation(..), _, 0) => "invhouse",
(Instantiation(..), _, _) => "diamond",
(ENode(..) | GivenEquality(..) | TransEquality(..), 0, 0) => OTHER_FULL_SHAPE,
(Proof(..), 0, 0) => PROOF_FULL_SHAPE,
(Proof(..) | Cdcl(..), 0, 0) => PROOF_FULL_SHAPE,
(ENode(..) | GivenEquality(..) | TransEquality(..), _, _) => OTHER_SHAPE,
(Proof(..), _, _) => PROOF_SHAPE,
(Proof(..) | Cdcl(..), _, _) => PROOF_SHAPE,
}
}

Expand Down Expand Up @@ -268,12 +279,19 @@ impl
PROOF_COLOUR.to_owned()
}
}
Cdcl(cdcl) => match (parser[cdcl].conflicts, reach.cdcl_dead_branch()) {
(true, _) => FALSE_COLOUR,
(false, true) => EQ_COLOUR,
(false, false) => PROOF_COLOUR,
}
.to_string(),
}
}

fn ordering(&self, (): ()) -> &'static str {
match self {
NodeKind::Instantiation(..) => "in",
NodeKind::Cdcl(..) => "out",
_ => "",
}
}
Expand Down Expand Up @@ -639,8 +657,18 @@ pub trait DotEdgeProperties<
}
}

impl DotEdgeProperties<(), (bool, NodeKind, NodeKind), bool, bool, NodeKind, (), (), (), ()>
for VisibleEdge
impl
DotEdgeProperties<
(),
(bool, NodeKind, NodeKind),
(bool, EdgeKind),
bool,
(EdgeKind, NodeKind),
(),
(),
(),
EdgeKind,
> for VisibleEdge
{
fn tooltip(&self, (is_indirect, from, to): (bool, NodeKind, NodeKind)) -> String {
let arrow = match is_indirect {
Expand All @@ -650,7 +678,10 @@ impl DotEdgeProperties<(), (bool, NodeKind, NodeKind), bool, bool, NodeKind, (),
format!("{} {arrow} {}", from.label(()), to.label(()))
}

fn style(&self, is_indirect: bool) -> &'static str {
fn style(&self, (is_indirect, last): (bool, EdgeKind)) -> &'static str {
if let EdgeKind::Cdcl(CdclEdge::Backtrack) = last {
return "dotted";
}
match is_indirect {
true => "dashed",
false => "solid",
Expand All @@ -664,12 +695,22 @@ impl DotEdgeProperties<(), (bool, NodeKind, NodeKind), bool, bool, NodeKind, (),
}
}

fn arrowhead(&self, blame: NodeKind) -> &'static str {
fn arrowhead(&self, (last, blame): (EdgeKind, NodeKind)) -> &'static str {
if matches!(last, EdgeKind::Cdcl(CdclEdge::RetryFrom)) {
return "none";
}
match blame {
NodeKind::GivenEquality(..) | NodeKind::TransEquality(_) => "empty",
_ => "normal",
}
}

fn constraint(&self, last: EdgeKind) -> &'static str {
match last {
EdgeKind::Cdcl(CdclEdge::Backtrack) => "false",
_ => "",
}
}
}

impl DotEdgeProperties<bool, (), (), (), (), (), (), (), ()> for MLGraphEdge {
Expand Down
4 changes: 4 additions & 0 deletions axiom-profiler-GUI/src/screen/homepage/file.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ use gloo::file::File;
use gloo_net::http::Response;
use serde::{Deserialize, Serialize};
use smt_log_parser::{
analysis::CdclAnalysis,
parsers::{AsyncBufferRead, AsyncParser, ParseState, ReaderState, StreamParser},
LogParser, Z3Parser,
};
Expand Down Expand Up @@ -43,9 +44,11 @@ impl RcParser {
pub fn new(parser: Box<Z3Parser>) -> Self {
let colour_map = QuantIdxToColourMap::new(&parser);
let summary = SummaryAnalysis::new(&parser);
let cdcl = CdclAnalysis::new(&parser);
let parser = Parser {
parser: RefCell::new(*parser),
summary,
cdcl,
colour_map,
};
Self(Rc::new(parser))
Expand All @@ -55,6 +58,7 @@ impl RcParser {
pub struct Parser {
pub parser: RefCell<Z3Parser>,
pub summary: SummaryAnalysis,
pub cdcl: CdclAnalysis,
pub colour_map: QuantIdxToColourMap,
}

Expand Down
44 changes: 42 additions & 2 deletions axiom-profiler-GUI/src/screen/inst_graph/display/node_info.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,13 @@ use std::rc::Rc;

use smt_log_parser::{
analysis::{
raw::{EdgeKind, Node, NodeKind, RawInstGraph},
raw::{CdclEdge, EdgeKind, Node, NodeKind, RawInstGraph},
visible::{VisibleEdge, VisibleEdgeKind},
InstGraph, RawNodeIndex, VisibleEdgeIndex,
},
display_with::{DisplayCtxt, DisplayWithCtxt},
formatter::TermDisplayContext,
items::{MatchKind, VarNames},
items::{CdclKind, MatchKind, VarNames},
};
use yew::{
function_component, html, use_context, AttrValue, Callback, Html, MouseEvent, Properties,
Expand Down Expand Up @@ -68,6 +68,7 @@ impl<'a, 'b> NodeInfo<'a, 'b> {
}
}
NodeKind::Proof(_) => "Proof",
NodeKind::Cdcl(_) => "CDCL",
}
}
pub fn description(&self) -> Html {
Expand Down Expand Up @@ -101,6 +102,20 @@ impl<'a, 'b> NodeInfo<'a, 'b> {
let detail = self.ctxt.parser[pidx].result.with(self.ctxt).to_string();
("Proved", detail)
}
NodeKind::Cdcl(cdcl) => match &self.ctxt.parser[cdcl].kind {
CdclKind::Root => ("Root", "(no assignment)".to_string()),
CdclKind::Empty(..) => ("Empty", "(no assignment)".to_string()),
CdclKind::Decision(assign) => ("Decision", assign.with(self.ctxt).to_string()),
CdclKind::Conflict(conflict) => {
let cut = conflict.cut.iter();
let cut = cut.fold(String::new(), |mut f, c| {
use std::fmt::Write;
let _ = write!(f, "<br>{}", c.with(self.ctxt));
f
});
("Cut (or'd)", cut)
}
},
}
}

Expand Down Expand Up @@ -198,6 +213,18 @@ impl<'a, 'b> NodeInfo<'a, 'b> {
)
}

// CDCL specific
pub fn propagates(&self) -> Option<Vec<String>> {
let cdcl = self.node.kind().cdcl()?;
let propagates = &self.ctxt.parser[cdcl].propagates;
Some(
propagates
.iter()
.map(|assign| assign.with(self.ctxt).to_string())
.collect(),
)
}

pub fn extra_info(&self) -> Option<Vec<(&'static str, String)>> {
let mut extra_info = Vec::new();
if let Some(z3gen) = self
Expand Down Expand Up @@ -314,6 +341,12 @@ pub fn SelectedNodesInfo(
}
});
let proof_hr = proof_step_name.is_some().then(|| html! { <hr/> });
let propagates = info.propagates().filter(|p| !p.is_empty()).map(|propagates| {
let propagates: Html = propagates.into_iter().map(|propagate| html! {
<InfoLine header="Propagate" text={propagate} code=true />
}).collect();
html! { <>{propagates}<hr/></> }
});
let extra_info = info.extra_info().map(|extra_info| {
let extra_info: Html = extra_info.into_iter().map(|(header, info)| html! {
<InfoLine {header} text={info} code=true />
Expand All @@ -334,6 +367,7 @@ pub fn SelectedNodesInfo(
{hypotheses}
{prerequisites}
{proof_hr}
{propagates}
{extra_info}
<InfoLine header="Cost" text={format!("{:.1}", info.node.cost)} code=false />
<InfoLine header="To Root" text={format!("short {}, long {}", info.node.fwd_depth.min, info.node.fwd_depth.max)} code=false />
Expand Down Expand Up @@ -391,6 +425,12 @@ impl<'a, 'b> EdgeInfo<'a, 'b> {
),
Direct(_, EdgeKind::ProofStep) => "Proof Step".to_string(),
Direct(_, EdgeKind::YieldProof) => "Instantiation Proof Step".to_string(),
Direct(_, EdgeKind::Cdcl(kind)) => match kind {
CdclEdge::Decide => "Decide".to_string(),
CdclEdge::RetryFrom => "Retry".to_string(),
CdclEdge::Backtrack => "Backtrack".to_string(),
CdclEdge::Sidetrack => "Sidetrack".to_string(),
},
YieldBlame { pattern_term, .. } => {
format!("Yield/Blame pattern #{pattern_term}")
}
Expand Down
Loading

0 comments on commit 98c9409

Please sign in to comment.