Simplify the syntax and representation of the separation logic empty heap constraint (#7268)

Since ~1 year ago, we insist that the location and data types of the separation logic heap are set upfront, analogous to the set-logic command. This means that the separation logic empty heap constraint does not need to be annotated with its types.

This makes SEP_EMP a nullary Boolean operator instead of binary predicate (taking dummy arguments whose types specify the heap type). It changes the smt2 extended syntax from (_ emp T1 T2) to sep.emp.

17 files changed, 19 insertions, 19 deletions

diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2
index 45dd29459..5191ecd5b 100644
--- a/test/regress/regress0/sep/dispose-1.smt2
+++ b/test/regress/regress0/sep/dispose-1.smt2
@@ -13,7 +13,7 @@
 ;-----------------
 
 (assert (pto w (as sep.nil Int)))
-(assert (not (and (sep (and (_ emp Int Int) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
+(assert (not (and (sep (and sep.emp (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
 
 (check-sat)
 ;(get-model)
diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2
index 5682a0a02..3f792a4fb 100644
--- a/test/regress/regress0/sep/dup-nemp.smt2
+++ b/test/regress/regress0/sep/dup-nemp.smt2
@@ -3,6 +3,6 @@
 (declare-sort Loc 0)
 (declare-const l Loc)
 (declare-heap (Loc Loc))
-(assert (sep (not (_ emp Loc Loc)) (not (_ emp Loc Loc))))
+(assert (sep (not sep.emp) (not sep.emp)))
 (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 7e9c73cb8..488c558b0 100644
--- a/test/regress/regress0/sep/issue3720-check-model.smt2
+++ b/test/regress/regress0/sep/issue3720-check-model.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --quiet
+; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic ALL)
 (declare-heap (Int Int))
-(assert (_ emp Int Int))
+(assert sep.emp)
 (check-sat)
diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index 583457e48..2d35a43d8 100644
--- a/test/regress/regress0/sep/nemp.smt2
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic QF_SEP_LIA)
 (declare-heap (Int Int))
-(assert (not (_ emp Int Int)))
+(assert (not sep.emp))
 (check-sat)
diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
index 312c97542..c83e98b66 100644
--- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
+++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
@@ -8,6 +8,6 @@
 (declare-fun a () U)
 (declare-fun b () U)
 
-(assert (_ emp U U))
+(assert sep.emp)
 (assert (sep (pto x a) (pto y b)))
 (check-sat)
diff --git a/test/regress/regress0/sep/skolem_emp.smt2 b/test/regress/regress0/sep/skolem_emp.smt2
index 2a836bef9..1c690cc75 100644
--- a/test/regress/regress0/sep/skolem_emp.smt2
+++ b/test/regress/regress0/sep/skolem_emp.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic QF_ALL)
 (declare-heap (Int Int))
-(assert (not (_ emp Int Int)))
+(assert (not sep.emp))
 (check-sat)
diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2
index 2c742c60f..31c85d62d 100644
--- a/test/regress/regress0/sep/trees-1.smt2
+++ b/test/regress/regress0/sep/trees-1.smt2
@@ -18,7 +18,7 @@
 (declare-const r Loc)
 
 (define-fun ten-tree0 ((x Loc) (d Int)) Bool 
-(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (_ emp Loc Node) (= l (as sep.nil Loc))) (and (_ emp Loc Node) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
+(or (and sep.emp (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and sep.emp (= l (as sep.nil Loc))) (and sep.emp (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
 
 (declare-const dy Int)
 (declare-const y Loc)
@@ -26,7 +26,7 @@
 (declare-const z Loc)
 
 (define-fun ord-tree0 ((x Loc) (d Int)) Bool 
-(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (_ emp Loc Node) (= y (as sep.nil Loc))) (and (_ emp Loc Node) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
+(or (and sep.emp (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and sep.emp (= y (as sep.nil Loc))) (and sep.emp (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
 
 ;------- f -------
 (assert (= y (as sep.nil Loc)))
diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2
index 02511bbae..d84d900f3 100644
--- a/test/regress/regress0/sep/wand-crash.smt2
+++ b/test/regress/regress0/sep/wand-crash.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic QF_ALL)
 (declare-heap (Int Int))
-(assert (wand (_ emp Int Int) (_ emp Int Int)))
+(assert (wand sep.emp sep.emp))
 (check-sat)
diff --git a/test/regress/regress1/sep/emp2-quant-unsat.smt2 b/test/regress/regress1/sep/emp2-quant-unsat.smt2
index cdca1a909..acdd5f6c6 100644
--- a/test/regress/regress1/sep/emp2-quant-unsat.smt2
+++ b/test/regress/regress1/sep/emp2-quant-unsat.smt2
@@ -6,7 +6,7 @@
 (declare-fun u () U)
 (declare-heap (U U))
 
-(assert (sep (not (_ emp U U)) (not (_ emp U U))))
+(assert (sep (not sep.emp) (not sep.emp)))
 
 (assert (forall ((x U) (y U)) (= x y)))
 
diff --git a/test/regress/regress1/sep/finite-witness-sat.smt2 b/test/regress/regress1/sep/finite-witness-sat.smt2
index 479dbe2b2..1d5488296 100644
--- a/test/regress/regress1/sep/finite-witness-sat.smt2
+++ b/test/regress/regress1/sep/finite-witness-sat.smt2
@@ -5,7 +5,7 @@
 (declare-const l Loc)
 (declare-heap (Loc Loc))
 
-(assert (not (_ emp Loc Loc)))
+(assert (not sep.emp))
 (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 e6e2aca98..c40106c48 100644
--- a/test/regress/regress1/sep/fmf-nemp-2.smt2
+++ b/test/regress/regress1/sep/fmf-nemp-2.smt2
@@ -6,6 +6,6 @@
 (declare-fun u1 () U)
 (declare-fun u2 () U)
 (assert (not (= u1 u2)))
-(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (_ emp U Int)) (pto x 0)))))
+(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not sep.emp) (pto x 0)))))
 ; satisfiable with heap of size 2, model of U of size 3
 (check-sat)
diff --git a/test/regress/regress1/sep/quant_wand.smt2 b/test/regress/regress1/sep/quant_wand.smt2
index 87f0a974b..63dcebfda 100644
--- a/test/regress/regress1/sep/quant_wand.smt2
+++ b/test/regress/regress1/sep/quant_wand.smt2
@@ -6,7 +6,7 @@
 
 (declare-const u Int)
 
-(assert (_ emp Int Int))
+(assert sep.emp)
 
 (assert 
 (forall ((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 c6fa301f0..7935ccdc1 100644
--- a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
+++ b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
@@ -11,7 +11,7 @@
 (declare-const c Int)
 
 (assert (and
-        (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (_ emp Int Int)) ))
+        (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not sep.emp) ))
         (sep (pto x a) (pto y b))
   )
 )
diff --git a/test/regress/regress1/sep/wand-0526-sat.smt2 b/test/regress/regress1/sep/wand-0526-sat.smt2
index a07d0b8ae..334908e64 100644
--- a/test/regress/regress1/sep/wand-0526-sat.smt2
+++ b/test/regress/regress1/sep/wand-0526-sat.smt2
@@ -7,5 +7,5 @@
 (declare-fun u () Int)
 (declare-fun v () Int)
 (assert (wand (pto x u) (pto y v)))
-(assert (_ emp Int Int))
+(assert sep.emp)
 (check-sat)
diff --git a/test/regress/regress1/sep/wand-nterm-simp.smt2 b/test/regress/regress1/sep/wand-nterm-simp.smt2
index 47d39eb0b..4239a415e 100644
--- a/test/regress/regress1/sep/wand-nterm-simp.smt2
+++ b/test/regress/regress1/sep/wand-nterm-simp.smt2
@@ -3,6 +3,6 @@
 (set-logic QF_ALL)
 (declare-heap (Int Int))
 (declare-fun x () Int)
-(assert (wand (_ emp Int Int) (pto x 3)))
+(assert (wand sep.emp (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 647421665..15362f227 100644
--- a/test/regress/regress1/sep/wand-nterm-simp2.smt2
+++ b/test/regress/regress1/sep/wand-nterm-simp2.smt2
@@ -4,5 +4,5 @@
 (set-info :status sat)
 (declare-heap (Int Int))
 (declare-fun x () Int)
-(assert (wand (pto x 1) (_ emp Int Int)))
+(assert (wand (pto x 1) sep.emp))
 (check-sat)
diff --git a/test/regress/regress1/sep/wand-simp-unsat.smt2 b/test/regress/regress1/sep/wand-simp-unsat.smt2
index 2e90dfb26..b974b9a32 100644
--- a/test/regress/regress1/sep/wand-simp-unsat.smt2
+++ b/test/regress/regress1/sep/wand-simp-unsat.smt2
@@ -4,5 +4,5 @@
 (declare-fun x () Int)
 (declare-heap (Int Int))
 (assert (wand (pto x 1) (pto x 3)))
-(assert (_ emp Int Int))
+(assert sep.emp)
 (check-sat)