From c914f3eca82aaf51dd9a208574dab6aa3b000201 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 Mar 2022 20:27:20 -0500 Subject: [PATCH] Refactor result class (#8313) 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. --- src/api/cpp/cvc5.cpp | 15 +- src/api/cpp/cvc5.h | 2 +- src/api/java/io/github/cvc5/api/Result.java | 7 +- src/api/java/jni/result.cpp | 6 +- src/api/python/cvc5.pxd | 2 +- src/api/python/cvc5.pxi | 4 +- src/main/command_executor.cpp | 4 +- src/omt/bitvector_optimizer.cpp | 12 +- src/omt/integer_optimizer.cpp | 4 +- src/prop/prop_engine.cpp | 6 +- src/smt/abduction_solver.cpp | 4 +- src/smt/assertions.cpp | 2 +- src/smt/command.cpp | 2 +- src/smt/interpolation_solver.cpp | 2 +- src/smt/optimization_solver.cpp | 34 ++- src/smt/optimization_solver.h | 19 +- src/smt/quant_elim_solver.cpp | 4 +- src/smt/smt_mode.cpp | 2 +- src/smt/smt_solver.cpp | 12 +- src/smt/solver_engine.cpp | 42 ++- src/smt/solver_engine.h | 24 +- src/smt/solver_engine_state.cpp | 19 +- src/smt/sygus_solver.cpp | 6 +- src/theory/arith/attempt_solution_simplex.cpp | 6 +- src/theory/arith/attempt_solution_simplex.h | 4 +- src/theory/arith/dual_simplex.cpp | 11 +- src/theory/arith/dual_simplex.h | 4 +- src/theory/arith/fc_simplex.cpp | 17 +- src/theory/arith/fc_simplex.h | 4 +- src/theory/arith/nl/nonlinear_extension.cpp | 17 +- src/theory/arith/nl/nonlinear_extension.h | 4 +- src/theory/arith/simplex.h | 2 +- src/theory/arith/soi_simplex.cpp | 16 +- src/theory/arith/soi_simplex.h | 4 +- src/theory/arith/theory_arith_private.cpp | 22 +- src/theory/arith/theory_arith_private.h | 4 +- .../candidate_rewrite_database.cpp | 4 +- src/theory/quantifiers/query_generator.cpp | 3 +- .../query_generator_sample_sat.cpp | 2 +- .../quantifiers/query_generator_unsat.cpp | 6 +- src/theory/quantifiers/solution_filter.cpp | 4 +- .../sygus/ce_guided_single_inv.cpp | 2 +- .../sygus/cegis_core_connective.cpp | 10 +- .../quantifiers/sygus/sygus_interpol.cpp | 4 +- .../quantifiers/sygus/sygus_repair_const.cpp | 3 +- .../quantifiers/sygus/synth_conjecture.cpp | 4 +- src/theory/quantifiers/sygus/synth_verify.cpp | 2 +- src/theory/smt_engine_subsolver.cpp | 6 +- src/util/result.cpp | 253 ++++-------------- src/util/result.h | 81 ++---- test/unit/api/cpp/result_black.cpp | 10 +- test/unit/api/java/ResultTest.java | 12 +- test/unit/api/python/test_result.py | 8 +- test/unit/theory/theory_bv_opt_white.cpp | 10 +- test/unit/theory/theory_bv_white.cpp | 2 +- test/unit/theory/theory_int_opt_white.cpp | 8 +- .../theory/theory_opt_multigoal_white.cpp | 18 +- .../theory_quantifiers_bv_inverter_white.cpp | 14 +- 58 files changed, 315 insertions(+), 500 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index b6e4ef187..d92774743 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -920,25 +920,22 @@ Result::Result() : d_result(new cvc5::Result()) {} 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 @@ -953,7 +950,7 @@ 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; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 83187a1b0..5083bec38 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -222,7 +222,7 @@ class CVC5_EXPORT Result * 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. diff --git a/src/api/java/io/github/cvc5/api/Result.java b/src/api/java/io/github/cvc5/api/Result.java index 1657d4a13..d222de788 100644 --- a/src/api/java/io/github/cvc5/api/Result.java +++ b/src/api/java/io/github/cvc5/api/Result.java @@ -117,12 +117,11 @@ public class Result extends AbstractPointer * 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. diff --git a/src/api/java/jni/result.cpp b/src/api/java/jni/result.cpp index 98bdcc765..1825ca3ff 100644 --- a/src/api/java/jni/result.cpp +++ b/src/api/java/jni/result.cpp @@ -77,15 +77,15 @@ JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isUnsat(JNIEnv* env, /* * 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); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 7f0037d99..ed11921b8 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -142,7 +142,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": 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 + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index f90cd5fa2..46fd480cb 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -587,11 +587,11 @@ cdef class Result: """ return self.cr.isUnsat() - def isSatUnknown(self): + def isUnknown(self): """ :return: True if query was a :cpp:func:`Solver::checkSat() ` or :cpp:func:`Solver::checkSatAssuming() ` query and cvc5 was not able to determine (un)satisfiability. """ - return self.cr.isSatUnknown() + return self.cr.isUnknown() def getUnknownExplanation(self): """ diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index efd092c5b..a3f3b6d73 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -141,7 +141,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) std::vector > getterCommands; if (d_solver->getOptionInfo("dump-models").boolValue() && (isResultSat - || (res.isSatUnknown() + || (res.isUnknown() && res.getUnknownExplanation() == api::Result::INCOMPLETE))) { getterCommands.emplace_back(new GetModelCommand()); @@ -165,7 +165,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) } if (d_solver->getOptionInfo("dump-difficulty").boolValue() - && (isResultUnsat || isResultSat || res.isSatUnknown())) + && (isResultUnsat || isResultSat || res.isUnknown())) { getterCommands.emplace_back(new GetDifficultyCommand()); } diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index 6e202cb70..a282429c1 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -54,7 +54,7 @@ OptimizationResult OMTOptimizerBitVector::minimize(SolverEngine* optChecker, // 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); } @@ -102,9 +102,9 @@ OptimizationResult OMTOptimizerBitVector::minimize(SolverEngine* optChecker, 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: @@ -143,7 +143,7 @@ OptimizationResult OMTOptimizerBitVector::maximize(SolverEngine* optChecker, // 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); } @@ -188,9 +188,9 @@ OptimizationResult OMTOptimizerBitVector::maximize(SolverEngine* optChecker, 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: diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp index caa29fcea..6ee6f9aa8 100644 --- a/src/omt/integer_optimizer.cpp +++ b/src/omt/integer_optimizer.cpp @@ -34,7 +34,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SolverEngine* optChecker, // 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); } @@ -58,7 +58,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SolverEngine* optChecker, // 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); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 4c099ad0f..b2c777e88 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -354,7 +354,7 @@ Result PropEngine::checkSat() { 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 @@ -387,7 +387,7 @@ Result PropEngine::checkSat() { { why = Result::RESOURCEOUT; } - return Result(Result::SAT_UNKNOWN, why); + return Result(Result::UNKNOWN, why); } if( result == SAT_VALUE_TRUE && TraceIsOn("prop") ) { @@ -397,7 +397,7 @@ Result PropEngine::checkSat() { 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); } diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 3e5912837..63030880d 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -181,7 +181,7 @@ void AbductionSolver::checkAbduct(Node a) bool isError = false; if (j == 0) { - if (r.asSatisfiabilityResult().isSat() != Result::SAT) + if (r.getStatus() != Result::SAT) { isError = true; serr @@ -197,7 +197,7 @@ void AbductionSolver::checkAbduct(Node a) } else { - if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + if (r.getStatus() != Result::UNSAT) { isError = true; serr << "SolverEngine::checkAbduct(): negated goal cannot be shown " diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 3d7cb0601..549b78a19 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -77,7 +77,7 @@ void Assertions::initializeCheckSat(const std::vector& assumptions) /* 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. diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 59e79c28c..4222ef4a6 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1839,7 +1839,7 @@ bool GetInstantiationsCommand::isEnabled(api::Solver* solver, const api::Result& res) { return (res.isSat() - || (res.isSatUnknown() + || (res.isUnknown() && res.getUnknownExplanation() == api::Result::INCOMPLETE)) || res.isUnsat(); } diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 97d3a4224..2f45c611e 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -119,7 +119,7 @@ void InterpolationSolver::checkInterpol(Node interpol, 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) { diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 77157625a..382c0e9b8 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -42,10 +42,10 @@ std::ostream& operator<<(std::ostream& out, const OptimizationResult& result) << "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()) { @@ -169,7 +169,7 @@ Result OptimizationSolver::optimizeBox() // resets the optChecker d_optChecker = createOptCheckerWithTimeout(d_parent); OptimizationResult partialResult; - Result aggregatedResult(Result::Sat::SAT); + Result aggregatedResult(Result::SAT); std::unique_ptr optimizer; for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { @@ -191,7 +191,7 @@ Result OptimizationSolver::optimizeBox() } // 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: @@ -202,9 +202,7 @@ Result OptimizationSolver::optimizeBox() } d_optChecker.reset(); return partialResult.getResult(); - case Result::SAT_UNKNOWN: - aggregatedResult = partialResult.getResult(); - break; + case Result::UNKNOWN: aggregatedResult = partialResult.getResult(); break; default: Unreachable(); } @@ -249,7 +247,7 @@ Result OptimizationSolver::optimizeLexicographicIterative() 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 @@ -259,7 +257,7 @@ Result OptimizationSolver::optimizeLexicographicIterative() case Result::UNSAT: d_optChecker.reset(); return partialResult.getResult(); - case Result::SAT_UNKNOWN: + case Result::UNKNOWN: d_optChecker.reset(); return partialResult.getResult(); default: Unreachable(); @@ -287,11 +285,11 @@ Result OptimizationSolver::optimizeParetoNaiveGIA() // 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 @@ -315,7 +313,7 @@ Result OptimizationSolver::optimizeParetoNaiveGIA() std::vector someObjBetter; d_optChecker->push(); - while (satResult.isSat() == Result::Sat::SAT) + while (satResult.getStatus() == Result::SAT) { noWorseObj.clear(); someObjBetter.clear(); @@ -342,18 +340,18 @@ Result OptimizationSolver::optimizeParetoNaiveGIA() // 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 diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 044500c14..f919bad19 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -64,8 +64,7 @@ class OptimizationResult { } OptimizationResult() - : d_result(Result::Sat::SAT_UNKNOWN, - Result::UnknownExplanation::NO_STATUS), + : d_result(Result::UNKNOWN, Result::UnknownExplanation::NO_STATUS), d_value(), d_infinity(FINITE) { @@ -75,7 +74,7 @@ class OptimizationResult /** * 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; } @@ -84,7 +83,7 @@ class OptimizationResult * @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; } @@ -271,8 +270,8 @@ class OptimizationSolver /** * 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(); @@ -284,10 +283,10 @@ class OptimizationSolver * 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(); @@ -305,8 +304,8 @@ class OptimizationSolver * * @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(); diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 8d41be049..8d198d69b 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -75,9 +75,9 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, Result r = d_smtSolver.checkSatisfiability(as, std::vector{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 : " diff --git a/src/smt/smt_mode.cpp b/src/smt/smt_mode.cpp index 37d1d5950..b971e14ac 100644 --- a/src/smt/smt_mode.cpp +++ b/src/smt/smt_mode.cpp @@ -26,7 +26,7 @@ std::ostream& operator<<(std::ostream& out, SmtMode m) 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; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 8876692b7..f65e07d9e 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -136,7 +136,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as, { Result::UnknownExplanation why = rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; - result = Result(Result::ENTAILMENT_UNKNOWN, why); + result = Result(Result::UNKNOWN, why); } else { @@ -161,20 +161,20 @@ Result SmtSolver::checkSatisfiability(Assertions& as, 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 @@ -188,7 +188,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as, } else { - result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + result = Result(Result::UNKNOWN, Result::UNKNOWN_REASON); } } Trace("smt") << "SmtSolver::global negate returned " << result diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 7cefea507..78e0a40b3 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -417,7 +417,7 @@ std::string SolverEngine::getInfo(const std::string& key) const { // 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"; @@ -434,7 +434,7 @@ std::string SolverEngine::getInfo(const std::string& key) const 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; @@ -634,15 +634,6 @@ void SolverEngine::defineFunctionRec(Node func, 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) @@ -772,7 +763,7 @@ Result SolverEngine::checkSatInternal(const std::vector& assumptions) // 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(); } @@ -780,7 +771,7 @@ Result SolverEngine::checkSatInternal(const std::vector& assumptions) // 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(); } @@ -788,7 +779,7 @@ Result SolverEngine::checkSatInternal(const std::vector& assumptions) // 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(); @@ -832,16 +823,16 @@ std::vector SolverEngine::getUnsatAssumptions(void) 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. @@ -851,7 +842,6 @@ Result SolverEngine::assertFormulaInternal(const Node& formula) Node n = d_absValues->substituteAbstractValues(formula); d_asserts->assertFormula(n); - return quickCheck().asEntailmentResult(); } /* @@ -1097,7 +1087,7 @@ std::string SolverEngine::getModel(const std::vector& declaredSorts, return ssm.str(); } -Result SolverEngine::blockModel() +void SolverEngine::blockModel() { Trace("smt") << "SMT blockModel()" << endl; SolverEngineScope smts(this); @@ -1119,10 +1109,10 @@ Result SolverEngine::blockModel() 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& exprs) +void SolverEngine::blockModelValues(const std::vector& exprs) { Trace("smt") << "SMT blockModelValues()" << endl; SolverEngineScope smts(this); @@ -1142,7 +1132,7 @@ Result SolverEngine::blockModelValues(const std::vector& exprs) ModelBlocker mb(*d_env.get()); Node eblocker = mb.getModelBlocker( eassertsProc, m, options::BlockModelsMode::VALUES, exprs); - return assertFormulaInternal(eblocker); + assertFormulaInternal(eblocker); } std::pair SolverEngine::getSepHeapAndNilExpr(void) @@ -1360,11 +1350,11 @@ std::vector SolverEngine::reduceUnsatCore(const std::vector& core) 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 " @@ -1438,13 +1428,13 @@ void SolverEngine::checkUnsatCore() } 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."; diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 824f67dbd..1b186c247 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -229,10 +229,8 @@ class CVC5_EXPORT SolverEngine * * 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. @@ -243,10 +241,8 @@ class CVC5_EXPORT SolverEngine * 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& exprs); + void blockModelValues(const std::vector& exprs); /** * Declare heap. For smt2 inputs, this is called when the command @@ -336,13 +332,12 @@ class CVC5_EXPORT SolverEngine /** * 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. @@ -351,7 +346,7 @@ class CVC5_EXPORT SolverEngine /** * 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 */ @@ -898,7 +893,7 @@ class CVC5_EXPORT SolverEngine 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, @@ -938,13 +933,6 @@ class CVC5_EXPORT SolverEngine */ 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. diff --git a/src/smt/solver_engine_state.cpp b/src/smt/solver_engine_state.cpp index 4ec577b68..3cab423ab 100644 --- a/src/smt/solver_engine_state.cpp +++ b/src/smt/solver_engine_state.cpp @@ -45,6 +45,7 @@ void SolverEngineState::notifyExpectedStatus(const std::string& status) << "SolverEngineState::notifyExpectedStatus: unexpected status string " << status; d_expectedStatus = Result(status, options().driver.filename); + Assert(d_expectedStatus.getStatus() != Result::NONE); } void SolverEngineState::notifyResetAssertions() @@ -95,17 +96,21 @@ void SolverEngineState::notifyCheckSatResult(bool hasAssumptions, Result r) // 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; @@ -115,7 +120,7 @@ void SolverEngineState::notifyCheckSatResult(bool hasAssumptions, Result r) 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; diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index e3844ab46..9ffdfc438 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -300,7 +300,7 @@ Result SygusSolver::checkSynth(Assertions& as, bool isNext) else { // otherwise, we return "unknown" - r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + r = Result(Result::UNKNOWN, Result::UNKNOWN_REASON); } return r; } @@ -400,13 +400,13 @@ void SygusSolver::checkSynthSolution(Assertions& as, 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 " diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 2ff166cbf..8d7ad5e74 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -54,7 +54,9 @@ bool AttemptSolutionSDP::matchesNewValue(const DenseMap& nv, Arit 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& newValues = sol.newValues; @@ -141,7 +143,7 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol) return Result::SAT; }else{ d_errorSet.reduceToSignals(); - return Result::SAT_UNKNOWN; + return Result::UNKNOWN; } } diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index 2bf4948a4..a68b7d536 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -71,9 +71,9 @@ public: 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& nv, ArithVar v) const; diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 1f98044eb..ea870fac7 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -58,7 +58,8 @@ DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots) { } -Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ +Result::Status DualSimplexDecisionProcedure::dualFindModel(bool exactResult) +{ Assert(d_conflictVariables.empty()); d_pivots = 0; @@ -85,12 +86,13 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ 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; @@ -126,7 +128,8 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ } Assert(!d_errorSet.moreSignals()); - if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){ + if (result == Result::UNKNOWN && d_errorSet.errorEmpty()) + { result = Result::SAT; } diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index 930b884ac..a7a2aa793 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -70,7 +70,7 @@ public: RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - Result::Sat findModel(bool exactResult) override + Result::Status findModel(bool exactResult) override { return dualFindModel(exactResult); } @@ -83,7 +83,7 @@ private: */ DenseMultiset d_pivotsInRound; - Result::Sat dualFindModel(bool exactResult); + Result::Status dualFindModel(bool exactResult); /** * This is the main simplex for DPLL(T) loop. diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 6042d4484..940a82fb3 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -67,7 +67,8 @@ FCSimplexDecisionProcedure::Statistics::Statistics(const std::string& name, { } -Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ +Result::Status FCSimplexDecisionProcedure::findModel(bool exactResult) +{ Assert(d_conflictVariables.empty()); Assert(d_sgnDisagreements.empty()); @@ -103,9 +104,10 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ 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{ @@ -124,7 +126,8 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ } Assert(!d_errorSet.moreSignals()); - if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){ + if (result == Result::UNKNOWN && d_errorSet.errorEmpty()) + { result = Result::SAT; } @@ -658,8 +661,8 @@ bool FCSimplexDecisionProcedure::debugDualLike(WitnessImprovement w, return false; } -Result::Sat FCSimplexDecisionProcedure::dualLike(){ - +Result::Status FCSimplexDecisionProcedure::dualLike() +{ TimerStat::CodeTimer codeTimer(d_statistics.d_fcTimer); Assert(d_sgnDisagreements.empty()); @@ -752,7 +755,7 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ return Result::SAT; }else{ Assert(d_pivotBudget == 0); - return Result::SAT_UNKNOWN; + return Result::UNKNOWN; } } diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index f3dbccc6e..9cba57b2d 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -74,7 +74,7 @@ public: 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); @@ -83,7 +83,7 @@ public: // dual like // - found conflict // - satisfied error set - Result::Sat dualLike(); + Result::Status dualLike(); private: static constexpr uint32_t PENALTY = 4; diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index bcece4e4d..6a554272d 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -288,8 +288,8 @@ void NonlinearExtension::checkFullEffort(std::map& arithModel, 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 @@ -301,7 +301,8 @@ void NonlinearExtension::checkFullEffort(std::map& arithModel, d_trSlv.postProcessModel(arithModel, termSet); } -Result::Sat NonlinearExtension::modelBasedRefinement(const std::set& termSet) +Result::Status NonlinearExtension::modelBasedRefinement( + const std::set& termSet) { ++(d_stats.d_mbrRuns); d_checkCounter++; @@ -364,7 +365,7 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set& termS 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 @@ -385,7 +386,7 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set& termS if (d_im.hasUsed()) { d_im.clearWaitingLemmas(); - return Result::Sat::UNSAT; + return Result::UNSAT; } } @@ -399,7 +400,7 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set& termS d_im.flushWaitingLemmas(); Trace("nl-ext") << "...added " << count << " waiting lemmas." << std::endl; - return Result::Sat::UNSAT; + return Result::UNSAT; } // we are incomplete @@ -419,14 +420,14 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set& termS "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, diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 0080f8948..337f26cb2 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -128,11 +128,11 @@ class NonlinearExtension : EnvObj * 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& termSet); + Result::Status modelBasedRefinement(const std::set& termSet); /** get assertions * diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index f2fa8b6a6..172b080ad 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -168,7 +168,7 @@ public: * * 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++; } diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 2f3c2ac83..bdef50f8d 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -73,7 +73,8 @@ SumOfInfeasibilitiesSPD::Statistics::Statistics(const std::string& name, { } -Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ +Result::Status SumOfInfeasibilitiesSPD::findModel(bool exactResult) +{ Assert(d_conflictVariables.empty()); Assert(d_sgnDisagreements.empty()); @@ -110,9 +111,10 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ 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{ @@ -131,7 +133,8 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ } Assert(!d_errorSet.moreSignals()); - if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){ + if (result == Result::UNKNOWN && d_errorSet.errorEmpty()) + { result = Result::SAT; } @@ -857,7 +860,8 @@ WitnessImprovement SumOfInfeasibilitiesSPD::soiRound() { } } -Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ +Result::Status SumOfInfeasibilitiesSPD::sumOfInfeasibilities() +{ TimerStat::CodeTimer codeTimer(d_statistics.d_soiTimer); Assert(d_sgnDisagreements.empty()); @@ -899,7 +903,7 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ return Result::SAT; }else{ Assert(d_pivotBudget == 0); - return Result::SAT_UNKNOWN; + return Result::UNKNOWN; } } diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 96e1de531..c0962c87c 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -73,7 +73,7 @@ public: 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); @@ -86,7 +86,7 @@ private: // dual like // - found conflict // - satisfied error set - Result::Sat sumOfInfeasibilities(); + Result::Status sumOfInfeasibilities(); int32_t d_pivotBudget; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 13d169040..1fd44f136 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -102,7 +102,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, 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()), @@ -166,7 +166,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_solveIntMaybeHelp(0u), d_solveIntAttempts(0u), d_newFacts(false), - d_previousStatus(Result::SAT_UNKNOWN), + d_previousStatus(Result::UNKNOWN), d_statistics(statisticsRegistry(), "theory::arith::") { } @@ -1915,7 +1915,7 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){ } /* 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()); @@ -2884,12 +2884,12 @@ bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel) { // 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) @@ -2938,7 +2938,8 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ 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()); @@ -3060,7 +3061,7 @@ bool TheoryArithPrivate::preCheck(Theory::Effort level) d_previousStatus = d_qflraStatus; if (d_newFacts) { - d_qflraStatus = Result::SAT_UNKNOWN; + d_qflraStatus = Result::UNKNOWN; d_hasDoneWorkSinceCut = true; } return false; @@ -3181,7 +3182,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } } break; - case Result::SAT_UNKNOWN: + case Result::UNKNOWN: ++d_unknownsInARow; ++(d_statistics.d_unknownChecks); Assert(!Theory::fullEffort(effortLevel)); @@ -3737,7 +3738,7 @@ void TheoryArithPrivate::propagate(Theory::Effort e) { 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)) { @@ -4032,7 +4033,8 @@ void TheoryArithPrivate::presolve(){ } EqualityStatus TheoryArithPrivate::getEqualityStatus(TNode a, TNode b) { - if(d_qflraStatus == Result::SAT_UNKNOWN){ + if (d_qflraStatus == Result::UNKNOWN) + { return EQUALITY_UNKNOWN; }else{ try { diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index c10a4ad84..43b073460 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -111,7 +111,7 @@ class TheoryArithPrivate : protected EnvObj */ 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 @@ -773,7 +773,7 @@ private: /** 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. */ diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 8d8e2fcb9..452fb35cb 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -147,7 +147,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol, 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(); @@ -191,7 +191,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol, } else { - verified = !r.asSatisfiabilityResult().isUnknown(); + verified = !r.isUnknown(); } } else diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 535142227..8805fcf96 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -51,8 +51,7 @@ void QueryGenerator::dumpQuery(Node qy, const Result& r) 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; } diff --git a/src/theory/quantifiers/query_generator_sample_sat.cpp b/src/theory/quantifiers/query_generator_sample_sat.cpp index e259a875f..61873f45b 100644 --- a/src/theory/quantifiers/query_generator_sample_sat.cpp +++ b/src/theory/quantifiers/query_generator_sample_sat.cpp @@ -169,7 +169,7 @@ void QueryGeneratorSampleSat::checkQuery(Node qy, 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 diff --git a/src/theory/quantifiers/query_generator_unsat.cpp b/src/theory/quantifiers/query_generator_unsat.cpp index 90ac3bcd9..ae23d3ae6 100644 --- a/src/theory/quantifiers/query_generator_unsat.cpp +++ b/src/theory/quantifiers/query_generator_unsat.cpp @@ -70,7 +70,7 @@ bool QueryGeneratorUnsat::addTerm(Node n, std::ostream& out) std::vector 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(); @@ -131,7 +131,7 @@ Result QueryGeneratorUnsat::checkCurrent(const std::vector& activeTerms, 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 unsatCore; @@ -140,7 +140,7 @@ Result QueryGeneratorUnsat::checkCurrent(const std::vector& activeTerms, 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; diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index 364a3c812..f2489f143 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -72,7 +72,7 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) // 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; @@ -91,7 +91,7 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) // 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); } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 7eff21314..6ecdb5c6f 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -236,7 +236,7 @@ bool CegSingleInv::solve() 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 " diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index c0b87a406..cae7190a2 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -309,10 +309,10 @@ bool CegisCoreConnective::constructSolution( std::vector 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); } @@ -683,7 +683,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, 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 @@ -723,7 +723,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, 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." @@ -770,7 +770,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, 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 diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index eb9bed3dc..4787b65db 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -349,7 +349,7 @@ bool SygusInterpol::solveInterpolation(const std::string& name, 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); } @@ -364,7 +364,7 @@ bool SygusInterpol::solveInterpolationNext(Node& interpol) 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); } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 9059fe8d0..a7df0bb51 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -243,8 +243,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, // 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; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index bb671bb02..84eb54499 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -560,12 +560,12 @@ bool SynthConjecture::doCheck() std::vector 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 diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp index c01df10a6..a1470c305 100644 --- a/src/theory/quantifiers/sygus/synth_verify.cpp +++ b/src/theory/quantifiers/sygus/synth_verify.cpp @@ -112,7 +112,7 @@ Result SynthVerify::verify(Node query, 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")) { diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index c41f7895e..425808911 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -38,7 +38,7 @@ Result quickCheck(Node& query) 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& smte, @@ -111,7 +111,7 @@ Result checkWithSubsolver(Node query, Result r = quickCheck(query); if (!r.isUnknown()) { - if (r.asSatisfiabilityResult().isSat() == Result::SAT) + if (r.getStatus() == Result::SAT) { // default model NodeManager* nm = NodeManager::currentNM(); @@ -126,7 +126,7 @@ Result checkWithSubsolver(Node query, 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) { diff --git a/src/util/result.cpp b/src/util/result.cpp index 20c0beae5..22cce81e7 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -28,122 +28,71 @@ using namespace std; 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 { @@ -154,7 +103,8 @@ Result::Result(const std::string& instr, std::string inputName) } } -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"); @@ -162,78 +112,12 @@ Result::UnknownExplanation Result::whyUnknown() const { } 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; @@ -241,34 +125,22 @@ string Result::toString() const { 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) @@ -304,61 +176,44 @@ ostream& operator<<(ostream& out, const Result& r) { } }; 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 { diff --git a/src/util/result.h b/src/util/result.h index 9bdc99319..949d10e93 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -35,20 +35,16 @@ std::ostream& operator<<(std::ostream& out, const Result& r); 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 @@ -65,24 +61,12 @@ class Result 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 = ""); @@ -93,27 +77,15 @@ class Result 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; @@ -121,7 +93,7 @@ class Result /** * 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; @@ -140,20 +112,19 @@ class Result * 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 */ diff --git a/test/unit/api/cpp/result_black.cpp b/test/unit/api/cpp/result_black.cpp index 9606a2540..b291a88cc 100644 --- a/test/unit/api/cpp/result_black.cpp +++ b/test/unit/api/cpp/result_black.cpp @@ -31,7 +31,7 @@ TEST_F(TestApiBlackResult, isNull) 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)); @@ -59,7 +59,7 @@ TEST_F(TestApiBlackResult, isSat) 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) @@ -69,10 +69,10 @@ 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"); @@ -82,7 +82,7 @@ TEST_F(TestApiBlackResult, isSatUnknown) 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 diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java index 5f149dd8a..f21d5e8f0 100644 --- a/test/unit/api/java/ResultTest.java +++ b/test/unit/api/java/ResultTest.java @@ -42,7 +42,7 @@ class ResultTest 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)); @@ -70,7 +70,7 @@ class ResultTest d_solver.assertFormula(x.eqTerm(x)); Result res = d_solver.checkSat(); assertTrue(res.isSat()); - assertFalse(res.isSatUnknown()); + assertFalse(res.isUnknown()); } @Test void isUnsat() @@ -80,11 +80,11 @@ class ResultTest 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"); @@ -93,6 +93,6 @@ class ResultTest d_solver.assertFormula(x.eqTerm(x).notTerm()); Result res = d_solver.checkSat(); assertFalse(res.isSat()); - assertTrue(res.isSatUnknown()); + assertTrue(res.isUnknown()); } } diff --git a/test/unit/api/python/test_result.py b/test/unit/api/python/test_result.py index 86f2ab8a7..72e4ba314 100644 --- a/test/unit/api/python/test_result.py +++ b/test/unit/api/python/test_result.py @@ -31,7 +31,7 @@ def test_is_null(solver): 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)) @@ -56,7 +56,7 @@ def test_is_sat(solver): solver.assertFormula(x.eqTerm(x)) res = solver.checkSat() assert res.isSat() - assert not res.isSatUnknown() + assert not res.isUnknown() def test_is_unsat(solver): @@ -65,7 +65,7 @@ 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): @@ -77,4 +77,4 @@ 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() diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index b03a7345c..ae9880ad9 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -59,7 +59,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) 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(32u, (uint32_t)0x3FFFFFA1)); @@ -80,7 +80,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) 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(); std::cout << "opt value is: " << val << std::endl; @@ -107,7 +107,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) 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(); std::cout << "opt value is: " << val << std::endl; @@ -132,7 +132,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max) 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(), @@ -156,7 +156,7 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) 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(), diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 847ca9415..5429dddc0 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -57,7 +57,7 @@ TEST_F(TestTheoryWhiteBv, mkUmulo) 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(); } } diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index 329e4d569..07b982b9a 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -64,7 +64,7 @@ TEST_F(TestTheoryWhiteIntOpt, max) 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(), @@ -95,7 +95,7 @@ TEST_F(TestTheoryWhiteIntOpt, min) 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(), @@ -128,7 +128,7 @@ TEST_F(TestTheoryWhiteIntOpt, result) 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(); } @@ -159,7 +159,7 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) 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(), diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp index 91a058efd..5d344620d 100644 --- a/test/unit/theory/theory_opt_multigoal_white.cpp +++ b/test/unit/theory/theory_opt_multigoal_white.cpp @@ -66,7 +66,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, box) // Box optimization Result r = optSolver.checkOpt(OptimizationSolver::BOX); - ASSERT_EQ(r.isSat(), Result::SAT); + ASSERT_EQ(r.getStatus(), Result::SAT); std::vector results = optSolver.getValues(); @@ -107,7 +107,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex) Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); - ASSERT_EQ(r.isSat(), Result::SAT); + ASSERT_EQ(r.getStatus(), Result::SAT); std::vector results = optSolver.getValues(); @@ -186,7 +186,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) {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 results = optSolver.getValues(); std::pair res = { results[0].getValue().getConst().toInteger().toUnsignedInt(), @@ -201,7 +201,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) 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().toInteger().toUnsignedInt(), @@ -216,7 +216,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) 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().toInteger().toUnsignedInt(), @@ -231,7 +231,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) 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); } @@ -265,7 +265,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) // Lexico optimization Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); - ASSERT_EQ(r.isSat(), Result::SAT); + ASSERT_EQ(r.getStatus(), Result::SAT); std::vector results = optSolver.getValues(); @@ -284,7 +284,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) // 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(32u, 18u)); @@ -292,7 +292,7 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) // 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); } diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index cfdced65d..9ee5a2644 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -89,7 +89,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit 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, @@ -118,14 +118,14 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit 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) @@ -174,7 +174,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit 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()) @@ -184,7 +184,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit 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) @@ -214,13 +214,13 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit 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; -- 2.30.2