fixing problems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

examples/java/JavaExample.java

@@ -712,9 +712,9 @@ class JavaExample
         System.out.println("QuantifierExample3");
 
         HashMap<String, String> cfg = new HashMap<String, String>();
-        cfg.put("MBQI", "false");
+        cfg.put("smt.mbqi", "false");
-        cfg.put("PROOF_MODE", "2");
+        cfg.put("proof", "true");
-        cfg.put("AUTO_CONFIG", "false");
+        cfg.put("auto_config", "false");
 
         /*
          * If quantified formulas are asserted in a logical context, then the
@@ -761,9 +761,9 @@ class JavaExample
         System.out.println("QuantifierExample4");
 
         HashMap<String, String> cfg = new HashMap<String, String>();
-        cfg.put("MBQI", "false");
+        cfg.put("smt.mbqi", "false");
-        cfg.put("PROOF_MODE", "2");
+        cfg.put("proof", "true");
-        cfg.put("AUTO_CONFIG", "false");
+        cfg.put("auto_config", "false");
 
         /*
          * If quantified formulas are asserted in a logical context, then the
@@ -1081,7 +1081,7 @@ class JavaExample
 
         {
             HashMap<String, String> cfg = new HashMap<String, String>();
-            cfg.put("MODEL", "true");
+            cfg.put("model", "true");
             Context ctx = new Context(cfg);
             Expr a = ctx.ParseSMTLIB2File(filename, null, null, null, null);
 
@@ -2100,7 +2100,7 @@ class JavaExample
         System.out.println("UnsatCoreAndProofExample");
 
         HashMap<String, String> cfg = new HashMap<String, String>();
-        cfg.put("PROOF_MODE", "2");
+        cfg.put("proof", "true");
 
         {
             Context ctx = new Context(cfg);
@@ -2176,8 +2176,8 @@ class JavaExample
 
             {
                 HashMap<String, String> cfg = new HashMap<String, String>();
-                cfg.put("MODEL", "true");
+                cfg.put("model", "true");
-                cfg.put("PROOF_MODE", "2");
+                cfg.put("proof", "true");
                 Context ctx = new Context(cfg);
                 p.BasicTests(ctx);
                 p.CastingTest(ctx);

src/api/api_context.cpp

@@ -80,7 +80,7 @@ namespace api {
     }
 
     context::context(context_params * p, bool user_ref_count):
-        m_params(*p),
+        m_params(p != 0 ? *p : context_params()),
         m_user_ref_count(user_ref_count),
         m_manager(m_params.m_proof ? PGM_FINE : PGM_DISABLED, m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0), 
         m_plugins(m_manager),

src/smt/qi_queue.cpp

@@ -47,10 +47,21 @@ namespace smt {
 
     void qi_queue::setup() {
         TRACE("qi_cost", tout << "qi_cost: " << m_params.m_qi_cost << "\n";);
-        if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function))
+        if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) {
-            throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str());
+            // it is not reasonable to abort here during the creation of smt::context just because an invalid option was provided.
-        if (!m_parser.parse_string(m_params.m_qi_new_gen.c_str(), m_new_gen_function))
+            // throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str());
-            throw default_exception("invalid new-gen function %s", m_params.m_qi_new_gen.c_str());
+            
+            // using warning message instead
+            warning_msg("invalid cost function '%s', switching to default one", m_params.m_qi_cost.c_str());
+            // Trying again with default function
+            VERIFY(m_parser.parse_string("(+ weight generation)", m_cost_function));
+        }
+        if (!m_parser.parse_string(m_params.m_qi_new_gen.c_str(), m_new_gen_function)) {
+            // See comment above
+            // throw default_exception("invalid new-gen function %s", m_params.m_qi_new_gen.c_str());
+            warning_msg("invalid new_gen function '%s', switching to default one", m_params.m_qi_new_gen.c_str());
+            VERIFY(m_parser.parse_string("cost", m_new_gen_function));
+        }
         m_eager_cost_threshold = m_params.m_qi_eager_threshold;
     }
 

src/smt/smt_solver.cpp

@@ -56,9 +56,13 @@ namespace smt {
 
         virtual void init_core(ast_manager & m, symbol const & logic) {
             reset();
+            // We can throw exceptions when creating a smt::kernel object
+            // So, we should create the smt::kernel outside of the criticial section
+            // block. OMP does not allow exceptions to cross critical section boundaries.
+            smt::kernel * new_kernel = alloc(smt::kernel, m, m_params);
             #pragma omp critical (solver)
             {
-                m_context = alloc(smt::kernel, m, m_params);
+                m_context = new_kernel;
                 if (m_callback)
                     m_context->set_progress_callback(m_callback);
             }
@@ -85,51 +89,59 @@ namespace smt {
             }
         }
         
+        // An exception may be thrown when creating a smt::kernel.
+        // So, there is no guarantee that m_context != 0 when
+        // using smt_solver from the SMT 2.0 command line frontend.
+        void check_context() const {
+            if (m_context == 0)
+                throw default_exception("Z3 failed to create solver, check previous error messages");
+        }
+
         virtual void assert_expr(expr * t) {
-            SASSERT(m_context);
+            check_context();
             m_context->assert_expr(t);
         }
 
         virtual void push_core() {
-            SASSERT(m_context);
+            check_context();
             m_context->push();
         }
 
         virtual void pop_core(unsigned n) {
-            SASSERT(m_context);
+            check_context();
             m_context->pop(n);
         }
 
         virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
-            SASSERT(m_context);
+            check_context();
             TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";);
             return m_context->check(num_assumptions, assumptions);
         }
 
         virtual void get_unsat_core(ptr_vector<expr> & r) {
-            SASSERT(m_context);
+            check_context();
             unsigned sz = m_context->get_unsat_core_size();
             for (unsigned i = 0; i < sz; i++)
                 r.push_back(m_context->get_unsat_core_expr(i));
         }
 
         virtual void get_model(model_ref & m) {
-            SASSERT(m_context);
+            check_context();
             m_context->get_model(m);
         }
 
         virtual proof * get_proof() {
-            SASSERT(m_context);
+            check_context();
             return m_context->get_proof();
         }
 
         virtual std::string reason_unknown() const {
-            SASSERT(m_context);
+            check_context();
             return m_context->last_failure_as_string();
         }
 
         virtual void get_labels(svector<symbol> & r) {
-            SASSERT(m_context);
+            check_context();
             buffer<symbol> tmp;
             m_context->get_relevant_labels(0, tmp);
             r.append(tmp.size(), tmp.c_ptr());

src/util/gparams.cpp

@@ -178,6 +178,11 @@ public:
             long val = strtol(value, 0, 10);
             ps.set_uint(param_name, static_cast<unsigned>(val));
         }
+        else if (k == CPK_DOUBLE) {
+            char * aux;
+            double val = strtod(value, &aux);
+            ps.set_double(param_name, val);
+        }
         else if (k == CPK_BOOL) {
             if (strcmp(value, "true") == 0) {
                 ps.set_bool(param_name, true);
@@ -196,7 +201,16 @@ public:
             ps.set_sym(param_name, symbol(value));
         }
         else if (k == CPK_STRING) {
-            ps.set_str(param_name, value);
+            // There is no guarantee that (external) callers will not delete value after invoking gparams::set.
+            // I see two solutions:
+            //    1) Modify params_ref to create a copy of set_str parameters.
+            //       This solution is not nice since we create copies and move the params_ref around.
+            //       We would have to keep copying the strings.
+            //       Moreover, when we use params_ref internally, the value is usually a static value. 
+            //       So, we would be paying this price for nothing.
+            //    2) "Copy" value by transforming it into a symbol. 
+            //       I'm using this solution for now.
+            ps.set_str(param_name, symbol(value).bare_str());
         }
         else {
             if (mod_name == symbol::null)