checkpoint

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

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" {
 

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<expr> & 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<symbol> & r) {
-        SASSERT(m_context);
-        buffer<symbol> 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

src/cmd_context/solver.h

@@ -58,6 +58,4 @@ public:
     virtual void display(std::ostream & out) const;
 };
 
-solver * mk_default_solver();
-
 #endif

src/old_params/pattern_inference_params.cpp

@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    pattern_inference_params.cpp
+
+Abstract:
+
+    <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<int&>(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.");
+}
+
+

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 {                                                                    \