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.

31 files changed, 31 insertions, 0 deletions

diff --git a/test/regress/regress1/sep/chain-int.smt2 b/test/regress/regress1/sep/chain-int.smt2
index ebe52fa46..6aaca31c5 100644
--- a/test/regress/regress1/sep/chain-int.smt2
+++ b/test/regress/regress1/sep/chain-int.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/regress1/sep/crash1220.smt2 b/test/regress/regress1/sep/crash1220.smt2
index f68434f33..4df23fd80 100644
--- a/test/regress/regress1/sep/crash1220.smt2
+++ b/test/regress/regress1/sep/crash1220.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 (declare-const a Int)
diff --git a/test/regress/regress1/sep/dispose-list-4-init.smt2 b/test/regress/regress1/sep/dispose-list-4-init.smt2
index b3e2088b1..0ee63cc8a 100644
--- a/test/regress/regress1/sep/dispose-list-4-init.smt2
+++ b/test/regress/regress1/sep/dispose-list-4-init.smt2
@@ -3,6 +3,7 @@
 (set-logic QF_ALL_SUPPORTED)
 
 (declare-sort Loc 0)
+(declare-heap (Loc Loc))
 
 (declare-const w Loc)
 (declare-const u1 Loc)
diff --git a/test/regress/regress1/sep/emp2-quant-unsat.smt2 b/test/regress/regress1/sep/emp2-quant-unsat.smt2
index 118e63f07..a0921aa31 100644
--- a/test/regress/regress1/sep/emp2-quant-unsat.smt2
+++ b/test/regress/regress1/sep/emp2-quant-unsat.smt2
@@ -4,6 +4,7 @@
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun u () U)
+(declare-heap (U U))
 
 (assert (sep (not (_ emp U U)) (not (_ emp U U))))
 
diff --git a/test/regress/regress1/sep/finite-witness-sat.smt2 b/test/regress/regress1/sep/finite-witness-sat.smt2
index 1f3338ed7..fac9d6b9d 100644
--- a/test/regress/regress1/sep/finite-witness-sat.smt2
+++ b/test/regress/regress1/sep/finite-witness-sat.smt2
@@ -3,6 +3,7 @@
 (set-logic ALL_SUPPORTED)
 (declare-sort Loc 0)
 (declare-const l Loc)
+(declare-heap (Loc Loc))
 
 (assert (not (_ emp Loc Loc)))
 (assert (forall ((x Loc) (y Loc)) (not (pto x y))))
diff --git a/test/regress/regress1/sep/fmf-nemp-2.smt2 b/test/regress/regress1/sep/fmf-nemp-2.smt2
index 356405869..49420145e 100644
--- a/test/regress/regress1/sep/fmf-nemp-2.smt2
+++ b/test/regress/regress1/sep/fmf-nemp-2.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (declare-sort U 0)
+(declare-heap (U Int))
 (declare-fun u1 () U)
 (declare-fun u2 () U)
 (assert (not (= u1 u2)))
diff --git a/test/regress/regress1/sep/loop-1220.smt2 b/test/regress/regress1/sep/loop-1220.smt2
index b857aec2a..41078391a 100644
--- a/test/regress/regress1/sep/loop-1220.smt2
+++ b/test/regress/regress1/sep/loop-1220.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 (declare-const a Int)
diff --git a/test/regress/regress1/sep/pto-04.smt2 b/test/regress/regress1/sep/pto-04.smt2
index 9b0afda7a..e3d3ea7a1 100644
--- a/test/regress/regress1/sep/pto-04.smt2
+++ b/test/regress/regress1/sep/pto-04.smt2
@@ -1,5 +1,6 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
+(declare-heap (Int Int))
 
 (declare-const x1 Int)
 (declare-const x2 Int)
diff --git a/test/regress/regress1/sep/quant_wand.smt2 b/test/regress/regress1/sep/quant_wand.smt2
index 662682ec3..bb4e40308 100644
--- a/test/regress/regress1/sep/quant_wand.smt2
+++ b/test/regress/regress1/sep/quant_wand.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
+(declare-heap (Int Int))
 
 (declare-const u Int)
 
diff --git a/test/regress/regress1/sep/sep-02.smt2 b/test/regress/regress1/sep/sep-02.smt2
index 6f190d964..a67394d90 100644
--- a/test/regress/regress1/sep/sep-02.smt2
+++ b/test/regress/regress1/sep/sep-02.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/regress1/sep/sep-03.smt2 b/test/regress/regress1/sep/sep-03.smt2
index 8dce5acc7..f29d081fc 100644
--- a/test/regress/regress1/sep/sep-03.smt2
+++ b/test/regress/regress1/sep/sep-03.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/regress1/sep/sep-find2.smt2 b/test/regress/regress1/sep/sep-find2.smt2
index 3d6188894..412caee9b 100644
--- a/test/regress/regress1/sep/sep-find2.smt2
+++ b/test/regress/regress1/sep/sep-find2.smt2
@@ -1,5 +1,6 @@
 (set-logic QF_SEP_LIA)
 (set-info :status unsat)
+(declare-heap (Int Int))
 
 (declare-const x1 Int)
 (declare-const x2 Int)
diff --git a/test/regress/regress1/sep/sep-fmf-priority.smt2 b/test/regress/regress1/sep/sep-fmf-priority.smt2
index fe3af1b35..8aed93119 100644
--- a/test/regress/regress1/sep/sep-fmf-priority.smt2
+++ b/test/regress/regress1/sep/sep-fmf-priority.smt2
@@ -5,6 +5,7 @@
 (declare-sort Loc 0)
 (declare-const l Loc)
 (declare-const x Loc)
+(declare-heap (Loc Loc))
 
 (assert (wand (pto x x) false))
 (assert (forall ((x Loc) (y Loc)) (not (pto x y))))
diff --git a/test/regress/regress1/sep/sep-neg-1refine.smt2 b/test/regress/regress1/sep/sep-neg-1refine.smt2
index ab12c6461..81b107ab5 100644
--- a/test/regress/regress1/sep/sep-neg-1refine.smt2
+++ b/test/regress/regress1/sep/sep-neg-1refine.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 (declare-const y Int)
diff --git a/test/regress/regress1/sep/sep-neg-nstrict.smt2 b/test/regress/regress1/sep/sep-neg-nstrict.smt2
index 425e5ce3c..6594a1075 100644
--- a/test/regress/regress1/sep/sep-neg-nstrict.smt2
+++ b/test/regress/regress1/sep/sep-neg-nstrict.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/regress1/sep/sep-neg-nstrict2.smt2 b/test/regress/regress1/sep/sep-neg-nstrict2.smt2
index 7ada6ff06..0243282a3 100644
--- a/test/regress/regress1/sep/sep-neg-nstrict2.smt2
+++ b/test/regress/regress1/sep/sep-neg-nstrict2.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 (declare-const y Int)
diff --git a/test/regress/regress1/sep/sep-neg-simple.smt2 b/test/regress/regress1/sep/sep-neg-simple.smt2
index 7b6fc69e9..8b23a6da8 100644
--- a/test/regress/regress1/sep/sep-neg-simple.smt2
+++ b/test/regress/regress1/sep/sep-neg-simple.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 (declare-const y Int)
diff --git a/test/regress/regress1/sep/sep-neg-swap.smt2 b/test/regress/regress1/sep/sep-neg-swap.smt2
index 53f890b0d..ba83f2575 100644
--- a/test/regress/regress1/sep/sep-neg-swap.smt2
+++ b/test/regress/regress1/sep/sep-neg-swap.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 (declare-const y Int)
diff --git a/test/regress/regress1/sep/sep-nterm-again.smt2 b/test/regress/regress1/sep/sep-nterm-again.smt2
index 3e595b5e9..43fb7b00d 100644
--- a/test/regress/regress1/sep/sep-nterm-again.smt2
+++ b/test/regress/regress1/sep/sep-nterm-again.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 (declare-const y Int)
diff --git a/test/regress/regress1/sep/sep-nterm-val-model.smt2 b/test/regress/regress1/sep/sep-nterm-val-model.smt2
index d4fb0fd52..635f0895a 100644
--- a/test/regress/regress1/sep/sep-nterm-val-model.smt2
+++ b/test/regress/regress1/sep/sep-nterm-val-model.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/regress1/sep/sep-simp-unc.smt2 b/test/regress/regress1/sep/sep-simp-unc.smt2
index cedbb53eb..88950d655 100644
--- a/test/regress/regress1/sep/sep-simp-unc.smt2
+++ b/test/regress/regress1/sep/sep-simp-unc.smt2
@@ -3,6 +3,7 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (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/regress1/sep/simple-neg-sat.smt2 b/test/regress/regress1/sep/simple-neg-sat.smt2
index 70927ad82..929a8e66f 100644
--- a/test/regress/regress1/sep/simple-neg-sat.smt2
+++ b/test/regress/regress1/sep/simple-neg-sat.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 
 (declare-const x Int)
 (declare-const y Int)
diff --git a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
index 91b07093c..1b7932dc4 100644
--- a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
+++ b/test/regress/regress1/sep/split-find-unsat-w-emp.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/regress1/sep/split-find-unsat.smt2 b/test/regress/regress1/sep/split-find-unsat.smt2
index 1a9e76a8a..60ab5d038 100644
--- a/test/regress/regress1/sep/split-find-unsat.smt2
+++ b/test/regress/regress1/sep/split-find-unsat.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: unsat
 (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/regress1/sep/wand-0526-sat.smt2 b/test/regress/regress1/sep/wand-0526-sat.smt2
index 99116c9d1..556be6c18 100644
--- a/test/regress/regress1/sep/wand-0526-sat.smt2
+++ b/test/regress/regress1/sep/wand-0526-sat.smt2
@@ -1,6 +1,7 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
+(declare-heap (Int Int))
 (declare-fun x () Int)
 (declare-fun y () Int)
 (declare-fun u () Int)
diff --git a/test/regress/regress1/sep/wand-false.smt2 b/test/regress/regress1/sep/wand-false.smt2
index 65500f775..9f95c06b7 100644
--- a/test/regress/regress1/sep/wand-false.smt2
+++ b/test/regress/regress1/sep/wand-false.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 (declare-fun x () Int)
 (assert (wand (pto x x) false))
 (check-sat)
diff --git a/test/regress/regress1/sep/wand-nterm-simp.smt2 b/test/regress/regress1/sep/wand-nterm-simp.smt2
index 702f03a02..4ecc8ad1e 100644
--- a/test/regress/regress1/sep/wand-nterm-simp.smt2
+++ b/test/regress/regress1/sep/wand-nterm-simp.smt2
@@ -1,6 +1,7 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
+(declare-heap (Int Int))
 (declare-fun x () Int)
 (assert (wand (_ emp Int Int) (pto x 3)))
 (check-sat)
diff --git a/test/regress/regress1/sep/wand-nterm-simp2.smt2 b/test/regress/regress1/sep/wand-nterm-simp2.smt2
index 352be5777..5b7c92a4a 100644
--- a/test/regress/regress1/sep/wand-nterm-simp2.smt2
+++ b/test/regress/regress1/sep/wand-nterm-simp2.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 (declare-fun x () Int)
 (assert (wand (pto x 1) (_ emp Int Int)))
 (check-sat)
diff --git a/test/regress/regress1/sep/wand-simp-sat.smt2 b/test/regress/regress1/sep/wand-simp-sat.smt2
index 120683f74..ec63a762e 100644
--- a/test/regress/regress1/sep/wand-simp-sat.smt2
+++ b/test/regress/regress1/sep/wand-simp-sat.smt2
@@ -1,6 +1,7 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
+(declare-heap (Int Int))
 (declare-fun x () Int)
 (assert (wand (pto x 1) (pto x 1)))
 (check-sat)
diff --git a/test/regress/regress1/sep/wand-simp-sat2.smt2 b/test/regress/regress1/sep/wand-simp-sat2.smt2
index c684d16ad..315071c05 100644
--- a/test/regress/regress1/sep/wand-simp-sat2.smt2
+++ b/test/regress/regress1/sep/wand-simp-sat2.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
+(declare-heap (Int Int))
 (declare-fun x () Int)
 (assert (wand (pto x 1) (pto x 3)))
 (check-sat)
diff --git a/test/regress/regress1/sep/wand-simp-unsat.smt2 b/test/regress/regress1/sep/wand-simp-unsat.smt2
index 8c038e3d7..da1d8bd51 100644
--- a/test/regress/regress1/sep/wand-simp-unsat.smt2
+++ b/test/regress/regress1/sep/wand-simp-unsat.smt2
@@ -2,6 +2,7 @@
 ; EXPECT: unsat
 (set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
+(declare-heap (Int Int))
 (assert (wand (pto x 1) (pto x 3)))
 (assert (_ emp Int Int))
 (check-sat)