A satisfiability checker for circuit equivalence. More...
#include <Solver.h>
Classes | |
| class | Circuit |
| The representation of a circuit within a logical engine. More... | |
Public Member Functions | |
| Solver (mlir::MLIRContext *mlirCtx, bool statisticsOpt) | |
| ~Solver ()=default | |
| mlir::LogicalResult | solve () |
| Solve the equivalence problem between the two circuits, then present the results to the user. More... | |
| Circuit * | addCircuit (llvm::StringRef name) |
| Create a new circuit to be compared and return it. More... | |
Private Member Functions | |
| void | printModel () |
| Prints a model satisfying the solved constraints. More... | |
| void | printAssertions () |
| Prints the constraints which were added to the solver. More... | |
| void | printStatistics () |
| Prints the internal statistics of the SMT solver for benchmarking purposes and operational insight. More... | |
| mlir::LogicalResult | constrainCircuits () |
| Formulates additional constraints which are satisfiable if only if the two circuits which are being compared are NOT equivalent, in which case there would be a model acting as a counterexample. More... | |
Private Attributes | |
| llvm::DenseMap< mlir::StringAttr, mlir::Value > | symbolTable |
| A map from internal solver symbols to the IR values they represent. More... | |
| Circuit * | circuits [2] |
| The two circuits to be compared. More... | |
| mlir::MLIRContext * | mlirCtx |
| The MLIR context of reference, owning all the MLIR entities. More... | |
| z3::context | context |
| The Z3 context of reference, owning all the declared values, constants and expressions. More... | |
| z3::solver | solver |
| The Z3 solver acting as the logical engine backend. More... | |
| bool | statisticsOpt |
The value of the statistics command-line option. More... | |
Detailed Description
A satisfiability checker for circuit equivalence.
This class interfaces with an external SMT solver acting as a logical engine. First spawn two circuits through addCircuit; after collecting their logical constraints, the solve method will compare them and report whether they result to be equivalent or, when not, also printing a model acting as a counterexample.
Constructor & Destructor Documentation
◆ Solver()
| Solver::Solver | ( | mlir::MLIRContext * | mlirCtx, |
| bool | statisticsOpt | ||
| ) |
Definition at line 26 of file Solver.cpp.
◆ ~Solver()
|
default |
Member Function Documentation
◆ addCircuit()
| Solver::Circuit * Solver::addCircuit | ( | llvm::StringRef | name | ) |
Create a new circuit to be compared and return it.
Definition at line 65 of file Solver.cpp.
◆ constrainCircuits()
|
private |
Formulates additional constraints which are satisfiable if only if the two circuits which are being compared are NOT equivalent, in which case there would be a model acting as a counterexample.
The procedure fails when detecting a mismatch of arity or type between the inputs and outputs of the circuits.
Definition at line 139 of file Solver.cpp.
References circuits, context, lec::errs(), circt::Solver::Circuit::getInputs(), circt::Solver::Circuit::getOutputs(), and solver.
Referenced by solve().
◆ printAssertions()
|
private |
Prints the constraints which were added to the solver.
Compared to solver.assertions().to_string() this method exposes each assertion as a z3::expression for eventual in-depth debugging.
Definition at line 115 of file Solver.cpp.
References lec::dbgs(), and solver.
Referenced by solve().
◆ printModel()
|
private |
Prints a model satisfying the solved constraints.
Definition at line 79 of file Solver.cpp.
References builder, mlirCtx, lec::outs(), solver, and symbolTable.
Referenced by solve().
◆ printStatistics()
|
private |
Prints the internal statistics of the SMT solver for benchmarking purposes and operational insight.
Definition at line 125 of file Solver.cpp.
References lec::outs(), and solver.
Referenced by solve().
◆ solve()
| LogicalResult Solver::solve | ( | ) |
Solve the equivalence problem between the two circuits, then present the results to the user.
Definition at line 32 of file Solver.cpp.
References constrainCircuits(), lec::errs(), lec::outs(), printAssertions(), printModel(), printStatistics(), solver, and statisticsOpt.
Member Data Documentation
◆ circuits
|
private |
The two circuits to be compared.
Definition at line 65 of file Solver.h.
Referenced by addCircuit(), and constrainCircuits().
◆ context
|
private |
The Z3 context of reference, owning all the declared values, constants and expressions.
Definition at line 70 of file Solver.h.
Referenced by constrainCircuits().
◆ mlirCtx
|
private |
The MLIR context of reference, owning all the MLIR entities.
Definition at line 67 of file Solver.h.
Referenced by printModel().
◆ solver
|
private |
The Z3 solver acting as the logical engine backend.
Definition at line 72 of file Solver.h.
Referenced by constrainCircuits(), printAssertions(), printModel(), printStatistics(), and solve().
◆ statisticsOpt
|
private |
◆ symbolTable
|
private |
A map from internal solver symbols to the IR values they represent.
Definition at line 63 of file Solver.h.
Referenced by printModel().
The documentation for this class was generated from the following files:
- /home/runner/work/circt-www/circt-www/circt_src/include/circt/LogicalEquivalence/Solver.h
- /home/runner/work/circt-www/circt-www/circt_src/lib/LogicalEquivalence/Solver.cpp
