diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-13 16:12:29 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-13 16:12:29 -0500 |
commit | a34f29798b3f4d1f83e1ced57fe53db53b9956f0 (patch) | |
tree | e04a6211d7e1968688da3fa48014cec861434d74 /src/smt | |
parent | 4b86268a71d0d6fd179134889f7d15304623b130 (diff) |
User-facing print debug option for sygus candidates (#4720)
This makes an option --debug-sygus available to the user for tracing the sygus solver. For the classic max2 example the option is:
(sygus-enum 0)
(sygus-candidate (max 0))
(sygus-enum 0)
(sygus-enum 1)
(sygus-enum x)
(sygus-enum x)
(sygus-candidate (max x))
(sygus-enum x)
(sygus-enum y)
(sygus-enum y)
(sygus-candidate (max y))
(sygus-enum y)
(sygus-enum (+ x x))
(sygus-enum (+ x 1))
(sygus-enum (+ 1 1))
...
(sygus-enum (ite (<= x y) y 1))
(sygus-candidate (max (ite (<= x y) y 1)))
(sygus-enum (ite (<= x y) y 1))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-candidate (max (ite (<= x y) y x)))
unsat
(define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
Where sygus-enum denotes enumerated terms and sygus-candidate is one that passes a CEGIS refinement check.
Diffstat (limited to 'src/smt')
0 files changed, 0 insertions, 0 deletions