diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-06 01:24:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-06 01:24:17 -0700 |
commit | fd60da4a22f02f6f5b82cef3585240c1b33595e9 (patch) | |
tree | 137d45e65f204c2f604fed65d47a7d7b4f716c78 /test | |
parent | 6a61c1a75b08867c7c06623b8c03084056b6bed7 (diff) |
Keep definitions when global-declarations enabled (#4572)
Fixes #4552. Fixes #4555. The SMT-LIB standard mandates that definitions
are kept when `:global-declarations` are enabled. Until now, CVC4 was
keeping track of the symbols of a definition correctly but lost the body
of the definition when the user context was popped. This commit fixes
the issue by adding a `global` parameter to
`SmtEngine::defineFunction()` and `SmtEngine::defineFunctionRec()`. If
that parameter is set, the definitions of functions are added at level 0
to `d_definedFunctions` and the lemmas for recursive function
definitions are kept in an additional list and asserted during each
`checkSat` call. The commit also updates new API, the commands, and the
parsers to reflect this change.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/smtlib/issue4552.smt2 | 27 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 73 |
3 files changed, 101 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4bc9d2705..e0ce456bc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -921,6 +921,7 @@ set(regress_0_tests regress0/smtlib/issue4028.smt2 regress0/smtlib/issue4077.smt2 regress0/smtlib/issue4151.smt2 + regress0/smtlib/issue4552.smt2 regress0/smtlib/reason-unknown.smt2 regress0/smtlib/reset.smt2 regress0/smtlib/reset-assertions1.smt2 diff --git a/test/regress/regress0/smtlib/issue4552.smt2 b/test/regress/regress0/smtlib/issue4552.smt2 new file mode 100644 index 000000000..af8e0b948 --- /dev/null +++ b/test/regress/regress0/smtlib/issue4552.smt2 @@ -0,0 +1,27 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +(set-logic UF) +(set-option :global-declarations true) + +(push) +(define a true) +(define (f (b Bool)) b) +(define-const a2 Bool true) + +(define-fun a3 () Bool true) + +(define-fun-rec b () Bool true) +(define-funs-rec ((g ((b Bool)) Bool)) (b)) +(assert (or (not a) (not a2) (not a3) (not b) (g false))) +(check-sat) +(pop) + +(assert (or (not a) (not a2) (not a3) (not b) (g false))) +(check-sat) + +(reset-assertions) + +(assert (or (not a) (not a2) (not a3) (not b) (g false))) +(check-sat) diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 3dcf18f78..257c28669 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -84,8 +84,11 @@ class SolverBlack : public CxxTest::TestSuite void testDeclareSort(); void testDefineFun(); + void testDefineFunGlobal(); void testDefineFunRec(); + void testDefineFunRecGlobal(); void testDefineFunsRec(); + void testDefineFunsRecGlobal(); void testUFIteration(); @@ -1036,6 +1039,30 @@ void SolverBlack::testDefineFun() CVC4ApiException&); } +void SolverBlack::testDefineFunGlobal() +{ + Sort bSort = d_solver->getBooleanSort(); + Sort fSort = d_solver->mkFunctionSort({bSort}, bSort); + + Term bTrue = d_solver->mkBoolean(true); + // (define-fun f () Bool true) + Term f = d_solver->defineFun("f", {}, bSort, bTrue, true); + Term b = d_solver->mkVar(bSort, "b"); + Term gSym = d_solver->mkConst(fSort, "g"); + // (define-fun g (b Bool) Bool b) + Term g = d_solver->defineFun(gSym, {b}, b, true); + + // (assert (or (not f) (not (g true)))) + d_solver->assertFormula(d_solver->mkTerm( + OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm())); + TS_ASSERT(d_solver->checkSat().isUnsat()); + d_solver->resetAssertions(); + // (assert (or (not f) (not (g true)))) + d_solver->assertFormula(d_solver->mkTerm( + OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm())); + TS_ASSERT(d_solver->checkSat().isUnsat()); +} + void SolverBlack::testDefineFunRec() { Sort bvSort = d_solver->mkBitVectorSort(32); @@ -1090,6 +1117,31 @@ void SolverBlack::testDefineFunRec() CVC4ApiException&); } +void SolverBlack::testDefineFunRecGlobal() +{ + Sort bSort = d_solver->getBooleanSort(); + Sort fSort = d_solver->mkFunctionSort({bSort}, bSort); + + d_solver->push(); + Term bTrue = d_solver->mkBoolean(true); + // (define-fun f () Bool true) + Term f = d_solver->defineFunRec("f", {}, bSort, bTrue, true); + Term b = d_solver->mkVar(bSort, "b"); + Term gSym = d_solver->mkConst(fSort, "g"); + // (define-fun g (b Bool) Bool b) + Term g = d_solver->defineFunRec(gSym, {b}, b, true); + + // (assert (or (not f) (not (g true)))) + d_solver->assertFormula(d_solver->mkTerm( + OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm())); + TS_ASSERT(d_solver->checkSat().isUnsat()); + d_solver->pop(); + // (assert (or (not f) (not (g true)))) + d_solver->assertFormula(d_solver->mkTerm( + OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm())); + TS_ASSERT(d_solver->checkSat().isUnsat()); +} + void SolverBlack::testDefineFunsRec() { Sort uSort = d_solver->mkUninterpretedSort("u"); @@ -1162,6 +1214,27 @@ void SolverBlack::testDefineFunsRec() CVC4ApiException&); } +void SolverBlack::testDefineFunsRecGlobal() +{ + Sort bSort = d_solver->getBooleanSort(); + Sort fSort = d_solver->mkFunctionSort({bSort}, bSort); + + d_solver->push(); + Term bTrue = d_solver->mkBoolean(true); + Term b = d_solver->mkVar(bSort, "b"); + Term gSym = d_solver->mkConst(fSort, "g"); + // (define-funs-rec ((g ((b Bool)) Bool)) (b)) + d_solver->defineFunsRec({gSym}, {{b}}, {b}, true); + + // (assert (not (g true))) + d_solver->assertFormula(d_solver->mkTerm(APPLY_UF, gSym, bTrue).notTerm()); + TS_ASSERT(d_solver->checkSat().isUnsat()); + d_solver->pop(); + // (assert (not (g true))) + d_solver->assertFormula(d_solver->mkTerm(APPLY_UF, gSym, bTrue).notTerm()); + TS_ASSERT(d_solver->checkSat().isUnsat()); +} + void SolverBlack::testUFIteration() { Sort intSort = d_solver->getIntegerSort(); |