remove dependency on ast from params

scripts/mk_project.py

@@ -23,12 +23,12 @@ def init_project_def():
     add_lib('realclosure', ['interval'], 'math/realclosure')
     add_lib('subpaving', ['interval'], 'math/subpaving')
     add_lib('ast', ['util', 'polynomial'])
-    add_lib('params', ['ast', 'util'])
+    add_lib('params', ['util'])
     add_lib('euf', ['ast', 'util'], 'ast/euf')
     add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner')    
     add_lib('sat', ['util', 'dd', 'grobner'])    
     add_lib('nlsat', ['polynomial', 'sat'])
-    add_lib('smt_params', ['ast', 'params'], 'smt/params')
+    add_lib('smt_params', ['params'], 'smt/params')
     add_lib('lp', ['util', 'nlsat', 'grobner', 'interval', 'smt_params'], 'math/lp')
     add_lib('rewriter', ['ast', 'polynomial', 'automata', 'params'], 'ast/rewriter')
     add_lib('macros', ['rewriter'], 'ast/macros')

src/api/api_config_params.cpp

@@ -24,7 +24,6 @@ Revision History:
 #include "util/symbol.h"
 #include "util/gparams.h"
 #include "util/env_params.h"
-#include "params/context_params.h"
 
 extern "C" {
     void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value) {
@@ -71,7 +70,7 @@ extern "C" {
         try {
             memory::initialize(UINT_MAX);
             LOG_Z3_mk_config();
-            Z3_config r = reinterpret_cast<Z3_config>(alloc(context_params));
+            Z3_config r = reinterpret_cast<Z3_config>(alloc(ast_context));
             RETURN_Z3(r);
         } catch (z3_exception & ex) {
             // The error handler is only available for contexts
@@ -83,13 +82,13 @@ extern "C" {
     
     void Z3_API Z3_del_config(Z3_config c) {
         LOG_Z3_del_config(c);
-        dealloc((reinterpret_cast<context_params*>(c)));
+        dealloc((reinterpret_cast<ast_context*>(c)));
     }
     
     void Z3_API Z3_set_param_value(Z3_config c, char const * param_id, char const * param_value) {
         LOG_Z3_set_param_value(c, param_id, param_value);
         try {
-            context_params * p = reinterpret_cast<context_params*>(c);
+            ast_context * p = reinterpret_cast<ast_context*>(c);
             p->set(param_id, param_value);
         }
         catch (z3_exception & ex) {

src/api/api_context.cpp

@@ -70,8 +70,8 @@ namespace api {
     //
     // ------------------------
 
-    context::context(context_params * p, bool user_ref_count):
+    context::context(ast_context * p, bool user_ref_count):
-        m_params(p != nullptr ? *p : context_params()),
+        m_params(p != nullptr ? *p : ast_context()),
         m_user_ref_count(user_ref_count),
         m_manager(m_params.mk_ast_manager()),
         m_plugins(m()),
@@ -343,7 +343,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_context(c);
         memory::initialize(UINT_MAX);
-        Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), false));
+        Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<ast_context*>(c), false));
         RETURN_Z3(r);
         Z3_CATCH_RETURN_NO_HANDLE(nullptr);
     }
@@ -352,7 +352,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_context_rc(c);
         memory::initialize(UINT_MAX);
-        Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), true));
+        Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<ast_context*>(c), true));
         RETURN_Z3(r);
         Z3_CATCH_RETURN_NO_HANDLE(nullptr);
     }

src/api/api_context.h

@@ -36,7 +36,6 @@ Revision History:
 #include "smt/smt_kernel.h"
 #include "smt/smt_solver.h"
 #include "cmd_context/tactic_manager.h"
-#include "params/context_params.h"
 #include "cmd_context/cmd_context.h"
 #include "solver/solver.h"
 #include "api/z3.h"
@@ -74,7 +73,7 @@ namespace api {
 
     class context : public tactic_manager {
         struct add_plugins {  add_plugins(ast_manager & m); };
-        context_params             m_params;
+        ast_context                m_params;
         bool                       m_user_ref_count; //!< if true, the user is responsible for managing reference counters.
         scoped_ptr<ast_manager>    m_manager;
         scoped_ptr<cmd_context>    m_cmd;
@@ -136,11 +135,11 @@ namespace api {
         //
         // ------------------------
         
-        context(context_params * p, bool user_ref_count = false);
+        context(ast_context * p, bool user_ref_count = false);
         ~context();
         ast_manager & m() const { return *(m_manager.get()); }
 
-        context_params & params() { m_params.updt_params(); return m_params; }
+        ast_context & params() { m_params.updt_params(); return m_params; }
         scoped_ptr<cmd_context>& cmd() { return m_cmd; }
         bool produce_proofs() const { return m().proofs_enabled(); }
         bool produce_models() const { return m_params.m_model; }

src/api/api_solver.cpp

@@ -876,7 +876,7 @@ extern "C" {
         solver::push_eh_t _push = push_eh;
         solver::pop_eh_t _pop = pop_eh;
         solver::fresh_eh_t _fresh = [&](void * user_ctx, ast_manager& m, solver::context_obj*& _ctx) {
-            context_params params;
+            ast_context params;
             params.set_foreign_manager(&m);
             auto* ctx = alloc(api::context, &params, false);
             _ctx = alloc(api_context_obj, ctx);

src/cmd_context/cmd_context.cpp

@@ -280,6 +280,20 @@ void macro_decls::erase_last(ast_manager& m) {
     m_decls->pop_back();
 }
 
+ast_manager * ast_context::mk_ast_manager() {
+    if (m_manager)
+        return m_manager;
+    ast_manager * r = alloc(ast_manager,
+                            m_proof ? PGM_ENABLED : PGM_DISABLED,
+                            m_trace ? m_trace_file_name.c_str() : nullptr);
+    if (m_smtlib2_compliant)
+        r->enable_int_real_coercions(false);
+    if (m_debug_ref_count)
+        r->debug_ref_count();
+    return r;
+}
+
+
 bool cmd_context::contains_func_decl(symbol const& s, unsigned n, sort* const* domain, sort* range) const {
     func_decls fs;
     return m_func_decls.find(s, fs) && fs.contains(n, domain, range);
@@ -1889,6 +1903,8 @@ void cmd_context::validate_model() {
                 if (m().is_true(r))
                     continue;
 
+                TRACE("model_validate", tout << *md << "\n";);
+
                 // The evaluator for array expressions is not complete
                 // If r contains as_array/store/map/const expressions, then we do not generate the error.
                 // TODO: improve evaluator for model expressions.
@@ -1897,7 +1913,8 @@ void cmd_context::validate_model() {
                     continue;
                 }
                 try {
-                    for_each_expr(contains_underspecified, a);
+                    if (!m().is_false(r))
+                        for_each_expr(contains_underspecified, a);
                     for_each_expr(contains_underspecified, r);
                 }
                 catch (const contains_underspecified_op_proc::found &) {

src/cmd_context/cmd_context.h

@@ -160,6 +160,18 @@ public:
     virtual void updt_params(params_ref const& p) = 0;
 };
 
+class ast_context : public context_params { 
+    ast_manager* m_manager { nullptr };
+public:
+    /**
+       \brief Create an AST manager using this configuration.
+    */
+    ast_manager * mk_ast_manager();
+
+    void set_foreign_manager(ast_manager* m) { m_manager = m; }
+    bool owns_manager() const { return m_manager != nullptr; }
+};
+
 class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {
 public:
     enum status {
@@ -179,8 +191,10 @@ public:
         ~scoped_watch() { m_ctx.m_watch.stop(); }
     };
 
+    
+
 protected:
-    context_params               m_params;
+    ast_context                  m_params;
     bool                         m_main_ctx;
     symbol                       m_logic;
     bool                         m_interactive_mode;

src/params/CMakeLists.txt

@@ -4,7 +4,6 @@ z3_add_component(params
     context_params.cpp
   COMPONENT_DEPENDENCIES
     util
-    ast
   PYG_FILES
     arith_rewriter_params.pyg
     array_rewriter_params.pyg

src/params/context_params.cpp

@@ -19,7 +19,6 @@ Notes:
 --*/
 #include "util/gparams.h"
 #include "util/params.h"
-#include "ast/ast.h"
 #include "params/context_params.h"
 
 context_params::context_params() {
@@ -194,17 +193,5 @@ void context_params::get_solver_params(params_ref & p, bool & proofs_enabled, bo
     p = merge_default_params(p);
 }
 
-ast_manager * context_params::mk_ast_manager() {
-    if (m_manager)
-        return m_manager;
-    ast_manager * r = alloc(ast_manager,
-                            m_proof ? PGM_ENABLED : PGM_DISABLED,
-                            m_trace ? m_trace_file_name.c_str() : nullptr);
-    if (m_smtlib2_compliant)
-        r->enable_int_real_coercions(false);
-    if (m_debug_ref_count)
-        r->debug_ref_count();
-    return r;
-}
 
 

src/params/context_params.h

@@ -20,14 +20,12 @@ Notes:
 #pragma once
 
 #include "util/params.h"
-class ast_manager;
 
 class context_params {
     void set_bool(bool & opt, char const * param, char const * value);
     void set_uint(unsigned & opt, char const * param, char const * value);
 
     unsigned    m_rlimit { 0 };
-    ast_manager* m_manager { nullptr };
 
 public:
     bool        m_auto_config { true };
@@ -71,13 +69,7 @@ public:
     */
     params_ref merge_default_params(params_ref const & p);
 
-    /**
-       \brief Create an AST manager using this configuration.
-    */
-    ast_manager * mk_ast_manager();
 
-    void set_foreign_manager(ast_manager* m) { m_manager = m; }
-    bool owns_manager() const { return m_manager != nullptr; }
 };
 
 

src/sat/smt/array_axioms.cpp

@@ -128,7 +128,6 @@ namespace array {
             r.set_delayed();
             return false;
         }
-        r.set_applied();
         if (a.is_const(child))
             return assert_select_const_axiom(select, to_app(child));
         else if (a.is_as_array(child))
@@ -205,12 +204,6 @@ namespace array {
         if (s().value(sel_eq) == l_true)
             return false;
 
-#if 0
-        static unsigned count = 0;
-        ++count;
-        std::cout << count << " " << sel_eq << "\n";
-#endif
-
         bool new_prop = false;
         for (unsigned i = 1; i < num_args; i++) {
             expr* idx1 = store->get_arg(i);
@@ -238,6 +231,7 @@ namespace array {
      *    select(const(v), i) = v
      */
     bool solver::assert_select_const_axiom(app* select, app* cnst) {
+        
         ++m_stats.m_num_select_const_axiom;
         expr* val = nullptr;
         VERIFY(a.is_const(cnst, val));

src/sat/smt/euf_model.cpp

@@ -73,7 +73,7 @@ namespace euf {
         values2model(deps, mdl);
         for (auto* mb : m_solvers)
             mb->finalize_model(*mdl);
-        // validate_model(*mdl);
+        validate_model(*mdl);
     }
 
     bool solver::include_func_interp(func_decl* f) {

src/sat/smt/euf_solver.cpp

@@ -308,7 +308,7 @@ namespace euf {
             euf::enode* nb = n->get_arg(1);
             m_egraph.merge(na, nb, c);
         }
-        else if (n->merge_enabled() && n->num_parents() > 0) {
+        else if (n->merge_enabled() && (n->num_parents() > 0 || n->num_args() > 0)) {
             euf::enode* nb = sign ? mk_false() : mk_true();
             m_egraph.merge(n, nb, c);
         }