use expression structure for objectives instead of custom s-expression

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

src/cmd_context/cmd_context.h

@@ -211,7 +211,6 @@ protected:
 
     void register_builtin_sorts(decl_plugin * p);
     void register_builtin_ops(decl_plugin * p);
-    void register_plugin(symbol const & name, decl_plugin * p, bool install_names);
     void init_manager_core(bool new_manager);
     void init_manager();
     void init_external_manager();
@@ -298,7 +297,8 @@ public:
     check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
     check_sat_state cs_state() const;
     void validate_model();
-    
+
+    void register_plugin(symbol const & name, decl_plugin * p, bool install_names);    
     bool is_func_decl(symbol const & s) const;
     bool is_sort_decl(symbol const& s) const { return m_psort_decls.contains(s); }
     void insert(cmd * c);

src/opt/objective_decl_plugin.cpp

@@ -0,0 +1,88 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    objective_decl_plugin.cpp
+
+Abstract:
+    Abstract data-type for compound objectives.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-11-21
+
+Notes:
+
+--*/
+
+#include "objective_decl_plugin.h"
+
+namespace opt{
+    objective_decl_plugin::objective_decl_plugin() {}
+
+    objective_decl_plugin::~objective_decl_plugin() {}
+        
+    sort * objective_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
+        SASSERT(k == OBJECTIVE_SORT);
+        SASSERT(num_parameters == 0);
+        return m_manager->mk_sort(symbol("objective"), sort_info(get_family_id(), k));
+    }
+
+    symbol objective_decl_plugin::get_name(obj_kind k) const {
+        switch(k) {
+        case OP_MINIMIZE: return symbol("minimize");
+        case OP_MAXIMIZE: return symbol("maximize");
+        case OP_LEX: return symbol("lex");
+        case OP_BOX: return symbol("box");
+        case OP_PARETO: return symbol("pareto");
+        default:
+            UNREACHABLE();
+            return symbol();
+        }
+    }
+        
+    func_decl * objective_decl_plugin::mk_func_decl(
+        decl_kind k, unsigned num_parameters, parameter const * parameters, 
+        unsigned arity, sort * const * domain, sort * range) {
+        SASSERT(num_parameters == 0);
+        symbol name = get_name(static_cast<obj_kind>(k));
+        func_decl_info info(get_family_id(), k, num_parameters, parameters);
+        return m_manager->mk_func_decl(name, arity, domain, range, info);
+    }
+    
+    void objective_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
+        if (logic == symbol::null) {
+            op_names.push_back(builtin_name(get_name(OP_MAXIMIZE).bare_str(), OP_MAXIMIZE));
+            op_names.push_back(builtin_name(get_name(OP_MINIMIZE).bare_str(), OP_MINIMIZE));
+            op_names.push_back(builtin_name(get_name(OP_LEX).bare_str(), OP_LEX));
+            op_names.push_back(builtin_name(get_name(OP_BOX).bare_str(), OP_BOX));
+            op_names.push_back(builtin_name(get_name(OP_PARETO).bare_str(), OP_PARETO));
+        }
+    }
+
+
+    objective_util::objective_util(ast_manager& m): m(m), m_fid(m.get_family_id("objective")) {}
+
+    app* objective_util::mk_max(expr_ref& e) {
+        expr* es[1] = { e };
+        return m.mk_app(m_fid, OP_MAXIMIZE, 0, 0, 1, es);
+    }
+    app* objective_util::mk_min(expr_ref& e) {
+        expr* es[1] = { e };
+        return m.mk_app(m_fid, OP_MINIMIZE, 0, 0, 1, es);
+    }
+    app* objective_util::mk_maxsat(symbol id) {
+        return m.mk_const(id, m.mk_sort(m_fid, OBJECTIVE_SORT, 0, 0));
+    }
+    app* objective_util::mk_lex(unsigned sz, expr * const * children) {
+        return m.mk_app(m_fid, OP_LEX, 0, 0, sz, children);
+    }
+    app* objective_util::mk_box(unsigned sz, expr * const * children) {
+        return m.mk_app(m_fid, OP_BOX, 0, 0, sz, children);
+    }
+    app* objective_util::mk_pareto(unsigned sz, expr * const * children) {
+        return m.mk_app(m_fid, OP_PARETO, 0, 0, sz, children);
+    }
+    
+}

src/opt/objective_decl_plugin.h

@@ -0,0 +1,71 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    objective_decl_plugin.h
+
+Abstract:
+    Abstract data-type for compound objectives.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-11-21
+
+Notes:
+
+--*/
+#ifndef __OBJECTIVE_DECL_PLUGIN_H_
+#define __OBJECTIVE_DECL_PLUGIN_H_
+
+#include"ast.h"
+
+namespace opt {
+
+    enum obj_kind {
+        OP_MINIMIZE, 
+        OP_MAXIMIZE,
+        OP_LEX,
+        OP_BOX,
+        OP_PARETO,
+        LAST_OBJ_OP
+    };
+
+    enum objective_sort_kind {
+        OBJECTIVE_SORT
+    };
+    
+    class objective_decl_plugin : public decl_plugin {
+    public:
+        objective_decl_plugin();
+        virtual ~objective_decl_plugin();
+        
+        virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
+
+        virtual decl_plugin * mk_fresh() { return alloc(objective_decl_plugin); }
+        
+        virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+                                         unsigned arity, sort * const * domain, sort * range);
+
+        virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);        
+
+    private:
+        symbol objective_decl_plugin::get_name(obj_kind k) const;
+    };
+
+    class objective_util {
+        ast_manager& m;
+        family_id m_fid;
+    public:
+        objective_util(ast_manager& m);
+        family_id get_family_id() const { return m_fid; }
+        app* mk_max(expr_ref& e);
+        app* mk_min(expr_ref& e);
+        app* mk_maxsat(symbol id);
+        app* mk_lex(unsigned sz, expr * const * children);
+        app* mk_box(unsigned sz, expr * const * children);
+        app* mk_pareto(unsigned sz, expr * const * children);
+    };
+};
+
+#endif

src/opt/opt_cmds.cpp

@@ -30,6 +30,7 @@ Notes:
 #include "scoped_timer.h"
 #include "parametric_cmd.h"
 #include "objective_ast.h"
+#include "objective_decl_plugin.h"
 
 class opt_context {
     cmd_context& ctx;
@@ -39,6 +40,8 @@ public:
     opt::context& operator()() { 
         if (!m_opt) {
             m_opt = alloc(opt::context, ctx.m());
+            decl_plugin * p = alloc(opt::objective_decl_plugin);
+            ctx.register_plugin(symbol("objective"), p, true);            
         }
         return *m_opt;
     }
@@ -251,12 +254,13 @@ private:
 
 class execute_cmd : public parametric_cmd {
 protected:
-    sexpr * m_objective;
+    expr * m_objective;
     opt_context& m_opt_ctx;
 public:
     execute_cmd(opt_context& opt_ctx):
         parametric_cmd("optimize"),
-        m_opt_ctx(opt_ctx)
+        m_opt_ctx(opt_ctx),
+        m_objective(0)
     {}
 
     virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
@@ -270,19 +274,26 @@ public:
     virtual char const * get_usage() const { return "(<keyword> <value>)*"; }
     virtual void prepare(cmd_context & ctx) {
         parametric_cmd::prepare(ctx);
-        m_objective = 0;
+        reset(ctx);
     }
     virtual void failure_cleanup(cmd_context & ctx) {
         reset(ctx);
     }
+    virtual void reset(cmd_context& ctx) {
+        if (m_objective) {
+            ctx.m().dec_ref(m_objective);
+        }
+        m_objective = 0;
+    }
 
     virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
-        if (m_objective == 0) return CPK_SEXPR;
+        if (m_objective == 0) return CPK_EXPR;
         return parametric_cmd::next_arg_kind(ctx);
     }
 
-    virtual void set_next_arg(cmd_context & ctx, sexpr * arg) {
+    virtual void set_next_arg(cmd_context & ctx, expr * arg) {
         m_objective = arg;
+        ctx.m().inc_ref(arg);
     }
 
     virtual void execute(cmd_context & ctx) {
@@ -303,9 +314,7 @@ public:
             scoped_timer timer(timeout, &eh);
             cmd_context::scoped_watch sw(ctx);
             try {
-                opt::objective * o = sexpr2objective(ctx, *m_objective);
+                r = opt.optimize(m_objective);
-                r = opt.optimize(*o);
-                dealloc(o);
             }
             catch (z3_error& ex) {
                 ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl;
@@ -343,6 +352,18 @@ private:
         m_opt_ctx().collect_statistics(stats);
         stats.display_smt2(ctx.regular_stream());        
     }
+};
+
+void install_opt_cmds(cmd_context & ctx) {
+    opt_context* opt_ctx = alloc(opt_context, ctx);
+    ctx.insert(alloc(assert_weighted_cmd, ctx, *opt_ctx));
+    ctx.insert(alloc(execute_cmd, *opt_ctx));
+    //ctx.insert(alloc(min_maximize_cmd, ctx, *opt_ctx, true));
+    //ctx.insert(alloc(min_maximize_cmd, ctx, *opt_ctx, false));
+    //ctx.insert(alloc(optimize_cmd, *opt_ctx));
+}
+
+#if 0
 
     expr_ref sexpr2expr(cmd_context & ctx, sexpr& s) {
         expr_ref result(ctx.m());
@@ -370,17 +391,18 @@ private:
             ctx.mk_const(s.get_symbol(), result);
             return result;
         }
+        return result;
     }
 
     opt::objective_t get_objective_type(sexpr& s) {
         if (!s.is_symbol())
             throw cmd_exception("invalid objective, symbol expected", s.get_line(), s.get_pos());
         symbol const & sym = s.get_symbol();
-        if (sym == symbol("maximize")) return opt::objective_t::MAXIMIZE;
+        if (sym == symbol("maximize")) return opt::MAXIMIZE;
-        if (sym == symbol("minimize")) return opt::objective_t::MINIMIZE;
+        if (sym == symbol("minimize")) return opt::MINIMIZE;
-        if (sym == symbol("lex")) return opt::objective_t::LEX;
+        if (sym == symbol("lex")) return opt::LEX;
-        if (sym == symbol("box")) return opt::objective_t::BOX;
+        if (sym == symbol("box")) return opt::BOX;
-        if (sym == symbol("pareto")) return opt::objective_t::PARETO;
+        if (sym == symbol("pareto")) return opt::PARETO;
         throw cmd_exception("invalid objective, unexpected input", s.get_line(), s.get_pos());
     }
 
@@ -435,13 +457,4 @@ private:
         return 0;
     }
 
-};
+#endif
-
-void install_opt_cmds(cmd_context & ctx) {
-    opt_context* opt_ctx = alloc(opt_context, ctx);
-    ctx.insert(alloc(assert_weighted_cmd, ctx, *opt_ctx));
-    ctx.insert(alloc(execute_cmd, *opt_ctx));
-    //ctx.insert(alloc(min_maximize_cmd, ctx, *opt_ctx, true));
-    //ctx.insert(alloc(min_maximize_cmd, ctx, *opt_ctx, false));
-    //ctx.insert(alloc(optimize_cmd, *opt_ctx));
-}

src/opt/opt_context.cpp

@@ -28,7 +28,8 @@ namespace opt {
         m(m),
         m_hard_constraints(m),
         m_optsmt(m),
-        m_objs(m)
+        m_objs(m),
+        m_obj_util(m)
     {
         m_params.set_bool("model", true);
         m_params.set_bool("unsat_core", true);
@@ -51,66 +52,74 @@ namespace opt {
         ms->add(f, w);
     }
 
-    lbool context::execute(objective & obj, bool committed) {
+    lbool context::execute(expr* _obj, bool committed) {
-        switch (obj.type()) {
+        SASSERT(is_app(_obj));
-        case MINIMIZE:
+        app* obj = to_app(_obj);
-        case MAXIMIZE: 
+
-            return execute_min_max(obj.get_min_max(), committed);
+        if (obj->get_family_id() == null_family_id) {
-        case MAXSAT:
+            return execute_maxsat(obj, committed);
-            return execute_maxsat(obj.get_maxsat(), committed);
+        }
-        case LEX:
+        if (obj->get_family_id() != m_obj_util.get_family_id()) {
-            return execute_lex(obj.get_compound());
+            // error
-        case BOX:
+            return l_undef;
-            return execute_box(obj.get_compound());
+        }
-        case PARETO:
+
-            return execute_pareto(obj.get_compound());
+        switch (obj->get_decl_kind()) {
+        case OP_MINIMIZE:
+        case OP_MAXIMIZE: 
+            return execute_min_max(obj, committed);
+        case OP_LEX:
+            return execute_lex(obj);
+        case OP_BOX:
+            return execute_box(obj);
+        case OP_PARETO:
+            return execute_pareto(obj);
         default:
             UNREACHABLE();
             return l_undef;
         }
     }
 
-    lbool context::execute_min_max(min_max_objective & obj, bool committed) {
+    lbool context::execute_min_max(app* obj, bool committed) {
         // HACK: reuse m_optsmt but add only a single objective each round
-        m_optsmt.add(to_app(obj.term()), obj.is_max());
+        bool is_max = (obj->get_decl_kind() == OP_MAXIMIZE);
+        m_optsmt.add(to_app(obj->get_arg(0)), is_max);
         opt_solver& s = *m_solver.get();
         lbool result = m_optsmt(s);
         if (committed) m_optsmt.commit_assignment(0);
         return result;
     }
 
-    lbool context::execute_maxsat(maxsat_objective & obj, bool committed) {
+    lbool context::execute_maxsat(app* obj, bool committed) {
         maxsmt* ms;
-        SASSERT(m_maxsmts.find(obj.get_id(), ms));
+        VERIFY(m_maxsmts.find(obj->get_decl()->get_name(), ms));
         opt_solver& s = *m_solver.get();
         lbool result = (*ms)(s);
         if (committed) ms->commit_assignment();
         return result;
     }
     
-    lbool context::execute_lex(compound_objective & obj) {
+    lbool context::execute_lex(app* obj) {
-        ptr_vector<objective> children(obj.num_children(), obj.children());
         lbool result = l_true;
-        for (unsigned i = 0; i < children.size(); ++i) {
+        for (unsigned i = 0; i < obj->get_num_args(); ++i) {
-            result = execute(*children[i], true);
+            result = execute(obj->get_arg(i), true);
             if (result != l_true) break;
         }
         return result;
     }    
 
-    lbool context::execute_box(compound_objective & obj) {
+    lbool context::execute_box(app* obj) {
-        ptr_vector<objective> children(obj.num_children(), obj.children());
         lbool result = l_true;
-        for (unsigned i = 0; i < children.size(); ++i) {
+        for (unsigned i = 0; i < obj->get_num_args(); ++i) {
             push();
-            result = execute(*children[i], false);
+            result = execute(obj->get_arg(i), false);
             pop(1);
             if (result != l_true) break;
         }
         return result;
     }
 
-    lbool context::execute_pareto(compound_objective & obj) {
+    lbool context::execute_pareto(app* obj) {
         // TODO: record a stream of results from pareto front
         return execute_lex(obj);
     }
@@ -125,7 +134,7 @@ namespace opt {
         s.pop(sz);
     }
 
-    lbool context::optimize(objective & objective) {
+    lbool context::optimize(expr* objective) {
         opt_solver& s = *m_solver.get(); 
         solver::scoped_push _sp(s);
 
@@ -138,29 +147,27 @@ namespace opt {
 
     lbool context::optimize() {
         // Construct objectives
-        ptr_vector<objective> objectives;
+        expr_ref_vector objectives(m);
+        expr_ref objective(m);
+        objective_util util(m);
         map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
         for (; it != end; ++it) {
-            objectives.push_back(objective::mk_maxsat(it->m_key));
+            objectives.push_back(util.mk_maxsat(it->m_key));
         }
 
         for (unsigned i = 0; i < m_objs.size(); ++i) {
             expr_ref e(m_objs[i].get(), m);
-            objective * o = m_ismaxs[i] ? objective::mk_max(e) : objective::mk_min(e);
+            app * o = m_ismaxs[i] ? util.mk_max(e) : util.mk_min(e);
             objectives.push_back(o);
         }
 
-        objective * objective;
         if (m_params.get_bool("pareto", false)) {            
-            objective = objective::mk_pareto(objectives.size(), objectives.c_ptr());
+            objective = util.mk_pareto(objectives.size(), objectives.c_ptr());
         }
         else {
-            objective = objective::mk_box(objectives.size(), objectives.c_ptr());
+            objective = util.mk_box(objectives.size(), objectives.c_ptr());
         }
-
+        return optimize(objective);
-        lbool result = optimize(*objective);
-        dealloc(objective);
-        return result;
     }
 
     void context::display_assignment(std::ostream& out) {

src/opt/opt_context.h

@@ -29,7 +29,7 @@ Notes:
 #include "opt_solver.h"
 #include "optsmt.h"
 #include "maxsmt.h"
-#include "objective_ast.h"
+#include "objective_decl_plugin.h"
 
 namespace opt {
 
@@ -45,6 +45,7 @@ namespace opt {
         map_t               m_maxsmts;
         expr_ref_vector     m_objs;
         svector<bool>       m_ismaxs;
+        objective_util      m_obj_util;
     public:
         context(ast_manager& m);
         ~context();
@@ -52,17 +53,17 @@ namespace opt {
         void add_objective(app* t, bool is_max) { m_objs.push_back(t); m_ismaxs.push_back(is_max); }
         void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f);  }
 
-        lbool execute(objective & obj, bool committed);
+        lbool execute(expr* obj, bool committed);
-        lbool execute_min_max(min_max_objective & obj, bool committed);
+        lbool execute_min_max(app* obj, bool committed);
-        lbool execute_maxsat(maxsat_objective & obj, bool committed);
+        lbool execute_maxsat(app* obj, bool committed);
-        lbool execute_lex(compound_objective & obj);
+        lbool execute_lex(app* obj);
-        lbool execute_box(compound_objective & obj);
+        lbool execute_box(app* obj);
-        lbool execute_pareto(compound_objective & obj);
+        lbool execute_pareto(app* obj);
 
         void push();
         void pop(unsigned sz);
 
-        lbool optimize(objective & objective);
+        lbool optimize(expr* objective);
         lbool optimize();
 
         void set_cancel(bool f);