Interruption, time-out, and deterministic time-out ("resource-out") features.

Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.

Also implemented TheoryEngine::properPropagation().

Other minor things.

4 files changed, 74 insertions, 2 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 9c438a5cd..a01237fd0 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -138,7 +138,11 @@ static const string optionsDescription = "\
    --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --disable-arithmetic-propagation turns on arithmetic propagation\n\
    --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\
-   --incremental | -i     enable incremental solving\n";
+   --incremental | -i     enable incremental solving\n\
+   --time-limit=MS        enable time limiting (give milliseconds)\n\
+   --time-limit-per=MS    enable time limiting per query (give milliseconds)\n\
+   --limit=N              enable resource limiting\n\
+   --limit-per=N          enable resource limiting per query\n";
 
 #warning "Change CL options as --disable-variable-removal cannot do anything currently."
 
@@ -296,7 +300,11 @@ enum OptionValue {
   ARITHMETIC_PROPAGATION,
   ARITHMETIC_PIVOT_THRESHOLD,
   ARITHMETIC_PROP_MAX_LENGTH,
-  DISABLE_SYMMETRY_BREAKER
+  DISABLE_SYMMETRY_BREAKER,
+  TIME_LIMIT,
+  TIME_LIMIT_PER,
+  LIMIT,
+  LIMIT_PER
 };/* enum OptionValue */
 
 /**
@@ -371,6 +379,10 @@ static struct option cmdlineOptions[] = {
   { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL },
   { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
   { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
+  { "time-limit" , required_argument, NULL, TIME_LIMIT  },
+  { "time-limit-per", required_argument, NULL, TIME_LIMIT_PER },
+  { "limit"      , required_argument, NULL, LIMIT       },
+  { "limit-per"  , required_argument, NULL, LIMIT_PER   },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -677,6 +689,43 @@ throw(OptionException) {
       ufSymmetryBreaker = false;
       break;
 
+    case TIME_LIMIT:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--time-limit requires a nonnegative argument.");
+        }
+        cumulativeMillisecondLimit = (unsigned long) i;
+      }
+      break;
+    case TIME_LIMIT_PER:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--time-limit-per requires a nonnegative argument.");
+        }
+        perCallMillisecondLimit = (unsigned long) i;
+      }
+      break;
+    case LIMIT:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--limit requires a nonnegative argument.");
+        }
+        cumulativeResourceLimit = (unsigned long) i;
+      }
+      break;
+    case LIMIT_PER:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--limit-per requires a nonnegative argument.");
+        }
+        perCallResourceLimit = (unsigned long) i;
+        break;
+      }
+
     case RANDOM_SEED:
       satRandomSeed = atof(optarg);
       break;
diff --git a/src/util/options.h b/src/util/options.h
index 7fc894d93..f9dc042d1 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -129,6 +129,16 @@ struct CVC4_PUBLIC Options {
    */
   bool interactiveSetByUser;
 
+  /** Per-query resource limit. */
+  unsigned long perCallResourceLimit;
+  /** Cumulative resource limit. */
+  unsigned long cumulativeResourceLimit;
+
+  /** Per-query time limit in milliseconds. */
+  unsigned long perCallMillisecondLimit;
+  /** Cumulative time limit in milliseconds. */
+  unsigned long cumulativeMillisecondLimit;
+
   /** Whether we should "spin" on a SIG_SEGV. */
   bool segvNoSpin;
 
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 8a2bcf3b2..bdb17f54c 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -55,10 +55,18 @@ Result::Result(const std::string& instr) :
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = TIMEOUT;
+  } else if(s == "resourceout") {
+    d_which = TYPE_SAT;
+    d_sat = SAT_UNKNOWN;
+    d_unknownExplanation = RESOURCEOUT;
   } else if(s == "memout") {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = MEMOUT;
+  } else if(s == "interrupted") {
+    d_which = TYPE_SAT;
+    d_sat = SAT_UNKNOWN;
+    d_unknownExplanation = INTERRUPTED;
   } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
@@ -169,8 +177,11 @@ ostream& operator<<(ostream& out,
   case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
   case Result::INCOMPLETE: out << "INCOMPLETE"; break;
   case Result::TIMEOUT: out << "TIMEOUT"; break;
+  case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
   case Result::MEMOUT: out << "MEMOUT"; break;
+  case Result::INTERRUPTED: out << "INTERRUPTED"; break;
   case Result::NO_STATUS: out << "NO_STATUS"; break;
+  case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
   case Result::OTHER: out << "OTHER"; break;
   case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
   default: Unhandled(e);
diff --git a/src/util/result.h b/src/util/result.h
index c4733eab9..ac52ee382 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -59,7 +59,9 @@ public:
     REQUIRES_FULL_CHECK,
     INCOMPLETE,
     TIMEOUT,
+    RESOURCEOUT,
     MEMOUT,
+    INTERRUPTED,
     NO_STATUS,
     UNSUPPORTED,
     OTHER,