From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 6 Jan 2022 23:26:10 +0000 (-0600)
Subject: Disallow separation logic in incremental mode (#7888)
X-Git-Tag: cvc5-1.0.0~590
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=668518797aa22f2cb905b4e63397da304ed22967;p=cvc5.git

Disallow separation logic in incremental mode (#7888)

Fixes #5541. Fixes #5607.
---

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 9f4e05409..4bb3bfabf 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1219,6 +1219,13 @@ void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
   }
   SolverEngineScope smts(this);
   finishInit();
+  // check whether incremental is enabled, where separation logic is not
+  // supported.
+  if (d_env->getOptions().base.incrementalSolving)
+  {
+    throw RecoverableModalException(
+        "Separation logic not supported in incremental mode");
+  }
   TheoryEngine* te = getTheoryEngine();
   te->declareSepHeap(locT, dataT);
 }
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index bdd8201bc..7a04566dd 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1902,6 +1902,7 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
 TEST_F(TestApiBlackSolver, declareSepHeap)
 {
   d_solver.setLogic("ALL");
+  d_solver.setOption("incremental", "false");
   Sort integer = d_solver.getIntegerSort();
   ASSERT_NO_THROW(d_solver.declareSepHeap(integer, integer));
   // cannot declare separation logic heap more than once
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 7313405be..2de49dfb4 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1879,6 +1879,7 @@ class SolverTest
   @Test void declareSepHeap() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
+    d_solver.setOption("incremental", "false");
     Sort integer = d_solver.getIntegerSort();
     assertDoesNotThrow(() -> d_solver.declareSepHeap(integer, integer));
     // cannot declare separation logic heap more than once
diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 90e6610d8..b73b691c4 100644
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -1338,6 +1338,7 @@ def test_get_value3(solver):
 
 def test_declare_sep_heap(solver):
     solver.setLogic("ALL")
+    solver.setOption("incremental", "false")
     integer = solver.getIntegerSort()
     solver.declareSepHeap(integer, integer)
     # cannot declare separation logic heap more than once
@@ -2100,16 +2101,6 @@ def test_declare_pool(solver):
     with pytest.raises(RuntimeError):
         solver.declarePool("i", nullSort, [])
 
-
-def test_declare_sep_heap(solver):
-    solver.setLogic("ALL")
-    integer = solver.getIntegerSort()
-    solver.declareSepHeap(integer, integer)
-    # cannot declare separation logic heap more than once
-    with pytest.raises(RuntimeError):
-        solver.declareSepHeap(integer, integer)
-
-
 def test_define_fun_global(solver):
     bSort = solver.getBooleanSort()