Module Extract
Extract an active path from a formula given a model
- author
- Christoph Sticksel
val extract : (UfSymbol.t * (Var.t list * Term.t)) list -> Model.t -> Term.t -> Term.t list * Term.t listExtract 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
gin the formulaf, that is, a formulagthat must be satisfied if the formulafis satisfied.