port more from hybridSMT

Signed-off-by: Lev Nachmanson <[email protected]>

src/nlsat/CMakeLists.txt

@@ -7,7 +7,10 @@ z3_add_component(nlsat
     nlsat_simplify.cpp
     nlsat_solver.cpp
     nlsat_types.cpp
-  COMPONENT_DEPENDENCIES
+    nlsat_simple_checker.cpp
+    nlsat_variable_ordering_strategy.cpp
+    nlsat_symmetry_checker.cpp
+    COMPONENT_DEPENDENCIES
     polynomial
     sat
   PYG_FILES

src/nlsat/nlsat_params.pyg

@@ -3,7 +3,10 @@ def_module_params('nlsat',
                   description='nonlinear solver',
                   export=True,
                   params=(max_memory_param(),
+                          ('linxi_simple_check', BOOL, False, "linxi precheck about variables sign"),
+                          ('linxi_variable_ordering_strategy', UINT, 0, "linxi Variable Ordering Strategy, 0 for none, 1 for BROWN, 2 for TRIANGULAR, 3 for ONLYPOLY"),
                           ('cell_sample', BOOL, True, "cell sample projection"),
+                          ('linxi_symmetry_check', BOOL, False, "linxi symmetry check and learning"),
                           ('lazy', UINT, 0, "how lazy the solver is."),
                           ('reorder', BOOL, True, "reorder variables."),
                           ('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"),