fix performance for model construction, recognize concats of values as a value for pre-processing

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

src/ast/rewriter/seq_rewriter.cpp

@@ -246,6 +246,8 @@ eautomaton* re2automaton::re2aut(expr* e) {
             expr_ref _stop(bv.mk_numeral(stop, nb), m);
             expr_ref _pred(m.mk_not(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop))), m);
             a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
+            display_expr1 disp(m);
+            TRACE("seq", tout << mk_pp(e, m) << "\n"; a->display(tout, disp););
             return a.detach();
         }
         else if (u.re.is_to_re(e0, e1) && u.str.is_string(e1, s1) && s1.length() == 1) {
@@ -255,6 +257,8 @@ eautomaton* re2automaton::re2aut(expr* e) {
             expr_ref _ch(bv.mk_numeral(s1[0], nb), m);          
             expr_ref _pred(m.mk_not(m.mk_eq(v, _ch)), m);
             a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
+            display_expr1 disp(m);
+            TRACE("seq", tout << mk_pp(e, m) << "\n"; a->display(tout, disp););
             return a.detach();
         }
         else if (u.re.is_to_re(e0, e1) && u.str.is_unit(e1, e2)) {
@@ -262,6 +266,8 @@ eautomaton* re2automaton::re2aut(expr* e) {
             expr_ref v(m.mk_var(0, s), m);
             expr_ref _pred(m.mk_not(m.mk_eq(v, e2)), m);
             a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
+            display_expr1 disp(m);
+            TRACE("seq", tout << mk_pp(e, m) << "\n"; a->display(tout, disp););
             return a.detach();
         }
         else {

src/ast/seq_decl_plugin.cpp

@@ -112,6 +112,11 @@ zstring::zstring(zstring const& other) {
     m_encoding = other.m_encoding;
 }
 
+zstring::zstring(unsigned sz, unsigned const* s, encoding enc) {
+    m_buffer.append(sz, s);
+    m_encoding = enc;
+}
+
 zstring::zstring(unsigned num_bits, bool const* ch) {
     SASSERT(num_bits == 8 || num_bits == 16);
     m_encoding = (num_bits == 8)?ascii:unicode;
@@ -578,6 +583,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_RE_OF_PRED:
     case OP_STRING_ITOS:
     case OP_STRING_STOI:
+    case OP_RE_COMPLEMENT:
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
 
@@ -632,7 +638,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         default:
             m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters");
         }
-
+        
 
     case OP_STRING_CONST:
         if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
@@ -641,7 +647,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return m.mk_const_decl(m_stringc_sym, m_string,
                                func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
 
-    case OP_RE_COMPLEMENT:
     case OP_RE_UNION:
     case OP_RE_CONCAT:
     case OP_RE_INTERSECT:
@@ -761,10 +766,28 @@ app* seq_decl_plugin::mk_string(zstring const& s) {
 
 
 bool seq_decl_plugin::is_value(app* e) const {
-    return
+    while (true) {
-        is_app_of(e, m_family_id, OP_SEQ_EMPTY) ||
+        if (is_app_of(e, m_family_id, OP_SEQ_EMPTY)) {
-        (is_app_of(e, m_family_id, OP_SEQ_UNIT) &&
+            return true;
-         m_manager->is_value(e->get_arg(0)));
+        }
+        if (is_app_of(e, m_family_id, OP_STRING_CONST)) {
+            return true;
+        }
+        if (is_app_of(e, m_family_id, OP_SEQ_UNIT) &&
+            m_manager->is_value(e->get_arg(0))) {
+            return true;
+        }
+        if (is_app_of(e, m_family_id, OP_SEQ_CONCAT) &&
+            e->get_num_args() == 2 && 
+            is_app(e->get_arg(0)) &&
+            is_app(e->get_arg(1)) &&
+            is_value(to_app(e->get_arg(0)))) {
+            e = to_app(e->get_arg(1));
+            continue;
+        }
+        TRACE("seq", tout << mk_pp(e, *m_manager) << "\n";);
+        return false;
+    }
 }
 
 expr* seq_decl_plugin::get_some_value(sort* s) {

src/ast/seq_decl_plugin.h

@@ -95,6 +95,7 @@ private:
 public:
     zstring(encoding enc = ascii);
     zstring(char const* s, encoding enc = ascii);
+    zstring(unsigned sz, unsigned const* s, encoding enc = ascii);
     zstring(zstring const& other);
     zstring(unsigned num_bits, bool const* ch);
     zstring(unsigned ch, encoding enc = ascii);

src/opt/opt_cmds.cpp

@@ -116,11 +116,9 @@ public:
     {}
 
     virtual void reset(cmd_context & ctx) { }
-
     virtual char const * get_usage() const { return "<term>"; }
     virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo objective function";}
     virtual unsigned get_arity() const { return 1; }
-
     virtual void prepare(cmd_context & ctx) {}
     virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR; }
 
@@ -139,204 +137,72 @@ public:
     }
 };
 
+class alternate_min_max_cmd : public cmd {
+    app_ref_vector       m_vars;
+    svector<bool>        m_is_max;
+    unsigned             m_position;
+public:
+    alternate_min_max_cmd(ast_manager& m):
+        cmd("min-max"),
+        m_vars(m),
+        m_position(0)
+    {}
+    
+    virtual void reset(cmd_context & ctx) { 
+        m_vars.reset();
+        m_is_max.reset();
+        m_position = 0;
+    }
+    virtual char const * get_usage() const { return "(min | max | var)+ <term>"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo alternating min-max objectives";}
+    virtual unsigned get_arity() const { return 2; }
+    virtual void prepare(cmd_context & ctx) {}
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
+        switch (m_position) {
+        case 0: return CPK_SYMBOL_LIST;
+        case 1: return CPK_EXPR;
+        default: return CPK_SYMBOL;
+        }
+    }
+
+    virtual void set_next_arg(cmd_context & ctx, unsigned num, symbol const * slist) {
+        bool is_max = false;
+        for (unsigned i = 0; i < num; ++i) {
+            if (slist[i] == symbol("max")) {
+                is_max = true;
+            }
+            else if (slist[i] == symbol("min")) {
+                is_max = false;
+            }
+            else {
+                m_is_max.push_back(is_max);
+                m_vars.push_back(ctx.m().mk_const(ctx.find_func_decl(slist[i])));
+            }
+        }
+        ++m_position;
+    }
+
+    virtual void set_next_arg(cmd_context & ctx, expr * t) {
+        if (!is_app(t)) {
+            throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable");
+        }
+        ++m_position;
+        get_opt(ctx).min_max(to_app(t), m_vars, m_is_max);
+    }
+
+    virtual void failure_cleanup(cmd_context & ctx) {
+        reset(ctx);
+    }
+
+    virtual void execute(cmd_context & ctx) { }
+};
 
 
 void install_opt_cmds(cmd_context & ctx) {
     ctx.insert(alloc(assert_soft_cmd));
     ctx.insert(alloc(min_maximize_cmd, true));
     ctx.insert(alloc(min_maximize_cmd, false));
+    ctx.insert(alloc(alternate_min_max_cmd, ctx.m()));
 }
 
 
-#if 0
-    ctx.insert(alloc(optimize_cmd));
-    ctx.insert(alloc(assert_weighted_cmd));
-
-
-class optimize_cmd : public parametric_cmd {
-public:
-    optimize_cmd():
-        parametric_cmd("optimize")
-    {}
-
-    virtual ~optimize_cmd() {
-    }
-
-    virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
-        insert_timeout(p);
-        insert_max_memory(p);
-        p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
-        opt::context::collect_param_descrs(p);
-    }
-
-    virtual char const * get_main_descr() const { return "check sat modulo objective function";}
-    virtual char const * get_usage() const { return "(<keyword> <value>)*"; }
-    virtual void prepare(cmd_context & ctx) {
-        parametric_cmd::prepare(ctx);
-    }
-    virtual void failure_cleanup(cmd_context & ctx) {
-        reset(ctx);
-    }
-
-    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
-        return parametric_cmd::next_arg_kind(ctx);
-    }
-
-
-    virtual void execute(cmd_context & ctx) {
-        params_ref p = ctx.params().merge_default_params(ps());
-        opt::context& opt = get_opt(ctx);
-        opt.updt_params(p);
-        unsigned timeout = p.get_uint("timeout", UINT_MAX);
-
-        ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
-        ptr_vector<expr>::const_iterator end = ctx.end_assertions();
-        for (; it != end; ++it) {
-            opt.add_hard_constraint(*it);
-        }
-        lbool r = l_undef;
-        cancel_eh<reslimit> eh(m.limit());
-        {
-            scoped_ctrl_c ctrlc(eh);
-            scoped_timer timer(timeout, &eh);
-            cmd_context::scoped_watch sw(ctx);
-            try {
-                r = opt.optimize();
-                if (r == l_true && opt.is_pareto()) {
-                    while (r == l_true) {
-                        display_result(ctx);
-                        ctx.regular_stream() << "\n";
-                        r = opt.optimize();
-                    }
-                    if (p.get_bool("print_statistics", false)) {
-                        display_statistics(ctx);
-                    }
-                    return;
-                }
-            }
-            catch (z3_error& ex) {
-                ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl;
-            }
-            catch (z3_exception& ex) {
-                ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl;
-            }
-        }
-        switch(r) {
-        case l_true: {
-            ctx.regular_stream() << "sat\n";
-            display_result(ctx);
-            break;
-        }
-        case l_false:
-            ctx.regular_stream() << "unsat\n";
-            break;
-        case l_undef:
-            ctx.regular_stream() << "unknown\n";
-            display_result(ctx);
-            break;
-        }
-        if (p.get_bool("print_statistics", false)) {
-            display_statistics(ctx);
-        }
-    }
-
-    void display_result(cmd_context & ctx) {
-        params_ref p = ctx.params().merge_default_params(ps());
-        opt::context& opt = get_opt(ctx);
-        opt.display_assignment(ctx.regular_stream());
-        opt_params optp(p);
-        if (optp.print_model()) {
-            model_ref mdl;
-            opt.get_model(mdl);
-            if (mdl) {
-                ctx.regular_stream() << "(model " << std::endl;
-                model_smt2_pp(ctx.regular_stream(), ctx, *(mdl.get()), 2);
-                ctx.regular_stream() << ")" << std::endl;                    
-            }
-        }
-    }
-private:
-
-    void display_statistics(cmd_context& ctx) {
-        statistics stats;
-        get_opt(ctx).collect_statistics(stats);
-        stats.update("time", ctx.get_seconds());
-        stats.display_smt2(ctx.regular_stream());        
-    }
-};
-
-class assert_weighted_cmd : public cmd {
-    unsigned     m_idx;
-    expr*        m_formula;
-    rational     m_weight;
-    symbol       m_id;
-
-public:
-    assert_weighted_cmd():
-        cmd("assert-weighted"),
-        m_idx(0),
-        m_formula(0),
-        m_weight(0)
-    {}
-
-    virtual ~assert_weighted_cmd() {
-    }
-
-    virtual void reset(cmd_context & ctx) { 
-        m_idx = 0; 
-        m_formula = 0;
-        m_id = symbol::null;
-    }
-
-    virtual char const * get_usage() const { return "<formula> <rational-weight>"; }
-    virtual char const * get_descr(cmd_context & ctx) const { return "assert soft constraint with weight"; }
-    virtual unsigned get_arity() const { return VAR_ARITY; }
-
-    // command invocation
-    virtual void prepare(cmd_context & ctx) {}
-    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { 
-        switch(m_idx) {
-        case 0: return CPK_EXPR; 
-        case 1: return CPK_NUMERAL; 
-        default: return CPK_SYMBOL;
-        }
-    }
-    virtual void set_next_arg(cmd_context & ctx, rational const & val) { 
-        SASSERT(m_idx == 1);
-        if (!val.is_pos()) {
-            throw cmd_exception("Invalid weight. Weights must be positive.");
-        }
-        m_weight = val;
-        ++m_idx;
-    }
-
-    virtual void set_next_arg(cmd_context & ctx, expr * t) {
-        SASSERT(m_idx == 0);
-        if (!ctx.m().is_bool(t)) {
-            throw cmd_exception("Invalid type for expression. Expected Boolean type.");
-        }
-        m_formula = t;
-        ++m_idx;
-    }
-
-    virtual void set_next_arg(cmd_context & ctx, symbol const& s) {
-        SASSERT(m_idx > 1);
-        m_id = s;
-        ++m_idx;
-    }
-
-    virtual void failure_cleanup(cmd_context & ctx) {
-        reset(ctx);
-    }
-
-    virtual void execute(cmd_context & ctx) {
-        get_opt(ctx).add_soft_constraint(m_formula, m_weight, m_id);
-        reset(ctx);
-    }
-
-    virtual void finalize(cmd_context & ctx) { 
-    }
-
-};
-
-#endif

src/opt/opt_context.cpp

@@ -193,6 +193,8 @@ namespace opt {
         return m_scoped_state.add(t, is_max);
     }
 
+
+
     void context::import_scoped_state() {
         m_optsmt.reset();        
         reset_maxsmts();
@@ -209,6 +211,20 @@ namespace opt {
         m_hard_constraints.append(s.m_hard);
     }
 
+    lbool context::min_max(app* t, app_ref_vector const& vars, svector<bool> const& is_max) {
+        clear_state();
+        init_solver(); 
+        import_scoped_state(); 
+        normalize();
+        internalize();
+        update_solver();
+        solver& s = get_solver();
+        s.assert_expr(m_hard_constraints);
+        std::cout << "min-max is TBD\n";
+        return l_undef;
+    }
+
+
     lbool context::optimize() {
         if (m_pareto) {
             return execute_pareto();
@@ -223,10 +239,7 @@ namespace opt {
         internalize();
         update_solver();
         solver& s = get_solver();
-        for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
+        s.assert_expr(m_hard_constraints);
-            TRACE("opt", tout << "Hard constraint: " << mk_ismt2_pp(m_hard_constraints[i].get(), m) << std::endl;);
-            s.assert_expr(m_hard_constraints[i].get());
-        }
         display_benchmark();
         IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";);
         lbool is_sat = s.check_sat(0,0);

src/opt/opt_context.h

@@ -172,6 +172,7 @@ namespace opt {
         virtual ~context();
         unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id);
         unsigned add_objective(app* t, bool is_max);
+        lbool min_max(app* t, app_ref_vector const& vars, svector<bool> const& is_max);
         void add_hard_constraint(expr* f);
         
 

src/smt/asserted_formulas.cpp

@@ -607,27 +607,25 @@ void asserted_formulas::propagate_values() {
         expr_ref   n(m_asserted_formulas.get(i), m_manager);
         proof_ref pr(m_asserted_formula_prs.get(i, 0), m_manager);
         TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";);
-        if (m_manager.is_eq(n)) {
+        expr* lhs, *rhs;
-            expr * lhs = to_app(n)->get_arg(0);
+        if (m_manager.is_eq(n, lhs, rhs) &&
-            expr * rhs = to_app(n)->get_arg(1);
+            (m_manager.is_value(lhs) || m_manager.is_value(rhs))) {
-            if (m_manager.is_value(lhs) || m_manager.is_value(rhs)) {
+            if (m_manager.is_value(lhs)) {
-                if (m_manager.is_value(lhs)) {
+                std::swap(lhs, rhs);
-                    std::swap(lhs, rhs);
+                n  = m_manager.mk_eq(lhs, rhs);
-                    n = m_manager.mk_eq(lhs, rhs);
+                pr = m_manager.mk_symmetry(pr);
-                    pr = m_manager.mk_symmetry(pr);
+            }
-                }
+            if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
-                if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
+                if (i >= m_asserted_qhead) {
-                    if (i >= m_asserted_qhead) {
+                    new_exprs1.push_back(n);
-                        new_exprs1.push_back(n);
+                    if (m_manager.proofs_enabled())
-                        if (m_manager.proofs_enabled())
+                        new_prs1.push_back(pr);
-                            new_prs1.push_back(pr);
-                    }
-                    TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";
-                          if (pr) tout << "proof: " << mk_pp(pr, m_manager) << "\n";);
-                    m_simplifier.cache_result(lhs, rhs, pr);
-                    found = true;
-                    continue;
                 }
+                TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";
+                      if (pr) tout << "proof: " << mk_pp(pr, m_manager) << "\n";);
+                m_simplifier.cache_result(lhs, rhs, pr);
+                found = true;
+                continue;
             }
         }
         if (i >= m_asserted_qhead) {

src/smt/theory_seq.cpp

@@ -2028,29 +2028,36 @@ public:
         expr_ref_vector args(th.m);
         unsigned j = 0, k = 0;
         bool is_string = th.m_util.is_string(m_sort);
-        for (unsigned i = 0; i < m_source.size(); ++i) {
+        svector<unsigned> sbuffer;
-            if (m_source[i] && is_string) {
+        expr_ref result(th.m);
-                bv_util bv(th.m);
+        if (is_string) {
-                rational val;
+            bv_util bv(th.m);
-                unsigned sz;
+            rational val;
-                VERIFY(bv.is_numeral(values[j++], val, sz));
+            unsigned sz;
-                svector<bool> val_as_bits;
+
-                unsigned v = val.get_unsigned();
+            for (unsigned i = 0; i < m_source.size(); ++i) {
-                for (unsigned i = 0; i < sz; ++i) {
+                if (m_source[i]) {
-                    val_as_bits.push_back(1 == v % 2);
+                    VERIFY(bv.is_numeral(values[j++], val, sz));
-                    v = v / 2;
                 }
-                args.push_back(th.m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr())));
+                else {
-            }
+                    VERIFY(bv.is_numeral(m_strings[k++], val, sz));
-            else if (m_source[i]) {
+                }
-                args.push_back(th.m_util.str.mk_unit(values[j++]));
+                sbuffer.push_back(val.get_unsigned());
-            }
-            else {
-                args.push_back(m_strings[k++]);
             }
+            result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr()));
+        }
+        else {
+            for (unsigned i = 0; i < m_source.size(); ++i) {
+                if (m_source[i]) {
+                    args.push_back(th.m_util.str.mk_unit(values[j++]));
+                }
+                else {
+                    args.push_back(m_strings[k++]);
+                }
+            }
+            result = th.mk_concat(args, m_sort);
+            th.m_rewrite(result);
         }
-        expr_ref result = th.mk_concat(args, m_sort);
-        th.m_rewrite(result);
         th.m_factory->add_trail(result);
         return to_app(result);
     }

src/solver/solver.h

@@ -75,6 +75,10 @@ public:
     */
     virtual void assert_expr(expr * t) = 0;
 
+    void assert_expr(expr_ref_vector const& ts) { 
+        for (unsigned i = 0; i < ts.size(); ++i) assert_expr(ts[i]); 
+    }
+
     /**
        \brief Add a new formula \c t to the assertion stack, and "tag" it with \c a.
        The propositional variable \c a is used to track the use of \c t in a proof