From 142bf71b35f4835f8ad1c370dceb56bbee34a75e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Oct 2012 22:04:19 -0700 Subject: [PATCH] checkpoint Signed-off-by: Leonardo de Moura --- src/api/api_solver.cpp | 1 + src/cmd_context/solver.cpp | 161 -------------------- src/cmd_context/solver.h | 2 - src/old_params/pattern_inference_params.cpp | 37 +++++ src/portfolio/smt_strategic_solver.cpp | 1 + 5 files changed, 39 insertions(+), 163 deletions(-) create mode 100644 src/old_params/pattern_inference_params.cpp diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 1a4a2ef45..71a24c534 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -29,6 +29,7 @@ Revision History: #include"cancel_eh.h" #include"scoped_timer.h" #include"smt_strategic_solver.h" +#include"default_solver.h" extern "C" { diff --git a/src/cmd_context/solver.cpp b/src/cmd_context/solver.cpp index 12f1b76f3..59118c5ca 100644 --- a/src/cmd_context/solver.cpp +++ b/src/cmd_context/solver.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include"solver.h" -// #include"smt_solver.h" unsigned solver::get_num_assertions() const { NOT_IMPLEMENTED_YET(); @@ -33,163 +32,3 @@ void solver::display(std::ostream & out) const { out << "(solver)"; } -#if 0 -class default_solver : public solver { - front_end_params * m_params; - smt::solver * m_context; -public: - default_solver():m_params(0), m_context(0) {} - - virtual ~default_solver() { - if (m_context != 0) - dealloc(m_context); - } - - virtual void set_front_end_params(front_end_params & p) { - m_params = &p; - } - - virtual void updt_params(params_ref const & p) { - if (m_context == 0) - return; - m_context->updt_params(p); - } - - virtual void collect_param_descrs(param_descrs & r) { - if (m_context == 0) { - ast_manager m; - m.register_decl_plugins(); - front_end_params p; - smt::solver s(m, p); - s.collect_param_descrs(r); - } - else { - m_context->collect_param_descrs(r); - } - } - - virtual void init(ast_manager & m, symbol const & logic) { - SASSERT(m_params); - reset(); - #pragma omp critical (solver) - { - m_context = alloc(smt::solver, m, *m_params); - } - if (logic != symbol::null) - m_context->set_logic(logic); - } - - virtual void collect_statistics(statistics & st) const { - if (m_context == 0) { - return; - } - else { - m_context->collect_statistics(st); - } - } - - virtual void reset() { - if (m_context != 0) { - #pragma omp critical (solver) - { - dealloc(m_context); - m_context = 0; - } - } - } - - virtual void assert_expr(expr * t) { - SASSERT(m_context); - m_context->assert_expr(t); - } - - virtual void push() { - SASSERT(m_context); - m_context->push(); - } - - virtual void pop(unsigned n) { - SASSERT(m_context); - m_context->pop(n); - } - - virtual unsigned get_scope_level() const { - if (m_context) - return m_context->get_scope_level(); - else - return 0; - } - - virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { - SASSERT(m_context); - return m_context->check(num_assumptions, assumptions); - } - - virtual void get_unsat_core(ptr_vector & r) { - SASSERT(m_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); - m_context->get_model(m); - } - - virtual proof * get_proof() { - SASSERT(m_context); - return m_context->get_proof(); - } - - virtual std::string reason_unknown() const { - SASSERT(m_context); - return m_context->last_failure_as_string(); - } - - virtual void get_labels(svector & r) { - SASSERT(m_context); - buffer tmp; - m_context->get_relevant_labels(0, tmp); - r.append(tmp.size(), tmp.c_ptr()); - } - - virtual void set_cancel(bool f) { - #pragma omp critical (solver) - { - if (m_context) - m_context->set_cancel(f); - } - } - - virtual void set_progress_callback(progress_callback * callback) { - SASSERT(m_context); - m_context->set_progress_callback(callback); - } - - virtual unsigned get_num_assertions() const { - if (m_context) - return m_context->size(); - else - return 0; - } - - virtual expr * get_assertion(unsigned idx) const { - SASSERT(m_context); - SASSERT(idx < get_num_assertions()); - return m_context->get_formulas()[idx]; - } - - virtual void display(std::ostream & out) const { - if (m_context) - m_context->display(out); - else - out << "(solver)"; - } - -}; - -solver * mk_default_solver() { - return alloc(default_solver); -} -#endif diff --git a/src/cmd_context/solver.h b/src/cmd_context/solver.h index c7077a0a2..373f878bb 100644 --- a/src/cmd_context/solver.h +++ b/src/cmd_context/solver.h @@ -58,6 +58,4 @@ public: virtual void display(std::ostream & out) const; }; -solver * mk_default_solver(); - #endif diff --git a/src/old_params/pattern_inference_params.cpp b/src/old_params/pattern_inference_params.cpp new file mode 100644 index 000000000..38fc24dca --- /dev/null +++ b/src/old_params/pattern_inference_params.cpp @@ -0,0 +1,37 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + pattern_inference_params.cpp + +Abstract: + + + +Author: + + Leonardo de Moura (leonardo) 2008-03-24. + +Revision History: + +--*/ +#include"pattern_inference_params.h" + +void pattern_inference_params::register_params(ini_params & p) { + p.register_unsigned_param("PI_MAX_MULTI_PATTERNS", m_pi_max_multi_patterns, + "when patterns are not provided, the prover uses a heuristic to infer them. This option sets the threshold on the number of extra multi-patterns that can be created. By default, the prover creates at most one multi-pattern when there is no unary pattern"); + p.register_bool_param("PI_BLOCK_LOOOP_PATTERNS", m_pi_block_loop_patterns, + "block looping patterns during pattern inference"); + p.register_int_param("PI_ARITH", 0, 2, reinterpret_cast(m_pi_arith), + "0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms."); + p.register_bool_param("PI_USE_DATABASE", m_pi_use_database); + p.register_unsigned_param("PI_ARITH_WEIGHT", m_pi_arith_weight, "default weight for quantifiers where the only available pattern has nested arithmetic terms."); + p.register_unsigned_param("PI_NON_NESTED_ARITH_WEIGHT", m_pi_non_nested_arith_weight, "default weight for quantifiers where the only available pattern has non nested arithmetic terms."); + p.register_bool_param("PI_PULL_QUANTIFIERS", m_pi_pull_quantifiers, "pull nested quantifiers, if no pattern was found."); + p.register_int_param("PI_NOPAT_WEIGHT", m_pi_nopat_weight, "set weight of quantifiers without patterns, if negative the weight is not changed."); + p.register_bool_param("PI_AVOID_SKOLEMS", m_pi_avoid_skolems); + p.register_bool_param("PI_WARNINGS", m_pi_warnings, "enable/disable warning messages in the pattern inference module."); +} + + diff --git a/src/portfolio/smt_strategic_solver.cpp b/src/portfolio/smt_strategic_solver.cpp index 7776a95c2..00022368d 100644 --- a/src/portfolio/smt_strategic_solver.cpp +++ b/src/portfolio/smt_strategic_solver.cpp @@ -35,6 +35,7 @@ Notes: #include"ufbv_strategy.h" #include"st2tactic.h" #include"qffpa_tactic.h" +#include"default_solver.h" #define MK_ST2TACTIC_FACTORY(NAME, ST) \ class NAME : public tactic_factory { \