started solver_factory

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3250 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/cbmc/bmc.h

@@ -93,6 +93,8 @@ class bmct:public messaget
   virtual void do_unwind_module(
     decision_proceduret &decision_procedure);
   void do_conversion(prop_convt &solver);
+  
+  prop_convt *solver_factory();
 
   virtual void show_vcc();
   virtual bool all_claims(

src/cbmc/cbmc_solvers.cpp

@@ -26,6 +26,84 @@ Author: Daniel Kroening, [email protected]
 
 /*******************************************************************\
 
+Function: bmct::solver_factory
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Decide using "default" decision procedure
+
+\*******************************************************************/
+
+prop_convt *bmct::solver_factory()
+{
+  //const std::string &filename=options.get_option("outfile");
+  
+  if(options.get_bool_option("boolector"))
+  {
+  }
+  else if(options.get_bool_option("mathsat"))
+  {
+  }
+  else if(options.get_bool_option("cvc"))
+  {
+  }
+  else if(options.get_bool_option("dimacs"))
+  {
+  }
+  else if(options.get_bool_option("opensmt"))
+  {
+  }
+  else if(options.get_bool_option("refine"))
+  {
+  }
+  else if(options.get_bool_option("aig"))
+  {
+  }
+  else if(options.get_bool_option("smt1"))
+  {
+  }
+  else if(options.get_bool_option("smt2"))
+  {
+  }
+  else if(options.get_bool_option("yices"))
+  {
+  }
+  else if(options.get_bool_option("z3"))
+  {
+  }
+  else
+  {
+    // THE DEFAULT
+
+    #if 0
+    // SAT preprocessor won't work with beautification.
+    if(options.get_bool_option("sat-preprocessor") &&
+       !options.get_bool_option("beautify"))
+    {
+      solver=std::auto_ptr<propt>(new satcheckt);
+    }
+    else
+      solver=std::auto_ptr<propt>(new satcheck_minisat_no_simplifiert);
+
+    solver->set_message_handler(get_message_handler());
+    solver->set_verbosity(get_verbosity());
+      
+    bv_cbmct bv_cbmc(ns, *solver);
+      
+    if(options.get_option("arrays-uf")=="never")
+      bv_cbmc.unbounded_array=bv_cbmct::U_NONE;
+    else if(options.get_option("arrays-uf")=="always")
+      bv_cbmc.unbounded_array=bv_cbmct::U_ALL;
+    #endif
+  }      
+
+  return 0;
+}
+
+/*******************************************************************\
+
 Function: bmct::decide_default
 
   Inputs: