add __copy__, __deepcopy__ as alias to translate on same context #1427. Add generalized Gaussian elimination as an option to first-pass NL solver

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

src/api/python/z3/z3.py

@@ -365,6 +365,12 @@ class AstRef(Z3PPObject):
             _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
         return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
 
+    def __copy__(self):
+        return self.translate(self.ctx)
+
+    def __deepcopy__(self):
+        return self.translate(self.ctx)
+
     def hash(self):
         """Return a hashcode for the `self`.
 
@@ -5048,6 +5054,12 @@ class Goal(Z3PPObject):
             _z3_assert(isinstance(target, Context), "target must be a context")
         return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target)
 
+    def __copy__(self):
+        return self.translate(self.ctx)
+
+    def __deepcopy__(self):
+        return self.translate(self.ctx)
+
     def simplify(self, *arguments, **keywords):
         """Return a new simplified goal.
 
@@ -5230,6 +5242,12 @@ class AstVector(Z3PPObject):
         """
         return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx)
 
+    def __copy__(self):
+        return self.translate(self.ctx)
+
+    def __deepcopy__(self):
+        return self.translate(self.ctx)
+
     def __repr__(self):
         return obj_to_string(self)
 
@@ -6430,6 +6448,12 @@ class Solver(Z3PPObject):
         solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
         return Solver(solver, target)
 
+    def __copy__(self):
+        return self.translate(self.ctx)
+
+    def __deepcopy__(self):
+        return self.translate(self.ctx)
+
     def sexpr(self):
         """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
 

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -1193,7 +1193,6 @@ bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const *
         return false;
     }
     SASSERT(out_bits.empty());
-    
     ptr_buffer<expr, 128> na_bits;
     na_bits.append(sz, a_bits);
     ptr_buffer<expr, 128> nb_bits;

src/nlsat/nlsat_params.pyg

@@ -10,6 +10,7 @@ def_module_params('nlsat',
                           ('randomize', BOOL, True, "randomize selection of a witness in nlsat."),
                           ('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts."),
                           ('shuffle_vars', BOOL, False, "use a random variable order."),
+                          ('inline_vars', BOOL, False, "inline variables that can be isolated from equations"),
                           ('seed', UINT, 0, "random seed."),
                           ('factor', BOOL, True, "factor polynomials produced during conflict resolution.")     
                           ))         

src/nlsat/nlsat_solver.cpp

@@ -154,6 +154,7 @@ namespace nlsat {
         bool                   m_randomize;
         bool                   m_random_order;
         unsigned               m_random_seed;
+        bool                   m_inline_vars;
         unsigned               m_max_conflicts;
 
         // statistics
@@ -210,6 +211,7 @@ namespace nlsat {
             m_max_conflicts  = p.max_conflicts();
             m_random_order   = p.shuffle_vars();
             m_random_seed    = p.seed();
+            m_inline_vars    = p.inline_vars();
             m_ism.set_seed(m_random_seed);
             m_explain.set_simplify_cores(m_simplify_cores);
             m_explain.set_minimize_cores(min_cores);
@@ -1313,11 +1315,8 @@ namespace nlsat {
             m_explain.set_full_dimensional(is_full_dimensional());
             bool reordered = false;
 
-#if 0
+            if (!m_incremental && m_inline_vars) 
-            // disabled
-            if (!m_incremental) 
                 simplify();
-#endif
 
             if (!can_reorder()) {
 

src/tactic/smtlogics/qfnra_tactic.cpp

@@ -33,7 +33,9 @@ static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigne
 }
 
 tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) {
-    params_ref p1 = p;
+    params_ref p0 = p;
+    p0.set_bool("inline_vars", true);
+    params_ref p1 = p;    
     p1.set_uint("seed", 11);
     p1.set_bool("factor", false);
     params_ref p2 = p;
@@ -42,7 +44,7 @@ tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) {
 
     return and_then(mk_simplify_tactic(m, p), 
                     mk_propagate_values_tactic(m, p),
-                    or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000),
+                    or_else(try_for(mk_qfnra_nlsat_tactic(m, p0), 5000),
                             try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
                             mk_qfnra_sat_solver(m, p, 4),
                             and_then(try_for(mk_smt_tactic(), 5000), mk_fail_if_undecided_tactic()),