diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
| commit | 3cbb76ef86a769cfe3dac5976a14e1bc43c42ca6 (patch) | |
| tree | e08efdc63abd663de4f5750db9326b69c79829e5 /src/util/result.cpp | |
| parent | 3a7aafccadbfa1543c435b7dfe4f53116224a11f (diff) | |
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.
Diffstat (limited to 'src/util/result.cpp')
| -rw-r--r-- | src/util/result.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
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); |