cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

use z3

Browse Source
This commit is contained in:
chriseth 2022-04-17 18:11:42 +02:00
parent 4ace0ed82c
commit 1cc485bf72
2 changed files with 13 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libyul/optimiser/ReasoningBasedSimplifier.cpp
View File

@ -24,6 +24,7 @@
#include <libsmtutil/SMTPortfolio.h> #include <libsmtutil/SMTPortfolio.h>
#include <libsmtutil/Helpers.h> #include <libsmtutil/Helpers.h>
#include <libsmtutil/Z3Interface.h>
#include <libsolutil/CommonData.h> #include <libsolutil/CommonData.h>
@ -42,7 +43,8 @@ void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _ast)
{ {
ReasoningBasedSimplifier simpl{_context.dialect}; ReasoningBasedSimplifier simpl{_context.dialect};
// Hack to inject the boolean lp solver. // Hack to inject the boolean lp solver.
simpl.m_solver = make_unique<BooleanLPSolver>(); //simpl.m_solver = make_unique<BooleanLPSolver>();
simpl.m_solver = make_unique<Z3Interface>();
simpl(_ast); simpl(_ast);
} }

12
test/libyul/yulOptimizerTests/reasoningBasedSimplifier/loopinc.yul
View File

@ -17,6 +17,14 @@
// //
// { // {
// let y := calldataload(0) // let y := calldataload(0)
// let t := calldataload(32) // let sum := 0
// if sgt(sub(y, 1), y) { if 1 { sstore(0, 1) } } // let x := 0
// for { } lt(x, y) { }
// {
// if 0 { }
// if 0 { }
// sum := calldataload(add(0x20, mul(x, 0x20)))
// x := add(x, 1)
// }
// sstore(0, sum)
// } // }