This significantly refactors the internal result class. Entailments and "which" field are deleted, "Sat" is renamed to "Status". Moreover "TYPE_NONE" is made into a status.
Simplifies the usage of this class throughout the code.
It also changes the API Result method isSatUnknown to isUnknown.
bool Result::isNull() const
{
- return d_result->getType() == cvc5::Result::TYPE_NONE;
+ return d_result->getStatus() == cvc5::Result::NONE;
}
bool Result::isSat(void) const
{
- return d_result->getType() == cvc5::Result::TYPE_SAT
- && d_result->isSat() == cvc5::Result::SAT;
+ return d_result->getStatus() == cvc5::Result::SAT;
}
bool Result::isUnsat(void) const
{
- return d_result->getType() == cvc5::Result::TYPE_SAT
- && d_result->isSat() == cvc5::Result::UNSAT;
+ return d_result->getStatus() == cvc5::Result::UNSAT;
}
-bool Result::isSatUnknown(void) const
+bool Result::isUnknown(void) const
{
- return d_result->getType() == cvc5::Result::TYPE_SAT
- && d_result->isSat() == cvc5::Result::SAT_UNKNOWN;
+ return d_result->getStatus() == cvc5::Result::UNKNOWN;
}
bool Result::operator==(const Result& r) const
Result::UnknownExplanation Result::getUnknownExplanation(void) const
{
- cvc5::Result::UnknownExplanation expl = d_result->whyUnknown();
+ cvc5::Result::UnknownExplanation expl = d_result->getUnknownExplanation();
switch (expl)
{
case cvc5::Result::REQUIRES_FULL_CHECK: return REQUIRES_FULL_CHECK;
* Return true if query was a checkSat() or checkSatAssuming() query and
* cvc5 was not able to determine (un)satisfiability.
*/
- bool isSatUnknown() const;
+ bool isUnknown() const;
/**
* Operator overloading for equality of two results.
* Return true if query was a checkSat() or checkSatAssuming() query and
* cvc5 was not able to determine (un)satisfiability.
*/
- public boolean isSatUnknown()
- {
- return isSatUnknown(pointer);
+ public boolean isUnknown() {
+ return isUnknown(pointer);
}
- private native boolean isSatUnknown(long pointer);
+ private native boolean isUnknown(long pointer);
/**
* Operator overloading for equality of two results.
/*
* Class: io_github_cvc5_api_Result
- * Method: isSatUnknown
+ * Method: isUnknown
* Signature: (J)Z
*/
JNIEXPORT jboolean JNICALL
-Java_io_github_cvc5_api_Result_isSatUnknown(JNIEnv* env, jobject, jlong pointer)
+Java_io_github_cvc5_api_Result_isUnknown(JNIEnv* env, jobject, jlong pointer)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Result* current = (Result*)pointer;
- return (jboolean)current->isSatUnknown();
+ return (jboolean)current->isUnknown();
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
}
bint isNull() except +
bint isSat() except +
bint isUnsat() except +
- bint isSatUnknown() except +
+ bint isUnknown() except +
bint operator==(const Result& r) except +
bint operator!=(const Result& r) except +
UnknownExplanation getUnknownExplanation() except +
"""
return self.cr.isUnsat()
- def isSatUnknown(self):
+ def isUnknown(self):
"""
:return: True if query was a :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query and cvc5 was not able to determine (un)satisfiability.
"""
- return self.cr.isSatUnknown()
+ return self.cr.isUnknown()
def getUnknownExplanation(self):
"""
std::vector<std::unique_ptr<Command> > getterCommands;
if (d_solver->getOptionInfo("dump-models").boolValue()
&& (isResultSat
- || (res.isSatUnknown()
+ || (res.isUnknown()
&& res.getUnknownExplanation() == api::Result::INCOMPLETE)))
{
getterCommands.emplace_back(new GetModelCommand());
}
if (d_solver->getOptionInfo("dump-difficulty").boolValue()
- && (isResultUnsat || isResultSat || res.isSatUnknown()))
+ && (isResultUnsat || isResultSat || res.isUnknown()))
{
getterCommands.emplace_back(new GetDifficultyCommand());
}
// Model-value of objective (used in optimization loop)
Node value;
if (intermediateSatResult.isUnknown()
- || intermediateSatResult.isSat() == Result::UNSAT)
+ || intermediateSatResult.getStatus() == Result::UNSAT)
{
return OptimizationResult(intermediateSatResult, value);
}
nm->mkNode(LTOperator, target, nm->mkConst(pivot))));
}
intermediateSatResult = optChecker->checkSat();
- switch (intermediateSatResult.isSat())
+ switch (intermediateSatResult.getStatus())
{
- case Result::SAT_UNKNOWN:
+ case Result::UNKNOWN:
optChecker->pop();
return OptimizationResult(intermediateSatResult, value);
case Result::SAT:
// Model-value of objective (used in optimization loop)
Node value;
if (intermediateSatResult.isUnknown()
- || intermediateSatResult.isSat() == Result::UNSAT)
+ || intermediateSatResult.getStatus() == Result::UNSAT)
{
return OptimizationResult(intermediateSatResult, value);
}
nm->mkNode(GTOperator, target, nm->mkConst(pivot)),
nm->mkNode(LEOperator, target, nm->mkConst(upperBound))));
intermediateSatResult = optChecker->checkSat();
- switch (intermediateSatResult.isSat())
+ switch (intermediateSatResult.getStatus())
{
- case Result::SAT_UNKNOWN:
+ case Result::UNKNOWN:
optChecker->pop();
return OptimizationResult(intermediateSatResult, value);
case Result::SAT:
// Model-value of objective (used in optimization loop)
Node value;
if (intermediateSatResult.isUnknown()
- || intermediateSatResult.isSat() == Result::UNSAT)
+ || intermediateSatResult.getStatus() == Result::UNSAT)
{
return OptimizationResult(intermediateSatResult, value);
}
// This loop will keep incrmenting/decrementing the objective until unsat
// When unsat is hit,
// the optimized value is the model value just before the unsat call
- while (intermediateSatResult.isSat() == Result::SAT)
+ while (intermediateSatResult.getStatus() == Result::SAT)
{
lastSatResult = intermediateSatResult;
value = optChecker->getValue(target);
if (options().base.preprocessOnly)
{
- return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
+ return Result(Result::UNKNOWN, Result::REQUIRES_FULL_CHECK);
}
// Reset the interrupted flag
{
why = Result::RESOURCEOUT;
}
- return Result(Result::SAT_UNKNOWN, why);
+ return Result(Result::UNKNOWN, why);
}
if( result == SAT_VALUE_TRUE && TraceIsOn("prop") ) {
Trace("prop") << "PropEngine::checkSat() => " << result << std::endl;
if (result == SAT_VALUE_TRUE && d_theoryProxy->isIncomplete())
{
- return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
+ return Result(Result::UNKNOWN, Result::INCOMPLETE);
}
return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT);
}
bool isError = false;
if (j == 0)
{
- if (r.asSatisfiabilityResult().isSat() != Result::SAT)
+ if (r.getStatus() != Result::SAT)
{
isError = true;
serr
}
else
{
- if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+ if (r.getStatus() != Result::UNSAT)
{
isError = true;
serr << "SolverEngine::checkAbduct(): negated goal cannot be shown "
/* Assume: BIGAND assumptions */
d_assumptions = assumptions;
- Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+ Result r(Result::UNKNOWN, Result::UNKNOWN_REASON);
for (const Node& e : d_assumptions)
{
// Substitute out any abstract values in ex.
const api::Result& res)
{
return (res.isSat()
- || (res.isSatUnknown()
+ || (res.isUnknown()
&& res.getUnknownExplanation() == api::Result::INCOMPLETE))
|| res.isUnsat();
}
Trace("check-interpol") << "SolverEngine::checkInterpol: phase " << j
<< ": result is " << r << std::endl;
std::stringstream serr;
- if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+ if (r.getStatus() != Result::UNSAT)
{
if (j == 0)
{
<< "Only the SMTLib2 language supports optimization right now";
}
out << "(" << result.getResult();
- switch (result.getResult().isSat())
+ switch (result.getResult().getStatus())
{
case Result::SAT:
- case Result::SAT_UNKNOWN:
+ case Result::UNKNOWN:
{
switch (result.isInfinity())
{
// resets the optChecker
d_optChecker = createOptCheckerWithTimeout(d_parent);
OptimizationResult partialResult;
- Result aggregatedResult(Result::Sat::SAT);
+ Result aggregatedResult(Result::SAT);
std::unique_ptr<OMTOptimizer> optimizer;
for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
{
}
// match the optimization result type, and aggregate the results of
// subproblems
- switch (partialResult.getResult().isSat())
+ switch (partialResult.getResult().getStatus())
{
case Result::SAT: break;
case Result::UNSAT:
}
d_optChecker.reset();
return partialResult.getResult();
- case Result::SAT_UNKNOWN:
- aggregatedResult = partialResult.getResult();
- break;
+ case Result::UNKNOWN: aggregatedResult = partialResult.getResult(); break;
default: Unreachable();
}
d_results[i] = partialResult;
// checks the optimization result of the current objective
- switch (partialResult.getResult().isSat())
+ switch (partialResult.getResult().getStatus())
{
case Result::SAT:
// assert target[i] == value[i] and proceed
case Result::UNSAT:
d_optChecker.reset();
return partialResult.getResult();
- case Result::SAT_UNKNOWN:
+ case Result::UNKNOWN:
d_optChecker.reset();
return partialResult.getResult();
default: Unreachable();
// checks whether the current set of assertions are satisfied or not
Result satResult = d_optChecker->checkSat();
- switch (satResult.isSat())
+ switch (satResult.getStatus())
{
- case Result::Sat::UNSAT:
- case Result::Sat::SAT_UNKNOWN: return satResult;
- case Result::Sat::SAT:
+ case Result::UNSAT:
+ case Result::UNKNOWN: return satResult;
+ case Result::SAT:
{
// if satisfied, use d_results to store the initial results
// they will be gradually updated and optimized
std::vector<Node> someObjBetter;
d_optChecker->push();
- while (satResult.isSat() == Result::Sat::SAT)
+ while (satResult.getStatus() == Result::SAT)
{
noWorseObj.clear();
someObjBetter.clear();
// checks if previous assertions + noWorseObj + someObjBetter are satisfied
satResult = d_optChecker->checkSat();
- switch (satResult.isSat())
+ switch (satResult.getStatus())
{
- case Result::Sat::UNSAT:
+ case Result::UNSAT:
// if result is UNSAT, it means no more improvement could be made,
// then the results stored in d_results are one of the Pareto optimal
// results
break;
- case Result::Sat::SAT_UNKNOWN:
+ case Result::UNKNOWN:
// if result is UNKNOWN, abort the current session and return UNKNOWN
d_optChecker.reset();
return satResult;
- case Result::Sat::SAT:
+ case Result::SAT:
{
lastSatResult = satResult;
// if result is SAT, update d_results to the more optimal values
{
}
OptimizationResult()
- : d_result(Result::Sat::SAT_UNKNOWN,
- Result::UnknownExplanation::NO_STATUS),
+ : d_result(Result::UNKNOWN, Result::UnknownExplanation::NO_STATUS),
d_value(),
d_infinity(FINITE)
{
/**
* Returns an enum indicating whether
* the result is SAT or not.
- * @return whether the result is SAT, UNSAT or SAT_UNKNOWN
+ * @return whether the result is SAT, UNSAT or UNKNOWN
**/
Result getResult() const { return d_result; }
* @return Node containing the optimal value,
* if result is infinite, this will be an empty node,
* if getResult() is UNSAT, it will return an empty node,
- * if getResult() is SAT_UNKNOWN, it will return something suboptimal
+ * if getResult() is UNKNOWN, it will return something suboptimal
* or an empty node, depending on how the solver runs.
**/
Node getValue() const { return d_value; }
/**
* Optimize multiple goals in Box order
* @return SAT if all of the objectives are optimal (could be infinite);
- * UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN;
- * SAT_UNKNOWN if any of the objective is SAT_UNKNOWN.
+ * UNSAT if at least one objective is UNSAT and no objective is UNKNOWN;
+ * UNKNOWN if any of the objective is UNKNOWN.
**/
Result optimizeBox();
* the optimization will stop at that objective;
* UNSAT if any of the objectives is UNSAT
* and optimization will stop at that objective;
- * SAT_UNKNOWN if any of the objectives is UNKNOWN
+ * UNKNOWN if any of the objectives is UNKNOWN
* and optimization will stop at that objective;
* If the optimization is stopped at an objective,
- * all objectives following that objective will be SAT_UNKNOWN.
+ * all objectives following that objective will be UNKNOWN.
**/
Result optimizeLexicographicIterative();
*
* @return if it finds a new Pareto optimal result it will return SAT;
* if it exhausts the results in the Pareto front it will return UNSAT;
- * if the underlying SMT solver returns SAT_UNKNOWN,
- * it will return SAT_UNKNOWN.
+ * if the underlying SMT solver returns UNKNOWN,
+ * it will return UNKNOWN.
**/
Result optimizeParetoNaiveGIA();
Result r =
d_smtSolver.checkSatisfiability(as, std::vector<Node>{ne.notNode()});
Trace("smt-qe") << "Query returned " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+ if (r.getStatus() != Result::UNSAT)
{
- if (r.asSatisfiabilityResult().isSat() != Result::SAT && doFull)
+ if (r.getStatus() != Result::SAT && doFull)
{
verbose(1)
<< "While performing quantifier elimination, unexpected result : "
case SmtMode::START: out << "START"; break;
case SmtMode::ASSERT: out << "ASSERT"; break;
case SmtMode::SAT: out << "SAT"; break;
- case SmtMode::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break;
+ case SmtMode::SAT_UNKNOWN: out << "UNKNOWN"; break;
case SmtMode::UNSAT: out << "UNSAT"; break;
case SmtMode::ABDUCT: out << "ABDUCT"; break;
case SmtMode::INTERPOL: out << "INTERPOL"; break;
{
Result::UnknownExplanation why =
rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
- result = Result(Result::ENTAILMENT_UNKNOWN, why);
+ result = Result(Result::UNKNOWN, why);
}
else
{
if ((d_env.getOptions().smt.solveRealAsInt
|| d_env.getOptions().smt.solveIntAsBV > 0)
- && result.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ && result.getStatus() == Result::UNSAT)
{
- result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+ result = Result(Result::UNKNOWN, Result::UNKNOWN_REASON);
}
// flipped if we did a global negation
if (as.isGlobalNegated())
{
Trace("smt") << "SmtSolver::process global negate " << result
<< std::endl;
- if (result.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (result.getStatus() == Result::UNSAT)
{
result = Result(Result::SAT);
}
- else if (result.asSatisfiabilityResult().isSat() == Result::SAT)
+ else if (result.getStatus() == Result::SAT)
{
// Only can answer unsat if the theory is satisfaction complete. This
// includes linear arithmetic and bitvectors, which are the primary
}
else
{
- result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+ result = Result(Result::UNKNOWN, Result::UNKNOWN_REASON);
}
}
Trace("smt") << "SmtSolver::global negate returned " << result
{
// sat | unsat | unknown
Result status = d_state->getStatus();
- switch (status.asSatisfiabilityResult().isSat())
+ switch (status.getStatus())
{
case Result::SAT: return "sat";
case Result::UNSAT: return "unsat";
if (!status.isNull() && status.isUnknown())
{
std::stringstream ss;
- ss << status.whyUnknown();
+ ss << status.getUnknownExplanation();
std::string s = ss.str();
transform(s.begin(), s.end(), s.begin(), ::tolower);
return s;
defineFunctionsRec(funcs, formals_multi, formulas, global);
}
-Result SolverEngine::quickCheck()
-{
- Assert(d_state->isFullyInited());
- Trace("smt") << "SMT quickCheck()" << endl;
- const std::string& filename = d_env->getOptions().driver.filename;
- return Result(
- Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
-}
-
TheoryModel* SolverEngine::getAvailableModel(const char* c) const
{
if (!d_env->getOptions().theory.assignFunctionValues)
// Check that SAT results generate a model correctly.
if (d_env->getOptions().smt.checkModels)
{
- if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ if (r.getStatus() == Result::SAT)
{
checkModel();
}
// Check that UNSAT results generate a proof correctly.
if (d_env->getOptions().smt.checkProofs)
{
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
checkProof();
}
// Check that UNSAT results generate an unsat core correctly.
if (d_env->getOptions().smt.checkUnsatCores)
{
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
checkUnsatCore();
return res;
}
-Result SolverEngine::assertFormula(const Node& formula)
+void SolverEngine::assertFormula(const Node& formula)
{
SolverEngineScope smts(this);
finishInit();
d_state->doPendingPops();
ensureWellFormedTerm(formula, "assertFormula");
- return assertFormulaInternal(formula);
+ assertFormulaInternal(formula);
}
-Result SolverEngine::assertFormulaInternal(const Node& formula)
+void SolverEngine::assertFormulaInternal(const Node& formula)
{
// as an optimization we do not check whether formula is well-formed here, and
// defer this check for certain cases within the assertions module.
Node n = d_absValues->substituteAbstractValues(formula);
d_asserts->assertFormula(n);
- return quickCheck().asEntailmentResult();
}
/*
return ssm.str();
}
-Result SolverEngine::blockModel()
+void SolverEngine::blockModel()
{
Trace("smt") << "SMT blockModel()" << endl;
SolverEngineScope smts(this);
Node eblocker = mb.getModelBlocker(
eassertsProc, m, d_env->getOptions().smt.blockModelsMode);
Trace("smt") << "Block formula: " << eblocker << std::endl;
- return assertFormulaInternal(eblocker);
+ assertFormulaInternal(eblocker);
}
-Result SolverEngine::blockModelValues(const std::vector<Node>& exprs)
+void SolverEngine::blockModelValues(const std::vector<Node>& exprs)
{
Trace("smt") << "SMT blockModelValues()" << endl;
SolverEngineScope smts(this);
ModelBlocker mb(*d_env.get());
Node eblocker = mb.getModelBlocker(
eassertsProc, m, options::BlockModelsMode::VALUES, exprs);
- return assertFormulaInternal(eblocker);
+ assertFormulaInternal(eblocker);
}
std::pair<Node, Node> SolverEngine::getSepHeapAndNilExpr(void)
throw;
}
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
removed.insert(skip);
}
- else if (r.asSatisfiabilityResult().isUnknown())
+ else if (r.isUnknown())
{
d_env->warning()
<< "SolverEngine::reduceUnsatCore(): could not reduce unsat core "
}
d_env->verbose(1) << "SolverEngine::checkUnsatCore(): result is " << r
<< std::endl;
- if (r.asSatisfiabilityResult().isUnknown())
+ if (r.isUnknown())
{
d_env->warning() << "SolverEngine::checkUnsatCore(): could not check core result "
"unknown."
<< std::endl;
}
- else if (r.asSatisfiabilityResult().isSat())
+ else if (r.getStatus() == Result::SAT)
{
InternalError()
<< "SolverEngine::checkUnsatCore(): produced core was satisfiable.";
*
* This adds an assertion to the assertion stack that blocks the current
* model based on the current options configured by cvc5.
- *
- * The return value has the same meaning as that of assertFormula.
*/
- Result blockModel();
+ void blockModel();
/**
* Block the current model values of (at least) the values in exprs.
* This adds an assertion to the assertion stack of the form:
* (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn)))
* where M0 ... Mn are the current model values of exprs[0] ... exprs[n].
- *
- * The return value has the same meaning as that of assertFormula.
*/
- Result blockModelValues(const std::vector<Node>& exprs);
+ void blockModelValues(const std::vector<Node>& exprs);
/**
* Declare heap. For smt2 inputs, this is called when the command
/**
* Add a formula to the current context: preprocess, do per-theory
* setup, use processAssertionList(), asserting to T-solver for
- * literals and conjunction of literals. Returns false if
- * immediately determined to be inconsistent. Note this formula will
+ * literals and conjunction of literals. Note this formula will
* be included in the unsat core when applicable.
*
* @throw TypeCheckingException, LogicException
*/
- Result assertFormula(const Node& formula);
+ void assertFormula(const Node& formula);
/**
* Reduce an unsatisfiable core to make it minimal.
/**
* Assert a formula (if provided) to the current context and call
- * check(). Returns SAT, UNSAT, or SAT_UNKNOWN result.
+ * check(). Returns SAT, UNSAT, or UNKNOWN result.
*
* @throw Exception
*/
UnsatCore getUnsatCoreInternal();
/** Internal version of assertFormula */
- Result assertFormulaInternal(const Node& formula);
+ void assertFormulaInternal(const Node& formula);
/**
* Check that a generated proof checks. This method is the same as printProof,
*/
void shutdown();
- /**
- * Quick check of consistency in current context: calls
- * processAssertionList() then look for inconsistency (based only on
- * that).
- */
- Result quickCheck();
-
/**
* Get the (SMT-level) model pointer, if we are in SAT mode. Otherwise,
* return nullptr.
<< "SolverEngineState::notifyExpectedStatus: unexpected status string "
<< status;
d_expectedStatus = Result(status, options().driver.filename);
+ Assert(d_expectedStatus.getStatus() != Result::NONE);
}
void SolverEngineState::notifyResetAssertions()
// Remember the status
d_status = r;
- // Check against expected status
- if (!d_expectedStatus.isUnknown() && !d_status.isUnknown()
- && d_status != d_expectedStatus)
+ // Check against expected status, if it is set
+ if (d_expectedStatus.getStatus() != Result::NONE)
{
- CVC5_FATAL() << "Expected result " << d_expectedStatus << " but got "
- << d_status;
+ // unknown results don't give an error
+ if (!d_expectedStatus.isUnknown() && !d_status.isUnknown()
+ && d_status != d_expectedStatus)
+ {
+ CVC5_FATAL() << "Expected result " << d_expectedStatus << " but got "
+ << d_status;
+ }
}
// clear expected status
d_expectedStatus = Result();
// Update the SMT mode
- switch (d_status.asSatisfiabilityResult().isSat())
+ switch (d_status.getStatus())
{
case Result::UNSAT: d_smtMode = SmtMode::UNSAT; break;
case Result::SAT: d_smtMode = SmtMode::SAT; break;
void SolverEngineState::notifyCheckSynthResult(Result r)
{
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
// successfully generated a synthesis solution, update to abduct state
d_smtMode = SmtMode::SYNTH;
else
{
// otherwise, we return "unknown"
- r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+ r = Result(Result::UNKNOWN, Result::UNKNOWN_REASON);
}
return r;
}
verbose(1) << "SyGuS::checkSynthSolution: result is " << r << std::endl;
}
Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
- if (r.asSatisfiabilityResult().isUnknown())
+ if (r.isUnknown())
{
InternalError() << "SygusSolver::checkSynthSolution(): could not check "
"solution, result "
"unknown.";
}
- else if (r.asSatisfiabilityResult().isSat())
+ else if (r.getStatus() == Result::SAT)
{
InternalError()
<< "SygusSolver::checkSynthSolution(): produced solution leads to "
return nv[v] == d_variables.getAssignment(v);
}
-Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol){
+Result::Status AttemptSolutionSDP::attempt(
+ const ApproximateSimplex::Solution& sol)
+{
const DenseSet& newBasis = sol.newBasis;
const DenseMap<DeltaRational>& newValues = sol.newValues;
return Result::SAT;
}else{
d_errorSet.reduceToSignals();
- return Result::SAT_UNKNOWN;
+ return Result::UNKNOWN;
}
}
RaiseConflict conflictChannel,
TempVarMalloc tvmalloc);
- Result::Sat attempt(const ApproximateSimplex::Solution& sol);
+ Result::Status attempt(const ApproximateSimplex::Solution& sol);
- Result::Sat findModel(bool exactResult) override { Unreachable(); }
+ Result::Status findModel(bool exactResult) override { Unreachable(); }
private:
bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const;
{
}
-Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
+Result::Status DualSimplexDecisionProcedure::dualFindModel(bool exactResult)
+{
Assert(d_conflictVariables.empty());
d_pivots = 0;
Trace("arith::findModel") << "dualFindModel() start non-trivial" << endl;
- Result::Sat result = Result::SAT_UNKNOWN;
+ Result::Status result = Result::UNKNOWN;
exactResult |= d_varOrderPivotLimit < 0;
uint32_t checkPeriod = options().arith.arithSimplexCheckPeriod;
- if(result == Result::SAT_UNKNOWN){
+ if (result == Result::UNKNOWN)
+ {
uint32_t numDifferencePivots = options().arith.arithHeuristicPivots < 0
? d_numVariables + 1
: options().arith.arithHeuristicPivots;
}
Assert(!d_errorSet.moreSignals());
- if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
+ if (result == Result::UNKNOWN && d_errorSet.errorEmpty())
+ {
result = Result::SAT;
}
RaiseConflict conflictChannel,
TempVarMalloc tvmalloc);
- Result::Sat findModel(bool exactResult) override
+ Result::Status findModel(bool exactResult) override
{
return dualFindModel(exactResult);
}
*/
DenseMultiset d_pivotsInRound;
- Result::Sat dualFindModel(bool exactResult);
+ Result::Status dualFindModel(bool exactResult);
/**
* This is the main simplex for DPLL(T) loop.
{
}
-Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
+Result::Status FCSimplexDecisionProcedure::findModel(bool exactResult)
+{
Assert(d_conflictVariables.empty());
Assert(d_sgnDisagreements.empty());
d_prevWitnessImprovement = HeuristicDegenerate;
d_witnessImprovementInARow = 0;
- Result::Sat result = Result::SAT_UNKNOWN;
+ Result::Status result = Result::UNKNOWN;
- if(result == Result::SAT_UNKNOWN){
+ if (result == Result::UNKNOWN)
+ {
if(exactResult){
d_pivotBudget = -1;
}else{
}
Assert(!d_errorSet.moreSignals());
- if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
+ if (result == Result::UNKNOWN && d_errorSet.errorEmpty())
+ {
result = Result::SAT;
}
return false;
}
-Result::Sat FCSimplexDecisionProcedure::dualLike(){
-
+Result::Status FCSimplexDecisionProcedure::dualLike()
+{
TimerStat::CodeTimer codeTimer(d_statistics.d_fcTimer);
Assert(d_sgnDisagreements.empty());
return Result::SAT;
}else{
Assert(d_pivotBudget == 0);
- return Result::SAT_UNKNOWN;
+ return Result::UNKNOWN;
}
}
RaiseConflict conflictChannel,
TempVarMalloc tvmalloc);
- Result::Sat findModel(bool exactResult) override;
+ Result::Status findModel(bool exactResult) override;
// other error variables are dropping
WitnessImprovement dualLikeImproveError(ArithVar evar);
// dual like
// - found conflict
// - satisfied error set
- Result::Sat dualLike();
+ Result::Status dualLike();
private:
static constexpr uint32_t PENALTY = 4;
d_model.reset(d_containing.getValuation().getModel(), arithModel);
// run a last call effort check
Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
- Result::Sat res = modelBasedRefinement(termSet);
- if (res == Result::Sat::SAT)
+ Result::Status res = modelBasedRefinement(termSet);
+ if (res == Result::SAT)
{
Trace("nl-ext") << "interceptModel: do model repair" << std::endl;
// modify the model values
d_trSlv.postProcessModel(arithModel, termSet);
}
-Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
+Result::Status NonlinearExtension::modelBasedRefinement(
+ const std::set<Node>& termSet)
{
++(d_stats.d_mbrRuns);
d_checkCounter++;
if (d_im.hasSentLemma() || d_im.hasPendingLemma())
{
d_im.clearWaitingLemmas();
- return Result::Sat::UNSAT;
+ return Result::UNSAT;
}
}
Trace("nl-ext") << "Finished check with status : " << complete_status
if (d_im.hasUsed())
{
d_im.clearWaitingLemmas();
- return Result::Sat::UNSAT;
+ return Result::UNSAT;
}
}
d_im.flushWaitingLemmas();
Trace("nl-ext") << "...added " << count << " waiting lemmas."
<< std::endl;
- return Result::Sat::UNSAT;
+ return Result::UNSAT;
}
// we are incomplete
"NonLinearExtension, set incomplete"
<< std::endl;
d_containing.getOutputChannel().setIncomplete(IncompleteId::ARITH_NL);
- return Result::Sat::SAT_UNKNOWN;
+ return Result::UNKNOWN;
}
}
d_im.clearWaitingLemmas();
} while (needsRecheck);
// did not add lemmas
- return Result::Sat::SAT;
+ return Result::SAT;
}
void NonlinearExtension::runStrategy(Theory::Effort effort,
* the current candidate model.
*
* This function returns whether we found a satisfying assignment
- * (Result::Sat::SAT), or not (Result::Sat::UNSAT). Note that UNSAT does not
+ * (Result::SAT), or not (Result::UNSAT). Note that UNSAT does not
* necessarily means the whole query is UNSAT, but that the linear model was
* refuted by a lemma.
*/
- Result::Sat modelBasedRefinement(const std::set<Node>& termSet);
+ Result::Status modelBasedRefinement(const std::set<Node>& termSet);
/** get assertions
*
*
* Corresponds to the "check()" procedure in [Cav06].
*/
- virtual Result::Sat findModel(bool exactResult) = 0;
+ virtual Result::Status findModel(bool exactResult) = 0;
void increaseMax() { d_numVariables++; }
{
}
-Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
+Result::Status SumOfInfeasibilitiesSPD::findModel(bool exactResult)
+{
Assert(d_conflictVariables.empty());
Assert(d_sgnDisagreements.empty());
d_prevWitnessImprovement = HeuristicDegenerate;
d_witnessImprovementInARow = 0;
- Result::Sat result = Result::SAT_UNKNOWN;
+ Result::Status result = Result::UNKNOWN;
- if(result == Result::SAT_UNKNOWN){
+ if (result == Result::UNKNOWN)
+ {
if(exactResult){
d_pivotBudget = -1;
}else{
}
Assert(!d_errorSet.moreSignals());
- if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
+ if (result == Result::UNKNOWN && d_errorSet.errorEmpty())
+ {
result = Result::SAT;
}
}
}
-Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){
+Result::Status SumOfInfeasibilitiesSPD::sumOfInfeasibilities()
+{
TimerStat::CodeTimer codeTimer(d_statistics.d_soiTimer);
Assert(d_sgnDisagreements.empty());
return Result::SAT;
}else{
Assert(d_pivotBudget == 0);
- return Result::SAT_UNKNOWN;
+ return Result::UNKNOWN;
}
}
RaiseConflict conflictChannel,
TempVarMalloc tvmalloc);
- Result::Sat findModel(bool exactResult) override;
+ Result::Status findModel(bool exactResult) override;
// other error variables are dropping
WitnessImprovement dualLikeImproveError(ArithVar evar);
// dual like
// - found conflict
// - satisfied error set
- Result::Sat sumOfInfeasibilities();
+ Result::Status sumOfInfeasibilities();
int32_t d_pivotBudget;
d_congruenceManager,
RaiseConflict(*this),
d_pfGen.get()),
- d_qflraStatus(Result::SAT_UNKNOWN),
+ d_qflraStatus(Result::UNKNOWN),
d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
d_learner(userContext()),
d_solveIntMaybeHelp(0u),
d_solveIntAttempts(0u),
d_newFacts(false),
- d_previousStatus(Result::SAT_UNKNOWN),
+ d_previousStatus(Result::UNKNOWN),
d_statistics(statisticsRegistry(), "theory::arith::")
{
}
}
/* It is not clear what the d_qflraStatus is at this point */
- d_qflraStatus = Result::SAT_UNKNOWN;
+ d_qflraStatus = Result::UNKNOWN;
Assert(d_replayVariables.empty());
Assert(d_replayConstraints.empty());
{
// if at this point the linear relaxation is still unknown,
// attempt to branch an integer variable as a last ditch effort on full check
- if (d_qflraStatus == Result::SAT_UNKNOWN)
+ if (d_qflraStatus == Result::UNKNOWN)
{
d_qflraStatus = selectSimplex(true).findModel(false);
}
- if (Theory::fullEffort(effortLevel) && d_qflraStatus == Result::SAT_UNKNOWN)
+ if (Theory::fullEffort(effortLevel) && d_qflraStatus == Result::UNKNOWN)
{
ArithVar canBranch = nextIntegerViolation(false);
if (canBranch != ARITHVAR_SENTINEL)
Trace("TheoryArithPrivate::solveRealRelaxation")
<< "solveRealRelaxation()" << " pass1 " << d_qflraStatus << endl;
- if(d_qflraStatus == Result::SAT_UNKNOWN && useApprox && safeToCallApprox()){
+ if (d_qflraStatus == Result::UNKNOWN && useApprox && safeToCallApprox())
+ {
// pass2: fancy-final
static constexpr int32_t relaxationLimit = 10000;
Assert(ApproximateSimplex::enabled());
d_previousStatus = d_qflraStatus;
if (d_newFacts)
{
- d_qflraStatus = Result::SAT_UNKNOWN;
+ d_qflraStatus = Result::UNKNOWN;
d_hasDoneWorkSinceCut = true;
}
return false;
}
}
break;
- case Result::SAT_UNKNOWN:
+ case Result::UNKNOWN:
++d_unknownsInARow;
++(d_statistics.d_unknownChecks);
Assert(!Theory::fullEffort(effortLevel));
DeltaRational TheoryArithPrivate::getDeltaValue(TNode term) const
{
- AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN);
+ AlwaysAssert(d_qflraStatus != Result::UNKNOWN);
Trace("arith::value") << term << std::endl;
if (d_partialModel.hasArithVar(term)) {
}
EqualityStatus TheoryArithPrivate::getEqualityStatus(TNode a, TNode b) {
- if(d_qflraStatus == Result::SAT_UNKNOWN){
+ if (d_qflraStatus == Result::UNKNOWN)
+ {
return EQUALITY_UNKNOWN;
}else{
try {
*/
ConstraintDatabase d_constraintDatabase;
- enum Result::Sat d_qflraStatus;
+ enum Result::Status d_qflraStatus;
// check()
// !done() -> d_qflraStatus = Unknown
// fullEffort(e) -> simplex returns either sat or unsat
/** Whether there were new facts during preCheck */
bool d_newFacts;
/** The previous status, computed during preCheck */
- Result::Sat d_previousStatus;
+ Result::Status d_previousStatus;
//---------------- end during check
/** These fields are designed to be accessible to TheoryArith methods. */
initializeChecker(rrChecker, crr);
Result r = rrChecker->checkSat();
Trace("rr-check") << "...result : " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ if (r.getStatus() == Result::SAT)
{
Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
NodeManager* nm = NodeManager::currentNM();
}
else
{
- verified = !r.asSatisfiabilityResult().isUnknown();
+ verified = !r.isUnknown();
}
}
else
if (options().quantifiers.sygusQueryGenDumpFiles
== options::SygusQueryDumpFilesMode::UNSOLVED)
{
- if (r.asSatisfiabilityResult().isSat() == Result::SAT
- || r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::SAT || r.getStatus() == Result::UNSAT)
{
return;
}
initializeChecker(queryChecker, qy);
r = queryChecker->checkSat();
Trace("sygus-qgen-check") << " query: ...got : " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
std::stringstream ss;
ss << "--sygus-rr-query-gen detected unsoundness in cvc5 on input " << qy
std::vector<Node> aTermCurr = activeTerms;
std::shuffle(aTermCurr.begin(), aTermCurr.end(), Random::getRandom());
Result r = checkCurrent(aTermCurr, out, currModel);
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
// exclude the last active term
activeTerms.pop_back();
initializeChecker(queryChecker, qy, d_subOptions, logicInfo());
Result r = queryChecker->checkSat();
Trace("sygus-qgen-check") << "..finished check got " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
// if unsat, get the unsat core
std::vector<Node> unsatCore;
Trace("sygus-qgen-check") << "...unsat core: " << unsatCore << std::endl;
d_cores.add(d_false, unsatCore);
}
- else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ else if (r.getStatus() == Result::SAT)
{
getModelFromSubsolver(*queryChecker.get(), d_skolems, currModel);
Trace("sygus-qgen-check") << "...model: " << currModel << std::endl;
// check the satisfiability query
Result r = doCheck(imp);
Trace("sygus-sol-implied") << " implies: ...got : " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
// it is subsumed by the current, discard this
return false;
// check the satisfiability query
Result r = doCheck(imp);
Trace("sygus-sol-implied") << " implies: ...got : " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+ if (r.getStatus() != Result::UNSAT)
{
nsubsume.push_back(s);
}
siSmt->assertFormula(siq);
Result r = siSmt->checkSat();
Trace("sygus-si") << "Result: " << r << std::endl;
- Result::Sat res = r.asSatisfiabilityResult().isSat();
+ Result::Status res = r.getStatus();
if (res != Result::UNSAT)
{
warning() << "Warning : the single invocation solver determined the SyGuS "
std::vector<Node> mvs;
Result r = checkSat(fassert, mvs);
Trace("sygus-ccore-debug") << "...got " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+ if (r.getStatus() != Result::UNSAT)
{
// failed the filter, remember the refinement point
- if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ if (r.getStatus() == Result::SAT)
{
cfilter.addRefinementPt(fassert, mvs);
}
Result r = checkSol->checkSat();
Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl;
// In terms of Variant #2, this is the check "if (S ^ D) => B"
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
// it entails the postcondition, now get the unsat core
// In terms of Variant #2, this is the line
Result rsc = checkSc->checkSat();
Trace("sygus-ccore")
<< "----- check-sat returned " << rsc << std::endl;
- if (rsc.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (rsc.getStatus() == Result::UNSAT)
{
// In terms of Variant #2, this is the line
// "Let W be a subset of D such that S ^ W is unsat."
return constructSolutionFromPool(ccheck, asserts, passerts);
}
}
- else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ else if (r.getStatus() == Result::SAT)
{
// it does not entail the postcondition, add an assertion that blocks
// the current point
Result r = d_subSolver->checkSynth();
Trace("sygus-interpol") << " SygusInterpol::solveInterpolation result: " << r
<< std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
return findInterpol(d_subSolver.get(), interpol, d_itp);
}
Result r = d_subSolver->checkSynth(true);
Trace("sygus-interpol") << " SygusInterpol::solveInterpolationNext result: "
<< r << std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ if (r.getStatus() == Result::UNSAT)
{
return findInterpol(d_subSolver.get(), interpol, d_itp);
}
// check satisfiability
Result r = repcChecker->checkSat();
Trace("sygus-repair-const") << "...got : " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
- || r.asSatisfiabilityResult().isUnknown())
+ if (r.getStatus() == Result::UNSAT || r.isUnknown())
{
Trace("sygus-engine") << "...failed" << std::endl;
return false;
std::vector<Node> skModel;
Result r = d_verify.verify(query, d_innerSks, skModel);
- if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ if (r.getStatus() == Result::SAT)
{
// we have a counterexample
return processCounterexample(skModel);
}
- else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+ else if (r.getStatus() != Result::UNSAT)
{
// In the rare case that the subcall is unknown, we simply exclude the
// solution, without adding a counterexample point. This should only
query = rewrite(query);
Result r = checkWithSubsolver(query, vars, mvs, d_subOptions, d_subLogicInfo);
Trace("sygus-engine") << " ...got " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ if (r.getStatus() == Result::SAT)
{
if (TraceIsOn("sygus-engine"))
{
return Result(Result::SAT);
}
}
- return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
+ return Result(Result::UNKNOWN, Result::REQUIRES_FULL_CHECK);
}
void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
Result r = quickCheck(query);
if (!r.isUnknown())
{
- if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ if (r.getStatus() == Result::SAT)
{
// default model
NodeManager* nm = NodeManager::currentNM();
initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout);
smte->assertFormula(query);
r = smte->checkSat();
- if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ if (r.getStatus() == Result::SAT)
{
for (const Node& v : vars)
{
namespace cvc5 {
Result::Result()
- : d_sat(SAT_UNKNOWN),
- d_entailment(ENTAILMENT_UNKNOWN),
- d_which(TYPE_NONE),
- d_unknownExplanation(UNKNOWN_REASON),
- d_inputName("")
+ : d_status(NONE), d_unknownExplanation(UNKNOWN_REASON), d_inputName("")
{
}
-Result::Result(enum Sat s, std::string inputName)
- : d_sat(s),
- d_entailment(ENTAILMENT_UNKNOWN),
- d_which(TYPE_SAT),
- d_unknownExplanation(UNKNOWN_REASON),
- d_inputName(inputName)
+Result::Result(Status s, std::string inputName)
+ : d_status(s), d_unknownExplanation(UNKNOWN_REASON), d_inputName(inputName)
{
- PrettyCheckArgument(s != SAT_UNKNOWN,
+ PrettyCheckArgument(s != UNKNOWN,
"Must provide a reason for satisfiability being unknown");
}
-Result::Result(enum Entailment e, std::string inputName)
- : d_sat(SAT_UNKNOWN),
- d_entailment(e),
- d_which(TYPE_ENTAILMENT),
- d_unknownExplanation(UNKNOWN_REASON),
- 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(Status s,
+ UnknownExplanation unknownExplanation,
std::string inputName)
- : d_sat(s),
- d_entailment(ENTAILMENT_UNKNOWN),
- d_which(TYPE_SAT),
+ : d_status(s),
d_unknownExplanation(unknownExplanation),
d_inputName(inputName)
{
- PrettyCheckArgument(s == SAT_UNKNOWN,
- "improper use of unknown-result constructor");
-}
-
-Result::Result(enum Entailment e,
- enum UnknownExplanation unknownExplanation,
- std::string inputName)
- : d_sat(SAT_UNKNOWN),
- d_entailment(e),
- d_which(TYPE_ENTAILMENT),
- d_unknownExplanation(unknownExplanation),
- d_inputName(inputName)
-{
- PrettyCheckArgument(e == ENTAILMENT_UNKNOWN,
+ PrettyCheckArgument(s == UNKNOWN,
"improper use of unknown-result constructor");
}
Result::Result(const std::string& instr, std::string inputName)
- : d_sat(SAT_UNKNOWN),
- d_entailment(ENTAILMENT_UNKNOWN),
- d_which(TYPE_NONE),
+ : d_status(NONE),
d_unknownExplanation(UNKNOWN_REASON),
d_inputName(inputName)
{
- string s = instr;
+ std::string s = instr;
transform(s.begin(), s.end(), s.begin(), ::tolower);
- if (s == "sat" || s == "satisfiable") {
- d_which = TYPE_SAT;
- d_sat = SAT;
- } else if (s == "unsat" || s == "unsatisfiable") {
- d_which = TYPE_SAT;
- d_sat = UNSAT;
- }
- else if (s == "entailed")
+ if (s == "sat" || s == "satisfiable")
{
- d_which = TYPE_ENTAILMENT;
- d_entailment = ENTAILED;
+ d_status = SAT;
}
- else if (s == "not_entailed")
+ else if (s == "unsat" || s == "unsatisfiable")
{
- d_which = TYPE_ENTAILMENT;
- d_entailment = NOT_ENTAILED;
+ d_status = UNSAT;
}
else if (s == "incomplete")
{
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
+ d_status = UNKNOWN;
d_unknownExplanation = INCOMPLETE;
}
else if (s == "timeout")
{
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
+ d_status = UNKNOWN;
d_unknownExplanation = TIMEOUT;
}
else if (s == "resourceout")
{
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
+ d_status = UNKNOWN;
d_unknownExplanation = RESOURCEOUT;
}
else if (s == "memout")
{
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
+ d_status = UNKNOWN;
d_unknownExplanation = MEMOUT;
}
else if (s == "interrupted")
{
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
+ d_status = UNKNOWN;
d_unknownExplanation = INTERRUPTED;
}
else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0)
{
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
+ d_status = UNKNOWN;
}
else
{
}
}
-Result::UnknownExplanation Result::whyUnknown() const {
+Result::UnknownExplanation Result::getUnknownExplanation() const
+{
PrettyCheckArgument(isUnknown(), this,
"This result is not unknown, so the reason for "
"being unknown cannot be inquired of it");
}
bool Result::operator==(const Result& r) const {
- if (d_which != r.d_which) {
- return false;
- }
- if (d_which == TYPE_SAT) {
- return d_sat == r.d_sat && (d_sat != SAT_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::Entailment e, const Result& r) { return r == e; }
-bool operator!=(enum Result::Sat s, const Result& r) { return !(s == 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_ENTAILMENT)
- {
- switch (d_entailment)
- {
- case NOT_ENTAILED: return Result(SAT, d_inputName);
-
- case ENTAILED: return Result(UNSAT, d_inputName);
-
- case ENTAILMENT_UNKNOWN:
- return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
-
- default: Unhandled() << d_entailment;
- }
- }
-
- // TYPE_NONE
- return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
+ return d_status == r.d_status
+ && (d_status != UNKNOWN
+ || d_unknownExplanation == r.d_unknownExplanation);
}
-Result Result::asEntailmentResult() const
-{
- if (d_which == TYPE_ENTAILMENT)
- {
- return *this;
- }
-
- if (d_which == TYPE_SAT) {
- switch (d_sat) {
- case SAT: return Result(NOT_ENTAILED, d_inputName);
-
- case UNSAT: return Result(ENTAILED, d_inputName);
-
- case SAT_UNKNOWN:
- return Result(ENTAILMENT_UNKNOWN, d_unknownExplanation, d_inputName);
-
- default: Unhandled() << d_sat;
- }
- }
-
- // TYPE_NONE
- return Result(ENTAILMENT_UNKNOWN, NO_STATUS, d_inputName);
-}
+bool Result::operator!=(const Result& r) const { return !(*this == r); }
string Result::toString() const {
stringstream ss;
return ss.str();
}
-ostream& operator<<(ostream& out, enum Result::Sat s) {
+ostream& operator<<(ostream& out, enum Result::Status s)
+{
switch (s) {
+ case Result::NONE: out << "NONE"; break;
case Result::UNSAT:
out << "UNSAT";
break;
case Result::SAT:
out << "SAT";
break;
- case Result::SAT_UNKNOWN:
- out << "SAT_UNKNOWN";
- break;
+ case Result::UNKNOWN: out << "UNKNOWN"; break;
default: Unhandled() << s;
}
return out;
}
-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;
-}
-
ostream& operator<<(ostream& out, enum Result::UnknownExplanation e)
{
switch (e)
}
};
return out;
-} /* operator<<(ostream&, const Result&) */
+}
void Result::toStreamDefault(std::ostream& out) const {
- if (getType() == Result::TYPE_SAT) {
- switch (isSat()) {
- case Result::UNSAT:
- out << "unsat";
- break;
- case Result::SAT:
- out << "sat";
- break;
- case Result::SAT_UNKNOWN:
- out << "unknown";
- if (whyUnknown() != Result::UNKNOWN_REASON) {
- out << " (" << whyUnknown() << ")";
- }
- break;
- }
- } else {
- 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() << ")";
- }
- break;
- }
+ switch (d_status)
+ {
+ case Result::NONE: out << "none"; break;
+ case Result::UNSAT: out << "unsat"; break;
+ case Result::SAT: out << "sat"; break;
+ case Result::UNKNOWN:
+ out << "unknown";
+ if (getUnknownExplanation() != Result::UNKNOWN_REASON)
+ {
+ out << " (" << getUnknownExplanation() << ")";
+ }
+ break;
+ default: out << "???"; break;
}
-} /* Result::toStreamDefault() */
+}
void Result::toStreamSmt2(ostream& out) const {
- if (getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) {
+ if (d_status == Result::UNKNOWN)
+ {
+ // to avoid printing the reason
out << "unknown";
- } else {
- toStreamDefault(out);
+ return;
}
+ toStreamDefault(out);
}
void Result::toStreamTptp(std::ostream& out) const {
out << "% SZS status ";
- if (isSat() == Result::SAT) {
- out << "Satisfiable";
- } else if (isSat() == Result::UNSAT) {
- out << "Unsatisfiable";
- }
- else if (isEntailed() == Result::ENTAILED)
+ if (d_status == Result::SAT)
{
- out << "Theorem";
+ out << "Satisfiable";
}
- else if (isEntailed() == Result::NOT_ENTAILED)
+ else if (d_status == Result::UNSAT)
{
- out << "CounterSatisfiable";
+ out << "Unsatisfiable";
}
else
{
class Result
{
public:
- enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 };
-
- enum Entailment
- {
- NOT_ENTAILED = 0,
- ENTAILED = 1,
- ENTAILMENT_UNKNOWN = 2
- };
-
- enum Type
+ enum Status
{
- TYPE_SAT,
- TYPE_ENTAILMENT,
- TYPE_NONE
+ // the status has not been set
+ NONE,
+ // the status is "unsat"
+ UNSAT,
+ // the status is "sat"
+ SAT,
+ // the status is "unknown"
+ UNKNOWN
};
enum UnknownExplanation
UNKNOWN_REASON
};
- private:
- enum Sat d_sat;
- enum Entailment d_entailment;
- enum Type d_which;
- enum UnknownExplanation d_unknownExplanation;
- std::string d_inputName;
-
public:
Result();
- Result(enum Sat s, std::string inputName = "");
-
- Result(enum Entailment v, std::string inputName = "");
+ Result(Status s, std::string inputName = "");
- Result(enum Sat s, enum UnknownExplanation unknownExplanation,
- std::string inputName = "");
-
- Result(enum Entailment v,
+ Result(Status s,
enum UnknownExplanation unknownExplanation,
std::string inputName = "");
d_inputName = inputName;
}
- enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; }
-
- enum Entailment isEntailed() const
- {
- return d_which == TYPE_ENTAILMENT ? d_entailment : ENTAILMENT_UNKNOWN;
- }
-
- bool isUnknown() const {
- return isSat() == SAT_UNKNOWN && isEntailed() == ENTAILMENT_UNKNOWN;
- }
-
- Type getType() const { return d_which; }
+ Status getStatus() const { return d_status; }
- bool isNull() const { return d_which == TYPE_NONE; }
+ bool isNull() const { return d_status == NONE; }
+ bool isUnknown() const { return d_status == UNKNOWN; }
- enum UnknownExplanation whyUnknown() const;
+ UnknownExplanation getUnknownExplanation() const;
bool operator==(const Result& r) const;
- inline bool operator!=(const Result& r) const;
- Result asSatisfiabilityResult() const;
- Result asEntailmentResult() const;
+ bool operator!=(const Result& r) const;
std::string toString() const;
/**
* This is mostly the same the default
- * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN,
+ * If getType() == Result::TYPE_SAT && getStatus() == Result::UNKNOWN,
*
*/
void toStreamSmt2(std::ostream& out) const;
* has a particular preference for how results should appear.
*/
void toStreamDefault(std::ostream& out) const;
-}; /* class Result */
-inline bool Result::operator!=(const Result& r) const { return !(*this == r); }
+ private:
+ /** The result */
+ Status d_status;
+ /** The unknown explanation */
+ UnknownExplanation d_unknownExplanation;
+ /** The input name */
+ std::string d_inputName;
+}; /* class Result */
-std::ostream& operator<<(std::ostream& out, enum Result::Sat s);
-std::ostream& operator<<(std::ostream& out, enum Result::Entailment e);
+std::ostream& operator<<(std::ostream& out, enum Result::Status s);
std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e);
-bool operator==(enum Result::Sat s, const Result& r);
-bool operator==(enum Result::Entailment e, const Result& r);
-
-bool operator!=(enum Result::Sat s, const Result& r);
-bool operator!=(enum Result::Entailment e, const Result& r);
-
} // namespace cvc5
#endif /* CVC5__RESULT_H */
ASSERT_TRUE(res_null.isNull());
ASSERT_FALSE(res_null.isSat());
ASSERT_FALSE(res_null.isUnsat());
- ASSERT_FALSE(res_null.isSatUnknown());
+ ASSERT_FALSE(res_null.isUnknown());
Sort u_sort = d_solver.mkUninterpretedSort("u");
Term x = d_solver.mkConst(u_sort, "x");
d_solver.assertFormula(x.eqTerm(x));
d_solver.assertFormula(x.eqTerm(x));
cvc5::api::Result res = d_solver.checkSat();
ASSERT_TRUE(res.isSat());
- ASSERT_FALSE(res.isSatUnknown());
+ ASSERT_FALSE(res.isUnknown());
}
TEST_F(TestApiBlackResult, isUnsat)
d_solver.assertFormula(x.eqTerm(x).notTerm());
cvc5::api::Result res = d_solver.checkSat();
ASSERT_TRUE(res.isUnsat());
- ASSERT_FALSE(res.isSatUnknown());
+ ASSERT_FALSE(res.isUnknown());
}
-TEST_F(TestApiBlackResult, isSatUnknown)
+TEST_F(TestApiBlackResult, isUnknown)
{
d_solver.setLogic("QF_NIA");
d_solver.setOption("incremental", "false");
d_solver.assertFormula(x.eqTerm(x).notTerm());
cvc5::api::Result res = d_solver.checkSat();
ASSERT_FALSE(res.isSat());
- ASSERT_TRUE(res.isSatUnknown());
+ ASSERT_TRUE(res.isUnknown());
}
} // namespace test
assertTrue(res_null.isNull());
assertFalse(res_null.isSat());
assertFalse(res_null.isUnsat());
- assertFalse(res_null.isSatUnknown());
+ assertFalse(res_null.isUnknown());
Sort u_sort = d_solver.mkUninterpretedSort("u");
Term x = d_solver.mkConst(u_sort, "x");
d_solver.assertFormula(x.eqTerm(x));
d_solver.assertFormula(x.eqTerm(x));
Result res = d_solver.checkSat();
assertTrue(res.isSat());
- assertFalse(res.isSatUnknown());
+ assertFalse(res.isUnknown());
}
@Test void isUnsat()
d_solver.assertFormula(x.eqTerm(x).notTerm());
Result res = d_solver.checkSat();
assertTrue(res.isUnsat());
- assertFalse(res.isSatUnknown());
+ assertFalse(res.isUnknown());
}
- @Test void isSatUnknown() throws CVC5ApiException
- {
+ @Test
+ void isUnknown() throws CVC5ApiException {
d_solver.setLogic("QF_NIA");
d_solver.setOption("incremental", "false");
d_solver.setOption("solve-int-as-bv", "32");
d_solver.assertFormula(x.eqTerm(x).notTerm());
Result res = d_solver.checkSat();
assertFalse(res.isSat());
- assertTrue(res.isSatUnknown());
+ assertTrue(res.isUnknown());
}
}
assert res_null.isNull()
assert not res_null.isSat()
assert not res_null.isUnsat()
- assert not res_null.isSatUnknown()
+ assert not res_null.isUnknown()
u_sort = solver.mkUninterpretedSort("u")
x = solver.mkConst(u_sort, "x")
solver.assertFormula(x.eqTerm(x))
solver.assertFormula(x.eqTerm(x))
res = solver.checkSat()
assert res.isSat()
- assert not res.isSatUnknown()
+ assert not res.isUnknown()
def test_is_unsat(solver):
solver.assertFormula(x.eqTerm(x).notTerm())
res = solver.checkSat()
assert res.isUnsat()
- assert not res.isSatUnknown()
+ assert not res.isUnknown()
def test_is_sat_unknown(solver):
solver.assertFormula(x.eqTerm(x).notTerm())
res = solver.checkSat()
assert not res.isSat()
- assert res.isSatUnknown()
+ assert res.isUnknown()
Result r = d_optslv->checkOpt();
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
BitVector(32u, (uint32_t)0x3FFFFFA1));
Result r = d_optslv->checkOpt();
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>();
std::cout << "opt value is: " << val << std::endl;
Result r = d_optslv->checkOpt();
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>();
std::cout << "opt value is: " << val << std::endl;
Result r = d_optslv->checkOpt();
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
// expect the maxmum x =
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
Result r = d_optslv->checkOpt();
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
// expect the maximum x = 18
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
Node eq = d_nodeManager->mkNode(kind::DISTINCT, lhs, rhs);
d_slvEngine->assertFormula(eq);
Result res = d_slvEngine->checkSat();
- ASSERT_EQ(res.isSat(), Result::UNSAT);
+ ASSERT_EQ(res.getStatus(), Result::UNSAT);
d_slvEngine->pop();
}
}
Result r = d_optslv->checkOpt();
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
// We expect max_cost == 99
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
Result r = d_optslv->checkOpt();
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
// We expect max_cost == 99
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
Result r = d_optslv->checkOpt();
// We expect our check to have returned UNSAT
- ASSERT_EQ(r.isSat(), Result::UNSAT);
+ ASSERT_EQ(r.getStatus(), Result::UNSAT);
d_slvEngine->resetAssertions();
}
Result r = d_optslv->checkOpt();
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
// expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
// Box optimization
Result r = optSolver.checkOpt(OptimizationSolver::BOX);
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
std::vector<OptimizationResult> results = optSolver.getValues();
Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
std::vector<OptimizationResult> results = optSolver.getValues();
{1, 3}, {2, 2}, {3, 1}};
r = optSolver.checkOpt(OptimizationSolver::PARETO);
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
std::vector<OptimizationResult> results = optSolver.getValues();
std::pair<uint32_t, uint32_t> res = {
results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
possibleResults.erase(res);
r = optSolver.checkOpt(OptimizationSolver::PARETO);
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
results = optSolver.getValues();
res = {
results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
possibleResults.erase(res);
r = optSolver.checkOpt(OptimizationSolver::PARETO);
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
results = optSolver.getValues();
res = {
results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
possibleResults.erase(res);
r = optSolver.checkOpt(OptimizationSolver::PARETO);
- ASSERT_EQ(r.isSat(), Result::UNSAT);
+ ASSERT_EQ(r.getStatus(), Result::UNSAT);
ASSERT_EQ(possibleResults.size(), 0);
}
// Lexico optimization
Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
std::vector<OptimizationResult> results = optSolver.getValues();
// now we only have one objective: (minimize x)
r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
results = optSolver.getValues();
ASSERT_EQ(results.size(), 1);
ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
// resetting the assertions also resets the optimization objectives
d_slvEngine->resetAssertions();
r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
- ASSERT_EQ(r.isSat(), Result::SAT);
+ ASSERT_EQ(r.getStatus(), Result::SAT);
results = optSolver.getValues();
ASSERT_EQ(results.size(), 0);
}
Node scr = d_nodeManager->mkNode(EXISTS, d_bvarlist, body);
Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
Result res = d_slvEngine->checkSat(a);
- ASSERT_EQ(res.d_sat, Result::UNSAT);
+ ASSERT_EQ(res.getStatus(), Result::UNSAT);
}
void runTest(bool pol,
d_nodeManager->mkNode(EXISTS, d_bvarlist, pol ? body : body.notNode());
Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
Result res = d_slvEngine->checkSat(a);
- if (res.d_sat == Result::SAT)
+ if (res.getStatus() == Result::SAT)
{
std::cout << std::endl;
std::cout << "s " << d_slvEngine->getValue(d_s) << std::endl;
std::cout << "t " << d_slvEngine->getValue(d_t) << std::endl;
std::cout << "x " << d_slvEngine->getValue(d_x) << std::endl;
}
- ASSERT_EQ(res.d_sat, Result::UNSAT);
+ ASSERT_EQ(res.getStatus(), Result::UNSAT);
}
void runTestConcat(bool pol, Kind litk, unsigned idx)
d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode());
Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
Result res = d_slvEngine->checkSat(a);
- if (res.d_sat == Result::SAT)
+ if (res.getStatus() == Result::SAT)
{
std::cout << std::endl;
if (!s1.isNull())
std::cout << "t " << d_slvEngine->getValue(t) << std::endl;
std::cout << "x " << d_slvEngine->getValue(x) << std::endl;
}
- ASSERT_TRUE(res.d_sat == Result::UNSAT);
+ ASSERT_TRUE(res.getStatus() == Result::UNSAT);
}
void runTestSext(bool pol, Kind litk)
d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode());
Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
Result res = d_slvEngine->checkSat(a);
- if (res.d_sat == Result::SAT)
+ if (res.getStatus() == Result::SAT)
{
std::cout << std::endl;
std::cout << "t " << d_slvEngine->getValue(t) << std::endl;
std::cout << "x " << d_slvEngine->getValue(x) << std::endl;
}
- ASSERT_TRUE(res.d_sat == Result::UNSAT);
+ ASSERT_TRUE(res.getStatus() == Result::UNSAT);
}
Node d_s;
projects / cvc5.git / commitdiff