Adding a model based axiom instantiation scheme for multiplication. Merge commit for nlAlgMaster.

1 files changed, 24 insertions, 0 deletions

diff --git a/src/options/arith_options b/src/options/arith_options
index f38e377ba..6f76758e3 100644
--- a/src/options/arith_options
+++ b/src/options/arith_options
@@ -165,4 +165,28 @@ option pbRewriteThreshold --pb-rewrite-threshold int :default 256
 option sNormInferEq --snorm-infer-eq bool :default false
  infer equalities based on Shostak normalization
 
+option nlAlg --nl-alg bool :default false
+ algebraic approach to non-linear
+ 
+option nlAlgResBound --nl-alg-rbound bool :default false
+ use resolution-style inference for inferring new bounds
+
+option nlAlgTangentPlanes --nl-alg-tplanes bool :default false
+ use non-terminating tangent plane strategy for non-linear
+
+option nlAlgEntailConflicts --nl-alg-ent-conf bool :default false
+ check for entailed conflicts in non-linear solver
+ 
+option nlAlgRewrites --nl-alg-rewrite bool :default true
+ do rewrites in non-linear solver
+ 
+option nlAlgSolveSubs --nl-alg-solve-subs bool :default true
+ do solving for determining constant substitutions
+ 
+option nlAlgPurify --nl-alg-purify bool :default false
+ purify non-linear terms at preprocess
+ 
+option nlAlgSplitZero --nl-alg-split-zero bool :default false
+ intial splits on zero for all variables
+
 endmodule