include rlimit in nlsat, include dedicated error message, for issue #216

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

src/ast/rewriter/rewriter_def.h

@@ -579,7 +579,7 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
         if (m_cancel)
             throw rewriter_exception(Z3_CANCELED_MSG);
         if (!m().limit().inc()) 
-            throw rewriter_exception(Z3_CANCELED_MSG);
+            throw rewriter_exception(Z3_MAX_RESOURCE_MSG);
         SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
         frame & fr = frame_stack().back();
         expr * t   = fr.m_curr;

src/nlsat/nlsat_solver.cpp

@@ -67,6 +67,7 @@ namespace nlsat {
         typedef ptr_vector<interval_set> interval_set_vector;
 
         solver &               m_solver;
+        reslimit&              m_rlimit;
         small_object_allocator m_allocator;
         unsynch_mpq_manager    m_qm;
         pmanager               m_pm;
@@ -159,8 +160,9 @@ namespace nlsat {
         unsigned               m_stages;
         unsigned               m_irrational_assignments; // number of irrational witnesses
 
-        imp(solver & s, params_ref const & p):
+        imp(solver & s, reslimit& rlim, params_ref const & p):
             m_solver(s),
+            m_rlimit(rlim),
             m_allocator("nlsat"),
             m_pm(m_qm, &m_allocator),
             m_cache(m_pm),
@@ -224,6 +226,7 @@ namespace nlsat {
 
         void checkpoint() {
             if (m_cancel) throw solver_exception(Z3_CANCELED_MSG);
+            if (!m_rlimit.inc()) throw solver_exception(Z3_MAX_RESOURCE_MSG);
             if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
         }
 
@@ -2556,8 +2559,8 @@ namespace nlsat {
         }
     };
     
-    solver::solver(params_ref const & p) {
+    solver::solver(reslimit& rlim, params_ref const & p) {
-        m_imp = alloc(imp, *this, p);
+        m_imp = alloc(imp, *this, rlim, p);
     }
         
     solver::~solver() {

src/nlsat/nlsat_solver.h

@@ -24,6 +24,7 @@ Revision History:
 #include"nlsat_types.h"
 #include"params.h"
 #include"statistics.h"
+#include"rlimit.h"
 
 namespace nlsat {
 
@@ -31,7 +32,7 @@ namespace nlsat {
         struct imp;
         imp * m_imp;
     public:
-        solver(params_ref const & p);
+        solver(reslimit& rlim, params_ref const & p);
         ~solver();
 
         /**

src/nlsat/tactic/nlsat_tactic.cpp

@@ -50,7 +50,7 @@ class nlsat_tactic : public tactic {
             m(_m),
             m_params(p),
             m_display_var(_m),
-            m_solver(p) {
+            m_solver(m.limit(), p) {
         }
         
         void updt_params(params_ref const & p) {

src/util/common_msgs.cpp

@@ -24,3 +24,4 @@ char const * common_msgs::g_max_scopes_msg = "max. scopes exceeded";
 char const * common_msgs::g_max_steps_msg  = "max. steps exceeded";
 char const * common_msgs::g_max_frames_msg = "max. frames exceeded";
 char const * common_msgs::g_no_proofs_msg  = "component does not support proof generation";
+char const * common_msgs::g_max_resource_msg = "max. resource limit exceeded";

src/util/common_msgs.h

@@ -27,6 +27,7 @@ public:
     static char const * g_max_steps_msg;
     static char const * g_max_frames_msg;
     static char const * g_no_proofs_msg;
+    static char const * g_max_resource_msg;
 };
 
 #define Z3_CANCELED_MSG      common_msgs::g_canceled_msg
@@ -35,5 +36,6 @@ public:
 #define Z3_MAX_STEPS_MSG     common_msgs::g_max_steps_msg
 #define Z3_MAX_FRAMES_MSG    common_msgs::g_max_frames_msg
 #define Z3_NO_PROOF_GEN_MSG  common_msgs::g_no_proofs_msg
+#define Z3_MAX_RESOURCE_MSG  common_msgs::g_max_resource_msg
 
 #endif