Merge experimental feature axiom-usage-info

Author: utaal

source/air/Cargo.toml

@@ -19,3 +19,4 @@ win32job = "1"
 
 [features]
 singular = []
+axiom-usage-info = []

source/air/src/ast.rs

@@ -176,6 +176,12 @@ pub enum StmtX {
     Switch(Stmts),
 }
 
+#[derive(Debug)]
+pub struct Axiom {
+    pub named: Option<Ident>,
+    pub expr: Expr,
+}
+
 pub type Field = Binder<Typ>;
 pub type Fields = Binders<Typ>;
 pub type Variant = Binder<Fields>;
@@ -192,7 +198,7 @@ pub enum DeclX {
     Const(Ident, Typ),
     Fun(Ident, Typs, Typ),
     Var(Ident, Typ),
-    Axiom(Expr),
+    Axiom(Axiom),
 }
 
 pub type Query = Arc<QueryX>;

source/air/src/ast_util.rs

@@ -1,6 +1,6 @@
 use crate::ast::{
-    BinaryOp, Bind, BindX, Binder, BinderX, Command, CommandX, Constant, DeclX, Expr, ExprX, Exprs,
-    Ident, MultiOp, Qid, Quant, Trigger, Typ, TypX, Typs, UnaryOp,
+    Axiom, BinaryOp, Bind, BindX, Binder, BinderX, Command, CommandX, Constant, Decl, DeclX, Expr,
+    ExprX, Exprs, Ident, MultiOp, Qid, Quant, Trigger, Typ, TypX, Typs, UnaryOp,
 };
 use std::fmt::Debug;
 use std::sync::Arc;
@@ -295,3 +295,7 @@ pub fn mk_neg(e: &Expr) -> Expr {
 pub fn mk_sub(e1: &Expr, e2: &Expr) -> Expr {
     Arc::new(ExprX::Multi(MultiOp::Sub, Arc::new(vec![e1.clone(), e2.clone()])))
 }
+
+pub fn mk_unnamed_axiom(expr: Expr) -> Decl {
+    Arc::new(DeclX::Axiom(Axiom { named: None, expr: expr.clone() }))
+}

source/air/src/closure.rs

@@ -1,8 +1,8 @@
 use crate::ast::{
-    BinaryOp, BindX, Binder, Binders, Constant, Decl, DeclX, Expr, ExprX, Ident, MultiOp, Qid,
-    Quant, Stmt, StmtX, Stmts, Trigger, Triggers, Typ, TypX, Typs, UnaryOp,
+    Axiom, BinaryOp, BindX, Binder, Binders, Constant, Decl, DeclX, Expr, ExprX, Ident, MultiOp,
+    Qid, Quant, Stmt, StmtX, Stmts, Trigger, Triggers, Typ, TypX, Typs, UnaryOp,
 };
-use crate::ast_util::{ident_binder, mk_and, mk_eq, mk_forall};
+use crate::ast_util::{ident_binder, mk_and, mk_eq, mk_forall, mk_unnamed_axiom};
 use crate::context::Context;
 use crate::typecheck::{typ_eq, DeclaredX};
 use crate::util::vec_map;
@@ -248,7 +248,7 @@ fn simplify_lambda(
                 trigs
             });
             let forall = mk_forall(&bs, &trigs, qid.clone(), &eq);
-            let decl = Arc::new(DeclX::Axiom(forall));
+            let decl = mk_unnamed_axiom(forall);
             state.generated_decls.push(decl);
 
             closure_fun
@@ -370,7 +370,7 @@ fn simplify_choose(
             let trigs = Arc::new(vec![trig]);
             let forall_qid = None; // The forall uses a trivial trigger, so no need to profile
             let forall = mk_forall(&bs, &trigs, forall_qid, &imply);
-            let decl = Arc::new(DeclX::Axiom(forall));
+            let decl = mk_unnamed_axiom(forall);
             state.generated_decls.push(decl);
 
             closure_fun
@@ -664,9 +664,9 @@ pub(crate) fn simplify_decl(ctxt: &mut Context, decl: &Decl) -> (Vec<Decl>, Decl
         DeclX::Const(..) => decl.clone(),
         DeclX::Fun(..) => decl.clone(),
         DeclX::Var(..) => decl.clone(),
-        DeclX::Axiom(expr) => {
+        DeclX::Axiom(Axiom { named, expr }) => {
             let (_, expr, _) = simplify_expr(ctxt, &mut state, expr);
-            Arc::new(DeclX::Axiom(expr))
+            Arc::new(DeclX::Axiom(Axiom { named: named.clone(), expr }))
         }
     };
     (state.generated_decls, decl)

source/air/src/context.rs

@@ -36,9 +36,16 @@ pub(crate) struct AxiomInfo {
     pub(crate) decl: Decl,
 }
 
+#[cfg(feature = "axiom-usage-info")]
+#[derive(Debug)]
+pub enum UsageInfo {
+    None,
+    UsedAxioms(Vec<Ident>),
+}
+
 #[derive(Debug)]
 pub enum ValidityResult {
-    Valid,
+    Valid(#[cfg(feature = "axiom-usage-info")] UsageInfo),
     Invalid(Option<Model>, Option<ArcDynMessage>, Option<AssertId>),
     Canceled,
     TypeError(TypeError),
@@ -91,6 +98,7 @@ pub struct Context {
     pub(crate) expected_solver_version: Option<String>,
     pub(crate) profile_logfile_name: Option<String>,
     pub(crate) disable_incremental_solving: bool,
+    pub(crate) usage_info_enabled: bool,
     pub(crate) check_valid_used: bool,
 }
 
@@ -128,6 +136,7 @@ impl Context {
             expected_solver_version: None,
             profile_logfile_name: None,
             disable_incremental_solving: false,
+            usage_info_enabled: false,
             check_valid_used: false,
         };
         context.axiom_infos.push_scope(false);
@@ -206,6 +215,12 @@ impl Context {
         self.air_final_log.log_set_option("disable_incremental_solving", "true");
     }
 
+    pub fn enable_usage_info(&mut self) {
+        assert!(matches!(self.state, ContextState::NotStarted));
+        self.usage_info_enabled = true;
+        self.set_z3_param_bool("produce-unsat-cores", true, true);
+    }
+
     // emit blank line into log files
     pub fn blank_line(&mut self) {
         self.air_initial_log.blank_line();
@@ -466,21 +481,33 @@ impl Context {
         match &**command {
             CommandX::Push => {
                 self.push();
-                ValidityResult::Valid
+                ValidityResult::Valid(
+                    #[cfg(feature = "axiom-usage-info")]
+                    UsageInfo::None,
+                )
             }
             CommandX::Pop => {
                 self.pop();
-                ValidityResult::Valid
+                ValidityResult::Valid(
+                    #[cfg(feature = "axiom-usage-info")]
+                    UsageInfo::None,
+                )
             }
             CommandX::SetOption(option, value) => {
                 self.set_z3_param(option, value);
-                ValidityResult::Valid
+                ValidityResult::Valid(
+                    #[cfg(feature = "axiom-usage-info")]
+                    UsageInfo::None,
+                )
             }
             CommandX::Global(decl) => {
                 if let Err(err) = self.global(&decl) {
                     ValidityResult::TypeError(err)
                 } else {
-                    ValidityResult::Valid
+                    ValidityResult::Valid(
+                        #[cfg(feature = "axiom-usage-info")]
+                        UsageInfo::None,
+                    )
                 }
             }
             CommandX::CheckValid(query) => {

source/air/src/emitter.rs

@@ -1,4 +1,4 @@
-use crate::ast::{Decl, Expr, Query};
+use crate::ast::{Decl, Expr, Ident, Query};
 use crate::printer::{macro_push_node, NodeWriter, Printer};
 use crate::{node, nodes};
 use sise::Node;
@@ -137,9 +137,14 @@ impl Emitter {
         }
     }
 
-    pub fn log_assert(&mut self, expr: &Expr) {
+    pub fn log_assert(&mut self, named: &Option<Ident>, expr: &Expr) {
         if !self.is_none() {
-            self.log_node(&nodes!(assert {self.printer.expr_to_node(expr)}));
+            self.log_node(&
+                if let Some(named) = named {
+                    nodes!(assert ({Node::Atom("!".to_string())} {self.printer.expr_to_node(expr)} {Node::Atom(":named".to_string())} {Node::Atom((**named).clone())}))
+                } else {
+                    nodes!(assert {self.printer.expr_to_node(expr)})
+                })
         }
     }
 

source/air/src/main.rs

@@ -1,4 +1,6 @@
 use air::ast::CommandX;
+#[cfg(feature = "axiom-usage-info")]
+use air::context::UsageInfo;
 use air::context::{Context, ValidityResult};
 use air::messages::{AirMessage, AirMessageLabel, Reporter};
 use air::profiler::{Profiler, PROVER_LOG_FILE};
@@ -138,11 +140,29 @@ pub fn main() {
         let result =
             air_context.command(&*message_interface, &reporter, &command, Default::default());
         match result {
-            ValidityResult::Valid => {
+            #[cfg(not(feature = "axiom-usage-info"))]
+            ValidityResult::Valid() => {
                 if let CommandX::CheckValid(_) = &**command {
                     count_verified += 1;
                 }
             }
+            #[cfg(feature = "axiom-usage-info")]
+            ValidityResult::Valid(usage_info) => {
+                if let CommandX::CheckValid(_) = &**command {
+                    count_verified += 1;
+
+                    if let UsageInfo::UsedAxioms(axioms) = usage_info {
+                        println!(
+                            "Query used named axioms: {}",
+                            axioms
+                                .iter()
+                                .map(|x| (**x).clone())
+                                .collect::<Vec<String>>()
+                                .join(", ")
+                        )
+                    }
+                }
+            }
             ValidityResult::TypeError(err) => {
                 panic!("Type error: {}", err);
             }

source/air/src/parser.rs

@@ -1,7 +1,7 @@
 use crate::ast::{
-    BinaryOp, BindX, Binder, BinderX, Binders, Command, CommandX, Commands, Constant, Decl, DeclX,
-    Decls, Expr, ExprX, Exprs, Ident, MultiOp, Qid, Quant, QueryX, Relation, Stmt, StmtX, Stmts,
-    Trigger, Triggers, Typ, TypX, UnaryOp,
+    Axiom, BinaryOp, BindX, Binder, BinderX, Binders, Command, CommandX, Commands, Constant, Decl,
+    DeclX, Decls, Expr, ExprX, Exprs, Ident, MultiOp, Qid, Quant, QueryX, Relation, Stmt, StmtX,
+    Stmts, Trigger, Triggers, Typ, TypX, UnaryOp,
 };
 use crate::def::mk_skolem_id;
 use crate::messages::ArcDynMessageLabel;
@@ -444,6 +444,28 @@ impl Parser {
         }
     }
 
+    fn nodes_to_named(&self, nodes: &[Node]) -> Result<Option<Ident>, String> {
+        let mut named = None;
+        let mut consume_named = false;
+
+        for node in nodes {
+            match node {
+                Node::Atom(s) if s.to_string() == ":named" => {
+                    consume_named = true;
+                }
+                Node::Atom(s) if consume_named && named.is_none() => {
+                    named = Some(Arc::new(s.clone()));
+                    consume_named = false;
+                }
+                _ => {
+                    return Err(format!("expected :named; found {}", node_to_string(node)));
+                }
+            }
+        }
+
+        Ok(named)
+    }
+
     fn node_to_quant_or_lambda_expr(
         &self,
         quantchooselambda: QuantOrChooseOrLambda,
@@ -621,9 +643,19 @@ impl Parser {
                     let typ = self.node_to_typ(t)?;
                     Ok(Arc::new(DeclX::Var(Arc::new(x.clone()), typ)))
                 }
-                [Node::Atom(s), e] if s.to_string() == "axiom" => {
+                [Node::Atom(s), axiom_node] if s.to_string() == "axiom" => {
+                    let (e, named) = match &axiom_node {
+                        Node::List(nodes) if nodes.len() >= 2 => match &nodes[0] {
+                            Node::Atom(s) if s.to_string() == "!" => {
+                                let named = self.nodes_to_named(&nodes[2..])?;
+                                (&nodes[1], named)
+                            }
+                            _ => (axiom_node, None),
+                        },
+                        _ => (axiom_node, None),
+                    };
                     let expr = self.node_to_expr(e)?;
-                    Ok(Arc::new(DeclX::Axiom(expr)))
+                    Ok(Arc::new(DeclX::Axiom(Axiom { named, expr })))
                 }
                 _ => Err(format!("expected declaration, found: {}", node_to_string(node))),
             },

source/air/src/printer.rs

@@ -1,6 +1,6 @@
 use crate::ast::{
-    BinaryOp, BindX, Binder, Binders, Constant, Datatypes, Decl, DeclX, Expr, ExprX, Exprs, Ident,
-    MultiOp, Qid, Quant, Query, QueryX, Stmt, StmtX, Triggers, Typ, TypX, Typs, UnaryOp,
+    Axiom, BinaryOp, BindX, Binder, Binders, Constant, Datatypes, Decl, DeclX, Expr, ExprX, Exprs,
+    Ident, MultiOp, Qid, Quant, Query, QueryX, Stmt, StmtX, Triggers, Typ, TypX, Typs, UnaryOp,
 };
 use crate::def::mk_skolem_id;
 use crate::util::vec_map;
@@ -366,14 +366,23 @@ impl Printer {
         nodes!(declare-var {str_to_node(x)} {self.typ_to_node(typ)})
     }
 
+    pub fn axiom_to_node(&self, axiom: &Axiom) -> Node {
+        let Axiom { named, expr } = axiom;
+        if let Some(named) = named {
+            nodes!(axiom ({str_to_node("!")} {self.expr_to_node(expr)} {str_to_node(":named")} {str_to_node(named)}))
+        } else {
+            nodes!(axiom {self.expr_to_node(expr)})
+        }
+    }
+
     pub fn decl_to_node(&self, decl: &Decl) -> Node {
         match &**decl {
             DeclX::Sort(x) => self.sort_decl_to_node(x),
             DeclX::Datatypes(datatypes) => self.datatypes_decl_to_node(datatypes),
             DeclX::Const(x, typ) => self.const_decl_to_node(x, typ),
             DeclX::Fun(x, typs, typ) => self.fun_decl_to_node(x, typs, typ),
             DeclX::Var(x, typ) => self.var_decl_to_node(x, typ),
-            DeclX::Axiom(expr) => nodes!(axiom {self.expr_to_node(expr)}),
+            DeclX::Axiom(axiom) => self.axiom_to_node(axiom),
         }
     }