litex-lang 0.9.6-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

use crate::prelude::*;

/// Map any binary order literal to an equivalent [`LessFact`] or [`LessEqualFact`] (strict / weak).
/// Used by numeric builtin and shared congruence reasoning so `>` / `>=` / negated forms need not
/// duplicate `<` / `<=` logic.
pub(crate) fn normalize_positive_order_atomic_fact(atomic_fact: &AtomicFact) -> Option<AtomicFact> {
    match atomic_fact {
        AtomicFact::LessFact(f) => Some(AtomicFact::LessFact(f.clone())),
        AtomicFact::LessEqualFact(f) => Some(AtomicFact::LessEqualFact(f.clone())),
        AtomicFact::GreaterFact(f) => Some(AtomicFact::LessFact(LessFact::new(
            f.right.clone(),
            f.left.clone(),
            f.line_file.clone(),
        ))),
        AtomicFact::GreaterEqualFact(f) => Some(AtomicFact::LessEqualFact(LessEqualFact::new(
            f.right.clone(),
            f.left.clone(),
            f.line_file.clone(),
        ))),
        AtomicFact::NotLessFact(f) => Some(AtomicFact::LessEqualFact(LessEqualFact::new(
            f.right.clone(),
            f.left.clone(),
            f.line_file.clone(),
        ))),
        AtomicFact::NotLessEqualFact(f) => Some(AtomicFact::LessFact(LessFact::new(
            f.right.clone(),
            f.left.clone(),
            f.line_file.clone(),
        ))),
        AtomicFact::NotGreaterFact(f) => Some(AtomicFact::LessEqualFact(LessEqualFact::new(
            f.left.clone(),
            f.right.clone(),
            f.line_file.clone(),
        ))),
        AtomicFact::NotGreaterEqualFact(f) => Some(AtomicFact::LessFact(LessFact::new(
            f.left.clone(),
            f.right.clone(),
            f.line_file.clone(),
        ))),
        _ => None,
    }
}