running updates to bv_solver (#4674)

* na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * dbg Signed-off-by: Nikolaj Bjorner <[email protected]> * bv Signed-off-by: Nikolaj Bjorner <[email protected]> * drat and fresh Signed-off-by: Nikolaj Bjorner <[email protected]> * move ackerman functionality Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * debugability Signed-off-by: Nikolaj Bjorner <[email protected]> * towards debugability Signed-off-by: Nikolaj Bjorner <[email protected]> * missing file Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * remove csp Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Sep 8, 2020 · d02b0cd · d02b0cd
1 parent 4d1a2a2
commit d02b0cd
Show file tree

Hide file tree

Showing 63 changed files with 3,049 additions and 3,084 deletions.
diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt
@@ -14,7 +14,6 @@ z3_add_component(ast
     ast_translation.cpp
     ast_util.cpp
     bv_decl_plugin.cpp
-    csp_decl_plugin.cpp
     datatype_decl_plugin.cpp
     decl_collector.cpp
     display_dimacs.cpp

diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
@@ -1342,6 +1342,17 @@ std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p) {
     return out;
 }
 
+std::ostream& operator<<(std::ostream& out, mk_ismt2_func const& p) {
+    smt2_pp_environment_dbg env(p.m);        
+    format_ref r(fm(p.m));
+    unsigned len = 0;
+    r = env.pp_fdecl(p.m_fn, len);
+    params_ref pa;
+    pp(out, r.get(), p.m, pa);
+    return out;
+}
+
+
 std::ostream& operator<<(std::ostream& out, expr_ref const&  e) {
     return out << mk_ismt2_pp(e.get(), e.get_manager());
 }
@@ -1388,6 +1399,8 @@ std::ostream& operator<<(std::ostream& out, sort_ref_vector const&  e) {
     return out;
 }
 
+
+
 #ifdef Z3DEBUG
 void pp(expr const * n, ast_manager & m) {
     std::cout << mk_ismt2_pp(const_cast<expr*>(n), m) << std::endl;

diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
@@ -122,6 +122,7 @@ struct mk_ismt2_pp {
     mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr);
 };
 
+
 std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p);
 
 std::ostream& operator<<(std::ostream& out, expr_ref const& e);
@@ -136,3 +137,10 @@ std::ostream& operator<<(std::ostream& out, var_ref_vector const& e);
 std::ostream& operator<<(std::ostream& out, func_decl_ref_vector const& e);
 std::ostream& operator<<(std::ostream& out, sort_ref_vector const& e);
 
+struct mk_ismt2_func {
+    func_decl* m_fn;
+    ast_manager &m;
+    mk_ismt2_func(func_decl* f, ast_manager& m): m_fn(f), m(m) {}
+};
+
+std::ostream& operator<<(std::ostream& out, mk_ismt2_func const& f);
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
@@ -131,12 +131,8 @@ void bv_decl_plugin::finalize() {
 
     DEC_REF(m_int2bv);
     DEC_REF(m_bv2int);
-    vector<ptr_vector<func_decl> >::iterator it  = m_bit2bool.begin();
-    vector<ptr_vector<func_decl> >::iterator end = m_bit2bool.end();
-    for (; it != end; ++it) {
-        ptr_vector<func_decl> & ds = *it;
+    for (auto& ds : m_bit2bool)
         DEC_REF(ds);
-    }
     DEC_REF(m_mkbv);
 }
 
@@ -829,6 +825,14 @@ bool bv_recognizers::is_bv2int(expr const* e, expr*& r) const {
     return true;
 }
 
+bool bv_recognizers::is_bit2bool(expr* e, expr*& bv, unsigned& idx) const {
+    if (!is_bit2bool(e))
+        return false;
+    bv = to_app(e)->get_arg(0);
+    idx = to_app(e)->get_parameter(0).get_int();
+    return true;
+}
+
 bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational & result) {
     if (n.is_one()) {
         result = n;

diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
@@ -368,6 +368,9 @@ class bv_recognizers {
     MATCH_BINARY(is_bv_sdivi);
     MATCH_BINARY(is_bv_udivi);
     MATCH_BINARY(is_bv_smodi);
+    MATCH_UNARY(is_bit2bool);
+    MATCH_UNARY(is_int2bv);
+    bool is_bit2bool(expr* e, expr*& bv, unsigned& idx) const;
 
     rational norm(rational const & val, unsigned bv_size, bool is_signed) const ;
     rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
@@ -432,6 +435,7 @@ class bv_util : public bv_recognizers {
     app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, n, m); }
     app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); }
     app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); }
+    app * mk_bit2bool(expr* e, unsigned idx) { parameter p(idx); return m_manager.mk_app(get_fid(), OP_BIT2BOOL, 1, &p, 1, &e); }
 
     private:
     void log_bv_from_exprs(app * r, unsigned n, expr* const* es) {