diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-12 17:13:14 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-12 17:13:14 -0500 |
| commit | 103b5ea715e532e021e91f9b03ea7d7876a3ccbf (patch) | |
| tree | be6dbe34884cf96e4d22bfefd8071e3afb11e841 /test/regress/regress0/sygus | |
| parent | 85a8dfddd887a041f397d1ff2c3a6c34900c5775 (diff) | |
Fixes for degenerate case of sygus decision tree learning (#4800)
Fixes #4790.
Fixes two bugs in the decision tree learning solver for sygus, one involving evaluation of "templated" enumerators, and one involving ITE strategies where child types are different than the root.
Diffstat (limited to 'test/regress/regress0/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/issue4790-dtd.sy | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/issue4790-dtd.sy b/test/regress/regress0/sygus/issue4790-dtd.sy new file mode 100644 index 000000000..55f4723ec --- /dev/null +++ b/test/regress/regress0/sygus/issue4790-dtd.sy @@ -0,0 +1,23 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic NIA) +(synth-fun patternGen ((i Int)) Int +((ITE Int) (CONST Int) (I Int) (B Bool)) +( (ITE Int ( + (ite (<= i CONST) I I) + + )) + (CONST Int (0)) + (I Int (i 1 + (+ I I) (- I I) (* I I) + )) + (B Bool ( + (<= I I) + )) +) +) +(declare-var i Int) +(constraint (= (patternGen 0) 1)) +(constraint (= (patternGen 1) 1)) +(constraint (= (patternGen 2) 1)) +(check-synth) |