summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cvc4cpp.cpp7
-rw-r--r--src/api/cvc4cpp.h9
-rw-r--r--src/smt/smt_engine.cpp14
-rw-r--r--test/unit/api/CMakeLists.txt1
-rw-r--r--test/unit/api/result_black.h136
5 files changed, 161 insertions, 6 deletions
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<Expr>& assumptions, bool inUnsatCore)
Result SmtEngine::query(const Expr& assumption, bool inUnsatCore)
{
- return checkSatisfiability(
- assumption.isNull() ? std::vector<Expr>() : std::vector<Expr>{assumption},
- inUnsatCore,
- true);
+ return checkSatisfiability(assumption.isNull()
+ ? std::vector<Expr>()
+ : std::vector<Expr>{assumption},
+ inUnsatCore,
+ true)
+ .asValidityResult();
}
Result SmtEngine::query(const vector<Expr>& 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<Expr>& 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 <cxxtest/TestSuite.h>
+
+#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<Solver> 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");
+}
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback