Improve syntax for fmf cardinality constraints (#7556)

This is an experimental extension of smt2.

9 files changed, 18 insertions, 18 deletions

diff --git a/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2
index f38a3ce41..6ce1c41cd 100644
--- a/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2
+++ b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2
@@ -4,7 +4,7 @@
 ; generated by Nunchaku
 (declare-sort i_ 0)
 (declare-fun __nun_card_witness_0_ () i_)
-(assert (fmf.card __nun_card_witness_0_ 2))
+(assert (_ fmf.card i_ 2))
 (declare-fun i2_ () i_)
 (declare-fun i1_ () i_)
 (declare-fun i3_ () i_)
diff --git a/test/regress/regress0/fmf/fc-simple.smt2 b/test/regress/regress0/fmf/fc-simple.smt2
index d1fd2301c..26c9b423f 100644
--- a/test/regress/regress0/fmf/fc-simple.smt2
+++ b/test/regress/regress0/fmf/fc-simple.smt2
@@ -6,7 +6,7 @@
 (declare-fun a () U)
 (declare-fun c () U)
 
-(assert (fmf.card c 2))
-(assert (not (fmf.card a 4)))
+(assert (_ fmf.card U 2))
+(assert (not (_ fmf.card U 4)))
 
 (check-sat)
diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2
index 2d4000e6e..b07c53077 100644
--- a/test/regress/regress0/fmf/fc-unsat-pent.smt2
+++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2
@@ -15,6 +15,6 @@
 (assert (not (= d e)))
 (assert (not (= e a)))
 
-(assert (fmf.card c 2))
+(assert (_ fmf.card U 2))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
index 0d438f718..404b3abea 100644
--- a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
+++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
@@ -7,8 +7,8 @@
 (declare-fun b () U)
 (declare-fun c () U)
 
-(assert (not (fmf.card a 2)))
+(assert (not (_ fmf.card U 2)))
 
 (assert (forall ((x U)) (or (= x a) (= x b))))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/fmf/issue4850-force-card.smt2 b/test/regress/regress0/fmf/issue4850-force-card.smt2
index 5aa7fc894..465584a83 100644
--- a/test/regress/regress0/fmf/issue4850-force-card.smt2
+++ b/test/regress/regress0/fmf/issue4850-force-card.smt2
@@ -2,5 +2,5 @@
 (set-info :status sat)
 (declare-sort a 0)
 (declare-fun b () a)
-(assert (not (fmf.card b 1)))
+(assert (not (_ fmf.card a 1)))
 (check-sat)
diff --git a/test/regress/regress0/fmf/issue4872-qf_ufc.smt2 b/test/regress/regress0/fmf/issue4872-qf_ufc.smt2
index c46bc1e28..c265dddcd 100644
--- a/test/regress/regress0/fmf/issue4872-qf_ufc.smt2
+++ b/test/regress/regress0/fmf/issue4872-qf_ufc.smt2
@@ -2,6 +2,6 @@
 (set-info :status sat)
 (declare-sort S0 0)
 (declare-const S0-0 S0)
-(assert (fmf.card S0-0 1))
-(assert (fmf.card S0-0 4))
+(assert (_ fmf.card S0 1))
+(assert (_ fmf.card S0 4))
 (check-sat)
diff --git a/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 b/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2
index a92f2f441..d032114ac 100644
--- a/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2
+++ b/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2
@@ -2,5 +2,5 @@
 (set-info :status sat)
 (declare-sort a 0)
 (declare-fun b () a)
-(assert (fmf.card b 2))
+(assert (_ fmf.card a 2))
 (check-sat)
diff --git a/test/regress/regress0/issue5550-num-children.smt2 b/test/regress/regress0/issue5550-num-children.smt2
index 75810699b..62d078b32 100644
--- a/test/regress/regress0/issue5550-num-children.smt2
+++ b/test/regress/regress0/issue5550-num-children.smt2
@@ -2,5 +2,5 @@
 (set-logic UFC)
 (declare-sort a 0)
 (declare-fun b () a)
-(assert (not (fmf.card b 1)))
-(check-sat)
\ No newline at end of file
+(assert (not (_ fmf.card a 1)))
+(check-sat)
diff --git a/test/regress/regress1/fmf/fc-pigeonhole19.smt2 b/test/regress/regress1/fmf/fc-pigeonhole19.smt2
index f145013d8..2945a8a24 100644
--- a/test/regress/regress1/fmf/fc-pigeonhole19.smt2
+++ b/test/regress/regress1/fmf/fc-pigeonhole19.smt2
@@ -8,13 +8,13 @@
 (declare-fun h () H)
 
 ; pigeonhole using native cardinality constraints
-(assert (fmf.card p 19))
-(assert (not (fmf.card p 18)))
-(assert (fmf.card h 18))
-(assert (not (fmf.card h 17)))
+(assert (_ fmf.card P 19))
+(assert (not (_ fmf.card P 18)))
+(assert (_ fmf.card H 18))
+(assert (not (_ fmf.card H 17)))
 
 ; each pigeon has different holes
 (declare-fun f (P) H)
 (assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))
 
-(check-sat)
\ No newline at end of file
+(check-sat)