add parameter to disable pattern inference #6884

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 3, 2023 · 4d9af78 · 4d9af78 · utaal · Sep 5, 2023
1 parent 9923906
commit 4d9af78
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 10 deletions.
diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp
@@ -624,9 +624,11 @@ bool pattern_inference_cfg::reduce_quantifier(
     proof_ref & result_pr) {
 
     TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";);
-    if (!is_forall(q)) {
+    if (!m_params.m_pi_enabled)
+        return false;
+
+    if (!is_forall(q)) 
         return false;
-    }
 
     int weight = q->get_weight();
 
@@ -653,9 +655,8 @@ bool pattern_inference_cfg::reduce_quantifier(
         }
     }
 
-    if (q->get_num_patterns() > 0) {
+    if (q->get_num_patterns() > 0) 
         return false;
-    }
 
     if (m_params.m_pi_nopat_weight >= 0)
         weight = m_params.m_pi_nopat_weight;

diff --git a/src/params/pattern_inference_params.cpp b/src/params/pattern_inference_params.cpp
@@ -21,6 +21,7 @@ Revision History:
 
 void pattern_inference_params::updt_params(params_ref const & _p) {
     pattern_inference_params_helper p(_p);
+    m_pi_enabled                 = p.enabled();
     m_pi_max_multi_patterns      = p.max_multi_patterns();
     m_pi_block_loop_patterns     = p.block_loop_patterns();
     m_pi_decompose_patterns      = p.decompose_patterns();
@@ -35,6 +36,7 @@ void pattern_inference_params::updt_params(params_ref const & _p) {
 #define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void pattern_inference_params::display(std::ostream & out) const {
+    DISPLAY_PARAM(m_pi_enabled);
     DISPLAY_PARAM(m_pi_max_multi_patterns);
     DISPLAY_PARAM(m_pi_block_loop_patterns);
     DISPLAY_PARAM(m_pi_decompose_patterns);

diff --git a/src/params/pattern_inference_params.h b/src/params/pattern_inference_params.h
@@ -27,21 +27,20 @@ enum arith_pattern_inference_kind {
 };
 
 struct pattern_inference_params {
-    unsigned                      m_pi_max_multi_patterns; 
+    bool                          m_pi_enabled = true;
+    unsigned                      m_pi_max_multi_patterns = 1; 
     bool                          m_pi_block_loop_patterns; 
     bool                          m_pi_decompose_patterns;
     arith_pattern_inference_kind  m_pi_arith;
     bool                          m_pi_use_database;
     unsigned                      m_pi_arith_weight;
     unsigned                      m_pi_non_nested_arith_weight;
     bool                          m_pi_pull_quantifiers;
-    int                           m_pi_nopat_weight;
-    bool                          m_pi_avoid_skolems;
+    int                           m_pi_nopat_weight = -1;
+    bool                          m_pi_avoid_skolems = true;
     bool                          m_pi_warnings;
 
-    pattern_inference_params(params_ref const & p = params_ref()):
-        m_pi_nopat_weight(-1),
-        m_pi_avoid_skolems(true) {
+    pattern_inference_params(params_ref const & p = params_ref()) {
         updt_params(p);
     }
 

diff --git a/src/params/pattern_inference_params_helper.pyg b/src/params/pattern_inference_params_helper.pyg
@@ -7,6 +7,7 @@ def_module_params(class_name='pattern_inference_params_helper',
                           ('decompose_patterns', BOOL, True, 'allow decomposition of patterns into multipatterns'),
                           ('arith', UINT, 1, '0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms'),
                           ('use_database', BOOL, False, 'use pattern database'),
+                          ('enabled', BOOL, True, 'enable a heuristic to infer patterns, when they are not provided'),	
                           ('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'),
                           ('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pattern has non nested arithmetic terms'),
                           ('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),