projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 45e489e) | patch
Enum for all remaining string inferences (#4220)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 7 Apr 2020 00:00:13 +0000 (19:00 -0500)
committerGitHub <noreply@github.com>
Tue, 7 Apr 2020 00:00:13 +0000 (19:00 -0500)
commitfab7010523fd2e635c2c9dfd382acdefdb96d6b4
treed69370211e672c9d32534a39d01d6108c24e2261tree
parent45e489e2d48e3edde15be2187e32893fc35d859bcommit | diff
Enum for all remaining string inferences (#4220)

Merges the Flat Form inferences enum into Inferences. Adds documentation for (most of) these inferences. Removes the old infrastructure for inferences based on a debug string in InferenceManager.
src/theory/strings/base_solver.cpp diff | blob | history
src/theory/strings/core_solver.cpp diff | blob | history
src/theory/strings/extf_solver.cpp diff | blob | history
src/theory/strings/infer_info.cpp diff | blob | history
src/theory/strings/infer_info.h diff | blob | history
src/theory/strings/inference_manager.cpp diff | blob | history
src/theory/strings/inference_manager.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history