This also fixes some minor issues in the `parseenums.py` script.
api/cpp/cvc5.h
api/cpp/cvc5_checks.h
api/cpp/cvc5_kind.h
+ api/cpp/cvc5_types.cpp
api/cpp/cvc5_types.h
decision/assertion_list.cpp
decision/assertion_list.h
return *d_result != *r.d_result;
}
-Result::UnknownExplanation Result::getUnknownExplanation(void) const
+UnknownExplanation Result::getUnknownExplanation(void) const
{
- internal::Result::UnknownExplanation expl = d_result->getUnknownExplanation();
- switch (expl)
- {
- case internal::Result::REQUIRES_FULL_CHECK: return REQUIRES_FULL_CHECK;
- case internal::Result::INCOMPLETE: return INCOMPLETE;
- case internal::Result::TIMEOUT: return TIMEOUT;
- case internal::Result::RESOURCEOUT: return RESOURCEOUT;
- case internal::Result::MEMOUT: return MEMOUT;
- case internal::Result::INTERRUPTED: return INTERRUPTED;
- case internal::Result::NO_STATUS: return NO_STATUS;
- case internal::Result::UNSUPPORTED: return UNSUPPORTED;
- case internal::Result::OTHER: return OTHER;
- default: return UNKNOWN_REASON;
- }
- return UNKNOWN_REASON;
+ return d_result->getUnknownExplanation();
}
std::string Result::toString(void) const { return d_result->toString(); }
return out;
}
-std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e)
-{
- switch (e)
- {
- 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;
- }
- return out;
-}
-
/* -------------------------------------------------------------------------- */
/* SynthResult */
/* -------------------------------------------------------------------------- */
friend class Solver;
public:
- enum UnknownExplanation
- {
- REQUIRES_FULL_CHECK,
- INCOMPLETE,
- TIMEOUT,
- RESOURCEOUT,
- MEMOUT,
- INTERRUPTED,
- NO_STATUS,
- UNSUPPORTED,
- OTHER,
- UNKNOWN_REASON
- };
-
/** Constructor. */
Result();
*/
std::ostream& operator<<(std::ostream& out, const Result& r) CVC5_EXPORT;
-/**
- * Serialize an UnknownExplanation to given stream.
- * @param out the output stream
- * @param e the explanation to be serialized to the given output stream
- * @return the output stream
- */
-std::ostream& operator<<(std::ostream& out,
- enum Result::UnknownExplanation e) CVC5_EXPORT;
-
/* -------------------------------------------------------------------------- */
/* Result */
/* -------------------------------------------------------------------------- */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Common cvc5 types. These types are used internally as well as externally and
+ * the language bindings are generated automatically.
+ */
+
+#include "api/cpp/cvc5_types.h"
+
+#include <iostream>
+
+#include "base/check.h"
+
+namespace cvc5 {
+
+std::ostream& operator<<(std::ostream& out, UnknownExplanation e)
+{
+ switch (e)
+ {
+ case UnknownExplanation::REQUIRES_FULL_CHECK:
+ out << "REQUIRES_FULL_CHECK";
+ break;
+ case UnknownExplanation::INCOMPLETE: out << "INCOMPLETE"; break;
+ case UnknownExplanation::TIMEOUT: out << "TIMEOUT"; break;
+ case UnknownExplanation::RESOURCEOUT: out << "RESOURCEOUT"; break;
+ case UnknownExplanation::MEMOUT: out << "MEMOUT"; break;
+ case UnknownExplanation::INTERRUPTED: out << "INTERRUPTED"; break;
+ case UnknownExplanation::NO_STATUS: out << "NO_STATUS"; break;
+ case UnknownExplanation::UNSUPPORTED: out << "UNSUPPORTED"; break;
+ case UnknownExplanation::OTHER: out << "OTHER"; break;
+ case UnknownExplanation::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
+ default: Unhandled() << e;
+ }
+ return out;
+}
+
+} // namespace cvc5
* directory for licensing information.
* ****************************************************************************
*
- * Common cvc5 types.
+ * Common cvc5 types. These types are used internally as well as externally and
+ * the language bindings are generated automatically.
*/
#include "cvc5_export.h"
#ifndef CVC5__API__CVC5_TYPES_H
#define CVC5__API__CVC5_TYPES_H
+#include <iosfwd>
+
namespace cvc5 {
+/**
+ * The different reasons for returning an "unknown" result.
+ */
+enum UnknownExplanation
+{
+ REQUIRES_FULL_CHECK,
+ INCOMPLETE,
+ TIMEOUT,
+ RESOURCEOUT,
+ MEMOUT,
+ INTERRUPTED,
+ NO_STATUS,
+ UNSUPPORTED,
+ OTHER,
+ UNKNOWN_REASON
+};
+
+/**
+ * Serialize an UnknownExplanation to given stream.
+ * @param out the output stream
+ * @param e the explanation to be serialized to the given output stream
+ * @return the output stream
+ */
+std::ostream& operator<<(std::ostream& out, UnknownExplanation e) CVC5_EXPORT;
+
/**
* Rounding modes for floating-point numbers.
*
set(JAVA_TYPES_FILES
"${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/BlockModelsMode.java"
"${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/RoundingMode.java"
+ "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/UnknownExplanation.java"
)
add_custom_command(
OUTPUT
// endregion
- public enum UnknownExplanation {
- REQUIRES_FULL_CHECK(0),
- INCOMPLETE(1),
- TIMEOUT(2),
- RESOURCEOUT(3),
- MEMOUT(4),
- INTERRUPTED(5),
- NO_STATUS(6),
- UNSUPPORTED(7),
- OTHER(8),
- UNKNOWN_REASON(9);
-
- /* the int value of the UnknownExplanation */
- private int value;
- private static Map<Integer, UnknownExplanation> explanationMap = new HashMap<>();
- private UnknownExplanation(int value)
- {
- this.value = value;
- }
-
- static
- {
- for (UnknownExplanation explanation : UnknownExplanation.values())
- {
- explanationMap.put(explanation.getValue(), explanation);
- }
- }
-
- public static UnknownExplanation fromInt(int value) throws CVC5ApiException
- {
- if (value < REQUIRES_FULL_CHECK.value || value > UNKNOWN_REASON.value)
- {
- throw new CVC5ApiException("UnknownExplanation value " + value
- + " is outside the valid range [" + REQUIRES_FULL_CHECK.value + ","
- + UNKNOWN_REASON.value + "]");
- }
- return explanationMap.get(value);
- }
-
- public int getValue()
- {
- return value;
- }
- }
-
/**
* @return true if Result is empty, i.e., a nullary Result, and not an actual
* result returned from a checkSat() (and friends) query.
if ENUM_END in line:
self.in_enum = False
- break
+ self.last_value = -1
+ continue
elif self.in_enum:
if line == OCB:
continue
fmt_comment = self.format_comment(
self.latest_block_comment)
enum.enumerators_doc[name] = fmt_comment
- elif ENUM_START in line:
+ elif line.startswith(ENUM_START):
self.in_enum = True
tokens = line.split()
name = tokens[1]
from libcpp.map cimport map
from libcpp.pair cimport pair
from cvc5kinds cimport Kind
-from cvc5types cimport RoundingMode
+from cvc5types cimport RoundingMode, UnknownExplanation
cdef extern from "<iostream>" namespace "std":
bint isUnknown() except +
string toString() except +
- cdef extern from "api/cpp/cvc5.h" namespace "cvc5::Result":
- cdef cppclass UnknownExplanation:
- pass
-
-
cdef cppclass Solver:
Solver() except +
Sort getBooleanSort() except +
cdef cppclass TermHashFunction:
TermHashFunction() except +
size_t operator()(const Term & t) except +
-
-
-cdef extern from "api/cpp/cvc5.h" namespace "cvc5::Result::UnknownExplanation":
- cdef UnknownExplanation REQUIRES_FULL_CHECK
- cdef UnknownExplanation INCOMPLETE
- cdef UnknownExplanation TIMEOUT
- cdef UnknownExplanation RESOURCEOUT
- cdef UnknownExplanation MEMOUT
- cdef UnknownExplanation INTERRUPTED
- cdef UnknownExplanation NO_STATUS
- cdef UnknownExplanation UNSUPPORTED
- cdef UnknownExplanation OTHER
- cdef UnknownExplanation UNKNOWN_REASON
from cvc5 cimport DatatypeSelector as c_DatatypeSelector
from cvc5 cimport Result as c_Result
from cvc5 cimport SynthResult as c_SynthResult
-from cvc5 cimport UnknownExplanation as c_UnknownExplanation
from cvc5 cimport Op as c_Op
from cvc5 cimport OptionInfo as c_OptionInfo
from cvc5 cimport holds as c_holds
from cvc5 cimport Stat as c_Stat
from cvc5 cimport Grammar as c_Grammar
from cvc5 cimport Sort as c_Sort
-from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT
-from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED
-from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON
-from cvc5 cimport OTHER
from cvc5 cimport Term as c_Term
from cvc5 cimport hash as c_hash
from cvc5 cimport wstring as c_wstring
from cvc5 cimport get0, get1, get2
from cvc5kinds cimport Kind as c_Kind
from cvc5types cimport RoundingMode as c_RoundingMode
+from cvc5types cimport UnknownExplanation as c_UnknownExplanation
cdef extern from "Python.h":
wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
def __repr__(self):
return self.cr.toString().decode()
-cdef class UnknownExplanation:
- """
- Wrapper class for :cpp:enum:`cvc5::Result::UnknownExplanation`.
- """
- cdef c_UnknownExplanation cue
- cdef str name
- def __cinit__(self, int ue):
- # crm always assigned externally
- self.cue = <c_UnknownExplanation> ue
- self.name = __unknown_explanations[ue]
-
- def __eq__(self, UnknownExplanation other):
- return (<int> self.cue) == (<int> other.cue)
-
- def __ne__(self, UnknownExplanation other):
- return not self.__eq__(other)
-
- def __hash__(self):
- return hash((<int> self.crm, self.name))
-
- def __str__(self):
- return self.name
-
- def __repr__(self):
- return self.name
-
cdef class Solver:
"""Wrapper class for :cpp:class:`cvc5::Solver`."""
res[k] = v
return res
-
-
-# Generate unknown explanations
-cdef __unknown_explanations = {
- <int> REQUIRES_FULL_CHECK: "RequiresFullCheck",
- <int> INCOMPLETE: "Incomplete",
- <int> TIMEOUT: "Timeout",
- <int> RESOURCEOUT: "Resourceout",
- <int> MEMOUT: "Memout",
- <int> INTERRUPTED: "Interrupted",
- <int> NO_STATUS: "NoStatus",
- <int> UNSUPPORTED: "Unsupported",
- <int> OTHER: "Other",
- <int> UNKNOWN_REASON: "UnknownReason"
-}
-
-mod_ref = sys.modules[__name__]
-for ue_int, name in __unknown_explanations.items():
- u = UnknownExplanation(ue_int)
-
- if name in dir(mod_ref):
- raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name)
-
- setattr(mod_ref, name, u)
-
-del u
-del ue_int
-del name
if (d_solver->getOptionInfo("dump-models").boolValue()
&& (isResultSat
|| (res.isUnknown()
- && res.getUnknownExplanation() == cvc5::Result::INCOMPLETE)))
+ && res.getUnknownExplanation()
+ == cvc5::UnknownExplanation::INCOMPLETE)))
{
getterCommands.emplace_back(new GetModelCommand());
}
if (options().base.preprocessOnly)
{
- return Result(Result::UNKNOWN, Result::REQUIRES_FULL_CHECK);
+ return Result(Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK);
}
// Reset the interrupted flag
if( result == SAT_VALUE_UNKNOWN ) {
ResourceManager* rm = resourceManager();
- Result::UnknownExplanation why = Result::INTERRUPTED;
+ UnknownExplanation why = UnknownExplanation::INTERRUPTED;
if (rm->outOfTime())
{
- why = Result::TIMEOUT;
+ why = UnknownExplanation::TIMEOUT;
}
if (rm->outOfResources())
{
- why = Result::RESOURCEOUT;
+ why = UnknownExplanation::RESOURCEOUT;
}
return Result(Result::UNKNOWN, why);
}
Trace("prop") << "PropEngine::checkSat() => " << result << std::endl;
if (result == SAT_VALUE_TRUE && d_theoryProxy->isIncomplete())
{
- return Result(Result::UNKNOWN, Result::INCOMPLETE);
+ return Result(Result::UNKNOWN, UnknownExplanation::INCOMPLETE);
}
return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT);
}
/* Assume: BIGAND assumptions */
d_assumptions = assumptions;
- Result r(Result::UNKNOWN, Result::UNKNOWN_REASON);
+ Result r(Result::UNKNOWN, UnknownExplanation::UNKNOWN_REASON);
for (const Node& e : d_assumptions)
{
// Substitute out any abstract values in ex.
{
return (res.isSat()
|| (res.isUnknown()
- && res.getUnknownExplanation() == cvc5::Result::INCOMPLETE))
+ && res.getUnknownExplanation()
+ == cvc5::UnknownExplanation::INCOMPLETE))
|| res.isUnsat();
}
void GetInstantiationsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
{
}
OptimizationResult()
- : d_result(Result::UNKNOWN, Result::UnknownExplanation::NO_STATUS),
+ : d_result(Result::UNKNOWN, UnknownExplanation::NO_STATUS),
d_value(),
d_infinity(FINITE)
{
ResourceManager* rm = d_env.getResourceManager();
if (rm->out())
{
- Result::UnknownExplanation why =
- rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
+ UnknownExplanation why = rm->outOfResources()
+ ? UnknownExplanation::RESOURCEOUT
+ : UnknownExplanation::TIMEOUT;
result = Result(Result::UNKNOWN, why);
}
else
|| d_env.getOptions().smt.solveIntAsBV > 0)
&& result.getStatus() == Result::UNSAT)
{
- result = Result(Result::UNKNOWN, Result::UNKNOWN_REASON);
+ result = Result(Result::UNKNOWN, UnknownExplanation::UNKNOWN_REASON);
}
// flipped if we did a global negation
if (as.isGlobalNegated())
}
else
{
- result = Result(Result::UNKNOWN, Result::UNKNOWN_REASON);
+ result =
+ Result(Result::UNKNOWN, UnknownExplanation::UNKNOWN_REASON);
}
}
Trace("smt") << "SmtSolver::global negate returned " << result
else
{
// otherwise, we return "unknown"
- sr = SynthResult(SynthResult::UNKNOWN, Result::UNKNOWN_REASON);
+ sr = SynthResult(SynthResult::UNKNOWN, UnknownExplanation::UNKNOWN_REASON);
}
return sr;
}
return Result(Result::SAT);
}
}
- return Result(Result::UNKNOWN, Result::REQUIRES_FULL_CHECK);
+ return Result(Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK);
}
void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
}
}
-Result::UnknownExplanation Result::getUnknownExplanation() const
+UnknownExplanation Result::getUnknownExplanation() const
{
PrettyCheckArgument(isUnknown(), this,
"This result is not unknown, so the reason for "
return out;
}
-ostream& operator<<(ostream& out, enum Result::UnknownExplanation e)
-{
- switch (e)
- {
- 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;
- }
- return out;
-}
-
ostream& operator<<(ostream& out, const Result& r) {
Language language = options::ioutils::getOutputLang(out);
switch (language) {
case Result::SAT: out << "sat"; break;
case Result::UNKNOWN:
out << "unknown";
- if (getUnknownExplanation() != Result::UNKNOWN_REASON)
+ if (getUnknownExplanation() != UnknownExplanation::UNKNOWN_REASON)
{
out << " (" << getUnknownExplanation() << ")";
}
#include <iosfwd>
#include <string>
+#include "api/cpp/cvc5_types.h"
#include "options/language.h"
namespace cvc5::internal {
UNKNOWN
};
- enum UnknownExplanation
- {
- REQUIRES_FULL_CHECK,
- INCOMPLETE,
- TIMEOUT,
- RESOURCEOUT,
- MEMOUT,
- INTERRUPTED,
- NO_STATUS,
- UNSUPPORTED,
- OTHER,
- UNKNOWN_REASON
- };
-
public:
Result();
}; /* class Result */
std::ostream& operator<<(std::ostream& out, enum Result::Status s);
-std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e);
} // namespace cvc5::internal
namespace cvc5::internal {
SynthResult::SynthResult()
- : d_status(NONE), d_unknownExplanation(Result::UNKNOWN_REASON)
+ : d_status(NONE), d_unknownExplanation(UnknownExplanation::UNKNOWN_REASON)
{
}
-SynthResult::SynthResult(Status s,
- Result::UnknownExplanation unknownExplanation)
+SynthResult::SynthResult(Status s, UnknownExplanation unknownExplanation)
: d_status(s), d_unknownExplanation(unknownExplanation)
{
}
SynthResult::Status SynthResult::getStatus() const { return d_status; }
-Result::UnknownExplanation SynthResult::getUnknownExplanation() const
+UnknownExplanation SynthResult::getUnknownExplanation() const
{
return d_unknownExplanation;
}
{
std::stringstream ss;
ss << "(" << d_status;
- if (d_unknownExplanation != Result::UNKNOWN_REASON)
+ if (d_unknownExplanation != UnknownExplanation::UNKNOWN_REASON)
{
ss << " :unknown-explanation " << d_unknownExplanation;
}
/** Default constructor */
SynthResult();
/** Constructor when the solution is not successful */
- SynthResult(
- Status s,
- Result::UnknownExplanation unknownExplanation = Result::UNKNOWN_REASON);
+ SynthResult(Status s,
+ UnknownExplanation unknownExplanation =
+ UnknownExplanation::UNKNOWN_REASON);
/** Get the status */
Status getStatus() const;
/** Get the unknown explanation */
- Result::UnknownExplanation getUnknownExplanation() const;
+ UnknownExplanation getUnknownExplanation() const;
/** Get the string representation */
std::string toString() const;
/** The status */
Status d_status;
/** The unknown explanation */
- Result::UnknownExplanation d_unknownExplanation;
+ UnknownExplanation d_unknownExplanation;
};
std::ostream& operator<<(std::ostream& out, const SynthResult& r);
projects / cvc5.git / commitdiff