MagicRewriting.RewritingSourceModule to rewrite program and derivations.
Log is the log module for Rewriting
type magic_context = {predicates_from_magic : Magic.extra_pred_type ASPred.PredIdMap.t;A record of the predicates addded by the magic rewriting
*)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)
*)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.
*)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.
*)unique_binding_program : ASProg.program;}Record to rewrite proof
val rewrite_programs :
?msg:string ->
ASProg.program ->
(ASProg.program * magic_context) QueryMap.trewrite_programs program Build a map of magic programs for every predicate that occur in the program
val get_program :
ASPred.predicate ->
(ASProg.program * magic_context) QueryMap.t ->
ASProg.program * magic_contextget_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.trewrite_derivations derivations magic_context Rewrites derivations from a magic program to the corresponding derivations in the original program.