From 4e9cef3063ca0155d4d97714d288ab7d88df5c30 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Apr 2021 22:02:31 -0500 Subject: [PATCH] Add unit test for abduction (#6400) --- test/unit/api/solver_black.cpp | 35 ++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index db950dd7e..5240d8020 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1270,6 +1270,41 @@ TEST_F(TestApiBlackSolver, getInfo) ASSERT_THROW(d_solver.getInfo("asdf"), CVC5ApiException); } +TEST_F(TestApiBlackSolver, getAbduct) +{ + d_solver.setLogic("QF_LIA"); + d_solver.setOption("produce-abducts", "true"); + d_solver.setOption("incremental", "false"); + + Sort intSort = d_solver.getIntegerSort(); + Term zero = d_solver.mkInteger(0); + Term x = d_solver.mkConst(intSort, "x"); + Term y = d_solver.mkConst(intSort, "y"); + + // Assumptions for abduction: x > 0 + d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); + // Conjecture for abduction: y > 0 + Term conj = d_solver.mkTerm(GT, y, zero); + Term output; + // Call the abduction api, while the resulting abduct is the output + ASSERT_TRUE(d_solver.getAbduct(conj, output)); + // We expect the resulting output to be a boolean formula + ASSERT_TRUE(!output.isNull() && output.getSort().isBoolean()); + + // try with a grammar, a simple grammar admitting true + Sort boolean = d_solver.getBooleanSort(); + Term truen = d_solver.mkBoolean(true); + Term start = d_solver.mkVar(boolean); + Term output2; + Grammar g = d_solver.mkSygusGrammar({}, {start}); + Term conj2 = d_solver.mkTerm(GT, x, zero); + ASSERT_NO_THROW(g.addRule(start, truen)); + // Call the abduction api, while the resulting abduct is the output + ASSERT_TRUE(d_solver.getAbduct(conj2, g, output2)); + // abduct must be true + ASSERT_EQ(output2, truen); +} + TEST_F(TestApiBlackSolver, getInterpolant) { d_solver.setLogic("QF_LIA"); -- 2.30.2