Add proper support for the declare-heap command for separation logic (#5405)

This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic.

This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred.

Fixes #5343, fixes #4926.

Work towards CVC4/cvc4-wishues#22.

15 files changed, 17 insertions, 1 deletions

diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2
index 25a38b018..aff32e241 100644
--- a/test/regress/regress0/sep/dispose-1.smt2
+++ b/test/regress/regress0/sep/dispose-1.smt2
@@ -1,6 +1,8 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
+(declare-heap (Int Int))
+
 (declare-const w Int)
 (declare-const w1 Int)
 (declare-const w2 Int)
diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2
index 20421e735..454b73f64 100644
--- a/test/regress/regress0/sep/dup-nemp.smt2
+++ b/test/regress/regress0/sep/dup-nemp.smt2
@@ -2,6 +2,7 @@
 (set-info :status unsat)
 (declare-sort Loc 0)
 (declare-const l Loc)
+(declare-heap (Loc Loc))
 (assert (sep (not (_ emp Loc Loc)) (not (_ emp Loc Loc))))
 (assert (pto l l))
 (check-sat)
diff --git a/test/regress/regress0/sep/issue3720-check-model.smt2 b/test/regress/regress0/sep/issue3720-check-model.smt2
index 6130c0ca8..7e9c73cb8 100644
--- a/test/regress/regress0/sep/issue3720-check-model.smt2
+++ b/test/regress/regress0/sep/issue3720-check-model.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --quiet
 ; EXPECT: sat
 (set-logic ALL)
+(declare-heap (Int Int))
 (assert (_ emp Int Int))
 (check-sat)
diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index 2eaf664cd..583457e48 100644
--- a/test/regress/regress0/sep/nemp.smt2
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_SEP_LIA)
+(declare-heap (Int Int))
 (assert (not (_ emp Int Int)))
 (check-sat)
diff --git a/test/regress/regress0/sep/nil-no-elim.smt2 b/test/regress/regress0/sep/nil-no-elim.smt2
index e9aa3807a..6e6656865 100644
--- a/test/regress/regress0/sep/nil-no-elim.smt2
+++ b/test/regress/regress0/sep/nil-no-elim.smt2
@@ -3,6 +3,7 @@
 (declare-sort U 0)
 (declare-fun f (U) U)
 (declare-fun a () U)
+(declare-heap (U Int))
 
 (assert (= (as sep.nil U) (f a)))
 
diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2
index c807757d1..e57e50ea2 100644
--- a/test/regress/regress0/sep/nspatial-simp.smt2
+++ b/test/regress/regress0/sep/nspatial-simp.smt2
@@ -3,6 +3,7 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun x () Int)
+(declare-heap (Int Int))
 
 (assert (sep (= x 0) (not (= x 5))))
 
diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2
index 28ed5c47b..f980ac13f 100644
--- a/test/regress/regress0/sep/pto-01.smt2
+++ b/test/regress/regress0/sep/pto-01.smt2
@@ -1,5 +1,6 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 
diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2
index ab1cea0c8..111048c70 100644
--- a/test/regress/regress0/sep/pto-02.smt2
+++ b/test/regress/regress0/sep/pto-02.smt2
@@ -1,5 +1,6 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
+(declare-heap (Int Int))
 
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2
index a93fc4db8..8e577d5b7 100644
--- a/test/regress/regress0/sep/sep-01.smt2
+++ b/test/regress/regress0/sep/sep-01.smt2
@@ -1,5 +1,6 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 (declare-const y Int)
diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2
index 9522e2420..b843c1eda 100644
--- a/test/regress/regress0/sep/sep-plus1.smt2
+++ b/test/regress/regress0/sep/sep-plus1.smt2
@@ -1,5 +1,6 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 (declare-const y Int)
diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
index f620e9360..fc7bd0a51 100644
--- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
+++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
@@ -1,7 +1,8 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
-
 (declare-sort U 0)
+(declare-heap (U U))
+
 (declare-fun x () U)
 (declare-fun y () U)
 (declare-fun a () U)
diff --git a/test/regress/regress0/sep/simple-080420-const-sets.smt2 b/test/regress/regress0/sep/simple-080420-const-sets.smt2
index 1d85fb133..785017d5c 100644
--- a/test/regress/regress0/sep/simple-080420-const-sets.smt2
+++ b/test/regress/regress0/sep/simple-080420-const-sets.smt2
@@ -3,6 +3,7 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-option :produce-models true)
 (set-info :status sat)
+(declare-heap (Int Int))
 (declare-fun x () Int)
 
 ; works
diff --git a/test/regress/regress0/sep/skolem_emp.smt2 b/test/regress/regress0/sep/skolem_emp.smt2
index 7798f6bed..aac8382a7 100644
--- a/test/regress/regress0/sep/skolem_emp.smt2
+++ b/test/regress/regress0/sep/skolem_emp.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --no-check-models --sep-pre-skolem-emp
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
+(declare-heap (Int Int))
 (assert (not (_ emp Int Int)))
 (check-sat)
diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2
index 7daf012e2..46d96e84c 100644
--- a/test/regress/regress0/sep/trees-1.smt2
+++ b/test/regress/regress0/sep/trees-1.smt2
@@ -5,6 +5,7 @@
 (declare-const loc0 Loc)
 
 (declare-datatypes ((Node 0)) (((node (data Int) (left Loc) (right Loc)))))
+(declare-heap (Loc Node))
 
 (declare-fun data0 () Node)
 
diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2
index 4828646cb..95156a20c 100644
--- a/test/regress/regress0/sep/wand-crash.smt2
+++ b/test/regress/regress0/sep/wand-crash.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
+(declare-heap (Int Int))
 (assert (wand (_ emp Int Int) (_ emp Int Int)))
 (check-sat)