From b0dcd82a9e235ffcce6a8f261cecb83a3dcf90e1 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 15 Jan 2020 08:25:21 -0800 Subject: [PATCH] New C++ API: Add nullary constructor for Result. (#3603) --- src/api/cvc4cpp.cpp | 7 ++ src/api/cvc4cpp.h | 9 +++ src/smt/smt_engine.cpp | 14 ++-- test/unit/api/CMakeLists.txt | 1 + test/unit/api/result_black.h | 136 +++++++++++++++++++++++++++++++++++ 5 files changed, 161 insertions(+), 6 deletions(-) create mode 100644 test/unit/api/result_black.h diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index f7ffe850a..ddc1a61a0 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -706,6 +706,13 @@ class CVC4ApiExceptionStream Result::Result(const CVC4::Result& r) : d_result(new CVC4::Result(r)) {} +Result::Result() : d_result(new CVC4::Result()) {} + +bool Result::isNull() const +{ + return d_result->getType() == CVC4::Result::TYPE_NONE; +} + bool Result::isSat(void) const { return d_result->getType() == CVC4::Result::TYPE_SAT diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index e05c228bc..396c4eedb 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -82,6 +82,15 @@ class CVC4_PUBLIC Result */ Result(const CVC4::Result& r); + /** Constructor. */ + Result(); + + /** + * Return true if Result is empty, i.e., a nullary Result, and not an actual + * result returned from a checkSat() (and friends) query. + */ + bool isNull() const; + /** * Return true if query was a satisfiable checkSat() or checkSatAssuming() * query. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3343abc29..910855505 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3678,15 +3678,17 @@ Result SmtEngine::checkSat(const vector& assumptions, bool inUnsatCore) Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) { - return checkSatisfiability( - assumption.isNull() ? std::vector() : std::vector{assumption}, - inUnsatCore, - true); + return checkSatisfiability(assumption.isNull() + ? std::vector() + : std::vector{assumption}, + inUnsatCore, + true) + .asValidityResult(); } Result SmtEngine::query(const vector& assumptions, bool inUnsatCore) { - return checkSatisfiability(assumptions, inUnsatCore, true); + return checkSatisfiability(assumptions, inUnsatCore, true).asValidityResult(); } Result SmtEngine::checkSatisfiability(const Expr& expr, @@ -3771,7 +3773,7 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, d_private->addFormula(e.getNode(), inUnsatCore, true, true); } - r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult(); + r = check(); if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) && r.asSatisfiabilityResult().isSat() == Result::UNSAT) diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 7566c432d..fc1461862 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -3,6 +3,7 @@ cvc4_add_unit_test_black(datatype_api_black api) cvc4_add_unit_test_black(op_black api) +cvc4_add_unit_test_black(result_black api) cvc4_add_unit_test_black(solver_black api) cvc4_add_unit_test_black(sort_black api) cvc4_add_unit_test_black(term_black api) diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h new file mode 100644 index 000000000..ab5d65e72 --- /dev/null +++ b/test/unit/api/result_black.h @@ -0,0 +1,136 @@ +/********************* */ +/*! \file result_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the Result class + **/ + +#include + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class ResultBlack : public CxxTest::TestSuite +{ + public: + void setUp() { d_solver.reset(new Solver()); } + void tearDown() override {} + + void testIsNull(); + void testEq(); + void testIsSat(); + void testIsUnsat(); + void testIsSatUnknown(); + void testIsValid(); + void testIsInvalid(); + void testIsValidUnknown(); + + private: + std::unique_ptr d_solver; +}; + +void ResultBlack::testIsNull() +{ + Result res_null; + TS_ASSERT(res_null.isNull()); + TS_ASSERT(!res_null.isSat()); + TS_ASSERT(!res_null.isUnsat()); + TS_ASSERT(!res_null.isSatUnknown()); + TS_ASSERT(!res_null.isValid()); + TS_ASSERT(!res_null.isInvalid()); + TS_ASSERT(!res_null.isValidUnknown()); + Sort u_sort = d_solver->mkUninterpretedSort("u"); + Term x = d_solver->mkVar(u_sort, "x"); + d_solver->assertFormula(x.eqTerm(x)); + Result res = d_solver->checkSat(); + TS_ASSERT(!res.isNull()); +} + +void ResultBlack::testEq() +{ + Sort u_sort = d_solver->mkUninterpretedSort("u"); + Term x = d_solver->mkVar(u_sort, "x"); + d_solver->assertFormula(x.eqTerm(x)); + Result res; + Result res2 = d_solver->checkSat(); + Result res3 = d_solver->checkSat(); + res = res2; + TS_ASSERT_EQUALS(res, res2); + TS_ASSERT_EQUALS(res3, res2); +} + +void ResultBlack::testIsSat() +{ + Sort u_sort = d_solver->mkUninterpretedSort("u"); + Term x = d_solver->mkVar(u_sort, "x"); + d_solver->assertFormula(x.eqTerm(x)); + Result res = d_solver->checkSat(); + TS_ASSERT(res.isSat()); + TS_ASSERT(!res.isSatUnknown()); +} + +void ResultBlack::testIsUnsat() +{ + Sort u_sort = d_solver->mkUninterpretedSort("u"); + Term x = d_solver->mkVar(u_sort, "x"); + d_solver->assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver->checkSat(); + TS_ASSERT(res.isUnsat()); + TS_ASSERT(!res.isSatUnknown()); +} + +void ResultBlack::testIsSatUnknown() +{ + d_solver->setLogic("QF_NIA"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("solve-int-as-bv", "32"); + Sort int_sort = d_solver->getIntegerSort(); + Term x = d_solver->mkVar(int_sort, "x"); + d_solver->assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver->checkSat(); + TS_ASSERT(!res.isSat()); + TS_ASSERT(res.isSatUnknown()); +} + +void ResultBlack::testIsValid() +{ + Sort u_sort = d_solver->mkUninterpretedSort("u"); + Term x = d_solver->mkVar(u_sort, "x"); + d_solver->assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver->checkValid(); + TS_ASSERT(res.isValid()); + TS_ASSERT(!res.isValidUnknown()); +} + +void ResultBlack::testIsInvalid() +{ + Sort u_sort = d_solver->mkUninterpretedSort("u"); + Term x = d_solver->mkVar(u_sort, "x"); + d_solver->assertFormula(x.eqTerm(x)); + Result res = d_solver->checkValid(); + TS_ASSERT(res.isInvalid()); + TS_ASSERT(!res.isValidUnknown()); +} + +void ResultBlack::testIsValidUnknown() +{ + d_solver->setLogic("QF_NIA"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("solve-int-as-bv", "32"); + Sort int_sort = d_solver->getIntegerSort(); + Term x = d_solver->mkVar(int_sort, "x"); + d_solver->assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver->checkValid(); + TS_ASSERT(!res.isValid()); + TS_ASSERT(res.isValidUnknown()); + TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON"); +} + -- 2.30.2