fix regression in get-consequence on QF_FD

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/api/api_solver.cpp

@@ -79,22 +79,24 @@ extern "C" {
     }
 
     void solver2smt2_pp::check(unsigned n, expr* const* asms) {
-        for (unsigned i = 0; i < n; ++i) {
+        for (unsigned i = 0; i < n; ++i) 
             m_pp_util.collect(asms[i]);
-        }
         m_pp_util.display_decls(m_out);
         m_out << "(check-sat";        
-        for (unsigned i = 0; i < n; ++i) {
+        for (unsigned i = 0; i < n; ++i) 
             m_pp_util.display_expr(m_out << "\n", asms[i]);            
-        }
-        for (expr* e : m_tracked) {
+        for (expr* e : m_tracked) 
             m_pp_util.display_expr(m_out << "\n", e);
-        }
         m_out << ")\n";
         m_out.flush();
     }
 
     void solver2smt2_pp::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& variables) {
+        for (expr* a : assumptions)
+            m_pp_util.collect(a);
+        for (expr* v : variables)
+            m_pp_util.collect(v);
+        m_pp_util.display_decls(m_out);        
         m_out << "(get-consequences (";
         for (expr* f : assumptions) {
             m_out << "\n";
@@ -105,7 +107,7 @@ extern "C" {
             m_out << "\n";
             m_pp_util.display_expr(m_out, f);
         }
-        m_out << ")\n";
+        m_out << "))\n";
         m_out.flush();
     }
 

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp

@@ -190,18 +190,24 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
         }
     }
 
-    unsigned m_keypos;
+    unsigned m_keypos { 0 };
 
     void start_rewrite() {
         m_keypos = m_keys.size();
     }
 
     void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) {
-        for (unsigned i = m_keypos; i < m_keys.size(); ++i) {
-            const2bits.insert(m_keys[i].get(), m_values[i].get());
-        }
-        for (func_decl* f : m_newbits) newbits.push_back(f);
-
+        for (unsigned i = m_keypos; i < m_keys.size(); ++i) 
+            const2bits.insert(m_keys.get(i), m_values.get(i));
+        for (func_decl* f : m_newbits) 
+            newbits.push_back(f);        
+    }
+
+    void get_translation(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) {
+        for (unsigned i = 0; i < m_keys.size(); ++i) 
+            const2bits.insert(m_keys.get(i), m_values.get(i));
+        for (func_decl* f : m_newbits) 
+            newbits.push_back(f);        
     }
 
     template<typename V>
@@ -679,6 +685,7 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
     void pop(unsigned s) { m_cfg.pop(s); }
     void start_rewrite() { m_cfg.start_rewrite(); }
     void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) { m_cfg.end_rewrite(const2bits, newbits); }
+    void get_translation(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) { m_cfg.get_translation(const2bits, newbits); }
     unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); }
 };
 
@@ -734,3 +741,7 @@ void bit_blaster_rewriter::start_rewrite() {
 void bit_blaster_rewriter::end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) {
     m_imp->end_rewrite(const2bits, newbits);
 }
+
+void bit_blaster_rewriter::get_translation(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) {
+    m_imp->get_translation(const2bits, newbits);
+}

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h

@@ -34,6 +34,7 @@ class bit_blaster_rewriter {
     void cleanup();
     void start_rewrite();
     void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits);
+    void get_translation(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits);
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
     void push();
     void pop(unsigned num_scopes);

src/sat/sat_solver/inc_sat_solver.cpp

@@ -718,7 +718,7 @@ class inc_sat_solver : public solver {
     bool internalize_var(expr* v, sat::bool_var_vector& bvars) {
         obj_map<func_decl, expr*> const2bits;
         ptr_vector<func_decl> newbits;
-        m_bb_rewriter->end_rewrite(const2bits, newbits);
+        m_bb_rewriter->get_translation(const2bits, newbits);
         expr* bv;
         bv_util bvutil(m);
         bool internalized = false;

src/tactic/fd_solver/enum2bv_solver.cpp

@@ -146,6 +146,7 @@ class enum2bv_solver : public solver_na2as {
         m_rewriter.flush_side_constraints(bounds);
         m_solver->assert_expr(bounds);
 
+
         // translate enumeration constants to bit-vectors.
         for (expr* v : vars) {
             func_decl* f = nullptr;
@@ -159,12 +160,13 @@ class enum2bv_solver : public solver_na2as {
         lbool r = m_solver->get_consequences(asms, bvars, consequences);
 
         // translate bit-vector consequences back to enumeration types
-        for (unsigned i = 0; i < consequences.size(); ++i) {
+        unsigned i = 0;
+        for (expr* c : consequences) {
             expr* a = nullptr, *b = nullptr, *u = nullptr, *v = nullptr;
             func_decl* f;
             rational num;
             unsigned bvsize;
-            VERIFY(m.is_implies(consequences[i].get(), a, b));
+            VERIFY(m.is_implies(c, a, b));
             if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) {
                 SASSERT(num.is_unsigned());
                 expr_ref head(m);
@@ -174,6 +176,7 @@ class enum2bv_solver : public solver_na2as {
                     consequences[i] = m.mk_implies(a, head);
                 }
             }
+            ++i;
         }
         return r;
     }