Module Extract

module Extract: sig .. end
Extract an active path from a formula given a model
Author(s): Christoph Sticksel

val extract : (UfSymbol.t * (Var.t list * Term.t)) list ->
Model.t -> Term.t -> Term.t list * Term.t list
Extract an active path from a formula and return a conjunction that is true in the model given.

Assumption: the formula is satisfiable under the given partial assignment. Then, return an active path g in the formula f, that is, a formula g that must be satisfied if the formula f is satisfied.