Commit c1ae0cd
fixes for sec flow
Signed-off-by: Noam Cohen <noam.chn1@gmail.com>1 parent ee50120 commit c1ae0cd
2 files changed
Lines changed: 11 additions & 3 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
54 | 54 | | |
55 | 55 | | |
56 | 56 | | |
| 57 | + | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
57 | 64 | | |
58 | 65 | | |
59 | 66 | | |
| |||
64 | 71 | | |
65 | 72 | | |
66 | 73 | | |
| 74 | + | |
67 | 75 | | |
68 | | - | |
| 76 | + | |
69 | 77 | | |
70 | | - | |
| 78 | + | |
71 | 79 | | |
72 | 80 | | |
73 | 81 | | |
| |||
Submodule kepler-formal updated 60 files
- .github/workflows/regress-imc.yml+157
- .github/workflows/regress-ki.yml+157
- .github/workflows/regress-lec.yml+16-69
- .github/workflows/regress-pdr.yml+157
- .gitmodules+3
- CMakeLists.txt+75-1
- MODULE.bazel+7-7
- bazel/deps.bzl+13-4
- example/tinyrocket.if/db_interface.snl
- example/tinyrocket.if/snl.mf+3-3
- example/tinyrocket_edited.v+3-3
- example/tinyrocket_naja_edited.if/snl.mf+3-3
- example/tinyrocket_pre_edited.v+3-3
- regress/run_sec_strategies_regress.sh+147
- src/bin/CMakeLists.txt+1
- src/bin/KeplerFormal.cpp+23-16
- src/clauses/SNLLogicCloud.cpp+14-14
- src/clauses/SNLTruthTableTree.cpp+30-30
- src/clauses/Tree2BoolExpr.cpp+11-11
- src/config/Config.h+2-1
- src/formal/BoolExpr.h+1-1
- src/sat/BUILD.bazel+1
- src/sat/SATSolverWrapper.h+462-8
- src/scope/ScopeExtraction.cpp+8-8
- src/sec/BUILD.bazel+4
- src/sec/CMakeLists.txt+3
- src/sec/common/BoolExprUtils.cpp+129-36
- src/sec/common/BoolExprUtils.h+10
- src/sec/common/ProofProblemDebug.cpp+6-6
- src/sec/imc/ExactInterpolantSynthesizer.cpp+1-1
- src/sec/imc/IMCEngine.cpp+34-1
- src/sec/kinduction/BaseCaseSolver.cpp+3.3k-71
- src/sec/kinduction/BaseCaseSolver.h+157
- src/sec/kinduction/InductionStepSolver.cpp+276-22
- src/sec/kinduction/KInductionEngine.cpp+179-33
- src/sec/kinduction/KInductionEngine.h-4
- src/sec/kinduction/KInductionProblem.h+32
- src/sec/kinduction/OutputBatching.cpp+116
- src/sec/kinduction/OutputBatching.h+38
- src/sec/kinduction/SatEncoding.cpp+311-41
- src/sec/kinduction/SatEncoding.h+54-2
- src/sec/model/SequentialDesignModel.cpp+393-129
- src/sec/pdr/PDREngine.cpp+10.2k-415
- src/sec/pdr/PDREngine.h+51-2
- src/sec/proof/ProofEngineShared.cpp+190-23
- src/sec/proof/ProofEngineShared.h+8
- src/sec/proof/TransitionExprResolver.cpp+442
- src/sec/proof/TransitionExprResolver.h+48
- src/sec/strategy/ReachableStateInvariant.cpp+603-108
- src/sec/strategy/ReachableStateInvariant.h+6-1
- src/sec/strategy/SequentialEquivalenceStrategy.cpp+944-90
- src/sec/strategy/StructuralStateInvariant.cpp+235-93
- src/sec/strategy/StructuralStateInvariant.h+25
- src/strategies/CMakeLists.txt+2-2
- src/strategies/miter/BuildPrimaryOutputClauses.cpp+9-9
- src/strategies/miter/MiterStrategy.cpp+17-17
- src/utils/SNLLogicCone.cpp+9-9
- test/sec/SequentialEquivalenceStrategyTests.cpp+6.0k-916
- thirdparty/CMakeLists.txt+2
- thirdparty/cadical+1
0 commit comments