summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.subdir8
-rw-r--r--src/util/result.cpp63
-rw-r--r--src/util/result.h11
-rw-r--r--test/Makefile4
-rw-r--r--test/regress/regress0/Makefile.am3
-rw-r--r--test/regress/regress0/bug220.smt22
-rw-r--r--test/regress/regress0/uf/bug217.smt212
-rw-r--r--test/system/Makefile4
-rw-r--r--test/unit/Makefile4
9 files changed, 67 insertions, 44 deletions
diff --git a/Makefile.subdir b/Makefile.subdir
index 4b3afdbbf..293b2771b 100644
--- a/Makefile.subdir
+++ b/Makefile.subdir
@@ -21,8 +21,8 @@ all %:
.PHONY: check units
ifeq ($(srcdir:test/%=test),test)
# under the test/ directory, additional subtargets
-.PHONY: regress0 regress1 regress2 regress3
-check units regress0 regress1 regress2 regress3:
+.PHONY: regress regress0 regress1 regress2 regress3
+check units regress regress0 regress1 regress2 regress3:
@if test -e $(builddir); then \
echo cd $(builddir); \
cd $(builddir); \
@@ -49,5 +49,5 @@ check units:
endif
# synonyms for "check"
-.PHONY: regress test
-regress test: check
+.PHONY: test
+test: check
diff --git a/src/util/result.cpp b/src/util/result.cpp
index b8f34f47f..9760eaefb 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -47,9 +47,6 @@ Result::Result(const string& instr) :
} else if(s == "invalid") {
d_which = TYPE_VALIDITY;
d_validity = INVALID;
- } else if(s == "unknown") {
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
} else if(s == "incomplete") {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
@@ -62,13 +59,16 @@ Result::Result(const string& instr) :
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = MEMOUT;
+ } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
+ d_which = TYPE_SAT;
+ d_sat = SAT_UNKNOWN;
} else {
IllegalArgument(s, "expected satisfiability/validity result, "
"instead got `%s'", s.c_str());
}
}
-bool Result::operator==(const Result& r) const {
+bool Result::operator==(const Result& r) const throw() {
if(d_which != r.d_which) {
return false;
}
@@ -85,50 +85,56 @@ bool Result::operator==(const Result& r) const {
return false;
}
-Result Result::asSatisfiabilityResult() const {
+Result Result::asSatisfiabilityResult() const throw() {
if(d_which == TYPE_SAT) {
return *this;
}
- Assert(d_which == TYPE_VALIDITY);
-
- switch(d_validity) {
+ if(d_which == TYPE_VALIDITY) {
+ switch(d_validity) {
- case INVALID:
- return Result(SAT);
+ case INVALID:
+ return Result(SAT);
- case VALID:
- return Result(UNSAT);
+ case VALID:
+ return Result(UNSAT);
- case VALIDITY_UNKNOWN:
- return Result(SAT_UNKNOWN, d_unknownExplanation);
+ case VALIDITY_UNKNOWN:
+ return Result(SAT_UNKNOWN, d_unknownExplanation);
- default:
- Unhandled(d_validity);
+ default:
+ Unhandled(d_validity);
+ }
}
+
+ // TYPE_NONE
+ return Result(SAT_UNKNOWN, NO_STATUS);
}
-Result Result::asValidityResult() const {
+Result Result::asValidityResult() const throw() {
if(d_which == TYPE_VALIDITY) {
return *this;
}
- Assert(d_which == TYPE_SAT);
-
- switch(d_sat) {
+ if(d_which == TYPE_SAT) {
+ switch(d_sat) {
- case SAT:
- return Result(INVALID);
+ case SAT:
+ return Result(INVALID);
- case UNSAT:
- return Result(VALID);
+ case UNSAT:
+ return Result(VALID);
- case SAT_UNKNOWN:
- return Result(VALIDITY_UNKNOWN, d_unknownExplanation);
+ case SAT_UNKNOWN:
+ return Result(VALIDITY_UNKNOWN, d_unknownExplanation);
- default:
- Unhandled(d_sat);
+ default:
+ Unhandled(d_sat);
+ }
}
+
+ // TYPE_NONE
+ return Result(VALIDITY_UNKNOWN, NO_STATUS);
}
string Result::toString() const {
@@ -164,6 +170,7 @@ ostream& operator<<(ostream& out,
case Result::INCOMPLETE: out << "INCOMPLETE"; break;
case Result::TIMEOUT: out << "TIMEOUT"; break;
case Result::MEMOUT: out << "MEMOUT"; break;
+ case Result::NO_STATUS: out << "NO_STATUS"; 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 62ddc74d0..1e0729332 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -60,6 +60,7 @@ public:
INCOMPLETE,
TIMEOUT,
MEMOUT,
+ NO_STATUS,
OTHER,
UNKNOWN_REASON
};
@@ -132,16 +133,16 @@ public:
return d_unknownExplanation;
}
- bool operator==(const Result& r) const;
- inline bool operator!=(const Result& r) const;
- Result asSatisfiabilityResult() const;
- Result asValidityResult() const;
+ bool operator==(const Result& r) const throw();
+ inline bool operator!=(const Result& r) const throw();
+ Result asSatisfiabilityResult() const throw();
+ Result asValidityResult() const throw();
std::string toString() const;
};/* class Result */
-inline bool Result::operator!=(const Result& r) const {
+inline bool Result::operator!=(const Result& r) const throw() {
return !(*this == r);
}
diff --git a/test/Makefile b/test/Makefile
index 45659ae1e..d1ebf4bb9 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -4,5 +4,5 @@ srcdir = test
include $(topdir)/Makefile.subdir
# synonyms for "check"
-.PHONY: regress test
-regress test: check
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 9bc8991ab..019eda76d 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -82,7 +82,8 @@ BUG_TESTS = \
bug164.smt \
bug167.smt \
bug168.smt \
- bug187.smt2
+ bug187.smt2 \
+ bug220.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
diff --git a/test/regress/regress0/bug220.smt2 b/test/regress/regress0/bug220.smt2
new file mode 100644
index 000000000..117ee3be2
--- /dev/null
+++ b/test/regress/regress0/bug220.smt2
@@ -0,0 +1,2 @@
+% EXIT: 0
+(exit)
diff --git a/test/regress/regress0/uf/bug217.smt2 b/test/regress/regress0/uf/bug217.smt2
new file mode 100644
index 000000000..45f0f3c0c
--- /dev/null
+++ b/test/regress/regress0/uf/bug217.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-fun f (Bool) Bool)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+;(assert (and x (or (f x) (f y))))
+(assert (or (f x) (f y) (f z)))
+(assert (not (f false)))
+(assert (not (f true)))
+(check-sat)
+;(get-value ((f true) (f false) (f x) (f y) (f z) x y z))
diff --git a/test/system/Makefile b/test/system/Makefile
index 2ca4091cb..87b92bb11 100644
--- a/test/system/Makefile
+++ b/test/system/Makefile
@@ -4,5 +4,5 @@ srcdir = test/system
include $(topdir)/Makefile.subdir
# synonyms for "check"
-.PHONY: regress test
-regress test: check
+.PHONY: test
+test: check
diff --git a/test/unit/Makefile b/test/unit/Makefile
index 94a9d1d9e..16dc971e1 100644
--- a/test/unit/Makefile
+++ b/test/unit/Makefile
@@ -4,5 +4,5 @@ srcdir = test/unit
include $(topdir)/Makefile.subdir
# synonyms for "check"
-.PHONY: regress test
-regress test: check
+.PHONY: test
+test: check
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback