Commit 8b8a56d
bp fix + dual rail as default
Signed-off-by: Noam Cohen <noam.chn1@gmail.com>1 parent 69100d4 commit 8b8a56d
1 file changed
Lines changed: 1 addition & 1 deletion
Submodule kepler-formal updated 42 files
- .github/workflows/regress-imc.yml+13-19
- .github/workflows/regress-ki.yml+13-19
- .github/workflows/regress-lec.yml+2
- .github/workflows/regress-pdr.yml+13-19
- bazel/homebrew_tbb.BUILD.bazel+19
- bazel/naja_includes.bzl+31
- bazel/tbb.bzl+17
- docs/sec-clock-handling.md+197
- docs/sec-flags-spec.md+2
- regress/run_sec_strategies_regress.sh+42-7
- src/bin/KeplerFormal.cpp+26-8
- src/clauses/SNLLogicCloud.cpp+1-1
- src/clauses/Tree2BoolExpr.cpp+2-2
- src/clocks/BUILD.bazel+1
- src/clocks/SecClockModel.h+1-1
- src/sat/SATSolverWrapper.h+18-18
- src/scope/ScopeExtraction.h+1-1
- src/sec/BUILD.bazel+17
- src/sec/common/BoolExprUtils.cpp+1-1
- src/sec/common/SecDiag.h+4
- src/sec/kinduction/BaseCaseSolver.cpp+55-28
- src/sec/kinduction/InductionStepSolver.cpp+11-11
- src/sec/kinduction/KInductionEngine.cpp+40-40
- src/sec/kinduction/KInductionEngine.h+1-1
- src/sec/kinduction/KInductionProblem.h+20
- src/sec/kinduction/SatEncoding.cpp+17-9
- src/sec/model/SequentialDesignModel.cpp+363-363
- src/sec/model/SequentialDesignModel.h+1-1
- src/sec/pdr/PDREngine.cpp+276-156
- src/sec/proof/DualRailEncoding.cpp+11-11
- src/sec/proof/DualRailEncoding.h+1-1
- src/sec/proof/ProofEngineShared.cpp+2-2
- src/sec/proof/TransitionExprResolver.cpp+5-5
- src/sec/strategy/ReachableStateInvariant.cpp+83-83
- src/sec/strategy/SequentialEquivalenceStrategy.cpp+356-238
- src/sec/strategy/SequentialEquivalenceStrategy.h+2-2
- src/sec/strategy/StructuralStateInvariant.cpp+235-235
- src/strategies/miter/BuildPrimaryOutputClauses.h+1-1
- test/sec/SequentialEquivalenceStrategyTests.cpp+591-126
- test/strategies/miter/KeplerFormalCliTests.cpp+254-168
- test/strategies/miter/MiterTests.cpp+2
- test/unit_designs/UnitDesignCompare.cpp+4
0 commit comments