merge

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

contrib/cmake/src/ast/rewriter/CMakeLists.txt

@@ -9,14 +9,15 @@ z3_add_component(rewriter
     datatype_rewriter.cpp
     der.cpp
     dl_rewriter.cpp
+    enum2bv_rewriter.cpp
     expr_replacer.cpp
     expr_safe_replace.cpp
     factor_rewriter.cpp
-    fd_rewriter.cpp
     fpa_rewriter.cpp
     label_rewriter.cpp
     mk_simplified_app.cpp
     pb_rewriter.cpp
+    pb2bv_rewriter.cpp
     quant_hoist.cpp
     rewriter.cpp
     seq_rewriter.cpp

contrib/cmake/src/tactic/portfolio/CMakeLists.txt

@@ -1,6 +1,9 @@
 z3_add_component(portfolio
   SOURCES
     default_tactic.cpp
+    enum2bv_solver.cpp
+    pb2bv_solver.cpp
+    bounded_int2bv_solver.cpp
     fd_solver.cpp
     smt_strategic_solver.cpp
   COMPONENT_DEPENDENCIES

contrib/cmake/src/test/CMakeLists.txt

@@ -78,6 +78,7 @@ add_executable(test-z3
   old_interval.cpp
   optional.cpp
   parray.cpp
+  pb2bv.cpp
   pdr.cpp
   permutation.cpp
   polynomial.cpp

examples/python/all_interval_series.py

@@ -0,0 +1,76 @@
+# Copyright Microsoft Research 2016
+# The following script finds sequences of length n-1 of
+# integers 0,..,n-1 such that the difference of the n-1
+# adjacent entries fall in the range 0,..,n-1
+# This is known as the "The All-Interval Series Problem"
+# See http://www.csplib.org/Problems/prob007/
+
+from z3 import *
+import time
+
+def diff_at_j_is_i(xs, j, i):
+    assert(0 <= j and j + 1 < len(xs))
+    assert(1 <= i and i < len(xs))
+    return Or([ And(xs[j][k], xs[j+1][k-i]) for k in range(i,len(xs))] + 
+              [ And(xs[j][k], xs[j+1][k+i]) for k in range(0,len(xs)-i)])
+    
+
+def ais(n):
+    xij = [ [ Bool("x_%d_%d" % (i,j)) for j in range(n)] for i in range(n) ]
+    s = SolverFor("QF_FD")
+# Optionally replace by (slower) default solver if using
+# more then just finite domains (Booleans, Bit-vectors, enumeration types
+# and bounded integers)
+#   s = Solver() 
+    for i in range(n):
+        s.add(AtMost(xij[i] + [1]))
+        s.add(Or(xij[i]))
+    for j in range(n):
+        xi = [ xij[i][j] for i in range(n) ]
+        s.add(AtMost(xi + [1]))
+        s.add(Or(xi))
+    dji = [ [ diff_at_j_is_i(xij, j, i + 1) for i in range(n-1)] for j in range(n-1) ]
+    for j in range(n-1):
+        s.add(AtMost(dji[j] + [1]))
+        s.add(Or(dji[j]))
+    for i in range(n-1):
+        dj = [dji[j][i] for j in range(n-1)]
+        s.add(AtMost(dj + [1]))
+        s.add(Or(dj))
+    return s, xij
+
+def process_model(s, xij, n):
+    # x_ij integer i is at position j
+    # d_ij difference between integer at position j, j+1 is i
+    # sum_j d_ij = 1 i = 1,...,n-1
+    # sum_j x_ij = 1
+    # sum_i x_ij = 1
+    m = s.model()
+    block = []
+    values = []
+    for i in range(n):
+        k = -1
+        for j in range(n):
+            if is_true(m.eval(xij[i][j])):
+               assert(k == -1)
+               block += [xij[i][j]]
+               k = j
+        values += [k]
+    print values
+    sys.stdout.flush()
+    return block
+
+def all_models(n):
+    count = 0
+    s, xij = ais(n)
+    start = time.clock()
+    while sat == s.check():
+        block = process_model(s, xij, n)
+        s.add(Not(And(block)))
+        count += 1
+    print s.statistics()
+    print time.clock() - start
+    print count
+
+set_option(verbose=1)  
+all_models(12)

src/api/api_fpa.cpp

@@ -914,7 +914,7 @@ extern "C" {
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         family_id fid = mk_c(c)->get_fpa_fid();
         expr * e = to_expr(t);
-        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN)) {
+        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
@@ -933,6 +933,8 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_significand_string(c, t);
         RESET_ERROR_CODE();
+        CHECK_NON_NULL(t, 0);
+        CHECK_VALID_AST(t, 0);
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
         unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
@@ -940,10 +942,7 @@ extern "C" {
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
         SASSERT(plugin != 0);
         expr * e = to_expr(t);
-        if (!is_app(e) ||
-            is_app_of(e, fid, OP_FPA_NAN) ||
-            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
-            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return "";
         }
@@ -958,6 +957,7 @@ extern "C" {
         mpqm.set(q, mpfm.sig(val));
         if (!mpfm.is_denormal(val)) mpqm.add(q, mpfm.m_powers2(sbits - 1), q);
         mpqm.div(q, mpfm.m_powers2(sbits - 1), q);
+        if (mpfm.is_inf(val)) mpqm.set(q, 0);
         std::stringstream ss;
         mpqm.display_decimal(ss, q, sbits);
         return mk_c(c)->mk_external_string(ss.str());
@@ -975,10 +975,7 @@ extern "C" {
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
         SASSERT(plugin != 0);
         expr * e = to_expr(t);
-        if (!is_app(e) ||
-            is_app_of(e, fid, OP_FPA_NAN) ||
-            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
-            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             *n = 0;
             return 0;
@@ -1008,10 +1005,7 @@ extern "C" {
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         SASSERT(plugin != 0);
         expr * e = to_expr(t);
-        if (!is_app(e) ||
-            is_app_of(e, fid, OP_FPA_NAN) ||
-            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
-            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return "";
         }
@@ -1040,10 +1034,7 @@ extern "C" {
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         SASSERT(plugin != 0);
         expr * e = to_expr(t);
-        if (!is_app(e) ||
-            is_app_of(e, fid, OP_FPA_NAN) ||
-            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
-            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             *n = 0;
             return 0;

src/api/api_opt.cpp

@@ -27,6 +27,7 @@ Revision History:
 #include"cancel_eh.h"
 #include"scoped_timer.h"
 #include"smt2parser.h"
+#include"api_ast_vector.h"
 
 extern "C" {
 
@@ -296,6 +297,35 @@ extern "C" {
     }
 
 
+    Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_assertions(c, o);
+        RESET_ERROR_CODE();
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        expr_ref_vector hard(mk_c(c)->m());
+        to_optimize_ptr(o)->get_hard_constraints(hard);
+        for (unsigned i = 0; i < hard.size(); i++) {
+            v->m_ast_vector.push_back(hard[i].get());
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(0);        
+    }
+    
+    Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_objectives(c, o);
+        RESET_ERROR_CODE();
+        unsigned n = to_optimize_ptr(o)->num_objectives();
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        for (unsigned i = 0; i < n; i++) {
+            v->m_ast_vector.push_back(to_optimize_ptr(o)->get_objective(i));
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(0);
+    }
+
 
 
 };

src/api/c++/z3++.h

@@ -2053,6 +2053,8 @@ namespace z3 {
             check_error();
             return expr(ctx(), r);
         }
+        expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
+        expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
         stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
         friend std::ostream & operator<<(std::ostream & out, optimize const & s);
         void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }

src/api/dotnet/Optimize.cs

@@ -290,6 +290,33 @@ namespace Microsoft.Z3
             Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s);
         }
 
+        /// <summary>
+        /// The set of asserted formulas.
+        /// </summary>
+        public BoolExpr[] Assertions
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
+
+                ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject));
+                return assertions.ToBoolExprArray();
+            }
+        }
+
+        /// <summary>
+        /// The set of asserted formulas.
+        /// </summary>
+        public Expr[] Objectives
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Expr[]>() != null);
+
+                ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject));
+                return objectives.ToExprArray();
+            }
+        }
 
 
         /// <summary>

src/api/python/z3/z3.py

@@ -6796,6 +6796,14 @@ class Optimize(Z3PPObject):
         """Parse assertions and objectives from a string"""
         Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
 
+    def assertions(self):
+        """Return an AST vector containing all added constraints."""
+        return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
+
+    def objectives(self):
+        """returns set of objective functions"""
+        return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
+
     def __repr__(self):
         """Return a formatted string with all added rules and constraints."""
         return self.sexpr()
@@ -8496,7 +8504,7 @@ class FPNumRef(FPRef):
     """
     def as_string(self):
         s = Z3_fpa_get_numeral_string(self.ctx.ref(), self.as_ast())
-        return ("FPVal(%s, %s)" % (s, FPSortRef(self.sort()).as_string()))
+        return ("FPVal(%s, %s)" % (s, self.sort()))
 
 def is_fp(a):
     """Return `True` if `a` is a Z3 floating-point expression.
@@ -8536,7 +8544,7 @@ def FPSort(ebits, sbits, ctx=None):
     >>> eq(x, FP('x', FPSort(8, 24)))
     True
     """
-    ctx = z3._get_ctx(ctx)
+    ctx = _get_ctx(ctx)
     return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
 
 def _to_float_str(val, exp=0):
@@ -8722,7 +8730,7 @@ def FPs(names, fpsort, ctx=None):
     >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
     fpMul(RNE(), fpAdd(RNE(), x, y), z)
     """
-    ctx = z3._get_ctx(ctx)
+    ctx = _get_ctx(ctx)
     if isinstance(names, str):
         names = names.split(" ")
     return [FP(name, fpsort, ctx) for name in names]

src/api/z3_api.h

@@ -5832,7 +5832,7 @@ extern "C" {
     void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p);
 
     /**
-       \brief Return the set of asserted formulas as a goal object.
+       \brief Return the set of asserted formulas on the solver.
 
        def_API('Z3_solver_get_assertions', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
     */

src/api/z3_optimization.h

@@ -239,6 +239,28 @@ extern "C" {
        def_API('Z3_optimize_get_statistics', STATS, (_in(CONTEXT), _in(OPTIMIZE)))
     */
     Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d);
+
+
+    /**
+       \brief Return the set of asserted formulas on the optimization context.
+
+       def_API('Z3_optimize_get_assertions', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o);
+
+    /**
+       \brief Return objectives on the optimization context.
+       If the objective function is a max-sat objective it is returned
+       as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...)       
+       If the objective function is entered as a maximization objective, then return the corresponding minimizaiton
+       objective. In this way the resulting objective function is always returned as a minimization objective.
+
+       def_API('Z3_optimize_get_objectives', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o);
+    
+        
+
     /*@}*/
     /*@}*/
 

src/ast/rewriter/arith_rewriter.cpp

@@ -162,8 +162,8 @@ bool arith_rewriter::div_polynomial(expr * t, numeral const & g, const_treatment
 }
 
 bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) {
-    numeral c;
-    if (!is_add(arg1) && is_numeral(arg2, c)) {
+    numeral b, c;
+    if (!is_add(arg1) && !m_util.is_mod(arg1) && is_numeral(arg2, c)) {
         numeral a;
         bool r = false;
         expr * pp = get_power_product(arg1, a);
@@ -193,6 +193,45 @@ bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref &
         case EQ: result = m_util.mk_eq(pp, k); return true;
         }
     }
+    expr* t1, *t2;
+    bool is_int;
+    if (m_util.is_mod(arg2)) {
+        std::swap(arg1, arg2);
+        switch (kind) {
+        case LE: kind = GE; break;
+        case GE: kind = LE; break;
+        case EQ: break;
+        }
+    }
+
+    if (m_util.is_numeral(arg2, c, is_int) && is_int && 
+        m_util.is_mod(arg1, t1, t2) && m_util.is_numeral(t2, b, is_int) && !b.is_zero()) {
+        //  mod x b <= c = false if c < 0, b != 0, true if c >= b, b != 0
+        if (c.is_neg()) {
+            switch (kind) {
+            case EQ:
+            case LE: result = m().mk_false(); return true;
+            case GE: result = m().mk_true(); return true;
+            }
+        }                    
+        if (c.is_zero() && kind == GE) {
+            result = m().mk_true(); 
+            return true;
+        }
+        if (c.is_pos() && c >= abs(b)) {
+            switch (kind) {
+            case LE: result = m().mk_true(); return true;
+            case EQ:
+            case GE: result = m().mk_false(); return true;
+            }
+        }
+        // mod x b <= b - 1
+        if (c + rational::one() == abs(b) && kind == LE) {
+            result = m().mk_true();
+            return true;
+        }
+    }
+
     return false;
 }
 

src/ast/rewriter/enum2bv_rewriter.cpp

@@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation
 
 Module Name:
 
-    fd_rewriter.cpp
+    enum2bv_rewriter.cpp
 
 Abstract:
 
@@ -19,11 +19,11 @@ Notes:
 
 #include"rewriter.h"
 #include"rewriter_def.h"
-#include"fd_rewriter.h"
+#include"enum2bv_rewriter.h"
 #include"ast_util.h"
 #include"ast_pp.h"
 
-struct fd_rewriter::imp {
+struct enum2bv_rewriter::imp {
     ast_manager&              m;
     params_ref                m_params;
     obj_map<func_decl, func_decl*> m_enum2bv;
@@ -258,6 +258,7 @@ struct fd_rewriter::imp {
             m_enum_defs.resize(lim);
             m_enum_bvs.resize(lim);
         }
+        m_rw.reset();
     }
 
     void flush_side_constraints(expr_ref_vector& side_constraints) { 
@@ -275,18 +276,18 @@ struct fd_rewriter::imp {
 };
 
 
-fd_rewriter::fd_rewriter(ast_manager & m, params_ref const& p) {  m_imp = alloc(imp, m, p); }
-fd_rewriter::~fd_rewriter() { dealloc(m_imp); }
-void fd_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
-ast_manager & fd_rewriter::m() const { return m_imp->m; }
-unsigned fd_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
-void fd_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p);  }
-obj_map<func_decl, func_decl*> const& fd_rewriter::enum2bv() const { return m_imp->m_enum2bv; }
-obj_map<func_decl, func_decl*> const& fd_rewriter::bv2enum() const { return m_imp->m_bv2enum; }
-obj_map<func_decl, expr*> const& fd_rewriter::enum2def() const { return m_imp->m_enum2def; }
-void fd_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
-void fd_rewriter::push() { m_imp->push(); }
-void fd_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
-void fd_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } 
-unsigned fd_rewriter::num_translated() const { return m_imp->m_num_translated; }
-void fd_rewriter::set_is_fd(i_sort_pred* sp) const { m_imp->set_is_fd(sp); }
+enum2bv_rewriter::enum2bv_rewriter(ast_manager & m, params_ref const& p) {  m_imp = alloc(imp, m, p); }
+enum2bv_rewriter::~enum2bv_rewriter() { dealloc(m_imp); }
+void enum2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
+ast_manager & enum2bv_rewriter::m() const { return m_imp->m; }
+unsigned enum2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
+void enum2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p);  }
+obj_map<func_decl, func_decl*> const& enum2bv_rewriter::enum2bv() const { return m_imp->m_enum2bv; }
+obj_map<func_decl, func_decl*> const& enum2bv_rewriter::bv2enum() const { return m_imp->m_bv2enum; }
+obj_map<func_decl, expr*> const& enum2bv_rewriter::enum2def() const { return m_imp->m_enum2def; }
+void enum2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
+void enum2bv_rewriter::push() { m_imp->push(); }
+void enum2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
+void enum2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } 
+unsigned enum2bv_rewriter::num_translated() const { return m_imp->m_num_translated; }
+void enum2bv_rewriter::set_is_fd(i_sort_pred* sp) const { m_imp->set_is_fd(sp); }

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -0,0 +1,453 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    pb2bv_rewriter.cpp
+
+Abstract:
+
+    Conversion from pseudo-booleans to bit-vectors.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-10-23
+
+Notes:
+
+--*/
+
+#include"rewriter.h"
+#include"rewriter_def.h"
+#include"statistics.h"
+#include"pb2bv_rewriter.h"
+#include"sorting_network.h"
+#include"ast_util.h"
+#include"ast_pp.h"
+
+
+struct pb2bv_rewriter::imp {
+
+    struct argc_t {
+        expr*    m_arg;
+        rational m_coeff;
+        argc_t():m_arg(0), m_coeff(0) {}
+        argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {}
+    };
+    
+    struct argc_gt {
+        bool operator()(argc_t const& a, argc_t const& b) const {
+            return a.m_coeff > b.m_coeff;
+        }
+    };
+
+    struct argc_entry {
+        unsigned m_index;
+        rational m_k;
+        expr*    m_value;
+        argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {}
+        argc_entry():m_index(0), m_k(0), m_value(0) {}
+        
+        struct eq {
+            bool operator()(argc_entry const& a, argc_entry const& b) const {
+                return a.m_index == b.m_index && a.m_k == b.m_k;
+            }
+        };
+        struct hash {
+            unsigned operator()(argc_entry const& a) const {
+                return a.m_index ^ a.m_k.hash();
+            }
+        };
+    };
+    typedef hashtable<argc_entry, argc_entry::hash, argc_entry::eq> argc_cache;
+
+    ast_manager&              m;
+    params_ref                m_params;
+    expr_ref_vector           m_lemmas;
+    func_decl_ref_vector      m_fresh;       // all fresh variables
+    unsigned_vector           m_fresh_lim;
+    unsigned                  m_num_translated;
+
+    struct card2bv_rewriter {               
+        typedef expr* literal;
+        typedef ptr_vector<expr> literal_vector;
+        psort_nw<card2bv_rewriter> m_sort;
+        ast_manager& m;
+        imp&         m_imp;
+        arith_util   au;
+        pb_util      pb;
+        bv_util      bv;
+        expr_ref_vector m_trail;
+
+        unsigned get_num_bits(func_decl* f) {
+            rational r(0);
+            unsigned sz = f->get_arity();
+            for (unsigned i = 0; i < sz; ++i) {
+                r += pb.get_coeff(f, i);
+            }
+            r = r > pb.get_k(f)? r : pb.get_k(f);
+            return r.get_num_bits();
+        }
+
+        void mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+
+            expr_ref zero(m), a(m), b(m);
+            expr_ref_vector es(m);
+            unsigned bw = get_num_bits(f);        
+            zero = bv.mk_numeral(rational(0), bw);
+            for (unsigned i = 0; i < sz; ++i) {
+                es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero));
+            }
+            switch (es.size()) {
+            case 0:  a = zero; break;
+            case 1:  a = es[0].get(); break;
+            default:
+                a = es[0].get();
+                for (unsigned i = 1; i < es.size(); ++i) {
+                    a = bv.mk_bv_add(a, es[i].get());
+                }
+                break;
+            }
+            b = bv.mk_numeral(pb.get_k(f), bw);
+            
+            switch (f->get_decl_kind()) {
+            case OP_AT_MOST_K:
+            case OP_PB_LE:
+                result = bv.mk_ule(a, b);
+                break;
+            case OP_AT_LEAST_K:
+            case OP_PB_GE:
+                result = bv.mk_ule(b, a);
+                break;
+            case OP_PB_EQ:
+                result = m.mk_eq(a, b);
+                break;
+            default:
+                UNREACHABLE();
+            }
+            TRACE("pb", tout << result << "\n";);
+        }
+
+        bool mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+            decl_kind kind = f->get_decl_kind();
+            if (kind != OP_PB_GE && kind != OP_AT_LEAST_K) {
+                return false;
+            }
+            unsigned max_clauses = sz*10;
+            vector<argc_t> argcs;
+            for (unsigned i = 0; i < sz; ++i) {
+                argcs.push_back(argc_t(args[i], pb.get_coeff(f, i)));
+            }
+            std::sort(argcs.begin(), argcs.end(), argc_gt());
+            DEBUG_CODE(
+                for (unsigned i = 0; i + 1 < sz; ++i) {
+                    SASSERT(argcs[i].m_coeff >= argcs[i+1].m_coeff);
+                });
+            result = m.mk_app(f, sz, args);
+            TRACE("pb", tout << result << "\n";);
+            argc_cache cache;
+            expr_ref_vector trail(m);
+            vector<rational> todo_k;
+            unsigned_vector  todo_i;
+            todo_k.push_back(pb.get_k(f));
+            todo_i.push_back(0);
+            argc_entry entry1;
+            while (!todo_i.empty()) {
+                SASSERT(todo_i.size() == todo_k.size());
+                if (cache.size() > max_clauses) {
+                    return false;
+                }
+                unsigned i = todo_i.back();
+                rational k = todo_k.back();
+                argc_entry entry(i, k);
+                if (cache.contains(entry)) {
+                    todo_i.pop_back();
+                    todo_k.pop_back();
+                    continue;
+                }
+                SASSERT(i < sz);
+                SASSERT(!k.is_neg());
+                rational const& coeff = argcs[i].m_coeff;
+                expr* arg = argcs[i].m_arg;
+                if (i + 1 == sz) {
+                    if (k.is_zero()) {
+                        entry.m_value = m.mk_true();
+                    }
+                    else if (coeff < k) {
+                        entry.m_value = m.mk_false();
+                    }
+                    else if (coeff.is_zero()) {
+                            entry.m_value = m.mk_true();
+                    }
+                    else {
+                        SASSERT(coeff >= k && k.is_pos());
+                        entry.m_value = arg;
+                    }
+                    todo_i.pop_back();
+                    todo_k.pop_back();
+                    cache.insert(entry);
+                    continue;
+                }
+                entry.m_index++;        
+                expr* lo = 0, *hi = 0;
+                if (cache.find(entry, entry1)) {
+                    lo = entry1.m_value;                
+                }
+                else {
+                    todo_i.push_back(i+1);
+                    todo_k.push_back(k);
+                }                
+                entry.m_k -= coeff;
+                if (!entry.m_k.is_pos()) {
+                    hi = m.mk_true();
+                }
+                else if (cache.find(entry, entry1)) {
+                    hi = entry1.m_value;
+                }
+                else {
+                    todo_i.push_back(i+1);
+                    todo_k.push_back(entry.m_k);
+                }
+                if (hi && lo) {
+                    todo_i.pop_back();
+                    todo_k.pop_back();
+                    entry.m_index = i;
+                    entry.m_k = k;
+                    entry.m_value = mk_ite(arg, hi, lo);
+                    trail.push_back(entry.m_value);
+                    cache.insert(entry);
+                }
+            }        
+            argc_entry entry(0, pb.get_k(f));
+            VERIFY(cache.find(entry, entry));
+            result = entry.m_value;
+            TRACE("pb", tout << result << "\n";);
+            return true;
+        }
+
+        expr* negate(expr* e) {
+            if (m.is_not(e, e)) return e;
+            return m.mk_not(e);
+        }
+        expr* mk_ite(expr* c, expr* hi, expr* lo) {
+            while (m.is_not(c, c)) {
+                std::swap(hi, lo);
+            }
+            if (hi == lo) return hi;
+            if (m.is_true(hi) && m.is_false(lo)) return c;
+            if (m.is_false(hi) && m.is_true(lo)) return negate(c);
+            if (m.is_true(hi)) return m.mk_or(c, lo);
+            if (m.is_false(lo)) return m.mk_and(c, hi);
+            if (m.is_false(hi)) return m.mk_and(negate(c), lo);
+            if (m.is_true(lo)) return m.mk_implies(c, hi);
+            return m.mk_ite(c, hi, lo);
+        }
+        
+        bool is_or(func_decl* f) {
+            switch (f->get_decl_kind()) {
+            case OP_AT_MOST_K:
+            case OP_PB_LE:
+                return false;
+            case OP_AT_LEAST_K:
+            case OP_PB_GE: 
+                return pb.get_k(f).is_one();
+            case OP_PB_EQ:
+                return false;
+            default:
+                UNREACHABLE();
+                return false;
+            }
+        }
+
+
+    public:
+
+        card2bv_rewriter(imp& i, ast_manager& m):
+            m(m),
+            m_imp(i),
+            au(m),
+            pb(m),
+            bv(m),
+            m_sort(*this),
+            m_trail(m)
+        {}
+
+        br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+            if (f->get_family_id() == pb.get_family_id()) {
+                mk_pb(f, sz, args, result);
+                ++m_imp.m_num_translated;
+                return BR_DONE;
+            }
+            else if (f->get_family_id() == au.get_family_id() && mk_arith(f, sz, args, result)) {
+                ++m_imp.m_num_translated;
+                return BR_DONE;
+            }
+            else {
+                return BR_FAILED;
+            }
+        }
+
+        //
+        // NSB: review
+        // we should remove this code and rely on a layer above to deal with 
+        // whatever it accomplishes. It seems to break types.
+        // 
+        bool mk_arith(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+            if (f->get_decl_kind() == OP_ADD) {
+                unsigned bits = 0;
+                for (unsigned i = 0; i < sz; i++) {
+                    rational val1, val2;
+                    if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) {
+                        bits += val1.get_num_bits();
+                    }
+                    else if (m.is_ite(args[i]) &&
+                             au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() &&
+                             au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) {
+                        bits++;                        
+                    }
+                    else
+                        return false;
+                }
+                
+                result = 0;
+                for (unsigned i = 0; i < sz; i++) {
+                    rational val1, val2;
+                    expr * q;
+                    if (au.is_int(args[i]) && au.is_numeral(args[i], val1))
+                        q = bv.mk_numeral(val1, bits);
+                    else
+                        q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits));
+                    result = (i == 0) ? q : bv.mk_bv_add(result.get(), q);
+                }                
+                return true;
+            }
+            else {
+                return false;
+            } 
+        }
+
+        void mk_pb(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+            SASSERT(f->get_family_id() == pb.get_family_id());
+            if (is_or(f)) {
+                result = m.mk_or(sz, args);
+            }
+            else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) {
+                result = m_sort.le(true, pb.get_k(f).get_unsigned(), sz, args);
+            }
+            else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) {
+                result = m_sort.ge(true, pb.get_k(f).get_unsigned(), sz, args);
+            }
+            else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
+                result = m_sort.eq(pb.get_k(f).get_unsigned(), sz, args);
+            }
+            else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
+                result = m_sort.le(true, pb.get_k(f).get_unsigned(), sz, args);
+            }
+            else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
+                result = m_sort.ge(true, pb.get_k(f).get_unsigned(), sz, args);
+            }
+            else if (!mk_shannon(f, sz, args, result)) {
+                mk_bv(f, sz, args, result);
+            }
+        }
+   
+        // definitions used for sorting network
+        literal mk_false() { return m.mk_false(); }
+        literal mk_true() { return m.mk_true(); }
+        literal mk_max(literal a, literal b) { return trail(m.mk_or(a, b)); }
+        literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); }
+        literal mk_not(literal a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); }
+
+        std::ostream& pp(std::ostream& out, literal lit) {  return out << mk_ismt2_pp(lit, m);  }
+        
+        literal trail(literal l) {
+            m_trail.push_back(l);
+            return l;
+        }
+        literal fresh() {
+            expr_ref fr(m.mk_fresh_const("sn", m.mk_bool_sort()), m);
+            m_imp.m_fresh.push_back(to_app(fr)->get_decl());
+            return trail(fr);
+        }
+        
+        void mk_clause(unsigned n, literal const* lits) {
+            m_imp.m_lemmas.push_back(mk_or(m, n, lits));
+        }        
+    };
+
+    struct card2bv_rewriter_cfg : public default_rewriter_cfg {
+        card2bv_rewriter m_r;
+        bool rewrite_patterns() const { return false; }
+        bool flat_assoc(func_decl * f) const { return false; }
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+            result_pr = 0;
+            return m_r.mk_app_core(f, num, args, result);
+        }
+        card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}
+    };
+    
+    class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
+    public:
+        card2bv_rewriter_cfg m_cfg;
+        card_pb_rewriter(imp& i, ast_manager & m):
+            rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
+            m_cfg(i, m) {}
+    };
+
+    card_pb_rewriter m_rw;
+    
+    imp(ast_manager& m, params_ref const& p): 
+        m(m), m_params(p), m_lemmas(m),
+        m_fresh(m),
+        m_num_translated(0), 
+        m_rw(*this, m) {
+    }
+
+    void updt_params(params_ref const & p) {}
+    unsigned get_num_steps() const { return m_rw.get_num_steps(); }
+    void cleanup() { m_rw.cleanup(); }
+    void operator()(expr * e, expr_ref & result, proof_ref & result_proof) {
+        m_rw(e, result, result_proof);
+    }
+    void push() {
+        m_fresh_lim.push_back(m_fresh.size());
+    }
+    void pop(unsigned num_scopes) {
+        SASSERT(m_lemmas.empty()); // lemmas must be flushed before pop.
+        if (num_scopes > 0) {
+            SASSERT(num_scopes <= m_fresh_lim.size());
+            unsigned new_sz = m_fresh_lim.size() - num_scopes;
+            unsigned lim = m_fresh_lim[new_sz];
+            m_fresh.resize(lim);
+            m_fresh_lim.resize(new_sz);
+        }
+        m_rw.reset();
+    }
+
+    void flush_side_constraints(expr_ref_vector& side_constraints) { 
+        side_constraints.append(m_lemmas);  
+        m_lemmas.reset(); 
+    }
+
+    void collect_statistics(statistics & st) const {
+        st.update("pb-aux-variables", m_fresh.size());
+        st.update("pb-aux-clauses", m_rw.m_cfg.m_r.m_sort.m_stats.m_num_compiled_clauses);
+    }
+
+};
+
+
+pb2bv_rewriter::pb2bv_rewriter(ast_manager & m, params_ref const& p) {  m_imp = alloc(imp, m, p); }
+pb2bv_rewriter::~pb2bv_rewriter() { dealloc(m_imp); }
+void pb2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
+ast_manager & pb2bv_rewriter::m() const { return m_imp->m; }
+unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
+void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p);  }
+func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; }
+void pb2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
+void pb2bv_rewriter::push() { m_imp->push(); }
+void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
+void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } 
+unsigned pb2bv_rewriter::num_translated() const { return m_imp->m_num_translated; }
+
+void pb2bv_rewriter::collect_statistics(statistics & st) const { m_imp->collect_statistics(st); }

src/ast/rewriter/pb2bv_rewriter.h

@@ -3,46 +3,44 @@ Copyright (c) 2016 Microsoft Corporation
 
 Module Name:
 
-    fd_rewriter.h
+    pb2bv_rewriter.h
 
 Abstract:
 
-    Conversion from enumeration types to bit-vectors.
+    Conversion from pseudo-booleans to bit-vectors.
 
 Author:
 
-    Nikolaj Bjorner (nbjorner) 2016-10-18
+    Nikolaj Bjorner (nbjorner) 2016-10-23
 
 Notes:
 
 --*/
-#ifndef ENUM_REWRITER_H_
-#define ENUM_REWRITER_H_
+#ifndef PB2BV_REWRITER_H_
+#define PB2BV_REWRITER_H_
 
-#include"datatype_decl_plugin.h"
+#include"pb_decl_plugin.h"
 #include"rewriter_types.h"
 #include"expr_functors.h"
 
-class fd_rewriter {
+class pb2bv_rewriter {
     struct imp;
     imp* m_imp;
 public:
-    fd_rewriter(ast_manager & m, params_ref const& p);
-    ~fd_rewriter();
+    pb2bv_rewriter(ast_manager & m, params_ref const& p);
+    ~pb2bv_rewriter();
 
     void updt_params(params_ref const & p);
     ast_manager & m() const;
     unsigned get_num_steps() const;
     void cleanup();
-    obj_map<func_decl, func_decl*> const& enum2bv() const;
-    obj_map<func_decl, func_decl*> const& bv2enum() const;
-    obj_map<func_decl, expr*> const& enum2def() const;
+    func_decl_ref_vector const& fresh_constants() const;
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
     void push();
     void pop(unsigned num_scopes);
     void flush_side_constraints(expr_ref_vector& side_constraints);
     unsigned num_translated() const;
-    void set_is_fd(i_sort_pred* sp) const;
+    void collect_statistics(statistics & st) const;
 };
 
 #endif

src/ast/rewriter/pb_rewriter.cpp

@@ -257,7 +257,12 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
             all_unit &= m_coeffs.back().is_one();
         }
         if (is_eq) {
-            result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k);
+            if (sz == 0) {
+                result = k.is_zero()?m.mk_true():m.mk_false();
+            }
+            else {
+                result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k);
+            }
         }
         else if (all_unit && k.is_one()) {
             result = mk_or(m, sz, m_args.c_ptr());

src/cmd_context/check_logic.cpp

@@ -182,8 +182,8 @@ struct check_logic::imp {
             m_quantifiers = false;
         }
         else if (logic == "QF_FD") {
-            m_bvs = true;
-            m_uf = true;
+            m_bvs         = true;
+            m_uf          = true;
             m_ints        = true;
         }
         else {

src/cmd_context/cmd_context.cpp

@@ -547,6 +547,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
         s == "QF_BVFP" ||
         s == "QF_S" ||
         s == "ALL" ||
+        s == "QF_FD" || 
         s == "HORN";
 }
 

src/opt/maxres.cpp

@@ -297,12 +297,16 @@ public:
         sort_assumptions(mutex);
         ptr_vector<expr> core(mutex.size(), mutex.c_ptr());
         remove_soft(core, m_asms);
-        rational weight(0);
+        rational weight(0), sum1(0), sum2(0);
+        for (unsigned i = 0; i < mutex.size(); ++i) {
+            sum1 += get_weight(mutex[i].get());
+        }
         while (!mutex.empty()) {
             expr_ref soft = mk_or(mutex);
             rational w = get_weight(mutex.back());
             weight = w - weight;
             m_lower += weight*rational(mutex.size()-1);
+            sum2 += weight*rational(mutex.size());
             add_soft(soft, weight);
             mutex.pop_back();
             while (!mutex.empty() && get_weight(mutex.back()) == w) {
@@ -310,6 +314,7 @@ public:
             }
             weight = w;
         }        
+        SASSERT(sum1 == sum2);
     }
 
     lbool check_sat_hill_climb(expr_ref_vector& asms1) {
@@ -398,7 +403,7 @@ public:
         while (is_sat == l_false) {
             core.reset();
             s().get_unsat_core(core);
-            //verify_core(core);
+            // verify_core(core);
             model_ref mdl;
             get_mus_model(mdl);
             is_sat = minimize_core(core);
@@ -772,8 +777,6 @@ public:
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             m_assignment[i] = is_true(m_soft[i]);
         }
-
-
        
         DEBUG_CODE(verify_assignment(););
 

src/opt/opt_context.cpp

@@ -181,6 +181,43 @@ namespace opt {
         clear_state();
     }
 
+    void context::get_hard_constraints(expr_ref_vector& hard) {
+        hard.append(m_scoped_state.m_hard);
+    }
+
+    expr_ref context::get_objective(unsigned i) {
+        SASSERT(i < num_objectives());
+        objective const& o = m_scoped_state.m_objectives[i];
+        expr_ref result(m), zero(m);
+        expr_ref_vector args(m);
+        switch (o.m_type) {
+        case O_MAXSMT:
+            zero = m_arith.mk_numeral(rational(0), false);
+            for (unsigned i = 0; i < o.m_terms.size(); ++i) {
+                args.push_back(m.mk_ite(o.m_terms[i], zero, m_arith.mk_numeral(o.m_weights[i], false)));
+            }
+            result = m_arith.mk_add(args.size(), args.c_ptr());
+            break;
+        case O_MAXIMIZE:
+            result = o.m_term;
+            if (m_arith.is_arith_expr(result)) {
+                result = m_arith.mk_uminus(result);
+            }
+            else if (m_bv.is_bv(result)) {
+                result = m_bv.mk_bv_neg(result);
+            }
+            else {
+                UNREACHABLE();
+            }
+            break;
+        case O_MINIMIZE:
+            result = o.m_term;
+            break;
+        }
+        return result;
+    }
+
+
     unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) { 
         clear_state();
         return m_scoped_state.add(f, w, id);
@@ -1328,14 +1365,21 @@ namespace opt {
     }
 
     std::string context::to_string() const {
+        return to_string(m_scoped_state.m_hard, m_scoped_state.m_objectives);
+    }
+
+    std::string context::to_string_internal() const {
+        return to_string(m_hard_constraints, m_objectives);
+    }
+
+    std::string context::to_string(expr_ref_vector const& hard, vector<objective> const& objectives) const {
         smt2_pp_environment_dbg env(m);
         ast_pp_util visitor(m);
         std::ostringstream out;
-#define PP(_e_) ast_smt2_pp(out, _e_, env);
-        visitor.collect(m_scoped_state.m_hard);
+        visitor.collect(hard);
                 
-        for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
-            objective const& obj = m_scoped_state.m_objectives[i];
+        for (unsigned i = 0; i < objectives.size(); ++i) {
+            objective const& obj = objectives[i];
             switch(obj.m_type) {
             case O_MAXIMIZE: 
             case O_MINIMIZE:
@@ -1351,33 +1395,34 @@ namespace opt {
         }
 
         visitor.display_decls(out);
-        visitor.display_asserts(out, m_scoped_state.m_hard, m_pp_neat);
-        for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
-            objective const& obj = m_scoped_state.m_objectives[i];
+        visitor.display_asserts(out, hard, m_pp_neat);
+        for (unsigned i = 0; i < objectives.size(); ++i) {
+            objective const& obj = objectives[i];
             switch(obj.m_type) {
             case O_MAXIMIZE: 
                 out << "(maximize ";
-                PP(obj.m_term);
+                ast_smt2_pp(out, obj.m_term, env);
                 out << ")\n";
                 break;
             case O_MINIMIZE:
                 out << "(minimize ";
-                PP(obj.m_term);
+                ast_smt2_pp(out, obj.m_term, env);
                 out << ")\n";
                 break;
             case O_MAXSMT: 
                 for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
                     out << "(assert-soft ";
-                    PP(obj.m_terms[j]);
+                    ast_smt2_pp(out, obj.m_terms[j], env);
                     rational w = obj.m_weights[j];
-                    if (w.is_int()) {
-                        out << " :weight " << w;
-                    }
-                    else {
-                        out << " :dweight " << w;
-                    }
+                    
+                    w.display_decimal(out << " :weight ", 3, true);
                     if (obj.m_id != symbol::null) {
-                        out << " :id " << obj.m_id;
+                        if (is_smt2_quoted_symbol(obj.m_id)) {
+                            out << " :id " << mk_smt2_quoted_symbol(obj.m_id);
+                        }
+                        else {
+                            out << " :id " << obj.m_id;
+                        }
                     }
                     out << ")\n";
                 }

src/opt/opt_context.h

@@ -175,6 +175,8 @@ namespace opt {
         unsigned add_objective(app* t, bool is_max);
         void add_hard_constraint(expr* f);
         
+        void get_hard_constraints(expr_ref_vector& hard);
+        expr_ref get_objective(unsigned i);
 
         virtual void push();
         virtual void pop(unsigned n);
@@ -208,7 +210,7 @@ namespace opt {
         std::string to_string() const;
 
 
-        virtual unsigned num_objectives() { return m_objectives.size(); }
+        virtual unsigned num_objectives() { return m_scoped_state.m_objectives.size(); }       
         virtual expr_ref mk_gt(unsigned i, model_ref& model);
         virtual expr_ref mk_ge(unsigned i, model_ref& model);
         virtual expr_ref mk_le(unsigned i, model_ref& model);
@@ -284,6 +286,9 @@ namespace opt {
         void display_objective(std::ostream& out, objective const& obj) const;
         void display_bounds(std::ostream& out, bounds_t const& b) const;
 
+        std::string to_string(expr_ref_vector const& hard, vector<objective> const& objectives) const;
+        std::string to_string_internal() const;
+
 
         void validate_lex();
 

src/opt/opt_sls_solver.h

@@ -90,19 +90,6 @@ namespace opt {
         virtual void get_labels(svector<symbol> & r) {
             m_solver->get_labels(r);
         }
-        virtual void set_cancel(bool f) {
-            m_solver->set_cancel(f);
-            m_pb2bv.set_cancel(f);
-            #pragma omp critical (sls_solver)
-            {
-                if (m_bvsls) {
-                    m_bvsls->set_cancel(f);
-                }
-                if (m_pbsls) {
-                    m_pbsls->set_cancel(f);
-                }
-            }
-        }
         virtual void set_progress_callback(progress_callback * callback) {
             m_solver->set_progress_callback(callback);
         }
@@ -203,14 +190,11 @@ namespace opt {
         }
 
         void pbsls_opt(model_ref& mdl) {
-            #pragma omp critical (sls_solver)
-            {
-                if (m_pbsls) {
-                    m_pbsls->reset();
-                }
-                else {
-                    m_pbsls = alloc(smt::pb_sls, m);
-                }
+            if (m_pbsls) {
+                m_pbsls->reset();
+            }
+            else {
+                m_pbsls = alloc(smt::pb_sls, m);
             }
             m_pbsls->set_model(mdl);
             m_pbsls->updt_params(m_params);
@@ -226,10 +210,7 @@ namespace opt {
         }
 
         void bvsls_opt(model_ref& mdl) {
-            #pragma omp critical (sls_solver)
-            {
-                m_bvsls = alloc(bvsls_opt_engine, m, m_params);
-            }
+            m_bvsls = alloc(bvsls_opt_engine, m, m_params);            
             assertions2sls();
             expr_ref objective = soft2bv(m_soft, m_weights);
             TRACE("opt", tout << objective << "\n";);

src/smt/smt_consequences.cpp

@@ -373,7 +373,7 @@ namespace smt {
             expr* n = vars[i];
             bool neg = m_manager.is_not(n, n);
             if (b_internalized(n)) {
-                lits.insert(literal(get_bool_var(n), !neg).index());
+                lits.insert(literal(get_bool_var(n), neg).index());
             }
         }
         while (!lits.empty()) {

src/smt/smt_internalizer.cpp

@@ -1281,7 +1281,7 @@ namespace smt {
        The deletion event handler is ignored if binary clause optimization is applicable.
     */
     clause * context::mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k, clause_del_eh * del_eh) {
-        TRACE("mk_clause", tout << "creating clause:\n"; display_literals(tout, num_lits, lits); tout << "\n";);
+        TRACE("mk_clause", tout << "creating clause:\n"; display_literals_verbose(tout, num_lits, lits); tout << "\n";);
         switch (k) {
         case CLS_AUX: {
             literal_buffer simp_lits;

src/smt/smt_kernel.cpp

@@ -222,6 +222,12 @@ namespace smt {
         m_imp->assert_expr(e);
     }
 
+    void kernel::assert_expr(expr_ref_vector const& es) {
+        for (unsigned i = 0; i < es.size(); ++i) {
+            m_imp->assert_expr(es[i]);
+        }
+    }
+
     void kernel::assert_expr(expr * e, proof * pr) {
         m_imp->assert_expr(e, pr);
     }

src/smt/smt_kernel.h

@@ -70,7 +70,8 @@ namespace smt {
            This method uses the "asserted" proof as a justification for e.
         */
         void assert_expr(expr * e);
-        
+
+        void assert_expr(expr_ref_vector const& es);
         /**
            \brief Assert the given assertion with the given proof as a justification.
         */

src/smt/theory_arith_aux.h

@@ -1709,7 +1709,7 @@ namespace smt {
             SASSERT(!maintain_integrality || valid_assignment());
             SASSERT(satisfy_bounds());
         }
-        TRACE("opt", display(tout););
+        TRACE("opt_verbose", display(tout););
         return (best_efforts>0 || ctx.get_cancel_flag())?BEST_EFFORT:result;
     }
 

src/smt/theory_arith_int.h

@@ -1385,7 +1385,7 @@ namespace smt {
         m_branch_cut_counter++;
         // TODO: add giveup code
         if (m_branch_cut_counter % m_params.m_arith_branch_cut_ratio == 0) {
-            TRACE("opt", display(tout););
+            TRACE("opt_verbose", display(tout););
             move_non_base_vars_to_bounds();
             if (!make_feasible()) {
                 TRACE("arith_int", tout << "failed to move variables to bounds.\n";);

src/smt/theory_arith_nl.h

@@ -704,8 +704,8 @@ namespace smt {
         bool bounded      = false;
         unsigned n        = 0;
         numeral range;
-        for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
-            theory_var v = m_nl_monomials[i];
+        for (unsigned j = 0; j < m_nl_monomials.size(); ++j) {
+            theory_var v = m_nl_monomials[j];
             if (is_real(v))
                 continue;
             bool computed_epsilon = false;
@@ -2336,8 +2336,8 @@ namespace smt {
     bool theory_arith<Ext>::max_min_nl_vars() {
         var_set             already_found;
         svector<theory_var> vars;
-        for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
-            theory_var v = m_nl_monomials[i];
+        for (unsigned j = 0; j < m_nl_monomials.size(); ++j) {
+            theory_var v = m_nl_monomials[j];
             mark_var(v, vars, already_found);
             expr * n     = var2expr(v);
             SASSERT(is_pure_monomial(n));

src/smt/theory_pb.cpp

@@ -321,7 +321,8 @@ namespace smt {
                 if (m_simplex.upper_valid(v)) {
                     m_simplex.get_upper(v, last_bound);
                     if (m_mpq_inf_mgr.gt(bound, last_bound)) {
-                        literal lit = m_explain_upper.get(v, null_literal);
+                        literal lit = m_explain_upper.get(v, null_literal);                        
+                        TRACE("pb", tout << ~lit << " " << ~explain << "\n";);
                         get_context().mk_clause(~lit, ~explain, justify(~lit, ~explain));
                         return false;
                     }
@@ -342,6 +343,7 @@ namespace smt {
                     m_simplex.get_lower(v, last_bound);
                     if (m_mpq_inf_mgr.gt(last_bound, bound)) {
                         literal lit = m_explain_lower.get(v, null_literal);
+                        TRACE("pb", tout << ~lit << " " << ~explain << "\n";);
                         get_context().mk_clause(~lit, ~explain, justify(~lit, ~explain));
                         return false;
                     }
@@ -405,6 +407,7 @@ namespace smt {
         if (proofs_enabled()) {                                         
             js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
         }
+        TRACE("pb", tout << lits << "\n";);
         ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
 
         return false;
@@ -515,11 +518,10 @@ namespace smt {
                 ++log;
                 n *= 2;
             }
-            unsigned th = args.size()*log; // 10*
+            unsigned th = args.size()*log; 
             c->m_compilation_threshold = th;
-            IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threhshold to " << th << ")\n";);
+            IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threshold to " << th << ")\n";);
             TRACE("pb", tout << "compilation threshold: " << th << "\n";);
-            //compile_ineq(*c);
         }
         else {
             c->m_compilation_threshold = UINT_MAX;
@@ -1247,9 +1249,9 @@ namespace smt {
         literal_vector in;
         for (unsigned i = 0; i < num_args; ++i) {
             rational n = c.coeff(i);
-            lbool val = ctx.get_assignment(c.lit()); 
-            if (val != l_undef  && 
-                ctx.get_assign_level(thl) == ctx.get_base_level()) {
+            literal lit = c.lit(i);
+            lbool val = ctx.get_assignment(lit); 
+            if (val != l_undef  && ctx.get_assign_level(lit) == ctx.get_base_level()) {
                 if (val == l_true) {
                     unsigned m = n.get_unsigned();
                     if (k < m) {
@@ -1264,38 +1266,35 @@ namespace smt {
                 n -= rational::one();
             }
         }
+        
+        TRACE("pb", tout << in << " >= " << k << "\n";);
 
-        unsigned num_compiled_vars, num_compiled_clauses;
+
+        psort_expr ps(ctx, *this);
+        psort_nw<psort_expr> sortnw(ps);
+        sortnw.m_stats.reset();
 
         if (ctx.get_assignment(thl) == l_true  && 
             ctx.get_assign_level(thl) == ctx.get_base_level()) {
-            psort_expr ps(ctx, *this);
-            psort_nw<psort_expr> sortnw(ps);
-            sortnw.m_stats.reset();
             at_least_k = sortnw.ge(false, k, in.size(), in.c_ptr());            
+            TRACE("pb", tout << ~thl << " " << at_least_k << "\n";);
             ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k));
-            num_compiled_vars = sortnw.m_stats.m_num_compiled_vars;
-            num_compiled_clauses = sortnw.m_stats.m_num_compiled_clauses;
         }
         else {
-            psort_expr ps(ctx, *this);
-            psort_nw<psort_expr> sortnw(ps);
-            sortnw.m_stats.reset();
             literal at_least_k = sortnw.ge(true, k, in.size(), in.c_ptr());
+            TRACE("pb", tout << ~thl << " " << at_least_k << "\n";);
             ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k));
             ctx.mk_clause(~at_least_k, thl, justify(thl, ~at_least_k));
-            num_compiled_vars = sortnw.m_stats.m_num_compiled_vars;
-            num_compiled_clauses = sortnw.m_stats.m_num_compiled_clauses;
         }
-        m_stats.m_num_compiled_vars += num_compiled_vars;
-        m_stats.m_num_compiled_clauses += num_compiled_clauses;
+        m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars;
+        m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses;
+
         IF_VERBOSE(1, verbose_stream() 
                    << "(smt.pb compile sorting network bound: " 
                    << k << " literals: " << in.size() 
                    << " clauses: " << num_compiled_clauses 
                    << " vars: " << num_compiled_vars << ")\n";);
 
-        TRACE("pb", tout << thl << "\n";);
         // auxiliary clauses get removed when popping scopes.
         // we have to recompile the circuit after back-tracking.
         c.m_compiled = l_false;
@@ -1305,7 +1304,6 @@ namespace smt {
 
 
     void theory_pb::init_search_eh() {
-        m_to_compile.reset();
     }
 
     void theory_pb::push_scope_eh() {
@@ -1334,6 +1332,7 @@ namespace smt {
                     m_ineq_rep.erase(r_info.m_rep);
                 }
             }
+            m_to_compile.erase(c);
             dealloc(c);
         }
         m_ineqs_lim.resize(new_lim);
@@ -1459,6 +1458,7 @@ namespace smt {
         if (proofs_enabled()) {                                         
             js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
         }
+        TRACE("pb", tout << lits << "\n";);
         ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
     }
 
@@ -1765,6 +1765,7 @@ namespace smt {
             for (unsigned i = 0; i < m_ineq_literals.size(); ++i) {
                 m_ineq_literals[i].neg();
             }
+            TRACE("pb", tout << m_ineq_literals << "\n";);
             ctx.mk_clause(m_ineq_literals.size(), m_ineq_literals.c_ptr(), justify(m_ineq_literals), CLS_AUX_LEMMA, 0);
             break;
         default: {

src/tactic/arith/bv2int_rewriter.h

@@ -34,7 +34,7 @@ class bv2int_rewriter_ctx {
     
 public:
     bv2int_rewriter_ctx(ast_manager& m, params_ref const& p) : 
-        m_side_conditions(m), m_trail(m) { update_params(p); }
+        m_max_size(UINT_MAX), m_side_conditions(m), m_trail(m) { update_params(p); }
 
     void reset() { m_side_conditions.reset(); m_trail.reset(); m_power2.reset(); }
     void add_side_condition(expr* e) { m_side_conditions.push_back(e); }

src/tactic/arith/card2bv_tactic.cpp

@@ -18,500 +18,22 @@ Notes:
 --*/
 #include"tactical.h"
 #include"cooperate.h"
-#include"rewriter_def.h"
 #include"ast_smt2_pp.h"
-#include"expr_substitution.h"
 #include"card2bv_tactic.h"
-#include"pb_rewriter.h"
+#include"pb2bv_rewriter.h"
 #include"ast_util.h"
 #include"ast_pp.h"
-
-namespace pb {
-    unsigned card2bv_rewriter::get_num_bits(func_decl* f) {
-        rational r(0);
-        unsigned sz = f->get_arity();
-        for (unsigned i = 0; i < sz; ++i) {
-            r += pb.get_coeff(f, i);
-        }
-        r = r > pb.get_k(f)? r : pb.get_k(f);
-        return r.get_num_bits();
-    }
-    
-    card2bv_rewriter::card2bv_rewriter(ast_manager& m):
-        m(m),
-        au(m),
-        pb(m),
-        bv(m),
-        m_sort(*this),
-        m_lemmas(m),
-        m_trail(m)
-    {}
-
-    void card2bv_rewriter::mk_assert(func_decl * f, unsigned sz, expr * const* args, expr_ref & result, expr_ref_vector& lemmas) {
-        m_lemmas.reset();
-        SASSERT(f->get_family_id() == pb.get_family_id());
-        if (is_or(f)) {
-            result = m.mk_or(sz, args);
-        }
-        else if (is_and(f)) {
-            result = m.mk_and(sz, args);
-        }
-        else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
-            result = m_sort.eq(pb.get_k(f).get_unsigned(), sz, args);
-        }
-        else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
-            result = m_sort.le(false, pb.get_k(f).get_unsigned(), sz, args);
-        }
-        else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
-            result = m_sort.ge(false, pb.get_k(f).get_unsigned(), sz, args);
-        }
-        else {
-            br_status st = mk_shannon(f, sz, args, result);
-            if (st == BR_FAILED) {
-                mk_bv(f, sz, args, result);
-            }
-        }
-        lemmas.append(m_lemmas);
-    }
-    
-    std::ostream& card2bv_rewriter::pp(std::ostream& out, literal lit) {
-        return out << mk_ismt2_pp(lit, m);
-    }
-
-    card2bv_rewriter::literal card2bv_rewriter::trail(literal l) {
-        m_trail.push_back(l);
-        return l;
-    }
-    card2bv_rewriter::literal card2bv_rewriter::fresh() {
-        return trail(m.mk_fresh_const("sn", m.mk_bool_sort()));
-    }
-
-    void card2bv_rewriter::mk_clause(unsigned n, literal const* lits) {
-        m_lemmas.push_back(mk_or(m, n, lits));
-    }
-
-    
-    br_status card2bv_rewriter::mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
-        if (f->get_family_id() == null_family_id) {
-            if (sz == 1) {
-                // Expecting minimize/maximize.
-                func_decl_ref fd(m);
-                fd = m.mk_func_decl(f->get_name(), m.get_sort(args[0]), f->get_range());
-                result = m.mk_app(fd.get(), args[0]);
-                return BR_DONE;
-            }
-            else
-                return BR_FAILED;
-        }
-        else if (f->get_family_id() == m.get_basic_family_id()) {
-            result = m.mk_app(f, sz, args);
-            return BR_DONE;
-        }
-        else if (f->get_family_id() == pb.get_family_id()) {
-            if (is_or(f)) {
-                result = m.mk_or(sz, args);
-                return BR_DONE;
-            }
-            if (is_and(f)) {
-                result = m.mk_and(sz, args);
-                return BR_DONE;
-            }
-            if (is_atmost1(f, sz, args, result)) {
-                return BR_DONE;
-            }
-            br_status st = mk_shannon(f, sz, args, result);
-            if (st == BR_FAILED) {
-                mk_bv(f, sz, args, result);
-                return BR_DONE;
-            }
-            else {
-                return st;
-            }
-        }
-        // NSB: review
-        // we should remove this code and rely on a layer above to deal with 
-        // whatever it accomplishes. It seems to break types.
-        // 
-        else if (f->get_family_id() == au.get_family_id()) {
-            if (f->get_decl_kind() == OP_ADD) {
-                unsigned bits = 0;
-                for (unsigned i = 0; i < sz; i++) {
-                    rational val1, val2;
-                    if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) {
-                        bits += val1.get_num_bits();
-                    }
-                    else if (m.is_ite(args[i]) &&
-                             au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() &&
-                             au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) {
-                        bits++;                        
-                    }
-                    else
-                        return BR_FAILED;
-                }
-                
-                result = 0;
-                for (unsigned i = 0; i < sz; i++) {
-                    rational val1, val2;
-                    expr * q;
-                    if (au.is_int(args[i]) && au.is_numeral(args[i], val1))
-                        q = bv.mk_numeral(val1, bits);
-                    else
-                        q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits));
-                    result = (i == 0) ? q : bv.mk_bv_add(result.get(), q);
-                }                
-                return BR_DONE;
-            }
-            else 
-                return BR_FAILED;
-        }
-        else
-            return BR_FAILED;
-    }
-
-    expr_ref card2bv_rewriter::mk_atmost1(unsigned n, expr * const* xs) {
-        expr_ref_vector result(m), in(m);
-        in.append(n, xs);
-        unsigned inc_size = 4;
-        while (!in.empty()) {
-            expr_ref_vector ors(m);
-            unsigned i = 0;
-            unsigned n = in.size();
-            bool last = n <= inc_size;
-            for (; i + inc_size < n; i += inc_size) {                    
-                mk_at_most_1_small(last, inc_size, in.c_ptr() + i, result, ors);
-            }
-            if (i < n) {
-                mk_at_most_1_small(last, n - i, in.c_ptr() + i, result, ors);
-            }
-            if (last) {
-                break;
-            }
-            in.reset();
-            in.append(ors);
-        }
-        return mk_and(result);
-    }
-
-    void card2bv_rewriter::mk_at_most_1_small(bool last, unsigned n, literal const* xs, expr_ref_vector& result, expr_ref_vector& ors) {
-        if (!last) {
-            ors.push_back(m.mk_or(n, xs));
-        }
-        for (unsigned i = 0; i < n; ++i) {
-            for (unsigned j = i + 1; j < n; ++j) {
-                result.push_back(m.mk_not(m.mk_and(xs[i], xs[j])));
-            }
-        }
-    }
-
-    bool card2bv_rewriter::is_atmost1(func_decl* f, unsigned sz, expr * const* args, expr_ref& result) {
-        switch (f->get_decl_kind()) {
-        case OP_AT_MOST_K:            
-        case OP_PB_LE: 
-            if (pb.get_k(f).is_one() && pb.has_unit_coefficients(f)) {
-                result = mk_atmost1(sz, args);
-                return true;
-            }
-            return false;
-        case OP_AT_LEAST_K:
-        case OP_PB_GE: 
-            if (pb.get_k(f) == rational(sz-1) && pb.has_unit_coefficients(f)) {
-                expr_ref_vector nargs(m);
-                for (unsigned i = 0; i < sz; ++i) {
-                    nargs.push_back(mk_not(args[i]));
-                }
-                result = mk_atmost1(nargs.size(), nargs.c_ptr());
-                return true;
-            }
-            return false;
-        case OP_PB_EQ:
-            return false;
-        default:
-            UNREACHABLE();
-            return false;
-        }        
-    }
-
-    bool card2bv_rewriter::is_or(func_decl* f) {
-        switch (f->get_decl_kind()) {
-        case OP_AT_MOST_K:
-        case OP_PB_LE:
-            return false;
-        case OP_AT_LEAST_K:
-        case OP_PB_GE: 
-            return pb.get_k(f).is_one();
-        case OP_PB_EQ:
-            return false;
-        default:
-            UNREACHABLE();
-            return false;
-        }
-    }
-
-    bool card2bv_rewriter::is_and(func_decl* f) {
-        return false;
-    }
-
-    void card2bv_rewriter::mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
-        expr_ref zero(m), a(m), b(m);
-        expr_ref_vector es(m);
-        unsigned bw = get_num_bits(f);        
-        zero = bv.mk_numeral(rational(0), bw);
-        for (unsigned i = 0; i < sz; ++i) {
-            es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero));
-        }
-        switch (es.size()) {
-        case 0:  a = zero; break;
-        case 1:  a = es[0].get(); break;
-        default:
-            a = es[0].get();
-            for (unsigned i = 1; i < es.size(); ++i) {
-                a = bv.mk_bv_add(a, es[i].get());
-            }
-            break;
-        }
-        b = bv.mk_numeral(pb.get_k(f), bw);
-        
-        switch (f->get_decl_kind()) {
-        case OP_AT_MOST_K:
-        case OP_PB_LE:
-            UNREACHABLE();
-            result = bv.mk_ule(a, b);
-            break;
-        case OP_AT_LEAST_K:
-            UNREACHABLE();
-        case OP_PB_GE:
-            result = bv.mk_ule(b, a);
-            break;
-        case OP_PB_EQ:
-            result = m.mk_eq(a, b);
-            break;
-        default:
-            UNREACHABLE();
-        }
-        TRACE("card2bv", tout << result << "\n";);
-    }
-
-    struct argc_t {
-        expr*    m_arg;
-        rational m_coeff;
-        argc_t():m_arg(0), m_coeff(0) {}
-        argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {}
-    };
-    struct argc_gt {
-        bool operator()(argc_t const& a, argc_t const& b) const {
-            return a.m_coeff > b.m_coeff;
-        }
-    };
-    struct argc_entry {
-        unsigned m_index;
-        rational m_k;
-        expr*    m_value;
-        argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {}
-        argc_entry():m_index(0), m_k(0), m_value(0) {}
-
-        struct eq {
-            bool operator()(argc_entry const& a, argc_entry const& b) const {
-                return a.m_index == b.m_index && a.m_k == b.m_k;
-            }
-        };
-        struct hash {
-            unsigned operator()(argc_entry const& a) const {
-                return a.m_index ^ a.m_k.hash();
-            }
-        };
-    };
-    typedef hashtable<argc_entry, argc_entry::hash, argc_entry::eq> argc_cache;
-    
-    br_status card2bv_rewriter::mk_shannon(
-        func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
-
-        unsigned max_clauses = sz*10;
-        vector<argc_t> argcs;
-        for (unsigned i = 0; i < sz; ++i) {
-            argcs.push_back(argc_t(args[i], pb.get_coeff(f, i)));
-        }
-        std::sort(argcs.begin(), argcs.end(), argc_gt());
-        DEBUG_CODE(
-            for (unsigned i = 0; i + 1 < sz; ++i) {
-                SASSERT(argcs[i].m_coeff >= argcs[i+1].m_coeff);
-            }
-            );
-        result = m.mk_app(f, sz, args);
-        TRACE("card2bv", tout << result << "\n";);
-        argc_cache cache;
-        expr_ref_vector trail(m);
-        vector<rational> todo_k;
-        unsigned_vector  todo_i;
-        todo_k.push_back(pb.get_k(f));
-        todo_i.push_back(0);
-        decl_kind kind = f->get_decl_kind();
-        argc_entry entry1;
-        while (!todo_i.empty()) {
-            SASSERT(todo_i.size() == todo_k.size());
-            if (cache.size() > max_clauses) {
-                return BR_FAILED;
-            }
-            unsigned i = todo_i.back();
-            rational k = todo_k.back();
-            argc_entry entry(i, k);
-            if (cache.contains(entry)) {
-                todo_i.pop_back();
-                todo_k.pop_back();
-                continue;
-            }
-            SASSERT(i < sz);
-            SASSERT(!k.is_neg());
-            rational const& coeff = argcs[i].m_coeff;
-            expr* arg = argcs[i].m_arg;
-            if (i + 1 == sz) {
-                switch(kind) {
-                case OP_AT_MOST_K:
-                case OP_PB_LE:
-                    if (coeff <= k) {
-                        entry.m_value = m.mk_true();
-                    }
-                    else {
-                        entry.m_value = negate(arg);
-                        trail.push_back(entry.m_value);
-                    }
-                    break;
-                case OP_AT_LEAST_K:
-                case OP_PB_GE:
-                    if (k.is_zero()) {
-                        entry.m_value = m.mk_true();
-                    }
-                    else if (coeff < k) {
-                        entry.m_value = m.mk_false();
-                    }
-                    else if (coeff.is_zero()) {
-                        entry.m_value = m.mk_true();
-                    }
-                    else {
-                        SASSERT(coeff >= k && k.is_pos());
-                        entry.m_value = arg;
-                    }
-                    break;
-                case OP_PB_EQ:
-                    if (coeff == k) {
-                        entry.m_value = arg;
-                    }
-                    else if (k.is_zero()) {
-                        entry.m_value = negate(arg);
-                        trail.push_back(entry.m_value);
-                    }
-                    else {
-                        entry.m_value = m.mk_false();
-                    }
-                    break;
-                }
-                todo_i.pop_back();
-                todo_k.pop_back();
-                cache.insert(entry);
-                continue;
-            }
-            entry.m_index++;        
-            expr* lo = 0, *hi = 0;
-            if (cache.find(entry, entry1)) {
-                lo = entry1.m_value;                
-            }
-            else {
-                todo_i.push_back(i+1);
-                todo_k.push_back(k);
-            }
-            entry.m_k -= coeff;
-            if (kind != OP_PB_EQ && !entry.m_k.is_pos()) {
-                switch (kind) {
-                case OP_AT_MOST_K:
-                case OP_PB_LE:
-                    hi = m.mk_false();
-                    break;
-                case OP_AT_LEAST_K:
-                case OP_PB_GE:
-                    hi = m.mk_true();
-                    break;
-                default:
-                    UNREACHABLE();
-                }
-            }
-            else if (cache.find(entry, entry1)) {
-                hi = entry1.m_value;
-            }
-            else {
-                todo_i.push_back(i+1);
-                todo_k.push_back(entry.m_k);
-            }
-            if (hi && lo) {
-                todo_i.pop_back();
-                todo_k.pop_back();
-                entry.m_index = i;
-                entry.m_k = k;
-                entry.m_value = mk_ite(arg, hi, lo);
-                trail.push_back(entry.m_value);
-                cache.insert(entry);
-            }
-        }        
-        argc_entry entry(0, pb.get_k(f));
-        VERIFY(cache.find(entry, entry));
-        result = entry.m_value;
-        TRACE("card2bv", tout << result << "\n";);
-        return BR_DONE;
-    }
-
-    expr* card2bv_rewriter::negate(expr* e) {
-        if (m.is_not(e, e)) return e;
-        return m.mk_not(e);
-    }
-
-    expr* card2bv_rewriter::mk_ite(expr* c, expr* hi, expr* lo) {
-        while (m.is_not(c, c)) {
-            std::swap(hi, lo);
-        }
-        if (hi == lo) return hi;
-        if (m.is_true(hi) && m.is_false(lo)) return c;
-        if (m.is_false(hi) && m.is_true(lo)) return negate(c);
-        if (m.is_true(hi)) return m.mk_or(c, lo);
-        if (m.is_false(lo)) return m.mk_and(c, hi);
-        if (m.is_false(hi)) return m.mk_and(negate(c), lo);
-        if (m.is_true(lo)) return m.mk_implies(c, hi);
-        return m.mk_ite(c, hi, lo);
-    }
-
-    void card_pb_rewriter::rewrite(expr* e, expr_ref& result) {
-        if (pb.is_eq(e)) {
-            app* a = to_app(e);
-            ast_manager& m = m_lemmas.get_manager();
-            unsigned sz = a->get_num_args();
-            expr_ref_vector args(m);
-            expr_ref tmp(m);
-            for (unsigned i = 0; i < sz; ++i) {
-                (*this)(a->get_arg(i), tmp);
-                args.push_back(tmp);
-            }
-            m_cfg.m_r.mk_assert(a->get_decl(), sz, args.c_ptr(), result, m_lemmas);
-        }
-        else {
-            (*this)(e, result);    
-        }
-    }
-
-};
-
-template class rewriter_tpl<pb::card2bv_rewriter_cfg>;
-
+#include"filter_model_converter.h"
 
 class card2bv_tactic : public tactic {
     ast_manager &              m;
     params_ref                 m_params;
-    th_rewriter                m_rw1;
-    pb::card_pb_rewriter       m_rw2;
     
 public:
 
     card2bv_tactic(ast_manager & m, params_ref const & p):
         m(m),
-        m_params(p),
-        m_rw1(m),
-        m_rw2(m) {
+        m_params(p) {
     }
 
     virtual tactic * translate(ast_manager & m) {
@@ -538,9 +60,8 @@ public:
         SASSERT(g->is_well_sorted());
         mc = 0; pc = 0; core = 0; result.reset();
         tactic_report report("card2bv", *g);
-        m_rw1.reset(); 
-        m_rw2.reset(); 
-        m_rw2.lemmas().reset();
+        th_rewriter rw1(m, m_params);
+        pb2bv_rewriter rw2(m, m_params);
         
         if (g->inconsistent()) {
             result.push_back(g.get());
@@ -550,18 +71,28 @@ public:
         expr_ref new_f1(m), new_f2(m);
         proof_ref new_pr1(m), new_pr2(m);
         for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {
-            m_rw1(g->form(idx), new_f1, new_pr1);
+            rw1(g->form(idx), new_f1, new_pr1);
             TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;);
-            m_rw2.rewrite(new_f1, new_f2);
+            rw2(new_f1, new_f2, new_pr2);
             if (m.proofs_enabled()) {
                 new_pr1  = m.mk_modus_ponens(g->pr(idx), new_pr1);
-                new_pr2  = m.mk_rewrite(new_f1, new_f2);
                 new_pr1  = m.mk_modus_ponens(new_pr1, new_pr2);
             }
             g->update(idx, new_f2, new_pr1, g->dep(idx));
         }
-        for (unsigned i = 0; i < m_rw2.lemmas().size(); ++i) {
-            g->assert_expr(m_rw2.lemmas()[i].get());
+        expr_ref_vector fmls(m);
+        rw2.flush_side_constraints(fmls);
+        for (unsigned i = 0; !g->inconsistent() && i < fmls.size(); ++i) {
+            g->assert_expr(fmls[i].get());
+        }
+        
+        func_decl_ref_vector const& fns = rw2.fresh_constants();
+        if (!fns.empty()) {
+            filter_model_converter* filter = alloc(filter_model_converter, m);
+            for (unsigned i = 0; i < fns.size(); ++i) {
+                filter->insert(fns[i]);
+            }
+            mc = filter;
         }
 
         g->inc_depth();

src/tactic/arith/pb2bv_tactic.cpp

@@ -29,10 +29,11 @@ Notes:
 #include"filter_model_converter.h"
 #include"pb2bv_model_converter.h"
 #include"pb2bv_tactic.h"
+#include"ast_pp.h"
 
 class pb2bv_tactic : public tactic {
 public:
-    struct non_pb {};
+    struct non_pb { expr* e; non_pb(expr* e) : e(e) {}};
 
     struct only_01_visitor {
         typedef rational numeral;
@@ -48,7 +49,7 @@ public:
     
         void throw_non_pb(expr * n) {
             TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";);
-            throw non_pb();
+            throw non_pb(n);
         }
     
         void operator()(var * n) { 
@@ -575,7 +576,7 @@ private:
     
         void throw_non_pb(expr * n) {        
             TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";);
-            throw non_pb();
+            throw non_pb(n);
         }
 
         // check if polynomial is encoding 
@@ -910,8 +911,8 @@ private:
             try {
                 quick_pb_check(g);
             }
-            catch (non_pb) {
-                throw tactic_exception("goal is in a fragment unsupported by pb2bv");
+            catch (non_pb& p) {
+                throw_tactic(p.e);
             }
                         
             unsigned size = g->size();
@@ -940,8 +941,8 @@ private:
                     new_exprs.push_back(new_f);
                 }                
             }
-            catch (non_pb) {
-                throw tactic_exception("goal is in a fragment unsupported by pb2bv");
+            catch (non_pb& p) {
+                throw_tactic(p.e);
             }
 
             for (unsigned idx = 0; idx < size; idx++)
@@ -966,6 +967,12 @@ private:
             TRACE("pb2bv", g->display(tout););
             SASSERT(g->is_well_sorted());
         }
+
+        void throw_tactic(expr* e) {
+            std::stringstream strm;
+            strm << "goal is in a fragment unsupported by pb2bv. Offending expression: " << mk_pp(e, m);
+            throw tactic_exception(strm.str().c_str());
+        }
     };
 
     imp *      m_imp;

src/tactic/bv/dt2bv_tactic.cpp

@@ -29,7 +29,7 @@ Revision History:
 #include "extension_model_converter.h"
 #include "var_subst.h"
 #include "ast_util.h"
-#include "fd_rewriter.h"
+#include "enum2bv_rewriter.h"
 
 
 class dt2bv_tactic : public tactic {
@@ -40,7 +40,6 @@ class dt2bv_tactic : public tactic {
     bv_util       m_bv;
     obj_hashtable<sort> m_fd_sorts;
     obj_hashtable<sort> m_non_fd_sorts;
-    obj_map<func_decl, func_decl*>*     m_translate;
     
 
     bool is_fd(expr* a) { return is_fd(get_sort(a)); }
@@ -99,11 +98,11 @@ class dt2bv_tactic : public tactic {
     sort_pred m_is_fd;
 public:
 
-    dt2bv_tactic(ast_manager& m, params_ref const& p, obj_map<func_decl, func_decl*>* tr): 
-        m(m), m_params(p), m_dt(m), m_bv(m), m_translate(tr), m_is_fd(*this) {}
+    dt2bv_tactic(ast_manager& m, params_ref const& p): 
+        m(m), m_params(p), m_dt(m), m_bv(m), m_is_fd(*this) {}
     
     virtual tactic * translate(ast_manager & m) {
-        return alloc(dt2bv_tactic, m, m_params, 0);
+        return alloc(dt2bv_tactic, m, m_params);
     }
 
     virtual void updt_params(params_ref const & p) {
@@ -133,7 +132,7 @@ public:
         if (!m_fd_sorts.empty()) {
             ref<extension_model_converter> ext = alloc(extension_model_converter, m);
             ref<filter_model_converter> filter = alloc(filter_model_converter, m);
-            fd_rewriter rw(m, m_params);
+            enum2bv_rewriter rw(m, m_params);
             rw.set_is_fd(&m_is_fd);            
             expr_ref   new_curr(m);
             proof_ref  new_pr(m);
@@ -154,9 +153,6 @@ public:
                 obj_map<func_decl, func_decl*>::iterator it = rw.enum2bv().begin(), end = rw.enum2bv().end();
                 for (; it != end; ++it) {
                     filter->insert(it->m_value);
-                    if (m_translate) {
-                        m_translate->insert(it->m_key, it->m_value);
-                    }
                 }
             }
             {
@@ -182,6 +178,6 @@ public:
 
 };
 
-tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p, obj_map<func_decl, func_decl*>* tr) {
-    return alloc(dt2bv_tactic, m, p, tr);
+tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p) {
+    return alloc(dt2bv_tactic, m, p);
 }

src/tactic/bv/dt2bv_tactic.h

@@ -24,7 +24,7 @@ Revision History:
 class ast_manager;
 class tactic;
 
-tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref(), obj_map<func_decl, func_decl*>* tr = 0);
+tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref());
 
 /*
     ADD_TACTIC("dt2bv", "eliminate finite domain data-types. Replace by bit-vectors.", "mk_dt2bv_tactic(m, p)")

src/tactic/portfolio/bounded_int2bv_solver.cpp

@@ -0,0 +1,296 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    bounded_int2bv_solver.cpp
+
+Abstract:
+
+    This solver identifies bounded integers and rewrites them to bit-vectors.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-10-23
+
+Notes:
+   
+--*/
+
+#include "bounded_int2bv_solver.h"
+#include "solver_na2as.h"
+#include "tactic.h"
+#include "pb2bv_rewriter.h"
+#include "filter_model_converter.h"
+#include "extension_model_converter.h"
+#include "ast_pp.h"
+#include "model_smt2_pp.h"
+#include "bound_manager.h"
+#include "bv2int_rewriter.h"
+#include "expr_safe_replace.h"
+#include "bv_decl_plugin.h"
+#include "arith_decl_plugin.h"
+
+class bounded_int2bv_solver : public solver_na2as {
+    ast_manager&     m;
+    params_ref       m_params;
+    bv_util          m_bv;
+    arith_util       m_arith;
+    expr_ref_vector  m_assertions;
+    ref<solver>      m_solver;
+    ptr_vector<bound_manager> m_bounds;
+    func_decl_ref_vector  m_bv_fns;
+    func_decl_ref_vector  m_int_fns;
+    unsigned_vector       m_bv_fns_lim;
+    obj_map<func_decl, func_decl*> m_int2bv;
+    obj_map<func_decl, func_decl*> m_bv2int;
+    obj_map<func_decl, rational>   m_bv2offset;
+    bv2int_rewriter_ctx   m_rewriter_ctx;
+    bv2int_rewriter_star  m_rewriter;
+
+public:
+
+    bounded_int2bv_solver(ast_manager& m, params_ref const& p, solver* s):
+        solver_na2as(m),
+        m(m),
+        m_params(p),
+        m_bv(m),
+        m_arith(m),
+        m_assertions(m),
+        m_solver(s),
+        m_bv_fns(m),
+        m_int_fns(m),
+        m_rewriter_ctx(m, p),
+        m_rewriter(m, m_rewriter_ctx)
+    {
+        m_bounds.push_back(alloc(bound_manager, m));
+    }
+
+    virtual ~bounded_int2bv_solver() {
+        while (!m_bounds.empty()) {
+            dealloc(m_bounds.back());
+            m_bounds.pop_back();
+        }
+    }
+
+    virtual solver* translate(ast_manager& m, params_ref const& p) {
+        return alloc(bounded_int2bv_solver, m, p, m_solver->translate(m, p));
+    }
+    
+    virtual void assert_expr(expr * t) {
+        m_assertions.push_back(t);
+    }
+
+    virtual void push_core() {
+        flush_assertions();
+        m_solver->push();
+        m_bv_fns_lim.push_back(m_bv_fns.size());
+        m_bounds.push_back(alloc(bound_manager, m));
+    }
+
+    virtual void pop_core(unsigned n) {
+        m_assertions.reset();        
+        m_solver->pop(n);
+
+        if (n > 0) {
+            SASSERT(n <= m_bv_fns_lim.size());
+            unsigned new_sz = m_bv_fns_lim.size() - n;
+            unsigned lim = m_bv_fns_lim[new_sz];
+            for (unsigned i = m_int_fns.size(); i > lim; ) {
+                --i;
+                m_int2bv.erase(m_int_fns[i].get());
+                m_bv2int.erase(m_bv_fns[i].get());
+                m_bv2offset.erase(m_bv_fns[i].get());
+            }
+            m_bv_fns_lim.resize(new_sz);
+            m_bv_fns.resize(lim);
+            m_int_fns.resize(lim);
+        }
+
+        while (n > 0) {
+            dealloc(m_bounds.back());
+            m_bounds.pop_back();            
+            --n;
+        }
+    }
+
+    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
+        flush_assertions();
+        return m_solver->check_sat(num_assumptions, assumptions);
+    }
+
+    virtual void updt_params(params_ref const & p) { m_solver->updt_params(p);  }
+    virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }    
+    virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
+    virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback);  }
+    virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); }
+    virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
+    virtual void get_model(model_ref & mdl) { 
+        m_solver->get_model(mdl);
+        if (mdl) {
+            extend_model(mdl);
+            filter_model(mdl);            
+        }
+    } 
+    virtual proof * get_proof() { return m_solver->get_proof(); }
+    virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
+    virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
+    virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
+    virtual ast_manager& get_manager() const { return m;  }
+    virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }    
+    virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { 
+        flush_assertions();
+        expr_ref_vector bvars(m);
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            expr* v = vars[i];
+            func_decl* f;
+            rational offset;
+            if (is_app(v) && is_uninterp_const(v) && m_int2bv.find(to_app(v)->get_decl(), f)) {
+                bvars.push_back(m.mk_const(f));
+            }
+            else {
+                bvars.push_back(v);
+            }
+        }
+        lbool r = m_solver->get_consequences(asms, bvars, consequences);
+
+        // translate bit-vector consequences back to integer values
+        for (unsigned i = 0; i < consequences.size(); ++i) {
+            expr* a, *b, *u, *v;
+            func_decl* f;
+            rational num;
+            unsigned bvsize;
+            rational offset;
+            VERIFY(m.is_implies(consequences[i].get(), a, b));
+            if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_bv2int.find(to_app(u)->get_decl(), f) && m_bv.is_numeral(v, num, bvsize)) {
+                SASSERT(num.is_unsigned());
+                expr_ref head(m);
+                VERIFY (m_bv2offset.find(to_app(u)->get_decl(), offset));
+                // f + offset == num
+                // f == num - offset
+                head = m.mk_eq(m.mk_const(f), m_arith.mk_numeral(num + offset, true));
+                consequences[i] = m.mk_implies(a, head);
+            }
+        }
+        return r;
+
+    }
+
+private:
+
+    void filter_model(model_ref& mdl) const {
+        if (m_bv_fns.empty()) {
+            return;
+        }
+        filter_model_converter filter(m);
+        func_decl_ref_vector const& fns = m_bv_fns;
+        for (unsigned i = 0; i < m_bv_fns.size(); ++i) {
+            filter.insert(m_bv_fns[i]);
+        }
+        filter(mdl, 0);
+    }
+
+    void extend_model(model_ref& mdl) {
+        extension_model_converter ext(m);
+        obj_map<func_decl, func_decl*>::iterator it = m_int2bv.begin(), end = m_int2bv.end();
+        for (; it != end; ++it) {
+            rational offset;
+            VERIFY (m_bv2offset.find(it->m_value, offset));
+            expr_ref value(m_bv.mk_bv2int(m.mk_const(it->m_value)), m);
+            if (!offset.is_zero()) {
+                value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true));
+            }
+            TRACE("int2bv", tout << mk_pp(it->m_key, m) << " " << value << "\n";);
+            ext.insert(it->m_key, value);            
+        }
+        ext(mdl, 0);
+    }
+
+    void accumulate_sub(expr_safe_replace& sub) {
+        for (unsigned i = 0; i < m_bounds.size(); ++i) {
+            accumulate_sub(sub, *m_bounds[i]);
+        }
+    }
+
+    void accumulate_sub(expr_safe_replace& sub, bound_manager& bm) {
+        bound_manager::iterator it = bm.begin(), end = bm.end();
+        for (; it != end; ++it) {
+            expr* e = *it;
+            rational lo, hi;
+            bool s1, s2;
+            SASSERT(is_uninterp_const(e));
+            func_decl* f = to_app(e)->get_decl();
+
+            if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2) {
+                func_decl* fbv;
+                rational offset;
+                if (!m_int2bv.find(f, fbv)) {                    
+                    rational n = hi - lo + rational::one();
+                    unsigned num_bits = get_num_bits(n);
+                    expr_ref b(m);
+                    b = m.mk_fresh_const("b", m_bv.mk_sort(num_bits));
+                    fbv = to_app(b)->get_decl();
+                    offset = lo;
+                    m_int2bv.insert(f, fbv);
+                    m_bv2int.insert(fbv, f);
+                    m_bv2offset.insert(fbv, offset);
+                    m_bv_fns.push_back(fbv);
+                    m_int_fns.push_back(f);
+                    unsigned shift;
+                    if (!offset.is_zero() && !n.is_power_of_two(shift)) {
+                        m_assertions.push_back(m_bv.mk_ule(b, m_bv.mk_numeral(n-rational::one(), num_bits)));
+                    }
+                }
+                else {
+                    VERIFY(m_bv2offset.find(fbv, offset));
+                }
+                expr_ref t(m.mk_const(fbv), m);
+                t = m_bv.mk_bv2int(t);
+                if (!offset.is_zero()) {
+                    t = m_arith.mk_add(t, m_arith.mk_numeral(lo, true));
+                }
+                sub.insert(e, t);
+            }
+        }
+    }
+
+    unsigned get_num_bits(rational const& k) {
+        SASSERT(!k.is_neg());
+        SASSERT(k.is_int());
+        rational two(2);
+        rational bound(1);
+        unsigned num_bits = 1;
+        while (bound <= k) {
+            ++num_bits;
+            bound *= two;
+        }
+        return num_bits;
+    }
+
+    void flush_assertions() {
+        bound_manager& bm = *m_bounds.back();
+        for (unsigned i = 0; i < m_assertions.size(); ++i) {
+            bm(m_assertions[i].get());
+        }
+        expr_safe_replace sub(m);
+        accumulate_sub(sub);        
+        proof_ref proof(m);
+        expr_ref fml1(m), fml2(m);
+        if (sub.empty()) {
+            m_solver->assert_expr(m_assertions);
+        }
+        else {
+            for (unsigned i = 0; i < m_assertions.size(); ++i) {
+                sub(m_assertions[i].get(), fml1);            
+                m_rewriter(fml1, fml2, proof);
+                m_solver->assert_expr(fml2);
+                TRACE("int2bv", tout << fml2 << "\n";);
+            }
+        }
+        m_assertions.reset();
+    }
+};
+
+solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s) {
+    return alloc(bounded_int2bv_solver, m, p, s);
+}

src/tactic/portfolio/bounded_int2bv_solver.h

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    bounded_int2bv_solver.h
+
+Abstract:
+
+    Finite domain solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-10-23
+
+Notes:
+   
+--*/
+#ifndef BOUNDED_INT2BV_SOLVER_H_
+#define BOUNDED_INT2BV_SOLVER_H_
+
+#include"ast.h"
+#include"params.h"
+
+class solver;
+
+solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s);
+
+#endif

src/tactic/portfolio/enum2bv_solver.cpp

@@ -0,0 +1,162 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    enum2bv_solver.cpp
+
+Abstract:
+
+    Finite domain solver.
+
+    Enumeration data-types are translated into bit-vectors, and then 
+    the incremental sat-solver is applied to the resulting assertions.    
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-10-17
+
+Notes:
+   
+--*/
+
+#include "solver_na2as.h"
+#include "tactic.h"
+#include "bv_decl_plugin.h"
+#include "datatype_decl_plugin.h"
+#include "enum2bv_rewriter.h"
+#include "extension_model_converter.h"
+#include "filter_model_converter.h"
+#include "ast_pp.h"
+#include "model_smt2_pp.h"
+#include "enum2bv_solver.h"
+
+class enum2bv_solver : public solver_na2as {
+    ast_manager&   m;
+    params_ref     m_params;
+    ref<solver>    m_solver;
+    enum2bv_rewriter    m_rewriter;
+
+public:
+
+    enum2bv_solver(ast_manager& m, params_ref const& p, solver* s):
+        solver_na2as(m),
+        m(m),
+        m_params(p),
+        m_solver(s),
+        m_rewriter(m, p)
+    {
+    }
+
+    virtual ~enum2bv_solver() {}
+
+    virtual solver* translate(ast_manager& m, params_ref const& p) {
+        return alloc(enum2bv_solver, m, p, m_solver->translate(m, p));
+    }
+    
+    virtual void assert_expr(expr * t) {
+        expr_ref tmp(t, m);
+        expr_ref_vector bounds(m);
+        proof_ref tmp_proof(m);
+        m_rewriter(t, tmp, tmp_proof);
+        m_solver->assert_expr(tmp);
+        m_rewriter.flush_side_constraints(bounds);
+        m_solver->assert_expr(bounds);
+    }
+
+    virtual void push_core() {
+        m_rewriter.push();
+        m_solver->push();
+    }
+
+    virtual void pop_core(unsigned n) {
+        m_solver->pop(n);
+        m_rewriter.pop(n);
+    }
+
+    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
+        return m_solver->check_sat(num_assumptions, assumptions);
+    }
+
+    virtual void updt_params(params_ref const & p) { m_solver->updt_params(p);  }
+    virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }    
+    virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
+    virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback);  }
+    virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); }
+    virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
+    virtual void get_model(model_ref & mdl) { 
+        m_solver->get_model(mdl);
+        if (mdl) {
+            extend_model(mdl);
+            filter_model(mdl);            
+        }
+    } 
+    virtual proof * get_proof() { return m_solver->get_proof(); }
+    virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
+    virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
+    virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
+    virtual ast_manager& get_manager() const { return m;  }
+    virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
+    
+    virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
+
+        datatype_util dt(m);
+        bv_util bv(m);
+
+        // translate enumeration constants to bit-vectors.
+        expr_ref_vector bvars(m), conseq(m);
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            func_decl* f;
+            if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) {
+                bvars.push_back(m.mk_const(f));
+            }
+            else {
+                bvars.push_back(vars[i]);
+            }
+        }
+        lbool r = m_solver->get_consequences(asms, bvars, consequences);
+        std::cout << consequences.size() << "\n";
+
+
+        // translate bit-vector consequences back to enumeration types
+        for (unsigned i = 0; i < consequences.size(); ++i) {
+            expr* a, *b, *u, *v;
+            func_decl* f;
+            rational num;
+            unsigned bvsize;
+            VERIFY(m.is_implies(consequences[i].get(), 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);
+                ptr_vector<func_decl> const& enums = *dt.get_datatype_constructors(f->get_range());
+                head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
+                consequences[i] = m.mk_implies(a, head);
+            }
+        }
+        return r;
+    }
+
+    void filter_model(model_ref& mdl) {
+        filter_model_converter filter(m);
+        obj_map<func_decl, func_decl*>::iterator it = m_rewriter.enum2bv().begin(), end = m_rewriter.enum2bv().end();
+        for (; it != end; ++it) {
+            filter.insert(it->m_value);
+        }
+        filter(mdl, 0);
+    }
+
+    void extend_model(model_ref& mdl) {
+        extension_model_converter ext(m);
+        obj_map<func_decl, expr*>::iterator it = m_rewriter.enum2def().begin(), end = m_rewriter.enum2def().end();
+        for (; it != end; ++it) {
+            ext.insert(it->m_key, it->m_value);
+            
+        }
+        ext(mdl, 0);
+    }
+
+};
+
+solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s) {
+    return alloc(enum2bv_solver, m, p, s);
+}

src/tactic/portfolio/enum2bv_solver.h

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    enum2bv_solver.h
+
+Abstract:
+
+    Finite domain solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-10-17
+
+Notes:
+   
+--*/
+#ifndef ENUM2BV_SOLVER_H_
+#define ENUM2BV_SOLVER_H_
+
+#include"ast.h"
+#include"params.h"
+
+class solver;
+
+solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s);
+
+#endif

src/tactic/portfolio/fd_solver.cpp

@@ -9,9 +9,6 @@ Abstract:
 
     Finite domain solver.
 
-    Enumeration data-types are translated into bit-vectors, and then 
-    the incremental sat-solver is applied to the resulting assertions.    
-
 Author:
 
     Nikolaj Bjorner (nbjorner) 2016-10-17
@@ -21,141 +18,16 @@ Notes:
 --*/
 
 #include "fd_solver.h"
-#include "solver_na2as.h"
 #include "tactic.h"
 #include "inc_sat_solver.h"
-#include "bv_decl_plugin.h"
-#include "datatype_decl_plugin.h"
-#include "fd_rewriter.h"
-#include "extension_model_converter.h"
-#include "filter_model_converter.h"
-#include "ast_pp.h"
-#include "model_smt2_pp.h"
-
-class fd_solver : public solver_na2as {
-    ast_manager&   m;
-    params_ref     m_params;
-    ref<solver>    m_solver;
-    fd_rewriter    m_rewriter;
-
-public:
-
-    fd_solver(ast_manager& m, params_ref const& p):
-        solver_na2as(m),
-        m(m),
-        m_params(p),
-        m_solver(mk_inc_sat_solver(m, p)),
-        m_rewriter(m, p)
-    {
-    }
-
-    virtual ~fd_solver() {}
-
-    virtual solver* translate(ast_manager& m, params_ref const& p) {
-        return alloc(fd_solver, m, p);
-    }
-    
-    virtual void assert_expr(expr * t) {
-        expr_ref tmp(t, m);
-        expr_ref_vector bounds(m);
-        proof_ref tmp_proof(m);
-        m_rewriter(t, tmp, tmp_proof);
-        m_solver->assert_expr(tmp);
-        m_rewriter.flush_side_constraints(bounds);
-        m_solver->assert_expr(bounds);
-    }
-
-    virtual void push_core() {
-        m_rewriter.push();
-        m_solver->push();
-    }
-
-    virtual void pop_core(unsigned n) {
-        m_solver->pop(n);
-        m_rewriter.pop(n);
-    }
-
-    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
-        return m_solver->check_sat(num_assumptions, assumptions);
-    }
-
-    virtual void updt_params(params_ref const & p) { m_solver->updt_params(p);  }
-    virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }    
-    virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
-    virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback);  }
-    virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); }
-    virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
-    virtual void get_model(model_ref & mdl) { 
-        m_solver->get_model(mdl);
-        if (mdl) {
-            extend_model(mdl);
-            filter_model(mdl);            
-        }
-    } 
-    virtual proof * get_proof() { return m_solver->get_proof(); }
-    virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
-    virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
-    virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
-    virtual ast_manager& get_manager() const { return m;  }
-    virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
-    
-    virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
-
-        datatype_util dt(m);
-        bv_util bv(m);
-
-        // translate enumeration constants to bit-vectors.
-        expr_ref_vector bvars(m), conseq(m);
-        for (unsigned i = 0; i < vars.size(); ++i) {
-            func_decl* f;
-            if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) {
-                bvars.push_back(m.mk_const(f));
-            }
-            else {
-                bvars.push_back(vars[i]);
-            }
-        }
-        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) {
-            expr* a, *b, *u, *v;
-            func_decl* f;
-            rational num;
-            unsigned bvsize;
-            VERIFY(m.is_implies(consequences[i].get(), 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);
-                ptr_vector<func_decl> const& enums = *dt.get_datatype_constructors(f->get_range());
-                head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
-                consequences[i] = m.mk_implies(a, head);
-            }
-        }
-        return r;
-    }
-
-    void filter_model(model_ref& mdl) {
-        filter_model_converter filter(m);
-        obj_map<func_decl, func_decl*>::iterator it = m_rewriter.enum2bv().begin(), end = m_rewriter.enum2bv().end();
-        for (; it != end; ++it) {
-            filter.insert(it->m_value);
-        }
-        filter(mdl, 0);
-    }
-
-    void extend_model(model_ref& mdl) {
-        extension_model_converter ext(m);
-        obj_map<func_decl, expr*>::iterator it = m_rewriter.enum2def().begin(), end = m_rewriter.enum2def().end();
-        for (; it != end; ++it) {
-            ext.insert(it->m_key, it->m_value);
-            
-        }
-        ext(mdl, 0);
-    }
-
-};
+#include "enum2bv_solver.h"
+#include "pb2bv_solver.h"
+#include "bounded_int2bv_solver.h"
 
 solver * mk_fd_solver(ast_manager & m, params_ref const & p) {
-    return alloc(fd_solver, m, p);
+    solver* s = mk_inc_sat_solver(m, p);
+    s = mk_enum2bv_solver(m, p, s);
+    s = mk_pb2bv_solver(m, p, s);
+    s = mk_bounded_int2bv_solver(m, p, s);
+    return s;
 }

src/tactic/portfolio/pb2bv_solver.cpp

@@ -0,0 +1,127 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    pb2bv_solver.cpp
+
+Abstract:
+
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-10-23
+
+Notes:
+   
+--*/
+
+#include "pb2bv_solver.h"
+#include "solver_na2as.h"
+#include "tactic.h"
+#include "pb2bv_rewriter.h"
+#include "filter_model_converter.h"
+#include "ast_pp.h"
+#include "model_smt2_pp.h"
+
+class pb2bv_solver : public solver_na2as {
+    ast_manager&     m;
+    params_ref       m_params;
+    expr_ref_vector  m_assertions;
+    ref<solver>      m_solver;
+    pb2bv_rewriter   m_rewriter;
+
+public:
+
+    pb2bv_solver(ast_manager& m, params_ref const& p, solver* s):
+        solver_na2as(m),
+        m(m),
+        m_params(p),
+        m_assertions(m),
+        m_solver(s),
+        m_rewriter(m, p)
+    {
+    }
+
+    virtual ~pb2bv_solver() {}
+
+    virtual solver* translate(ast_manager& m, params_ref const& p) {
+        return alloc(pb2bv_solver, m, p, m_solver->translate(m, p));
+    }
+    
+    virtual void assert_expr(expr * t) {
+        m_assertions.push_back(t);
+    }
+
+    virtual void push_core() {
+        flush_assertions();
+        m_rewriter.push();
+        m_solver->push();
+    }
+
+    virtual void pop_core(unsigned n) {
+        m_assertions.reset();
+        m_solver->pop(n);
+        m_rewriter.pop(n);
+    }
+
+    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
+        flush_assertions();
+        return m_solver->check_sat(num_assumptions, assumptions);
+    }
+
+    virtual void updt_params(params_ref const & p) { m_solver->updt_params(p);  }
+    virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }    
+    virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
+    virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback);  }
+    virtual void collect_statistics(statistics & st) const { 
+        m_rewriter.collect_statistics(st);
+        m_solver->collect_statistics(st); 
+    }
+    virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
+    virtual void get_model(model_ref & mdl) { 
+        m_solver->get_model(mdl);
+        if (mdl) {
+            filter_model(mdl);            
+        }
+    } 
+    virtual proof * get_proof() { return m_solver->get_proof(); }
+    virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
+    virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
+    virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
+    virtual ast_manager& get_manager() const { return m;  }
+    virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }    
+    virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
+        flush_assertions(); 
+        return m_solver->get_consequences(asms, vars, consequences); }
+
+    void filter_model(model_ref& mdl) {
+        if (m_rewriter.fresh_constants().empty()) {
+            return;
+        }
+        filter_model_converter filter(m);
+        func_decl_ref_vector const& fns = m_rewriter.fresh_constants();
+        for (unsigned i = 0; i < fns.size(); ++i) {
+            filter.insert(fns[i]);
+        }
+        filter(mdl, 0);
+    }
+
+private:
+    void flush_assertions() {
+        proof_ref proof(m);
+        expr_ref fml(m);
+        expr_ref_vector fmls(m);
+        for (unsigned i = 0; i < m_assertions.size(); ++i) {
+            m_rewriter(m_assertions[i].get(), fml, proof);
+            m_solver->assert_expr(fml);
+        }
+        m_rewriter.flush_side_constraints(fmls);
+        m_solver->assert_expr(fmls);
+        m_assertions.reset();
+    }
+};
+
+solver * mk_pb2bv_solver(ast_manager & m, params_ref const & p, solver* s) {
+    return alloc(pb2bv_solver, m, p, s);
+}

src/tactic/portfolio/pb2bv_solver.h

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    pb2bv_solver.h
+
+Abstract:
+
+    Pseudo-Boolean to bit-vector solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-10-23
+
+Notes:
+   
+--*/
+#ifndef PB2BV_SOLVER_H_
+#define PB2BV_SOLVER_H_
+
+#include"ast.h"
+#include"params.h"
+
+class solver;
+
+solver * mk_pb2bv_solver(ast_manager & m, params_ref const & p, solver* s);
+
+#endif

src/test/get_consequences.cpp

@@ -51,85 +51,8 @@ static void test1() {
     std::cout << conseq << "\n";
 }
 
-static void test2() {
-    ast_manager m;
-    reg_decl_plugins(m);
-    bv_util bv(m);
-    datatype_util dtutil(m);
-    params_ref p;
 
-    datatype_decl_plugin & dt = *(static_cast<datatype_decl_plugin*>(m.get_plugin(m.get_family_id("datatype"))));
-    sort_ref_vector new_sorts(m);
-    constructor_decl* R = mk_constructor_decl(symbol("R"), symbol("is-R"), 0, 0);
-    constructor_decl* G = mk_constructor_decl(symbol("G"), symbol("is-G"), 0, 0);
-    constructor_decl* B = mk_constructor_decl(symbol("B"), symbol("is-B"), 0, 0);
-    constructor_decl* constrs[3] = { R, G, B };
-    datatype_decl * enum_sort = mk_datatype_decl(symbol("RGB"), 3, constrs);
-    VERIFY(dt.mk_datatypes(1, &enum_sort, new_sorts));    
-    del_constructor_decls(3, constrs);
-    sort* rgb = new_sorts[0].get();
-
-    expr_ref x = mk_const(m, "x", rgb), y = mk_const(m, "y", rgb), z = mk_const(m, "z", rgb);
-    ptr_vector<func_decl> const& enums = *dtutil.get_datatype_constructors(rgb);
-    expr_ref r = expr_ref(m.mk_const(enums[0]), m);
-    expr_ref g = expr_ref(m.mk_const(enums[1]), m);
-    expr_ref b = expr_ref(m.mk_const(enums[2]), m);
-    expr_ref val(m);
-
-    // Eliminate enumeration data-types:
-    goal_ref gl = alloc(goal, m);
-    gl->assert_expr(m.mk_not(m.mk_eq(x, r)));
-    gl->assert_expr(m.mk_not(m.mk_eq(x, b)));
-    gl->display(std::cout);
-    obj_map<func_decl, func_decl*> tr;
-    obj_map<func_decl, func_decl*> rev_tr;
-    ref<tactic> dt2bv = mk_dt2bv_tactic(m, p, &tr);
-    goal_ref_buffer result;
-    model_converter_ref mc;
-    proof_converter_ref pc;
-    expr_dependency_ref core(m);
-    (*dt2bv)(gl, result, mc, pc, core);
-
-    // Collect translations from enumerations to bit-vectors
-    obj_map<func_decl, func_decl*>::iterator it = tr.begin(), end = tr.end();
-    for (; it != end; ++it) {
-        rev_tr.insert(it->m_value, it->m_key);
-    }
-
-    // Create bit-vector implication problem
-    val = m.mk_const(tr.find(to_app(x)->get_decl()));
-    std::cout << val << "\n";
-    ptr_vector<expr> fmls;
-    result[0]->get_formulas(fmls);    
-    ref<solver> solver = mk_inc_sat_solver(m, p);
-    for (unsigned i = 0; i < fmls.size(); ++i) {
-        solver->assert_expr(fmls[i]);
-    }
-    expr_ref_vector asms(m), vars(m), conseq(m);
-    vars.push_back(val);
-
-    // retrieve consequences
-    solver->get_consequences(asms, vars, conseq);
-    
-    // Convert consequences over bit-vectors to enumeration types.
-    std::cout << conseq << "\n";
-    for (unsigned i = 0; i < conseq.size(); ++i) {
-        expr* a, *b, *u, *v;
-        func_decl* f;
-        rational num;
-        unsigned bvsize;
-        VERIFY(m.is_implies(conseq[i].get(), a, b));
-        if (m.is_eq(b, u, v) && rev_tr.find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) {
-            SASSERT(num.is_unsigned());
-            expr_ref head(m);
-            head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
-            conseq[i] = m.mk_implies(a, head);
-        }
-    }
-    std::cout << conseq << "\n";
-}
-
-void test3() {
+void test2() {
     ast_manager m;
     reg_decl_plugins(m);
     bv_util bv(m);
@@ -189,6 +112,4 @@ void test3() {
 void tst_get_consequences() {
     test1();
     test2();
-    test3();
-
 }

src/test/main.cpp

@@ -229,6 +229,7 @@ int main(int argc, char ** argv) {
     TST_ARGV(ddnf);
     TST(model_evaluator);
     TST(get_consequences);
+    TST(pb2bv);
     //TST_ARGV(hs);
 }
 

src/test/pb2bv.cpp

@@ -0,0 +1,195 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+#include "trace.h"
+#include "vector.h"
+#include "ast.h"
+#include "ast_pp.h"
+#include "statistics.h"
+#include "reg_decl_plugins.h"
+#include "pb2bv_rewriter.h"
+#include "smt_kernel.h"
+#include "model_smt2_pp.h"
+#include "smt_params.h"
+#include "ast_util.h"
+#include "pb_decl_plugin.h"
+#include "th_rewriter.h"
+#include "fd_solver.h"
+#include "solver.h"
+
+static void test1() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    pb_util pb(m);
+    params_ref p;
+    pb2bv_rewriter rw(m, p);
+    expr_ref_vector vars(m);
+    unsigned N = 5;
+    for (unsigned i = 0; i < N; ++i) {
+        std::stringstream strm;
+        strm << "b" << i;
+        vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()));
+    }
+    
+    for (unsigned k = 1; k <= N; ++k) {
+        expr_ref fml(m), result(m);
+        proof_ref proof(m);
+        fml = pb.mk_at_least_k(vars.size(), vars.c_ptr(), k);
+        rw(fml, result, proof);
+        std::cout << fml << " |-> " << result << "\n";
+    }
+    expr_ref_vector lemmas(m);
+    rw.flush_side_constraints(lemmas);
+    std::cout << lemmas << "\n";
+}
+
+static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k, unsigned kind) {
+    pb_util pb(m);
+    params_ref p;
+    pb2bv_rewriter rw(m, p);
+    unsigned N = vars.size();
+    expr_ref fml1(m), fml2(m), result1(m), result2(m);
+    proof_ref proof(m);
+    expr_ref_vector lemmas(m);
+    th_rewriter th_rw(m);
+
+    switch (kind) {
+    case 0: fml1 = pb.mk_ge(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+    case 1: fml1 = pb.mk_le(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+    default: fml1 = pb.mk_eq(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+    }
+    rw(fml1, result1, proof);
+    rw.flush_side_constraints(lemmas);
+    std::cout << lemmas << "\n";
+    for (unsigned values = 0; values < static_cast<unsigned>(1 << N); ++values) {
+        smt_params fp;
+        smt::kernel solver(m, fp);
+        expr_ref_vector tf(m);
+        for (unsigned i = 0; i < N; ++i) {
+            bool is_true = 0 != (values & (1 << i));
+            tf.push_back(is_true ? m.mk_true() : m.mk_false());
+            solver.assert_expr(is_true ? vars[i] : m.mk_not(vars[i]));
+        }
+        
+        solver.assert_expr(lemmas);
+        switch (kind) {
+        case 0: fml2 = pb.mk_ge(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+        case 1: fml2 = pb.mk_le(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+        default: fml2 = pb.mk_eq(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+        }
+        std::cout << fml1 << " " << fml2 << "\n";
+        th_rw(fml2, result2, proof);
+        SASSERT(m.is_true(result2) || m.is_false(result2));
+        lbool res = solver.check();
+        SASSERT(res == l_true);
+        solver.assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());
+        res = solver.check();
+        SASSERT(res == l_false);
+    }
+}
+
+static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k) {
+    test_semantics(m, vars, coeffs, k, 0);
+    test_semantics(m, vars, coeffs, k, 1);
+    test_semantics(m, vars, coeffs, k, 2);
+}
+
+static void test2() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    expr_ref_vector vars(m);
+    unsigned N = 4;
+    for (unsigned i = 0; i < N; ++i) {
+        std::stringstream strm;
+        strm << "b" << i;
+        vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()));
+    }
+    for (unsigned coeff = 0; coeff < static_cast<unsigned>(1 << N); ++coeff) {
+        vector<rational> coeffs;
+        for (unsigned i = 0; i < N; ++i) {
+            bool is_one = 0 != (coeff & (1 << i));
+            coeffs.push_back(is_one ? rational(1) : rational(2));
+        }
+        for (unsigned i = 0; i <= N; ++i) {
+            test_semantics(m, vars, coeffs, i);
+        }
+    }
+}
+
+
+static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k, unsigned kind) {
+    pb_util pb(m);
+    params_ref p;
+    unsigned N = vars.size();
+    expr_ref fml1(m), fml2(m), result1(m), result2(m);
+    proof_ref proof(m);
+    th_rewriter th_rw(m);
+
+    switch (kind) {
+    case 0: fml1 = pb.mk_ge(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+    case 1: fml1 = pb.mk_le(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+    default: fml1 = pb.mk_eq(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break;
+    }
+    result1 = m.mk_fresh_const("xx", m.mk_bool_sort());
+    for (unsigned values = 0; values < static_cast<unsigned>(1 << N); ++values) {
+        ref<solver> slv = mk_fd_solver(m, p);
+        expr_ref_vector tf(m);
+        for (unsigned i = 0; i < N; ++i) {
+            bool is_true = 0 != (values & (1 << i));
+            tf.push_back(is_true ? m.mk_true() : m.mk_false());
+            slv->assert_expr(is_true ? vars[i] : m.mk_not(vars[i]));
+        }
+        slv->assert_expr(m.mk_eq(result1, fml1));
+        
+        switch (kind) {
+        case 0: fml2 = pb.mk_ge(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+        case 1: fml2 = pb.mk_le(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+        default: fml2 = pb.mk_eq(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break;
+        }
+        std::cout << fml1 << " " << fml2 << "\n";
+        th_rw(fml2, result2, proof);
+        SASSERT(m.is_true(result2) || m.is_false(result2));
+        lbool res = slv->check_sat(0,0);
+        SASSERT(res == l_true);
+        slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());
+        res = slv->check_sat(0,0);
+        SASSERT(res == l_false);
+    }
+}
+
+static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k) {
+    test_solver_semantics(m, vars, coeffs, k, 0);
+    test_solver_semantics(m, vars, coeffs, k, 1);
+    test_solver_semantics(m, vars, coeffs, k, 2);
+}
+
+static void test3() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    expr_ref_vector vars(m);
+    unsigned N = 4;
+    for (unsigned i = 0; i < N; ++i) {
+        std::stringstream strm;
+        strm << "b" << i;
+        vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()));
+    }
+    for (unsigned coeff = 0; coeff < static_cast<unsigned>(1 << N); ++coeff) {
+        vector<rational> coeffs;
+        for (unsigned i = 0; i < N; ++i) {
+            bool is_one = 0 != (coeff & (1 << i));
+            coeffs.push_back(is_one ? rational(1) : rational(2));
+        }
+        for (unsigned i = 0; i <= N; ++i) {
+            test_solver_semantics(m, vars, coeffs, i);
+        }
+    }
+}
+
+void tst_pb2bv() {
+    test1();
+    test2();
+    test3();
+}
+

src/test/sorting_network.cpp

@@ -332,31 +332,106 @@ void test_sorting5(unsigned n, unsigned k) {
     test_sorting_ge(n, k);
 }
 
-void test_at_most_1(unsigned n) {
+expr_ref naive_at_most1(expr_ref_vector const& xs) {
+    ast_manager& m = xs.get_manager();
+    expr_ref_vector clauses(m);
+    for (unsigned i = 0; i < xs.size(); ++i) {
+        for (unsigned j = i + 1; j < xs.size(); ++j) {
+            clauses.push_back(m.mk_not(m.mk_and(xs[i], xs[j])));
+        }
+    }
+    return mk_and(clauses);
+}
+
+void test_at_most_1(unsigned n, bool full) {
     ast_manager m;
     reg_decl_plugins(m);
     expr_ref_vector in(m), out(m);
     for (unsigned i = 0; i < n; ++i) {
         in.push_back(m.mk_fresh_const("a",m.mk_bool_sort()));
     }
-
     
+    ast_ext2 ext(m);
+    psort_nw<ast_ext2> sn(ext);
+    expr_ref result1(m), result2(m);    
+    result1 = sn.le(full, 1, in.size(), in.c_ptr());
+    result2 = naive_at_most1(in);
+
+    std::cout << "clauses: " << ext.m_clauses << "\n-----\n";
+
+    smt_params fp;
+    smt::kernel solver(m, fp);
+    for (unsigned i = 0; i < ext.m_clauses.size(); ++i) {
+        solver.assert_expr(ext.m_clauses[i].get());
+    }
+    lbool res;
+    if (full) {
+        solver.push();
+        solver.assert_expr(m.mk_not(m.mk_eq(result1, result2)));
+        
+        std::cout << result1 << "\n";
+        
+        res = solver.check();
+        SASSERT(res == l_false);
+    
+        solver.pop(1);
+    }
+
+    if (n >= 9) return;
+    for (unsigned i = 0; i < static_cast<unsigned>(1 << n); ++i) {
+        std::cout << "checking: " << n << ": " << i << "\n";
+        solver.push();
+        unsigned k = 0;
+        for (unsigned j = 0; j < n; ++j) {
+            bool is_true = (i & (1 << j)) != 0;
+            expr_ref atom(m);
+            atom = is_true ? in[j].get() : m.mk_not(in[j].get());
+            solver.assert_expr(atom);
+            std::cout << atom << "\n";
+            if (is_true) ++k;
+        }
+        res = solver.check();
+        SASSERT(res == l_true);
+        if (k > 1) {
+            solver.assert_expr(result1);
+        }
+        else if (!full) {
+            solver.pop(1);
+            continue;
+        }
+        else {
+            solver.assert_expr(m.mk_not(result1));
+        }
+        res = solver.check();
+        SASSERT(res == l_false);
+        solver.pop(1);
+    }
+}
+
+
+static void test_at_most1() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    expr_ref_vector in(m), out(m);
+    for (unsigned i = 0; i < 5; ++i) {
+        in.push_back(m.mk_fresh_const("a",m.mk_bool_sort()));
+    }
+    in[4] = in[3];
+
     ast_ext2 ext(m);
     psort_nw<ast_ext2> sn(ext);
     expr_ref result(m);
-    result = sn.le(false, 1, in.size(), in.c_ptr());
+    result = sn.le(true, 1, in.size(), in.c_ptr());
     std::cout << result << "\n";
     std::cout << ext.m_clauses << "\n";
 }
 
 void tst_sorting_network() {
-    test_at_most_1(1);
-    test_at_most_1(2);
-    test_at_most_1(3);
-    test_at_most_1(4);
-    test_at_most_1(5);
-    test_at_most_1(10);
-    return;
+    for (unsigned i = 1; i < 17; ++i) {
+        test_at_most_1(i, true);
+        test_at_most_1(i, false);
+    }
+    test_at_most1();
 
     test_sorting_eq(11,7);
     for (unsigned n = 3; n < 20; n += 2) {

src/util/mpq.cpp

@@ -153,7 +153,7 @@ void mpq_manager<SYNCH>::display_smt2(std::ostream & out, mpq const & a, bool de
 }
 
 template<bool SYNCH>
-void mpq_manager<SYNCH>::display_decimal(std::ostream & out, mpq const & a, unsigned prec) {
+void mpq_manager<SYNCH>::display_decimal(std::ostream & out, mpq const & a, unsigned prec, bool truncate) {
     mpz n1, d1, v1;
     get_numerator(a, n1);
     get_denominator(a, d1);
@@ -177,7 +177,7 @@ void mpq_manager<SYNCH>::display_decimal(std::ostream & out, mpq const & a, unsi
         if (is_zero(n1))
             goto end; // number is precise
     }
-    out << "?";
+    if (!truncate) out << "?";
  end:
     del(ten); del(n1); del(d1); del(v1);
 }

src/util/mpq.h

@@ -265,7 +265,7 @@ public:
 
     void display_smt2(std::ostream & out, mpq const & a, bool decimal) const;
 
-    void display_decimal(std::ostream & out, mpq const & a, unsigned prec);
+    void display_decimal(std::ostream & out, mpq const & a, unsigned prec, bool truncate = false);
 
     void add(mpz const & a, mpz const & b, mpz & c) { mpz_manager<SYNCH>::add(a, b, c); }
     

src/util/rational.h

@@ -86,7 +86,7 @@ public:
 
     void display(std::ostream & out) const { return m().display(out, m_val); }
     
-    void display_decimal(std::ostream & out, unsigned prec) const { return m().display_decimal(out, m_val, prec); }
+    void display_decimal(std::ostream & out, unsigned prec, bool truncate = false) const { return m().display_decimal(out, m_val, prec, truncate); }
 
     bool is_uint64() const { return m().is_uint64(m_val); }
 

src/util/sorting_network.h

@@ -226,7 +226,12 @@ Notes:
                 m_t = EQ;
                 card(k+1, n, xs, out);
                 SASSERT(out.size() >= k+1);
-                return ctx.mk_min(out[k-1], ctx.mk_not(out[k]));
+                if (k == 0) {
+                    return ctx.mk_not(out[k]);
+                }
+                else {
+                    return ctx.mk_min(out[k-1], ctx.mk_not(out[k]));
+                }
             }
         }
 
@@ -234,19 +239,28 @@ Notes:
     private:
 
         literal mk_at_most_1(bool full, unsigned n, literal const* xs) {
+            TRACE("pb", tout << (full?"full":"partial") << " ";
+                  for (unsigned i = 0; i < n; ++i) tout << xs[i] << " ";
+                  tout << "\n";);
+
+            if (!full && n >= 4) {
+                return mk_at_most_1_bimander(n, xs);
+            }
             literal_vector in(n, xs);
             literal result = fresh();
             unsigned inc_size = 4;
+            literal_vector ands;
+            ands.push_back(result);
             while (!in.empty()) {
                 literal_vector ors;
                 unsigned i = 0;
                 unsigned n = in.size();
                 bool last = n <= inc_size;
                 for (; i + inc_size < n; i += inc_size) {                    
-                    mk_at_most_1_small(full, last, inc_size, in.c_ptr() + i, result, ors);
+                    mk_at_most_1_small(full, last, inc_size, in.c_ptr() + i, result, ands, ors);
                 }
                 if (i < n) {
-                    mk_at_most_1_small(full, last, n - i, in.c_ptr() + i, result, ors);
+                    mk_at_most_1_small(full, last, n - i, in.c_ptr() + i, result, ands, ors);
                 }
                 if (last) {
                     break;
@@ -255,10 +269,20 @@ Notes:
                 in.append(ors);
                 ors.reset();                
             }
+            if (full) {
+                add_clause(ands);
+            }
             return result;
         }
 
-        void mk_at_most_1_small(bool full, bool last, unsigned n, literal const* xs, literal result, literal_vector& ors) {
+        void mk_at_most_1_small(bool full, bool last, unsigned n, literal const* xs, literal result, literal_vector& ands, literal_vector& ors) {
+            SASSERT(n > 0);
+            if (n == 1) {
+                if (!last) {
+                    ors.push_back(xs[0]);
+                }
+                return;
+            }
             if (!last) {
                 literal ex = fresh();
                 for (unsigned j = 0; j < n; ++j) {
@@ -271,16 +295,59 @@ Notes:
                 }
                 ors.push_back(ex);
             }
+            // result => xs[0] + ... + xs[n-1] <= 1
             for (unsigned i = 0; i < n; ++i) {
                 for (unsigned j = i + 1; j < n; ++j) {
                     add_clause(ctx.mk_not(result), ctx.mk_not(xs[i]), ctx.mk_not(xs[j]));
                 }
-                if (full) {
-                    add_clause(result, xs[i]);
+            }            
+            // xs[0] + ... + xs[n-1] <= 1 => and_x
+            if (full) {
+                literal and_i = fresh();
+                for (unsigned i = 0; i < n; ++i) {
+                    literal_vector lits;
+                    lits.push_back(and_i);
+                    for (unsigned j = 0; j < n; ++j) {
+                        if (j != i) lits.push_back(xs[j]);
+                    }
+                    add_clause(lits);
                 }
+                ands.push_back(ctx.mk_not(and_i));
             }
         }
 
+        literal mk_at_most_1_bimander(unsigned n, literal const* xs) {
+            literal_vector in(n, xs);
+            literal result = fresh();
+            unsigned inc_size = 2;
+            bool last = false;
+            bool full = false;
+            literal_vector ors, ands;
+            unsigned i = 0;
+            for (; i + inc_size < n; i += inc_size) {                    
+                mk_at_most_1_small(full, last, inc_size, in.c_ptr() + i, result, ands, ors);
+            }
+            if (i < n) {
+                mk_at_most_1_small(full, last, n - i, in.c_ptr() + i, result, ands, ors);
+            }
+            
+            unsigned nbits = 0;
+            while (static_cast<unsigned>(1 << nbits) < ors.size()) {
+                ++nbits;
+            }
+            literal_vector bits;
+            for (unsigned k = 0; k < nbits; ++k) {
+                bits.push_back(fresh());
+            }
+            for (i = 0; i < ors.size(); ++i) {
+                for (unsigned k = 0; k < nbits; ++k) {
+                    bool bit_set = (i & (static_cast<unsigned>(1 << k))) != 0;
+                    add_clause(ctx.mk_not(result), ctx.mk_not(ors[i]), bit_set ? bits[k] : ctx.mk_not(bits[k]));
+                }
+            }            
+            return result;
+        }
+
         std::ostream& pp(std::ostream& out, unsigned n, literal const* lits) {
             for (unsigned i = 0; i < n; ++i) ctx.pp(out, lits[i]) << " ";
             return out;
@@ -344,9 +411,13 @@ Notes:
             literal lits[2] = { l1, l2 };
             add_clause(2, lits);
         }
+        void add_clause(literal_vector const& lits) {
+            add_clause(lits.size(), lits.c_ptr());
+        }
         void add_clause(unsigned n, literal const* ls) {
             m_stats.m_num_compiled_clauses++;
             literal_vector tmp(n, ls);
+            TRACE("pb", for (unsigned i = 0; i < n; ++i) tout << ls[i] << " "; tout << "\n";);
             ctx.mk_clause(n, tmp.c_ptr());
         }
 
@@ -383,7 +454,7 @@ Notes:
         }
 
         void card(unsigned k, unsigned n, literal const* xs, literal_vector& out) {
-            TRACE("pb", tout << "card k:" << k << " n: " << n << "\n";);
+            TRACE("pb", tout << "card k: " << k << " n: " << n << "\n";);
             if (n <= k) {
                 psort_nw<psort_expr>::sorting(n, xs, out);
             }
@@ -397,7 +468,7 @@ Notes:
                 card(k, n-l, xs + l, out2);
                 smerge(k, out1.size(), out1.c_ptr(), out2.size(), out2.c_ptr(), out);
             }
-            TRACE("pb", tout << "card k:" << k << " n: " << n << "\n";
+            TRACE("pb", tout << "card k: " << k << " n: " << n << "\n";
                   pp(tout << "in:", n, xs) << "\n";
                   pp(tout << "out:", out) << "\n";);
 
@@ -743,7 +814,7 @@ Notes:
                         if (j < b) {
                             ls.push_back(as[i]);
                             ls.push_back(bs[j]);
-                            add_clause(ls.size(), ls.c_ptr());
+                            add_clause(ls);
                             ls.pop_back();
                             ls.pop_back();
                         }
@@ -804,7 +875,7 @@ Notes:
                   pp(tout, lits) << "\n";);
             SASSERT(k + offset <= n);
             if (k == 0) {
-                add_clause(lits.size(), lits.c_ptr());
+                add_clause(lits);
                 return;
             }
             for (unsigned i = offset; i < n - k + 1; ++i) {