From f0bdcbb3db67709ea68d2b88ae7765684a1cba02 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 19 Mar 2016 18:40:59 -0700
Subject: [PATCH] expose qsat tactic to default tactics

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/smtlogics/nra_tactic.cpp    | 11 ++++++++++-
 src/tactic/smtlogics/quant_tactics.cpp | 18 +++++++++++++++---
 2 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp
index 845b6bfec..2bb9ef75c 100644
--- a/src/tactic/smtlogics/nra_tactic.cpp
+++ b/src/tactic/smtlogics/nra_tactic.cpp
@@ -22,7 +22,9 @@ Notes:
 #include"smt_tactic.h"
 #include"nnf_tactic.h"
 #include"qe_tactic.h"
+#include"nlqsat.h"
 #include"qfnra_nlsat_tactic.h"
+#include"qe_lite.h"
 #include"probe_arith.h"
 
 tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
@@ -36,12 +38,19 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
     return and_then(mk_simplify_tactic(m, p),
                     mk_nnf_tactic(m, p),
                     mk_propagate_values_tactic(m, p),
+                    mk_qe_lite_tactic(m), 
                     mk_qe_tactic(m, p),
                     cond(mk_is_qfnra_probe(),
                          or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000),
                                  try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
                                  mk_qfnra_nlsat_tactic(m, p2)),
-                         mk_smt_tactic(p)));
+#if 0
+                         or_else(mk_nlqsat_tactic(m, p),
+                                 mk_smt_tactic(p))
+#else
+                         mk_smt_tactic(p)
+#endif
+                         ));
 }
 
 
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 8714b055f..8760d255e 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -23,6 +23,9 @@ Revision History:
 #include"elim_uncnstr_tactic.h"
 #include"qe_tactic.h"
 #include"qe_sat_tactic.h"
+#include"qe_lite.h"
+#include"qsat.h"
+#include"nlqsat.h"
 #include"ctx_simplify_tactic.h"
 #include"smt_tactic.h"
 
@@ -37,10 +40,12 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f
     ctx_simp_p.set_uint("max_steps", 5000000);
 
     tactic * solve_eqs;
-    if (disable_gaussian)
+    if (disable_gaussian) {
         solve_eqs = mk_skip_tactic();
-    else
+    }
+    else {
         solve_eqs = when(mk_not(mk_has_pattern_probe()), mk_solve_eqs_tactic(m));
+    }
  
     // remark: investigate if gaussian elimination is useful when patterns are not provided.
     return and_then(mk_simplify_tactic(m), 
@@ -49,6 +54,7 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f
                     using_params(mk_simplify_tactic(m), pull_ite_p),
                     solve_eqs,
                     mk_elim_uncnstr_tactic(m),
+                    mk_qe_lite_tactic(m),
                     mk_simplify_tactic(m));    
 }
 
@@ -98,13 +104,18 @@ tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) {
 }
 
 tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
+#if 0
     tactic * st = and_then(mk_quant_preprocessor(m),
                            or_else(try_for(mk_smt_tactic(), 100), 
                                    try_for(qe::mk_sat_tactic(m), 1000), 
                                    try_for(mk_smt_tactic(), 1000),
                                    and_then(mk_qe_tactic(m), mk_smt_tactic())
                                    ));
-
+#else
+    tactic * st = and_then(mk_quant_preprocessor(m),
+                           or_else(mk_qsat_tactic(m, p),
+                                   and_then(mk_qe_tactic(m), mk_smt_tactic())));
+#endif
     st->updt_params(p);
     return st;
 }
@@ -116,3 +127,4 @@ tactic * mk_lia_tactic(ast_manager & m, params_ref const & p) {
 tactic * mk_lira_tactic(ast_manager & m, params_ref const & p) {
     return mk_lra_tactic(m, p);
 }
+