<commit_before>//! Inference infrastructure for indicative conditional expressions and
//! representation querying.
//!
//! ## Safety
//! There is some unsafe code on this module, the unsafe code performs to taks:
//!     * Assure the compiler that data being referenced will have the proper
//!       lifetimes to satisfy the compiler.
//!     * Cheat the compiler on ```Send + Sync``` impl in certain types.
//!
//! Both of those are safe because a Representation owns, uniquely, all its
//! knowledge by the duration of it's own lifetime (data is never dropped, while
//! the representation is alive), thereby is safe to point to the data being
//! referenced from the representation or the query (for the duration of the query).

use std::collections::{HashMap, HashSet, VecDeque};
use std::hash::{Hash, Hasher};
use std::iter::FromIterator;
use std::mem;
use std::rc::Rc;
use std::sync::{Arc, RwLock};

use rayon;
use rayon::prelude::*;

use super::repr::{Answer, Representation};
use super::VarAssignment;
use crate::agent::lang::{
    Assert, ClassDecl, FreeClsMemb, FreeClsOwner, FuncDecl, Grounded, GroundedFunc, GroundedMemb,
    LogSentence, ParseTree, Predicate, ProofResContext, SentID, Terminal, Time, Var, VarKind,
};

type ObjName<'a> = &'a str;
type QueryPred = String;
/// Whether there is a result or not, if it's true or false, and from what point in time
pub type GroundedResult = Option<(bool, Option<Time>)>;
type GroundedResults<'a> = HashMap<ObjName<'a>, GroundedResult>;
type QueryResMemb<'a> = HashMap<ObjName<'a>, Vec<Arc<GroundedMemb>>>;
type QueryResRels<'a> = HashMap<ObjName<'a>, Vec<Arc<GroundedFunc>>>;

/// A succesful query will return an `InfResult` which contains all the answer data.
/// The data can be manipulated and filtered throught various methods returning
/// whatever is requested by the consumer.
#[derive(Debug)]
pub(super) struct InfResults<'b> {
    grounded_queries: RwLock<HashMap<QueryPred, GroundedResults<'b>>>,
    membership: RwLock<HashMap<&'b Var, QueryResMemb<'b>>>,
    relationships: RwLock<HashMap<&'b Var, QueryResRels<'b>>>,
    query: Arc<QueryProcessed<'b>>,
}

impl<'b> InfResults<'b> {
    fn new(query: Arc<QueryProcessed<'b>>) -> InfResults<'b> {
        InfResults {
            grounded_queries: RwLock::new(HashMap::new()),
            membership: RwLock::new(HashMap::new()),
            relationships: RwLock::new(HashMap::new()),
            query,
        }
    }

    fn add_membership(&self, var: &'b Var, name: &'b str, membership: Arc<GroundedMemb>) {
        let mut lock = self.membership.write().unwrap();
        lock.entry(var)
            .or_insert_with(HashMap::new)
            .entry(name)
            .or_insert_with(Vec::new)
            .push(membership);
    }

    fn add_relationships(&self, var: &'b Var, rel: &[Arc<GroundedFunc>]) {
        let mut lock = self.relationships.write().unwrap();
        for func in rel {
            for obj in func.get_args_names() {
                let obj = unsafe { std::mem::transmute::<&str, &'b str>(obj) };
                lock.entry(var)
                    .or_insert_with(HashMap::new)
                    .entry(obj)
                    .or_insert_with(Vec::new)
                    .push(func.clone());
            }
        }
    }

    fn add_grounded(&self, obj: &str, pred: &str, res: Option<(bool, Option<Time>)>) {
        let obj = unsafe { std::mem::transmute::<&str, &'b str>(obj) };
        let mut lock = self.grounded_queries.write().unwrap();
        lock.entry(pred.to_string())
            .or_insert_with(HashMap::new)
            .insert(obj, res);
    }

    pub fn get_results_single(&self) -> Option<bool> {
        let results = self.grounded_queries.read().unwrap();
        if results.len() == 0 {
            return None;
        }
        for r0 in results.values() {
            for r1 in r0.values() {
                if let Some((false, _)) = *r1 {
                    return Some(false);
                } else if r1.is_none() {
                    return None;
                }
            }
        }
        Some(true)
    }

    pub fn get_results_multiple(self) -> HashMap<QueryPred, HashMap<String, GroundedResult>> {
        // WARNING: ObjName<'a> may (truly) outlive the content, own the &str first
        let orig: &mut HashMap<QueryPred, GroundedResults<'b>> =
            &mut *self.grounded_queries.write().unwrap();
        let mut res = HashMap::new();
        for (qpred, r) in orig.drain() {
            let r = HashMap::from_iter(r.into_iter().map(|(k, v)| (k.to_string(), v)));
            res.insert(qpred, r);
        }
        res
    }

    pub fn get_memberships(&self) -> HashMap<ObjName<'b>, Vec<&'b GroundedMemb>> {
        let lock = self.membership.read().unwrap();
        let mut res: HashMap<ObjName<'b>, Vec<&GroundedMemb>> = HashMap::new();
        for preds in lock.values() {
            for members in preds.values() {
                for gr in members {
                    let gr = unsafe { &*(&**gr as *const GroundedMemb) as &'b GroundedMemb };
                    if res.contains_key(gr.get_name()) {
                        let prev = res.get_mut(gr.get_name()).unwrap();
                        prev.push(gr);
                    } else {
                        let mut new = vec![];
                        new.push(gr);
                        res.insert(gr.get_name(), new);
                    }
                }
            }
        }
        res
    }

    pub fn get_relationships(&self) -> HashMap<ObjName<'b>, Vec<&'b GroundedFunc>> {
        let lock = self.relationships.read().unwrap();
        let mut res: HashMap<ObjName<'b>, HashSet<*const GroundedFunc>> = HashMap::new();
        for relations in lock.values() {
            for relation_ls in relations.values() {
                for grfunc in relation_ls {
                    for name in grfunc.get_args_names() {
                        unsafe {
                            let name = mem::transmute::<&str, &'b str>(name);
                            if res.contains_key(name) {
                                let prev = res.get_mut(name).unwrap();
                                prev.insert(&**grfunc as *const GroundedFunc);
                            } else {
                                let mut new = HashSet::new();
                                new.insert(&**grfunc as *const GroundedFunc);
                                res.insert(name, new);
                            }
                        }
                    }
                }
            }
        }
        HashMap::from_iter(res.into_iter().map(|(k, l)| {
            (
                k,
                l.into_iter()
                    .map(|v| unsafe { &*v as &'b GroundedFunc })
                    .collect::<Vec<_>>(),
            )
        }))
    }
}

pub(super) struct Inference<'a> {
    query: Arc<QueryProcessed<'a>>,
    kb: &'a Representation,
    depth: usize,
    ignore_current: bool,
    nodes: RwLock<HashMap<&'a str, Vec<ProofNode<'a>>>>,
    queue: RwLock<HashMap<usize, HashSet<PArgVal>>>, // K: *const ProofNode<'a>
    results: InfResults<'a>,
    tpool: rayon::ThreadPool,
}

impl<'a> Inference<'a> {
    pub fn try_new(
        agent: &'a Representation,
        query_input: QueryInput,
        depth: usize,
        ignore_current: bool,
        num_threads: usize,
    ) -> Result<Inference<'a>, ()> {
        let query = Arc::new(QueryProcessed::new().get_query(query_input)?);
        Ok(Inference {
            query: query.clone(),
            kb: agent,
            depth,
            ignore_current,
            nodes: RwLock::new(HashMap::new()),
            queue: RwLock::new(HashMap::new()),
            results: InfResults::new(query),
            tpool: rayon::ThreadPoolBuilder::new()
                .num_threads(num_threads)
                .build()
                .unwrap(),
        })
    }

    pub fn get_results(self) -> Answer<'a> {
        // TODO: filter results based on query composition
        Answer::new(self.results)
    }

    /// Inference function from first-order logic sentences.
    ///
    /// Gets a query from an 'ask' call, encapsulates the query subtitutions,
    /// processes it (including caching of partial results or tracking
    /// var substitution) and returns the answer to the query. If new
    /// knowledge is produced then it's passed to an other procedure for
    /// addition to the KB.
    pub fn infer_facts(&self) {
        self.tpool.install(|| self.query_cls_gr());
        self.tpool.install(|| self.query_func_gr());
        self.tpool.install(|| self.query_cls_free());
        self.tpool.install(|| self.query_func_free());
        self.tpool.install(|| self.query_cls_memb());
        self.tpool.install(|| self.query_func_memb());
        // AWAIT RESULTS
    }

    fn queue_query(&self, query: &str, actv_query: &ActiveQuery) {
        let mut pass = InfTrial::new(self, actv_query);
        pass.get_rules(vec![query]);
        // run the query, if there is no result and there is an update,
        // then loop again, else stop
        loop {
            pass.unify(query, VecDeque::new(), HashSet::new());
            if !pass.updated.contains(&true) || !pass.feedback {
                break;
            }
            pass.updated = vec![];
        }
        let obj = actv_query.get_obj();
        let pred = actv_query.get_pred();
        if pass.valid.is_none() {
            self.results.add_grounded(obj, pred, None);
        } else {
            let valid = pass.valid.as_ref().unwrap();
            let node: &ProofNode = unsafe { &*(valid.node as *const ProofNode) };
            let context = IExprResult::new(valid.args.clone(), node);
            node.proof
                .solve(self.kb, Some(&valid.args.as_proof_input()), context);
        }
    }

    #[inline]
    /// Find if a grounded class membership is true, false or unknown.
    /// ie. (person[$John,u=1])
    fn query_cls_gr(&self) {
        self.query
            .cls_queries_grounded
            .par_iter()
            .for_each(|(obj, preds)| {
                for pred in preds {
                    let query = pred.get_parent();
                    let result = if !self.ignore_current {
                        // FIXME: only checks for the current value, not for intervals
                        self.kb.class_membership_query(pred)
                    } else {
                        None
                    };
                    if result.is_some() {
                        self.results
                            .add_grounded(obj, query, Some((result.unwrap(), None)));
                    } else {
                        self.results.add_grounded(obj, query, None);
                        // if no result was found from the kb directly
                        // make an inference from a grounded fact
                        let actv_query = ActiveQuery::new_with_class(pred.clone());
                        self.queue_query(query, &actv_query);
                    }
                }
            });
    }

    #[inline]
    /// Find if a grounded function is true, false or unknown.
    /// ie. (fn::friend[$Lucy,u=0;$John])
    fn query_func_gr(&self) {
        self.query
            .func_queries_grounded
            .par_iter()
            .for_each(|pred| {
                let query: &str = pred.get_name();
                let mut result = None;
                for (i, arg) in pred.get_args().iter().enumerate() {
                    let obj = arg.get_name();
                    if !self.ignore_current {
                        result = self.kb.has_relationship(pred, obj);
                    }
                    if result.is_some() {
                        self.results
                            .add_grounded(obj, query, Some((result.unwrap(), None)));
                    } else {
                        self.results.add_grounded(obj, query, None);
                        let actv_query = ActiveQuery::new_with_func(i, pred.clone());
                        self.queue_query(query, &actv_query);
                    }
                }
            });
    }

    #[inline]
    /// Find all members (subclasses or entities) of a given class.
    /// ie. ((let x) (professor[x,u=1]))
    fn query_cls_free(&self) {
        self.query
            .cls_queries_free
            .par_iter()
            .for_each(|(var, classes)| {
                for cls in classes {
                    let cls_name = cls.get_parent();
                    let lock = self.kb.classes.read().unwrap();
                    if let Some(cls_curr) = lock.get(cls_name) {
                        let members: Vec<Arc<GroundedMemb>> = cls_curr.get_members(cls);
                        for m in members {
                            let t = unsafe { &*(&*m as *const GroundedMemb) as &GroundedMemb };
                            self.results.add_membership(var, t.get_name(), m.clone());
                        }
                    }
                }
            });
    }

    #[inline]
    /// Find all relationships of a given function type.
    /// ie. ((let x) (fn::produce[milk,u>0;x]))
    fn query_func_free(&self) {
        self.query
            .func_queries_free
            .par_iter()
            .for_each(|(var, funcs)| {
                for func in funcs {
                    let func_name = func.get_name();
                    let lock = &self.kb.classes.read().unwrap();
                    if let Some(cls_curr) = lock.get(func_name) {
                        let members: Vec<Arc<GroundedFunc>> = cls_curr.get_funcs(func);
                        self.results.add_relationships(var, &members);
                    }
                }
            });
    }

    #[inline]
    /// Find class membership of a grounded entity or class.
    /// ie. ((let x) (x[$Lucy,u>0.5]))
    fn query_cls_memb(&self) {
        self.query
            .cls_memb_query
            .par_iter()
            .for_each(|(var, objs)| {
                for obj in objs {
                    let member_of = self.kb.get_class_membership(obj);
                    for m in member_of {
                        self.results.add_membership(var, obj.get_name(), m.clone());
                    }
                }
            });
    }

    #[inline]
    /// Find relationships of a grounded entity or class.
    /// ie. ((let x, y) (fn::x[$Vicky,u=0;y]))
    fn query_func_memb(&self) {
        self.query
            .func_memb_query
            .par_iter()
            .for_each(|(var, funcs)| {
                for func in funcs {
                    let relationships = self.kb.get_relationships(func);
                    for funcs in relationships.values() {
                        self.results.add_relationships(var, funcs);
                    }
                }
            });
    }
}

#[derive(Clone)]
enum ActiveQuery {
    // (obj_name, pred_name, fn/cls decl)
    Class(Arc<GroundedMemb>),
    Func(usize, Arc<GroundedFunc>),
}

impl ActiveQuery {
    fn new_with_func(obj_arg: usize, decl: Arc<GroundedFunc>) -> ActiveQuery {
        ActiveQuery::Func(obj_arg, decl)
    }

    fn new_with_class(decl: Arc<GroundedMemb>) -> ActiveQuery {
        ActiveQuery::Class(decl)
    }

    #[inline]
    fn get_obj(&self) -> &str {
        match *self {
            ActiveQuery::Class(ref decl) => decl.get_name(),
            ActiveQuery::Func(pos, ref decl) => decl.get_arg_name(pos),
        }
    }

    #[inline]
    fn get_pred(&self) -> &str {
        match *self {
            ActiveQuery::Class(ref decl) => decl.get_parent(),
            ActiveQuery::Func(_, ref decl) => decl.get_name(),
        }
    }

    #[inline]
    fn is_func(&self) -> bool {
        match *self {
            ActiveQuery::Class(..) => false,
            ActiveQuery::Func(..) => true,
        }
    }

    #[inline]
    fn get_func(&self) -> &GroundedFunc {
        match *self {
            ActiveQuery::Func(_, ref gf) => &*gf,
            ActiveQuery::Class(_) => panic!(),
        }
    }

    #[inline]
    fn get_cls(&self) -> &GroundedMemb {
        match *self {
            ActiveQuery::Class(ref gt) => &*gt,
            ActiveQuery::Func(_, _) => panic!(),
        }
    }
}

#[derive(Debug)]
struct ProofArgs {
    ptr: usize, // *mut Vec<(&'a Var, Arc<VarAssignment<'a>>)
    hash_val: usize,
}

type PArgVal = usize;

impl ProofArgs {
    fn new<'a>(input: Vec<(&Var, Arc<VarAssignment<'a>>)>) -> ProofArgs {
        let hash_val = ProofArgs::arg_hash_val(&input[..]);
        let ptr = Box::into_raw(Box::new(input));
        ProofArgs {
            ptr: ptr as usize,
            hash_val,
        }
    }

    fn arg_hash_val(input: &[(&Var, Arc<VarAssignment>)]) -> usize {
        use std::collections::hash_map::DefaultHasher;
        let mut v = vec![];
        for &(var, ref assigned) in input {
            let mut var = format!("{:?}", var as *const Var).into_bytes();
            v.append(&mut var);
            let mut s = Vec::from_iter(assigned.name.as_bytes().iter().cloned());
            v.append(&mut s);
        }
        let mut s = DefaultHasher::new();
        v.hash(&mut s);
        s.finish() as usize
    }

    fn as_proof_input(&self) -> HashMap<&Var, &VarAssignment> {
        let data = unsafe {
            let data = self.ptr as *mut Vec<(&Var, Arc<VarAssignment>)>;
            &*data as &Vec<(&Var, Arc<VarAssignment>)>
        };
        let mut n_args = HashMap::with_capacity(data.len());
        for &(k, ref v) in data {
            n_args.insert(k, &**v);
        }
        n_args
    }
}

impl std::clone::Clone for ProofArgs {
    fn clone(&self) -> ProofArgs {
        unsafe {
            let data = self.ptr as *mut Vec<(&Var, Arc<VarAssignment>)>;
            let data = &*data as &Vec<(&Var, Arc<VarAssignment>)>;
            ProofArgs::new(data.clone())
        }
    }
}

impl std::ops::Drop for ProofArgs {
    fn drop(&mut self) {
        unsafe {
            Box::from_raw(self.ptr as *mut Vec<(&Var, Arc<VarAssignment>)>);
        }
    }
}

struct ValidAnswer {
    node: usize, // *const ProofNode<'a>,
    args: ProofArgs,
    newest_grfact: Time,
}

#[derive(Debug)]
pub(super) struct IExprResult {
    result: Option<bool>,
    newest_grfact: Time,
    antecedents: Vec<Grounded>,
    grounded_func: Vec<(GroundedFunc, Time)>,
    grounded_cls: Vec<(GroundedMemb, Time)>,
    sent_id: SentID,
    args: ProofArgs,
    node: usize, // *const ProofNode<'a>
    sub_mode: bool,
}

impl IExprResult {
    fn new(args: ProofArgs, node: &ProofNode) -> IExprResult {
        IExprResult {
            result: None,
            args,
            node: node as *const ProofNode as usize,
            newest_grfact: chrono::MIN_DATE.and_hms(0, 0, 0),
            sent_id: node.proof.get_id(),
            antecedents: vec![],
            grounded_func: vec![],
            grounded_cls: vec![],
            sub_mode: false,
        }
    }
}

impl ProofResContext for IExprResult {
    fn substituting(&mut self) {
        self.sub_mode = true;
    }

    fn is_substituting(&self) -> bool {
        self.sub_mode
    }

    fn set_inconsistent(&mut self, _val: bool) {}

    fn is_inconsistent(&self) -> bool {
        false
    }

    fn set_result(&mut self, res: Option<bool>) {
        self.result = res;
    }

    fn get_id(&self) -> SentID {
        self.sent_id
    }

    fn push_grounded_func(&mut self, grounded: GroundedFunc, time: Time) {
        self.grounded_func.push((grounded, time));
    }

    fn push_grounded_cls(&mut self, grounded: GroundedMemb, time: Time) {
        self.grounded_cls.push((grounded, time));
    }

    fn newest_grfact(&self) -> Time {
        self.newest_grfact
    }

    fn set_newest_grfact(&mut self, time: Time) {
        self.newest_grfact = time;
    }

    fn get_antecedents(&self) -> &[Grounded] {
        &self.antecedents
    }

    fn push_antecedents(&mut self, grounded: Grounded) {
        self.antecedents.push(grounded);
    }

    fn push_false_fn_assert(&mut self, _func: Arc<GroundedFunc>) {}

    fn push_false_cls_assert(&mut self, _cls: Arc<GroundedMemb>) {}

    fn compare_relation(&self, _func: &GroundedFunc) -> bool {
        false
    }

    fn compare_cls(&self, _cls: &GroundedMemb) -> bool {
        false
    }

    fn has_relationship(&self, _func: &GroundedFunc) -> Option<bool> {
        None
    }

    fn has_cls_memb(&self, _cls: &GroundedMemb) -> Option<bool> {
        None
    }
}

struct InfTrial<'a> {
    kb: &'a Representation,
    actv: ActiveQuery,
    updated: Vec<bool>,
    feedback: bool,
    valid: Option<ValidAnswer>,
    nodes: usize, // &'a RwLock<HashMap<&'a str, Vec<ProofNode<'a>>>>,
    queue: &'a RwLock<HashMap<usize, HashSet<PArgVal>>>, // K: *const ProofNode<'a>
    results: usize, // &'a InfResults<'a>,
    depth: usize,
    depth_cnt: RwLock<usize>,
}

impl<'a> InfTrial<'a> {
    fn new(inf: &'a Inference, actv_query: &ActiveQuery) -> InfTrial<'a> {
        let nodes = &inf.nodes as *const RwLock<_> as usize;
        let results = &inf.results as *const InfResults as usize;
        InfTrial {
            kb: inf.kb,
            actv: actv_query.clone(),
            updated: vec![],
            feedback: true,
            valid: None,
            nodes,
            queue: &inf.queue,
            results,
            depth: inf.depth,
            depth_cnt: RwLock::new(0_usize),
        }
    }

    fn unify(
        &mut self,
        mut parent: &'a str,
        mut chk: VecDeque<&'a str>,
        mut done: HashSet<&'a str>,
    ) {
        fn unification_trial(inf: &mut InfTrial, node: &ProofNode, args: &ProofArgs) {
            let node_raw = node as *const ProofNode as usize;
            let args_done = {
                if let Some(queued) = inf.queue.read().unwrap().get(&node_raw) {
                    queued.contains(&args.hash_val)
                } else {
                    false
                }
            };
            if !args_done {
                let n_args = &args.as_proof_input();
                let context = IExprResult::new(args.clone(), node);
                let solved_proof = node.proof.solve(inf.kb, Some(n_args), context);
                if solved_proof.result.is_some() {
                    {
                        inf.updated.push(true);
                        let mut lock1 = inf.queue.write().unwrap();
                        lock1
                            .entry(node_raw)
                            .or_insert_with(HashSet::new)
                            .insert(args.hash_val);
                    }
                    inf.add_result(solved_proof);
                }
            }
        };

        let nodes = unsafe { &*(self.nodes as *const RwLock<HashMap<&str, Vec<ProofNode>>>) };
        loop {
            self.valid = None;
            // for each node in the subtitution tree unifify variables
            // and try every possible substitution until (if) a solution is found
            // the proofs are tried in order of addition to the KB
            if let Some(nodes) = nodes.read().unwrap().get(parent) {
                // the node for each rule is stored in an efficient sorted list
                // by rule creation datetime, from newest to oldest
                // as the newest rules take precedence
                for node in nodes.iter() {
                    // recursively try unifying all possible argument with the
                    // operating logic sentence:
                    // get all the entities/classes from the kb that meet the proof requeriments
                    for var_req in node.proof.get_lhs_predicates().into_sent_req() {
                        let assignments = meet_sent_req(self.kb, &var_req);
                        if assignments.is_none() {
                            for e in node.antecedents.clone() {
                                if !done.contains(&e) && !chk.contains(&e) {
                                    chk.push_back(e);
                                }
                            }
                            continue;
                        }
                        // lazily iterate over all possible combinations of the substitutions
                        let mapped = ArgsProduct::product(assignments.unwrap());
                        if let Some(mapped) = mapped {
                            for args in mapped {
                                if let Some(ref valid) = self.valid {
                                    if valid.node == &*node as *const ProofNode as usize {
                                        break;
                                    }
                                }
                                let args: ProofArgs = ProofArgs::new(args);
                                unification_trial(self, node, &args);
                            }
                        }
                        if self.feedback {
                            for e in node.antecedents.clone() {
                                if !done.contains(&e) && !chk.contains(&e) {
                                    chk.push_back(e);
                                }
                            }
                        }
                    }
                }
            }
            if !self.feedback {
                return;
            }
            if !chk.is_empty() && (*self.depth_cnt.read().unwrap() < self.depth) {
                done.insert(parent);
                self.get_rules(Vec::from_iter(chk.iter().cloned()));
                let p1 = chk.pop_front().unwrap();
                parent = p1;
            } else {
                let mut c = self.depth_cnt.write().unwrap();
                *c += 1;
                return;
            }
        }
    }

    fn add_as_last_valid(
        &mut self,
        context: &IExprResult,
        r_dict: &mut GroundedResults<'a>,
        time: Time,
        value: bool,
    ) {
        let query_obj = unsafe {
            let obj = self.actv.get_obj();
            std::mem::transmute::<&str, &'a str>(obj)
        };
        if let Some(ref prev_answ) = self.valid {
            if prev_answ.newest_grfact >= context.newest_grfact {
                return;
            }
        }
        r_dict.insert(query_obj, Some((value, Some(time))));
        let answ = ValidAnswer {
            node: context.node,
            args: context.args.clone(),
            newest_grfact: context.newest_grfact,
        };
        self.valid = Some(answ);
    }

    fn add_result(&mut self, mut context: IExprResult) {
        // add category/function to the object dictionary
        // and to results dict if is the result for the query
        let query_obj = self.actv.get_obj().to_owned();
        let query_pred = self.actv.get_pred().to_owned();
        let is_func = self.actv.is_func();
        let results = unsafe { &*(self.results as *const InfResults) };

        let gr_cls: Vec<_> = context.grounded_cls.drain(..).collect();
        for (gt, time) in gr_cls {
            if !is_func {
                let query_cls = self.actv.get_cls();
                if query_cls.comparable(&gt) {
                    let val = query_cls == &gt;
                    let mut d = results.grounded_queries.write().unwrap();
                    let gr_results_dict = {
                        if d.contains_key(&query_pred) {
                            d.get_mut(&query_pred).unwrap()
                        } else {
                            let new = HashMap::new();
                            d.insert(query_pred.to_string(), new);
                            d.get_mut(&query_pred).unwrap()
                        }
                    };
                    if gr_results_dict.contains_key(query_obj.as_str()) {
                        let cond_ok;
                        if let Some(&Some((_, Some(cdate)))) =
                            gr_results_dict.get(query_obj.as_str())
                        {
                            if time >= cdate {
                                cond_ok = true;
                            } else {
                                cond_ok = false;
                            }
                        } else {
                            cond_ok = true;
                        }
                        if cond_ok {
                            self.add_as_last_valid(&context, gr_results_dict, time, val);
                        }
                    } else {
                        self.add_as_last_valid(&context, gr_results_dict, time, val);
                    }
                    self.feedback = false;
                }
            }
        }

        let gr_func: Vec<_> = context.grounded_func.drain(..).collect();
        for (gf, time) in gr_func {
            if is_func {
                let query_func = self.actv.get_func();
                if query_func.comparable(&gf) {
                    let val = query_func == &gf;
                    let mut d = results.grounded_queries.write().unwrap();
                    let gr_results_dict = {
                        if d.contains_key(query_pred.as_str()) {
                            d.get_mut(query_pred.as_str()).unwrap()
                        } else {
                            let new = HashMap::new();
                            d.insert(query_pred.clone(), new);
                            d.get_mut(query_pred.as_str()).unwrap()
                        }
                    };
                    if gr_results_dict.contains_key(query_obj.as_str()) {
                        let cond_ok;
                        if let Some(&Some((_, Some(cdate)))) =
                            gr_results_dict.get(query_obj.as_str())
                        {
                            if time >= cdate {
                                cond_ok = true;
                            } else {
                                cond_ok = false;
                            }
                        } else {
                            cond_ok = true;
                        }<commit_msg>Refactor unification trial to method<commit_after>//! Inference infrastructure for indicative conditional expressions and
//! representation querying.
//!
//! ## Safety
//! There is some unsafe code on this module, the unsafe code performs to taks:
//!     * Assure the compiler that data being referenced will have the proper
//!       lifetimes to satisfy the compiler.
//!     * Cheat the compiler on ```Send + Sync``` impl in certain types.
//!
//! Both of those are safe because a Representation owns, uniquely, all its
//! knowledge by the duration of it's own lifetime (data is never dropped, while
//! the representation is alive), thereby is safe to point to the data being
//! referenced from the representation or the query (for the duration of the query).

use std::collections::{HashMap, HashSet, VecDeque};
use std::hash::{Hash, Hasher};
use std::iter::FromIterator;
use std::mem;
use std::rc::Rc;
use std::sync::{Arc, RwLock};

use rayon;
use rayon::prelude::*;

use super::repr::{Answer, Representation};
use super::VarAssignment;
use crate::agent::lang::{
    Assert, ClassDecl, FreeClsMemb, FreeClsOwner, FuncDecl, Grounded, GroundedFunc, GroundedMemb,
    LogSentence, ParseTree, Predicate, ProofResContext, SentID, Terminal, Time, Var, VarKind,
};

type ObjName<'a> = &'a str;
type QueryPred = String;
/// Whether there is a result or not, if it's true or false, and from what point in time
pub type GroundedResult = Option<(bool, Option<Time>)>;
type GroundedResults<'a> = HashMap<ObjName<'a>, GroundedResult>;
type QueryResMemb<'a> = HashMap<ObjName<'a>, Vec<Arc<GroundedMemb>>>;
type QueryResRels<'a> = HashMap<ObjName<'a>, Vec<Arc<GroundedFunc>>>;

/// A succesful query will return an `InfResult` which contains all the answer data.
/// The data can be manipulated and filtered throught various methods returning
/// whatever is requested by the consumer.
#[derive(Debug)]
pub(super) struct InfResults<'b> {
    grounded_queries: RwLock<HashMap<QueryPred, GroundedResults<'b>>>,
    membership: RwLock<HashMap<&'b Var, QueryResMemb<'b>>>,
    relationships: RwLock<HashMap<&'b Var, QueryResRels<'b>>>,
    query: Arc<QueryProcessed<'b>>,
}

impl<'b> InfResults<'b> {
    fn new(query: Arc<QueryProcessed<'b>>) -> InfResults<'b> {
        InfResults {
            grounded_queries: RwLock::new(HashMap::new()),
            membership: RwLock::new(HashMap::new()),
            relationships: RwLock::new(HashMap::new()),
            query,
        }
    }

    fn add_membership(&self, var: &'b Var, name: &'b str, membership: Arc<GroundedMemb>) {
        let mut lock = self.membership.write().unwrap();
        lock.entry(var)
            .or_insert_with(HashMap::new)
            .entry(name)
            .or_insert_with(Vec::new)
            .push(membership);
    }

    fn add_relationships(&self, var: &'b Var, rel: &[Arc<GroundedFunc>]) {
        let mut lock = self.relationships.write().unwrap();
        for func in rel {
            for obj in func.get_args_names() {
                let obj = unsafe { std::mem::transmute::<&str, &'b str>(obj) };
                lock.entry(var)
                    .or_insert_with(HashMap::new)
                    .entry(obj)
                    .or_insert_with(Vec::new)
                    .push(func.clone());
            }
        }
    }

    fn add_grounded(&self, obj: &str, pred: &str, res: Option<(bool, Option<Time>)>) {
        let obj = unsafe { std::mem::transmute::<&str, &'b str>(obj) };
        let mut lock = self.grounded_queries.write().unwrap();
        lock.entry(pred.to_string())
            .or_insert_with(HashMap::new)
            .insert(obj, res);
    }

    pub fn get_results_single(&self) -> Option<bool> {
        let results = self.grounded_queries.read().unwrap();
        if results.len() == 0 {
            return None;
        }
        for r0 in results.values() {
            for r1 in r0.values() {
                if let Some((false, _)) = *r1 {
                    return Some(false);
                } else if r1.is_none() {
                    return None;
                }
            }
        }
        Some(true)
    }

    pub fn get_results_multiple(self) -> HashMap<QueryPred, HashMap<String, GroundedResult>> {
        // WARNING: ObjName<'a> may (truly) outlive the content, own the &str first
        let orig: &mut HashMap<QueryPred, GroundedResults<'b>> =
            &mut *self.grounded_queries.write().unwrap();
        let mut res = HashMap::new();
        for (qpred, r) in orig.drain() {
            let r = HashMap::from_iter(r.into_iter().map(|(k, v)| (k.to_string(), v)));
            res.insert(qpred, r);
        }
        res
    }

    pub fn get_memberships(&self) -> HashMap<ObjName<'b>, Vec<&'b GroundedMemb>> {
        let lock = self.membership.read().unwrap();
        let mut res: HashMap<ObjName<'b>, Vec<&GroundedMemb>> = HashMap::new();
        for preds in lock.values() {
            for members in preds.values() {
                for gr in members {
                    let gr = unsafe { &*(&**gr as *const GroundedMemb) as &'b GroundedMemb };
                    if res.contains_key(gr.get_name()) {
                        let prev = res.get_mut(gr.get_name()).unwrap();
                        prev.push(gr);
                    } else {
                        let mut new = vec![];
                        new.push(gr);
                        res.insert(gr.get_name(), new);
                    }
                }
            }
        }
        res
    }

    pub fn get_relationships(&self) -> HashMap<ObjName<'b>, Vec<&'b GroundedFunc>> {
        let lock = self.relationships.read().unwrap();
        let mut res: HashMap<ObjName<'b>, HashSet<*const GroundedFunc>> = HashMap::new();
        for relations in lock.values() {
            for relation_ls in relations.values() {
                for grfunc in relation_ls {
                    for name in grfunc.get_args_names() {
                        unsafe {
                            let name = mem::transmute::<&str, &'b str>(name);
                            if res.contains_key(name) {
                                let prev = res.get_mut(name).unwrap();
                                prev.insert(&**grfunc as *const GroundedFunc);
                            } else {
                                let mut new = HashSet::new();
                                new.insert(&**grfunc as *const GroundedFunc);
                                res.insert(name, new);
                            }
                        }
                    }
                }
            }
        }
        HashMap::from_iter(res.into_iter().map(|(k, l)| {
            (
                k,
                l.into_iter()
                    .map(|v| unsafe { &*v as &'b GroundedFunc })
                    .collect::<Vec<_>>(),
            )
        }))
    }
}

pub(super) struct Inference<'a> {
    query: Arc<QueryProcessed<'a>>,
    kb: &'a Representation,
    depth: usize,
    ignore_current: bool,
    nodes: RwLock<HashMap<&'a str, Vec<ProofNode<'a>>>>,
    queue: RwLock<HashMap<usize, HashSet<PArgVal>>>, // K: *const ProofNode<'a>
    results: InfResults<'a>,
    tpool: rayon::ThreadPool,
}

impl<'a> Inference<'a> {
    pub fn try_new(
        agent: &'a Representation,
        query_input: QueryInput,
        depth: usize,
        ignore_current: bool,
        num_threads: usize,
    ) -> Result<Inference<'a>, ()> {
        let query = Arc::new(QueryProcessed::new().get_query(query_input)?);
        Ok(Inference {
            query: query.clone(),
            kb: agent,
            depth,
            ignore_current,
            nodes: RwLock::new(HashMap::new()),
            queue: RwLock::new(HashMap::new()),
            results: InfResults::new(query),
            tpool: rayon::ThreadPoolBuilder::new()
                .num_threads(num_threads)
                .build()
                .unwrap(),
        })
    }

    pub fn get_results(self) -> Answer<'a> {
        // TODO: filter results based on query composition
        Answer::new(self.results)
    }

    /// Inference function from first-order logic sentences.
    ///
    /// Gets a query from an 'ask' call, encapsulates the query subtitutions,
    /// processes it (including caching of partial results or tracking
    /// var substitution) and returns the answer to the query. If new
    /// knowledge is produced then it's passed to an other procedure for
    /// addition to the KB.
    pub fn infer_facts(&self) {
        self.tpool.install(|| self.query_cls_gr());
        self.tpool.install(|| self.query_func_gr());
        self.tpool.install(|| self.query_cls_free());
        self.tpool.install(|| self.query_func_free());
        self.tpool.install(|| self.query_cls_memb());
        self.tpool.install(|| self.query_func_memb());
    }

    /// Find if a grounded class membership is true, false or unknown.
    /// ie. (person[$John,u=1])
    fn query_cls_gr(&self) {
        self.query
            .cls_queries_grounded
            .par_iter()
            .for_each(|(obj, preds)| {
                for pred in preds {
                    let query = pred.get_parent();
                    let result = if !self.ignore_current {
                        // FIXME: only checks for the current value, not for intervals
                        self.kb.class_membership_query(pred)
                    } else {
                        None
                    };
                    if result.is_some() {
                        self.results
                            .add_grounded(obj, query, Some((result.unwrap(), None)));
                    } else {
                        self.results.add_grounded(obj, query, None);
                        // if no result was found from the kb directly
                        // make an inference from a grounded fact
                        let actv_query = ActiveQuery::new_with_class(pred.clone());
                        self.queue_query(query, &actv_query);
                    }
                }
            });
    }

    /// Find if a grounded function is true, false or unknown.
    /// ie. (fn::friend[$Lucy,u=0;$John])
    fn query_func_gr(&self) {
        self.query
            .func_queries_grounded
            .par_iter()
            .for_each(|pred| {
                let query: &str = pred.get_name();
                let mut result = None;
                for (i, arg) in pred.get_args().iter().enumerate() {
                    let obj = arg.get_name();
                    if !self.ignore_current {
                        result = self.kb.has_relationship(pred, obj);
                    }
                    if result.is_some() {
                        self.results
                            .add_grounded(obj, query, Some((result.unwrap(), None)));
                    } else {
                        self.results.add_grounded(obj, query, None);
                        let actv_query = ActiveQuery::new_with_func(i, pred.clone());
                        self.queue_query(query, &actv_query);
                    }
                }
            });
    }

    fn queue_query(&self, query: &str, actv_query: &ActiveQuery) {
        let mut pass = InfTrial::new(self, actv_query);
        pass.get_rules(vec![query]);
        // run the query, if there is no result and there is an update,
        // then loop again, else stop
        loop {
            pass.unify(query, VecDeque::new(), HashSet::new());
            if !pass.updated.contains(&true) || !pass.feedback {
                break;
            }
            pass.updated = vec![];
        }
        let obj = actv_query.get_obj();
        let pred = actv_query.get_pred();
        if pass.valid.is_none() {
            self.results.add_grounded(obj, pred, None);
        } else {
            let valid = pass.valid.as_ref().unwrap();
            let node: &ProofNode = unsafe { &*(valid.node as *const ProofNode) };
            let context = IExprResult::new(valid.args.clone(), node);
            node.proof
                .solve(self.kb, Some(&valid.args.as_proof_input()), context);
        }
    }

    /// Find all members (subclasses or entities) of a given class.
    /// ie. ((let x) (professor[x,u=1]))
    fn query_cls_free(&self) {
        self.query
            .cls_queries_free
            .par_iter()
            .for_each(|(var, classes)| {
                for cls in classes {
                    let cls_name = cls.get_parent();
                    let lock = self.kb.classes.read().unwrap();
                    if let Some(cls_curr) = lock.get(cls_name) {
                        let members: Vec<Arc<GroundedMemb>> = cls_curr.get_members(cls);
                        for m in members {
                            let t = unsafe { &*(&*m as *const GroundedMemb) as &GroundedMemb };
                            self.results.add_membership(var, t.get_name(), m.clone());
                        }
                    }
                }
            });
    }

    /// Find all relationships of a given function type.
    /// ie. ((let x) (fn::produce[milk,u>0;x]))
    fn query_func_free(&self) {
        self.query
            .func_queries_free
            .par_iter()
            .for_each(|(var, funcs)| {
                for func in funcs {
                    let func_name = func.get_name();
                    let lock = &self.kb.classes.read().unwrap();
                    if let Some(cls_curr) = lock.get(func_name) {
                        let members: Vec<Arc<GroundedFunc>> = cls_curr.get_funcs(func);
                        self.results.add_relationships(var, &members);
                    }
                }
            });
    }

    /// Find class membership of a grounded entity or class.
    /// ie. ((let x) (x[$Lucy,u>0.5]))
    fn query_cls_memb(&self) {
        self.query
            .cls_memb_query
            .par_iter()
            .for_each(|(var, objs)| {
                for obj in objs {
                    let member_of = self.kb.get_class_membership(obj);
                    for m in member_of {
                        self.results.add_membership(var, obj.get_name(), m.clone());
                    }
                }
            });
    }

    /// Find relationships of a grounded entity or class.
    /// ie. ((let x, y) (fn::x[$Vicky,u=0;y]))
    fn query_func_memb(&self) {
        self.query
            .func_memb_query
            .par_iter()
            .for_each(|(var, funcs)| {
                for func in funcs {
                    let relationships = self.kb.get_relationships(func);
                    for funcs in relationships.values() {
                        self.results.add_relationships(var, funcs);
                    }
                }
            });
    }
}

#[derive(Clone)]
enum ActiveQuery {
    // (obj_name, pred_name, fn/cls decl)
    Class(Arc<GroundedMemb>),
    Func(usize, Arc<GroundedFunc>),
}

impl ActiveQuery {
    fn new_with_func(obj_arg: usize, decl: Arc<GroundedFunc>) -> ActiveQuery {
        ActiveQuery::Func(obj_arg, decl)
    }

    fn new_with_class(decl: Arc<GroundedMemb>) -> ActiveQuery {
        ActiveQuery::Class(decl)
    }

    #[inline]
    fn get_obj(&self) -> &str {
        match *self {
            ActiveQuery::Class(ref decl) => decl.get_name(),
            ActiveQuery::Func(pos, ref decl) => decl.get_arg_name(pos),
        }
    }

    #[inline]
    fn get_pred(&self) -> &str {
        match *self {
            ActiveQuery::Class(ref decl) => decl.get_parent(),
            ActiveQuery::Func(_, ref decl) => decl.get_name(),
        }
    }

    #[inline]
    fn is_func(&self) -> bool {
        match *self {
            ActiveQuery::Class(..) => false,
            ActiveQuery::Func(..) => true,
        }
    }

    #[inline]
    fn get_func(&self) -> &GroundedFunc {
        match *self {
            ActiveQuery::Func(_, ref gf) => &*gf,
            ActiveQuery::Class(_) => panic!(),
        }
    }

    #[inline]
    fn get_cls(&self) -> &GroundedMemb {
        match *self {
            ActiveQuery::Class(ref gt) => &*gt,
            ActiveQuery::Func(_, _) => panic!(),
        }
    }
}

#[derive(Debug)]
struct ProofArgs {
    ptr: usize, // *mut Vec<(&'a Var, Arc<VarAssignment<'a>>)
    hash_val: usize,
}

type PArgVal = usize;

impl ProofArgs {
    fn new<'a>(input: Vec<(&Var, Arc<VarAssignment<'a>>)>) -> ProofArgs {
        let hash_val = ProofArgs::arg_hash_val(&input[..]);
        let ptr = Box::into_raw(Box::new(input));
        ProofArgs {
            ptr: ptr as usize,
            hash_val,
        }
    }

    fn arg_hash_val(input: &[(&Var, Arc<VarAssignment>)]) -> usize {
        use std::collections::hash_map::DefaultHasher;
        let mut v = vec![];
        for &(var, ref assigned) in input {
            let mut var = format!("{:?}", var as *const Var).into_bytes();
            v.append(&mut var);
            let mut s = Vec::from_iter(assigned.name.as_bytes().iter().cloned());
            v.append(&mut s);
        }
        let mut s = DefaultHasher::new();
        v.hash(&mut s);
        s.finish() as usize
    }

    fn as_proof_input(&self) -> HashMap<&Var, &VarAssignment> {
        let data = unsafe {
            let data = self.ptr as *mut Vec<(&Var, Arc<VarAssignment>)>;
            &*data as &Vec<(&Var, Arc<VarAssignment>)>
        };
        let mut n_args = HashMap::with_capacity(data.len());
        for &(k, ref v) in data {
            n_args.insert(k, &**v);
        }
        n_args
    }
}

impl std::clone::Clone for ProofArgs {
    fn clone(&self) -> ProofArgs {
        unsafe {
            let data = self.ptr as *mut Vec<(&Var, Arc<VarAssignment>)>;
            let data = &*data as &Vec<(&Var, Arc<VarAssignment>)>;
            ProofArgs::new(data.clone())
        }
    }
}

impl std::ops::Drop for ProofArgs {
    fn drop(&mut self) {
        unsafe {
            Box::from_raw(self.ptr as *mut Vec<(&Var, Arc<VarAssignment>)>);
        }
    }
}

struct ValidAnswer {
    node: usize, // *const ProofNode<'a>,
    args: ProofArgs,
    newest_grfact: Time,
}

#[derive(Debug)]
pub(super) struct IExprResult {
    result: Option<bool>,
    newest_grfact: Time,
    antecedents: Vec<Grounded>,
    grounded_func: Vec<(GroundedFunc, Time)>,
    grounded_cls: Vec<(GroundedMemb, Time)>,
    sent_id: SentID,
    args: ProofArgs,
    node: usize, // *const ProofNode<'a>
    sub_mode: bool,
}

impl IExprResult {
    fn new(args: ProofArgs, node: &ProofNode) -> IExprResult {
        IExprResult {
            result: None,
            args,
            node: node as *const ProofNode as usize,
            newest_grfact: chrono::MIN_DATE.and_hms(0, 0, 0),
            sent_id: node.proof.get_id(),
            antecedents: vec![],
            grounded_func: vec![],
            grounded_cls: vec![],
            sub_mode: false,
        }
    }
}

impl ProofResContext for IExprResult {
    fn substituting(&mut self) {
        self.sub_mode = true;
    }

    fn is_substituting(&self) -> bool {
        self.sub_mode
    }

    fn set_inconsistent(&mut self, _val: bool) {}

    fn is_inconsistent(&self) -> bool {
        false
    }

    fn set_result(&mut self, res: Option<bool>) {
        self.result = res;
    }

    fn get_id(&self) -> SentID {
        self.sent_id
    }

    fn push_grounded_func(&mut self, grounded: GroundedFunc, time: Time) {
        self.grounded_func.push((grounded, time));
    }

    fn push_grounded_cls(&mut self, grounded: GroundedMemb, time: Time) {
        self.grounded_cls.push((grounded, time));
    }

    fn newest_grfact(&self) -> Time {
        self.newest_grfact
    }

    fn set_newest_grfact(&mut self, time: Time) {
        self.newest_grfact = time;
    }

    fn get_antecedents(&self) -> &[Grounded] {
        &self.antecedents
    }

    fn push_antecedents(&mut self, grounded: Grounded) {
        self.antecedents.push(grounded);
    }

    fn push_false_fn_assert(&mut self, _func: Arc<GroundedFunc>) {}

    fn push_false_cls_assert(&mut self, _cls: Arc<GroundedMemb>) {}

    fn compare_relation(&self, _func: &GroundedFunc) -> bool {
        false
    }

    fn compare_cls(&self, _cls: &GroundedMemb) -> bool {
        false
    }

    fn has_relationship(&self, _func: &GroundedFunc) -> Option<bool> {
        None
    }

    fn has_cls_memb(&self, _cls: &GroundedMemb) -> Option<bool> {
        None
    }
}

struct InfTrial<'a> {
    kb: &'a Representation,
    actv: ActiveQuery,
    updated: Vec<bool>,
    feedback: bool,
    valid: Option<ValidAnswer>,
    nodes: usize, // &'a RwLock<HashMap<&'a str, Vec<ProofNode<'a>>>>,
    queue: &'a RwLock<HashMap<usize, HashSet<PArgVal>>>, // K: *const ProofNode<'a>
    results: usize, // &'a InfResults<'a>,
    depth: usize,
    depth_cnt: RwLock<usize>,
}

impl<'a> InfTrial<'a> {
    fn new(inf: &'a Inference, actv_query: &ActiveQuery) -> InfTrial<'a> {
        let nodes = &inf.nodes as *const RwLock<_> as usize;
        let results = &inf.results as *const InfResults as usize;
        InfTrial {
            kb: inf.kb,
            actv: actv_query.clone(),
            updated: vec![],
            feedback: true,
            valid: None,
            nodes,
            queue: &inf.queue,
            results,
            depth: inf.depth,
            depth_cnt: RwLock::new(0_usize),
        }
    }

    fn unify(
        &mut self,
        mut parent: &'a str,
        mut chk: VecDeque<&'a str>,
        mut done: HashSet<&'a str>,
    ) {
        let nodes = unsafe { &*(self.nodes as *const RwLock<HashMap<&str, Vec<ProofNode>>>) };
        loop {
            self.valid = None;
            // for each node in the subtitution tree unifify variables
            // and try every possible substitution until (if) a solution is found
            // the proofs are tried in order of addition to the KB
            if let Some(nodes) = nodes.read().unwrap().get(parent) {
                // the node for each rule is stored in an efficient sorted list
                // by rule creation datetime, from newest to oldest
                // as the newest rules take precedence
                for node in nodes.iter() {
                    // recursively try unifying all possible argument with the
                    // operating logic sentence:
                    // get all the entities/classes from the kb that meet the proof requeriments
                    for var_req in node.proof.get_lhs_predicates().into_sent_req() {
                        let assignments = meet_sent_req(self.kb, &var_req);
                        if assignments.is_none() {
                            for e in node.antecedents.clone() {
                                if !done.contains(&e) && !chk.contains(&e) {
                                    chk.push_back(e);
                                }
                            }
                            continue;
                        }
                        // lazily iterate over all possible combinations of the substitutions
                        let mapped = ArgsProduct::product(assignments.unwrap());
                        if let Some(mapped) = mapped {
                            for args in mapped {
                                if let Some(ref valid) = self.valid {
                                    if valid.node == &*node as *const ProofNode as usize {
                                        break;
                                    }
                                }
                                let args: ProofArgs = ProofArgs::new(args);
                                self.unification_trial(node, &args);
                            }
                        }
                        if self.feedback {
                            for e in node.antecedents.clone() {
                                if !done.contains(&e) && !chk.contains(&e) {
                                    chk.push_back(e);
                                }
                            }
                        }
                    }
                }
            }
            if !self.feedback {
                return;
            }
            if !chk.is_empty() && (*self.depth_cnt.read().unwrap() < self.depth) {
                done.insert(parent);
                self.get_rules(Vec::from_iter(chk.iter().cloned()));
                let p1 = chk.pop_front().unwrap();
                parent = p1;
            } else {
                let mut c = self.depth_cnt.write().unwrap();
                *c += 1;
                return;
            }
        }
    }

    fn unification_trial(&mut self, node: &ProofNode, args: &ProofArgs) {
        let node_raw = node as *const ProofNode as usize;
        let args_done = {
            if let Some(queued) = self.queue.read().unwrap().get(&node_raw) {
                queued.contains(&args.hash_val)
            } else {
                false
            }
        };
        if !args_done {
            let n_args = &args.as_proof_input();
            let context = IExprResult::new(args.clone(), node);
            let solved_proof = node.proof.solve(self.kb, Some(n_args), context);
            if solved_proof.result.is_some() {
                {
                    self.updated.push(true);
                    let mut lock1 = self.queue.write().unwrap();
                    lock1
                        .entry(node_raw)
                        .or_insert_with(HashSet::new)
                        .insert(args.hash_val);
                }
                self.add_result(solved_proof);
            }
        }
    }

    fn add_as_last_valid(
        &mut self,
        context: &IExprResult,
        r_dict: &mut GroundedResults<'a>,
        time: Time,
        value: bool,
    ) {
        let query_obj = unsafe {
            let obj = self.actv.get_obj();
            std::mem::transmute::<&str, &'a str>(obj)
        };
        if let Some(ref prev_answ) = self.valid {
            if prev_answ.newest_grfact >= context.newest_grfact {
                return;
            }
        }
        r_dict.insert(query_obj, Some((value, Some(time))));
        let answ = ValidAnswer {
            node: context.node,
            args: context.args.clone(),
            newest_grfact: context.newest_grfact,
        };
        self.valid = Some(answ);
    }

    fn add_result(&mut self, mut context: IExprResult) {
        // add category/function to the object dictionary
        // and to results dict if is the result for the query
        let is_func = self.actv.is_func();
        let results = unsafe { &*(self.results as *const InfResults) };

        let gr_cls: Vec<_> = context.grounded_cls.drain(..).collect();
        for (gt, time) in gr_cls {
            if !is_func {
                let query_cls = self.actv.get_cls();
                if query_cls.comparable(&gt) {
                    let val = query_cls == &gt;
                    let mut d = results.grounded_queries.write().unwrap();
                    let gr_results_dict = {
                        if d.contains_key(self.actv.get_pred()) {
                            d.get_mut(self.actv.get_pred()).unwrap()
                        } else {
                            let new = HashMap::new();
                            d.insert(self.actv.get_pred().to_string(), new);
                            d.get_mut(self.actv.get_pred()).unwrap()
                        }
                    };
                    if gr_results_dict.contains_key(self.actv.get_obj()) {
                        let cond_ok;
                        if let Some(&Some((_, Some(cdate)))) =
                            gr_results_dict.get(self.actv.get_obj())
                        {
                            if time >= cdate {
                                cond_ok = true;
                            } else {
                                cond_ok = false;
                            }
                        } else {
                            cond_ok = true;
                        }
                        if cond_ok {
                            self.add_as_last_valid(&context, gr_results_dict, time, val);
                        }
                    } else {
                        self.add_as_last_valid(&context, gr_results_dict, time, val);
                    }
                    self.feedback = false;
                }
            }
        }

        let gr_func: Vec<_> = context.grounded_func.drain(..).collect();
        for (gf, time) in gr_func {
            if is_func {
                let query_func = self.actv.get_func();
                if query_func.comparable(&gf) {
                    let val = query_func == &gf;
                    let mut d = results.grounded_queries.write().unwrap();
                    let gr_results_dict = {
                        if d.contains_key(self.actv.get_pred()) {
                            d.get_mut(self.actv.get_pred()).unwrap()
                        } else {
                            let new = HashMap::new();
                            d.insert(self.actv.get_pred().to_string(), new);
                            d.get_mut(self.actv.get_pred()).unwrap()
                        }
                    };
                    if gr_results_dict.contains_key(self.actv.get_obj()) {
                        let cond_ok;
                        if let Some(&Some((_, Some(cdate)))) =
                            gr_results_dict.get(self.actv.get_obj())
                        {
                            if time >= cdate {
                                cond_ok = true;
                            } else {
                                cond_ok = false;
                            }
                        } else {
                            cond_ok = true;
                        }
{'fraction_non_alphanumeric': 0.122955197970221, 'fraction_numerical': 0.0007344595045736796, 'mean_word_length': 1.4770114942528736, 'pattern_counts': {'":': 0, '<': 287, '<?xml version=': 0, '>': 371, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 34, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2996114', 'n_tokens_mistral': 17532, 'n_tokens_neox': 17071, 'n_words': 3940}