use crate::prelude::*;
impl Runtime {
pub fn verify_non_equational_atomic_fact(
&mut self,
atomic_fact: &AtomicFact,
verify_state: &VerifyState,
post_process: bool,
) -> Result<StmtResult, RuntimeError> {
let mut result =
self.verify_non_equational_atomic_fact_with_builtin_rules(atomic_fact, verify_state)?;
if result.is_true() {
return Ok(result);
}
result = self.verify_non_equational_atomic_fact_with_known_atomic_facts(atomic_fact)?;
if result.is_true() {
return Ok(result);
}
if verify_state.is_round_0() {
let verify_state_add_one_round = verify_state.new_state_with_round_increased();
if let Some(verified_by_definition) =
self.verify_atomic_fact_using_builtin_or_prop_definition(atomic_fact, verify_state)?
{
return Ok(verified_by_definition);
}
result = self
.verify_atomic_fact_with_known_forall(atomic_fact, &verify_state_add_one_round)?;
if result.is_true() {
return Ok(result);
}
}
if post_process {
result =
self.post_process_non_equational_atomic_fact(atomic_fact, verify_state, result)?;
if result.is_true() {
return Ok(result);
}
}
Ok((StmtUnknown::new()).into())
}
pub fn verify_fact(
&mut self,
fact: &Fact,
verify_state: &VerifyState,
) -> Result<StmtResult, RuntimeError> {
match fact {
Fact::AtomicFact(atomic_fact) => self.verify_atomic_fact(atomic_fact, verify_state),
Fact::AndFact(and_fact) => self.verify_and_fact(and_fact, verify_state),
Fact::ChainFact(chain_fact) => self.verify_chain_fact(chain_fact, verify_state),
Fact::ForallFact(forall_fact) => self.verify_forall_fact(forall_fact, verify_state),
Fact::ForallFactWithIff(forall_iff) => {
self.verify_forall_fact_with_iff(forall_iff, verify_state)
}
Fact::NotForall(not_forall) => self.verify_not_forall_fact(not_forall, verify_state),
Fact::ExistFact(exist_fact) => self.verify_exist_fact(exist_fact, verify_state),
Fact::OrFact(or_fact) => self.verify_or_fact(or_fact, verify_state),
}
}
fn post_process_non_equational_atomic_fact(
&mut self,
atomic_fact: &AtomicFact,
verify_state: &VerifyState,
result: StmtResult,
) -> Result<StmtResult, RuntimeError> {
let result = self.builtin_post_process_non_equational_atomic_fact(
atomic_fact,
verify_state,
result,
)?;
if result.is_true() {
return Ok(result);
}
let result = self.use_known_reflexive_prop(atomic_fact, result)?;
if result.is_true() {
return Ok(result);
}
self.use_known_symmetric_prop(atomic_fact, verify_state, result)
}
fn builtin_post_process_non_equational_atomic_fact(
&mut self,
atomic_fact: &AtomicFact,
verify_state: &VerifyState,
result: StmtResult,
) -> Result<StmtResult, RuntimeError> {
let Some(transposed_fact) = atomic_fact.transposed_binary_order_equivalent() else {
return Ok(result);
};
let transposed_result =
self.verify_non_equational_atomic_fact(&transposed_fact, verify_state, false)?;
Self::wrap_post_process_alternate_fact_result(atomic_fact, transposed_result, result)
}
fn use_known_reflexive_prop(
&mut self,
atomic_fact: &AtomicFact,
result: StmtResult,
) -> Result<StmtResult, RuntimeError> {
let AtomicFact::NormalAtomicFact(f) = atomic_fact else {
return Ok(result);
};
if f.body.len() != 2 {
return Ok(result);
}
if f.body[0].to_string() != f.body[1].to_string() {
return Ok(result);
}
let prop_name = f.predicate.to_string();
for env in self.iter_environments_from_top() {
if env.known_reflexive_props.contains_key(&prop_name) {
return Ok(
FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
atomic_fact.clone().into(),
"registered reflexive prop".to_string(),
Vec::new(),
)
.into(),
);
}
}
Ok(result)
}
fn use_known_symmetric_prop(
&mut self,
atomic_fact: &AtomicFact,
verify_state: &VerifyState,
result: StmtResult,
) -> Result<StmtResult, RuntimeError> {
let AtomicFact::NormalAtomicFact(f) = atomic_fact else {
return Ok(result);
};
if f.body.len() < 2 {
return Ok(result);
}
let prop_name = f.predicate.to_string();
let mut permutations: Vec<Vec<usize>> = Vec::new();
for env in self.iter_environments_from_top() {
if let Some(perms) = env.known_symmetric_props.get(&prop_name) {
for g in perms {
if g.len() == f.body.len() {
permutations.push(g.clone());
}
}
}
}
for gather in permutations {
let Some(alt) = atomic_fact.symmetric_reordered_args(&gather) else {
continue;
};
let alt_result = self.verify_non_equational_atomic_fact(&alt, verify_state, false)?;
if alt_result.is_true() {
return Self::wrap_post_process_alternate_fact_result(
atomic_fact,
alt_result,
result,
);
}
}
Ok(result)
}
fn wrap_post_process_alternate_fact_result(
original: &AtomicFact,
alternate_result: StmtResult,
fallback: StmtResult,
) -> Result<StmtResult, RuntimeError> {
match alternate_result {
StmtResult::FactualStmtSuccess(inner_success) => {
let FactualStmtSuccess {
verified_by,
infers: _,
stmt: _,
} = inner_success;
Ok(FactualStmtSuccess::new_with_verified_by_known_fact(
original.clone().into(),
verified_by,
Vec::new(),
)
.into())
}
other if other.is_true() => Ok(other),
_ => Ok(fallback),
}
}
}