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
}