add rewriter and seq simplifiers

scripts/mk_project.py

@@ -20,26 +20,27 @@ def init_project_def():
     add_lib('simplex', ['util'], 'math/simplex')
     add_lib('hilbert', ['util'], 'math/hilbert')
     add_lib('automata', ['util'], 'math/automata')
+    add_lib('params', ['util'])
+    add_lib('smt_params', ['params'], 'smt/params')
     add_lib('realclosure', ['interval'], 'math/realclosure')
     add_lib('subpaving', ['interval'], 'math/subpaving')
     add_lib('ast', ['util', 'polynomial'])
-    add_lib('euf', ['ast', 'util'], 'ast/euf')
-    add_lib('params', ['util'])
-    add_lib('smt_params', ['params'], 'smt/params')
+    add_lib('parser_util', ['ast'], 'parsers/util')
+    add_lib('euf', ['ast'], 'ast/euf')
     add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner')    
     add_lib('sat', ['params', 'util', 'dd', 'grobner'])    
     add_lib('nlsat', ['polynomial', 'sat'])
     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')
-    add_lib('model', ['rewriter', 'macros'])
-    add_lib('converters', ['model'], 'ast/converters')
-    add_lib('simplifiers', ['euf', 'rewriter', 'converters'], 'ast/simplifiers')
+    add_lib('bit_blaster',  ['rewriter'], 'ast/rewriter/bit_blaster')
     add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
-    add_lib('tactic', ['ast', 'model', 'simplifiers'])
-    add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution')
-    add_lib('parser_util', ['ast'], 'parsers/util')
-    add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
+    add_lib('substitution', ['rewriter'], 'ast/substitution')
+    add_lib('proofs', ['rewriter'], 'ast/proofs')
+    add_lib('macros', ['rewriter'], 'ast/macros')
+    add_lib('model',  ['macros'])
+    add_lib('converters', ['model'], 'ast/converters')
+    add_lib('simplifiers', ['euf', 'rewriter', 'bit_blaster', 'converters'], 'ast/simplifiers')
+    add_lib('tactic', ['simplifiers'])
     add_lib('solver', ['params', 'model', 'tactic', 'proofs'])
     add_lib('cmd_context', ['solver', 'rewriter', 'params'])
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
@@ -47,7 +48,6 @@ def init_project_def():
     add_lib('aig_tactic', ['tactic'], 'tactic/aig')
     add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
     add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
-    add_lib('bit_blaster', ['rewriter', 'params'], 'ast/rewriter/bit_blaster')
     add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
     add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
     add_lib('mbp', ['model', 'simplex'], 'qe/mbp')

src/CMakeLists.txt

@@ -46,6 +46,7 @@ add_subdirectory(math/subpaving)
 add_subdirectory(ast)
 add_subdirectory(params)
 add_subdirectory(ast/rewriter)
+add_subdirectory(ast/rewriter/bit_blaster)
 add_subdirectory(ast/normal_forms)
 add_subdirectory(ast/macros)
 add_subdirectory(model)
@@ -71,7 +72,6 @@ add_subdirectory(qe/mbp)
 add_subdirectory(qe/lite)
 add_subdirectory(solver/assertions)
 add_subdirectory(ast/pattern)
-add_subdirectory(ast/rewriter/bit_blaster)
 add_subdirectory(math/lp)
 add_subdirectory(sat/smt)
 add_subdirectory(sat/tactic)

src/ast/simplifiers/CMakeLists.txt

@@ -15,4 +15,5 @@ z3_add_component(simplifiers
   COMPONENT_DEPENDENCIES
     euf
     rewriter
+    bit_blaster
 )

src/ast/simplifiers/card2bv.cpp

@@ -49,7 +49,7 @@ void card2bv::reduce() {
     for (func_decl* f : fns)
         m_fmls.model_trail().hide(f);    
 
-    advance_qhead(m_fmls.size());
+     advance_qhead(m_fmls.size());
 }
 
 void card2bv::collect_statistics(statistics& st) const {

src/ast/simplifiers/rewriter_simplifier.h

@@ -0,0 +1,53 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    rewriter_simplifier.h
+
+Abstract:
+
+    rewriter simplifier
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/th_rewriter.h"
+
+
+class rewriter_simplifier : public dependent_expr_simplifier {
+
+    unsigned               m_num_steps = 0;
+    params_ref             m_params;
+
+public:
+    rewriter_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls) {
+        updt_params(p);
+    }
+        
+    void reduce() override {
+        m_num_steps = 0;
+        expr_ref   new_curr(m);
+        proof_ref  new_pr(m);
+        for (unsigned idx = m_qhead; idx < m_fmls.size(); idx++) {
+            if (m_fmls.inconsistent())
+                break;
+            auto [f, d] = m_fmls[i]();
+            m_rewriter(f, new_curr, new_pr);
+            m_num_steps += m_rewriter.get_num_steps();
+            m_fmls.update(idx, dependent_expr(m, new_curr, d));            
+        }
+        advance_qhead(m_fmls.size());
+    }
+    void collect_statistics(statistics& st) const override { st.update("simplifier", m_num_steps); }
+    void reset_statistics() override { m_stats.reset(); }
+    void updt_params(params_ref const& p) override { m_params.append(p); m_rewriter.updt_params(m_params); }
+    void collect_param_descrs(param_descrs& r) override { th_rewriter::get_param_descrs(r); }
+};

src/ast/simplifiers/seq_simplifier.h

@@ -0,0 +1,72 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    seq_simplifier.h
+
+Abstract:
+
+    create a simplifier from a sequence of simplifiers
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+
+
+class seq_simplifier : public dependent_expr_simplifier {
+    scoped_ptr_vector<dependent_expr_simplifier> m_simplifiers;
+
+public:
+    seq_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls) {
+    }
+    
+    void add_simplifier(dependent_expr_simplifier* s) {
+        m_simplifiers.push_back(s);
+    }
+        
+    void reduce() override {
+        for (auto* s : m_simplifiers) {
+            if (m_fmls.inconsistent())
+                break;
+            s->reduce();
+        }
+    }
+    
+    void collect_statistics(statistics& st) const override {
+        for (auto* s : m_simplifiers)
+            s->collect_statistics(st);
+    }
+    
+    void reset_statistics() override {
+        for (auto* s : m_simplifiers)
+            s->reset_statistics(st);
+    }
+    
+    void updt_params(params_ref const& p) override {
+        for (auto* s : m_simplifiers)
+            s->updt_params(p);        
+    }
+    
+    void collect_param_descrs(param_descrs& r) override {
+        for (auto* s : m_simplifiers)
+            s->collect_param_descrs(r);
+    }
+    
+    void push() override {
+        for (auto* s : m_simplifiers)
+            s->push();       
+    }
+    
+    void pop(unsigned n) override {
+        for (auto* s : m_simplifiers)
+            s->pop(n);     
+    }
+};