summaryrefslogtreecommitdiff
path: root/CMakeLists.txt
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-07-17 09:40:56 -0500
committerGitHub <noreply@github.com>2020-07-17 09:40:56 -0500
commit0988217562006d3f59e01dc261f39121df6d75f5 (patch)
treecb634a136f07112758a118f523a4cc4596834d19 /CMakeLists.txt
parentcb8d041d3820a46721f689f188839184003e0e7c (diff)
(proof-new) Updates to strings core solver (#4642)
This updates the core strings solver in preparation for proofs. The main changes include: The addition of the strings PfRule enum values. The definition of a "getConclusion" static method, used by the core solver, and to be used in the future by the strings proof checker. This includes several optional forms of lemmas, which are added as options in this PR. Major simplifications to our inference schemas for disequality handling (a STRING_DECOMPOSE inference rule). Note this is the only significant intended behavioral change in this PR. Minor updates to the form of inferences send to inference manager, for instance to orient equalities in the expected way, and to reorder assumptions. These changes are done for uniformity and make the strings proof reconstruction from inference steps easier.
Diffstat (limited to 'CMakeLists.txt')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback