diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 49 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 40 | ||||
| -rw-r--r-- | src/api/python/cvc4.pxd | 9 | ||||
| -rw-r--r-- | src/api/python/cvc4.pxi | 16 | ||||
| -rw-r--r-- | src/smt/command.cpp | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 62 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 83 | ||||
| -rw-r--r-- | src/util/result.cpp | 188 | ||||
| -rw-r--r-- | src/util/result.h | 38 | ||||
| -rw-r--r-- | src/util/result.i | 6 |
10 files changed, 258 insertions, 235 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index fa727088e..fff4bef85 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -768,22 +768,22 @@ bool Result::isSatUnknown(void) const && d_result->isSat() == CVC4::Result::SAT_UNKNOWN; } -bool Result::isValid(void) const +bool Result::isEntailed(void) const { - return d_result->getType() == CVC4::Result::TYPE_VALIDITY - && d_result->isValid() == CVC4::Result::VALID; + return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT + && d_result->isEntailed() == CVC4::Result::ENTAILED; } -bool Result::isInvalid(void) const +bool Result::isNotEntailed(void) const { - return d_result->getType() == CVC4::Result::TYPE_VALIDITY - && d_result->isValid() == CVC4::Result::INVALID; + return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT + && d_result->isEntailed() == CVC4::Result::NOT_ENTAILED; } -bool Result::isValidUnknown(void) const +bool Result::isEntailmentUnknown(void) const { - return d_result->getType() == CVC4::Result::TYPE_VALIDITY - && d_result->isValid() == CVC4::Result::VALIDITY_UNKNOWN; + return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT + && d_result->isEntailed() == CVC4::Result::ENTAILMENT_UNKNOWN; } bool Result::operator==(const Result& r) const @@ -3585,7 +3585,7 @@ Term Solver::simplify(const Term& t) CVC4_API_SOLVER_TRY_CATCH_END; } -Result Solver::checkValid(void) const +Result Solver::checkEntailed(Term term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); @@ -3593,14 +3593,15 @@ Result Solver::checkValid(void) const || CVC4::options::incrementalSolving()) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; + CVC4_API_ARG_CHECK_NOT_NULL(term); - CVC4::Result r = d_smtEngine->query(); + CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; } -Result Solver::checkValidAssuming(Term assumption) const +Result Solver::checkEntailed(const std::vector<Term>& terms) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); @@ -3608,29 +3609,13 @@ Result Solver::checkValidAssuming(Term assumption) const || CVC4::options::incrementalSolving()) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; - CVC4_API_ARG_CHECK_NOT_NULL(assumption); - - CVC4::Result r = d_smtEngine->query(*assumption.d_expr); - return Result(r); - - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Result Solver::checkValidAssuming(const std::vector<Term>& assumptions) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(!d_smtEngine->isQueryMade() - || CVC4::options::incrementalSolving()) - << "Cannot make multiple queries unless incremental solving is enabled " - "(try --incremental)"; - for (const Term& assumption : assumptions) + for (const Term& term : terms) { - CVC4_API_ARG_CHECK_NOT_NULL(assumption); + CVC4_API_ARG_CHECK_NOT_NULL(term); } - std::vector<Expr> eassumptions = termVectorToExprs(assumptions); - CVC4::Result r = d_smtEngine->query(eassumptions); + std::vector<Expr> exprs = termVectorToExprs(terms); + CVC4::Result r = d_smtEngine->checkEntailed(exprs); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 3c99d2480..1a1cd3b61 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -114,22 +114,21 @@ class CVC4_PUBLIC Result bool isSatUnknown() const; /** - * Return true if corresponding query was a valid checkValid() or - * checkValidAssuming() query. + * Return true if corresponding query was an entailed checkEntailed() query. */ - bool isValid() const; + bool isEntailed() const; /** - * Return true if corresponding query was an invalid checkValid() or - * checkValidAssuming() query. + * Return true if corresponding query was a checkEntailed() query that is + * not entailed. */ - bool isInvalid() const; + bool isNotEntailed() const; /** - * Return true if query was a checkValid() or checkValidAssuming() query - * and CVC4 was not able to determine (in)validity. + * Return true if query was a checkEntailed() () query and CVC4 was not able + * to determine if it is entailed. */ - bool isValidUnknown() const; + bool isEntailmentUnknown() const; /** * Operator overloading for equality of two results. @@ -2555,24 +2554,19 @@ class CVC4_PUBLIC Solver Result checkSatAssuming(const std::vector<Term>& assumptions) const; /** - * Check validity. - * @return the result of the validity check. + * Check entailment of the given formula w.r.t. the current set of assertions. + * @param term the formula to check entailment for + * @return the result of the entailment check. */ - Result checkValid() const; + Result checkEntailed(Term term) const; /** - * Check validity assuming the given formula. - * @param assumption the formula to assume - * @return the result of the validity check. - */ - Result checkValidAssuming(Term assumption) const; - - /** - * Check validity assuming the given formulas. - * @param assumptions the formulas to assume - * @return the result of the validity check. + * Check entailment of the given set of given formulas w.r.t. the current + * set of assertions. + * @param terms the terms to check entailment for + * @return the result of the entailmentcheck. */ - Result checkValidAssuming(const std::vector<Term>& assumptions) const; + Result checkEntailed(const std::vector<Term>& terms) const; /** * Create datatype sort. diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index bbff6f58b..d81d0c0bf 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -87,9 +87,9 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": bint isSat() except + bint isUnsat() except + bint isSatUnknown() except + - bint isValid() except + - bint isInvalid() except + - bint isValidUnknown() except + + bint isEntailed() except + + bint isNotEntailed() except + + bint isEntailmentUnknown() except + string getUnknownExplanation() except + string toString() except + @@ -168,8 +168,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": void assertFormula(Term term) except + Result checkSat() except + Result checkSatAssuming(const vector[Term]& assumptions) except + - Result checkValid() except + - Result checkValidAssuming(const vector[Term]& assumptions) except + + Result checkEntailed(const vector[Term]& assumptions) except + Sort declareDatatype(const string& symbol, const vector[DatatypeConstructorDecl]& ctors) Term declareFun(const string& symbol, Sort sort) except + Term declareFun(const string& symbol, const vector[Sort]& sorts, Sort sort) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 188753122..60bd89cbd 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -749,19 +749,11 @@ cdef class Solver: explanation = r.getUnknownExplanation().decode() return Result(name, explanation) - def checkValid(self): - cdef c_Result r = self.csolver.checkValid() - name = r.toString().decode() - explanation = "" - if r.isValidUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) - @expand_list_arg(num_req_args=0) - def checkValidAssuming(self, *assumptions): + def checkEntailed(self, *assumptions): ''' Supports the following arguments: - Result checkValidAssuming(List[Term] assumptions) + Result checkEntailed(List[Term] assumptions) where assumptions can also be comma-separated arguments of type (boolean) Term @@ -771,10 +763,10 @@ cdef class Solver: cdef vector[c_Term] v for a in assumptions: v.push_back((<Term?> a).cterm) - r = self.csolver.checkValidAssuming(<const vector[c_Term]&> v) + r = self.csolver.checkEntailed(<const vector[c_Term]&> v) name = r.toString().decode() explanation = "" - if r.isValidUnknown(): + if r.isEntailmentUnknown(): explanation = r.getUnknownExplanation().decode() return Result(name, explanation) diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 79cc465ac..20f2dcff9 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -513,7 +513,7 @@ void QueryCommand::invoke(SmtEngine* smtEngine) { try { - d_result = smtEngine->query(d_expr); + d_result = smtEngine->checkEntailed(d_expr); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 10fc76bf7..2e1716543 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1766,7 +1766,7 @@ Result SmtEngine::check() { resourceManager->out()) { Result::UnknownExplanation why = resourceManager->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; - return Result(Result::VALIDITY_UNKNOWN, why, d_filename); + return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename); } // Make sure the prop layer has all of the assertions @@ -1791,7 +1791,8 @@ Result SmtEngine::check() { Result SmtEngine::quickCheck() { Assert(d_fullyInited); Trace("smt") << "SMT quickCheck()" << endl; - return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename); + return Result( + Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename); } theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const @@ -1807,7 +1808,8 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const { std::stringstream ss; ss << "Cannot " << c - << " unless immediately preceded by SAT/INVALID or UNKNOWN response."; + << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN " + "response."; throw RecoverableModalException(ss.str().c_str()); } @@ -2380,35 +2382,34 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) return checkSatisfiability(assumptions, inUnsatCore, false); } -Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) +Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore) { - Dump("benchmark") << QueryCommand(assumption, inUnsatCore); - return checkSatisfiability(assumption.isNull() - ? std::vector<Expr>() - : std::vector<Expr>{assumption}, - inUnsatCore, - true) - .asValidityResult(); + Dump("benchmark") << QueryCommand(expr, inUnsatCore); + return checkSatisfiability( + expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr}, + inUnsatCore, + true) + .asEntailmentResult(); } -Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore) +Result SmtEngine::checkEntailed(const vector<Expr>& exprs, bool inUnsatCore) { - return checkSatisfiability(assumptions, inUnsatCore, true).asValidityResult(); + return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult(); } Result SmtEngine::checkSatisfiability(const Expr& expr, bool inUnsatCore, - bool isQuery) + bool isEntailmentCheck) { return checkSatisfiability( expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr}, inUnsatCore, - isQuery); + isEntailmentCheck); } Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, bool inUnsatCore, - bool isQuery) + bool isEntailmentCheck) { try { @@ -2416,7 +2417,8 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, finalOptionsAreSet(); doPendingPops(); - Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" + Trace("smt") << "SmtEngine::" + << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "(" << assumptions << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { @@ -2434,7 +2436,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, setProblemExtended(); - if (isQuery) + if (isEntailmentCheck) { size_t size = assumptions.size(); if (size > 1) @@ -2540,8 +2542,8 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, d_smtMode = SMT_MODE_SAT_UNKNOWN; } - Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" - << assumptions << ") => " << r << endl; + Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat") + << "(" << assumptions << ") => " << r << endl; // Check that SAT results generate a model correctly. if(options::checkModels()) { @@ -2587,7 +2589,7 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void) { throw RecoverableModalException( "Cannot get unsat assumptions unless immediately preceded by " - "UNSAT/VALID response."); + "UNSAT/ENTAILED."); } finalOptionsAreSet(); if (Dump.isOn("benchmark")) @@ -2625,7 +2627,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) } bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); d_private->addFormula(e.getNode(), inUnsatCore, true, false, maybeHasFv); - return quickCheck().asValidityResult(); + return quickCheck().asEntailmentResult(); }/* SmtEngine::assertFormula() */ /* @@ -3218,13 +3220,13 @@ std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void) Expr heap; Expr nil; Model* m = getAvailableModel("get separation logic heap and nil"); - if (m->getHeapModel(heap, nil)) + if (!m->getHeapModel(heap, nil)) { - return std::make_pair(heap, nil); + InternalError() + << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil " + "expressions from theory model."; } - InternalError() - << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil " - "expressions from theory model."; + return std::make_pair(heap, nil); } std::vector<Expr> SmtEngine::getExpandedAssertions() @@ -3294,8 +3296,8 @@ UnsatCore SmtEngine::getUnsatCoreInternal() if (d_smtMode != SMT_MODE_UNSAT) { throw RecoverableModalException( - "Cannot get an unsat core unless immediately preceded by UNSAT/VALID " - "response."); + "Cannot get an unsat core unless immediately preceded by " + "UNSAT/ENTAILED response."); } d_proofManager->traceUnsatCore(); // just to trigger core creation @@ -3800,7 +3802,7 @@ const Proof& SmtEngine::getProof() if (d_smtMode != SMT_MODE_UNSAT) { throw RecoverableModalException( - "Cannot get a proof unless immediately preceded by UNSAT/VALID " + "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED " "response."); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2cb227fc9..37b89cfb7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -152,7 +152,9 @@ class CVC4_PUBLIC SmtEngine */ bool isFullyInited() { return d_fullyInited; } - /** Return true if a query() or checkSat() has already been made. */ + /** + * Return true if a checkEntailed() or checkSatisfiability() has been made. + */ bool isQueryMade() { return d_queryMade; } /** Return the user context level. */ @@ -211,8 +213,8 @@ class CVC4_PUBLIC SmtEngine std::string getFilename() const; /** - * Get the model (only if immediately preceded by a SAT - * or INVALID query). Only permitted if produce-models is on. + * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED + * query). Only permitted if produce-models is on. */ Model* getModel(); @@ -230,9 +232,9 @@ class CVC4_PUBLIC SmtEngine /** * Block the current model values of (at least) the values in exprs. - * Can be called only if immediately preceded by a SAT or INVALID query. Only - * permitted if produce-models is on, and the block-models option is set to a - * mode other than "none". + * Can be called only if immediately preceded by a SAT or NOT_ENTAILED query. + * Only permitted if produce-models is on, and the block-models option is set + * to a mode other than "none". * * This adds an assertion to the assertion stack of the form: * (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn))) @@ -310,18 +312,21 @@ class CVC4_PUBLIC SmtEngine Result assertFormula(const Expr& e, bool inUnsatCore = true); /** - * Check validity of an expression with respect to the current set - * of assertions by asserting the query expression's negation and - * calling check(). Returns valid, invalid, or unknown result. + * Check if a given (set of) expression(s) is entailed with respect to the + * current set of assertions. We check this by asserting the negation of + * the (big AND over the) given (set of) expression(s). + * Returns ENTAILED, NOT_ENTAILED, or ENTAILMENT_UNKNOWN result. * * @throw Exception */ - Result query(const Expr& assumption = Expr(), bool inUnsatCore = true); - Result query(const std::vector<Expr>& assumptions, bool inUnsatCore = true); + Result checkEntailed(const Expr& assumption = Expr(), + bool inUnsatCore = true); + Result checkEntailed(const std::vector<Expr>& assumptions, + bool inUnsatCore = true); /** * Assert a formula (if provided) to the current context and call - * check(). Returns sat, unsat, or unknown result. + * check(). Returns SAT, UNSAT, or SAT_UNKNOWN result. * * @throw Exception */ @@ -456,9 +461,9 @@ class CVC4_PUBLIC SmtEngine Expr expandDefinitions(const Expr& e); /** - * Get the assigned value of an expr (only if immediately preceded - * by a SAT or INVALID query). Only permitted if the SmtEngine is - * set to operate interactively and produce-models is on. + * Get the assigned value of an expr (only if immediately preceded by a SAT + * or NOT_ENTAILED query). Only permitted if the SmtEngine is set to operate + * interactively and produce-models is on. * * @throw ModalException, TypeCheckingException, LogicException, * UnsafeInterruptException @@ -483,15 +488,15 @@ class CVC4_PUBLIC SmtEngine /** * Get the assignment (only if immediately preceded by a SAT or - * INVALID query). Only permitted if the SmtEngine is set to + * NOT_ENTAILED query). Only permitted if the SmtEngine is set to * operate interactively and produce-assignments is on. */ std::vector<std::pair<Expr, Expr> > getAssignment(); /** - * Get the last proof (only if immediately preceded by an UNSAT - * or VALID query). Only permitted if CVC4 was built with proof - * support and produce-proofs is on. + * Get the last proof (only if immediately preceded by an UNSAT or ENTAILED + * query). Only permitted if CVC4 was built with proof support and + * produce-proofs is on. * * The Proof object is owned by this SmtEngine until the SmtEngine is * destroyed. @@ -624,9 +629,9 @@ class CVC4_PUBLIC SmtEngine std::vector<std::vector<Expr> >& tvecs); /** - * Get an unsatisfiable core (only if immediately preceded by an - * UNSAT or VALID query). Only permitted if CVC4 was built with - * unsat-core support and produce-unsat-cores is on. + * Get an unsatisfiable core (only if immediately preceded by an UNSAT or + * ENTAILED query). Only permitted if CVC4 was built with unsat-core support + * and produce-unsat-cores is on. */ UnsatCore getUnsatCore(); @@ -714,8 +719,8 @@ class CVC4_PUBLIC SmtEngine * * Note that the cumulative timer only ticks away when one of the * SmtEngine's workhorse functions (things like assertFormula(), - * query(), checkSat(), and simplify()) are running. Between calls, - * the timer is still. + * checkEntailed(), checkSat(), and simplify()) are running. + * Between calls, the timer is still. * * When an SmtEngine is first created, it has no time or resource * limits. @@ -774,7 +779,10 @@ class CVC4_PUBLIC SmtEngine /** Flush statistic from this SmtEngine. Safe to use in a signal handler. */ void safeFlushStatistics(int fd) const; - /** Returns the most recent result of checkSat/query or (set-info :status). */ + /** + * Returns the most recent result of checkSat/checkEntailed or + * (set-info :status). + */ Result getStatusOfLastCommand() const { return d_status; } /** @@ -881,7 +889,7 @@ class CVC4_PUBLIC SmtEngine /** * Internal method to get an unsatisfiable core (only if immediately preceded - * by an UNSAT or VALID query). Only permitted if CVC4 was built with + * by an UNSAT or ENTAILED query). Only permitted if CVC4 was built with * unsat-core support and produce-unsat-cores is on. Does not dump the * command. */ @@ -1007,13 +1015,13 @@ class CVC4_PUBLIC SmtEngine bool userVisible = true, const char* dumpTag = "declarations"); - /* Check satisfiability (used for query and check-sat). */ + /* Check satisfiability (used to check satisfiability and entailment). */ Result checkSatisfiability(const Expr& assumption, bool inUnsatCore, - bool isQuery); + bool isEntailmentCheck); Result checkSatisfiability(const std::vector<Expr>& assumptions, bool inUnsatCore, - bool isQuery); + bool isEntailmentCheck); /** * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is @@ -1123,9 +1131,9 @@ class CVC4_PUBLIC SmtEngine /** * The list of assumptions from the previous call to checkSatisfiability. - * Note that if the last call to checkSatisfiability was a validity check, - * i.e., a call to query(a1, ..., an), then d_assumptions contains one single - * assumption ~(a1 AND ... AND an). + * Note that if the last call to checkSatisfiability was an entailment check, + * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains + * one single assumption ~(a1 AND ... AND an). */ std::vector<Expr> d_assumptions; @@ -1189,10 +1197,10 @@ class CVC4_PUBLIC SmtEngine bool d_fullyInited; /** - * Whether or not a query() or checkSat() has already been made through - * this SmtEngine. If true, and incrementalSolving is false, then - * attempting an additional query() or checkSat() will fail with a - * ModalException. + * Whether or not a checkEntailed() or checkSatisfiability() has already been + * made through this SmtEngine. If true, and incrementalSolving is false, + * then attempting an additional checkEntailed() or checkSat() will fail with + * a ModalException. */ bool d_queryMade; @@ -1214,7 +1222,8 @@ class CVC4_PUBLIC SmtEngine bool d_globalNegation; /** - * Most recent result of last checkSat/query or (set-info :status). + * Most recent result of last checkSatisfiability/checkEntailed or + * (set-info :status). */ Result d_status; diff --git a/src/util/result.cpp b/src/util/result.cpp index 433dcbf29..916e16b4f 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -29,59 +29,68 @@ namespace CVC4 { Result::Result() : d_sat(SAT_UNKNOWN), - d_validity(VALIDITY_UNKNOWN), + d_entailment(ENTAILMENT_UNKNOWN), d_which(TYPE_NONE), d_unknownExplanation(UNKNOWN_REASON), - d_inputName("") {} + d_inputName("") +{ +} Result::Result(enum Sat s, std::string inputName) : d_sat(s), - d_validity(VALIDITY_UNKNOWN), + d_entailment(ENTAILMENT_UNKNOWN), d_which(TYPE_SAT), d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { + d_inputName(inputName) +{ PrettyCheckArgument(s != SAT_UNKNOWN, "Must provide a reason for satisfiability being unknown"); } -Result::Result(enum Validity v, std::string inputName) +Result::Result(enum Entailment e, std::string inputName) : d_sat(SAT_UNKNOWN), - d_validity(v), - d_which(TYPE_VALIDITY), + d_entailment(e), + d_which(TYPE_ENTAILMENT), d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { - PrettyCheckArgument(v != VALIDITY_UNKNOWN, - "Must provide a reason for validity being unknown"); + d_inputName(inputName) +{ + PrettyCheckArgument(e != ENTAILMENT_UNKNOWN, + "Must provide a reason for entailment being unknown"); } -Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation, +Result::Result(enum Sat s, + enum UnknownExplanation unknownExplanation, std::string inputName) : d_sat(s), - d_validity(VALIDITY_UNKNOWN), + d_entailment(ENTAILMENT_UNKNOWN), d_which(TYPE_SAT), d_unknownExplanation(unknownExplanation), - d_inputName(inputName) { + d_inputName(inputName) +{ PrettyCheckArgument(s == SAT_UNKNOWN, "improper use of unknown-result constructor"); } -Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation, +Result::Result(enum Entailment e, + enum UnknownExplanation unknownExplanation, std::string inputName) : d_sat(SAT_UNKNOWN), - d_validity(v), - d_which(TYPE_VALIDITY), + d_entailment(e), + d_which(TYPE_ENTAILMENT), d_unknownExplanation(unknownExplanation), - d_inputName(inputName) { - PrettyCheckArgument(v == VALIDITY_UNKNOWN, + d_inputName(inputName) +{ + PrettyCheckArgument(e == ENTAILMENT_UNKNOWN, "improper use of unknown-result constructor"); } Result::Result(const std::string& instr, std::string inputName) : d_sat(SAT_UNKNOWN), - d_validity(VALIDITY_UNKNOWN), + d_entailment(ENTAILMENT_UNKNOWN), d_which(TYPE_NONE), d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { + d_inputName(inputName) +{ string s = instr; transform(s.begin(), s.end(), s.begin(), ::tolower); if (s == "sat" || s == "satisfiable") { @@ -90,38 +99,56 @@ Result::Result(const std::string& instr, std::string inputName) } else if (s == "unsat" || s == "unsatisfiable") { d_which = TYPE_SAT; d_sat = UNSAT; - } else if (s == "valid") { - d_which = TYPE_VALIDITY; - d_validity = VALID; - } else if (s == "invalid") { - d_which = TYPE_VALIDITY; - d_validity = INVALID; - } else if (s == "incomplete") { + } + else if (s == "entailed") + { + d_which = TYPE_ENTAILMENT; + d_entailment = ENTAILED; + } + else if (s == "not_entailed") + { + d_which = TYPE_ENTAILMENT; + d_entailment = NOT_ENTAILED; + } + else if (s == "incomplete") + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = INCOMPLETE; - } else if (s == "timeout") { + } + else if (s == "timeout") + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = TIMEOUT; - } else if (s == "resourceout") { + } + else if (s == "resourceout") + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = RESOURCEOUT; - } else if (s == "memout") { + } + else if (s == "memout") + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = MEMOUT; - } else if (s == "interrupted") { + } + 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) { + } + else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0) + { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; - } else { + } + else + { IllegalArgument(s, - "expected satisfiability/validity result, " + "expected satisfiability/entailment result, " "instead got `%s'", s.c_str()); } @@ -142,37 +169,41 @@ bool Result::operator==(const Result& r) const { return d_sat == r.d_sat && (d_sat != SAT_UNKNOWN || d_unknownExplanation == r.d_unknownExplanation); } - if (d_which == TYPE_VALIDITY) { - return d_validity == r.d_validity && - (d_validity != VALIDITY_UNKNOWN || - d_unknownExplanation == r.d_unknownExplanation); + if (d_which == TYPE_ENTAILMENT) + { + return d_entailment == r.d_entailment + && (d_entailment != ENTAILMENT_UNKNOWN + || d_unknownExplanation == r.d_unknownExplanation); } return false; } bool operator==(enum Result::Sat sr, const Result& r) { return r == sr; } -bool operator==(enum Result::Validity vr, const Result& r) { return r == vr; } +bool operator==(enum Result::Entailment e, const Result& r) { return r == e; } bool operator!=(enum Result::Sat s, const Result& r) { return !(s == r); } -bool operator!=(enum Result::Validity v, const Result& r) { return !(v == r); } +bool operator!=(enum Result::Entailment e, const Result& r) +{ + return !(e == r); +} Result Result::asSatisfiabilityResult() const { if (d_which == TYPE_SAT) { return *this; } - if (d_which == TYPE_VALIDITY) { - switch (d_validity) { - case INVALID: - return Result(SAT, d_inputName); + if (d_which == TYPE_ENTAILMENT) + { + switch (d_entailment) + { + case NOT_ENTAILED: return Result(SAT, d_inputName); - case VALID: - return Result(UNSAT, d_inputName); + case ENTAILED: return Result(UNSAT, d_inputName); - case VALIDITY_UNKNOWN: + case ENTAILMENT_UNKNOWN: return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName); - default: Unhandled() << d_validity; + default: Unhandled() << d_entailment; } } @@ -180,28 +211,28 @@ Result Result::asSatisfiabilityResult() const { return Result(SAT_UNKNOWN, NO_STATUS, d_inputName); } -Result Result::asValidityResult() const { - if (d_which == TYPE_VALIDITY) { +Result Result::asEntailmentResult() const +{ + if (d_which == TYPE_ENTAILMENT) + { return *this; } if (d_which == TYPE_SAT) { switch (d_sat) { - case SAT: - return Result(INVALID, d_inputName); + case SAT: return Result(NOT_ENTAILED, d_inputName); - case UNSAT: - return Result(VALID, d_inputName); + case UNSAT: return Result(ENTAILED, d_inputName); case SAT_UNKNOWN: - return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName); + return Result(ENTAILMENT_UNKNOWN, d_unknownExplanation, d_inputName); default: Unhandled() << d_sat; } } // TYPE_NONE - return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName); + return Result(ENTAILMENT_UNKNOWN, NO_STATUS, d_inputName); } string Result::toString() const { @@ -226,18 +257,14 @@ ostream& operator<<(ostream& out, enum Result::Sat s) { return out; } -ostream& operator<<(ostream& out, enum Result::Validity v) { - switch (v) { - case Result::INVALID: - out << "INVALID"; - break; - case Result::VALID: - out << "VALID"; - break; - case Result::VALIDITY_UNKNOWN: - out << "VALIDITY_UNKNOWN"; - break; - default: Unhandled() << v; +ostream& operator<<(ostream& out, enum Result::Entailment e) +{ + switch (e) + { + case Result::NOT_ENTAILED: out << "NOT_ENTAILED"; break; + case Result::ENTAILED: out << "ENTAILED"; break; + case Result::ENTAILMENT_UNKNOWN: out << "ENTAILMENT_UNKNOWN"; break; + default: Unhandled() << e; } return out; } @@ -301,14 +328,11 @@ void Result::toStreamDefault(std::ostream& out) const { break; } } else { - switch (isValid()) { - case Result::INVALID: - out << "invalid"; - break; - case Result::VALID: - out << "valid"; - break; - case Result::VALIDITY_UNKNOWN: + switch (isEntailed()) + { + case Result::NOT_ENTAILED: out << "not_entailed"; break; + case Result::ENTAILED: out << "entailed"; break; + case Result::ENTAILMENT_UNKNOWN: out << "unknown"; if (whyUnknown() != Result::UNKNOWN_REASON) { out << " (" << whyUnknown() << ")"; @@ -332,11 +356,17 @@ void Result::toStreamTptp(std::ostream& out) const { out << "Satisfiable"; } else if (isSat() == Result::UNSAT) { out << "Unsatisfiable"; - } else if (isValid() == Result::VALID) { + } + else if (isEntailed() == Result::ENTAILED) + { out << "Theorem"; - } else if (isValid() == Result::INVALID) { + } + else if (isEntailed() == Result::NOT_ENTAILED) + { out << "CounterSatisfiable"; - } else { + } + else + { out << "GaveUp"; } out << " for " << getInputName(); diff --git a/src/util/result.h b/src/util/result.h index f34a9bb5a..10df05388 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -38,9 +38,19 @@ class CVC4_PUBLIC Result { public: enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 }; - enum Validity { INVALID = 0, VALID = 1, VALIDITY_UNKNOWN = 2 }; + enum Entailment + { + NOT_ENTAILED = 0, + ENTAILED = 1, + ENTAILMENT_UNKNOWN = 2 + }; - enum Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE }; + enum Type + { + TYPE_SAT, + TYPE_ENTAILMENT, + TYPE_NONE + }; enum UnknownExplanation { REQUIRES_FULL_CHECK, @@ -57,7 +67,7 @@ class CVC4_PUBLIC Result { private: enum Sat d_sat; - enum Validity d_validity; + enum Entailment d_entailment; enum Type d_which; enum UnknownExplanation d_unknownExplanation; std::string d_inputName; @@ -67,12 +77,13 @@ class CVC4_PUBLIC Result { Result(enum Sat s, std::string inputName = ""); - Result(enum Validity v, std::string inputName = ""); + Result(enum Entailment v, std::string inputName = ""); Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = ""); - Result(enum Validity v, enum UnknownExplanation unknownExplanation, + Result(enum Entailment v, + enum UnknownExplanation unknownExplanation, std::string inputName = ""); Result(const std::string& s, std::string inputName = ""); @@ -84,12 +95,13 @@ class CVC4_PUBLIC Result { enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; } - enum Validity isValid() const { - return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; + enum Entailment isEntailed() const + { + return d_which == TYPE_ENTAILMENT ? d_entailment : ENTAILMENT_UNKNOWN; } bool isUnknown() const { - return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; + return isSat() == SAT_UNKNOWN && isEntailed() == ENTAILMENT_UNKNOWN; } Type getType() const { return d_which; } @@ -101,7 +113,7 @@ class CVC4_PUBLIC Result { bool operator==(const Result& r) const; inline bool operator!=(const Result& r) const; Result asSatisfiabilityResult() const; - Result asValidityResult() const; + Result asEntailmentResult() const; std::string toString() const; @@ -128,7 +140,7 @@ class CVC4_PUBLIC Result { * Write a Result out to a stream. * * The default implementation writes a reasonable string in lowercase - * for sat, unsat, valid, invalid, or unknown results. This behavior + * for sat, unsat, entailed, not entailed, or unknown results. This behavior * is overridable by each Printer, since sometimes an output language * has a particular preference for how results should appear. */ @@ -139,15 +151,15 @@ inline bool Result::operator!=(const Result& r) const { return !(*this == r); } std::ostream& operator<<(std::ostream& out, enum Result::Sat s) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, - enum Result::Validity v) CVC4_PUBLIC; + enum Result::Entailment e) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e) CVC4_PUBLIC; bool operator==(enum Result::Sat s, const Result& r) CVC4_PUBLIC; -bool operator==(enum Result::Validity v, const Result& r) CVC4_PUBLIC; +bool operator==(enum Result::Entailment e, const Result& r) CVC4_PUBLIC; bool operator!=(enum Result::Sat s, const Result& r) CVC4_PUBLIC; -bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC; +bool operator!=(enum Result::Entailment e, const Result& r) CVC4_PUBLIC; } /* CVC4 namespace */ diff --git a/src/util/result.i b/src/util/result.i index b77bfd881..cb835fbb0 100644 --- a/src/util/result.i +++ b/src/util/result.i @@ -8,13 +8,13 @@ %ignore CVC4::Result::operator!=(const Result& r) const; %ignore CVC4::operator<<(std::ostream&, enum Result::Sat); -%ignore CVC4::operator<<(std::ostream&, enum Result::Validity); +%ignore CVC4::operator<<(std::ostream&, enum Result::Entailment); %ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation); %ignore CVC4::operator==(enum Result::Sat, const Result&); %ignore CVC4::operator!=(enum Result::Sat, const Result&); -%ignore CVC4::operator==(enum Result::Validity, const Result&); -%ignore CVC4::operator!=(enum Result::Validity, const Result&); +%ignore CVC4::operator==(enum Result::Entailment, const Result&); +%ignore CVC4::operator!=(enum Result::Entailment, const Result&); %include "util/result.h" |