From 9c767739c7ca2159de8800fff05dce3b7037cfc6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 2 Nov 2021 14:58:13 -0500 Subject: [PATCH] Improve syntax for fmf cardinality constraints (#7556) This is an experimental extension of smt2. --- src/parser/smt2/Smt2.g | 9 +++++++-- src/parser/smt2/smt2.cpp | 7 ++----- src/parser/smt2/smt2.h | 4 ++++ test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 | 2 +- test/regress/regress0/fmf/fc-simple.smt2 | 4 ++-- test/regress/regress0/fmf/fc-unsat-pent.smt2 | 4 ++-- test/regress/regress0/fmf/fc-unsat-tot-2.smt2 | 4 ++-- test/regress/regress0/fmf/issue4850-force-card.smt2 | 2 +- test/regress/regress0/fmf/issue4872-qf_ufc.smt2 | 4 ++-- test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 | 2 +- test/regress/regress0/issue5550-num-children.smt2 | 4 ++-- test/regress/regress1/fmf/fc-pigeonhole19.smt2 | 10 +++++----- 12 files changed, 31 insertions(+), 25 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index bf58e786d..daf148100 100644 --- 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 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 19c3527f7..2fd91e495 100644 --- 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 8d8f8febe..58a20cb27 100644 --- 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 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) -- 2.30.2