diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-04 14:24:02 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-04 14:24:02 -0600 |
| commit | 9ca190a3a2f7f952e1452efb69c78803ec302dd6 (patch) | |
| tree | 6581bc7bbb2b40a82ac65abf88d7b0c8610ef14f | |
| parent | 9a2913c2f1a22ed43ed772467ec42ba2262bee17 (diff) | |
Avoid non-well-founded sygus grammars (#3434)
| -rw-r--r-- | src/parser/smt2/Smt2.g | 28 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/sygus-no-wf.sy | 11 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/sygus-uf.sy | 2 |
4 files changed, 29 insertions, 15 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 0cce030b0..a5033278d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1054,21 +1054,21 @@ sygusGrammar[CVC4::Type & ret, // grammar. This results in the error below. // We can also be in a case where the only rule specified was // (Constant T), in which case we have not yet added a constructor. We - // ensure an arbitrary constant is added in this case. - if (datatypes[i].getNumConstructors() == 0) + // ensure an arbitrary constant is added in this case. We additionally + // add a constant if the grammar allows it regardless of whether the + // datatype has other constructors, since this ensures the datatype is + // well-founded (see 3423). + if (aci) { - if (aci) - { - Expr c = btt.mkGroundTerm(); - PARSER_STATE->addSygusConstructorTerm(datatypes[i], c, ntsToUnres); - } - else - { - std::stringstream se; - se << "Grouped rule listing for " << datatypes[i].getName() - << " produced an empty rule list."; - PARSER_STATE->parseError(se.str()); - } + Expr c = btt.mkGroundTerm(); + PARSER_STATE->addSygusConstructorTerm(datatypes[i], c, ntsToUnres); + } + else if (datatypes[i].getNumConstructors() == 0) + { + std::stringstream se; + se << "Grouped rule listing for " << datatypes[i].getName() + << " produced an empty rule list."; + PARSER_STATE->parseError(se.str()); } } // pop scope from the pre-declaration diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7e52501c2..7765591f8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -920,6 +920,8 @@ set(regress_0_tests regress0/sygus/parity-AIG-d0.sy regress0/sygus/parse-bv-let.sy regress0/sygus/real-si-all.sy + regress0/sygus/sygus-no-wf.sy + regress0/sygus/sygus-uf.sy regress0/sygus/strings-unconstrained.sy regress0/sygus/uminus_one.sy regress0/sygus/univ_3-long-repeat-conflict.sy @@ -2067,7 +2069,6 @@ set(regression_disabled_tests regress0/sets/sets-new.smt2 regress0/sets/sets-testlemma-ints.smt2 regress0/sets/sets-testlemma-reals.smt2 - regress0/sygus/sygus-uf.sy regress0/symmetric.smtv1.smt2 regress0/tptp/BOO003-4.p regress0/tptp/BOO027-1.p diff --git a/test/regress/regress0/sygus/sygus-no-wf.sy b/test/regress/regress0/sygus/sygus-no-wf.sy new file mode 100644 index 000000000..40a3d5547 --- /dev/null +++ b/test/regress/regress0/sygus/sygus-no-wf.sy @@ -0,0 +1,11 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat +(set-logic ALL) +(synth-fun f ((x0 Bool)) Bool + ( + (B Bool ((Variable Bool) (Constant Bool) (= I I) )) + (I Int ((Constant Int) (+ I I))) + ) +) +(constraint (= (f false) false)) +(check-synth) diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy index 95cd8771e..1b060637a 100644 --- a/test/regress/regress0/sygus/sygus-uf.sy +++ b/test/regress/regress0/sygus/sygus-uf.sy @@ -1,3 +1,5 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat (set-logic LIA) (declare-fun uf (Int) Int) |