From: Morgan Deters Date: Wed, 20 Oct 2010 04:09:50 +0000 (+0000) Subject: fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and bug217... X-Git-Tag: cvc5-1.0.0~8799 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=daad722774087de1cf35714868d3762b3ea7cb21;p=cvc5.git fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and bug217.smt2 as regressions; fix to build system to only run regressions (not units) if you "make -C test regress", for example (this matches behavior elsewhere) --- 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