New default behavior in the strategic_solver: invoke tactics when incremental solver returns unknown.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

lib/strategic_solver.cpp

@@ -33,7 +33,7 @@ strategic_solver::strategic_solver():
     m_check_sat_executed(false),
     m_inc_solver(0),
     m_inc_solver_timeout(UINT_MAX),
-    m_tactic_if_undef(false),
+    m_inc_unknown_behavior(IUB_USE_TACTIC_IF_QF),
     m_default_fct(0),
     m_curr_tactic(0),
     m_proof(0),
@@ -56,6 +56,29 @@ strategic_solver::~strategic_solver() {
         m().dec_ref(m_proof);
 }
 
+bool strategic_solver::has_quantifiers() const {
+    unsigned sz = get_num_assertions();
+    for (unsigned i = 0; i < sz; i++) {
+        if (::has_quantifiers(get_assertion(i)))
+            return true;
+    }
+    return false;
+}
+
+/**
+   \brief Return true if a tactic should be used when the incremental solver returns unknown.
+*/
+bool strategic_solver::use_tactic_when_undef() const {
+    switch (m_inc_unknown_behavior) {
+    case IUB_RETURN_UNDEF: return false;
+    case IUB_USE_TACTIC_IF_QF: return !has_quantifiers();
+    case IUB_USE_TACTIC: return true;
+    default:
+        UNREACHABLE();
+        return false;
+    }
+}
+
 void strategic_solver::set_inc_solver(solver * s) {
     SASSERT(m_inc_solver == 0);
     SASSERT(m_num_scopes == 0);
@@ -86,13 +109,6 @@ void strategic_solver::set_inc_solver_timeout(unsigned timeout) {
     m_inc_solver_timeout = timeout;
 }
 
-/**
-   \brief Use tactic when the incremental solver return undef.
-*/
-void strategic_solver::use_tactic_if_undef(bool f) {
-    m_tactic_if_undef = f;
-}
-
 /**
    \brief Set the default tactic factory.
    It is used if there is no tactic for a given logic.
@@ -285,7 +301,7 @@ lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assum
             IF_VERBOSE(PS_VB_LVL, verbose_stream() << "using incremental solver (without a timeout).\n";);            
             m_use_inc_solver_results = true;
             lbool r = m_inc_solver->check_sat(0, 0);
-            if (r != l_undef || factory == 0 || !m_tactic_if_undef) {
+            if (r != l_undef || factory == 0 || !use_tactic_when_undef()) {
                 m_use_inc_solver_results = true;
                 return r;
             }
@@ -299,7 +315,7 @@ lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assum
                 scoped_timer timer(m_inc_solver_timeout, &eh);
                 r = m_inc_solver->check_sat(0, 0);
             }
-            if ((r != l_undef || !m_tactic_if_undef) && !eh.m_canceled) {
+            if ((r != l_undef || !use_tactic_when_undef()) && !eh.m_canceled) {
                 m_use_inc_solver_results = true;
                 return r;
             }

lib/strategic_solver.h

@@ -26,6 +26,15 @@ class progress_callback;
 struct front_end_params;
 
 class strategic_solver : public solver {
+public:
+    // Behavior when the incremental solver returns unknown.
+    enum inc_unknown_behavior {
+        IUB_RETURN_UNDEF,      // just return unknown
+        IUB_USE_TACTIC_IF_QF,  // invoke tactic if problem is quantifier free
+        IUB_USE_TACTIC         // invoke tactic
+    };
+
+private:
     ast_manager *        m_manager;
     front_end_params *   m_fparams;
     symbol               m_logic;
@@ -34,7 +43,7 @@ class strategic_solver : public solver {
     bool                 m_check_sat_executed;
     scoped_ptr<solver>   m_inc_solver;
     unsigned             m_inc_solver_timeout;
-    bool                 m_tactic_if_undef;
+    inc_unknown_behavior m_inc_unknown_behavior;
     scoped_ptr<tactic_factory>  m_default_fct;
     dictionary<tactic_factory*> m_logic2fct;
 
@@ -63,6 +72,9 @@ class strategic_solver : public solver {
 
     struct mk_tactic;
 
+    bool has_quantifiers() const;
+    bool use_tactic_when_undef() const;
+
 public:
     strategic_solver();
     ~strategic_solver();
@@ -73,7 +85,7 @@ public:
     void set_inc_solver_timeout(unsigned timeout);
     void set_default_tactic(tactic_factory * fct);
     void set_tactic_for(symbol const & logic, tactic_factory * fct);
-    void use_tactic_if_undef(bool f);
+    void set_inc_unknown_behavior(inc_unknown_behavior b) { m_inc_unknown_behavior = b; }
     void force_tactic(bool f) { m_force_tactic = f; }
 
     virtual void set_front_end_params(front_end_params & p) { m_fparams = &p; }