shuffle dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/params/arith_rewriter_params.pyg

@@ -0,0 +1,16 @@
+def_module_params(module_name='rewriter',
+                  class_name='arith_rewriter_params',
+                  export=True,
+                  params=(("algebraic_number_evaluator", BOOL, True, "simplify/evaluate expressions containing (algebraic) irrational numbers."),
+                          ("mul_to_power", BOOL, False, "collpase (* t ... t) into (^ t k), it is ignored if expand_power is true."),
+                          ("expand_power", BOOL, False, "expand (^ t k) into (* t ... t) if  1 < k <= max_degree."),
+                          ("expand_tan", BOOL, False, "replace (tan x) with (/ (sin x) (cos x))."),
+                          ("max_degree", UINT, 64, "max degree of algebraic numbers (and power operators) processed by simplifier."),
+                          ("sort_sums", BOOL, False, "sort the arguments of + application."),
+                          ("gcd_rounding", BOOL, False, "use gcd rounding on integer arithmetic atoms."),
+                          ("arith_lhs", BOOL, False, "all monomials are moved to the left-hand-side, and the right-hand-side is just a constant."),
+                          ("arith_ineq_lhs", BOOL, False, "rewrite inequalities so that right-hand-side is a constant."),
+                          ("elim_to_real", BOOL, False, "eliminate to_real from arithmetic predicates that contain only integers."),
+                          ("push_to_real", BOOL, True, "distribute to_real over * and +."),
+                          ("eq2ineq", BOOL, False, "expand equalities into two inequalities"),
+                          ("elim_rem", BOOL, False, "replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).")))

src/params/bit_blaster_params.h

@@ -0,0 +1,41 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    bit_blaster_params.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-10-02.
+
+Revision History:
+
+--*/
+#pragma once
+
+struct bit_blaster_params {
+    bool  m_bb_ext_gates;
+    bool  m_bb_quantifiers;
+    bit_blaster_params() :
+        m_bb_ext_gates(false),
+        m_bb_quantifiers(false) {
+    }
+#if 0
+    void register_params(ini_params & p) {
+        p.register_bool_param("bb_ext_gates", m_bb_ext_gates, "use extended gates during bit-blasting");
+        p.register_bool_param("bb_quantifiers", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers");
+    }
+#endif
+
+    void display(std::ostream & out) const {
+        out << "m_bb_ext_gates=" << m_bb_ext_gates << std::endl;
+        out << "m_bb_quantifiers=" << m_bb_quantifiers << std::endl;
+    }
+};
+
+

src/params/bv_rewriter_params.pyg

@@ -0,0 +1,16 @@
+def_module_params(module_name='rewriter',
+                  class_name='bv_rewriter_params',
+                  export=True,
+                  params=(("split_concat_eq", BOOL, False, "split equalities of the form (= (concat t1 t2) t3)"),
+                          ("bit2bool", BOOL, True, "try to convert bit-vector terms of size 1 into Boolean terms"),
+                          ("blast_eq_value", BOOL, False, "blast (some) Bit-vector equalities into bits"),
+                          ("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"),
+                          ("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
+                          ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
+                          ("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)"),
+                          ("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators"),
+                          ("bv_extract_prop", BOOL, False, "attempt to partially propagate extraction inwards"),
+                          ("bv_not_simpl", BOOL, False, "apply simplifications for bvnot"),
+                          ("bv_ite2id", BOOL, False, "rewrite ite that can be simplified to identity"),
+                          ("bv_le_extra", BOOL, False, "additional bu_(u/s)le simplifications")
+                          ))

src/params/context_params.cpp

@@ -0,0 +1,205 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    context_params.cpp
+
+Abstract:
+
+    Goodies for managing context parameters in the cmd_context and
+    api_context
+
+Author:
+
+    Leonardo (leonardo) 2012-12-01
+
+Notes:
+
+--*/
+#include "util/gparams.h"
+#include "util/params.h"
+#include "ast/ast.h"
+#include "params/context_params.h"
+
+context_params::context_params() {
+    updt_params();
+}
+
+void context_params::set_bool(bool & opt, char const * param, char const * value) {
+    if (strcmp(value, "true") == 0) {
+        opt = true;
+    }
+    else if (strcmp(value, "false") == 0) {
+        opt = false;
+    }
+    else {
+        std::stringstream strm;
+        strm << "invalid value '" << value << "' for Boolean parameter '" << param << "'";
+        throw default_exception(strm.str());
+    }
+}
+
+void context_params::set_uint(unsigned & opt, char const * param, char const * value) {
+    bool is_uint = true;
+    size_t sz = strlen(value);
+    for (unsigned i = 0; i < sz; i++) {
+        if (!(value[i] >= '0' && value[i] <= '9'))
+            is_uint = false;
+    }
+
+    if (is_uint) {
+        long val = strtol(value, nullptr, 10);
+        opt = static_cast<unsigned>(val);
+    }
+    else {
+        std::stringstream strm;
+        strm << "invalid value '" << value << "' for unsigned int parameter '" << param << "'";
+        throw default_exception(strm.str());
+    }
+}
+
+void context_params::set(char const * param, char const * value) {
+    std::string p = param;
+    unsigned n = static_cast<unsigned>(p.size());
+    for (unsigned i = 0; i < n; i++) {
+        if (p[i] >= 'A' && p[i] <= 'Z')
+            p[i] = p[i] - 'A' + 'a';
+        else if (p[i] == '-')
+            p[i] = '_';
+    }
+    if (p == "timeout") {
+        set_uint(m_timeout, param, value);
+    }
+    else if (p == "rlimit") {
+        set_uint(m_rlimit, param, value);
+    }
+    else if (p == "type_check" || p == "well_sorted_check") {
+        set_bool(m_well_sorted_check, param, value);
+    }
+    else if (p == "auto_config") {
+        set_bool(m_auto_config, param, value);
+    }
+    else if (p == "proof") {
+        set_bool(m_proof, param, value);
+    }
+    else if (p == "model") {
+        set_bool(m_model, param, value);
+    }
+    else if (p == "model_validate") {
+        set_bool(m_model_validate, param, value);
+    }
+    else if (p == "dump_models") {
+        set_bool(m_dump_models, param, value);
+    }
+    else if (p == "stats") {
+        set_bool(m_statistics, param, value);
+    }
+    else if (p == "trace") {
+        set_bool(m_trace, param, value);
+    }
+    else if (p == "trace_file_name") {
+        m_trace_file_name = value;
+    }
+    else if (p == "dot_proof_file") {
+        m_dot_proof_file = value;  
+    }
+    else if (p == "unsat_core") {
+        if (!m_unsat_core) 
+            set_bool(m_unsat_core, param, value);
+    }
+    else if (p == "debug_ref_count") {
+        set_bool(m_debug_ref_count, param, value);
+    }
+    else if (p == "smtlib2_compliant") {
+        set_bool(m_smtlib2_compliant, param, value);
+    }
+    else {
+        param_descrs d;
+        collect_param_descrs(d);
+        std::stringstream strm;
+        strm << "unknown parameter '" << p << "'\n";
+        strm << "Legal parameters are:\n";
+        d.display(strm, 2, false, false);
+        throw default_exception(strm.str());
+    }
+}
+
+void context_params::updt_params() {
+    updt_params(gparams::get_ref());
+}
+
+void context_params::updt_params(params_ref const & p) {
+    m_timeout           = p.get_uint("timeout", m_timeout);
+    m_rlimit            = p.get_uint("rlimit", m_rlimit);
+    m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", m_well_sorted_check));
+    m_auto_config       = p.get_bool("auto_config", m_auto_config);
+    m_proof             = p.get_bool("proof", m_proof);
+    m_model             = p.get_bool("model", m_model);
+    m_model_validate    = p.get_bool("model_validate", m_model_validate);
+    m_dump_models       = p.get_bool("dump_models", m_dump_models);
+    m_trace             = p.get_bool("trace", m_trace);
+    m_trace_file_name   = p.get_str("trace_file_name", "z3.log");
+    m_dot_proof_file    = p.get_str("dot_proof_file", "proof.dot");
+    m_unsat_core        |= p.get_bool("unsat_core", m_unsat_core);
+    m_debug_ref_count   = p.get_bool("debug_ref_count", m_debug_ref_count);
+    m_smtlib2_compliant = p.get_bool("smtlib2_compliant", m_smtlib2_compliant);
+    m_statistics        = p.get_bool("stats", m_statistics);
+}
+
+void context_params::collect_param_descrs(param_descrs & d) {
+    insert_rlimit(d);
+    insert_timeout(d);
+    d.insert("well_sorted_check", CPK_BOOL, "type checker", "false");
+    d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
+    d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
+    d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false");
+    d.insert("dump_models", CPK_BOOL, "dump models whenever check-sat returns sat", "false");
+    d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
+    d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
+    d.insert("dot_proof_file", CPK_STRING, "file in which to output graphical proofs", "proof.dot");
+    d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");
+    d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false");
+    d.insert("stats", CPK_BOOL, "enable/disable statistics", "false");
+    // statistics are hidden as they are controlled by the /st option.
+    collect_solver_param_descrs(d);
+}
+
+void context_params::collect_solver_param_descrs(param_descrs & d) {
+    d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
+    d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
+    d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
+}
+
+params_ref context_params::merge_default_params(params_ref const & p) {
+    if (!m_auto_config && !p.contains("auto_config")) {
+        params_ref new_p = p;
+        new_p.set_bool("auto_config", false);
+        return new_p;
+    }
+    else {
+        return p;
+    }
+}
+
+void context_params::get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) {
+    proofs_enabled     = m.proofs_enabled() && p.get_bool("proof", m_proof);
+    models_enabled     = p.get_bool("model", m_model);
+    unsat_core_enabled = m_unsat_core || p.get_bool("unsat_core", false);
+    p = merge_default_params(p);
+}
+
+ast_manager * context_params::mk_ast_manager() {
+    if (m_manager)
+        return m_manager;
+    ast_manager * r = alloc(ast_manager,
+                            m_proof ? PGM_ENABLED : PGM_DISABLED,
+                            m_trace ? m_trace_file_name.c_str() : nullptr);
+    if (m_smtlib2_compliant)
+        r->enable_int_real_coercions(false);
+    if (m_debug_ref_count)
+        r->debug_ref_count();
+    return r;
+}
+
+

src/params/context_params.h

@@ -0,0 +1,82 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    context_params.h
+
+Abstract:
+
+    Goodies for managing context parameters in the cmd_context and
+    api_context
+
+Author:
+
+    Leonardo (leonardo) 2012-12-01
+
+Notes:
+
+--*/
+#pragma once
+
+#include "util/params.h"
+class ast_manager;
+
+class context_params {
+    void set_bool(bool & opt, char const * param, char const * value);
+    void set_uint(unsigned & opt, char const * param, char const * value);
+
+    unsigned    m_rlimit { 0 };
+    ast_manager* m_manager { nullptr };
+
+public:
+    bool        m_auto_config { true };
+    bool        m_proof { false };
+    std::string m_dot_proof_file;
+    bool        m_debug_ref_count { false };
+    bool        m_trace { false };
+    std::string m_trace_file_name;
+    bool        m_well_sorted_check { false };
+    bool        m_model { true };
+    bool        m_model_validate { false };
+    bool        m_dump_models { false };
+    bool        m_unsat_core { false };
+    bool        m_smtlib2_compliant { false }; // it must be here because it enable/disable the use of coercions in the ast_manager.
+    unsigned    m_timeout { UINT_MAX } ;
+    bool        m_statistics { false };
+
+    unsigned rlimit() const { return m_rlimit; }
+    context_params();
+    void set(char const * param, char const * value);
+    void set_rlimit(unsigned lim) { m_rlimit = lim; }
+    void updt_params();
+    void updt_params(params_ref const & p);
+    static void collect_param_descrs(param_descrs & d);
+    /*
+      REG_PARAMS('context_params::collect_param_descrs')
+    */
+
+    /**
+       \brief Goodies for extracting parameters for creating a solver object.
+    */
+    void get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled);
+
+    static void collect_solver_param_descrs(param_descrs & d);
+
+    /**
+       \brief Include in p parameters derived from this context_params.
+       These are parameters that are meaningful for tactics and solvers.
+       Example: auto_config
+    */
+    params_ref merge_default_params(params_ref const & p);
+
+    /**
+       \brief Create an AST manager using this configuration.
+    */
+    ast_manager * mk_ast_manager();
+
+    void set_foreign_manager(ast_manager* m) { m_manager = m; }
+    bool owns_manager() const { return m_manager != nullptr; }
+};
+
+

src/params/pattern_inference_params.cpp

@@ -0,0 +1,47 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    pattern_inference_params.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-12-02.
+
+Revision History:
+
+--*/
+#include "params/pattern_inference_params.h"
+#include "params/pattern_inference_params_helper.hpp"
+
+void pattern_inference_params::updt_params(params_ref const & _p) {
+    pattern_inference_params_helper p(_p);
+    m_pi_max_multi_patterns      = p.max_multi_patterns();
+    m_pi_block_loop_patterns     = p.block_loop_patterns();
+    m_pi_arith                   = static_cast<arith_pattern_inference_kind>(p.arith());
+    m_pi_use_database            = p.use_database();
+    m_pi_arith_weight            = p.arith_weight();
+    m_pi_non_nested_arith_weight = p.non_nested_arith_weight();
+    m_pi_pull_quantifiers        = p.pull_quantifiers();
+    m_pi_warnings                = p.warnings();
+}
+
+#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+
+void pattern_inference_params::display(std::ostream & out) const {
+    DISPLAY_PARAM(m_pi_max_multi_patterns);
+    DISPLAY_PARAM(m_pi_block_loop_patterns);
+    DISPLAY_PARAM(m_pi_arith);
+    DISPLAY_PARAM(m_pi_use_database);
+    DISPLAY_PARAM(m_pi_arith_weight);
+    DISPLAY_PARAM(m_pi_non_nested_arith_weight);
+    DISPLAY_PARAM(m_pi_pull_quantifiers);
+    DISPLAY_PARAM(m_pi_nopat_weight);
+    DISPLAY_PARAM(m_pi_avoid_skolems);
+    DISPLAY_PARAM(m_pi_warnings);
+}

src/params/pattern_inference_params.h

@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    pattern_inference_params.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-03-24.
+
+Revision History:
+
+--*/
+#pragma once
+
+#include "util/params.h"
+
+enum arith_pattern_inference_kind {
+    AP_NO,           // do not infer patterns with arithmetic terms
+    AP_CONSERVATIVE, // only infer patterns with arithmetic terms if there is no other option
+    AP_FULL          // always use patterns with arithmetic terms
+};
+
+struct pattern_inference_params {
+    unsigned                      m_pi_max_multi_patterns; 
+    bool                          m_pi_block_loop_patterns; 
+    arith_pattern_inference_kind  m_pi_arith;
+    bool                          m_pi_use_database;
+    unsigned                      m_pi_arith_weight;
+    unsigned                      m_pi_non_nested_arith_weight;
+    bool                          m_pi_pull_quantifiers;
+    int                           m_pi_nopat_weight;
+    bool                          m_pi_avoid_skolems;
+    bool                          m_pi_warnings;
+    
+    pattern_inference_params(params_ref const & p = params_ref()):
+        m_pi_nopat_weight(-1),
+        m_pi_avoid_skolems(true) {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & _p);
+
+    void display(std::ostream & out) const;
+};
+
+

src/params/pattern_inference_params_helper.pyg

@@ -0,0 +1,12 @@
+def_module_params(class_name='pattern_inference_params_helper',
+                  module_name='pi',
+                  description='pattern inference (heuristics) for universal formulas (without annotation)',
+                  export=True,
+                  params=(('max_multi_patterns', UINT, 0, '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'),
+                          ('block_loop_patterns', BOOL, True, 'block looping patterns during pattern inference'),
+                          ('arith', UINT, 1, '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'),
+                          ('use_database', BOOL, False, 'use pattern database'),
+                          ('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'),
+                          ('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pattern has non nested arithmetic terms'),
+                          ('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),
+                          ('warnings', BOOL, False, 'enable/disable warning messages in the pattern inference module')))