Improve syntax for fmf cardinality constraints (#7556)

This is an experimental extension of smt2.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index bf58e786ddabc43df16c776545557fe22ac342b7..daf1481004a1d9a2833242d4ff8510c8f6898f8b 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1690,8 +1690,7 @@ identifier[cvc5::ParseOp& p]
  */
 termAtomic[cvc5::api::Term& atomTerm]
 @init {
-  cvc5::api::Sort type;
-  cvc5::api::Sort type2;
+  cvc5::api::Sort t;
   std::string s;
   std::vector<uint64_t> numerals;
 }
@@ -1716,6 +1715,11 @@ termAtomic[cvc5::api::Term& atomTerm]
         std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
         atomTerm = PARSER_STATE->mkCharConstant(hexStr);
       }
+    | FMF_CARD_TOK sortSymbol[t,CHECK_DECLARED] INTEGER_LITERAL
+      {
+        uint32_t ubound = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+        atomTerm = SOLVER->mkCardinalityConstraint(t, ubound);
+      }
     | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
       {
         atomTerm =
@@ -2271,6 +2275,7 @@ FORALL_TOK        : 'forall';
 CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple';
 TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project';
+FMF_CARD_TOK: { !PARSER_STATE->strictModeEnabled() && PARSER_STATE->hasCardinalityConstraints() }? 'fmf.card';
 
 HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
 HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda';

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 19c3527f77c8cc61ddbaba75acda49a13b635f34..2fd91e49544965db8d0604262ebe18a5d7ecb88c 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -323,6 +323,8 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
 
 bool Smt2::isHoEnabled() const { return d_logic.isHigherOrder(); }
 
+bool Smt2::hasCardinalityConstraints() const { return d_logic.hasCardinalityConstraints(); }
+
 bool Smt2::logicIsSet() {
   return d_logicSet;
 }
@@ -512,11 +514,6 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
 
   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
     Parser::addOperator(api::APPLY_UF);
-
-    if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
-    {
-      addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card");
-    }
   }
 
   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 8d8f8febe334c628d352b7839de53de251bc2b9c..58a20cb2790a1f974c7b926e4a4afcebd5e28eaf 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -105,6 +105,10 @@ class Smt2 : public Parser
    * @return true if higher-order support is enabled, false otherwise
    */
   bool isHoEnabled() const;
+  /**
+   * @return true if cardinality constraints are enabled, false otherwise
+   */
+  bool hasCardinalityConstraints() const;
 
   bool logicIsSet() override;
 

diff --git a/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2
index f38a3ce41d33c83415aad490e6a48febcbb364ec..6ce1c41cd56cb67e3f43713b6c88156f18c2c53d 100644 (file)
--- 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 d1fd2301c67884ad10b6a2f4a505f9f4d1495d18..26c9b423f9d79172736f94c0505fbe82d6ab5a26 100644 (file)
--- 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 2d4000e6ef008268dfe26d1ab204421c1e46d97b..b07c53077d568183eef8e2a653257a8f7c4f2828 100644 (file)
--- 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 0d438f71803b74ed6fe3e32f589eca5fc81d8bb9..404b3abeaaa134344f9004161a6dc0a13136a48e 100644 (file)
--- 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 5aa7fc89411f83045b145b9672aec44b39aa3034..465584a833e6b12310b77628ecce689709dfd9ed 100644 (file)
--- 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 c46bc1e280e2ffc5199cfb596ea1bee7fb416e77..c265dddcd3ea249f617b9fd4383a13dc4e7b9b97 100644 (file)
--- 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 a92f2f441c8e4be64a3ce79a1a12d1cfaef9293e..d032114ac688707b55892bf619388e8b7f2f9ea8 100644 (file)
--- 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 75810699bae1e6181b8b1702b549225539d57100..62d078b32dbaf4e3703df29584bca5d799c24469 100644 (file)
--- 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 f145013d8539a7edec338ac2b123460b5e1d380c..2945a8a24e154be713fa81f9aa50e23dbde4819b 100644 (file)
--- 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)