module Types

end

module Impl

  use Firstorder_semantics.Sem
  use Firstorder_term_spec.Spec
  use Firstorder_formula_spec.Spec
  use Firstorder_formula_impl.Types
  use Firstorder_formula_impl.Logic
  use Firstorder_formula_impl.Impl
  use Firstorder_formula_list_spec.Spec
  use Firstorder_formula_list_impl.Types
  use Firstorder_formula_list_impl.Logic
  use Firstorder_formula_list_impl.Impl
  use Firstorder_tableau_spec.Spec
  use Firstorder_tableau_impl.Types
  use Firstorder_tableau_impl.Logic
  use Firstorder_tableau_impl.Impl
  use FormulaTransformations.Types
  use FormulaTransformations.Logic
  use FormulaTransformations.Impl
  use Unification.Types
  use Unification.Logic
  use Functions.Func
  use option.Option
  use OptionFuncs.Funcs
  use bool.Bool
  use int.Int
  use Prover.Types
  use Prover.Logic
  use Prover.Impl
  use list.List
  use import set.Set as S
  use import BacktrackArray.Impl as BA

  val ghost sdata_inv_hack (u:unit) : sdata -> bool
    ensures { result = sdata_inv }

  let main (base:nlimpl_fo_formula_list) (gnum:int) (ghost st:'st): int
    requires { nlimpl_fo_formula_list_ok base }
    diverges
    ensures { forall m:model int 'st,rho:int -> 'st.
      not(formula_list_conj_semantic base.model_fo_formula_list_field m rho) }
    raises { Sat -> forall m:model int 'st,rho:int -> 'st.
      formula_list_conj_semantic base.model_fo_formula_list_field m rho }
  =
    let root = construct_tableau NLC_Root in
    try let phip = preprocessing base gnum st in
      let phip0 = (phip:preprocessing_return 'st).preprocessed in
      let phip0m = phip0.model_fo_formula_list_field in
      assert { root.model_tableau_field  = Root } ;
      let gnum = phip.final_goals_number in
      let gnum = if gnum <= 0 then (-1) else gnum in
      let rec aux (n:int) (ghost st:'st) : (int, prover_return)
        diverges
        returns { (_,{ contradictory_assignment = s }) ->
        forall m:model int 'st,rho:int -> 'st.
          let rhos = semantic_subst s m rho in
          not(formula_list_conj_semantic phip0.model_fo_formula_list_field m rhos) }
      =
        (* Do work to define them outside the loop, but harder
           to prove while not more performant. *)
        let unifb = BA.create (sdata_inv_hack ()) in
        let unif = {
          unifier_base_model = subst_id_fo_term ;
          unifier = subst_id_fo_term } in
        assert { extensionalEqual (smodel (BA.current_timestamp unifb))
          (subst_id_fo_term) &&
          (smodel (BA.current_timestamp unifb)) = subst_id_fo_term } ;
        assert { forall x:int. unassigned (BA.current_timestamp unifb) x } ;
        try (n,extend_branch phip0 root unifb unif 0 n gnum st)
        with Failure -> aux (n+1) st
        end
      in
      let n,r = aux 0 st in
      let s = r.contradictory_assignment in
      let basem = base.model_fo_formula_list_field in
      let tr = phip.model_transf in
      assert { forall m:model int 'st,rho:int -> 'st.
        let m' = { interp_fun = (tr m).interp_fun ;
          interp_pred = (tr m).interp_pred } in
        let rhos = semantic_subst s m' rho in
        m' = (tr m) &&
        not(formula_list_conj_semantic phip0m m' rhos) &&
        (forall x:int. is_fo_term_free_var_in_fo_formula_list x phip0m ->
          rho x = rhos x) &&
        not(formula_list_conj_semantic phip0m m' rho) &&
        not(formula_list_conj_semantic basem m rho) };
      n
    with Unsat -> 0
    end

end