{"id":302135,"date":"2020-04-19T15:00:10","date_gmt":"2020-04-19T15:00:10","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=302135"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-29T21:00:00","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=302135","title":{"rendered":"\u041a\u0430\u0440\u043c\u0430\u043d\u043d\u043e\u0435 \u0440\u0443\u043a\u043e\u0432\u043e\u0434\u0441\u0442\u0432\u043e \u043f\u043e Z3"},"content":{"rendered":"\n<div class=\"post__text post__text-html post__text_v1\" id=\"post-content-body\" data-io-article-url=\"https:\/\/habr.com\/ru\/post\/498002\/\">\n<h2 id=\"preambula\">\u041f\u0440\u0435\u0430\u043c\u0431\u0443\u043b\u0430<\/h2>\n<p>  <\/p>\n<p><img decoding=\"async\" src=\"https:\/\/habrastorage.org\/getpro\/habr\/post_images\/599\/b08\/d8e\/599b08d8ef8ca3b274bb4a36e5b0018e.jpg\" alt=\"image\"><\/p>\n<p>  <\/p>\n<blockquote><p>&quot;\u0427\u0435\u043b\u043e\u0432\u0435\u0447\u0435\u0441\u043a\u0438\u0439 \u043c\u043e\u0437\u0433 \u044d\u0442\u043e \u043f\u0443\u0441\u0442\u043e\u0439 \u0447\u0435\u0440\u0434\u0430\u043a. \u0414\u0443\u0440\u0430\u043a \u0442\u0430\u043a \u0438 \u0434\u0435\u043b\u0430\u0435\u0442: \u0442\u0430\u0449\u0438\u0442 \u0442\u0443\u0434\u0430 \u043d\u0443\u0436\u043d\u043e\u0435 \u0438 \u043d\u0435 \u043d\u0443\u0436\u043d\u043e\u0435. \u0418 \u043d\u0430\u043a\u043e\u043d\u0435\u0446 \u043d\u0430\u0441\u0442\u0443\u043f\u0430\u0435\u0442 \u043c\u043e\u043c\u0435\u043d\u0442, \u043a\u043e\u0433\u0434\u0430 \u0441\u0430\u043c\u0443\u044e \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u0443\u044e \u0432\u0435\u0449\u044c \u0442\u0443\u0434\u0430 \u043d\u0435 \u0437\u0430\u043f\u0438\u0445\u043d\u0435\u0448\u044c, \u0438\u043b\u0438 \u043d\u0430\u043e\u0431\u043e\u0440\u043e\u0442 \u043d\u0435 \u0434\u043e\u0441\u0442\u0430\u043d\u0435\u0448\u044c&#8230;&quot;<\/p>\n<p>  \u0412.\u0411. \u041b\u0438\u0432\u0430\u043d\u043e\u0432 (\u0438\u0437 \u043a\/\u0444 &quot;\u0428\u0435\u0440\u043b\u043e\u043a \u0425\u043e\u043b\u043c\u0441 \u0438 \u0434\u043e\u043a\u0442\u043e\u0440 \u0412\u0430\u0442\u0441\u043e\u043d&quot;)<\/p><\/blockquote>\n<p>\u0414\u0430\u043d\u043d\u043e\u0435 \u0440\u0443\u043a\u043e\u0432\u043e\u0434\u0441\u0442\u0432\u043e \u043d\u0435 \u043e\u0445\u0432\u0430\u0442\u044b\u0432\u0430\u0435\u0442 \u0432\u0435\u0441\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b SMT \u0440\u0435\u0448\u0430\u0442\u0435\u043b\u044f. \u041e\u043d\u043e \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043e \u0434\u043b\u044f \u0442\u0430\u043a\u0438\u0445 \u0441\u0438\u0442\u0443\u0430\u0446\u0438\u0439, \u043a\u043e\u0433\u0434\u0430 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0443 \u0441\u0440\u043e\u0447\u043d\u043e \u043d\u0443\u0436\u043d\u043e \u0432\u0441\u043f\u043e\u043c\u043d\u0438\u0442\u044c, \u043f\u043e\u0434\u0441\u043c\u043e\u0442\u0440\u0435\u0442\u044c \u043a\u0430\u043a \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u0442\u044c \u0442\u0443 \u0438\u043b\u0438 \u0438\u043d\u0443\u044e \u0435\u0433\u043e \u0438\u0434\u0435\u044e, \u043d\u0435 \u0442\u0440\u0430\u0442\u044f \u043c\u043d\u043e\u0433\u043e \u0432\u0440\u0435\u043c\u0435\u043d\u0438 \u043d\u0430 \u043f\u043e\u0438\u0441\u043a \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u0438, \u043e\u0442\u043b\u0430\u0434\u043a\u0443 \u0438 \u0442.\u0434. \u0418\u043d\u044b\u043c\u0438 \u0441\u043b\u043e\u0432\u0430\u043c\u0438 \u044d\u0442\u043e \u0440\u0443\u043a\u043e\u0432\u043e\u0434\u0441\u0442\u0432\u043e \u2014 \u0448\u043f\u0430\u0440\u0433\u0430\u043b\u043a\u0430, \u0437\u0430\u0442\u0440\u0430\u0433\u0438\u0432\u0430\u044e\u0449\u0430\u044f \u043b\u0438\u0448\u044c \u0447\u0430\u0441\u0442\u043e \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0435\u043c\u043e\u0435.<\/p>\n<p><a name=\"habracut\"><\/a>  <\/p>\n<h2 id=\"tipy-dannyh\">\u0422\u0438\u043f\u044b \u0434\u0430\u043d\u043d\u044b\u0445<\/h2>\n<p>  <\/p>\n<ul>\n<li>\n<p>x = Int(&#8216;x&#8217;)<\/p>\n<p>  <\/li>\n<li>\n<p>y = Real(&#8216;y&#8217;)<\/p>\n<p>  <\/li>\n<li>\n<p>z = Bool(&#8216;z&#8217;)<\/p>\n<p>  <\/li>\n<li>\n<p>s = String(&#8216;s&#8217;)<\/p>\n<p>  <\/li>\n<li>\n<p>x, y, z = Ints(&#8216;x y z&#8217;)<\/p>\n<p>  <\/li>\n<li>\n<p>x, y, z = Reals(&#8216;x y z&#8217;)<\/p>\n<p>  <\/li>\n<li>\n<p>x, y, z = Bools(&#8216;x y z&#8217;)<\/p>\n<p>  <\/li>\n<li>\n<p>x, y, z = Strings(&#8216;x y z&#8217;)<\/p>\n<p>  <\/li>\n<li>\n<p>v = BitVec(&#8216;v&#8217;, N) # N \u2014 \u0440\u0430\u0437\u043c\u0435\u0440 \u0431\u0438\u0442-\u0432\u0435\u043a\u0442\u043e\u0440\u0430<\/p>\n<p>  <\/li>\n<li>\n<p>X = IntVector(&#8216;X&#8217;, N)<\/p>\n<p>  <\/li>\n<li>\n<p>Y = RealVector(&#8216;Y&#8217;, N)<\/p>\n<p>  <\/li>\n<li>\n<p>Z = BoolVector(&#8216;Z&#8217;, N)<\/p>\n<p>  <\/li>\n<li>\n<p>A = Array(&#8216;A&#8217;, b, c) # b \u2014 \u043e\u0431\u043b\u0430\u0441\u0442\u044c \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f, \u0441 \u2014 \u0434\u0438\u0430\u043f\u0430\u0437\u043e\u043d <\/p>\n<p>  <\/li>\n<li>\n<p>Select(A, i) # \u0432\u0441\u0435 \u0440\u0430\u0432\u043d\u043e \u0447\u0442\u043e A[i]<\/p>\n<p>  <\/li>\n<li>\n<p>Store(&#8216;A&#8217;, i, a) # \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u043c\u0430\u0441\u0441\u0438\u0432 A c a \u043d\u0430 i-\u043e\u0439 \u043f\u043e\u0437\u0438\u0446\u0438\u0438<\/p>\n<p>  <\/li>\n<li>\n<p>FloatingPoint = FP(&#8216;fp&#8217;, FPSort(ebits, sbits)) # \u0444\u043e\u0440\u043c\u0430\u0442 IEEE 754<\/p>\n<p>  <\/li>\n<li>\n<p>v = BitVecVal(10, 32) # \u0431\u0438\u0442-\u0432\u0435\u043a\u0442\u043e\u0440 0x0000000a<\/p>\n<p>  <\/li>\n<li>\n<p>str = StringVal(&quot;aaaaa&quot;)<\/p>\n<p>  <\/li>\n<li>\n<p>c = Const(5, IntSort())<\/p>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<h2 id=\"regulyarnye-vyrazheniya\">\u0420\u0435\u0433\u0443\u043b\u044f\u0440\u043d\u044b\u0435 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f<\/h2>\n<p>  <\/p>\n<p>reg = Re(&#8216;re&#8217;)<\/p>\n<p>  <\/p>\n<p>re = Loop( reg, L, U ) # L \u2014 \u043d\u0438\u0436\u043d\u044f\u044f \u0433\u0440\u0430\u043d\u0438\u0446\u0430, U \u2014 \u0432\u0435\u0440\u0445\u043d\u044f\u044f \u0433\u0440\u0430\u043d\u0438\u0446\u0430<\/p>\n<p>  <\/p>\n<pre><code class=\"plaintext\">Ex:  re = Loop( Re('a') , 2, 5)  print( simplify( InRe( &quot;aaaa&quot;, re ) ) )  print( simplify( InRe( &quot;a&quot;, re ) ) )  Out:  True  False<\/code><\/pre>\n<p>  <\/p>\n<h2 id=\"operacii\">\u041e\u043f\u0435\u0440\u0430\u0446\u0438\u0438<\/h2>\n<p>  <\/p>\n<h3 id=\"logicheskie-svyazki\">\u041b\u043e\u0433\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0441\u0432\u044f\u0437\u043a\u0438<\/h3>\n<p>  <\/p>\n<ul>\n<li>\n<p>And(a, b)<\/p>\n<p>  <\/li>\n<li>\n<p>Not(a)<\/p>\n<p>  <\/li>\n<li>\n<p>Or(a, b)<\/p>\n<p>  <\/li>\n<li>\n<p>Xor(a, b)<\/p>\n<p>  <\/li>\n<li>\n<p>Implies(a, b) # a == b \u0434\u043b\u044f \u0431\u0443\u043b\u0435\u0432\u044b\u0445 a \u0438 b<\/p>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<h3 id=\"stroki\">\u0421\u0442\u0440\u043e\u043a\u0438<\/h3>\n<p>  <\/p>\n<ul>\n<li>\n<p>PrefixOf(substr, str)<\/p>\n<p>  <\/li>\n<li>\n<p>SuffixOf(substr, str)<\/p>\n<p>  <\/li>\n<li>\n<p>Concat(str1, str2)<\/p>\n<p>  <\/li>\n<li>\n<p>Length(str)<\/p>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<h3 id=\"drugie-poleznye-funkcii\">\u0414\u0440\u0443\u0433\u0438\u0435 \u043f\u043e\u043b\u0435\u0437\u043d\u044b\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438<\/h3>\n<p>  <\/p>\n<ul>\n<li>Sum(a, b, c)<\/li>\n<\/ul>\n<p>  <\/p>\n<pre><code class=\"plaintext\">Out:  0 + a + b + c<\/code><\/pre>\n<p>  <\/p>\n<ul>\n<li>Product(a, b, c)<\/li>\n<\/ul>\n<p>  <\/p>\n<pre><code class=\"plaintext\">Out:  1 * a * b * c<\/code><\/pre>\n<p>  <\/p>\n<ul>\n<li>Distinct(x, y)<\/li>\n<\/ul>\n<p>  <\/p>\n<pre><code class=\"plaintext\">Out:  x != y<\/code><\/pre>\n<p>  <\/p>\n<ul>\n<li>simplify(Distinct(x, y, z), blast_distinct=True)<\/li>\n<\/ul>\n<p>  <\/p>\n<pre><code class=\"plaintext\">Out:  And(Not(x == y), Not(x == z), Not(y == z))<\/code><\/pre>\n<p>  <\/p>\n<ul>\n<li>Extract(L, U, &#8216;x&#8217;) # L \u2014 \u0432\u0435\u0440\u0445\u043d\u044f\u044f \u0433\u0440\u0430\u043d\u0438\u0446\u0430, U \u2014 \u043d\u0438\u0436\u043d\u044f\u044f \u0433\u0440\u0430\u043d\u0438\u0446\u0430<\/li>\n<\/ul>\n<p>  <\/p>\n<pre><code class=\"plaintext\">Ex:  s = Solver()  x = BitVec('x', 8)  k = Extract(3, 0, x)  s.add(k == BitVecVal(10,4))  s.check()  print(s.model())  Out:  x = 10<\/code><\/pre>\n<p>  <\/p>\n<ul>\n<li>\n<p>LShR(x, i) # x &gt;&gt; i<\/p>\n<p>  <\/li>\n<li>\n<p>RotateLeft(a, i)<\/p>\n<p>  <\/li>\n<li>\n<p>RotateRight(a, i)<\/p>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<h2 id=\"solver\">Solver<\/h2>\n<p>  <\/p>\n<p>SMT Solver \u2014 \u0443\u0436\u0435 \u0433\u043e\u0442\u043e\u0432\u043e\u0435 \u0443\u043d\u0438\u0432\u0435\u0440\u0441\u0430\u043b\u044c\u043d\u043e\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435.<\/p>\n<p>  <\/p>\n<p><strong>s = Solver()<\/strong><\/p>\n<p>  <\/p>\n<p><strong>s = SolverFor(&#8216;proc&#8217;)<\/strong> # \u0432\u044b\u0431\u0440\u0430\u0442\u044c \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0443 \u043f\u0440\u0438\u043d\u044f\u0442\u0438\u044f \u0440\u0435\u0448\u0435\u043d\u0438\u0439<\/p>\n<p>  <\/p>\n<ul>\n<li>\n<p>s.push\/pop() # \u0441\u043e\u0437\u0434\u0430\u0442\u044c\/\u0432\u0435\u0440\u043d\u0443\u0442\u044c \u0438\u0437\u043c\u0435\u043d\u0435\u043d\u0438\u044f<\/p>\n<p>  <\/li>\n<li>\n<p>s.statistics() # \u043f\u043e\u0441\u043c\u043e\u0442\u0440\u0435\u0442\u044c \u0432\u043d\u0443\u0442\u0440\u0435\u043d\u043d\u0438\u0435 \u0441\u0447\u0435\u0442\u0447\u0438\u043a\u0438 \u0440\u0435\u0448\u0430\u0442\u0435\u043b\u044f<\/p>\n<p>  <\/li>\n<li>\n<p>s.assertions() # \u043f\u043e\u0441\u043c\u043e\u0442\u0440\u0435\u0442\u044c \u043a\u0430\u043a\u0438\u0435 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u044f \u043b\u0435\u0436\u0430\u0442 \u0432 \u0440\u0435\u0448\u0430\u0442\u0435\u043b\u0435<\/p>\n<p>  <\/li>\n<li>\n<p>set_option() # \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u0438\u0442\u044c \u043e\u043f\u0446\u0438\u0438 \u0434\u043b\u044f \u0440\u0435\u0448\u0430\u0442\u0435\u043b\u044f<\/p>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<pre><code class=\"plaintext\">Ex:  set_option(precision=10)    #   \u0442\u043e\u0447\u043d\u043e\u0441\u0442\u044c 10 \u0437\u043d\u0430\u043a\u043e\u0432 \u043f\u043e\u0441\u043b\u0435 \u0437\u0430\u043f\u044f\u0442\u043e\u0439 (\u0432\u044b\u0432\u043e\u0434 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0443\u0441\u0435\u0447\u0435\u043d \u0440\u0435\u0448\u0430\u0442\u0435\u043b\u0435\u043c \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0437\u043d\u0430\u043a\u0430 &quot;?&quot; )<\/code><\/pre>\n<p>  <\/p>\n<ul>\n<li>\n<p>s.check() # \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u044c \u043d\u0430 \u043d\u0430\u043b\u0438\u0447\u0438\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0439 ( \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b 3 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f: sat\/unsat\/unknown )<\/p>\n<p>  <\/li>\n<li>\n<p>simplify() # \u0443\u043f\u0440\u043e\u0449\u0435\u043d\u0438\u0435 \u043c\u043e\u0434\u0435\u043b\u0438<\/p>\n<p>  <\/li>\n<li>\n<p>s.sexpr() # \u0438\u0437\u0432\u043b\u0435\u0447\u0435\u043d\u0438\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f \u0432 SMT-LIB2<\/p>\n<p>  <\/li>\n<li>\n<p>s.model() # \u043c\u043e\u0434\u0435\u043b\u044c \u0440\u0435\u0448\u0435\u043d\u0438\u044f<\/p>\n<p>  <\/li>\n<li>\n<p>s.reset() # \u0441\u0431\u0440\u043e\u0441\u0438\u0442\u044c \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0440\u0435\u0448\u0430\u0442\u0435\u043b\u044f<\/p>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<h2 id=\"optimizacii\">\u041e\u043f\u0442\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u0438<\/h2>\n<p>  <\/p>\n<p>\u041e\u043f\u0442\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u044f \u043c\u043e\u0434\u0435\u043b\u0438 \u0434\u043b\u044f \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 t<\/p>\n<p>  <\/p>\n<p><strong>o = Optimize()<\/strong><\/p>\n<p>  <\/p>\n<ul>\n<li>\n<p>o.maximize(t)<\/p>\n<p>  <\/li>\n<li>\n<p>o.minimize(t)<\/p>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<pre><code class=\"plaintext\">Ex:  x1, x2, x3, x4, x5, m = Reals('x1 x2 x3 x4 x5 m')  o = Optimize()  o.add(-5 * x1 - 5 * x2 + 0 * x3 + 0 * x4 + 20 * x5 == 2 )  o.add( 0 * x1 +5 * x2 - 10 * x3 + 0 * x4 - 5 * x5 == 3 )  o.add( 0 * x1 -5 * x2 + 0 * x3 - 15 * x4 + 15 * x5 == 1 )  o.add( x1&gt;=0, x2&gt;=0, x3&gt;= 0, x4&gt;= 0, x5&gt;= 0)  o.add( 0 * x1 -1 * x2 + 0 * x3 + 0 * x4 - 0.5 * x5 == m )  h = o.maximize(m)  if o.check() == sat:      print(o.lower(h))      print(o.model())  Out:  h =  -6\/5 [x3 = 0, x5 = 2\/5, m = -6\/5, x4 = 0, x1 = 1\/5, x2 = 1]<\/code><\/pre>\n<p>  <\/p>\n<h2 id=\"ponyatie-celi\">\u041f\u043e\u043d\u044f\u0442\u0438\u0435 \u0446\u0435\u043b\u0438<\/h2>\n<p>  <\/p>\n<p>Goal (\u0446\u0435\u043b\u044c) \u2014 \u044d\u0442\u043e \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u0438\u044f \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u044b \u0434\u0430\u0435\u043c \u0440\u0435\u0448\u0430\u0442\u0435\u043b\u044e. \u041e\u0431\u0440\u0430\u0431\u043e\u0442\u043a\u0430 \u0446\u0435\u043b\u0438 \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u0432 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u0438 \u0441 \u0442\u0430\u043a\u0442\u0438\u043a\u043e\u0439. \u0422\u0430\u043a\u0442\u0438\u043a\u0430 \u043f\u0440\u0435\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u0446\u0435\u043b\u044c \u0432 \u043f\u043e\u0434\u0446\u0435\u043b\u0438. \u0426\u0435\u043b\u044c \u0440\u0435\u0448\u0430\u0435\u043c\u0430, \u0435\u0441\u043b\u0438 \u0445\u043e\u0442\u044f \u0431\u044b \u043e\u0434\u043d\u0430 \u043f\u043e\u0434\u0446\u0435\u043b\u044c \u0440\u0435\u0448\u0430\u0435\u043c\u0430.<\/p>\n<p>  <\/p>\n<p>g = Goal()<\/p>\n<p>  <\/p>\n<p>g.add(&#8230;)<\/p>\n<p>  <\/p>\n<p>\u041a\u043e\u043f\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 Goal<\/p>\n<p>  <\/p>\n<pre><code class=\"plaintext\">c = Context()  g2 = g.translate(c)<\/code><\/pre>\n<p>  <\/p>\n<h2 id=\"taktiki\">\u0422\u0430\u043a\u0442\u0438\u043a\u0438<\/h2>\n<p>  <\/p>\n<p>\u0422\u0430\u043a\u0442\u0438\u043a\u0430 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0438\u0437\u043c\u0435\u043d\u0438\u0442\u044c \u043d\u0430\u0431\u043e\u0440 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u0438\u0439 \u0434\u043b\u044f \u0446\u0435\u043b\u0438. \u0414\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0442\u0430\u043a\u0442\u0438\u043a \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0442\u043e\u0440\u044b.<\/p>\n<p>  <\/p>\n<ul>\n<li>\n<p>tactics() \u2014 \u043f\u043e\u0441\u043c\u043e\u0442\u0440\u0435\u0442\u044c \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u0435 \u0442\u0430\u043a\u0442\u0438\u043a\u0438<\/p>\n<p>  <\/li>\n<li>\n<p>tactic_description(&#8216;tactic_name&#8217;) \u2014 \u043f\u043e\u0441\u043c\u043e\u0442\u0440\u0435\u0442\u044c \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u0442\u0430\u043a\u0442\u0438\u043a\u0438<\/p>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<pre><code class=\"plaintext\">Ex:  g = Goal()  x, y = Ints('x y')  g.add(x == y + 1)  t  = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10)  g2 = t(g)  print(g2.as_expr())  Out:  And(x == y + 1, x &lt;= 10, x &gt;= 0, y &lt;= 10, y &gt;= 0)<\/code><\/pre>\n<p>  <\/p>\n<h3 id=\"kombinatory-taktik\">\u041a\u043e\u043c\u0431\u0438\u043d\u0430\u0442\u043e\u0440\u044b \u0442\u0430\u043a\u0442\u0438\u043a<\/h3>\n<p>  <\/p>\n<ul>\n<li>\n<p>Then(t, s) # t \u2014 \u0442\u0430\u043a\u0442\u0438\u043a\u0430 \u0446\u0435\u043b\u0438<\/p>\n<p>  <\/li>\n<li>\n<p>OrElse(t, s) # s \u2014 \u0442\u0430\u043a\u0442\u0438\u043a\u0430 \u043f\u043e\u0434\u0446\u0435\u043b\u0438<\/p>\n<p>  <\/li>\n<li>\n<p>Repeat(t)<\/p>\n<p>  <\/li>\n<li>\n<p>TryFor(t, ms) # ms \u2014 \u043c\u0438\u043b\u0438\u0441\u0435\u043a\u0443\u043d\u0434\u044b<\/p>\n<p>  <\/li>\n<li>\n<p>With(t, params) # params \u2014 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u044b \u0434\u043b\u044f \u0442\u0430\u043a\u0442\u0438\u043a\u0438<\/p>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<pre><code class=\"plaintext\">Ex:  Then('simplify', 'nlsat').solver()<\/code><\/pre>\n<p>  <\/p>\n<h2 id=\"arifmetiki\">\u0410\u0440\u0438\u0444\u043c\u0435\u0442\u0438\u043a\u0438<\/h2>\n<p>  <\/p>\n<h3 id=\"tablica-logik\">\u0422\u0430\u0431\u043b\u0438\u0446\u0430 \u043b\u043e\u0433\u0438\u043a<\/h3>\n<p>  <\/p>\n<div class=\"scrollable-table\">\n<table>\n<thead>\n<tr>\n<th>\u041b\u043e\u0433\u0438\u043a\u0430<\/th>\n<th>\u041e\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u043b\u043e\u0433\u0438\u043a\u0438<\/th>\n<th>Solver<\/th>\n<\/tr>\n<\/thead>\n<tbody>\n<tr>\n<td>LIA<\/td>\n<td>Linear Real Arithmetic<\/td>\n<td>Dual Simplex<\/td>\n<\/tr>\n<tr>\n<td>LRA<\/td>\n<td>Linear Integer Arithmetic<\/td>\n<td>Cuts + Branch<\/td>\n<\/tr>\n<tr>\n<td>LIRA<\/td>\n<td>Mixed Real\/Integer<\/td>\n<td>Cuts + Branch<\/td>\n<\/tr>\n<tr>\n<td>IDL<\/td>\n<td>Integer Difference Logic<\/td>\n<td>Floyd-Warshall<\/td>\n<\/tr>\n<tr>\n<td>RDL<\/td>\n<td>Real Difference Logic<\/td>\n<td>Bellman-Ford<\/td>\n<\/tr>\n<tr>\n<td>UTVPI<\/td>\n<td>Unit two-variable \/ inequality<\/td>\n<td>Bellman-Ford<\/td>\n<\/tr>\n<tr>\n<td>NRA<\/td>\n<td>Polynomial Real Arithmetic<\/td>\n<td>Model based CAD<\/td>\n<\/tr>\n<tr>\n<td>NIA<\/td>\n<td>Non-linear Integer Arithmetic<\/td>\n<td>CAD + Branch<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/div>\n<p>  <\/p>\n<h2 id=\"sovety\">\u0421\u043e\u0432\u0435\u0442\u044b<\/h2>\n<p>  <\/p>\n<h3 id=\"reshateli-dlya-strok\">\u0420\u0435\u0448\u0430\u0442\u0435\u043b\u0438 \u0434\u043b\u044f \u0441\u0442\u0440\u043e\u043a<\/h3>\n<p>  <\/p>\n<ul>\n<li>\n<p>s.set( &quot;smt.string.solver&quot;,&quot;seq&quot; )<\/p>\n<p>  <\/li>\n<li>\n<p>s.set( &quot;smt.string.solver&quot;,&quot;z3str3&quot; )<\/p>\n<p>  <\/li>\n<\/ul>\n<p>  <\/p>\n<h3 id=\"prinuditelnye-minimizacii\">\u041f\u0440\u0438\u043d\u0443\u0434\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u043c\u0438\u043d\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u0438<\/h3>\n<p>  <\/p>\n<ul>\n<li>s.set( &quot;smt.core.minimize&quot;,&quot;true&quot; ) <\/li>\n<\/ul>\n<p>  <\/p>\n<h2 id=\"ssylki\">\u0421\u0441\u044b\u043b\u043a\u0438<\/h2>\n<p>  <\/p>\n<p><a href=\"https:\/\/theory.stanford.edu\/~nikolaj\/programmingz3.html\" rel=\"nofollow\">\u041d\u0430 \u043c\u043e\u0439 \u0432\u0437\u0433\u043b\u044f\u0434 \u0441\u0430\u043c\u043e\u0435 \u043f\u0440\u0438\u044f\u0442\u043d\u043e\u0435 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435<\/a><\/p>\n<p>  <\/p>\n<p><a href=\"https:\/\/z3prover.github.io\/\" rel=\"nofollow\">\u0421\u043f\u0440\u0430\u0432\u043e\u0447\u043d\u0438\u043a<\/a><\/p>\n<p>  <\/p>\n<p><a href=\"http:\/\/smtlib.cs.uiowa.edu\/logics.shtml\" rel=\"nofollow\">SMT \u043b\u043e\u0433\u0438\u043a\u0438<\/a><\/p>\n<p>  <\/p>\n<p>\u041f\u0440\u0438\u043c\u0435\u0440\u044b: <a href=\"https:\/\/github.com\/Z3Prover\/doc\/tree\/master\/programmingz3\/code\" rel=\"nofollow\">\u0440\u0430\u0437<\/a> \u0438 <a href=\"http:\/\/www.cs.tau.ac.il\/~msagiv\/courses\/asv\/z3py\/\" rel=\"nofollow\">\u0434\u0432\u0430<\/a><\/p>\n<\/div>\n<p> \u0441\u0441\u044b\u043b\u043a\u0430 \u043d\u0430 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"https:\/\/habr.com\/ru\/post\/498002\/\"> https:\/\/habr.com\/ru\/post\/498002\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"\n<div class=\"post__text post__text-html post__text_v1\" id=\"post-content-body\" data-io-article-url=\"https:\/\/habr.com\/ru\/post\/498002\/\">\n<h2 id=\"preambula\">\u041f\u0440\u0435\u0430\u043c\u0431\u0443\u043b\u0430<\/h2>\n<p>  <\/p>\n<p><img decoding=\"async\" src=\"https:\/\/habrastorage.org\/getpro\/habr\/post_images\/599\/b08\/d8e\/599b08d8ef8ca3b274bb4a36e5b0018e.jpg\" alt=\"image\"><\/p>\n<p>  <\/p>\n<blockquote><p>&quot;\u0427\u0435\u043b\u043e\u0432\u0435\u0447\u0435\u0441\u043a\u0438\u0439 \u043c\u043e\u0437\u0433 \u044d\u0442\u043e \u043f\u0443\u0441\u0442\u043e\u0439 \u0447\u0435\u0440\u0434\u0430\u043a. \u0414\u0443\u0440\u0430\u043a \u0442\u0430\u043a \u0438 \u0434\u0435\u043b\u0430\u0435\u0442: \u0442\u0430\u0449\u0438\u0442 \u0442\u0443\u0434\u0430 \u043d\u0443\u0436\u043d\u043e\u0435 \u0438 \u043d\u0435 \u043d\u0443\u0436\u043d\u043e\u0435. \u0418 \u043d\u0430\u043a\u043e\u043d\u0435\u0446 \u043d\u0430\u0441\u0442\u0443\u043f\u0430\u0435\u0442 \u043c\u043e\u043c\u0435\u043d\u0442, \u043a\u043e\u0433\u0434\u0430 \u0441\u0430\u043c\u0443\u044e \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u0443\u044e \u0432\u0435\u0449\u044c \u0442\u0443\u0434\u0430 \u043d\u0435 \u0437\u0430\u043f\u0438\u0445\u043d\u0435\u0448\u044c, \u0438\u043b\u0438 \u043d\u0430\u043e\u0431\u043e\u0440\u043e\u0442 \u043d\u0435 \u0434\u043e\u0441\u0442\u0430\u043d\u0435\u0448\u044c&#8230;&quot;<\/p>\n<p>  \u0412.\u0411. \u041b\u0438\u0432\u0430\u043d\u043e\u0432 (\u0438\u0437 \u043a\/\u0444 &quot;\u0428\u0435\u0440\u043b\u043e\u043a \u0425\u043e\u043b\u043c\u0441 \u0438 \u0434\u043e\u043a\u0442\u043e\u0440 \u0412\u0430\u0442\u0441\u043e\u043d&quot;)<\/p><\/blockquote>\n<p>\u0414\u0430\u043d\u043d\u043e\u0435 \u0440\u0443\u043a\u043e\u0432\u043e\u0434\u0441\u0442\u0432\u043e \u043d\u0435 \u043e\u0445\u0432\u0430\u0442\u044b\u0432\u0430\u0435\u0442 \u0432\u0435\u0441\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b SMT \u0440\u0435\u0448\u0430\u0442\u0435\u043b\u044f. \u041e\u043d\u043e \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043e \u0434\u043b\u044f \u0442\u0430\u043a\u0438\u0445 \u0441\u0438\u0442\u0443\u0430\u0446\u0438\u0439, \u043a\u043e\u0433\u0434\u0430 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0443 \u0441\u0440\u043e\u0447\u043d\u043e \u043d\u0443\u0436\u043d\u043e \u0432\u0441\u043f\u043e\u043c\u043d\u0438\u0442\u044c, \u043f\u043e\u0434\u0441\u043c\u043e\u0442\u0440\u0435\u0442\u044c \u043a\u0430\u043a \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u0442\u044c \u0442\u0443 \u0438\u043b\u0438 \u0438\u043d\u0443\u044e \u0435\u0433\u043e \u0438\u0434\u0435\u044e, \u043d\u0435 \u0442\u0440\u0430\u0442\u044f \u043c\u043d\u043e\u0433\u043e \u0432\u0440\u0435\u043c\u0435\u043d\u0438 \u043d\u0430 \u043f\u043e\u0438\u0441\u043a \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u0438, \u043e\u0442\u043b\u0430\u0434\u043a\u0443 \u0438 \u0442.\u0434. \u0418\u043d\u044b\u043c\u0438 \u0441\u043b\u043e\u0432\u0430\u043c\u0438 \u044d\u0442\u043e \u0440\u0443\u043a\u043e\u0432\u043e\u0434\u0441\u0442\u0432\u043e \u2014 \u0448\u043f\u0430\u0440\u0433\u0430\u043b\u043a\u0430, \u0437\u0430\u0442\u0440\u0430\u0433\u0438\u0432\u0430\u044e\u0449\u0430\u044f \u043b\u0438\u0448\u044c \u0447\u0430\u0441\u0442\u043e \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0435\u043c\u043e\u0435.<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-302135","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/302135","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=302135"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/302135\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=302135"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=302135"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=302135"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}