1use crate::prelude::*;
2use std::collections::HashMap;
3use std::rc::Rc;
4use std::result::Result;
5
6impl Runtime {
9 pub fn verify_or_fact_with_known_forall(
10 &mut self,
11 or_fact: &OrFact,
12 verify_state: &VerifyState,
13 ) -> Result<StmtResult, RuntimeError> {
14 if let Some(fact_verified) =
15 self.try_verify_or_fact_with_known_forall_facts_in_envs(or_fact, verify_state)?
16 {
17 return Ok((fact_verified).into());
18 }
19 Ok((StmtUnknown::new()).into())
20 }
21
22 fn get_matched_or_fact_in_known_forall_fact_in_envs(
23 &mut self,
24 iterate_from_env_index: usize,
25 iterate_from_known_forall_fact_index: usize,
26 given_or_fact: &OrFact,
27 ) -> Result<
28 (
29 (usize, usize),
30 Option<HashMap<String, Obj>>,
31 Option<(OrFact, Rc<KnownForallFactParamsAndDom>)>,
32 ),
33 RuntimeError,
34 > {
35 let lookup_key = given_or_fact.key();
36
37 let envs_count = self.environment_stack.len();
38 for i in iterate_from_env_index..envs_count {
39 let stack_idx = envs_count - 1 - i;
40 let known_forall_facts_count = {
41 let env = &self.environment_stack[stack_idx];
42 match env.known_or_facts_in_forall_facts.get(lookup_key.as_str()) {
43 Some(v) => v.len(),
44 None => continue,
45 }
46 };
47 for j in iterate_from_known_forall_fact_index..known_forall_facts_count {
48 let entry_idx = known_forall_facts_count - 1 - j;
49 let (fact_args_in_known_forall, given_fact_args, current_known_forall) = {
50 let env = &self.environment_stack[stack_idx];
51 let Some(known_forall_facts_in_env) =
52 env.known_or_facts_in_forall_facts.get(lookup_key.as_str())
53 else {
54 continue;
55 };
56 let Some(current_known_forall) = known_forall_facts_in_env.get(entry_idx)
57 else {
58 continue;
59 };
60 (
61 current_known_forall.0.get_args_from_fact(),
62 given_or_fact.get_args_from_fact(),
63 current_known_forall.clone(),
64 )
65 };
66 let match_result = self.match_args_in_fact_in_known_forall_fact_with_given_args(
67 &fact_args_in_known_forall,
68 &given_fact_args,
69 )?;
70 if let Some(arg_map) = match_result {
71 return Ok(((i, j), Some(arg_map), Some(current_known_forall)));
72 }
73 }
74 }
75
76 Ok(((0, 0), None, None))
77 }
78
79 fn try_verify_or_fact_with_known_forall_facts_in_envs(
80 &mut self,
81 or_fact: &OrFact,
82 verify_state: &VerifyState,
83 ) -> Result<Option<FactualStmtSuccess>, RuntimeError> {
84 let mut iterate_from_env_index = 0;
85 let mut iterate_from_known_forall_fact_index = 0;
86
87 loop {
88 let result = self.get_matched_or_fact_in_known_forall_fact_in_envs(
89 iterate_from_env_index,
90 iterate_from_known_forall_fact_index,
91 or_fact,
92 )?;
93 let ((i, j), arg_map_opt, known_forall_opt) = result;
94 match (arg_map_opt, known_forall_opt) {
95 (Some(arg_map), Some((or_fact_in_known_forall, forall_rc))) => {
96 if let Some(fact_verified) = self
97 .verify_or_fact_args_satisfy_forall_requirements(
98 &or_fact_in_known_forall,
99 &forall_rc,
100 arg_map,
101 or_fact,
102 verify_state,
103 )?
104 {
105 return Ok(Some(fact_verified));
106 }
107 iterate_from_env_index = i;
108 iterate_from_known_forall_fact_index = j + 1;
109 }
110 _ => return Ok(None),
111 }
112 }
113 }
114
115 fn verify_or_fact_args_satisfy_forall_requirements(
116 &mut self,
117 or_fact_in_known_forall: &OrFact,
118 known_forall: &Rc<KnownForallFactParamsAndDom>,
119 arg_map: HashMap<String, Obj>,
120 given_or_fact: &OrFact,
121 verify_state: &VerifyState,
122 ) -> Result<Option<FactualStmtSuccess>, RuntimeError> {
123 let param_names = known_forall.params_def.collect_param_names();
124
125 if !param_names
126 .iter()
127 .all(|param_name| arg_map.contains_key(param_name))
128 {
129 return Ok(None);
130 }
131
132 let mut args_for_params: Vec<Obj> = Vec::new();
133
134 for param_name in param_names.iter() {
135 let obj = match arg_map.get(param_name) {
136 Some(v) => v,
137 None => return Ok(None),
138 };
139
140 args_for_params.push(obj.clone());
141 }
142
143 let args_param_types = self
144 .verify_args_satisfy_param_def_flat_types(
145 &known_forall.params_def,
146 &args_for_params,
147 verify_state,
148 ParamObjType::Forall,
149 )
150 .map_err(|e| {
151 {
152 RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
153 Some(Fact::from(given_or_fact.clone()).into_stmt()),
154 String::new(),
155 given_or_fact.line_file.clone(),
156 Some(e),
157 vec![],
158 )))
159 }
160 })?;
161 if args_param_types.is_unknown() {
162 return Ok(None);
163 }
164
165 let param_to_arg_map = match known_forall
166 .params_def
167 .param_def_params_to_arg_map(&arg_map)
168 {
169 Some(m) => m,
170 None => return Ok(None),
171 };
172
173 for dom_fact in known_forall.dom.iter() {
174 let instantiated_dom_fact = self
175 .inst_fact(dom_fact, ¶m_to_arg_map, ParamObjType::Forall, None)
176 .map_err(|e| {
177 {
178 RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
179 Some(Fact::from(given_or_fact.clone()).into_stmt()),
180 String::new(),
181 given_or_fact.line_file.clone(),
182 Some(e),
183 vec![],
184 )))
185 }
186 })?;
187 let result = self
188 .verify_fact(&instantiated_dom_fact, verify_state)
189 .map_err(|e| {
190 {
191 RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
192 Some(Fact::from(given_or_fact.clone()).into_stmt()),
193 String::new(),
194 given_or_fact.line_file.clone(),
195 Some(e),
196 vec![],
197 )))
198 }
199 })?;
200 if result.is_unknown() {
201 return Ok(None);
202 }
203 }
204
205 let verified_by_known_forall_fact = ForallFact::new(
206 known_forall.params_def.clone(),
207 known_forall.dom.clone(),
208 vec![or_fact_in_known_forall.clone().into()],
209 known_forall.line_file.clone(),
210 )?;
211 let fact_verified = FactualStmtSuccess::new_with_verified_by_known_fact(
212 given_or_fact.clone().into(),
213 VerifiedByResult::wrap_bys(vec![VerifiedBysEnum::cited_fact(
214 given_or_fact.clone().into(),
215 verified_by_known_forall_fact.clone().into(),
216 None,
217 )]),
218 Vec::new(),
219 );
220 Ok(Some(fact_verified))
221 }
222}