Add resident speculate: test an instantiation hypothesis on a retained query

source/air/src/context.rs

@@ -650,6 +650,13 @@ pub struct Context {
     /// An equality to assert in the next query's scope just before its first
     /// `check-sat` (cvc5 only).
     pub(crate) inject_equality: Option<(sise::TreeNode, sise::TreeNode)>,
+    /// A hypothesis to send in the next query's scope just before its first
+    /// `check-sat` (cvc5 only, see `speculate`).
+    pub(crate) speculation: Option<crate::speculate::SpeculationRequest>,
+    /// cvc5's reply to the last hypothesis sent, until the caller takes it.
+    pub(crate) last_speculation: Option<crate::speculate::SpeculationReply>,
+    /// Whether this solver serves `(speculate ...)`, once asked.
+    speculation_supported: Option<bool>,
 }
 
 impl Context {
@@ -746,6 +753,9 @@ impl Context {
             egraph_focus: None,
             last_egraph: None,
             inject_equality: None,
+            speculation: None,
+            last_speculation: None,
+            speculation_supported: None,
             branch_profile: false,
             last_branch_profile: None,
             solver,
@@ -1198,6 +1208,74 @@ impl Context {
         Ok(())
     }
 
+    /// Whether this solver serves `(speculate ...)`, which it does if it
+    /// answers `(get-info :speculation)`; asked once (cvc5 only). A solver
+    /// without the command would end at it, so ask before `set_speculation`.
+    pub fn supports_speculation(&mut self) -> bool {
+        if !matches!(self.solver, SmtSolver::Cvc5) {
+            return false;
+        }
+        if let Some(supported) = self.speculation_supported {
+            return supported;
+        }
+        self.ensure_started();
+        self.smt_log.log_get_info("speculation");
+        let smt_data = self.smt_log.take_pipe_data();
+        let lines = self.get_smt_process().send_commands(smt_data);
+        let supported = lines.iter().any(|line| line.starts_with("(:speculation "));
+        self.speculation_supported = Some(supported);
+        supported
+    }
+
+    /// Send `request` in the next query's scope, after its assertions and
+    /// just before its first `check-sat`, and read `(get-info :speculation)`
+    /// right after that check (cvc5 with `supports_speculation` only).
+    /// `finish_query` pops the hypothesis with the scope. Take the reply with
+    /// `take_speculation`; when cvc5 refused the command, the reply carries
+    /// its error and the check answers `Canceled` without a `check-sat`.
+    /// `None` also drops a request that a check which never reached the
+    /// solver left behind.
+    pub fn set_speculation(&mut self, request: Option<crate::speculate::SpeculationRequest>) {
+        assert!(request.is_none() || matches!(self.solver, SmtSolver::Cvc5));
+        self.speculation = request;
+    }
+
+    /// The reply to the hypothesis of the most recent query, if one was sent;
+    /// each call returns it once.
+    pub fn take_speculation(&mut self) -> Option<crate::speculate::SpeculationReply> {
+        self.last_speculation.take().map(|mut reply| {
+            reply.variable_versions = self.variable_versions.clone();
+            reply
+        })
+    }
+
+    /// The universal quantifier named `qid` that `decls` or `query` asserts,
+    /// as the solver is sent it, the query's own first.
+    pub fn find_quantifier<'a>(
+        &self,
+        decls: impl Iterator<Item = &'a Decl>,
+        query: &Query,
+        qid: &str,
+    ) -> Option<crate::speculate::QuantifierSmt> {
+        let printer =
+            crate::printer::Printer::new(self.message_interface.clone(), true, self.solver.clone());
+        crate::speculate::find_quantifier(decls, query, qid, &printer)
+    }
+
+    /// The universal quantifiers `decls` and `query` assert that `keep`
+    /// accepts, by qid and whether the query asserts them, as the solver is
+    /// sent them: the query's own first, each qid once.
+    pub fn quantifiers<'a>(
+        &self,
+        decls: impl Iterator<Item = &'a Decl>,
+        query: &Query,
+        keep: impl Fn(&str, bool) -> bool,
+    ) -> Vec<crate::speculate::QuantifierSmt> {
+        let printer =
+            crate::printer::Printer::new(self.message_interface.clone(), true, self.solver.clone());
+        crate::speculate::quantifiers(decls, query, &printer, keep)
+    }
+
     pub fn set_profile_with_logfile_name(&mut self, file_name: String) {
         assert!(matches!(self.state, ContextState::NotStarted));
         self.profile_logfile_name = Some(file_name);
@@ -1460,7 +1538,7 @@ impl Context {
         };
         let (query, snapshots, local_vars, variable_versions) = crate::var_to_const::lower_query(
             &query,
-            self.provenance || self.egraph_request.is_some(),
+            self.provenance || self.egraph_request.is_some() || self.speculation.is_some(),
         );
         self.variable_versions = variable_versions;
         self.air_middle_log.log_query(&query);

source/air/src/lib.rs

@@ -13,6 +13,7 @@ pub mod profiler;
 pub mod remove_asserts;
 pub mod scope_map;
 pub mod smt_process;
+pub mod speculate;
 pub mod twin;
 
 #[macro_use]
@@ -27,6 +28,7 @@ mod tests;
 mod typecheck;
 mod util;
 mod var_to_const;
+pub use var_to_const::GoalScope;
 mod visitor;
 
 #[cfg(feature = "singular")]

source/air/src/smt_verify.rs

@@ -200,6 +200,9 @@ pub type ReportLongRunning<'a> =
     (std::time::Duration, Box<dyn FnMut(std::time::Duration, bool) -> () + 'a>);
 
 const GET_VERSION_RESPONSE_PREFIX: &str = "(:version";
+/// Echoed just before a `(speculate ...)` command: the early flush's output
+/// after it is the command's.
+const SPECULATION_MARKER: &str = "air-speculate";
 
 pub(crate) fn smt_check_assertion<'ctx>(
     context: &mut Context,
@@ -244,6 +247,22 @@ pub(crate) fn smt_check_assertion<'ctx>(
         None
     };
 
+    // A hypothesis goes in the query's scope before the flush below, so that a
+    // term cvc5 cannot read is refused there, before any check-sat. Only the
+    // query's first check sends it: later rounds share its scope. An echoed
+    // marker goes first, so that only an error after it is the hypothesis's.
+    let speculation = context.speculation.take();
+    if let Some(request) = &speculation {
+        context.last_speculation = None;
+        context.smt_log.log_node(&sise::TreeNode::List(vec![
+            sise::TreeNode::Atom("echo".to_string()),
+            sise::TreeNode::Atom(format!("\"{SPECULATION_MARKER}\"")),
+        ]));
+        context.smt_log.log_node(&request.to_node());
+    }
+    let mut past_speculation_marker = false;
+    let mut speculation_refused = None;
+
     context.smt_log.log_get_info("version");
     let smt_init_start_time = std::time::Instant::now();
     let smt_data = context.smt_log.take_pipe_data();
@@ -267,6 +286,10 @@ pub(crate) fn smt_check_assertion<'ctx>(
                     );
                 }
             }
+        } else if speculation.is_some() && line.trim_matches('"') == SPECULATION_MARKER {
+            past_speculation_marker = true;
+        } else if past_speculation_marker && line.starts_with("(error") {
+            speculation_refused = Some(line);
         } else if context.ignore_unexpected_smt {
             diagnostics.report(&context.message_interface.bare(
                 crate::messages::MessageLevel::Warning,
@@ -277,6 +300,14 @@ pub(crate) fn smt_check_assertion<'ctx>(
         }
     }
 
+    // cvc5 could not read the hypothesis, so there is nothing to check.
+    if let Some(error) = speculation_refused {
+        context.last_speculation =
+            Some(crate::speculate::SpeculationReply { error: Some(error), ..Default::default() });
+        context.state = ContextState::Canceled;
+        return ValidityResult::Canceled;
+    }
+
     if let Some(disabled_expr) = disabled_expr {
         context.smt_log.log_assert(&None, &None, &disabled_expr);
     }
@@ -327,6 +358,11 @@ pub(crate) fn smt_check_assertion<'ctx>(
         // in the same batch, right after the answer it describes
         context.smt_log.log_get_info("inst-pressure");
     }
+    if speculation.is_some() {
+        // in the same batch, right after the answer it describes and before
+        // the scope holding the hypothesis is popped
+        context.smt_log.log_get_info("speculation");
+    }
     if context.branch_profile {
         // in the same batch, right after the answer it describes
         context.smt_log.log_get_info("branch-profile");
@@ -398,6 +434,7 @@ pub(crate) fn smt_check_assertion<'ctx>(
     let mut nl_frontier = None;
     let mut egraph_lines: Vec<String> = Vec::new();
     let mut inst_pressure = None;
+    let mut speculation_reply = None;
     let mut branch_profile = None;
     let mut check_effort = None;
     let mut strategy_rung = None;
@@ -435,6 +472,8 @@ pub(crate) fn smt_check_assertion<'ctx>(
             // a cvc5 without the key; say so rather than fail the query
             inst_pressure =
                 Some(crate::context::InstPressure { unparsed: Some(line), ..Default::default() });
+        } else if speculation.is_some() && line.starts_with("(:speculation (") {
+            speculation_reply = Some(crate::speculate::parse_speculation(&line));
         } else if context.branch_profile && line.starts_with("(:branch-profile ") {
             branch_profile = Some(parse_branch_profile(&line));
         } else if context.branch_profile && branch_profile.is_none() && line == "unsupported" {
@@ -495,6 +534,13 @@ pub(crate) fn smt_check_assertion<'ctx>(
     context.last_nl_frontier = nl_frontier;
     context.last_difficulty = difficulty;
     context.last_inst_pressure = inst_pressure;
+    if speculation.is_some() {
+        context.last_speculation =
+            Some(speculation_reply.unwrap_or_else(|| crate::speculate::SpeculationReply {
+                unparsed: Some("no (:speculation ...) reply".to_string()),
+                ..Default::default()
+            }));
+    }
     context.last_branch_profile = branch_profile;
     context.last_check_effort = check_effort;
     if egraph_asked {
@@ -714,7 +760,7 @@ pub(crate) fn parse_nl_frontier(line: &str) -> crate::context::NlFrontier {
 /// A reply subterm as text: lists re-joined, quoted symbols unquoted (see
 /// `bar_symbols_as_strings`), unless whitespace or parentheses in one mean
 /// only its bars keep it one symbol.
-fn sexp_text(node: &sise::TreeNode) -> String {
+pub(crate) fn sexp_text(node: &sise::TreeNode) -> String {
     match node {
         sise::TreeNode::Atom(a) => match a.strip_prefix('"').and_then(|t| t.strip_suffix('"')) {
             Some(t) if t.contains(|c: char| c.is_whitespace() || c == '(' || c == ')') => {
@@ -824,15 +870,15 @@ fn parse_nl_atom(node: &sise::TreeNode) -> Option<crate::context::NlAtom> {
 
 /// A count from a solver reply. cvc5 prints arbitrary-precision integers, so
 /// one too large for u64 saturates rather than fails.
-fn difficulty_count(v: &str) -> Option<u64> {
+pub(crate) fn difficulty_count(v: &str) -> Option<u64> {
     (!v.is_empty() && v.bytes().all(|b| b.is_ascii_digit()))
         .then(|| v.parse::<u64>().unwrap_or(u64::MAX))
 }
 
 /// cvc5 quotes a symbol that needs it as `|...|`, which sise cannot read, so
 /// spell each one as a sise string. A symbol that cannot be a sise string
 /// (it holds `"` or `\`) is left alone, and the reply stays unparsed.
-fn bar_symbols_as_strings(line: &str) -> String {
+pub(crate) fn bar_symbols_as_strings(line: &str) -> String {
     let mut out = String::with_capacity(line.len());
     let mut rest = line;
     while let Some(start) = rest.find('|') {