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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

//! Data structures and algorithms for clausal and nonclausal connection proof search.
//!
//! This crate provides a multitude of fast data structures and associated algorithms
//! for connection proof search in first-order logic, such as
//! formulas, literals, terms, substitutions, clauses, matrices, ...
//! This is significantly based on the work
//! "Efficient Low-Level Connection Tableaux" (2015) by Cezary Kaliszyk,
//! in particular the idea of offset terms/clauses.
//!
//! This crate should allow you to build own, customised connection provers
//! without having to do all the foundational work necessary otherwise.
#![no_std]
#![forbid(unsafe_code)]
#![warn(missing_docs)]

extern crate alloc;

pub mod lean;
pub mod nano;

mod app;
mod args;
mod clause;
#[cfg(feature = "colosseum")]
mod colosseum;
mod database;
mod equality;
pub mod fof;
mod literal;
mod litmat;
mod matrix;
pub mod offset;
mod putrewind;
mod rewind;
pub mod role;
mod signed;
mod subst;
mod symbol;
pub mod szs;
mod term;
#[cfg(feature = "tptp")]
pub mod tptp;

pub use app::App;
pub use args::Args;
pub use clause::Clause;
pub use database::Db;
pub use fof::Fof;
pub use literal::Lit;
pub use litmat::LitMat;
pub use matrix::Matrix;
pub use offset::Offset;
pub use putrewind::PutRewind;
pub use rewind::Rewind;
pub use role::Role;
pub use signed::Signed;
pub use subst::Subst;
pub use symbol::Symbol;
pub use term::Term;

use alloc::vec::Vec;
use core::hash::Hash;

/// Return the keys that are mapped to more than one different value.
pub fn nonfunctional<K: Eq + Hash, V: Eq>(kv: &[(K, V)]) -> impl Iterator<Item = &K> {
    let iter = kv.iter().scan(hashbrown::HashMap::new(), |map, (k, v)| {
        Some(map.insert(k, v).and_then(|v_old| (v != v_old).then_some(k)))
    });
    iter.flatten()
}

fn keep_first<T: Eq>(v: impl Iterator<Item = T>) -> Vec<T> {
    let mut result = Vec::new();
    for x in v {
        if result.iter().all(|y| x != *y) {
            result.push(x)
        }
    }
    result
}

/// Remove all elements of `v2` from `v1` and append `v2` to the result.
///
/// ~~~
/// # use cop::union1;
/// let mut v1 = vec![0, 2, 3, 3, 4, 4];
/// let v2 = vec![1, 2, 2, 4, 5];
/// union1(&mut v1, v2);
/// assert_eq!(v1, vec![0, 3, 3, 1, 2, 2, 4, 5])
/// ~~~
pub fn union1<T: Eq>(v1: &mut Vec<T>, mut v2: Vec<T>) {
    v1.retain(|x| !v2.iter().any(|y| x == y));
    v1.append(&mut v2)
}

/// Compute the union of two vectors, removing duplicates from the first one.
///
/// This function first removes duplicates from the first vector,
/// keeping the first occurence of each element.
/// It then removes from the first vector any element present in the second vector.
/// Finally, it reverses the first vector and concatenates it with the second vector.
///
/// This function is so complicated in order to
/// simulate the function `union2` of Otten's leanCoP.
///
/// ~~~
/// assert_eq!(cop::union2(vec![2, 1, 3, 4, 1], vec![2, 2]), vec![4, 3, 1, 2, 2]);
/// ~~~
pub fn union2<T: Eq>(v1: Vec<T>, mut v2: Vec<T>) -> Vec<T> {
    let v1_uniq = keep_first(v1.into_iter()).into_iter();
    let mut result: Vec<T> = v1_uniq.filter(|x| v2.iter().all(|y| x != y)).collect();
    result.reverse();
    result.append(&mut v2);
    result
}