package acgtk

  1. Overview
  2. Docs
package acgtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Module to rewrite program and derivations.

Log is the log module for Rewriting

type magic_context = {
  1. predicates_from_magic : Magic.extra_pred_type ASPred.PredIdMap.t;
    (*

    A record of the predicates addded by the magic rewriting

    *)
  2. unique_to_original_rules_ids_map : (int * int) DatalogLib.Datalog_AbstractSyntax.RuleIdMap.t;
    (*

    A correspondance beetwen the rule ids of the original program and the preproccess program.

    The key is the rule id of the preprocess program and the value the corresponding id in the original program and the number of idb predicates (used to transform premises)

    *)
  3. magic_to_unique_rule_ids_map : int DatalogLib.Datalog_AbstractSyntax.RuleIdMap.t;
    (*

    A correspondance beetwen the rule ids of the preprocess program and the magic program.

    *)
  4. adorn_to_unadorm_pred_ids_map : ASPred.pred_id ASPred.PredIdMap.t;
    (*

    A correspondace beetween the id of an adorned predicate and the id of the original predicate.

    *)
  5. unique_binding_program : ASProg.program;
}

Record to rewrite proof

module QueryMap : Stdlib.Map.S with type key = ASPred.pred_id * MagicRewriting.Adornment.status list
val rewrite_programs : ?msg:string -> ASProg.program -> (ASProg.program * magic_context) QueryMap.t

rewrite_programs program Build a map of magic programs for every predicate that occur in the program

get_program query query_map Returns the good magic program for the query and updates this program with the seed in it.

val rewrite_derivations : DatalogLib.Datalog.Datalog.Predicate.PremiseSet.t DatalogLib.Datalog.Datalog.Predicate.PredicateMap.t -> magic_context -> DatalogLib.Datalog.Datalog.Predicate.PremiseSet.t DatalogLib.Datalog.Datalog.Predicate.PredicateMap.t

rewrite_derivations derivations magic_context Rewrites derivations from a magic program to the corresponding derivations in the original program.