projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 45c91fb) | patch
Eliminate uses of rewrite from datatypes theory (#7354)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 13 Oct 2021 15:22:03 +0000 (10:22 -0500)
committerGitHub <noreply@github.com>
Wed, 13 Oct 2021 15:22:03 +0000 (08:22 -0700)
commit55ce505ca757dc241bf4c1e10023bc43ac531a23
tree65193d766fed8a7091f21ecb5550c2188a9792b6tree
parent45c91fb32195d4f8de014c8ef91814c6625bcf43commit | diff
Eliminate uses of rewrite from datatypes theory (#7354)

Also simplifies slightly how rewritten forms of operators in sygus grammars are obtained.
src/smt/sygus_solver.cpp diff | blob | history
src/theory/datatypes/inference_manager.cpp diff | blob | history
src/theory/datatypes/proof_checker.cpp diff | blob | history
src/theory/datatypes/sygus_datatype_utils.cpp diff | blob | history
src/theory/evaluator.h diff | blob | history