projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0ad0496) | patch
Update purifySygusGTerm to the new API (#3830)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 27 Feb 2020 21:20:12 +0000 (15:20 -0600)
committerGitHub <noreply@github.com>
Thu, 27 Feb 2020 21:20:12 +0000 (15:20 -0600)
commita93b9c5a18bce93e2d66d1e98f13f69f0c193359
treef0ed05495eaf7bfefdc12aabad559f4666fa09e4tree
parent0ad0496cd474a167973195d1ddc9322ada7f2b4ecommit | diff
Update purifySygusGTerm to the new API (#3830)

Towards parser migration.

(Partially) updates the central function used for synth-fun in sygus v2 to the new API.

It also removes an optimization for "pure operators" from the v2 parser that is incompatible with the new API.
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history