(*
 * Copyright © 2008 The Regents of the University of California. All rights reserved.
 *
 * Permission is hereby granted, without written agreement and without
 * license or royalty fees, to use, copy, modify, and distribute this
 * software and its documentation for any purpose, provided that the
 * above copyright notice and the following two paragraphs appear in
 * all copies of this software.
 *
 * IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY
 * FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES
 * ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN
 * IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY
 * OF SUCH DAMAGE.
 *
 * THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
 * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY
 * AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
 * ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION
 * TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
 *)

open FixMisc.Ops

module Mem : ProverArch.PROVER = TpGen.MakeProver(SmtZ3.SMTZ3)
module Smt : ProverArch.PROVER = TpGen.MakeProver(SmtLIB2.SMTLib2)

let mydebug = false

let create ts env ps cs  
  = let xxx = Constants.get_smt2_file () in
    match !Constants.smt_solver with
      | None   -> 
          Constants.bprintflush mydebug "\nUSING z3 bindings \n"; 
          Mem.mkProver ts env ps cs
      | Some s -> 
          Constants.bprintflush mydebug ("\nUSING SMTLIB bindings -- " ^ xxx ^ " -- with " ^ s ^ "\n"); 
          Smt.mkProver ts env ps cs