Skip to content

Convert MRSolver to use SAWCore rewriter instead of TermModel simulator backend #2434

@brianhuffman

Description

@brianhuffman

Currently the MRSolver SAWScript commands internally use a term normalization procedure that is based on the TermModel backend of the SAWCore simulator. The kind of term normalization required here is exactly what the SAWCore rewriting engine was designed for, and we should convert MRSolver to use the SAWCore rewriter for this purpose.

On the other hand, the TermModel backend uses the SAWCore simulator in some unintended ways that interfere with some other refactoring efforts (#2429).

Metadata

Metadata

Assignees

Labels

obsoleteIssues that involve/depend on deprecated code, such that they are not worth pursuingsubsystem: MRSolverIssues related to the Mr. Solver monadic-recursive solver in Heapstertech debtIssues that document or involve technical debttype: bugIssues reporting bugs or unexpected/unwanted behavior

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions