1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
Quickstart Guide
================
First, we create two constants ``x`` and ``y`` of sort ``Real``,
and two constants ``a`` and ``b`` of sort ``Integer``.
Notice that these are *symbolic* constants, but not actual values.
.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
:language: python
:dedent: 4
:start-after: docs-pythonic-quickstart-1 start
:end-before: docs-pythonic-quickstart-1 end
We define the following constraints regarding ``x`` and ``y``:
.. math::
(0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y)
We check whether there is a solution to these constraints:
.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
:language: python
:dedent: 4
:start-after: docs-pythonic-quickstart-2 start
:end-before: docs-pythonic-quickstart-2 end
In this case, there is, so we get output:
.. code:: text
[x = 1/6, y = 1/6]
We can also get an explicit model (assignment) for the constraints.
.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
:language: python
:dedent: 4
:start-after: docs-pythonic-quickstart-3 start
:end-before: docs-pythonic-quickstart-3 end
With the model, we can evaluate variables and terms:
.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
:language: python
:dedent: 4
:start-after: docs-pythonic-quickstart-4 start
:end-before: docs-pythonic-quickstart-4 end
This will print:
.. code:: text
x: 1/6
y: 1/6
x - y: 0
We can also get these values in other forms:
.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
:language: python
:dedent: 4
:start-after: docs-pythonic-quickstart-5 start
:end-before: docs-pythonic-quickstart-5 end
Next, we assert the same assertions as above, but with integers.
This time, there is no solution, so "no solution" is printed.
.. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py
:language: python
:dedent: 4
:start-after: docs-pythonic-quickstart-6 start
:end-before: docs-pythonic-quickstart-6 end
Example
-------
.. api-examples::
<examples>/api/python/pythonic/quickstart.py
<examples>/api/python/quickstart.py
<examples>/api/cpp/quickstart.cpp
<examples>/api/c/quickstart.c
<examples>/api/java/QuickStart.java
<examples>/api/smtlib/quickstart.smt2
|
