add detection of non-fixed variables to consequence finding

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

src/api/api_opt.cpp

@@ -23,9 +23,10 @@ Revision History:
 #include"api_util.h"
 #include"api_model.h"
 #include"opt_context.h"
+#include"opt_cmds.h"
 #include"cancel_eh.h"
 #include"scoped_timer.h"
-
+#include"smt2parser.h"
 
 extern "C" {
 
@@ -248,6 +249,53 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    static void Z3_optimize_from_stream(
+        Z3_context    c,
+        Z3_optimize opt,
+        std::istream& s) {
+        ast_manager& m = mk_c(c)->m();
+        cmd_context ctx(false, &m);
+        install_opt_cmds(ctx, to_optimize_ptr(opt));
+        ctx.set_ignore_check(true);
+        if (!parse_smt2_commands(ctx, s)) {
+            SET_ERROR_CODE(Z3_PARSER_ERROR);
+            return;
+        }        
+        ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+        ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+        for (; it != end; ++it) {
+            to_optimize_ptr(opt)->add_hard_constraint(*it);
+        }
+    }
+
+    void Z3_API Z3_optimize_from_string(
+        Z3_context    c,
+        Z3_optimize   d,
+        Z3_string     s) {
+        Z3_TRY;
+        //LOG_Z3_optimize_from_string(c, d, s);
+        std::string str(s);
+        std::istringstream is(str);
+        Z3_optimize_from_stream(c, d, is);
+        Z3_CATCH;
+    }
+
+    void Z3_API Z3_optimize_from_file(
+        Z3_context    c,
+        Z3_optimize   d,
+        Z3_string     s) {
+        Z3_TRY;
+        //LOG_Z3_optimize_from_file(c, d, s);
+        std::ifstream is(s);
+        if (!is) {
+            SET_ERROR_CODE(Z3_PARSER_ERROR);
+            return;
+        }
+        Z3_optimize_from_stream(c, d, is);
+        Z3_CATCH;
+    }
+
+
 
 
 };

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

@@ -2035,6 +2035,8 @@ namespace z3 {
         }
         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(); }
+        void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
         std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error();  return r; }
     };
     inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }

src/api/dotnet/Optimize.cs

@@ -273,6 +273,25 @@ namespace Microsoft.Z3
             return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
         }
 
+        /// <summary>
+        /// Parse an SMT-LIB2 file with optimization objectives and constraints.
+        /// The parsed constraints and objectives are added to the optimization context.
+        /// </summary>                
+        public void FromFile(string file)
+        {
+            Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file);
+        }
+
+        /// <summary>
+        /// Similar to FromFile. Instead it takes as argument a string.
+        /// </summary>
+        public void FromString(string s)
+        {
+            Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s);
+        }
+
+
+
         /// <summary>
         /// Optimize statistics.
         /// </summary>

src/api/python/z3.py

@@ -6755,6 +6755,14 @@ class Optimize(Z3PPObject):
             raise Z3Exception("Expecting objective handle returned by maximize/minimize")
         return obj.upper()
 
+    def from_file(self, filename):
+        """Parse assertions and objectives from a file"""
+        Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
+
+    def from_string(self, s):
+        """Parse assertions and objectives from a string"""
+        Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
+
     def __repr__(self):
         """Return a formatted string with all added rules and constraints."""
         return self.sexpr()

src/api/z3_optimization.h

@@ -197,6 +197,34 @@ extern "C" {
     */
     Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o);
 
+    /**
+       \brief Parse an SMT-LIB2 string with assertions, 
+       soft constraints and optimization objectives.
+       Add the parsed constraints and objectives to the optimization context.
+
+       \param c - context.
+       \param o - optimize context.
+       \param s - string containing SMT2 specification.
+
+       def_API('Z3_optimize_from_string', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING)))
+    */
+    void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s);
+
+
+    /**
+       \brief Parse an SMT-LIB2 file with assertions, 
+       soft constraints and optimization objectives.
+       Add the parsed constraints and objectives to the optimization context.
+
+
+       \param c - context.
+       \param o - optimize context.
+       \param s - string containing SMT2 specification.
+
+       def_API('Z3_optimize_from_file', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING)))
+    */
+    void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s);
+
 
     /**
        \brief Return a string containing a description of parameters accepted by optimize.

src/muz/fp/dl_cmds.cpp

@@ -527,13 +527,8 @@ static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_c
     ctx.insert(alloc(dl_query_cmd, dl_ctx));
     ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx));
     ctx.insert(alloc(dl_declare_var_cmd, dl_ctx));
-    // #ifndef _EXTERNAL_RELEASE
+    ctx.insert(alloc(dl_push_cmd, dl_ctx)); 
-    // TODO: we need these!
-#if 1
-    ctx.insert(alloc(dl_push_cmd, dl_ctx)); // not exposed to keep command-extensions simple.
     ctx.insert(alloc(dl_pop_cmd, dl_ctx));
-#endif
-    // #endif
 }
 
 void install_dl_cmds(cmd_context & ctx) {

src/opt/opt_cmds.cpp

@@ -32,7 +32,10 @@ Notes:
 #include "opt_params.hpp"
 #include "model_smt2_pp.h"
 
-static opt::context& get_opt(cmd_context& cmd) {
+static opt::context& get_opt(cmd_context& cmd, opt::context* opt) {
+    if (opt) {
+        return *opt;
+    }
     if (!cmd.get_opt()) {
         cmd.set_opt(alloc(opt::context, cmd.m()));
     }
@@ -43,12 +46,14 @@ static opt::context& get_opt(cmd_context& cmd) {
 class assert_soft_cmd : public parametric_cmd {
     unsigned     m_idx;
     expr*        m_formula;
+    opt::context* m_opt;
 
 public:
-    assert_soft_cmd():
+    assert_soft_cmd(opt::context* opt):
         parametric_cmd("assert-soft"),
         m_idx(0),
-        m_formula(0)
+        m_formula(0),
+        m_opt(opt)
     {}
 
     virtual ~assert_soft_cmd() {
@@ -97,7 +102,7 @@ public:
             weight = rational::one();
         }
         symbol id = ps().get_sym(symbol("id"), symbol::null);        
-        get_opt(ctx).add_soft_constraint(m_formula, weight, id);
+        get_opt(ctx, m_opt).add_soft_constraint(m_formula, weight, id);
         reset(ctx);
     }
 
@@ -108,11 +113,13 @@ public:
 
 class min_maximize_cmd : public cmd {
     bool         m_is_max;
+    opt::context* m_opt;
 
 public:
-    min_maximize_cmd(bool is_max):
+    min_maximize_cmd(bool is_max, opt::context* opt):
         cmd(is_max?"maximize":"minimize"),
-        m_is_max(is_max)
+        m_is_max(is_max),
+        m_opt(opt)
     {}
 
     virtual void reset(cmd_context & ctx) { }
@@ -126,7 +133,7 @@ public:
         if (!is_app(t)) {
             throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable");
         }
-        get_opt(ctx).add_objective(to_app(t), m_is_max);
+        get_opt(ctx, m_opt).add_objective(to_app(t), m_is_max);
     }
 
     virtual void failure_cleanup(cmd_context & ctx) {
@@ -139,10 +146,10 @@ public:
 
 
 
-void install_opt_cmds(cmd_context & ctx) {
+void install_opt_cmds(cmd_context & ctx, opt::context* opt) {
-    ctx.insert(alloc(assert_soft_cmd));
+    ctx.insert(alloc(assert_soft_cmd, opt));
-    ctx.insert(alloc(min_maximize_cmd, true));
+    ctx.insert(alloc(min_maximize_cmd, true, opt));
-    ctx.insert(alloc(min_maximize_cmd, false));
+    ctx.insert(alloc(min_maximize_cmd, false, opt));
 }
 
 

src/opt/opt_cmds.h

@@ -19,10 +19,11 @@ Notes:
 #define OPT_CMDS_H_
 
 #include "ast.h"
+#include "opt_context.h"
 
 class cmd_context;
 
-void install_opt_cmds(cmd_context & ctx);
+void install_opt_cmds(cmd_context & ctx, opt::context* opt = 0);
 
 
 #endif

src/smt/smt_consequences.cpp

@@ -102,6 +102,47 @@ namespace smt {
         }
     }
 
+    void context::delete_unfixed(obj_map<expr, expr*>& var2val) {
+        ast_manager& m = m_manager;
+        ptr_vector<expr> to_delete;
+        obj_map<expr,expr*>::iterator it = var2val.begin(), end = var2val.end();
+        for (; it != end; ++it) {
+            expr* k = it->m_key;
+            expr* v = it->m_value;
+            if (m.is_bool(k)) {
+                literal lit = get_literal(k);
+                switch (get_assignment(lit)) {
+                case l_true: 
+                    if (m.is_false(v)) {
+                        to_delete.push_back(k);
+                    }
+                    else {
+                        force_phase(lit.var(), false);
+                    }
+                    break;
+                case l_false:
+                    if (m.is_true(v)) {
+                        to_delete.push_back(k);
+                    }
+                    else {
+                        force_phase(lit.var(), true);
+                    }
+                    break;
+                default:
+                    to_delete.push_back(k);
+                    break;
+                }
+            }
+            else if (e_internalized(k) && m.are_distinct(v, get_enode(k)->get_root()->get_owner())) {
+                to_delete.push_back(k);
+            }
+        }
+        IF_VERBOSE(1, verbose_stream() << "(get-consequences deleting: " << to_delete.size() << " num-values: " << var2val.size() << ")\n";);
+        for (unsigned i = 0; i < to_delete.size(); ++i) {
+            var2val.remove(to_delete[i]);
+        }
+    }
+
     lbool context::get_consequences(expr_ref_vector const& assumptions, 
                                     expr_ref_vector const& vars, expr_ref_vector& conseq) {
 
@@ -135,7 +176,10 @@ namespace smt {
               tout << "vars: " << vars.size() << "\n";
               tout << "lits: " << num_units << "\n";);
         m_case_split_queue->init_search_eh();
+        unsigned num_iterations = 0;
+        unsigned model_threshold = 2;
         while (!var2val.empty()) {
+            ++num_iterations;
             obj_map<expr,expr*>::iterator it = var2val.begin();
             expr* e = it->m_key;
             expr* val = it->m_value;
@@ -177,6 +221,17 @@ namespace smt {
             else {
                 TRACE("context", tout << "Fixed: " << mk_pp(e, m) << "\n";);
             }
+
+            TRACE("context", tout << "Unfixed variables: " << var2val.size() << "\n";);
+            if (model_threshold <= num_iterations) {
+                delete_unfixed(var2val);
+                // The next time we check the model is after 1.5 additional iterations.
+                model_threshold *= 3;
+                model_threshold /= 2;                
+            }
+            // repeat until we either have a model with negated literal or 
+            // the literal is implied at base.
+
             extract_fixed_consequences(num_units, var2val, _assumptions, conseq);
             num_units = assigned_literals().size();
             if (var2val.contains(e)) {
@@ -189,10 +244,8 @@ namespace smt {
                 SASSERT(get_assignment(lit) == l_false);
             }
         
-            // repeat until we either have a model with negated literal or 
-            // the literal is implied at base.
-            TRACE("context", tout << "Unfixed variables: " << var2val.size() << "\n";);
         }
+        end_search();
         return l_true;
     }
 

src/smt/smt_context.h

@@ -1345,7 +1345,9 @@ namespace smt {
             vector<bool_var> b2v, ast_translation& tr);
 
         u_map<uint_set> m_antecedents;
-        void extract_fixed_consequences(unsigned idx, obj_map<expr, expr*>& vars, uint_set const& assumptions, expr_ref_vector& conseq);
+        void extract_fixed_consequences(unsigned idx, obj_map<expr, expr*>& var2val, uint_set const& assumptions, expr_ref_vector& conseq);
+        
+        void delete_unfixed(obj_map<expr, expr*>& var2val);
 
         expr_ref antecedent2fml(uint_set const& ante);