diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index d06f72217..4d9b6dc1f 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -712,9 +712,9 @@ class JavaExample System.out.println("QuantifierExample3"); HashMap cfg = new HashMap(); - cfg.put("MBQI", "false"); - cfg.put("PROOF_MODE", "2"); - cfg.put("AUTO_CONFIG", "false"); + cfg.put("smt.mbqi", "false"); + cfg.put("proof", "true"); + 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 cfg = new HashMap(); - cfg.put("MBQI", "false"); - cfg.put("PROOF_MODE", "2"); - cfg.put("AUTO_CONFIG", "false"); + cfg.put("smt.mbqi", "false"); + cfg.put("proof", "true"); + cfg.put("auto_config", "false"); /* * If quantified formulas are asserted in a logical context, then the @@ -1081,7 +1081,7 @@ class JavaExample { HashMap cfg = new HashMap(); - 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 cfg = new HashMap(); - cfg.put("PROOF_MODE", "2"); + cfg.put("proof", "true"); { Context ctx = new Context(cfg); @@ -2176,8 +2176,8 @@ class JavaExample { HashMap cfg = new HashMap(); - cfg.put("MODEL", "true"); - cfg.put("PROOF_MODE", "2"); + cfg.put("model", "true"); + cfg.put("proof", "true"); Context ctx = new Context(cfg); p.BasicTests(ctx); p.CastingTest(ctx); diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index f197e8ad8..69b7ea999 100644 --- a/src/api/api_context.cpp +++ b/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), diff --git a/src/parsers/util/simple_parser.cpp b/src/parsers/util/simple_parser.cpp index 65f75e870..045a45b24 100644 --- a/src/parsers/util/simple_parser.cpp +++ b/src/parsers/util/simple_parser.cpp @@ -112,7 +112,7 @@ expr * simple_parser::parse_expr(scanner & s) { } bool simple_parser::parse(std::istream & in, expr_ref & result) { - scanner s(in, std::cerr, false); + scanner s(in, std::cerr, false); try { result = parse_expr(s); if (!result) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 9394dae34..35dd19087 100644 --- a/src/smt/qi_queue.cpp +++ b/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)) - throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str()); - if (!m_parser.parse_string(m_params.m_qi_new_gen.c_str(), m_new_gen_function)) - throw default_exception("invalid new-gen function %s", m_params.m_qi_new_gen.c_str()); + if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) { + // it is not reasonable to abort here during the creation of smt::context just because an invalid option was provided. + // throw default_exception("invalid cost function %s", m_params.m_qi_cost.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; } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 2aa4ee28f..e8c1c6698 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -56,9 +56,13 @@ namespace smt { virtual void init_core(ast_manager & m, symbol const & logic) { reset(); -#pragma omp critical (solver) + // 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); } @@ -77,59 +81,67 @@ namespace smt { virtual void reset_core() { if (m_context != 0) { -#pragma omp critical (solver) + #pragma omp critical (solver) { dealloc(m_context); m_context = 0; } } } + + // 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 & 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 & r) { - SASSERT(m_context); + check_context(); buffer tmp; m_context->get_relevant_labels(0, tmp); r.append(tmp.size(), tmp.c_ptr()); diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 4aecd0c05..183678c59 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -178,6 +178,11 @@ public: long val = strtol(value, 0, 10); ps.set_uint(param_name, static_cast(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)