add flag to control non-linear substitutions: smt.solve_eqs.linear is by default false, setting it to true restricts solutions to substitutions to only use linear terms. This can have an effect on cross-multiplication of nested substitutions

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

src/ast/simplifiers/solve_eqs.cpp

@@ -121,7 +121,10 @@ namespace euf {
                         continue;
 
                     if (!m_config.m_enable_non_ground && has_quantifiers(t)) 
-                        continue;                        
+                        continue;   
+
+                    if (!m_config.m_enable_non_linear && !is_linear(t))
+                        continue;
 
                     bool is_safe = true;                    
                     unsigned todo_sz = todo.size();
@@ -313,6 +316,15 @@ namespace euf {
         return num <= m_config.m_max_occs;
     }
 
+    bool solve_eqs::is_linear(expr* t) const {
+        unsigned num_values = 0;
+        if (!is_app(t))
+            return false;
+        for (auto arg : *to_app(t))
+            num_values += m.is_value(arg) ? 1 : 0;
+        return num_values <= 1;
+    }
+
     void solve_eqs::save_subst(vector<dependent_expr> const& old_fmls) {
         if (!m_subst->empty())   
             m_fmls.model_trail().push(m_subst.detach(), old_fmls, false);                
@@ -342,6 +354,7 @@ namespace euf {
         smt_params_helper sp(p);
         m_config.m_enabled = sp.solve_eqs();
         m_config.m_enable_non_ground = sp.solve_eqs_non_ground();
+        m_config.m_enable_non_linear = !sp.solve_eqs_linear();
     }
 
     void solve_eqs::collect_param_descrs(param_descrs& r) {

src/ast/simplifiers/solve_eqs.h

@@ -43,6 +43,7 @@ namespace euf {
             unsigned m_max_occs = UINT_MAX;
             bool m_enabled = true;
             bool m_enable_non_ground = true;
+            bool m_enable_non_linear = true;
         };
 
         stats                         m_stats;
@@ -74,6 +75,7 @@ namespace euf {
         void collect_num_occs(expr * t, expr_fast_mark1 & visited);
         void collect_num_occs();
         bool check_occs(expr* t) const;
+        bool is_linear(expr *t) const;
 
     public:
 

src/params/smt_params_helper.pyg

@@ -21,6 +21,7 @@ def_module_params(module_name='smt',
                           ('elim_unconstrained', BOOL, True, 'pre-processing: eliminate unconstrained subterms'),
                           ('solve_eqs', BOOL, True, 'pre-processing: solve equalities'),
                           ('solve_eqs.non_ground', BOOL, True, 'pre-processing: solve equalities. Allow eliminating variables by non-ground solutions which can break behavior for model evaluation.'),
+			  ('solve_eqs.linear', BOOL, False, 'allow only linear substitutions where a variable is replaced by a term having at most one non-constant argument'),
                           ('propagate_values', BOOL, True, 'pre-processing: propagate values'),
                           ('bound_simplifier', BOOL, True, 'apply bounds simplification during pre-processing'),
                           ('pull_nested_quantifiers', BOOL, False, 'pre-processing: pull nested quantifiers'),