extract/concat plumbing

src/math/polysat/solver.h

@@ -320,9 +320,6 @@ namespace polysat {
 
         void push_reinit_stack(clause& c);
 
-        /** Get variable representing v[hi:lo] */
-        pvar extract_var(pvar v, unsigned hi, unsigned lo);
-
         void add_clause(clause_ref clause);
         void add_clause(clause& clause);
         void add_clause(signed_constraint c1, bool is_redundant);
@@ -415,11 +412,11 @@ namespace polysat {
          */
         pdd var(pvar v) { return m_vars[v]; }
 
-        /** Create expression for v[hi:lo] */
-        pdd extract(pvar v, unsigned hi, unsigned lo);
-
         /** Create expression for p[hi:lo] */
-        pdd extract(pdd const& p, unsigned hi, unsigned lo);
+        pdd extract(pdd const& p, unsigned hi, unsigned lo) { return m_constraints.extract(p, hi, lo); }
+
+        /** Create expression for concatenation of args */
+        pdd concat(unsigned num_args, pdd const* args) { return m_constraints.concat(num_args, args); }
 
         /**
         * Create terms for unsigned quot-rem

src/sat/smt/bv_polysat.cpp

@@ -32,9 +32,11 @@ namespace bv {
 
     void solver::internalize_polysat(app* a) {
 
+        // verbose_stream() << "internalize_polysat: " << mk_ismt2_pp(a, m) << "\n";
+
 #define if_unary(F) if (a->get_num_args() == 1) { polysat_unary(a, [&](pdd const& p) { return F(p); }); break; }
 
-        switch (to_app(a)->get_decl_kind()) {
+        switch (a->get_decl_kind()) {
         case OP_BMUL:             polysat_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break;
         case OP_BADD:             polysat_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break;
         case OP_BSUB:             polysat_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break;
@@ -65,6 +67,18 @@ namespace bv {
         case OP_BSMUL_NO_OVFL:    polysat_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_ovfl(p, q); }); break;
         case OP_BSMUL_NO_UDFL:    polysat_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_udfl(p, q); }); break;
 
+        case OP_BUMUL_OVFL:
+        case OP_BSMUL_OVFL:
+        case OP_BSDIV_OVFL:
+        case OP_BNEG_OVFL:
+        case OP_BUADD_OVFL:
+        case OP_BSADD_OVFL:
+        case OP_BUSUB_OVFL:
+        case OP_BSSUB_OVFL:
+            // handled by bv_rewriter for now
+            UNREACHABLE();
+            break;
+
         case OP_BUDIV_I:          polysat_div_rem_i(a, true); break;
         case OP_BUREM_I:          polysat_div_rem_i(a, false); break;
 
@@ -76,6 +90,12 @@ namespace bv {
         case OP_BUREM0:           break;
         case OP_BSMOD0:           break;
 
+        case OP_EXTRACT:          polysat_extract(a); break;
+        case OP_CONCAT:           polysat_concat(a); break;
+
+        case OP_ZERO_EXT:
+        case OP_SIGN_EXT:
+
             // polysat::solver should also support at least:
         case OP_BREDAND: // x == 2^K - 1
         case OP_BREDOR:  // x > 0
@@ -87,10 +107,6 @@ namespace bv {
         case OP_BSMOD_I:
         case OP_BASHR:
         case OP_BCOMP:
-        case OP_SIGN_EXT:
-        case OP_ZERO_EXT:
-        case OP_CONCAT:
-        case OP_EXTRACT:
             std::cout << mk_pp(a, m) << "\n";
             NOT_IMPLEMENTED_YET();
             return;
@@ -164,6 +180,23 @@ namespace bv {
         }
     }
 
+    void solver::polysat_extract(app* e) {
+        unsigned const hi = bv.get_extract_high(e);
+        unsigned const lo = bv.get_extract_low(e);
+        auto const src = expr2pdd(e->get_arg(0));
+        auto const p = m_polysat.extract(src, hi, lo);
+        polysat_set(e, p);
+    }
+
+    void solver::polysat_concat(app* e) {
+        SASSERT(bv.is_concat(e));
+        vector<pdd> args;
+        for (unsigned i = 0; i < e->get_num_args(); ++i)
+            args.push_back(expr2pdd(e->get_arg(i)));
+        auto const p = m_polysat.concat(args.size(), args.data());
+        polysat_set(e, p);
+    }
+
     void solver::polysat_binary(app* e, std::function<polysat::pdd(polysat::pdd, polysat::pdd)> const& fn) {
         SASSERT(e->get_num_args() >= 1);
         auto p = expr2pdd(e->get_arg(0));

src/sat/smt/bv_solver.cpp

@@ -59,6 +59,10 @@ namespace bv {
         m_bb.set_flat_and_or(false);
     }
 
+    void solver::updt_params(params_ref const& p) {
+        m_polysat.updt_params(p);
+    }
+
     bool solver::is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) {
         numeral n;
         if (!get_fixed_value(v, n))

src/sat/smt/bv_solver.h

@@ -325,6 +325,8 @@ namespace bv {
         void polysat_pop(unsigned n);
         void polysat_unary(app* e, std::function<polysat::pdd(polysat::pdd)> const& fn);
         void polysat_binary(app* e, std::function<polysat::pdd(polysat::pdd, polysat::pdd)> const& fn);
+        void polysat_extract(app* e);
+        void polysat_concat(app* e);
         polysat::pdd expr2pdd(expr* e);
         void polysat_set(euf::theory_var v, polysat::pdd const& p);
         polysat::pdd var2pdd(euf::theory_var v);
@@ -404,6 +406,7 @@ namespace bv {
        
     public:
         solver(euf::solver& ctx, theory_id id);
+        void updt_params(params_ref const& p) override;
         void set_lookahead(sat::lookahead* s) override { }
         void init_search() override {}
         double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;