Created
December 4, 2018 22:19
-
-
Save timxor/47ba0078ef41ee22b0680ab5f430ed0b to your computer and use it in GitHub Desktop.
sudo pip3 install --user karl
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ``` | |
| ➜ karl git:(master) sudo pip3 install --user karl | |
| The directory '/Users/tim.siwula/Library/Caches/pip/http' or its parent directory is not owned by the current user and the cache has been disabled. Please check the permissions and owner of that directory. If executing pip with sudo, you may want sudo's -H flag. | |
| The directory '/Users/tim.siwula/Library/Caches/pip' or its parent directory is not owned by the current user and caching wheels has been disabled. check the permissions and owner of that directory. If executing pip with sudo, you may want sudo's -H flag. | |
| Collecting karl | |
| Downloading https://files.pythonhosted.org/packages/46/db/c75ee661d10e7a3aa49c3d1d05fdd34e008537fbcfee531fa66a55eea71f/karl-0.2.10-py3-none-any.whl | |
| Collecting mythril>=0.19.1 (from karl) | |
| Requirement already satisfied: web3>=4.8.2 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from karl) (4.8.2) | |
| Requirement already satisfied: rlp>=1.0.1 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (1.0.3) | |
| Requirement already satisfied: coloredlogs>=10.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (10.0) | |
| Requirement already satisfied: eth-keys>=0.2.0b3 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (0.2.0b3) | |
| Requirement already satisfied: ethereum-input-decoder>=0.2.2 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (0.2.2) | |
| Requirement already satisfied: eth-utils>=1.0.1 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (1.3.0) | |
| Requirement already satisfied: requests in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (2.20.1) | |
| Collecting z3-solver>=4.8.0.0 (from mythril>=0.19.1->karl) | |
| Downloading https://files.pythonhosted.org/packages/83/7e/9e3b84ed773945cfa3c00e64c3ef49c492bf4b6f60cf6223b8756053e7f4/z3-solver-4.8.0.0.post1.tar.gz (4.1MB) | |
| 100% |████████████████████████████████| 4.1MB 6.5MB/s | |
| Requirement already satisfied: eth-hash>=0.1.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (0.2.0) | |
| Requirement already satisfied: plyvel in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (1.0.5) | |
| Requirement already satisfied: coverage in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (4.5.2) | |
| Requirement already satisfied: eth-keyfile>=0.5.1 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (0.5.1) | |
| Requirement already satisfied: eth-tester>=0.1.0b21 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (0.1.0b33) | |
| Requirement already satisfied: eth-typing<2.0.0,>=1.3.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (1.3.0) | |
| Collecting transaction>=2.2.1 (from mythril>=0.19.1->karl) | |
| Downloading https://files.pythonhosted.org/packages/21/38/499bcc737411b00ea969fdc82e1ff56925a0ea634fe03173e18fbdd59015/transaction-2.4.0-py2.py3-none-any.whl (48kB) | |
| 100% |████████████████████████████████| 51kB 8.6MB/s | |
| Collecting py-solc (from mythril>=0.19.1->karl) | |
| Downloading https://files.pythonhosted.org/packages/47/74/d36abca3f36ccdcd04976c50f83502c870623e5beb4a4ec96c7bad4bb9e8/py_solc-3.2.0-py3-none-any.whl | |
| Requirement already satisfied: eth-abi>=1.0.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (1.2.2) | |
| Requirement already satisfied: persistent>=4.2.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (4.4.3) | |
| Requirement already satisfied: ethereum>=2.3.2 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (2.3.2) | |
| Requirement already satisfied: configparser>=3.5.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (3.5.0) | |
| Requirement already satisfied: eth-account>=0.1.0a2 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (0.3.0) | |
| Collecting py-flags (from mythril>=0.19.1->karl) | |
| Downloading https://files.pythonhosted.org/packages/0b/84/9dac0652068c2901f56d37797eb2c303befdafc5f5131f041951b7c86e22/py_flags-1.1.2-py3-none-any.whl | |
| Collecting jinja2>=2.9 (from mythril>=0.19.1->karl) | |
| Downloading https://files.pythonhosted.org/packages/7f/ff/ae64bacdfc95f27a016a7bed8e8686763ba4d277a78ca76f32659220a731/Jinja2-2.10-py2.py3-none-any.whl (126kB) | |
| 100% |████████████████████████████████| 133kB 23.6MB/s | |
| Collecting mock (from mythril>=0.19.1->karl) | |
| Downloading https://files.pythonhosted.org/packages/e6/35/f187bdf23be87092bd0f1200d43d23076cee4d0dec109f195173fd3ebc79/mock-2.0.0-py2.py3-none-any.whl (56kB) | |
| 100% |████████████████████████████████| 61kB 9.4MB/s | |
| Requirement already satisfied: eth-rlp>=0.1.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mythril>=0.19.1->karl) (0.1.2) | |
| Requirement already satisfied: websockets<7.0.0,>=6.0.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from web3>=4.8.2->karl) (6.0) | |
| Requirement already satisfied: hexbytes<1.0.0,>=0.1.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from web3>=4.8.2->karl) (0.1.0) | |
| Requirement already satisfied: cytoolz<1.0.0,>=0.9.0; implementation_name == "cpython" in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from web3>=4.8.2->karl) (0.9.0.1) | |
| Requirement already satisfied: lru-dict<2.0.0,>=1.1.6 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from web3>=4.8.2->karl) (1.1.6) | |
| Requirement already satisfied: humanfriendly>=4.7 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from coloredlogs>=10.0->mythril>=0.19.1->karl) (4.17) | |
| Requirement already satisfied: idna<2.8,>=2.5 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from requests->mythril>=0.19.1->karl) (2.7) | |
| Requirement already satisfied: certifi>=2017.4.17 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from requests->mythril>=0.19.1->karl) (2018.11.29) | |
| Requirement already satisfied: chardet<3.1.0,>=3.0.2 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from requests->mythril>=0.19.1->karl) (3.0.4) | |
| Requirement already satisfied: urllib3<1.25,>=1.21.1 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from requests->mythril>=0.19.1->karl) (1.24.1) | |
| Requirement already satisfied: pycryptodome<4.0.0,>=3.4.7 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from eth-keyfile>=0.5.1->mythril>=0.19.1->karl) (3.7.2) | |
| Requirement already satisfied: semantic-version<3.0.0,>=2.6.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from eth-tester>=0.1.0b21->mythril>=0.19.1->karl) (2.6.0) | |
| Requirement already satisfied: zope.interface in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from transaction>=2.2.1->mythril>=0.19.1->karl) (4.6.0) | |
| Requirement already satisfied: parsimonious<0.9.0,>=0.8.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from eth-abi>=1.0.0->mythril>=0.19.1->karl) (0.8.1) | |
| Requirement already satisfied: pbkdf2 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from ethereum>=2.3.2->mythril>=0.19.1->karl) (1.3) | |
| Requirement already satisfied: pysha3>=1.0.1 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from ethereum>=2.3.2->mythril>=0.19.1->karl) (1.0.2) | |
| Requirement already satisfied: py-ecc in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from ethereum>=2.3.2->mythril>=0.19.1->karl) (1.4.3) | |
| Requirement already satisfied: scrypt in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from ethereum>=2.3.2->mythril>=0.19.1->karl) (0.8.6) | |
| Requirement already satisfied: repoze.lru in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from ethereum>=2.3.2->mythril>=0.19.1->karl) (0.7) | |
| Requirement already satisfied: coincurve>=7.0.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from ethereum>=2.3.2->mythril>=0.19.1->karl) (10.0.0) | |
| Requirement already satisfied: future in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from ethereum>=2.3.2->mythril>=0.19.1->karl) (0.17.1) | |
| Requirement already satisfied: pyethash<1.0.0,>=0.1.27 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from ethereum>=2.3.2->mythril>=0.19.1->karl) (0.1.27) | |
| Requirement already satisfied: PyYAML in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from ethereum>=2.3.2->mythril>=0.19.1->karl) (3.13) | |
| Requirement already satisfied: attrdict<3,>=2.0.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from eth-account>=0.1.0a2->mythril>=0.19.1->karl) (2.0.0) | |
| Collecting dictionaries==0.0.1 (from py-flags->mythril>=0.19.1->karl) | |
| Downloading https://files.pythonhosted.org/packages/4d/54/b45e79bcfb116b7f946cb91f3955618b01a1f80dc0ee85da0d68fcc5f318/dictionaries-0.0.1-py2.py3-none-any.whl | |
| Collecting MarkupSafe>=0.23 (from jinja2>=2.9->mythril>=0.19.1->karl) | |
| Downloading https://files.pythonhosted.org/packages/96/52/eef455862764cb6d6c136aa52c7f9fc4e7c1c644790a7107b1244a2b8a53/MarkupSafe-1.1.0-cp37-cp37m-macosx_10_6_intel.whl | |
| Collecting pbr>=0.11 (from mock->mythril>=0.19.1->karl) | |
| Downloading https://files.pythonhosted.org/packages/f3/04/fddc1c2dd75b256eda4d360024692231a2c19a0c61ad7f4a162407c1ab58/pbr-5.1.1-py2.py3-none-any.whl (106kB) | |
| 100% |████████████████████████████████| 112kB 30.1MB/s | |
| Requirement already satisfied: six>=1.9 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from mock->mythril>=0.19.1->karl) (1.11.0) | |
| Requirement already satisfied: toolz>=0.8.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from cytoolz<1.0.0,>=0.9.0; implementation_name == "cpython"->web3>=4.8.2->karl) (0.9.0) | |
| Requirement already satisfied: setuptools in /usr/local/lib/python3.7/site-packages (from zope.interface->transaction>=2.2.1->mythril>=0.19.1->karl) (40.5.0) | |
| Requirement already satisfied: asn1crypto in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from coincurve>=7.0.0->ethereum>=2.3.2->mythril>=0.19.1->karl) (0.24.0) | |
| Requirement already satisfied: cffi>=1.3.0 in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from coincurve>=7.0.0->ethereum>=2.3.2->mythril>=0.19.1->karl) (1.11.5) | |
| Requirement already satisfied: pycparser in /Users/tim.siwula/Library/Python/3.7/lib/python/site-packages (from cffi>=1.3.0->coincurve>=7.0.0->ethereum>=2.3.2->mythril>=0.19.1->karl) (2.19) | |
| Installing collected packages: z3-solver, transaction, py-solc, dictionaries, py-flags, MarkupSafe, jinja2, pbr, mock, mythril, karl | |
| Running setup.py install for z3-solver ... error | |
| Complete output from command /usr/local/opt/python/bin/python3.7 -u -c "import setuptools, tokenize;__file__='/private/tmp/pip-install-am0j8884/z3-solver/setup.py';f=getattr(tokenize, 'open', open)(__file__);code=f.read().replace('\r\n', '\n');f.close();exec(compile(code, __file__, 'exec'))" install --record /private/tmp/pip-record-5clbyaoq/install-record.txt --single-version-externally-managed --compile --user --prefix=: | |
| running install | |
| running build | |
| Configuring Z3 | |
| Configured with: --prefix=/Applications/Xcode.app/Contents/Developer/usr --with-gxx-include-dir=/usr/include/c++/4.2.1 | |
| New component: 'util' | |
| New component: 'polynomial' | |
| New component: 'sat' | |
| New component: 'nlsat' | |
| New component: 'lp' | |
| New component: 'hilbert' | |
| New component: 'simplex' | |
| New component: 'automata' | |
| New component: 'interval' | |
| New component: 'realclosure' | |
| New component: 'subpaving' | |
| New component: 'ast' | |
| New component: 'rewriter' | |
| New component: 'macros' | |
| New component: 'normal_forms' | |
| New component: 'model' | |
| New component: 'tactic' | |
| New component: 'substitution' | |
| New component: 'parser_util' | |
| New component: 'grobner' | |
| New component: 'euclid' | |
| New component: 'core_tactics' | |
| New component: 'proofs' | |
| New component: 'solver' | |
| New component: 'sat_tactic' | |
| New component: 'arith_tactics' | |
| New component: 'nlsat_tactic' | |
| New component: 'subpaving_tactic' | |
| New component: 'aig_tactic' | |
| New component: 'ackermannization' | |
| New component: 'cmd_context' | |
| New component: 'smt2parser' | |
| New component: 'fpa' | |
| New component: 'pattern' | |
| New component: 'bit_blaster' | |
| New component: 'smt_params' | |
| New component: 'proto_model' | |
| New component: 'smt' | |
| New component: 'bv_tactics' | |
| New component: 'fuzzing' | |
| New component: 'smt_tactic' | |
| New component: 'sls_tactic' | |
| New component: 'qe' | |
| New component: 'muz' | |
| New component: 'dataflow' | |
| New component: 'transforms' | |
| New component: 'rel' | |
| New component: 'spacer' | |
| New component: 'clp' | |
| New component: 'tab' | |
| New component: 'bmc' | |
| New component: 'ddnf' | |
| New component: 'fp' | |
| New component: 'ufbv_tactic' | |
| New component: 'sat_solver' | |
| New component: 'smtlogic_tactics' | |
| New component: 'fpa_tactics' | |
| New component: 'portfolio' | |
| New component: 'opt' | |
| New component: 'api' | |
| New component: 'extra_cmds' | |
| New component: 'shell' | |
| New component: 'test' | |
| New component: 'api_dll' | |
| New component: 'dotnet' | |
| New component: 'java' | |
| New component: 'ml' | |
| New component: 'cpp' | |
| Python bindings directory was detected. | |
| New component: 'python' | |
| New component: 'python_install' | |
| New component: 'cpp_example' | |
| New component: 'z3_tptp' | |
| New component: 'c_example' | |
| New component: 'maxsat' | |
| New component: 'dotnet_example' | |
| New component: 'java_example' | |
| New component: 'ml_example' | |
| New component: 'py_example' | |
| Generating src/util/version.h from src/util/version.h.in | |
| Generated 'src/util/version.h' | |
| Generating src/api/dotnet/Properties/AssemblyInfo.cs from src/api/dotnet/Properties/AssemblyInfo.cs.in | |
| Generated 'src/tactic/smtlogics/qfufbv_tactic_params.hpp' | |
| Generated 'src/tactic/sls/sls_params.hpp' | |
| Generated 'src/parsers/util/parser_params.hpp' | |
| Generated 'src/util/lp/lp_params.hpp' | |
| Generated 'src/smt/params/smt_params_helper.hpp' | |
| Generated 'src/nlsat/nlsat_params.hpp' | |
| Generated 'src/solver/parallel_params.hpp' | |
| Generated 'src/solver/combined_solver_params.hpp' | |
| Generated 'src/math/realclosure/rcf_params.hpp' | |
| Generated 'src/math/polynomial/algebraic_params.hpp' | |
| Generated 'src/sat/sat_scc_params.hpp' | |
| Generated 'src/sat/sat_simplifier_params.hpp' | |
| Generated 'src/sat/sat_asymm_branch_params.hpp' | |
| Generated 'src/sat/sat_params.hpp' | |
| Generated 'src/model/model_params.hpp' | |
| Generated 'src/model/model_evaluator_params.hpp' | |
| Generated 'src/muz/base/fp_params.hpp' | |
| Generated 'src/ast/pp_params.hpp' | |
| Generated 'src/ast/rewriter/bool_rewriter_params.hpp' | |
| Generated 'src/ast/rewriter/poly_rewriter_params.hpp' | |
| Generated 'src/ast/rewriter/fpa_rewriter_params.hpp' | |
| Generated 'src/ast/rewriter/arith_rewriter_params.hpp' | |
| Generated 'src/ast/rewriter/bv_rewriter_params.hpp' | |
| Generated 'src/ast/rewriter/array_rewriter_params.hpp' | |
| Generated 'src/ast/rewriter/rewriter_params.hpp' | |
| Generated 'src/ast/normal_forms/nnf_params.hpp' | |
| Generated 'src/ast/pattern/pattern_inference_params_helper.hpp' | |
| Generated 'src/ast/fpa/fpa2bv_rewriter_params.hpp' | |
| Generated 'src/opt/opt_params.hpp' | |
| Generated 'src/ackermannization/ackermannization_params.hpp' | |
| Generated 'src/ackermannization/ackermannize_bv_tactic_params.hpp' | |
| Generated 'src/ast/pattern/database.h' | |
| Component api | |
| Component portfolio | |
| Component smtlogic_tactics | |
| Component ackermannization | |
| Component model | |
| Component rewriter | |
| Component ast | |
| Component util | |
| Component polynomial | |
| Component automata | |
| Component solver | |
| Component tactic | |
| Component proofs | |
| Component sat_solver | |
| Component core_tactics | |
| Component macros | |
| Component normal_forms | |
| Component aig_tactic | |
| Component bv_tactics | |
| Component bit_blaster | |
| Component arith_tactics | |
| Component sat | |
| Component sat_tactic | |
| Component nlsat_tactic | |
| Component nlsat | |
| Component smt_tactic | |
| Component smt | |
| Component cmd_context | |
| Component proto_model | |
| Component smt_params | |
| Component pattern | |
| Component smt2parser | |
| Component parser_util | |
| Component substitution | |
| Component grobner | |
| Component euclid | |
| Component simplex | |
| Component fpa | |
| Component lp | |
| Component fp | |
| Component muz | |
| Component qe | |
| Component clp | |
| Component transforms | |
| Component hilbert | |
| Component dataflow | |
| Component tab | |
| Component rel | |
| Component bmc | |
| Component ddnf | |
| Component spacer | |
| Component ufbv_tactic | |
| Component fpa_tactics | |
| Component sls_tactic | |
| Component subpaving_tactic | |
| Component subpaving | |
| Component interval | |
| Component realclosure | |
| Component opt | |
| Component extra_cmds | |
| Component shell | |
| Generated 'src/shell/install_tactic.cpp' | |
| Component api | |
| Component portfolio | |
| Component smtlogic_tactics | |
| Component ackermannization | |
| Component model | |
| Component rewriter | |
| Component ast | |
| Component util | |
| Component polynomial | |
| Component automata | |
| Component solver | |
| Component tactic | |
| Component proofs | |
| Component sat_solver | |
| Component core_tactics | |
| Component macros | |
| Component normal_forms | |
| Component aig_tactic | |
| Component bv_tactics | |
| Component bit_blaster | |
| Component arith_tactics | |
| Component sat | |
| Component sat_tactic | |
| Component nlsat_tactic | |
| Component nlsat | |
| Component smt_tactic | |
| Component smt | |
| Component cmd_context | |
| Component proto_model | |
| Component smt_params | |
| Component pattern | |
| Component smt2parser | |
| Component parser_util | |
| Component substitution | |
| Component grobner | |
| Component euclid | |
| Component simplex | |
| Component fpa | |
| Component lp | |
| Component fp | |
| Component muz | |
| Component qe | |
| Component clp | |
| Component transforms | |
| Component hilbert | |
| Component dataflow | |
| Component tab | |
| Component rel | |
| Component bmc | |
| Component ddnf | |
| Component spacer | |
| Component ufbv_tactic | |
| Component fpa_tactics | |
| Component sls_tactic | |
| Component subpaving_tactic | |
| Component subpaving | |
| Component interval | |
| Component realclosure | |
| Component opt | |
| Component fuzzing | |
| Component test | |
| Generated 'src/test/install_tactic.cpp' | |
| Component api | |
| Component portfolio | |
| Component smtlogic_tactics | |
| Component ackermannization | |
| Component model | |
| Component rewriter | |
| Component ast | |
| Component util | |
| Component polynomial | |
| Component automata | |
| Component solver | |
| Component tactic | |
| Component proofs | |
| Component sat_solver | |
| Component core_tactics | |
| Component macros | |
| Component normal_forms | |
| Component aig_tactic | |
| Component bv_tactics | |
| Component bit_blaster | |
| Component arith_tactics | |
| Component sat | |
| Component sat_tactic | |
| Component nlsat_tactic | |
| Component nlsat | |
| Component smt_tactic | |
| Component smt | |
| Component cmd_context | |
| Component proto_model | |
| Component smt_params | |
| Component pattern | |
| Component smt2parser | |
| Component parser_util | |
| Component substitution | |
| Component grobner | |
| Component euclid | |
| Component simplex | |
| Component fpa | |
| Component lp | |
| Component fp | |
| Component muz | |
| Component qe | |
| Component clp | |
| Component transforms | |
| Component hilbert | |
| Component dataflow | |
| Component tab | |
| Component rel | |
| Component bmc | |
| Component ddnf | |
| Component spacer | |
| Component ufbv_tactic | |
| Component fpa_tactics | |
| Component sls_tactic | |
| Component subpaving_tactic | |
| Component subpaving | |
| Component interval | |
| Component realclosure | |
| Component opt | |
| Component extra_cmds | |
| Component api_dll | |
| Generated 'src/api/dll/install_tactic.cpp' | |
| Generated 'src/shell/mem_initializer.cpp' | |
| Generated 'src/test/mem_initializer.cpp' | |
| Generated 'src/api/dll/mem_initializer.cpp' | |
| Generated 'src/shell/gparams_register_modules.cpp' | |
| Generated 'src/test/gparams_register_modules.cpp' | |
| Generated 'src/api/dll/gparams_register_modules.cpp' | |
| Generated 'src/api/python/z3/z3consts.py | |
| Generated 'src/api/api_log_macros.h' | |
| Generated 'src/api/api_log_macros.cpp' | |
| Generated 'src/api/api_commands.cpp' | |
| Generated 'src/api/python/z3/z3core.py' | |
| Listing 'src/api/python/z3'... | |
| Compiling 'src/api/python/z3/z3consts.py'... | |
| Compiling 'src/api/python/z3/z3core.py'... | |
| Generated python bytecode | |
| Copied 'z3consts.py' | |
| Copied 'z3core.py' | |
| Copied 'z3core.cpython-37.pyc' | |
| Copied 'z3consts.cpython-37.pyc' | |
| Testing ar... | |
| Testing g++... | |
| Testing gcc... | |
| Testing floating point support... | |
| Testing OpenMP... | |
| Host platform: Darwin | |
| C++ Compiler: g++ | |
| C Compiler : gcc | |
| Archive Tool: ar | |
| Arithmetic: internal | |
| OpenMP: False | |
| Prefix: /usr/local | |
| 64-bit: True | |
| FP math: SSE2-GCC | |
| Python pkg dir: /usr/local/Cellar/python/3.7.1/Frameworks/Python.framework/Versions/3.7/lib/python3.7/site-packages | |
| Python version: 3.7 | |
| Writing build/Makefile | |
| Copied Z3Py example 'all_interval_series.py' to 'build/python' | |
| Copied Z3Py example 'visitor.py' to 'build/python' | |
| Copied Z3Py example 'example.py' to 'build/python' | |
| Copied Z3Py example 'socrates.py' to 'build/python' | |
| Copied Z3Py example 'parallel.py' to 'build/python' | |
| Makefile was successfully generated. | |
| compilation mode: Release | |
| Type 'cd build; make' to build Z3 | |
| Building Z3 | |
| src/smt/smt_statistics.cpp | |
| src/util/common_msgs.cpp | |
| src/util/luby.cpp | |
| src/util/approx_nat.cpp | |
| src/api/dll/dll.cpp | |
| src/util/cooperate.cpp | |
| src/util/timeit.cpp | |
| src/util/memory_manager.cpp | |
| src/util/z3_exception.cpp | |
| src/api/api_commands.cpp | |
| src/util/page.cpp | |
| src/util/util.cpp | |
| src/util/approx_set.cpp | |
| src/util/scoped_ctrl_c.cpp | |
| src/util/timer.cpp | |
| src/util/bit_util.cpp | |
| src/util/stack.cpp | |
| src/util/scoped_timer.cpp | |
| src/util/lbool.cpp | |
| src/util/timeout.cpp | |
| src/shell/z3_log_frontend.cpp | |
| src/api/api_log.cpp | |
| src/util/fixed_bit_vector.cpp | |
| src/util/mpn.cpp | |
| src/util/hash.cpp | |
| src/solver/smt_logics.cpp | |
| src/util/prime_generator.cpp | |
| src/util/small_object_allocator.cpp | |
| src/util/min_cut.cpp | |
| src/util/smt2_util.cpp | |
| src/util/warning.cpp | |
| src/util/permutation.cpp | |
| src/api/api_log_macros.cpp | |
| src/math/automata/automaton.cpp | |
| src/util/symbol.cpp | |
| src/util/trace.cpp | |
| src/util/rlimit.cpp | |
| src/util/cmd_context_types.cpp | |
| src/util/debug.cpp | |
| src/util/region.cpp | |
| src/util/bit_vector.cpp | |
| src/api/z3_replayer.cpp | |
| src/sat/sat_par.cpp | |
| src/util/statistics.cpp | |
| src/util/mpz.cpp | |
| src/smt/params/theory_array_params.cpp | |
| src/smt/params/preprocessor_params.cpp | |
| src/smt/params/theory_pb_params.cpp | |
| src/smt/params/theory_str_params.cpp | |
| src/smt/params/theory_bv_params.cpp | |
| src/smt/params/theory_seq_params.cpp | |
| src/smt/params/qi_params.cpp | |
| src/smt/params/theory_arith_params.cpp | |
| src/smt/params/dyn_ack_params.cpp | |
| src/ast/pattern/pattern_inference_params.cpp | |
| src/math/euclid/euclidean_solver.cpp | |
| src/math/realclosure/mpz_matrix.cpp | |
| src/math/interval/interval_mpq.cpp | |
| src/sat/sat_clause.cpp | |
| src/sat/sat_watched.cpp | |
| src/sat/sat_bdd.cpp | |
| src/sat/sat_config.cpp | |
| src/sat/sat_clause_use_list.cpp | |
| src/util/mpq.cpp | |
| src/util/mpf.cpp | |
| src/util/hwf.cpp | |
| src/util/mpff.cpp | |
| src/util/env_params.cpp | |
| src/util/gparams.cpp | |
| src/util/mpq_inf.cpp | |
| src/util/mpfx.cpp | |
| src/shell/mem_initializer.cpp | |
| src/muz/rel/tbv.cpp | |
| src/muz/base/bind_variables.cpp | |
| src/smt/smt_quantifier_stat.cpp | |
| src/smt/old_interval.cpp | |
| src/smt/proto_model/value_factory.cpp | |
| src/smt/params/smt_params.cpp | |
| src/tactic/arith/linear_equation.cpp | |
| src/ast/expr_map.cpp | |
| src/ast/ast_util.cpp | |
| src/ast/used_vars.cpp | |
| src/ast/num_occurs.cpp | |
| src/ast/for_each_ast.cpp | |
| src/ast/ast_lt.cpp | |
| src/ast/has_free_vars.cpp | |
| src/ast/act_cache.cpp | |
| src/math/subpaving/subpaving.cpp | |
| src/math/subpaving/subpaving_mpff.cpp | |
| src/math/subpaving/subpaving_hwf.cpp | |
| src/math/subpaving/subpaving_mpf.cpp | |
| src/math/subpaving/subpaving_mpq.cpp | |
| src/sat/sat_clause_set.cpp | |
| src/util/rational.cpp | |
| src/util/sexpr.cpp | |
| src/util/s_integer.cpp | |
| src/util/inf_rational.cpp | |
| src/util/inf_int_rational.cpp | |
| src/util/params.cpp | |
| src/api/dll/mem_initializer.cpp | |
| src/api/dll/gparams_register_modules.cpp | |
| src/shell/gparams_register_modules.cpp | |
| src/muz/spacer/spacer_matrix.cpp | |
| src/smt/smt_value_sort.cpp | |
| src/smt/arith_eq_solver.cpp | |
| src/smt/uses_theory.cpp | |
| src/cmd_context/tactic_manager.cpp | |
| src/ackermannization/ackr_helper.cpp | |
| src/math/subpaving/tactic/expr2subpaving.cpp | |
| src/tactic/arith/bound_propagator.cpp | |
| src/parsers/util/simple_parser.cpp | |
| src/parsers/util/cost_parser.cpp | |
| src/parsers/util/scanner.cpp | |
| src/ast/rewriter/distribute_forall.cpp | |
| src/ast/rewriter/datatype_rewriter.cpp | |
| src/ast/rewriter/mk_extract_proc.cpp | |
| src/ast/expr_functors.cpp | |
| src/ast/expr_stat.cpp | |
| src/ast/fpa_decl_plugin.cpp | |
| src/ast/func_decl_dependencies.cpp | |
| src/ast/format.cpp | |
| src/ast/pp.cpp | |
| src/ast/macro_substitution.cpp | |
| src/ast/for_each_expr.cpp | |
| src/ast/ast_ll_pp.cpp | |
| src/ast/ast_smt_pp.cpp | |
| src/ast/occurs.cpp | |
| src/ast/reg_decl_plugins.cpp | |
| src/math/subpaving/subpaving_mpfx.cpp | |
| src/math/realclosure/realclosure.cpp | |
| src/math/simplex/simplex.cpp | |
| src/math/hilbert/hilbert_basis.cpp | |
| src/util/inf_s_integer.cpp | |
| src/util/mpbq.cpp | |
| src/shell/main.cpp | |
| src/qe/qe_solve_plugin.cpp | |
| src/smt/smt_literal.cpp | |
| src/smt/smt_farkas_util.cpp | |
| src/smt/cost_evaluator.cpp | |
| src/smt/fingerprints.cpp | |
| src/smt/elim_term_ite.cpp | |
| src/smt/proto_model/numeral_factory.cpp | |
| src/ast/pattern/pattern_inference.cpp | |
| src/ast/fpa/bv2fpa_converter.cpp | |
| src/ast/fpa/fpa2bv_rewriter.cpp | |
| src/ast/fpa/fpa2bv_converter.cpp | |
| src/cmd_context/pdecl.cpp | |
| src/cmd_context/check_logic.cpp | |
| src/tactic/arith/bv2real_rewriter.cpp | |
| src/ast/proofs/proof_checker.cpp | |
| src/ast/proofs/proof_utils.cpp | |
| src/math/grobner/grobner.cpp | |
| src/parsers/util/pattern_validation.cpp | |
| src/tactic/equiv_proof_converter.cpp | |
| src/tactic/replace_proof_converter.cpp | |
| src/model/model_pp.cpp | |
| src/model/model_v2_pp.cpp | |
| src/model/model_core.cpp | |
| src/model/func_interp.cpp | |
| src/ast/normal_forms/nnf.cpp | |
| src/ast/normal_forms/defined_names.cpp | |
| src/ast/normal_forms/pull_quant.cpp | |
| src/ast/normal_forms/name_exprs.cpp | |
| src/ast/rewriter/seq_rewriter.cpp | |
| src/ast/rewriter/bv_bounds.cpp | |
| src/ast/rewriter/elim_bounds.cpp | |
| src/ast/rewriter/factor_equivs.cpp | |
| src/ast/rewriter/bv_trailing.cpp | |
| src/ast/rewriter/maximize_ac_sharing.cpp | |
| src/ast/rewriter/factor_rewriter.cpp | |
| src/ast/rewriter/pb2bv_rewriter.cpp | |
| src/ast/rewriter/label_rewriter.cpp | |
| src/ast/rewriter/push_app_ite.cpp | |
| src/ast/rewriter/ast_counter.cpp | |
| src/ast/rewriter/var_subst.cpp | |
| src/ast/rewriter/array_rewriter.cpp | |
| src/ast/rewriter/bv_elim.cpp | |
| src/ast/rewriter/fpa_rewriter.cpp | |
| src/ast/rewriter/der.cpp | |
| src/ast/rewriter/dl_rewriter.cpp | |
| src/ast/rewriter/enum2bv_rewriter.cpp | |
| src/ast/rewriter/quant_hoist.cpp | |
| src/ast/rewriter/expr_replacer.cpp | |
| src/ast/rewriter/pb_rewriter.cpp | |
| src/ast/rewriter/rewriter.cpp | |
| src/ast/rewriter/bool_rewriter.cpp | |
| src/ast/rewriter/expr_safe_replace.cpp | |
| src/ast/rewriter/inj_axiom.cpp | |
| src/ast/shared_occs.cpp | |
| src/ast/array_decl_plugin.cpp | |
| src/ast/seq_decl_plugin.cpp | |
| src/ast/static_features.cpp | |
| src/ast/expr_abstract.cpp | |
| src/ast/pb_decl_plugin.cpp | |
| src/ast/ast.cpp | |
| src/ast/well_sorted.cpp | |
| src/ast/dl_decl_plugin.cpp | |
| src/ast/decl_collector.cpp | |
| src/ast/ast_translation.cpp | |
| src/ast/expr_substitution.cpp | |
| src/ast/expr2var.cpp | |
| src/ast/datatype_decl_plugin.cpp | |
| src/ast/ast_pp_dot.cpp | |
| src/ast/bv_decl_plugin.cpp | |
| src/math/simplex/model_based_opt.cpp | |
| src/util/lp/lp_utils.cpp | |
| src/sat/sat_scc.cpp | |
| src/sat/sat_elim_eqs.cpp | |
| src/sat/sat_lookahead.cpp | |
| src/sat/sat_elim_vars.cpp | |
| src/sat/sat_parallel.cpp | |
| src/sat/sat_drat.cpp | |
| src/sat/sat_simplifier.cpp | |
| src/sat/sat_unit_walk.cpp | |
| src/sat/sat_probing.cpp | |
| src/sat/sat_solver.cpp | |
| src/sat/sat_cleaner.cpp | |
| src/sat/sat_iff3_finder.cpp | |
| src/sat/sat_mus.cpp | |
| src/sat/sat_big.cpp | |
| src/sat/sat_asymm_branch.cpp | |
| src/sat/sat_model_converter.cpp | |
| src/sat/dimacs.cpp | |
| src/sat/sat_integrity_checker.cpp | |
| src/shell/dimacs_frontend.cpp | |
| src/muz/spacer/spacer_mev_array.cpp | |
| src/muz/spacer/spacer_antiunify.cpp | |
| src/muz/rel/doc.cpp | |
| src/qe/qe_array_plugin.cpp | |
| src/qe/nlarith_util.cpp | |
| src/qe/qe_dl_plugin.cpp | |
| src/qe/qe_bv_plugin.cpp | |
| src/qe/qe_datatype_plugin.cpp | |
| src/qe/qe_bool_plugin.cpp | |
| src/qe/qe_term_graph.cpp | |
| src/smt/watch_list.cpp | |
| src/smt/smt_clause.cpp | |
| src/smt/theory_opt.cpp | |
| src/smt/smt_cg_table.cpp | |
| src/smt/smt_almost_cg_table.cpp | |
| src/smt/cached_var_subst.cpp | |
| src/smt/expr_context_simplifier.cpp | |
| src/smt/proto_model/array_factory.cpp | |
| src/smt/proto_model/proto_model.cpp | |
| src/smt/proto_model/struct_factory.cpp | |
| src/smt/proto_model/datatype_factory.cpp | |
| src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp | |
| src/ast/rewriter/bit_blaster/bit_blaster.cpp | |
| src/ast/substitution/unifier.cpp | |
| src/ast/substitution/matcher.cpp | |
| src/ast/substitution/substitution_tree.cpp | |
| src/ast/substitution/substitution.cpp | |
| src/model/model2expr.cpp | |
| src/model/model_evaluator.cpp | |
| src/model/model_implicant.cpp | |
| src/model/model.cpp | |
| src/model/model_smt2_pp.cpp | |
| src/ast/rewriter/arith_rewriter.cpp | |
| src/ast/rewriter/mk_simplified_app.cpp | |
| src/ast/rewriter/bv_rewriter.cpp | |
| src/ast/rewriter/th_rewriter.cpp | |
| src/ast/ast_smt2_pp.cpp | |
| src/ast/ast_pp_util.cpp | |
| src/ast/expr2polynomial.cpp | |
| src/ast/arith_decl_plugin.cpp | |
| src/ast/ast_printer.cpp | |
| src/sat/sat_local_search.cpp | |
| src/sat/ba_solver.cpp | |
| src/math/polynomial/polynomial_cache.cpp | |
| src/opt/pb_sls.cpp | |
| src/tactic/ufbv/ufbv_rewriter.cpp | |
| src/muz/spacer/spacer_mbc.cpp | |
| src/muz/spacer/spacer_sem_matcher.cpp | |
| src/muz/spacer/spacer_iuc_proof.cpp | |
| src/muz/spacer/spacer_sym_mux.cpp | |
| src/muz/spacer/spacer_qe_project.cpp | |
| src/muz/base/dl_boogie_proof.cpp | |
| src/qe/qe_arith.cpp | |
| src/qe/qe_arith_plugin.cpp | |
| src/tactic/bv/bit_blaster_model_converter.cpp | |
| src/ackermannization/lackr_model_constructor.cpp | |
| src/ackermannization/ackr_model_converter.cpp | |
| src/ackermannization/ackermannize_bv_model_converter.cpp | |
| src/solver/check_sat_result.cpp | |
| src/tactic/generic_model_converter.cpp | |
| src/tactic/model_converter.cpp | |
| src/tactic/horn_subsume_model_converter.cpp | |
| src/ast/macros/macro_util.cpp | |
| src/ast/rewriter/bit2int.cpp | |
| src/util/lp/lp_settings.cpp | |
| src/util/lp/binary_heap_priority_queue.cpp | |
| src/nlsat/nlsat_interval_set.cpp | |
| src/nlsat/nlsat_types.cpp | |
| src/math/polynomial/rpolynomial.cpp | |
| src/math/polynomial/polynomial.cpp | |
| src/math/polynomial/sexpr2upolynomial.cpp | |
| src/tactic/fpa/fpa2bv_model_converter.cpp | |
| src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp | |
| src/muz/spacer/spacer_proof_utils.cpp | |
| src/muz/spacer/spacer_unsat_core_plugin.cpp | |
| src/muz/spacer/spacer_unsat_core_learner.cpp | |
| src/muz/spacer/spacer_farkas_learner.cpp | |
| src/muz/base/hnf.cpp | |
| src/qe/qe_mbi.cpp | |
| src/qe/qe_arrays.cpp | |
| src/qe/qe_datatypes.cpp | |
| src/qe/qe_mbp.cpp | |
| src/tactic/bv/bvarray2uf_rewriter.cpp | |
| src/smt/smt_implied_equalities.cpp | |
| src/cmd_context/context_params.cpp | |
| src/ackermannization/lackr_model_converter_lazy.cpp | |
| src/tactic/aig/aig.cpp | |
| src/tactic/arith/bv2int_rewriter.cpp | |
| src/tactic/arith/bound_manager.cpp | |
| src/tactic/arith/pb2bv_model_converter.cpp | |
| src/sat/tactic/atom2bool_var.cpp | |
| src/solver/combined_solver.cpp | |
| src/solver/mus.cpp | |
| src/solver/solver.cpp | |
| src/tactic/core/collect_occs.cpp | |
| src/tactic/dependency_converter.cpp | |
| src/tactic/proof_converter.cpp | |
| src/tactic/goal_shared_occs.cpp | |
| src/tactic/goal.cpp | |
| src/tactic/goal_num_occurs.cpp | |
| src/tactic/goal_util.cpp | |
| src/ast/macros/macro_manager.cpp | |
| src/ast/macros/quasi_macros.cpp | |
| src/util/lp/binary_heap_upair_queue.cpp | |
| src/util/lp/dense_matrix.cpp | |
| src/util/lp/indexed_vector.cpp | |
| src/nlsat/nlsat_clause.cpp | |
| src/math/polynomial/upolynomial.cpp | |
| src/math/polynomial/algebraic_numbers.cpp | |
| src/cmd_context/extra_cmds/dbg_cmds.cpp | |
| src/cmd_context/extra_cmds/subpaving_cmds.cpp | |
| src/cmd_context/extra_cmds/polynomial_cmds.cpp | |
| src/opt/opt_pareto.cpp | |
| src/tactic/portfolio/solver2lookahead.cpp | |
| src/tactic/portfolio/bounded_int2bv_solver.cpp | |
| src/tactic/portfolio/enum2bv_solver.cpp | |
| src/tactic/portfolio/smt_strategic_solver.cpp | |
| src/tactic/portfolio/pb2bv_solver.cpp | |
| src/muz/spacer/spacer_iuc_solver.cpp | |
| src/muz/spacer/spacer_manager.cpp | |
| src/muz/spacer/spacer_legacy_mbp.cpp | |
| src/muz/spacer/spacer_legacy_mev.cpp | |
| src/qe/qe_sat_tactic.cpp | |
| src/qe/qsat.cpp | |
| src/qe/qe_cmd.cpp | |
| src/tactic/sls/sls_engine.cpp | |
| src/smt/smt_solver.cpp | |
| src/smt/smt2_extra_cmds.cpp | |
| src/ast/pattern/expr_pattern_match.cpp | |
| src/parsers/smt2/marshal.cpp | |
| src/parsers/smt2/smt2parser.cpp | |
| src/cmd_context/cmd_context.cpp | |
| src/cmd_context/parametric_cmd.cpp | |
| src/cmd_context/basic_cmds.cpp | |
| src/cmd_context/echo_tactic.cpp | |
| src/cmd_context/simplify_cmd.cpp | |
| src/cmd_context/eval_cmd.cpp | |
| src/cmd_context/cmd_util.cpp | |
| src/cmd_context/cmd_context_to_goal.cpp | |
| src/ackermannization/lackr.cpp | |
| src/nlsat/tactic/goal2nlsat.cpp | |
| src/tactic/arith/arith_bounds_tactic.cpp | |
| src/tactic/arith/probe_arith.cpp | |
| src/sat/tactic/goal2sat.cpp | |
| src/solver/solver_na2as.cpp | |
| src/solver/tactic2solver.cpp | |
| src/solver/solver2tactic.cpp | |
| src/solver/solver_pool.cpp | |
| src/tactic/core/reduce_invertible_tactic.cpp | |
| src/tactic/core/cofactor_elim_term_ite.cpp | |
| src/tactic/probe.cpp | |
| src/tactic/tactic.cpp | |
| src/ast/macros/macro_finder.cpp | |
| src/nlsat/nlsat_evaluator.cpp | |
| src/nlsat/nlsat_explain.cpp | |
| src/nlsat/nlsat_solver.cpp | |
| src/math/polynomial/upolynomial_factorization.cpp | |
| src/api/api_array.cpp | |
| src/api/api_fpa.cpp | |
| src/api/api_arith.cpp | |
| src/api/api_datatype.cpp | |
| src/api/api_model.cpp | |
| src/api/api_ast_map.cpp | |
| src/api/api_ast_vector.cpp | |
| src/api/api_algebraic.cpp | |
| src/api/api_ast.cpp | |
| src/api/api_context.cpp | |
| src/api/api_qe.cpp | |
| src/api/api_pb.cpp | |
| src/api/api_polynomial.cpp | |
| src/api/api_goal.cpp | |
| src/api/api_rcf.cpp | |
| src/api/api_seq.cpp | |
| src/api/api_bv.cpp | |
| src/api/api_stats.cpp | |
| src/api/api_config_params.cpp | |
| src/api/api_solver.cpp | |
| src/api/api_quant.cpp | |
| src/api/api_params.cpp | |
| src/api/api_numeral.cpp | |
| src/api/api_parsers.cpp | |
| src/tactic/portfolio/default_tactic.cpp | |
| src/tactic/portfolio/fd_solver.cpp | |
| src/tactic/fpa/fpa2bv_tactic.cpp | |
| src/tactic/fpa/qffplra_tactic.cpp | |
| src/tactic/smtlogics/qflia_tactic.cpp | |
| src/tactic/smtlogics/qfauflia_tactic.cpp | |
| src/tactic/smtlogics/qfnra_tactic.cpp | |
| src/tactic/smtlogics/qfidl_tactic.cpp | |
| src/tactic/smtlogics/qfuf_tactic.cpp | |
| src/tactic/smtlogics/qflra_tactic.cpp | |
| src/tactic/smtlogics/quant_tactics.cpp | |
| src/tactic/smtlogics/qfnia_tactic.cpp | |
| src/tactic/smtlogics/qfaufbv_tactic.cpp | |
| src/tactic/smtlogics/nra_tactic.cpp | |
| src/sat/sat_solver/inc_sat_solver.cpp | |
| src/tactic/ufbv/ufbv_tactic.cpp | |
| src/tactic/ufbv/macro_finder_tactic.cpp | |
| src/tactic/ufbv/quasi_macros_tactic.cpp | |
| src/tactic/ufbv/ufbv_rewriter_tactic.cpp | |
| src/muz/spacer/spacer_prop_solver.cpp | |
| src/muz/spacer/spacer_util.cpp | |
| src/qe/nlqsat.cpp | |
| src/qe/qe_tactic.cpp | |
| src/qe/qe_lite.cpp | |
| src/tactic/sls/sls_tactic.cpp | |
| src/tactic/sls/bvsls_opt_engine.cpp | |
| src/smt/tactic/ctx_solver_simplify_tactic.cpp | |
| src/smt/tactic/smt_tactic.cpp | |
| src/tactic/bv/bv_size_reduction_tactic.cpp | |
| src/tactic/bv/bv_bounds_tactic.cpp | |
| src/tactic/bv/bvarray2uf_tactic.cpp | |
| src/tactic/bv/dt2bv_tactic.cpp | |
| src/tactic/bv/max_bv_sharing_tactic.cpp | |
| src/tactic/bv/elim_small_bv_tactic.cpp | |
| src/tactic/bv/bv1_blaster_tactic.cpp | |
| src/tactic/bv/bv_bound_chk_tactic.cpp | |
| src/tactic/bv/bit_blaster_tactic.cpp | |
| src/smt/asserted_formulas.cpp | |
| src/parsers/smt2/smt2scanner.cpp | |
| src/cmd_context/tactic_cmds.cpp | |
| src/ackermannization/ackr_bound_probe.cpp | |
| src/tactic/aig/aig_tactic.cpp | |
| src/math/subpaving/tactic/subpaving_tactic.cpp | |
| src/nlsat/tactic/nlsat_tactic.cpp | |
| src/nlsat/tactic/qfnra_nlsat_tactic.cpp | |
| src/tactic/arith/propagate_ineqs_tactic.cpp | |
| src/tactic/arith/recover_01_tactic.cpp | |
| src/tactic/arith/lia2card_tactic.cpp | |
| src/tactic/arith/lia2pb_tactic.cpp | |
| src/tactic/arith/factor_tactic.cpp | |
| src/tactic/arith/add_bounds_tactic.cpp | |
| src/tactic/arith/card2bv_tactic.cpp | |
| src/tactic/arith/fix_dl_var_tactic.cpp | |
| src/tactic/arith/diff_neq_tactic.cpp | |
| src/tactic/arith/nla2bv_tactic.cpp | |
| src/tactic/arith/degree_shift_tactic.cpp | |
| src/tactic/arith/eq2bv_tactic.cpp | |
| src/tactic/arith/pb2bv_tactic.cpp | |
| src/tactic/arith/purify_arith_tactic.cpp | |
| src/tactic/arith/normalize_bounds_tactic.cpp | |
| src/tactic/arith/fm_tactic.cpp | |
| src/sat/tactic/sat_tactic.cpp | |
| src/solver/parallel_tactic.cpp | |
| src/tactic/core/split_clause_tactic.cpp | |
| src/tactic/core/elim_term_ite_tactic.cpp | |
| src/tactic/core/occf_tactic.cpp | |
| src/tactic/core/collect_statistics_tactic.cpp | |
| src/tactic/core/elim_uncnstr_tactic.cpp | |
| src/tactic/core/der_tactic.cpp | |
| src/tactic/core/dom_simplify_tactic.cpp | |
| src/tactic/core/injectivity_tactic.cpp | |
| src/tactic/core/tseitin_cnf_tactic.cpp | |
| src/tactic/core/symmetry_reduce_tactic.cpp | |
| src/tactic/core/cofactor_term_ite_tactic.cpp | |
| src/tactic/core/distribute_forall_tactic.cpp | |
| src/tactic/core/propagate_values_tactic.cpp | |
| src/tactic/core/pb_preprocess_tactic.cpp | |
| src/tactic/core/ctx_simplify_tactic.cpp | |
| src/tactic/core/reduce_args_tactic.cpp | |
| src/tactic/core/blast_term_ite_tactic.cpp | |
| src/tactic/core/solve_eqs_tactic.cpp | |
| src/tactic/core/simplify_tactic.cpp | |
| src/tactic/core/nnf_tactic.cpp | |
| src/tactic/tactical.cpp | |
| src/tactic/sine_filter.cpp | |
| src/util/lp/matrix.cpp | |
| src/util/lp/permutation_matrix.cpp | |
| src/api/api_tactic.cpp | |
| src/tactic/fpa/qffp_tactic.cpp | |
| src/tactic/smtlogics/qfbv_tactic.cpp | |
| src/tactic/smtlogics/qfufbv_tactic.cpp | |
| src/muz/spacer/spacer_json.cpp | |
| src/muz/spacer/spacer_quant_generalizer.cpp | |
| src/muz/dataflow/dataflow.cpp | |
| src/qe/qe.cpp | |
| src/smt/tactic/unit_subsumption_tactic.cpp | |
| src/smt/arith_eq_adapter.cpp | |
| src/smt/theory_array_full.cpp | |
| src/smt/theory_wmaxsat.cpp | |
| src/smt/smt_justification.cpp | |
| src/smt/smt_quick_checker.cpp | |
| src/smt/smt_model_checker.cpp | |
| src/smt/dyn_ack.cpp | |
| src/smt/smt_internalizer.cpp | |
| src/smt/theory_dl.cpp | |
| src/smt/smt_context_inv.cpp | |
| src/smt/mam.cpp | |
| src/smt/smt_consequences.cpp | |
| src/smt/smt_checker.cpp | |
| src/smt/theory_array_base.cpp | |
| src/smt/smt_model_finder.cpp | |
| src/smt/smt_kernel.cpp | |
| src/smt/theory_seq.cpp | |
| src/smt/smt_model_generator.cpp | |
| src/smt/smt_enode.cpp | |
| src/smt/smt_case_split_queue.cpp | |
| src/smt/theory_bv.cpp | |
| src/smt/smt_relevancy.cpp | |
| src/smt/theory_fpa.cpp | |
| src/smt/theory_datatype.cpp | |
| src/smt/smt_quantifier.cpp | |
| src/smt/smt_theory.cpp | |
| src/smt/smt_context.cpp | |
| src/smt/qi_queue.cpp | |
| src/smt/theory_dummy.cpp | |
| src/smt/theory_str.cpp | |
| src/smt/theory_pb.cpp | |
| src/smt/smt_conflict_resolution.cpp | |
| src/smt/theory_array.cpp | |
| src/smt/smt_for_each_relevant_expr.cpp | |
| src/smt/smt_context_pp.cpp | |
| src/smt/smt_context_stat.cpp | |
| src/ackermannization/ackermannize_bv_tactic.cpp | |
| src/util/lp/eta_matrix.cpp | |
| src/util/lp/scaler.cpp | |
| src/api/dll/install_tactic.cpp | |
| src/shell/install_tactic.cpp | |
| src/opt/optsmt.cpp | |
| src/muz/fp/datalog_parser.cpp | |
| src/muz/ddnf/ddnf.cpp | |
| src/muz/clp/clp_context.cpp | |
| src/muz/spacer/spacer_generalizers.cpp | |
| src/muz/spacer/spacer_sat_answer.cpp | |
| src/muz/spacer/spacer_callback.cpp | |
| src/muz/spacer/spacer_pdr.cpp | |
| src/muz/transforms/dl_mk_coi_filter.cpp | |
| src/muz/transforms/dl_mk_quantifier_instantiation.cpp | |
| src/muz/transforms/dl_mk_scale.cpp | |
| src/muz/transforms/dl_mk_magic_symbolic.cpp | |
| src/muz/transforms/dl_mk_magic_sets.cpp | |
| src/muz/transforms/dl_mk_karr_invariants.cpp | |
| src/muz/transforms/dl_mk_array_instantiation.cpp | |
| src/muz/transforms/dl_mk_separate_negated_tails.cpp | |
| src/muz/transforms/dl_mk_loop_counter.cpp | |
| src/muz/transforms/dl_mk_unbound_compressor.cpp | |
| src/muz/transforms/dl_mk_quantifier_abstraction.cpp | |
| src/muz/transforms/dl_mk_backwards.cpp | |
| src/muz/transforms/dl_mk_filter_rules.cpp | |
| src/muz/transforms/dl_mk_bit_blast.cpp | |
| src/muz/transforms/dl_mk_array_eq_rewrite.cpp | |
| src/muz/base/dl_rule.cpp | |
| src/muz/base/dl_rule_transformer.cpp | |
| src/muz/base/dl_util.cpp | |
| src/muz/base/dl_context.cpp | |
| src/muz/base/dl_costs.cpp | |
| src/muz/base/rule_properties.cpp | |
| src/muz/base/dl_rule_subsumption_index.cpp | |
| src/muz/base/dl_rule_set.cpp | |
| src/smt/theory_utvpi.cpp | |
| src/smt/theory_diff_logic.cpp | |
| src/smt/smt_setup.cpp | |
| src/opt/opt_context.cpp | |
| src/opt/maxres.cpp | |
| src/opt/sortmax.cpp | |
| src/opt/opt_parse.cpp | |
| src/opt/wmax.cpp | |
| src/opt/opt_solver.cpp | |
| src/muz/fp/horn_tactic.cpp | |
| src/muz/spacer/spacer_legacy_frames.cpp | |
| src/muz/spacer/spacer_context.cpp | |
| src/muz/rel/dl_sparse_table.cpp | |
| src/muz/rel/dl_external_relation.cpp | |
| src/muz/transforms/dl_mk_interp_tail_simplifier.cpp | |
| src/muz/transforms/dl_mk_rule_inliner.cpp | |
| src/muz/transforms/dl_mk_unfold.cpp | |
| src/muz/transforms/dl_mk_coalesce.cpp | |
| src/muz/transforms/dl_mk_slice.cpp | |
| src/muz/transforms/dl_mk_elim_term_ite.cpp | |
| src/muz/transforms/dl_mk_array_blast.cpp | |
| src/muz/transforms/dl_mk_subsumption_checker.cpp | |
| src/muz/transforms/dl_transforms.cpp | |
| src/smt/theory_dense_diff_logic.cpp | |
| src/smt/theory_arith.cpp | |
| src/util/lp/row_eta_matrix.cpp | |
| src/util/lp/square_sparse_matrix.cpp | |
| src/util/lp/square_dense_submatrix.cpp | |
| src/shell/opt_frontend.cpp | |
| src/api/api_datalog.cpp | |
| src/api/api_opt.cpp | |
| src/opt/maxsmt.cpp | |
| src/opt/opt_cmds.cpp | |
| src/muz/fp/dl_register_engine.cpp | |
| src/muz/bmc/dl_bmc_engine.cpp | |
| src/muz/tab/tab_context.cpp | |
| src/muz/spacer/spacer_dl_interface.cpp | |
| src/muz/rel/dl_mk_simple_joins.cpp | |
| src/muz/rel/dl_lazy_table.cpp | |
| src/muz/rel/aig_exporter.cpp | |
| src/muz/rel/dl_table.cpp | |
| src/muz/rel/dl_interval_relation.cpp | |
| src/muz/rel/dl_instruction.cpp | |
| src/muz/rel/dl_mk_similarity_compressor.cpp | |
| src/muz/rel/dl_product_relation.cpp | |
| src/muz/rel/dl_sieve_relation.cpp | |
| src/muz/rel/dl_table_relation.cpp | |
| src/muz/rel/dl_check_table.cpp | |
| src/muz/rel/udoc_relation.cpp | |
| src/muz/rel/check_relation.cpp | |
| src/muz/rel/dl_base.cpp | |
| src/util/lp/lu.cpp | |
| src/shell/smtlib_frontend.cpp | |
| src/muz/fp/dl_cmds.cpp | |
| src/muz/rel/karr_relation.cpp | |
| src/muz/rel/dl_mk_explanations.cpp | |
| src/muz/rel/dl_finite_product_relation.cpp | |
| src/muz/rel/dl_bound_relation.cpp | |
| src/muz/rel/dl_compiler.cpp | |
| src/muz/rel/dl_relation_manager.cpp | |
| src/util/lp/lp_core_solver_base.cpp | |
| src/util/lp/core_solver_pretty_printer.cpp | |
| src/shell/datalog_frontend.cpp | |
| src/muz/rel/rel_context.cpp | |
| src/util/lp/lp_solver.cpp | |
| src/util/lp/lp_dual_core_solver.cpp | |
| src/util/lp/lp_dual_simplex.cpp | |
| src/util/lp/lar_core_solver.cpp | |
| src/smt/theory_lra.cpp | |
| src/util/lp/bound_propagator.cpp | |
| src/util/lp/static_matrix.cpp | |
| src/util/lp/lp_primal_core_solver.cpp | |
| src/util/lp/int_solver.cpp | |
| src/util/lp/lar_solver.cpp | |
| src/util/lp/nra_solver.cpp | |
| src/util/lp/lp_primal_simplex.cpp | |
| src/util/lp/random_updater.cpp | |
| src/shell/lp_frontend.cpp | |
| g++ -o z3 shell/lp_frontend.o shell/dimacs_frontend.o shell/z3_log_frontend.o shell/install_tactic.o shell/mem_initializer.o shell/datalog_frontend.o shell/gparams_register_modules.o shell/opt_frontend.o shell/smtlib_frontend.o shell/main.o cmd_context/extra_cmds/extra_cmds.a api/api.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a sat/sat_solver/sat_solver.a tactic/ufbv/ufbv_tactic.a muz/fp/fp.a muz/ddnf/ddnf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/fpa/fpa.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a solver/solver.a ast/proofs/proofs.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/automata/automata.a math/simplex/simplex.a math/hilbert/hilbert.a util/lp/lp.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -lpthread | |
| g++ -o libz3.dylib -dynamiclib api/dll/install_tactic.o api/dll/mem_initializer.o api/dll/gparams_register_modules.o api/dll/dll.o api/api_array.o api/api_fpa.o api/api_arith.o api/api_datatype.o api/z3_replayer.o api/api_model.o api/api_log_macros.o api/api_ast_map.o api/api_datalog.o api/api_ast_vector.o api/api_commands.o api/api_opt.o api/api_algebraic.o api/api_tactic.o api/api_ast.o api/api_context.o api/api_qe.o api/api_log.o api/api_pb.o api/api_polynomial.o api/api_goal.o api/api_rcf.o api/api_seq.o api/api_bv.o api/api_stats.o api/api_config_params.o api/api_solver.o api/api_quant.o api/api_params.o api/api_numeral.o api/api_parsers.o cmd_context/extra_cmds/extra_cmds.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a sat/sat_solver/sat_solver.a tactic/ufbv/ufbv_tactic.a muz/fp/fp.a muz/ddnf/ddnf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/fpa/fpa.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a solver/solver.a ast/proofs/proofs.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/automata/automata.a math/simplex/simplex.a math/hilbert/hilbert.a util/lp/lp.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a | |
| ld: warning: ld: warning: ld: warning: ld: warning: ignoring file cmd_context/extra_cmds/extra_cmds.a, file was built for archive which is not the architecture being linked (x86_64): cmd_context/extra_cmds/extra_cmds.ald: warning: ld: warning: ignoring file api/api.a, file was built for archive which is not the architecture being linked (x86_64): api/api.a | |
| ignoring file tactic/fpa/fpa_tactics.a, file was built for archive which is not the architecture being linked (x86_64): tactic/fpa/fpa_tactics.aignoring file tactic/portfolio/portfolio.a, file was built for archive which is not the architecture being linked (x86_64): tactic/portfolio/portfolio.ald: warning: ld: warning: ignoring file opt/opt.a, file was built for archive which is not the architecture being linked (x86_64): opt/opt.aignoring file tactic/portfolio/portfolio.a, file was built for archive which is not the architecture being linked (x86_64): tactic/portfolio/portfolio.a | |
| ld: warning: | |
| ignoring file tactic/smtlogics/smtlogic_tactics.a, file was built for archive which is not the architecture being linked (x86_64): tactic/smtlogics/smtlogic_tactics.aignoring file tactic/smtlogics/smtlogic_tactics.a, file was built for archive which is not the architecture being linked (x86_64): tactic/smtlogics/smtlogic_tactics.a | |
| ignoring file cmd_context/extra_cmds/extra_cmds.a, file was built for archive which is not the architecture being linked (x86_64): cmd_context/extra_cmds/extra_cmds.a | |
| ld: warning: ld: warning: ignoring file opt/opt.a, file was built for archive which is not the architecture being linked (x86_64): opt/opt.aignoring file tactic/fpa/fpa_tactics.a, file was built for archive which is not the architecture being linked (x86_64): tactic/fpa/fpa_tactics.a | |
| ld: warning: ignoring file muz/fp/fp.a, file was built for archive which is not the architecture being linked (x86_64): muz/fp/fp.a | |
| ld: warning: ignoring file muz/fp/fp.a, file was built for archive which is not the architecture being linked (x86_64): muz/fp/fp.ald: warning: ignoring file sat/sat_solver/sat_solver.a, file was built for archive which is not the architecture being linked (x86_64): sat/sat_solver/sat_solver.a | |
| ld: warning: ignoring file tactic/ufbv/ufbv_tactic.a, file was built for archive which is not the architecture being linked (x86_64): tactic/ufbv/ufbv_tactic.ald: warning: | |
| ignoring file tactic/ufbv/ufbv_tactic.a, file was built for archive which is not the architecture being linked (x86_64): tactic/ufbv/ufbv_tactic.ald: warning: ld: warning: ignoring file muz/ddnf/ddnf.a, file was built for archive which is not the architecture being linked (x86_64): muz/ddnf/ddnf.a | |
| ignoring file muz/bmc/bmc.a, file was built for archive which is not the architecture being linked (x86_64): muz/bmc/bmc.a | |
| ld: warning: ignoring file muz/tab/tab.a, file was built for archive which is not the architecture being linked (x86_64): muz/tab/tab.a | |
| ld: warning: ld: warning: ignoring file muz/dataflow/dataflow.a, file was built for archive which is not the architecture being linked (x86_64): muz/dataflow/dataflow.a | |
| ld: warning: ignoring file muz/transforms/transforms.a, file was built for archive which is not the architecture being linked (x86_64): muz/transforms/transforms.a | |
| ld: warning: ignoring file muz/ddnf/ddnf.a, file was built for archive which is not the architecture being linked (x86_64): muz/ddnf/ddnf.a | |
| ignoring file muz/tab/tab.a, file was built for archive which is not the architecture being linked (x86_64): muz/tab/tab.a | |
| ld: warning: ignoring file muz/bmc/bmc.a, file was built for archive which is not the architecture being linked (x86_64): muz/bmc/bmc.a | |
| ld: warning: ignoring file muz/spacer/spacer.a, file was built for archive which is not the architecture being linked (x86_64): muz/spacer/spacer.a | |
| ld: warning: ignoring file sat/sat_solver/sat_solver.a, file was built for archive which is not the architecture being linked (x86_64): sat/sat_solver/sat_solver.a | |
| ld: warning: ld: warning: ignoring file muz/clp/clp.a, file was built for archive which is not the architecture being linked (x86_64): muz/clp/clp.a | |
| ignoring file muz/clp/clp.a, file was built for archive which is not the architecture being linked (x86_64): muz/clp/clp.a | |
| ld: warning: ignoring file muz/rel/rel.a, file was built for archive which is not the architecture being linked (x86_64): muz/rel/rel.a | |
| ld: warning: ignoring file muz/base/muz.a, file was built for archive which is not the architecture being linked (x86_64): muz/base/muz.a | |
| ld: warning: ignoring file qe/qe.a, file was built for archive which is not the architecture being linked (x86_64): qe/qe.a | |
| ld: warning: ignoring file muz/spacer/spacer.a, file was built for archive which is not the architecture being linked (x86_64): muz/spacer/spacer.a | |
| ld: warning: ignoring file tactic/sls/sls_tactic.a, file was built for archive which is not the architecture being linked (x86_64): tactic/sls/sls_tactic.a | |
| ld: warning: ignoring file smt/tactic/smt_tactic.a, file was built for archive which is not the architecture being linked (x86_64): smt/tactic/smt_tactic.a | |
| ld: warning: ignoring file tactic/bv/bv_tactics.a, file was built for archive which is not the architecture being linked (x86_64): tactic/bv/bv_tactics.a | |
| ld: warning: ignoring file ast/pattern/pattern.a, file was built for archive which is not the architecture being linked (x86_64): ast/pattern/pattern.a | |
| ld: warning: ld: warning: ignoring file muz/rel/rel.a, file was built for archive which is not the architecture being linked (x86_64): muz/rel/rel.ald: warning: ignoring file parsers/smt2/smt2parser.a, file was built for archive which is not the architecture being linked (x86_64): parsers/smt2/smt2parser.aignoring file muz/transforms/transforms.a, file was built for archive which is not the architecture being linked (x86_64): muz/transforms/transforms.a | |
| ld: warning: ignoring file muz/dataflow/dataflow.a, file was built for archive which is not the architecture being linked (x86_64): muz/dataflow/dataflow.a | |
| ld: warning: ignoring file ackermannization/ackermannization.a, file was built for archive which is not the architecture being linked (x86_64): ackermannization/ackermannization.ald: warning: ignoring file tactic/sls/sls_tactic.a, file was built for archive which is not the architecture being linked (x86_64): tactic/sls/sls_tactic.a | |
| ld: warning: ignoring file qe/qe.a, file was built for archive which is not the architecture being linked (x86_64): qe/qe.a | |
| ld: warning: ignoring file muz/base/muz.a, file was built for archive which is not the architecture being linked (x86_64): muz/base/muz.a | |
| ld: warning: ignoring file smt/smt.a, file was built for archive which is not the architecture being linked (x86_64): smt/smt.a | |
| ld: warning: ignoring file cmd_context/cmd_context.a, file was built for archive which is not the architecture being linked (x86_64): cmd_context/cmd_context.a | |
| ld: warning: ignoring file tactic/aig/aig_tactic.a, file was built for archive which is not the architecture being linked (x86_64): tactic/aig/aig_tactic.a | |
| ld: warning: ignoring file math/subpaving/tactic/subpaving_tactic.a, file was built for archive which is not the architecture being linked (x86_64): math/subpaving/tactic/subpaving_tactic.a | |
| ld: warning: ignoring file tactic/bv/bv_tactics.a, file was built for archive which is not the architecture being linked (x86_64): tactic/bv/bv_tactics.a | |
| ld: warning: ignoring file nlsat/tactic/nlsat_tactic.a, file was built for archive which is not the architecture being linked (x86_64): nlsat/tactic/nlsat_tactic.a | |
| ld: warning: ignoring file smt/proto_model/proto_model.a, file was built for archive which is not the architecture being linked (x86_64): smt/proto_model/proto_model.a | |
| ld: warning: ignoring file sat/tactic/sat_tactic.a, file was built for archive which is not the architecture being linked (x86_64): sat/tactic/sat_tactic.a | |
| ld: warning: ignoring file tactic/arith/arith_tactics.a, file was built for archive which is not the architecture being linked (x86_64): tactic/arith/arith_tactics.a | |
| ld: warning: ignoring file solver/solver.a, file was built for archive which is not the architecture being linked (x86_64): solver/solver.a | |
| ld: warning: ignoring file smt/params/smt_params.a, file was built for archive which is not the architecture being linked (x86_64): smt/params/smt_params.a | |
| ld: warning: ignoring file smt/proto_model/proto_model.a, file was built for archive which is not the architecture being linked (x86_64): smt/proto_model/proto_model.a | |
| ld: warning: ignoring file ast/fpa/fpa.a, file was built for archive which is not the architecture being linked (x86_64): ast/fpa/fpa.a | |
| ld: warning: ignoring file ast/rewriter/bit_blaster/bit_blaster.a, file was built for archive which is not the architecture being linked (x86_64): ast/rewriter/bit_blaster/bit_blaster.a | |
| ld: warning: ignoring file smt/tactic/smt_tactic.a, file was built for archive which is not the architecture being linked (x86_64): smt/tactic/smt_tactic.a | |
| ld: warning: ignoring file tactic/core/core_tactics.a, file was built for archive which is not the architecture being linked (x86_64): tactic/core/core_tactics.a | |
| ld: warning: ignoring file tactic/tactic.a, file was built for archive which is not the architecture being linked (x86_64): tactic/tactic.a | |
| ld: warning: ignoring file smt/smt.a, file was built for archive which is not the architecture being linked (x86_64): smt/smt.a | |
| ld: warning: ignoring file cmd_context/cmd_context.a, file was built for archive which is not the architecture being linked (x86_64): cmd_context/cmd_context.a | |
| ld: warning: ignoring file ast/fpa/fpa.a, file was built for archive which is not the architecture being linked (x86_64): ast/fpa/fpa.a | |
| ld: warning: ignoring file ast/rewriter/bit_blaster/bit_blaster.a, file was built for archive which is not the architecture being linked (x86_64): ast/rewriter/bit_blaster/bit_blaster.a | |
| ld: warning: ignoring file ackermannization/ackermannization.a, file was built for archive which is not the architecture being linked (x86_64): ackermannization/ackermannization.a | |
| ld: warning: ignoring file ast/macros/macros.a, file was built for archive which is not the architecture being linked (x86_64): ast/macros/macros.a | |
| ld: warning: ignoring file tactic/aig/aig_tactic.a, file was built for archive which is not the architecture being linked (x86_64): tactic/aig/aig_tactic.ald: warning: | |
| ld: warning: ignoring file math/subpaving/tactic/subpaving_tactic.a, file was built for archive which is not the architecture being linked (x86_64): math/subpaving/tactic/subpaving_tactic.a | |
| ld: warning: ld: warning: ignoring file sat/tactic/sat_tactic.a, file was built for archive which is not the architecture being linked (x86_64): sat/tactic/sat_tactic.a | |
| ld: warning: ignoring file tactic/arith/arith_tactics.a, file was built for archive which is not the architecture being linked (x86_64): tactic/arith/arith_tactics.a | |
| ignoring file math/euclid/euclid.a, file was built for archive which is not the architecture being linked (x86_64): math/euclid/euclid.a | |
| ld: warning: ignoring file ast/rewriter/rewriter.a, file was built for archive which is not the architecture being linked (x86_64): ast/rewriter/rewriter.a | |
| ld: warning: ignoring file ast/proofs/proofs.a, file was built for archive which is not the architecture being linked (x86_64): ast/proofs/proofs.a | |
| ld: warning: ignoring file ast/pattern/pattern.a, file was built for archive which is not the architecture being linked (x86_64): ast/pattern/pattern.ald: warning: ignoring file math/euclid/euclid.a, file was built for archive which is not the architecture being linked (x86_64): math/euclid/euclid.a | |
| ld: warning: ignoring file nlsat/tactic/nlsat_tactic.a, file was built for archive which is not the architecture being linked (x86_64): nlsat/tactic/nlsat_tactic.aignoring file model/model.a, file was built for archive which is not the architecture being linked (x86_64): model/model.a | |
| ld: warning: ld: warning: ignoring file math/grobner/grobner.a, file was built for archive which is not the architecture being linked (x86_64): math/grobner/grobner.a | |
| ld: warning: | |
| ignoring file ast/normal_forms/normal_forms.a, file was built for archive which is not the architecture being linked (x86_64): ast/normal_forms/normal_forms.a | |
| ld: warning: ignoring file ast/substitution/substitution.a, file was built for archive which is not the architecture being linked (x86_64): ast/substitution/substitution.a | |
| ld: warning: ignoring file parsers/util/parser_util.a, file was built for archive which is not the architecture being linked (x86_64): parsers/util/parser_util.a | |
| ld: warning: ignoring file smt/params/smt_params.a, file was built for archive which is not the architecture being linked (x86_64): smt/params/smt_params.a | |
| ignoring file solver/solver.a, file was built for archive which is not the architecture being linked (x86_64): solver/solver.ald: warning: ignoring file ast/proofs/proofs.a, file was built for archive which is not the architecture being linked (x86_64): ast/proofs/proofs.ald: warning: ignoring file tactic/core/core_tactics.a, file was built for archive which is not the architecture being linked (x86_64): tactic/core/core_tactics.a | |
| ld: warning: ld: warning: ignoring file util/lp/lp.a, file was built for archive which is not the architecture being linked (x86_64): util/lp/lp.a | |
| ld: warning: ignoring file parsers/smt2/smt2parser.a, file was built for archive which is not the architecture being linked (x86_64): parsers/smt2/smt2parser.a | |
| ignoring file parsers/util/parser_util.a, file was built for archive which is not the architecture being linked (x86_64): parsers/util/parser_util.a | |
| ld: warning: ld: warning: ignoring file nlsat/nlsat.a, file was built for archive which is not the architecture being linked (x86_64): nlsat/nlsat.aignoring file ast/substitution/substitution.a, file was built for archive which is not the architecture being linked (x86_64): ast/substitution/substitution.a | |
| ld: warning: ignoring file math/subpaving/subpaving.a, file was built for archive which is not the architecture being linked (x86_64): math/subpaving/subpaving.a | |
| ld: warning: ignoring file tactic/tactic.a, file was built for archive which is not the architecture being linked (x86_64): tactic/tactic.a | |
| ld: warning: ignoring file model/model.a, file was built for archive which is not the architecture being linked (x86_64): model/model.a | |
| ld: warning: ignoring file ast/macros/macros.a, file was built for archive which is not the architecture being linked (x86_64): ast/macros/macros.a | |
| ld: warning: ignoring file math/realclosure/realclosure.a, file was built for archive which is not the architecture being linked (x86_64): math/realclosure/realclosure.a | |
| ld: warning: ignoring file ast/rewriter/rewriter.a, file was built for archive which is not the architecture being linked (x86_64): ast/rewriter/rewriter.a | |
| ld: warning: ignoring file math/polynomial/polynomial.a, file was built for archive which is not the architecture being linked (x86_64): math/polynomial/polynomial.a | |
| ld: warning: ignoring file math/grobner/grobner.a, file was built for archive which is not the architecture being linked (x86_64): math/grobner/grobner.a | |
| ld: warning: ignoring file ast/ast.a, file was built for archive which is not the architecture being linked (x86_64): ast/ast.a | |
| ld: warning: ignoring file math/automata/automata.a, file was built for archive which is not the architecture being linked (x86_64): math/automata/automata.a | |
| ld: warning: ignoring file math/realclosure/realclosure.a, file was built for archive which is not the architecture being linked (x86_64): math/realclosure/realclosure.a | |
| ld: warning: ignoring file math/simplex/simplex.a, file was built for archive which is not the architecture being linked (x86_64): math/simplex/simplex.a | |
| ld: warning: ignoring file math/interval/interval.a, file was built for archive which is not the architecture being linked (x86_64): math/interval/interval.a | |
| ld: warning: ignoring file math/automata/automata.a, file was built for archive which is not the architecture being linked (x86_64): math/automata/automata.a | |
| ld: warning: ignoring file util/lp/lp.a, file was built for archive which is not the architecture being linked (x86_64): util/lp/lp.a | |
| ld: warning: ignoring file nlsat/nlsat.a, file was built for archive which is not the architecture being linked (x86_64): nlsat/nlsat.a | |
| ld: warning: ignoring file math/hilbert/hilbert.a, file was built for archive which is not the architecture being linked (x86_64): math/hilbert/hilbert.a | |
| ld: warning: ld: warning: ignoring file math/polynomial/polynomial.a, file was built for archive which is not the architecture being linked (x86_64): math/polynomial/polynomial.a | |
| ld: warning: ignoring file math/hilbert/hilbert.a, file was built for archive which is not the architecture being linked (x86_64): math/hilbert/hilbert.aignoring file math/interval/interval.a, file was built for archive which is not the architecture being linked (x86_64): math/interval/interval.a | |
| ld: warning: ignoring file ast/normal_forms/normal_forms.a, file was built for archive which is not the architecture being linked (x86_64): ast/normal_forms/normal_forms.ald: warning: ignoring file math/simplex/simplex.a, file was built for archive which is not the architecture being linked (x86_64): math/simplex/simplex.a | |
| ld: warning: ignoring file ast/ast.a, file was built for archive which is not the architecture being linked (x86_64): ast/ast.a | |
| ld: warning: ignoring file math/subpaving/subpaving.a, file was built for archive which is not the architecture being linked (x86_64): math/subpaving/subpaving.a | |
| ld: warning: ignoring file sat/sat.a, file was built for archive which is not the architecture being linked (x86_64): sat/sat.a | |
| ld: warning: ignoring file sat/sat.a, file was built for archive which is not the architecture being linked (x86_64): sat/sat.a | |
| ld: warning: ignoring file util/util.a, file was built for archive which is not the architecture being linked (x86_64): util/util.a | |
| ld: warning: ignoring file util/util.a, file was built for archive which is not the architecture being linked (x86_64): util/util.a | |
| Undefined symbols for architecture x86_64: | |
| "parse_wcnf(opt::context&, std::__1::basic_istream<char, std::__1::char_traits<char> >&, svector<unsigned int, unsigned int>&)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "is_threaded()", referenced from: | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| read_datalog(char const*) in datalog_frontend.o | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| display_statistics() in opt_frontend.o | |
| "set_timeout(long)", referenced from: | |
| parse_cmd_line_args(int, char**) in main.o | |
| Undefined symbols for architecture x86_64: | |
| "warning_msg(char const*, ...)", referenced from: | |
| "parse_wcnf(opt::context&, std::__1::basic_istream<char, std::__1::char_traits<char> >&, svector<unsigned int, unsigned int>&)", referenced from: | |
| parse_cmd_line_args(int, char**) in main.o | |
| "mk_fd_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_75::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_fm_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_27::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| Z3_optimize_from_stream(_Z3_context*, _Z3_optimize*, std::__1::basic_istream<char, std::__1::char_traits<char> >&, char const*) in api_opt.o | |
| "mk_qe_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_9::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "parse_dimacs(std::__1::basic_istream<char, std::__1::char_traits<char> >&, sat::solver&)", referenced from: | |
| verify_solution(char const*) in dimacs_frontend.o | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| "mk_aig_tactic(params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_19::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_der_tactic(ast_manager&)", referenced from: | |
| install_tactics(tactic_manager&)::$_50::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_lia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_97::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_lra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_96::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "flatten_and(ref_vector<expr, ast_manager>&)", referenced from: | |
| "mk_nnf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_57::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_nra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_79::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qe2_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_11::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| _Z3_model_extrapolate in api_qe.o | |
| "mk_sat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_13::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_size_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_smt_tactic(params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_16::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_snf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_56::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "model_smt2_pp(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, ast_manager&, model_core const&, unsigned int)", referenced from: | |
| display_statistics() in opt_frontend.o | |
| "is_threaded()", referenced from: | |
| "finalize_debug()", referenced from: | |
| mem_finalize() in mem_initializer.o | |
| z3_replayer::imp::parse() in z3_replayer.o | |
| "mk_depth_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_fail_tactic()", referenced from: | |
| install_tactics(tactic_manager&)::$_100::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_horn_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_2::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_pb_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_lira_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_98::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_occf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_58::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "model_v2_pp(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, model_core const&, bool)", referenced from: | |
| "mk_qfbv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_82::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| _Z3_model_to_string in api_model.o | |
| "mk_qffp_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_71::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfuf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_88::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qsat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_10::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_sine_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_77::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_skip_tactic()", referenced from: | |
| install_tactics(tactic_manager&)::$_99::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_ufbv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_105::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| install_tactics(tactic_manager&)::$_106::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "verbose_stream()", referenced from: | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| read_datalog(char const*) in datalog_frontend.o | |
| "warning_msg(char const*, ...)", referenced from: | |
| display_statistics() in opt_frontend.o | |
| "install_dl_cmds(cmd_context&)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "mk_dt2bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_43::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| api::context::check_sorts(ast*) in api_context.o | |
| _Z3_global_param_set in api_config_params.o | |
| _Z3_global_param_get in api_config_params.o | |
| "mk_eq2bv_tactic(ast_manager&)", referenced from: | |
| _Z3_set_param_value in api_config_params.o | |
| install_tactics(tactic_manager&)::$_24::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_ilp_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_lia_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_lra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_nia_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_fd_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_75::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_nra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_memory_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_nlsat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_4::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_pb2bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_32::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfidl_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_83::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qflia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_84::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qflra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_85::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfnia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_86::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_fm_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_27::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfnra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_87::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_uflra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_92::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_ufnia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_91::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "finalize_symbols()", referenced from: | |
| mem_finalize() in mem_initializer.o | |
| "install_dbg_cmds(cmd_context&)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "install_opt_cmds(cmd_context&, opt::context*)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "mk_auflia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_93::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qe_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_9::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_factor_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_25::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_fpa2bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_70::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_lira_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_nira_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfbv_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qffp_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_lia2pb_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_29::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_nla2bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_30::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "par_and_then(tactic*, tactic*)", referenced from: | |
| "mk_nlqsat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_6::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qe_rec_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_12::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| _Z3_tactic_par_and_then in api_tactic.o | |
| "mk_qffpbv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_72::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfufbv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_89::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "reg_decl_plugins(ast_manager&)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "mk_auflira_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_94::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_aufnira_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_95::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_card2bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| "parse_dimacs(std::__1::basic_istream<char, std::__1::char_traits<char> >&, sat::solver&)", referenced from: | |
| install_tactics(tactic_manager&)::$_21::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_default_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_74::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_qflia_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| _Z3_solver_from_file in api_solver.o | |
| "mk_is_qflra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfnia_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfnra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_qe_lite_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_7::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfaufbv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_80::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "using_params(tactic*, params_ref const&)", referenced from: | |
| "mk_qffplra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_73::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "initialize_symbols()", referenced from: | |
| mem_initialize() in mem_initializer.o | |
| _Z3_tactic_using_params in api_tactic.o | |
| "mk_diff_neq_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_23::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_elim_and_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_64::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_qffpbv_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qflira_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_lia2card_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_28::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "expr_abstract(ast_manager&, unsigned int, unsigned int, expr* const*, expr*, obj_ref<expr, ast_manager>&)", referenced from: | |
| "mk_num_exprs_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_qfauflia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_81::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfbv_sls_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_78::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| _Z3_mk_lambda_const in api_quant.o | |
| _Z3_mk_quantifier_const_ex in api_quant.o | |
| "mk_simplify_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_63::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "get_verbosity_level()", referenced from: | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| read_datalog(char const*) in datalog_frontend.o | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| display_statistics() in opt_frontend.o | |
| "mk_ackr_bound_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_bv_bounds_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_39::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_aig_tactic(params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_19::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_qfaufbv_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfbv_eq_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qffplra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfufnra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_num_consts_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_solve_eqs_tactic(ast_manager&, params_ref const&, expr_replacer*)", referenced from: | |
| install_tactics(tactic_manager&)::$_65::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_subpaving_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_1::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_der_tactic(ast_manager&)", referenced from: | |
| install_tactics(tactic_manager&)::$_50::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "parse_smt2_commands(cmd_context&, std::__1::basic_istream<char, std::__1::char_traits<char> >&, bool, params_ref const&, char const*)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "set_verbosity_level(unsigned int)", referenced from: | |
| parse_cmd_line_args(int, char**) in main.o | |
| "mk_add_bounds_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_20::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_bvarray2uf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_42::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_fix_dl_var_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_26::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_has_pattern_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfauflia_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_lia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_97::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_quasi_pb_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_recover_01_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_35::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_arith_avg_bw_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_arith_max_bw_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_bit_blaster_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_36::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_bv1_blaster_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_37::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_injectivity_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_55::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_lra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_96::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_unbounded_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_qfnra_nlsat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_5::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfufbv_ackr_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_90::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_reduce_args_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_61::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_smt_solver_factory()", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "mk_tseitin_cnf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_68::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "install_subpaving_cmds(cmd_context&)", referenced from: | |
| "mk_nnf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_57::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "mk_bv_bound_chk_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_38::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_ctx_simplify_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_49::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_degree_shift_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_22::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_dom_simplify_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_52::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_elim_uncnstr_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_54::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_macro_finder_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_102::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_nra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_79::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_num_bv_consts_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_parallel_smt_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_17::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_purify_arith_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_34::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_quasi_macros_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_103::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| install_tactics(tactic_manager&)::$_104::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_split_clause_tactic(params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_66::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "enable_warning_messages(bool)", referenced from: | |
| "mk_qe2_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_11::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| parse_cmd_line_args(int, char**) in main.o | |
| "install_polynomial_cmds(cmd_context&)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "install_smt2_extra_cmds(cmd_context&)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "mk_dom_bv_bounds_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_40::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_elim_small_bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_44::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_elim_term_ite_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_53::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_has_quantifier_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_sat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| "mk_horn_simplify_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_13::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| install_tactics(tactic_manager&)::$_3::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_parallel_qffd_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_76::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_pb_preprocess_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_59::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_produce_models_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_produce_proofs_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_blast_term_ite_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_46::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_max_bv_sharing_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_45::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_size_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_num_bool_consts_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "register_on_timeout_proc(void (*)())", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| read_mps_file(char const*) in lp_frontend.o | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| read_datalog(char const*) in datalog_frontend.o | |
| parse_opt(char const*, opt_format) in opt_frontend.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| ... | |
| "mk_ackermannize_bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_0::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_arith_avg_degree_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_arith_max_degree_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_propositional_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_num_arith_consts_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_smt_tactic(params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_16::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_propagate_ineqs_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_33::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_symmetry_reduce_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_67::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_normalize_bounds_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_31::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_propagate_values_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_60::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_sat_preprocessor_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_14::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_tseitin_cnf_core_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_69::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_snf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| "mk_unit_subsumption_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_56::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| install_tactics(tactic_manager&)::$_18::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_bv_size_reduction_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_41::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_cofactor_term_ite_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_47::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_distribute_forall_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_51::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_fail_if_undecided_tactic()", referenced from: | |
| install_tactics(tactic_manager&)::$_101::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_reduce_invertible_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_62::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_collect_statistics_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_48::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "model_smt2_pp(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, ast_manager&, model_core const&, unsigned int)", referenced from: | |
| "mk_produce_unsat_cores_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| _Z3_model_to_string in api_model.o | |
| "mk_ctx_solver_simplify_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_15::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_smt_strategic_solver_factory(symbol const&)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "parse_lp(opt::context&, std::__1::basic_istream<char, std::__1::char_traits<char> >&, svector<unsigned int, unsigned int>&)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "parse_opb(opt::context&, std::__1::basic_istream<char, std::__1::char_traits<char> >&, svector<unsigned int, unsigned int>&)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "env_params::updt_params()", referenced from: | |
| _main in main.o | |
| "env_params::collect_param_descrs(param_descrs&)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "finalize_debug()", referenced from: | |
| mem_finalize() in mem_initializer.o | |
| "params_ref::g_empty_params_ref", referenced from: | |
| read_mps_file(char const*) in lp_frontend.o | |
| "params_ref::set_sym(char const*, symbol const&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "params_ref::set_bool(char const*, bool)", referenced from: | |
| verify_solution(char const*) in dimacs_frontend.o | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| "params_ref::set_uint(char const*, unsigned int)", referenced from: | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| "params_ref::~params_ref()", referenced from: | |
| read_mps_file(char const*) in lp_frontend.o | |
| verify_solution(char const*) in dimacs_frontend.o | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| install_tactics(tactic_manager&)::$_19::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| read_datalog(char const*) in datalog_frontend.o | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| ... | |
| "probe_info::probe_info(symbol const&, char const*, probe*)", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "is_well_sorted(ast_manager const&, expr*)", referenced from: | |
| "smt_params::updt_local_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| "statistics::update(char const*, double)", referenced from: | |
| display_statistics() in dimacs_frontend.o | |
| _Z3_is_well_sorted in api_ast.o | |
| "stream_ref::set(char const*)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| on_ctrl_c(int) in smtlib_frontend.o | |
| display_statistics() in smtlib_frontend.o | |
| "ast_manager::delete_node(ast*)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| display_statistics() in opt_frontend.o | |
| ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::~ref_vector_core() in opt_frontend.o | |
| "ast_manager::ast_manager(proof_gen_mode, char const*, bool)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "ast_manager::~ast_manager()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "cmd_context::display_statistics(bool, double)", referenced from: | |
| "mk_const_probe(double)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| on_ctrl_c(int) in smtlib_frontend.o | |
| display_statistics() in smtlib_frontend.o | |
| "cmd_context::set_solver_factory(solver_factory*)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| _Z3_probe_const in api_tactic.o | |
| "cmd_context::set_interpolating_solver_factory(solver_factory*)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "cmd_context::cmd_context(bool, ast_manager*, symbol const&)", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "cmd_context::~cmd_context()", referenced from: | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "mk_ismt2_pp::mk_ismt2_pp(ast*, ast_manager&, unsigned int, unsigned int, char const*)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "z3_replayer::parse()", referenced from: | |
| solve(char const*, std::__1::basic_istream<char, std::__1::char_traits<char> >&) in z3_log_frontend.o | |
| "mk_depth_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "z3_replayer::z3_replayer(std::__1::basic_istream<char, std::__1::char_traits<char> >&)", referenced from: | |
| solve(char const*, std::__1::basic_istream<char, std::__1::char_traits<char> >&) in z3_log_frontend.o | |
| "z3_replayer::~z3_replayer()", referenced from: | |
| solve(char const*, std::__1::basic_istream<char, std::__1::char_traits<char> >&) in z3_log_frontend.o | |
| "param_descrs::insert(char const*, cmd_arg_kind, char const*, char const*, char const*)", referenced from: | |
| read_mps_file(char const*) in lp_frontend.o | |
| gparams_register_modules() in gparams_register_modules.o | |
| pattern_inference_params_helper::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| pp_params::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| arith_rewriter_params::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| bool_rewriter_params::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| bv_rewriter_params::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| ... | |
| "param_descrs::param_descrs()", referenced from: | |
| read_mps_file(char const*) in lp_frontend.o | |
| gparams_register_modules() in gparams_register_modules.o | |
| "param_descrs::~param_descrs()", referenced from: | |
| read_mps_file(char const*) in lp_frontend.o | |
| gparams_register_modules() in gparams_register_modules.o | |
| "scoped_timer::scoped_timer(unsigned int, event_handler*)", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "mk_fail_tactic()", referenced from: | |
| "scoped_timer::~scoped_timer()", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| install_tactics(tactic_manager&)::$_100::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "context_params::collect_param_descrs(param_descrs&)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| _Z3_tactic_fail in api_tactic.o | |
| "dyn_ack_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| "prime_iterator::finalize()", referenced from: | |
| mem_finalize() in mem_initializer.o | |
| "tactic_manager::insert(probe_info*)", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "tactic_manager::insert(tactic_cmd*)", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "theory_bv_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| "mk_horn_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_2::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "theory_seq_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| "theory_str_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| "out_of_memory_error::out_of_memory_error()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "preprocessor_params::updt_local_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| "theory_arith_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| "pattern_inference_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| "lp::numeric_traits<double>::g_zero", referenced from: | |
| lp::mps_reader<double, double>::add_row(char) in lp_frontend.o | |
| lp::mps_reader<double, double>::create_or_update_bound() in lp_frontend.o | |
| lp::mps_reader<double, double>::read_bound_by_columns(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&) in lp_frontend.o | |
| "mk_is_pb_probe()", referenced from: | |
| lp::mps_reader<double, double>::maybe_modify_current_row_and_add_row_for_range(lp::mps_reader<double, double>::row*) in lp_frontend.o | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| lp::mps_reader<double, double>::fill_solver_on_columns(lp::lp_solver<double, double>*) in lp_frontend.o | |
| "lp::lp_primal_simplex<double, double>::find_maximal_solution()", referenced from: | |
| vtable for lp::lp_primal_simplex<double, double> in lp_frontend.o | |
| "lp::lp_primal_simplex<double, double>::~lp_primal_simplex()", referenced from: | |
| vtable for lp::lp_primal_simplex<double, double> in lp_frontend.o | |
| "lp::lp_primal_simplex<double, double>::~lp_primal_simplex()", referenced from: | |
| vtable for lp::lp_primal_simplex<double, double> in lp_frontend.o | |
| "lp::lp_status_to_string(lp::lp_status)", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| "lp::lp_solver<double, double>::flip_costs()", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| "lp::lp_solver<double, double>::add_constraint(lp::lp_relation, double, unsigned int)", referenced from: | |
| lp::mps_reader<double, double>::fill_solver_on_row(lp::mps_reader<double, double>::row*, lp::lp_solver<double, double>*) in lp_frontend.o | |
| "mk_lira_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_98::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "lp::lp_solver<double, double>::get_or_create_column_info(unsigned int)", referenced from: | |
| lp::mps_reader<double, double>::fill_solver_on_columns(lp::lp_solver<double, double>*) in lp_frontend.o | |
| lp::mps_reader<double, double>::set_solver_cost(lp::mps_reader<double, double>::row*, lp::lp_solver<double, double>*) in lp_frontend.o | |
| "lp::lp_solver<double, double>::give_symbolic_name_to_column(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >, unsigned int)", referenced from: | |
| lp::mps_reader<double, double>::fill_solver_on_columns(lp::lp_solver<double, double>*) in lp_frontend.o | |
| "lp::lp_solver<double, double>::~lp_solver()", referenced from: | |
| vtable for lp::lp_solver<double, double> in lp_frontend.o | |
| "lp::lp_solver<double, double>::~lp_solver()", referenced from: | |
| vtable for lp::lp_solver<double, double> in lp_frontend.o | |
| "qe::mk_sat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_8::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "nnf::get_param_descrs(param_descrs&)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "opt::context::updt_params(params_ref const&)", referenced from: | |
| "mk_occf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_58::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "opt::context::get_hard_constraints(ref_vector<expr, ast_manager>&)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "opt::context::optimize()", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "opt::context::get_lower(unsigned int)", referenced from: | |
| display_statistics() in opt_frontend.o | |
| "opt::context::get_upper(unsigned int)", referenced from: | |
| display_statistics() in opt_frontend.o | |
| "opt::context::context(ast_manager&)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "opt::context::~context()", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "mk_qfbv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_82::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "sat::solver::check(unsigned int, sat::literal const*)", referenced from: | |
| verify_solution(char const*) in dimacs_frontend.o | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| "sat::solver::mk_var(bool, bool)", referenced from: | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| track_clause(sat::solver&, svector<sat::literal, unsigned int>&, svector<sat::literal, unsigned int>&, vector<svector<sat::literal, unsigned int>, true, unsigned int>&) in dimacs_frontend.o | |
| "sat::solver::mk_clause(unsigned int, sat::literal*, bool)", referenced from: | |
| verify_solution(char const*) in dimacs_frontend.o | |
| track_clause(sat::solver&, svector<sat::literal, unsigned int>&, svector<sat::literal, unsigned int>&, vector<svector<sat::literal, unsigned int>, true, unsigned int>&) in dimacs_frontend.o | |
| "sat::solver::solver(params_ref const&, reslimit&)", referenced from: | |
| verify_solution(char const*) in dimacs_frontend.o | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| "sat::solver::~solver()", referenced from: | |
| verify_solution(char const*) in dimacs_frontend.o | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| "model::is_true(expr*)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "model::operator()(expr*)", referenced from: | |
| "mk_qffp_tactic(ast_manager&, params_ref const&)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| install_tactics(tactic_manager&)::$_71::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "memory::deallocate(void*)", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| lp::mps_reader<double, double>::read_ranges() in lp_frontend.o | |
| lp::mps_reader<double, double>::read_column(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&) in lp_frontend.o | |
| lp::split_and_trim(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&) in lp_frontend.o | |
| lp::string_split(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&, char const*, bool) in lp_frontend.o | |
| vector<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >, true, unsigned int>::expand_vector() in lp_frontend.o | |
| lp::mps_reader<double, double>::fill_rhs() in lp_frontend.o | |
| ... | |
| "memory::initialize(unsigned long)", referenced from: | |
| _main in main.o | |
| "memory::reallocate(void*, unsigned long)", referenced from: | |
| vector<sat::literal, false, unsigned int>::expand_vector() in dimacs_frontend.o | |
| "memory::display_max_usage(std::__1::basic_ostream<char, std::__1::char_traits<char> >&)", referenced from: | |
| solve(char const*, std::__1::basic_istream<char, std::__1::char_traits<char> >&) in z3_log_frontend.o | |
| "memory::above_high_watermark()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "memory::exit_when_out_of_memory(bool, char const*)", referenced from: | |
| _main in main.o | |
| "memory::allocate(unsigned long)", referenced from: | |
| vector<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >, true, unsigned int>::expand_vector() in lp_frontend.o | |
| lp::mps_reader<double, double>::create_or_update_bound() in lp_frontend.o | |
| lp::mps_reader<double, double>::read_bound_by_columns(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&) in lp_frontend.o | |
| track_clause(sat::solver&, svector<sat::literal, unsigned int>&, svector<sat::literal, unsigned int>&, vector<svector<sat::literal, unsigned int>, true, unsigned int>&) in dimacs_frontend.o | |
| vector<svector<sat::literal, unsigned int>, true, unsigned int>::expand_vector() in dimacs_frontend.o | |
| vector<sat::literal, false, unsigned int>::expand_vector() in dimacs_frontend.o | |
| "mk_qfuf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| ... | |
| install_tactics(tactic_manager&)::$_88::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "memory::finalize()", referenced from: | |
| _main in main.o | |
| "symbol::null", referenced from: | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| read_smtlib2_commands(char const*) in smtlib_frontend.o | |
| "symbol::symbol(char const*)", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| read_datalog(char const*) in datalog_frontend.o | |
| smt_params::smt_params(params_ref const&) in datalog_frontend.o | |
| "datalog::wpa_parser::create(datalog::context&, ast_manager&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::is_directory(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::register_engine::register_engine()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::accounted_object::set_accounting_parent_object(datalog::context&, datalog::rule*)", referenced from: | |
| "mk_qsat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_10::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| datalog::compiler::instruction_observer::notify(datalog::instruction*) in datalog_frontend.o | |
| "datalog::relation_manager::get_relation_plugin(symbol const&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::relation_manager::register_relation_plugin_impl(datalog::relation_plugin*)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::execution_context::set_timelimit(unsigned int)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::execution_context::reset_timelimit()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::execution_context::reset()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::execution_context::execution_context(datalog::context&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "mk_sine_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_77::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "datalog::execution_context::~execution_context()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::instruction_block::make_annotations(datalog::execution_context&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::instruction_block::process_all_costs()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| "datalog::instruction_block::reset()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::instruction_block::~instruction_block()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::finite_product_relation_plugin::finite_product_relation_plugin(datalog::relation_plugin&, datalog::relation_manager&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::parser::create(datalog::context&, ast_manager&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "mk_skip_tactic()", referenced from: | |
| install_tactics(tactic_manager&)::$_99::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "datalog::context::updt_params(params_ref const&)", referenced from: | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| "datalog::context::ensure_engine()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| _Z3_tactic_skip in api_tactic.o | |
| "datalog::context::replace_rules(datalog::rule_set const&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::context::flush_add_rules()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::context::close()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::context::reopen()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::context::context(ast_manager&, datalog::register_engine_base&, smt_params&, params_ref const&)", referenced from: | |
| "mk_ufbv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_105::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| install_tactics(tactic_manager&)::$_106::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::context::~context()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::compiler::do_compilation(datalog::instruction_block&, datalog::instruction_block&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::rule_set::rule_set(datalog::rule_set const&)", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::rule_set::~rule_set()", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "gparams::get_module(char const*)", referenced from: | |
| read_mps_file(char const*) in lp_frontend.o | |
| verify_solution(char const*) in dimacs_frontend.o | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "gparams::display_module(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, char const*)", referenced from: | |
| parse_cmd_line_args(int, char**) in main.o | |
| "mk_dt2bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_43::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "gparams::display_modules(std::__1::basic_ostream<char, std::__1::char_traits<char> >&)", referenced from: | |
| parse_cmd_line_args(int, char**) in main.o | |
| "gparams::register_global(param_descrs&)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "gparams::register_module(char const*, param_descrs*)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "gparams::display_parameter(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, char const*)", referenced from: | |
| parse_cmd_line_args(int, char**) in main.o | |
| "gparams::register_module_descr(char const*, char const*)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "gparams::set(char const*, char const*)", referenced from: | |
| parse_cmd_line_args(int, char**) in main.o | |
| "gparams::init()", referenced from: | |
| "mk_eq2bv_tactic(ast_manager&)", referenced from: | |
| install_tactics(tactic_manager&)::$_24::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| mem_initialize() in mem_initializer.o | |
| "gparams::display(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, unsigned int, bool, bool)", referenced from: | |
| parse_cmd_line_args(int, char**) in main.o | |
| "gparams::get_ref()", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "gparams::finalize()", referenced from: | |
| mem_finalize() in mem_initializer.o | |
| "gparams::get_value(char const*)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "rational::initialize()", referenced from: | |
| mem_initialize() in mem_initializer.o | |
| "rational::finalize()", referenced from: | |
| mem_finalize() in mem_initializer.o | |
| "mk_is_ilp_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "reslimit::dec_cancel()", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| cancel_eh<reslimit>::~cancel_eh() in lp_frontend.o | |
| cancel_eh<reslimit>::~cancel_eh() in lp_frontend.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| cancel_eh<reslimit>::~cancel_eh() in opt_frontend.o | |
| cancel_eh<reslimit>::~cancel_eh() in opt_frontend.o | |
| "reslimit::inc_cancel()", referenced from: | |
| cancel_eh<reslimit>::operator()(event_handler_caller_t) in lp_frontend.o | |
| cancel_eh<reslimit>::operator()(event_handler_caller_t) in opt_frontend.o | |
| "reslimit::inc()", referenced from: | |
| front_end_resource_limit::get_cancel_flag() in lp_frontend.o | |
| "reslimit::pop()", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "reslimit::push(unsigned int)", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "reslimit::cancel()", referenced from: | |
| on_ctrl_c(int) in opt_frontend.o | |
| "reslimit::reslimit()", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| verify_solution(char const*) in dimacs_frontend.o | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| "mk_is_lia_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "qi_params::updt_params(params_ref const&)", referenced from: | |
| qi_params::qi_params(params_ref const&) in datalog_frontend.o | |
| "params_ref::get_bool(char const*, params_ref const&, bool) const", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| "params_ref::get_bool(char const*, bool) const", referenced from: | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "params_ref::get_uint(char const*, params_ref const&, unsigned int) const", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| "params_ref::get_uint(char const*, unsigned int) const", referenced from: | |
| run_solver(lp_params&, char const*) in lp_frontend.o | |
| "statistics::display_smt2(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| display_statistics() in dimacs_frontend.o | |
| "mk_is_lra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "statistics::display(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| display_statistics() in opt_frontend.o | |
| "z3_replayer::get_line() const", referenced from: | |
| solve(char const*, std::__1::basic_istream<char, std::__1::char_traits<char> >&) in z3_log_frontend.o | |
| "z3_exception::has_error_code() const", referenced from: | |
| _main in main.o | |
| "lp::lp_primal_simplex<double, double>::get_current_cost() const", referenced from: | |
| vtable for lp::lp_primal_simplex<double, double> in lp_frontend.o | |
| "lp::lp_solver<double, double>::get_column_name(unsigned int) const", referenced from: | |
| vtable for lp::lp_solver<double, double> in lp_frontend.o | |
| vtable for lp::lp_primal_simplex<double, double> in lp_frontend.o | |
| "lp::lp_solver<double, double>::get_column_index_by_name(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >) const", referenced from: | |
| vtable for lp::lp_solver<double, double> in lp_frontend.o | |
| vtable for lp::lp_primal_simplex<double, double> in lp_frontend.o | |
| "mk_is_nia_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "lp::lp_solver<double, double>::get_column_value_with_core_solver(unsigned int, lp::lp_core_solver_base<double, double>*) const", referenced from: | |
| lp::lp_primal_simplex<double, double>::get_column_value(unsigned int) const in lp_frontend.o | |
| "sat::solver::display_status(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| "sat::solver::collect_statistics(statistics&) const", referenced from: | |
| display_statistics() in dimacs_frontend.o | |
| "sat::solver::collect_bin_clauses(svector<std::__1::pair<sat::literal, sat::literal>, unsigned int>&, bool, bool) const", referenced from: | |
| read_dimacs(char const*) in dimacs_frontend.o | |
| "datalog::relation_manager::display_relation_sizes(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| "datalog::execution_context::report_big_relations(unsigned int, std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| "datalog::instruction_block::display_indented(datalog::execution_context const&, std::__1::basic_ostream<char, std::__1::char_traits<char> >&, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&) const", referenced from: | |
| "mk_is_nra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| "datalog::instruction_block::perform(datalog::execution_context&) const", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::context::output_tuples() const", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::context::initial_restart_timeout() const", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::rule_set::display_deps(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| read_datalog(char const*) in datalog_frontend.o | |
| "datalog::rule_set::display(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| display_statistics(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, bool) in datalog_frontend.o | |
| "typeinfo for z3_exception", referenced from: | |
| GCC_except_table1 in z3_log_frontend.o | |
| GCC_except_table4 in opt_frontend.o | |
| GCC_except_table4 in main.o | |
| "mk_memory_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "typeinfo for default_exception", referenced from: | |
| vector<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >, true, unsigned int>::expand_vector() in lp_frontend.o | |
| vector<svector<sat::literal, unsigned int>, true, unsigned int>::expand_vector() in dimacs_frontend.o | |
| vector<sat::literal, false, unsigned int>::expand_vector() in dimacs_frontend.o | |
| "typeinfo for z3_error", referenced from: | |
| typeinfo for out_of_memory_error in datalog_frontend.o | |
| "vtable for default_exception", referenced from: | |
| vector<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >, true, unsigned int>::expand_vector() in lp_frontend.o | |
| default_exception::~default_exception() in lp_frontend.o | |
| vector<svector<sat::literal, unsigned int>, true, unsigned int>::expand_vector() in dimacs_frontend.o | |
| default_exception::~default_exception() in dimacs_frontend.o | |
| vector<sat::literal, false, unsigned int>::expand_vector() in dimacs_frontend.o | |
| NOTE: a missing vtable usually means the first non-inline virtual member function has no definition. | |
| "operator<<(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, mk_ismt2_pp const&)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| "operator<<(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, obj_ref<expr, ast_manager> const&)", referenced from: | |
| parse_opt(std::__1::basic_istream<char, std::__1::char_traits<char> >&, opt_format) in opt_frontend.o | |
| display_statistics() in opt_frontend.o | |
| "mk_nlsat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_4::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| ld: symbol(s) not found for architecture x86_64 | |
| "mk_pb2bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_32::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfidl_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_83::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| clang: error: linker command failed with exit code 1 (use -v to see invocation) | |
| "mk_qflia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_84::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qflra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_85::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| make: *** [z3] Error 1 | |
| make: *** Waiting for unfinished jobs.... | |
| "mk_qfnia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_86::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfnra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_87::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_uflra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_92::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_ufnia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_91::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "norm_param_name(symbol const&)", referenced from: | |
| _Z3_params_set_bool in api_params.o | |
| _Z3_params_set_uint in api_params.o | |
| _Z3_params_set_double in api_params.o | |
| _Z3_params_set_symbol in api_params.o | |
| "finalize_symbols()", referenced from: | |
| mem_finalize() in mem_initializer.o | |
| "install_opt_cmds(cmd_context&, opt::context*)", referenced from: | |
| Z3_optimize_from_stream(_Z3_context*, _Z3_optimize*, std::__1::basic_istream<char, std::__1::char_traits<char> >&, char const*) in api_opt.o | |
| "mk_auflia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_93::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_datatype_decl(datatype::util&, symbol const&, unsigned int, sort* const*, unsigned int, datatype::constructor* const*)", referenced from: | |
| _Z3_mk_tuple_sort in api_datatype.o | |
| _Z3_mk_enumeration_sort in api_datatype.o | |
| _Z3_mk_list_sort in api_datatype.o | |
| mk_datatype_decl(_Z3_context*, _Z3_symbol*, unsigned int, _Z3_constructor**) in api_datatype.o | |
| "mk_factor_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_25::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_fpa2bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_70::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_lira_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_nira_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfbv_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qffp_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_lia2pb_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_29::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_nla2bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_30::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_nlqsat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_6::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qe_rec_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_12::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qffpbv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_72::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfufbv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_89::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "reg_decl_plugins(ast_manager&)", referenced from: | |
| api::context::add_plugins::add_plugins(ast_manager&) in api_context.o | |
| api::context::add_plugins::add_plugins(ast_manager&) in api_context.o | |
| api::context::context(context_params*, bool) in api_context.o | |
| "ast_ll_bounded_pp(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, ast_manager&, ast*, unsigned int)", referenced from: | |
| api::context::check_sorts(ast*) in api_context.o | |
| "mk_auflira_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_94::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_aufnira_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_95::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_card2bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_21::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_default_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_74::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_qflia_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qflra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfnia_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfnra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_qe_lite_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_7::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfaufbv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_80::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qffplra_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_73::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "initialize_symbols()", referenced from: | |
| mem_initialize() in mem_initializer.o | |
| "mk_diff_neq_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_23::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_elim_and_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_64::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_qffpbv_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qflira_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_lia2card_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_28::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_num_exprs_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_qfauflia_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_81::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfbv_sls_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_78::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_simplify_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_63::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "get_verbosity_level()", referenced from: | |
| z3_replayer::imp::parse() in z3_replayer.o | |
| "mk_ackr_bound_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_bv_bounds_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_39::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_qfaufbv_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfbv_eq_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qffplra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfufnra_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_num_consts_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_solve_eqs_tactic(ast_manager&, params_ref const&, expr_replacer*)", referenced from: | |
| install_tactics(tactic_manager&)::$_65::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_subpaving_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_1::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "parse_smt2_commands(cmd_context&, std::__1::basic_istream<char, std::__1::char_traits<char> >&, bool, params_ref const&, char const*)", referenced from: | |
| _Z3_fixedpoint_from_stream in api_datalog.o | |
| Z3_optimize_from_stream(_Z3_context*, _Z3_optimize*, std::__1::basic_istream<char, std::__1::char_traits<char> >&, char const*) in api_opt.o | |
| _solver_from_stream in api_solver.o | |
| _parse_smtlib2_stream in api_parsers.o | |
| _Z3_eval_smtlib2_string in api_parsers.o | |
| "mk_add_bounds_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_20::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_bvarray2uf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_42::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_fix_dl_var_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_26::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_has_pattern_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_qfauflia_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_quasi_pb_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_recover_01_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_35::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "get_memory_statistics(statistics&)", referenced from: | |
| _Z3_solver_get_statistics in api_solver.o | |
| "get_rlimit_statistics(reslimit&, statistics&)", referenced from: | |
| _Z3_solver_get_statistics in api_solver.o | |
| "mk_arith_avg_bw_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_arith_max_bw_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_bit_blaster_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_36::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_bv1_blaster_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_37::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_injectivity_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_55::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_is_unbounded_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_qfnra_nlsat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_5::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_qfufbv_ackr_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_90::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_reduce_args_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_61::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_smt_solver_factory()", referenced from: | |
| _Z3_mk_simple_solver in api_solver.o | |
| "mk_tseitin_cnf_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_68::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "proof2proof_converter(ast_manager&, app*)", referenced from: | |
| _tactic_apply(_Z3_context*, _Z3_tactic*, _Z3_goal*, params_ref) in api_tactic.o | |
| "mk_bv_bound_chk_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_38::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_ctx_simplify_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_49::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_degree_shift_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_22::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_dom_simplify_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_52::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_elim_uncnstr_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_54::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_macro_finder_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_102::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_num_bv_consts_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_parallel_smt_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_17::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_purify_arith_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_34::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_quasi_macros_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_103::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| install_tactics(tactic_manager&)::$_104::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_split_clause_tactic(params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_66::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "enable_warning_messages(bool)", referenced from: | |
| _Z3_toggle_warning_messages in api_context.o | |
| "install_dl_collect_cmds(dl_collected_cmds&, cmd_context&)", referenced from: | |
| _Z3_fixedpoint_from_stream in api_datalog.o | |
| "mk_dom_bv_bounds_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_40::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_elim_small_bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_44::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_elim_term_ite_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_53::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_has_quantifier_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_horn_simplify_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_3::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_parallel_qffd_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_76::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_pb_preprocess_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_59::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_produce_models_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_produce_proofs_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_blast_term_ite_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_46::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_max_bv_sharing_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_45::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_num_bool_consts_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_tactic2solver_factory(tactic*)", referenced from: | |
| _Z3_mk_solver_from_tactic in api_solver.o | |
| "mk_ackermannize_bv_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_0::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_arith_avg_degree_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_arith_max_degree_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_is_propositional_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_num_arith_consts_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_propagate_ineqs_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_33::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_symmetry_reduce_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_67::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_normalize_bounds_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_31::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_propagate_values_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_60::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_sat_preprocessor_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_14::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_tseitin_cnf_core_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_69::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_unit_subsumption_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_18::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_bv_size_reduction_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_41::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_cofactor_term_ite_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_47::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_distribute_forall_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_51::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_fail_if_undecided_tactic()", referenced from: | |
| install_tactics(tactic_manager&)::$_101::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| _Z3_tactic_fail_if_not_decided in api_tactic.o | |
| "mk_reduce_invertible_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_62::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_collect_statistics_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_48::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_produce_unsat_cores_probe()", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "mk_ctx_solver_simplify_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_15::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mk_smt_strategic_solver_factory(symbol const&)", referenced from: | |
| _Z3_mk_solver in api_solver.o | |
| _Z3_mk_solver_for_logic in api_solver.o | |
| _Z3_eval_smtlib2_string in api_parsers.o | |
| "par(unsigned int, tactic* const*)", referenced from: | |
| _Z3_tactic_par_or in api_tactic.o | |
| "cond(probe*, tactic*, tactic*)", referenced from: | |
| _Z3_tactic_cond in api_tactic.o | |
| "exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&)", referenced from: | |
| _tactic_apply(_Z3_context*, _Z3_tactic*, _Z3_goal*, params_ref) in api_tactic.o | |
| "when(probe*, tactic*)", referenced from: | |
| _Z3_tactic_when in api_tactic.o | |
| "mk_eq(probe*, probe*)", referenced from: | |
| _Z3_probe_eq in api_tactic.o | |
| "mk_ge(probe*, probe*)", referenced from: | |
| _Z3_probe_ge in api_tactic.o | |
| "mk_gt(probe*, probe*)", referenced from: | |
| _Z3_probe_gt in api_tactic.o | |
| "mk_le(probe*, probe*)", referenced from: | |
| _Z3_probe_le in api_tactic.o | |
| "mk_lt(probe*, probe*)", referenced from: | |
| _Z3_probe_lt in api_tactic.o | |
| "mk_or(probe*, probe*)", referenced from: | |
| _Z3_probe_or in api_tactic.o | |
| "mk_and(probe*, probe*)", referenced from: | |
| _Z3_probe_and in api_tactic.o | |
| "mk_and(ast_manager&, unsigned int, expr* const*)", referenced from: | |
| _Z3_model_extrapolate in api_qe.o | |
| "mk_not(probe*)", referenced from: | |
| _Z3_probe_not in api_tactic.o | |
| "repeat(tactic*, unsigned int)", referenced from: | |
| _Z3_tactic_repeat in api_tactic.o | |
| "fail_if(probe*)", referenced from: | |
| _Z3_tactic_fail_if in api_tactic.o | |
| "or_else(tactic*, tactic*)", referenced from: | |
| _Z3_tactic_or_else in api_tactic.o | |
| "try_for(tactic*, unsigned int)", referenced from: | |
| _Z3_tactic_try_for in api_tactic.o | |
| "and_then(tactic*, tactic*)", referenced from: | |
| _Z3_tactic_and_then in api_tactic.o | |
| "get_sort(expr const*)", referenced from: | |
| _Z3_mk_select in api_array.o | |
| _Z3_mk_select_n in api_array.o | |
| _Z3_mk_store in api_array.o | |
| _Z3_mk_store_n in api_array.o | |
| _Z3_mk_map in api_array.o | |
| _Z3_mk_const_array in api_array.o | |
| _mk_app_array_core in api_array.o | |
| ... | |
| "parse_lp(opt::context&, std::__1::basic_istream<char, std::__1::char_traits<char> >&, svector<unsigned int, unsigned int>&)", referenced from: | |
| Z3_optimize_from_stream(_Z3_context*, _Z3_optimize*, std::__1::basic_istream<char, std::__1::char_traits<char> >&, char const*) in api_opt.o | |
| "ast_ll_pp(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, ast_manager&, ast*, bool, bool)", referenced from: | |
| _Z3_ast_to_string in api_ast.o | |
| "parse_opb(opt::context&, std::__1::basic_istream<char, std::__1::char_traits<char> >&, svector<unsigned int, unsigned int>&)", referenced from: | |
| Z3_optimize_from_stream(_Z3_context*, _Z3_optimize*, std::__1::basic_istream<char, std::__1::char_traits<char> >&, char const*) in api_opt.o | |
| "arith_util::init_plugin()", referenced from: | |
| _Z3_get_algebraic_number_lower in api_arith.o | |
| _Z3_get_algebraic_number_upper in api_arith.o | |
| _Z3_get_numerator in api_arith.o | |
| _Z3_get_denominator in api_arith.o | |
| _Z3_algebraic_sign in api_algebraic.o | |
| _Z3_algebraic_add in api_algebraic.o | |
| _Z3_algebraic_sub in api_algebraic.o | |
| ... | |
| "arith_util::to_irrational_algebraic_numeral(expr const*)", referenced from: | |
| _Z3_get_algebraic_number_lower in api_arith.o | |
| _Z3_get_algebraic_number_upper in api_arith.o | |
| _Z3_algebraic_sign in api_algebraic.o | |
| _Z3_algebraic_add in api_algebraic.o | |
| _Z3_algebraic_sub in api_algebraic.o | |
| _Z3_algebraic_mul in api_algebraic.o | |
| _Z3_algebraic_div in api_algebraic.o | |
| ... | |
| "arith_util::arith_util(ast_manager&)", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| "array_util::array_util(ast_manager&)", referenced from: | |
| _Z3_mk_as_array in api_array.o | |
| "ast_smt_pp::display_smt2(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, expr*)", referenced from: | |
| _Z3_benchmark_to_smtlib_string in api_ast.o | |
| "ast_smt_pp::ast_smt_pp(ast_manager&)", referenced from: | |
| _Z3_benchmark_to_smtlib_string in api_ast.o | |
| "env_params::updt_params()", referenced from: | |
| _Z3_global_param_set in api_config_params.o | |
| _Z3_global_param_reset_all in api_config_params.o | |
| "env_params::collect_param_descrs(param_descrs&)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "model_core::register_decl(func_decl*, func_interp*)", referenced from: | |
| _Z3_add_func_interp in api_model.o | |
| "model_core::register_decl(func_decl*, expr*)", referenced from: | |
| _Z3_add_const_interp in api_model.o | |
| "params_ref::set_double(char const*, double)", referenced from: | |
| _Z3_params_set_double in api_params.o | |
| "params_ref::g_empty_params_ref", referenced from: | |
| _Z3_model_to_string in api_model.o | |
| _Z3_benchmark_to_smtlib_string in api_ast.o | |
| "params_ref::copy(params_ref const&)", referenced from: | |
| _Z3_solver_set_params in api_solver.o | |
| "params_ref::set_sym(char const*, symbol const&)", referenced from: | |
| _Z3_params_set_symbol in api_params.o | |
| "params_ref::set_bool(char const*, bool)", referenced from: | |
| _Z3_params_set_bool in api_params.o | |
| "params_ref::set_uint(char const*, unsigned int)", referenced from: | |
| _Z3_ast_to_string in api_ast.o | |
| _Z3_params_set_uint in api_params.o | |
| "params_ref::validate(param_descrs const&)", referenced from: | |
| _Z3_fixedpoint_set_params in api_datalog.o | |
| _Z3_optimize_set_params in api_opt.o | |
| _Z3_tactic_using_params in api_tactic.o | |
| _Z3_tactic_apply_ex in api_tactic.o | |
| init_solver(_Z3_context*, _Z3_solver*) in api_solver.o | |
| _Z3_solver_set_params in api_solver.o | |
| _Z3_params_validate in api_params.o | |
| ... | |
| "params_ref::params_ref(params_ref const&)", referenced from: | |
| _Z3_fixedpoint_set_params in api_datalog.o | |
| _Z3_optimize_set_params in api_opt.o | |
| _Z3_tactic_using_params in api_tactic.o | |
| _Z3_tactic_apply in api_tactic.o | |
| _Z3_tactic_apply_ex in api_tactic.o | |
| simplify(_Z3_context*, _Z3_ast*, _Z3_params*) in api_ast.o | |
| init_solver(_Z3_context*, _Z3_solver*) in api_solver.o | |
| ... | |
| "params_ref::~params_ref()", referenced from: | |
| install_tactics(tactic_manager&)::$_19::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| _Z3_model_to_string in api_model.o | |
| _Z3_ast_map_to_string in api_ast_map.o | |
| _Z3_mk_fixedpoint in api_datalog.o | |
| _Z3_fixedpoint_from_stream in api_datalog.o | |
| _Z3_fixedpoint_set_params in api_datalog.o | |
| Z3_fixedpoint_ref::~Z3_fixedpoint_ref() in api_datalog.o | |
| ... | |
| "params_ref::operator=(params_ref const&)", referenced from: | |
| _Z3_fixedpoint_set_params in api_datalog.o | |
| "polynomial::manager::dec_ref(polynomial::polynomial*)", referenced from: | |
| _Z3_algebraic_roots in api_algebraic.o | |
| _Z3_algebraic_eval in api_algebraic.o | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "polynomial::manager::inc_ref(polynomial::polynomial*)", referenced from: | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "polynomial::manager::max_var(polynomial::polynomial const*)", referenced from: | |
| _Z3_algebraic_roots in api_algebraic.o | |
| _Z3_algebraic_eval in api_algebraic.o | |
| "polynomial::manager::psc_chain(polynomial::polynomial const*, polynomial::polynomial const*, unsigned int, ref_vector<polynomial::polynomial, polynomial::manager>&)", referenced from: | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "polynomial::manager::manager(reslimit&, mpz_manager<false>&, polynomial::monomial_manager*)", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| "polynomial::manager::~manager()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| api::pmanager::~pmanager() in api_context.o | |
| api::context::~context() in api_context.o | |
| "probe_info::probe_info(symbol const&, char const*, probe*)", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "smt_logics::supported_logic(symbol const&)", referenced from: | |
| _Z3_mk_solver_for_logic in api_solver.o | |
| "smt_params::updt_local_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in api_context.o | |
| "stream_ref::set(std::__1::basic_ostream<char, std::__1::char_traits<char> >&)", referenced from: | |
| Z3_optimize_from_stream(_Z3_context*, _Z3_optimize*, std::__1::basic_istream<char, std::__1::char_traits<char> >&, char const*) in api_opt.o | |
| _solver_from_stream in api_solver.o | |
| _parse_smtlib2_stream in api_parsers.o | |
| _Z3_eval_smtlib2_string in api_parsers.o | |
| "ast_manager::mk_pattern(unsigned int, app* const*)", referenced from: | |
| _Z3_mk_pattern in api_quant.o | |
| "ast_manager::delete_node(ast*)", referenced from: | |
| _Z3_del_constructor in api_datatype.o | |
| _Z3_mk_datatype in api_datatype.o | |
| _Z3_mk_datatypes in api_datatype.o | |
| ref_vector_core<sort, ref_manager_wrapper<sort, ast_manager> >::~ref_vector_core() in api_datatype.o | |
| _Z3_model_eval in api_model.o | |
| ref_vector_core<ast, ref_manager_wrapper<ast, ast_manager> >::~ref_vector_core() in api_model.o | |
| void dec_ref_key_values<ast_manager, obj_map<ast, ast*> >(ast_manager&, obj_map<ast, ast*>&) in api_ast_map.o | |
| ... | |
| "ast_manager::mk_func_decl(symbol const&, unsigned int, sort* const*, sort*, func_decl_info*)", referenced from: | |
| _Z3_mk_func_decl in api_ast.o | |
| _Z3_mk_const in api_ast.o | |
| "ast_manager::mk_func_decl(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*)", referenced from: | |
| _Z3_mk_array_default in api_array.o | |
| _Z3_mk_seq_empty in api_seq.o | |
| "ast_manager::mk_func_decl(int, int, unsigned int, parameter const*, unsigned int, sort* const*, sort*)", referenced from: | |
| _Z3_mk_select in api_array.o | |
| _Z3_mk_select_n in api_array.o | |
| _Z3_mk_store in api_array.o | |
| _Z3_mk_store_n in api_array.o | |
| _Z3_mk_map in api_array.o | |
| _Z3_mk_const_array in api_array.o | |
| _mk_app_array_core in api_array.o | |
| ... | |
| "ast_manager::mk_quantifier(quantifier_kind, unsigned int, sort* const*, symbol const*, expr*, int, symbol const&, symbol const&, unsigned int, expr* const*, unsigned int, expr* const*)", referenced from: | |
| _mk_quantifier_ex_core in api_quant.o | |
| "ast_manager::register_plugin(symbol const&, decl_plugin*)", referenced from: | |
| api::fixedpoint_context::set_state(void*) in api_datalog.o | |
| "ast_manager::update_fresh_id(ast_manager const&)", referenced from: | |
| ast_translation::ast_translation(ast_manager&, ast_manager&, bool) in api_model.o | |
| ast_translation::ast_translation(ast_manager&, ast_manager&, bool) in api_ast_vector.o | |
| ast_translation::ast_translation(ast_manager&, ast_manager&, bool) in api_ast.o | |
| ast_translation::ast_translation(ast_manager&, ast_manager&, bool) in api_goal.o | |
| "ast_manager::update_quantifier(quantifier*, expr*)", referenced from: | |
| _Z3_update_term in api_ast.o | |
| "ast_manager::mk_fresh_func_decl(symbol const&, symbol const&, unsigned int, sort* const*, sort*)", referenced from: | |
| _Z3_mk_fresh_func_decl in api_ast.o | |
| _Z3_mk_fresh_const in api_ast.o | |
| "ast_manager::copy_families_plugins(ast_manager const&)", referenced from: | |
| ast_translation::ast_translation(ast_manager&, ast_manager&, bool) in api_model.o | |
| ast_translation::ast_translation(ast_manager&, ast_manager&, bool) in api_ast_vector.o | |
| ast_translation::ast_translation(ast_manager&, ast_manager&, bool) in api_ast.o | |
| ast_translation::ast_translation(ast_manager&, ast_manager&, bool) in api_goal.o | |
| "ast_manager::mk_uninterpreted_sort(symbol const&, unsigned int, parameter const*)", referenced from: | |
| _Z3_mk_uninterpreted_sort in api_ast.o | |
| "ast_manager::mk_app(func_decl*, unsigned int, expr* const*)", referenced from: | |
| _Z3_mk_select in api_array.o | |
| _Z3_mk_select_n in api_array.o | |
| _Z3_mk_store in api_array.o | |
| _Z3_mk_store_n in api_array.o | |
| _Z3_mk_map in api_array.o | |
| _Z3_mk_const_array in api_array.o | |
| _Z3_mk_array_default in api_array.o | |
| ... | |
| "ast_manager::mk_app(int, int, expr*)", referenced from: | |
| _Z3_mk_fpa_abs in api_fpa.o | |
| _Z3_mk_fpa_neg in api_fpa.o | |
| _Z3_mk_fpa_is_normal in api_fpa.o | |
| _Z3_mk_fpa_is_subnormal in api_fpa.o | |
| _Z3_mk_fpa_is_zero in api_fpa.o | |
| _Z3_mk_fpa_is_infinite in api_fpa.o | |
| _Z3_mk_fpa_is_nan in api_fpa.o | |
| ... | |
| "ast_manager::mk_app(int, int, expr*, expr*)", referenced from: | |
| _Z3_mk_fpa_sqrt in api_fpa.o | |
| _Z3_mk_fpa_rem in api_fpa.o | |
| _Z3_mk_fpa_round_to_integral in api_fpa.o | |
| _Z3_mk_fpa_min in api_fpa.o | |
| _Z3_mk_fpa_max in api_fpa.o | |
| _Z3_mk_fpa_leq in api_fpa.o | |
| _Z3_mk_fpa_lt in api_fpa.o | |
| ... | |
| "ast_manager::mk_app(int, int, expr*, expr*, expr*)", referenced from: | |
| _Z3_mk_fpa_fp in api_fpa.o | |
| _Z3_mk_fpa_add in api_fpa.o | |
| _Z3_mk_fpa_sub in api_fpa.o | |
| _Z3_mk_fpa_mul in api_fpa.o | |
| _Z3_mk_fpa_div in api_fpa.o | |
| _mk_ite_core in api_ast.o | |
| _Z3_mk_ite in api_ast.o | |
| ... | |
| "ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*)", referenced from: | |
| _Z3_mk_set_union in api_array.o | |
| _Z3_mk_set_intersect in api_array.o | |
| _Z3_mk_set_difference in api_array.o | |
| _Z3_mk_set_complement in api_array.o | |
| _Z3_mk_set_subset in api_array.o | |
| _Z3_mk_array_ext in api_array.o | |
| _Z3_mk_as_array in api_array.o | |
| ... | |
| "ast_manager::mk_app(int, int, unsigned int, expr* const*)", referenced from: | |
| _Z3_mk_fpa_round_nearest_ties_to_even in api_fpa.o | |
| _Z3_mk_fpa_rne in api_fpa.o | |
| _Z3_mk_fpa_round_nearest_ties_to_away in api_fpa.o | |
| _Z3_mk_fpa_rna in api_fpa.o | |
| _Z3_mk_fpa_round_toward_positive in api_fpa.o | |
| _Z3_mk_fpa_rtp in api_fpa.o | |
| _Z3_mk_fpa_round_toward_negative in api_fpa.o | |
| ... | |
| "ast_manager::mk_var(unsigned int, sort*)", referenced from: | |
| _Z3_mk_bound in api_quant.o | |
| "ast_manager::mk_sort(int, int, unsigned int, parameter const*)", referenced from: | |
| _Z3_mk_array_sort in api_array.o | |
| _Z3_mk_array_sort_n in api_array.o | |
| _Z3_mk_const_array in api_array.o | |
| _mk_app_array_core in api_array.o | |
| _Z3_mk_fpa_rounding_mode_sort in api_fpa.o | |
| _Z3_mk_int_sort in api_arith.o | |
| _Z3_mk_real_sort in api_arith.o | |
| ... | |
| "ast_manager::mk_lambda(unsigned int, sort* const*, symbol const*, expr*)", referenced from: | |
| _Z3_mk_lambda in api_quant.o | |
| _Z3_mk_lambda_const in api_quant.o | |
| "ast_manager::~ast_manager()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| scoped_ptr<ast_manager>::~scoped_ptr() in api_context.o | |
| api::context::~context() in api_context.o | |
| "cmd_context::init_manager()", referenced from: | |
| _parse_smtlib2_stream in api_parsers.o | |
| "cmd_context::set_solver_factory(solver_factory*)", referenced from: | |
| _Z3_eval_smtlib2_string in api_parsers.o | |
| "cmd_context::insert(symbol const&, psort_decl*)", referenced from: | |
| _parse_smtlib2_stream in api_parsers.o | |
| "cmd_context::insert(symbol const&, func_decl*)", referenced from: | |
| _parse_smtlib2_stream in api_parsers.o | |
| "cmd_context::cmd_context(bool, ast_manager*, symbol const&)", referenced from: | |
| _Z3_fixedpoint_from_stream in api_datalog.o | |
| Z3_optimize_from_stream(_Z3_context*, _Z3_optimize*, std::__1::basic_istream<char, std::__1::char_traits<char> >&, char const*) in api_opt.o | |
| _solver_from_stream in api_solver.o | |
| _parse_smtlib2_stream in api_parsers.o | |
| _Z3_eval_smtlib2_string in api_parsers.o | |
| "cmd_context::~cmd_context()", referenced from: | |
| _Z3_fixedpoint_from_stream in api_datalog.o | |
| "func_interp::insert_entry(expr* const*, expr*)", referenced from: | |
| _Z3_func_interp_add_entry in api_model.o | |
| "func_interp::set_else(expr*)", referenced from: | |
| _Z3_add_func_interp in api_model.o | |
| _Z3_func_interp_set_else in api_model.o | |
| "func_interp::func_interp(ast_manager&, unsigned int)", referenced from: | |
| _Z3_add_func_interp in api_model.o | |
| "mk_ismt2_pp::mk_ismt2_pp(ast*, ast_manager&, unsigned int, unsigned int, char const*)", referenced from: | |
| _Z3_ast_map_to_string in api_ast_map.o | |
| _Z3_ast_vector_to_string in api_ast_vector.o | |
| _Z3_ast_to_string in api_ast.o | |
| "mk_ismt2_pp::mk_ismt2_pp(ast*, ast_manager&, params_ref const&, unsigned int, unsigned int, char const*)", referenced from: | |
| _Z3_ast_to_string in api_ast.o | |
| "mk_ismt2_pp::mk_ismt2_pp(ast*, ast_manager&, unsigned int, unsigned int, char const*)", referenced from: | |
| api::context::check_sorts(ast*) in api_context.o | |
| "mpf_manager::mk_min_exp(unsigned int)", referenced from: | |
| _Z3_fpa_get_numeral_exponent_string in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_int64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_bv in api_fpa.o | |
| "mpf_manager::mk_top_exp(unsigned int)", referenced from: | |
| _Z3_fpa_get_numeral_exponent_string in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_int64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_bv in api_fpa.o | |
| "mpf_manager::is_denormal(mpf const&)", referenced from: | |
| _Z3_fpa_get_numeral_significand_bv in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_string in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_uint64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_string in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_int64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_bv in api_fpa.o | |
| fpa_util::is_subnormal(expr*) in api_fpa.o | |
| ... | |
| "mpf_manager::set(mpf&, unsigned int, unsigned int, mpf_rounding_mode, char const*)", referenced from: | |
| _Z3_mk_numeral in api_numeral.o | |
| "mpf_manager::set(mpf&, unsigned int, unsigned int, bool, long long, unsigned long long)", referenced from: | |
| _Z3_mk_fpa_numeral_int_uint in api_fpa.o | |
| _Z3_mk_fpa_numeral_int64_uint64 in api_fpa.o | |
| "mpf_manager::set(mpf&, unsigned int, unsigned int, double)", referenced from: | |
| _Z3_mk_fpa_numeral_double in api_fpa.o | |
| "mpf_manager::set(mpf&, unsigned int, unsigned int, float)", referenced from: | |
| _Z3_mk_fpa_numeral_float in api_fpa.o | |
| "mpf_manager::set(mpf&, unsigned int, unsigned int, int)", referenced from: | |
| _Z3_mk_fpa_numeral_int in api_fpa.o | |
| "mpf_manager::is_inf(mpf const&)", referenced from: | |
| _Z3_fpa_get_numeral_significand_bv in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_string in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_uint64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_string in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_int64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_bv in api_fpa.o | |
| fpa_util::is_inf(expr*) in api_fpa.o | |
| ... | |
| "mpf_manager::is_nan(mpf const&)", referenced from: | |
| _Z3_fpa_get_numeral_sign in api_fpa.o | |
| _Z3_fpa_get_numeral_sign_bv in api_fpa.o | |
| fpa_util::is_nan(expr*) in api_fpa.o | |
| "mpf_manager::is_neg(mpf const&)", referenced from: | |
| fpa_util::is_negative(expr*) in api_fpa.o | |
| "mpf_manager::is_pos(mpf const&)", referenced from: | |
| _Z3_fpa_get_numeral_sign_bv in api_fpa.o | |
| fpa_util::is_positive(expr*) in api_fpa.o | |
| "mpf_manager::is_zero(mpf const&)", referenced from: | |
| _Z3_fpa_get_numeral_significand_bv in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_string in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_uint64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_string in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_int64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_bv in api_fpa.o | |
| fpa_util::is_zero(expr*) in api_fpa.o | |
| ... | |
| "mpf_manager::bias_exp(unsigned int, long long)", referenced from: | |
| _Z3_fpa_get_numeral_exponent_string in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_int64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_bv in api_fpa.o | |
| "mpf_manager::is_normal(mpf const&)", referenced from: | |
| _Z3_fpa_get_numeral_significand_bv in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_string in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_uint64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_string in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_int64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_bv in api_fpa.o | |
| fpa_util::is_normal(expr*) in api_fpa.o | |
| ... | |
| "mpf_manager::to_string(mpf const&)", referenced from: | |
| _Z3_get_numeral_string in api_numeral.o | |
| "mpq_manager<false>::display_decimal(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, mpq const&, unsigned int, bool)", referenced from: | |
| _Z3_fpa_get_numeral_significand_string in api_fpa.o | |
| _Z3_get_numeral_decimal_string in api_numeral.o | |
| "mpq_manager<false>::set(mpq&, char const*)", referenced from: | |
| _Z3_optimize_assert_soft in api_opt.o | |
| _Z3_rcf_mk_rational in api_rcf.o | |
| _Z3_mk_numeral in api_numeral.o | |
| "mpq_manager<false>::power(mpq const&, unsigned int, mpq&)", referenced from: | |
| _Z3_mk_bv2int in api_bv.o | |
| "mpq_manager<false>::rat_lt(mpq const&, mpq const&)", referenced from: | |
| _Z3_algebraic_lt in api_algebraic.o | |
| "mpq_manager<false>::rat_add(mpq const&, mpq const&, mpq&)", referenced from: | |
| operator+(rational const&, rational const&) in api_algebraic.o | |
| _Z3_mk_bv_numeral in api_numeral.o | |
| "mpq_manager<false>::rat_mul(mpq const&, mpq const&, mpq&)", referenced from: | |
| operator*(rational const&, rational const&) in api_algebraic.o | |
| "mpq_manager<false>::rat_sub(mpq const&, mpq const&, mpq&)", referenced from: | |
| operator-(rational const&, rational const&) in api_algebraic.o | |
| "mpq_manager<false>::mpq_manager()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| "mpq_manager<false>::~mpq_manager()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| api::context::~context() in api_context.o | |
| "mpz_manager<false>::big_compare(mpz const&, mpz const&)", referenced from: | |
| _Z3_algebraic_lt in api_algebraic.o | |
| _Z3_algebraic_eq in api_algebraic.o | |
| "mpz_manager<false>::set_big_i64(mpz&, long long)", referenced from: | |
| _Z3_mk_unsigned_int in api_numeral.o | |
| _Z3_mk_int64 in api_numeral.o | |
| "mpz_manager<false>::set_big_ui64(mpz&, unsigned long long)", referenced from: | |
| bv_util::mk_numeral(unsigned long long, unsigned int) const in api_fpa.o | |
| _Z3_mk_unsigned_int64 in api_numeral.o | |
| _Z3_get_numeral_rational in api_numeral.o | |
| "mpz_manager<false>::add(mpz const&, mpz const&, mpz&)", referenced from: | |
| _Z3_fpa_get_numeral_significand_string in api_fpa.o | |
| mpq_manager<false>::rat_add(mpq const&, mpz const&, mpq&) in api_fpa.o | |
| operator+(rational const&, rational const&) in api_algebraic.o | |
| _Z3_mk_bv_numeral in api_numeral.o | |
| "mpz_manager<false>::del(mpz&)", referenced from: | |
| _Z3_mk_fpa_numeral_float in api_fpa.o | |
| _Z3_mk_fpa_numeral_double in api_fpa.o | |
| _Z3_mk_fpa_numeral_int in api_fpa.o | |
| _Z3_mk_fpa_numeral_int_uint in api_fpa.o | |
| _Z3_mk_fpa_numeral_int64_uint64 in api_fpa.o | |
| _Z3_fpa_get_numeral_sign in api_fpa.o | |
| _Z3_fpa_get_numeral_sign_bv in api_fpa.o | |
| ... | |
| "mpz_manager<false>::div(mpz const&, mpz const&, mpz&)", referenced from: | |
| mpq_manager<false>::div(mpq const&, mpz const&, mpq&) in api_fpa.o | |
| mpq_manager<false>::rat_add(mpq const&, mpz const&, mpq&) in api_fpa.o | |
| _Z3_mk_real in api_arith.o | |
| mpq_manager<false>::div(mpq const&, mpq const&, mpq&) in api_algebraic.o | |
| "mpz_manager<false>::gcd(mpz const&, mpz const&, mpz&)", referenced from: | |
| mpq_manager<false>::div(mpq const&, mpz const&, mpq&) in api_fpa.o | |
| mpq_manager<false>::rat_add(mpq const&, mpz const&, mpq&) in api_fpa.o | |
| _Z3_mk_real in api_arith.o | |
| mpq_manager<false>::div(mpq const&, mpq const&, mpq&) in api_algebraic.o | |
| "mpz_manager<false>::mul(mpz const&, mpz const&, mpz&)", referenced from: | |
| mpq_manager<false>::div(mpq const&, mpz const&, mpq&) in api_fpa.o | |
| mpq_manager<false>::rat_add(mpq const&, mpz const&, mpq&) in api_fpa.o | |
| operator*(rational const&, rational const&) in api_algebraic.o | |
| mpq_manager<false>::div(mpq const&, mpq const&, mpq&) in api_algebraic.o | |
| "mpz_manager<false>::neg(mpz&)", referenced from: | |
| mpf_manager::powers2::operator()(unsigned int, bool) in api_fpa.o | |
| mpq_manager<false>::div(mpq const&, mpz const&, mpq&) in api_fpa.o | |
| mpq_manager<false>::div(mpq const&, mpq const&, mpq&) in api_algebraic.o | |
| "mpz_manager<false>::sub(mpz const&, mpz const&, mpz&)", referenced from: | |
| operator-(rational const&, rational const&) in api_algebraic.o | |
| "mpz_manager<false>::power(mpz const&, unsigned int, mpz&)", referenced from: | |
| mpf_manager::powers2::operator()(unsigned int, bool) in api_fpa.o | |
| "mpz_manager<false>::big_set(mpz&, mpz const&)", referenced from: | |
| _Z3_fpa_get_numeral_significand_bv in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_string in api_fpa.o | |
| mpq_manager<false>::div(mpq const&, mpz const&, mpq&) in api_fpa.o | |
| mpq_manager<false>::rat_add(mpq const&, mpz const&, mpq&) in api_fpa.o | |
| _Z3_get_numerator in api_arith.o | |
| _Z3_get_denominator in api_arith.o | |
| operator+(rational const&, rational const&) in api_algebraic.o | |
| ... | |
| "mpz_manager<false>::mpz_manager()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| "mpz_manager<false>::~mpz_manager()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| api::pmanager::~pmanager() in api_context.o | |
| api::context::~context() in api_context.o | |
| "realclosure::manager::isolate_roots(unsigned int, realclosure::num const*, svector<realclosure::num, unsigned int>&)", referenced from: | |
| _Z3_rcf_mk_roots in api_rcf.o | |
| "realclosure::manager::mk_infinitesimal(realclosure::num&)", referenced from: | |
| _Z3_rcf_mk_infinitesimal in api_rcf.o | |
| "realclosure::manager::clean_denominators(realclosure::num const&, realclosure::num&, realclosure::num&)", referenced from: | |
| _Z3_rcf_get_numerator_denominator in api_rcf.o | |
| "realclosure::manager::eq(realclosure::num const&, realclosure::num const&)", referenced from: | |
| _Z3_rcf_eq in api_rcf.o | |
| _Z3_rcf_neq in api_rcf.o | |
| "realclosure::manager::lt(realclosure::num const&, realclosure::num const&)", referenced from: | |
| _Z3_rcf_lt in api_rcf.o | |
| _Z3_rcf_gt in api_rcf.o | |
| _Z3_rcf_le in api_rcf.o | |
| _Z3_rcf_ge in api_rcf.o | |
| "realclosure::manager::add(realclosure::num const&, realclosure::num const&, realclosure::num&)", referenced from: | |
| _Z3_rcf_add in api_rcf.o | |
| "realclosure::manager::del(realclosure::num&)", referenced from: | |
| _Z3_rcf_del in api_rcf.o | |
| "realclosure::manager::div(realclosure::num const&, realclosure::num const&, realclosure::num&)", referenced from: | |
| _Z3_rcf_div in api_rcf.o | |
| "realclosure::manager::inv(realclosure::num const&, realclosure::num&)", referenced from: | |
| _Z3_rcf_inv in api_rcf.o | |
| "realclosure::manager::mul(realclosure::num const&, realclosure::num const&, realclosure::num&)", referenced from: | |
| _Z3_rcf_mul in api_rcf.o | |
| "realclosure::manager::neg(realclosure::num const&, realclosure::num&)", referenced from: | |
| _Z3_rcf_neg in api_rcf.o | |
| "realclosure::manager::set(realclosure::num&, mpq const&)", referenced from: | |
| _Z3_rcf_mk_rational in api_rcf.o | |
| "realclosure::manager::set(realclosure::num&, int)", referenced from: | |
| _Z3_rcf_mk_small_int in api_rcf.o | |
| "realclosure::manager::sub(realclosure::num const&, realclosure::num const&, realclosure::num&)", referenced from: | |
| _Z3_rcf_sub in api_rcf.o | |
| "realclosure::manager::mk_e(realclosure::num&)", referenced from: | |
| _Z3_rcf_mk_e in api_rcf.o | |
| "realclosure::manager::mk_pi(realclosure::num&)", referenced from: | |
| _Z3_rcf_mk_pi in api_rcf.o | |
| "realclosure::manager::power(realclosure::num const&, unsigned int, realclosure::num&)", referenced from: | |
| _Z3_rcf_power in api_rcf.o | |
| "realclosure::manager::is_zero(realclosure::num const&)", referenced from: | |
| _Z3_rcf_mk_roots in api_rcf.o | |
| "realclosure::manager::manager(reslimit&, mpq_manager<false>&, params_ref const&, small_object_allocator*)", referenced from: | |
| api::context::rcfm() in api_context.o | |
| "realclosure::manager::~manager()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| scoped_ptr<realclosure::manager>::~scoped_ptr() in api_context.o | |
| api::context::~context() in api_context.o | |
| api::context::rcfm() in api_context.o | |
| "th_rewriter::get_param_descrs(param_descrs&)", referenced from: | |
| _Z3_simplify_get_help in api_ast.o | |
| _Z3_simplify_get_param_descrs in api_ast.o | |
| "th_rewriter::th_rewriter(ast_manager&, params_ref const&)", referenced from: | |
| simplify(_Z3_context*, _Z3_ast*, _Z3_params*) in api_ast.o | |
| "th_rewriter::~th_rewriter()", referenced from: | |
| simplify(_Z3_context*, _Z3_ast*, _Z3_params*) in api_ast.o | |
| "th_rewriter::operator()(expr*, obj_ref<expr, ast_manager>&)", referenced from: | |
| simplify(_Z3_context*, _Z3_ast*, _Z3_params*) in api_ast.o | |
| "param_descrs::insert(char const*, cmd_arg_kind, char const*, char const*, char const*)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| pattern_inference_params_helper::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| pp_params::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| arith_rewriter_params::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| bool_rewriter_params::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| bv_rewriter_params::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| rewriter_params::collect_param_descrs(param_descrs&) in gparams_register_modules.o | |
| ... | |
| "param_descrs::param_descrs()", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| _Z3_fixedpoint_get_help in api_datalog.o | |
| _Z3_fixedpoint_get_param_descrs in api_datalog.o | |
| _Z3_fixedpoint_set_params in api_datalog.o | |
| _Z3_optimize_set_params in api_opt.o | |
| _Z3_optimize_get_param_descrs in api_opt.o | |
| _Z3_optimize_get_help in api_opt.o | |
| ... | |
| "param_descrs::~param_descrs()", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| _Z3_fixedpoint_get_help in api_datalog.o | |
| _Z3_fixedpoint_set_params in api_datalog.o | |
| Z3_param_descrs_ref::~Z3_param_descrs_ref() in api_datalog.o | |
| Z3_param_descrs_ref::~Z3_param_descrs_ref() in api_datalog.o | |
| _Z3_optimize_set_params in api_opt.o | |
| _Z3_optimize_get_help in api_opt.o | |
| ... | |
| "rewriter_tpl<beta_reducer_cfg>::rewriter_tpl(ast_manager&, bool, beta_reducer_cfg&)", referenced from: | |
| _Z3_substitute_vars in api_ast.o | |
| "rewriter_tpl<beta_reducer_cfg>::~rewriter_tpl()", referenced from: | |
| _Z3_substitute_vars in api_ast.o | |
| beta_reducer::~beta_reducer() in api_ast.o | |
| beta_reducer::~beta_reducer() in api_ast.o | |
| "scoped_timer::scoped_timer(unsigned int, event_handler*)", referenced from: | |
| _Z3_fixedpoint_query in api_datalog.o | |
| _Z3_fixedpoint_query_relations in api_datalog.o | |
| _Z3_fixedpoint_query_from_lvl in api_datalog.o | |
| _Z3_optimize_check in api_opt.o | |
| _Z3_algebraic_roots in api_algebraic.o | |
| _Z3_algebraic_eval in api_algebraic.o | |
| _tactic_apply(_Z3_context*, _Z3_tactic*, _Z3_goal*, params_ref) in api_tactic.o | |
| ... | |
| "scoped_timer::~scoped_timer()", referenced from: | |
| _Z3_fixedpoint_query in api_datalog.o | |
| _Z3_fixedpoint_query_relations in api_datalog.o | |
| _Z3_fixedpoint_query_from_lvl in api_datalog.o | |
| _Z3_optimize_check in api_opt.o | |
| _Z3_algebraic_roots in api_algebraic.o | |
| _Z3_algebraic_eval in api_algebraic.o | |
| _tactic_apply(_Z3_context*, _Z3_tactic*, _Z3_goal*, params_ref) in api_tactic.o | |
| ... | |
| "pdecl_manager::mk_psort_cnst(sort*)", referenced from: | |
| _parse_smtlib2_stream in api_parsers.o | |
| "pdecl_manager::mk_psort_user_decl(unsigned int, symbol const&, Z3_psort*)", referenced from: | |
| _parse_smtlib2_stream in api_parsers.o | |
| "scoped_ctrl_c::scoped_ctrl_c(event_handler&, bool, bool)", referenced from: | |
| _tactic_apply(_Z3_context*, _Z3_tactic*, _Z3_goal*, params_ref) in api_tactic.o | |
| simplify(_Z3_context*, _Z3_ast*, _Z3_params*) in api_ast.o | |
| _solver_check(_Z3_context*, _Z3_solver*, unsigned int, _Z3_ast* const*) in api_solver.o | |
| _Z3_solver_get_consequences in api_solver.o | |
| _Z3_solver_cube in api_solver.o | |
| "scoped_ctrl_c::~scoped_ctrl_c()", referenced from: | |
| _tactic_apply(_Z3_context*, _Z3_tactic*, _Z3_goal*, params_ref) in api_tactic.o | |
| simplify(_Z3_context*, _Z3_ast*, _Z3_params*) in api_ast.o | |
| _solver_check(_Z3_context*, _Z3_solver*, unsigned int, _Z3_ast* const*) in api_solver.o | |
| _Z3_solver_get_consequences in api_solver.o | |
| _Z3_solver_cube in api_solver.o | |
| "context_params::updt_params()", referenced from: | |
| _Z3_optimize_get_model in api_opt.o | |
| _Z3_algebraic_roots in api_algebraic.o | |
| _Z3_algebraic_eval in api_algebraic.o | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| _Z3_update_param_value in api_config_params.o | |
| init_solver(_Z3_context*, _Z3_solver*) in api_solver.o | |
| _Z3_solver_get_model in api_solver.o | |
| ... | |
| "context_params::mk_ast_manager()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| "context_params::get_solver_params(ast_manager const&, params_ref&, bool&, bool&, bool&)", referenced from: | |
| init_solver(_Z3_context*, _Z3_solver*) in api_solver.o | |
| "context_params::collect_param_descrs(param_descrs&)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "context_params::collect_solver_param_descrs(param_descrs&)", referenced from: | |
| init_solver(_Z3_context*, _Z3_solver*) in api_solver.o | |
| _Z3_solver_get_help in api_solver.o | |
| _Z3_solver_get_param_descrs in api_solver.o | |
| _Z3_solver_set_params in api_solver.o | |
| "context_params::set(char const*, char const*)", referenced from: | |
| _Z3_set_param_value in api_config_params.o | |
| _Z3_update_param_value in api_config_params.o | |
| "context_params::context_params()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| _Z3_mk_config in api_config_params.o | |
| "dyn_ack_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in api_context.o | |
| "family_manager::mk_family_id(symbol const&)", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| _Z3_mk_atmost in api_pb.o | |
| _Z3_mk_atleast in api_pb.o | |
| _Z3_mk_pble in api_pb.o | |
| _Z3_mk_pbge in api_pb.o | |
| _Z3_mk_pbeq in api_pb.o | |
| "prime_iterator::finalize()", referenced from: | |
| mem_finalize() in mem_initializer.o | |
| "tactic_manager::insert(probe_info*)", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "tactic_manager::insert(tactic_cmd*)", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| "tactic_manager::~tactic_manager()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| api::context::~context() in api_context.o | |
| "ast_translation::process(ast const*)", referenced from: | |
| _Z3_ast_vector_translate in api_ast_vector.o | |
| _Z3_translate in api_ast.o | |
| "ast_translation::~ast_translation()", referenced from: | |
| _Z3_model_translate in api_model.o | |
| _Z3_ast_vector_translate in api_ast_vector.o | |
| _Z3_translate in api_ast.o | |
| _Z3_goal_translate in api_goal.o | |
| "expr2polynomial::to_polynomial(expr*, obj_ref<polynomial::polynomial, polynomial::manager>&, _scoped_numeral<mpz_manager<false> >&)", referenced from: | |
| _Z3_algebraic_roots in api_algebraic.o | |
| _Z3_algebraic_eval in api_algebraic.o | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "expr2polynomial::to_expr(obj_ref<polynomial::polynomial, polynomial::manager> const&, bool, obj_ref<expr, ast_manager>&)", referenced from: | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "expr2polynomial::expr2polynomial(ast_manager&, polynomial::manager&, expr2var*, bool)", referenced from: | |
| _Z3_algebraic_roots in api_algebraic.o | |
| _Z3_algebraic_eval in api_algebraic.o | |
| "expr2polynomial::~expr2polynomial()", referenced from: | |
| _Z3_algebraic_roots in api_algebraic.o | |
| _Z3_algebraic_eval in api_algebraic.o | |
| "fpa_decl_plugin::is_numeral(expr*)", referenced from: | |
| _Z3_fpa_is_numeral_nan in api_fpa.o | |
| _Z3_fpa_is_numeral_inf in api_fpa.o | |
| _Z3_fpa_is_numeral_zero in api_fpa.o | |
| _Z3_fpa_is_numeral_normal in api_fpa.o | |
| _Z3_fpa_is_numeral_subnormal in api_fpa.o | |
| _Z3_fpa_is_numeral_positive in api_fpa.o | |
| _Z3_fpa_is_numeral_negative in api_fpa.o | |
| ... | |
| "fpa_decl_plugin::is_numeral(expr*, mpf&)", referenced from: | |
| _Z3_fpa_get_numeral_sign in api_fpa.o | |
| _Z3_fpa_get_numeral_sign_bv in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_bv in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_string in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_uint64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_string in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_int64 in api_fpa.o | |
| ... | |
| "fpa_decl_plugin::mk_numeral(mpf const&)", referenced from: | |
| _Z3_mk_fpa_numeral_float in api_fpa.o | |
| _Z3_mk_fpa_numeral_double in api_fpa.o | |
| _Z3_mk_fpa_numeral_int in api_fpa.o | |
| _Z3_mk_fpa_numeral_int_uint in api_fpa.o | |
| _Z3_mk_fpa_numeral_int64_uint64 in api_fpa.o | |
| _Z3_mk_numeral in api_numeral.o | |
| "fpa_decl_plugin::is_rm_numeral(expr*)", referenced from: | |
| _Z3_is_numeral_ast in api_numeral.o | |
| "fpa_decl_plugin::is_rm_numeral(expr*, mpf_rounding_mode&)", referenced from: | |
| _Z3_get_numeral_string in api_numeral.o | |
| "model_evaluator::set_model_completion(bool)", referenced from: | |
| _Z3_model_eval in api_model.o | |
| "check_sat_result::set_reason_unknown(event_handler&)", referenced from: | |
| _solver_check(_Z3_context*, _Z3_solver*, unsigned int, _Z3_ast* const*) in api_solver.o | |
| _Z3_solver_get_consequences in api_solver.o | |
| "theory_bv_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in api_context.o | |
| "algebraic_numbers::manager::eval_sign_at(obj_ref<polynomial::polynomial, polynomial::manager> const&, polynomial::var2value<algebraic_numbers::manager, algebraic_numbers::anum> const&)", referenced from: | |
| _Z3_algebraic_eval in api_algebraic.o | |
| "algebraic_numbers::manager::isolate_roots(obj_ref<polynomial::polynomial, polynomial::manager> const&, polynomial::var2value<algebraic_numbers::manager, algebraic_numbers::anum> const&, svector<algebraic_numbers::anum, unsigned int>&)", referenced from: | |
| _Z3_algebraic_roots in api_algebraic.o | |
| "algebraic_numbers::manager::eq(algebraic_numbers::anum const&, algebraic_numbers::anum const&)", referenced from: | |
| _Z3_algebraic_eq in api_algebraic.o | |
| "algebraic_numbers::manager::lt(algebraic_numbers::anum const&, algebraic_numbers::anum const&)", referenced from: | |
| _Z3_algebraic_lt in api_algebraic.o | |
| "algebraic_numbers::manager::add(algebraic_numbers::anum const&, algebraic_numbers::anum const&, algebraic_numbers::anum&)", referenced from: | |
| _Z3_algebraic_add in api_algebraic.o | |
| "algebraic_numbers::manager::del(algebraic_numbers::anum&)", referenced from: | |
| _Z3_algebraic_add in api_algebraic.o | |
| _Z3_algebraic_sub in api_algebraic.o | |
| _Z3_algebraic_mul in api_algebraic.o | |
| _Z3_algebraic_div in api_algebraic.o | |
| _Z3_algebraic_root in api_algebraic.o | |
| _Z3_algebraic_power in api_algebraic.o | |
| _Z3_algebraic_lt in api_algebraic.o | |
| ... | |
| "algebraic_numbers::manager::div(algebraic_numbers::anum const&, algebraic_numbers::anum const&, algebraic_numbers::anum&)", referenced from: | |
| _Z3_algebraic_div in api_algebraic.o | |
| "algebraic_numbers::manager::mul(algebraic_numbers::anum const&, algebraic_numbers::anum const&, algebraic_numbers::anum&)", referenced from: | |
| _Z3_algebraic_mul in api_algebraic.o | |
| "algebraic_numbers::manager::set(algebraic_numbers::anum&, mpq const&)", referenced from: | |
| _Z3_algebraic_add in api_algebraic.o | |
| _Z3_algebraic_sub in api_algebraic.o | |
| _Z3_algebraic_mul in api_algebraic.o | |
| _Z3_algebraic_div in api_algebraic.o | |
| _Z3_algebraic_root in api_algebraic.o | |
| _Z3_algebraic_power in api_algebraic.o | |
| _Z3_algebraic_lt in api_algebraic.o | |
| ... | |
| "algebraic_numbers::manager::set(algebraic_numbers::anum&, algebraic_numbers::anum const&)", referenced from: | |
| to_anum_vector(_Z3_context*, unsigned int, _Z3_ast**, _scoped_numeral_vector<algebraic_numbers::manager>&) in api_algebraic.o | |
| "algebraic_numbers::manager::sub(algebraic_numbers::anum const&, algebraic_numbers::anum const&, algebraic_numbers::anum&)", referenced from: | |
| _Z3_algebraic_sub in api_algebraic.o | |
| "algebraic_numbers::manager::root(algebraic_numbers::anum const&, unsigned int, algebraic_numbers::anum&)", referenced from: | |
| _Z3_algebraic_root in api_algebraic.o | |
| "algebraic_numbers::manager::power(algebraic_numbers::anum const&, unsigned int, algebraic_numbers::anum&)", referenced from: | |
| _Z3_algebraic_power in api_algebraic.o | |
| "algebraic_numbers::manager::is_neg(algebraic_numbers::anum const&)", referenced from: | |
| _Z3_algebraic_sign in api_algebraic.o | |
| _Z3_algebraic_root in api_algebraic.o | |
| "algebraic_numbers::manager::is_pos(algebraic_numbers::anum const&)", referenced from: | |
| _Z3_algebraic_sign in api_algebraic.o | |
| "algebraic_numbers::manager::is_zero(algebraic_numbers::anum const&)", referenced from: | |
| _Z3_algebraic_div in api_algebraic.o | |
| "algebraic_numbers::manager::get_lower(algebraic_numbers::anum const&, rational&, unsigned int)", referenced from: | |
| _Z3_get_algebraic_number_lower in api_arith.o | |
| "algebraic_numbers::manager::get_upper(algebraic_numbers::anum const&, rational&, unsigned int)", referenced from: | |
| _Z3_get_algebraic_number_upper in api_arith.o | |
| "arith_decl_plugin::mk_numeral(rational const&, bool)", referenced from: | |
| _Z3_get_algebraic_number_lower in api_arith.o | |
| _Z3_get_algebraic_number_upper in api_arith.o | |
| _Z3_get_numerator in api_arith.o | |
| _Z3_get_denominator in api_arith.o | |
| _Z3_algebraic_add in api_algebraic.o | |
| _Z3_algebraic_sub in api_algebraic.o | |
| _Z3_algebraic_mul in api_algebraic.o | |
| ... | |
| "arith_decl_plugin::mk_numeral(algebraic_numbers::anum const&, bool)", referenced from: | |
| _Z3_algebraic_add in api_algebraic.o | |
| _Z3_algebraic_sub in api_algebraic.o | |
| _Z3_algebraic_mul in api_algebraic.o | |
| _Z3_algebraic_div in api_algebraic.o | |
| _Z3_algebraic_root in api_algebraic.o | |
| _Z3_algebraic_power in api_algebraic.o | |
| _Z3_algebraic_roots in api_algebraic.o | |
| ... | |
| "expr_safe_replace::insert(expr*, expr*)", referenced from: | |
| _Z3_substitute in api_ast.o | |
| "expr_safe_replace::operator()(expr*, obj_ref<expr, ast_manager>&)", referenced from: | |
| _Z3_substitute in api_ast.o | |
| "pattern_validator::operator()(unsigned int, unsigned int, expr*, unsigned int, unsigned int)", referenced from: | |
| _mk_quantifier_ex_core in api_quant.o | |
| "theory_seq_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in api_context.o | |
| "theory_str_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in api_context.o | |
| "preprocessor_params::updt_local_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in api_context.o | |
| "theory_arith_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in api_context.o | |
| "small_object_allocator::deallocate(unsigned long, void*)", referenced from: | |
| parray_manager<ast_manager::expr_array_config>::reroot(parray_manager<ast_manager::expr_array_config>::ref&) in api_tactic.o | |
| parray_manager<ast_manager::expr_array_config>::get_values(parray_manager<ast_manager::expr_array_config>::cell*, expr**&) in api_tactic.o | |
| parray_manager<ast_manager::expr_array_config>::del(parray_manager<ast_manager::expr_array_config>::cell*) in api_tactic.o | |
| parray_manager<ast_manager::expr_array_config>::reroot(parray_manager<ast_manager::expr_array_config>::ref&) in api_goal.o | |
| parray_manager<ast_manager::expr_array_config>::get_values(parray_manager<ast_manager::expr_array_config>::cell*, expr**&) in api_goal.o | |
| parray_manager<ast_manager::expr_array_config>::del(parray_manager<ast_manager::expr_array_config>::cell*) in api_goal.o | |
| parray_manager<ast_manager::expr_array_config>::reroot(parray_manager<ast_manager::expr_array_config>::ref&) in api_solver.o | |
| ... | |
| "small_object_allocator::allocate(unsigned long)", referenced from: | |
| parray_manager<ast_manager::expr_array_config>::reroot(parray_manager<ast_manager::expr_array_config>::ref&) in api_tactic.o | |
| parray_manager<ast_manager::expr_array_config>::get_values(parray_manager<ast_manager::expr_array_config>::cell*, expr**&) in api_tactic.o | |
| parray_manager<ast_manager::expr_array_config>::reroot(parray_manager<ast_manager::expr_array_config>::ref&) in api_goal.o | |
| parray_manager<ast_manager::expr_array_config>::get_values(parray_manager<ast_manager::expr_array_config>::cell*, expr**&) in api_goal.o | |
| parray_manager<ast_manager::expr_array_config>::reroot(parray_manager<ast_manager::expr_array_config>::ref&) in api_solver.o | |
| parray_manager<ast_manager::expr_array_config>::get_values(parray_manager<ast_manager::expr_array_config>::cell*, expr**&) in api_solver.o | |
| "default_expr2polynomial::default_expr2polynomial(ast_manager&, polynomial::manager&)", referenced from: | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "default_expr2polynomial::~default_expr2polynomial()", referenced from: | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "pattern_inference_params::updt_params(params_ref const&)", referenced from: | |
| smt_params::smt_params(params_ref const&) in api_context.o | |
| "qe::mk_sat_tactic(ast_manager&, params_ref const&)", referenced from: | |
| install_tactics(tactic_manager&)::$_8::__invoke(ast_manager&, params_ref const&) in install_tactic.o | |
| "mpf::mpf()", referenced from: | |
| _Z3_mk_fpa_numeral_float in api_fpa.o | |
| _Z3_mk_fpa_numeral_double in api_fpa.o | |
| _Z3_mk_fpa_numeral_int in api_fpa.o | |
| _Z3_mk_fpa_numeral_int_uint in api_fpa.o | |
| _Z3_mk_fpa_numeral_int64_uint64 in api_fpa.o | |
| _Z3_fpa_get_numeral_sign in api_fpa.o | |
| _Z3_fpa_get_numeral_sign_bv in api_fpa.o | |
| ... | |
| "mpf::~mpf()", referenced from: | |
| _Z3_mk_fpa_numeral_float in api_fpa.o | |
| _Z3_mk_fpa_numeral_double in api_fpa.o | |
| _Z3_mk_fpa_numeral_int in api_fpa.o | |
| _Z3_mk_fpa_numeral_int_uint in api_fpa.o | |
| _Z3_mk_fpa_numeral_int64_uint64 in api_fpa.o | |
| _Z3_fpa_get_numeral_sign in api_fpa.o | |
| _Z3_fpa_get_numeral_sign_bv in api_fpa.o | |
| ... | |
| "nnf::get_param_descrs(param_descrs&)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "opt::context::add_objective(app*, bool)", referenced from: | |
| _Z3_optimize_maximize in api_opt.o | |
| _Z3_optimize_minimize in api_opt.o | |
| "opt::context::get_objective(unsigned int)", referenced from: | |
| _Z3_optimize_get_objectives in api_opt.o | |
| "opt::context::get_lower_as_num(unsigned int)", referenced from: | |
| _Z3_optimize_get_lower_as_vector in api_opt.o | |
| "opt::context::get_upper_as_num(unsigned int)", referenced from: | |
| _Z3_optimize_get_upper_as_vector in api_opt.o | |
| "opt::context::add_hard_constraint(expr*)", referenced from: | |
| _Z3_optimize_assert in api_opt.o | |
| Z3_optimize_from_stream(_Z3_context*, _Z3_optimize*, std::__1::basic_istream<char, std::__1::char_traits<char> >&, char const*) in api_opt.o | |
| "opt::context::add_soft_constraint(expr*, rational const&, symbol const&)", referenced from: | |
| _Z3_optimize_assert_soft in api_opt.o | |
| "opt::context::collect_param_descrs(param_descrs&)", referenced from: | |
| _Z3_optimize_set_params in api_opt.o | |
| _Z3_optimize_get_param_descrs in api_opt.o | |
| _Z3_optimize_get_help in api_opt.o | |
| "opt::context::get_hard_constraints(ref_vector<expr, ast_manager>&)", referenced from: | |
| _Z3_optimize_get_assertions in api_opt.o | |
| "opt::context::to_exprs(inf_eps_rational<inf_rational> const&, ref_vector<expr, ast_manager>&)", referenced from: | |
| _Z3_optimize_get_lower_as_vector in api_opt.o | |
| _Z3_optimize_get_upper_as_vector in api_opt.o | |
| "opt::context::get_lower(unsigned int)", referenced from: | |
| _Z3_optimize_get_lower in api_opt.o | |
| "opt::context::get_upper(unsigned int)", referenced from: | |
| _Z3_optimize_get_upper in api_opt.o | |
| "opt::context::context(ast_manager&)", referenced from: | |
| _Z3_mk_optimize in api_opt.o | |
| "sat::solver::solver(params_ref const&, reslimit&)", referenced from: | |
| _Z3_solver_from_file in api_solver.o | |
| "sat::solver::~solver()", referenced from: | |
| _Z3_solver_from_file in api_solver.o | |
| "smt::implied_equalities(ast_manager&, solver&, unsigned int, expr* const*, unsigned int*)", referenced from: | |
| _Z3_get_implied_equalities in api_solver.o | |
| "goal::assert_expr(expr*, dependency_manager<ast_manager::expr_dependency_config>::dependency*)", referenced from: | |
| _Z3_goal_assert in api_goal.o | |
| "goal::reset()", referenced from: | |
| _Z3_goal_reset in api_goal.o | |
| "goal::goal(ast_manager&, bool, bool)", referenced from: | |
| _Z3_solver_from_file in api_solver.o | |
| "goal::goal(ast_manager&, bool, bool, bool)", referenced from: | |
| _Z3_mk_goal in api_goal.o | |
| "goal::goal(goal const&)", referenced from: | |
| _tactic_apply(_Z3_context*, _Z3_tactic*, _Z3_goal*, params_ref) in api_tactic.o | |
| "goal::~goal()", referenced from: | |
| _Z3_probe_apply in api_tactic.o | |
| _tactic_apply(_Z3_context*, _Z3_tactic*, _Z3_goal*, params_ref) in api_tactic.o | |
| ref_buffer_core<goal, ref_unmanaged_wrapper<goal>, 16u>::~ref_buffer_core() in api_tactic.o | |
| Z3_goal_ref::~Z3_goal_ref() in api_tactic.o | |
| Z3_goal_ref::~Z3_goal_ref() in api_tactic.o | |
| _Z3_mk_goal in api_goal.o | |
| _Z3_goal_precision in api_goal.o | |
| ... | |
| "model::compress()", referenced from: | |
| _Z3_optimize_get_model in api_opt.o | |
| _Z3_solver_get_model in api_solver.o | |
| "model::model(ast_manager&)", referenced from: | |
| _Z3_mk_model in api_model.o | |
| _Z3_optimize_get_model in api_opt.o | |
| "model::operator()(expr*)", referenced from: | |
| _Z3_model_eval in api_model.o | |
| "memory::deallocate(void*)", referenced from: | |
| _Z3_mk_array_sort_n in api_array.o | |
| _Z3_mk_select_n in api_array.o | |
| _Z3_mk_store_n in api_array.o | |
| _Z3_mk_map in api_array.o | |
| vector<parameter, true, unsigned int>::expand_vector() in api_array.o | |
| core_hashtable<default_map_entry<unsigned int, mpz*>, table2map<default_map_entry<unsigned int, mpz*>, u_hash, u_eq>::entry_hash_proc, table2map<default_map_entry<unsigned int, mpz*>, u_hash, u_eq>::entry_eq_proc>::insert(_key_data<unsigned int, mpz*>&&) in api_fpa.o | |
| _Z3_mk_tuple_sort in api_datatype.o | |
| ... | |
| "memory::initialize(unsigned long)", referenced from: | |
| _Z3_mk_context in api_context.o | |
| _Z3_mk_context_rc in api_context.o | |
| _Z3_enable_trace in api_context.o | |
| _Z3_reset_memory in api_context.o | |
| _Z3_global_param_set in api_config_params.o | |
| _Z3_global_param_reset_all in api_config_params.o | |
| _Z3_global_param_get in api_config_params.o | |
| ... | |
| "memory::reallocate(void*, unsigned long)", referenced from: | |
| vector<expr*, false, unsigned int>::expand_vector() in api_array.o | |
| vector<sort*, false, unsigned int>::expand_vector() in api_array.o | |
| vector<datatype::accessor*, false, unsigned int>::expand_vector() in api_datatype.o | |
| vector<unsigned int, false, unsigned int>::expand_vector() in api_datatype.o | |
| vector<datatype::constructor*, false, unsigned int>::expand_vector() in api_datatype.o | |
| vector<symbol, false, unsigned int>::expand_vector() in api_datatype.o | |
| vector<sort*, false, unsigned int>::expand_vector() in api_datatype.o | |
| ... | |
| "memory::is_out_of_memory()", referenced from: | |
| core_hashtable<obj_map<ast, ast*>::obj_map_entry, obj_hash<obj_map<ast, ast*>::key_data>, default_eq<obj_map<ast, ast*>::key_data> >::remove_deleted_entries() in api_ast_map.o | |
| core_hashtable<default_map_entry<unsigned int, api::object*>, table2map<default_map_entry<unsigned int, api::object*>, u_hash, u_eq>::entry_hash_proc, table2map<default_map_entry<unsigned int, api::object*>, u_hash, u_eq>::entry_eq_proc>::remove_deleted_entries() in api_context.o | |
| "memory::get_allocation_size()", referenced from: | |
| _Z3_get_estimated_alloc_size in api_stats.o | |
| "memory::allocate(unsigned long)", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| gparams_register_modules() in gparams_register_modules.o | |
| vector<parameter, true, unsigned int>::expand_vector() in api_array.o | |
| vector<expr*, false, unsigned int>::expand_vector() in api_array.o | |
| vector<sort*, false, unsigned int>::expand_vector() in api_array.o | |
| mpf_manager::powers2::operator()(unsigned int, bool) in api_fpa.o | |
| core_hashtable<default_map_entry<unsigned int, mpz*>, table2map<default_map_entry<unsigned int, mpz*>, u_hash, u_eq>::entry_hash_proc, table2map<default_map_entry<unsigned int, mpz*>, u_hash, u_eq>::entry_eq_proc>::insert(_key_data<unsigned int, mpz*>&&) in api_fpa.o | |
| ... | |
| "memory::finalize()", referenced from: | |
| _Z3_reset_memory in api_context.o | |
| _Z3_finalize_memory in api_context.o | |
| "solver::assert_expr(expr*)", referenced from: | |
| _solver_from_stream in api_solver.o | |
| _Z3_solver_from_file in api_solver.o | |
| _Z3_solver_assert in api_solver.o | |
| "solver::assert_expr(expr*, expr*)", referenced from: | |
| _Z3_solver_assert_and_track in api_solver.o | |
| "solver::get_units(ast_manager&)", referenced from: | |
| _Z3_solver_get_units in api_solver.o | |
| "spacer::qe_project(ast_manager&, ref_vector<app, ast_manager>&, obj_ref<expr, ast_manager>&, ref<model>&, expr_map&)", referenced from: | |
| _Z3_qe_model_project_skolem in api_qe.o | |
| "spacer::qe_project(ast_manager&, ref_vector<app, ast_manager>&, obj_ref<expr, ast_manager>&, model&, bool, bool, bool)", referenced from: | |
| _Z3_qe_model_project in api_qe.o | |
| "spacer::compute_implicant_literals(model&, ref_vector<expr, ast_manager>&, ref_vector<expr, ast_manager>&)", referenced from: | |
| _Z3_model_extrapolate in api_qe.o | |
| "symbol::null", referenced from: | |
| Sy(_Z3_symbol*) in api_log_macros.o | |
| _Z3_fixedpoint_from_stream in api_datalog.o | |
| Z3_optimize_from_stream(_Z3_context*, _Z3_optimize*, std::__1::basic_istream<char, std::__1::char_traits<char> >&, char const*) in api_opt.o | |
| _Z3_mk_string_symbol in api_ast.o | |
| _Z3_mk_fresh_func_decl in api_ast.o | |
| _Z3_mk_fresh_const in api_ast.o | |
| _Z3_benchmark_to_smtlib_string in api_ast.o | |
| ... | |
| "symbol::symbol(char const*)", referenced from: | |
| install_tactics(tactic_manager&) in install_tactic.o | |
| _Z3_mk_tuple_sort in api_datatype.o | |
| _Z3_mk_enumeration_sort in api_datatype.o | |
| _Z3_mk_list_sort in api_datatype.o | |
| z3_replayer::imp::parse() in z3_replayer.o | |
| api::fixedpoint_context::set_state(void*) in api_datalog.o | |
| _Z3_fixedpoint_get_rule_names_along_trace in api_datalog.o | |
| ... | |
| "symbol::operator=(char const*)", referenced from: | |
| z3_replayer::imp::parse() in z3_replayer.o | |
| _Z3_benchmark_to_smtlib_string in api_ast.o | |
| "bv_util::mk_sort(unsigned int)", referenced from: | |
| _Z3_mk_bv_numeral in api_numeral.o | |
| "bv_util::bv_util(ast_manager&)", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| "datalog::dl_decl_util::mk_numeral(unsigned long long, sort*)", referenced from: | |
| api::context::mk_numeral_core(rational const&, sort*) in api_context.o | |
| "datalog::dl_decl_util::mk_sort(symbol const&, unsigned long long)", referenced from: | |
| _Z3_mk_finite_domain_sort in api_datalog.o | |
| "datalog::dl_decl_util::dl_decl_util(ast_manager&)", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| "datalog::dl_decl_plugin::dl_decl_plugin()", referenced from: | |
| api::fixedpoint_context::set_state(void*) in api_datalog.o | |
| "datalog::register_engine::register_engine()", referenced from: | |
| _Z3_mk_fixedpoint in api_datalog.o | |
| "datalog::relation_manager::register_relation_plugin_impl(datalog::relation_plugin*)", referenced from: | |
| api::fixedpoint_context::set_state(void*) in api_datalog.o | |
| "datalog::external_relation_plugin::external_relation_plugin(datalog::external_relation_context&, datalog::relation_manager&)", referenced from: | |
| api::fixedpoint_context::set_state(void*) in api_datalog.o | |
| "datalog::context::get_status()", referenced from: | |
| _Z3_fixedpoint_get_reason_unknown in api_datalog.o | |
| "datalog::context::assert_expr(expr*)", referenced from: | |
| _Z3_fixedpoint_assert in api_datalog.o | |
| _Z3_fixedpoint_from_stream in api_datalog.o | |
| "datalog::context::update_rule(expr*, symbol const&)", referenced from: | |
| _Z3_fixedpoint_update_rule in api_datalog.o | |
| "datalog::context::updt_params(params_ref const&)", referenced from: | |
| _Z3_fixedpoint_set_params in api_datalog.o | |
| "datalog::context::display_smt2(unsigned int, expr* const*, std::__1::basic_ostream<char, std::__1::char_traits<char> >&)", referenced from: | |
| api::fixedpoint_context::to_string(unsigned int, expr* const*) in api_datalog.o | |
| "datalog::context::add_invariant(func_decl*, expr*)", referenced from: | |
| _Z3_fixedpoint_add_invariant in api_datalog.o | |
| "datalog::context::ensure_engine()", referenced from: | |
| api::fixedpoint_context::set_state(void*) in api_datalog.o | |
| _Z3_fixedpoint_add_callback in api_datalog.o | |
| _Z3_fixedpoint_add_constraint in api_datalog.o | |
| "datalog::context::get_reachable(func_decl*)", referenced from: | |
| _Z3_fixedpoint_get_reachable in api_datalog.o | |
| "datalog::context::add_table_fact(func_decl*, unsigned int, unsigned int*)", referenced from: | |
| _Z3_fixedpoint_add_fact in api_datalog.o | |
| "datalog::context::collect_params(param_descrs&)", referenced from: | |
| _Z3_fixedpoint_get_help in api_datalog.o | |
| _Z3_fixedpoint_get_param_descrs in api_datalog.o | |
| _Z3_fixedpoint_set_params in api_datalog.o | |
| "datalog::context::get_num_levels(func_decl*)", referenced from: | |
| _Z3_fixedpoint_get_num_levels in api_datalog.o | |
| "datalog::context::query_from_lvl(expr*, unsigned int)", referenced from: | |
| _Z3_fixedpoint_query_from_lvl in api_datalog.o | |
| "datalog::context::get_cover_delta(int, func_decl*)", referenced from: | |
| _Z3_fixedpoint_get_cover_delta in api_datalog.o | |
| "datalog::context::register_predicate(func_decl*, bool)", referenced from: | |
| _Z3_fixedpoint_from_stream in api_datalog.o | |
| _Z3_fixedpoint_register_relation in api_datalog.o | |
| "datalog::context::get_answer_as_formula()", referenced from: | |
| _Z3_fixedpoint_get_answer in api_datalog.o | |
| "datalog::context::get_ground_sat_answer()", referenced from: | |
| _Z3_fixedpoint_get_ground_sat_answer in api_datalog.o | |
| "datalog::context::get_rules_as_formulas(ref_vector<expr, ast_manager>&, ref_vector<expr, ast_manager>&, svector<symbol, unsigned int>&)", referenced from: | |
| _Z3_fixedpoint_get_rules in api_datalog.o | |
| "datalog::context::set_predicate_representation(func_decl*, unsigned int, symbol const*)", referenced from: | |
| _Z3_fixedpoint_set_predicate_representation in api_datalog.o | |
| "datalog::context::get_rules_along_trace_as_formulas(ref_vector<expr, ast_manager>&, svector<symbol, unsigned int>&)", referenced from: | |
| _Z3_fixedpoint_get_rules_along_trace in api_datalog.o | |
| _Z3_fixedpoint_get_rule_names_along_trace in api_datalog.o | |
| "datalog::context::pop()", referenced from: | |
| _Z3_fixedpoint_pop in api_datalog.o | |
| "datalog::context::push()", referenced from: | |
| _Z3_fixedpoint_push in api_datalog.o | |
| "datalog::context::query(expr*)", referenced from: | |
| _Z3_fixedpoint_query in api_datalog.o | |
| "datalog::context::cleanup()", referenced from: | |
| _Z3_fixedpoint_query in api_datalog.o | |
| _Z3_fixedpoint_query_relations in api_datalog.o | |
| _Z3_fixedpoint_query_from_lvl in api_datalog.o | |
| "datalog::context::add_rule(expr*, symbol const&, unsigned int)", referenced from: | |
| _Z3_fixedpoint_add_rule in api_datalog.o | |
| _Z3_fixedpoint_from_stream in api_datalog.o | |
| "datalog::context::add_cover(int, func_decl*, expr*)", referenced from: | |
| _Z3_fixedpoint_add_cover in api_datalog.o | |
| "datalog::context::rel_query(unsigned int, func_decl* const*)", referenced from: | |
| _Z3_fixedpoint_query_relations in api_datalog.o | |
| "datalog::context::context(ast_manager&, datalog::register_engine_base&, smt_params&, params_ref const&)", referenced from: | |
| _Z3_mk_fixedpoint in api_datalog.o | |
| "datalog::context::~context()", referenced from: | |
| api::fixedpoint_context::~fixedpoint_context() in api_datalog.o | |
| api::fixedpoint_context::~fixedpoint_context() in api_datalog.o | |
| "gparams::get_module(char const*)", referenced from: | |
| _Z3_model_to_string in api_model.o | |
| _Z3_benchmark_to_smtlib_string in api_ast.o | |
| "gparams::register_global(param_descrs&)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "gparams::register_module(char const*, param_descrs*)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "gparams::register_module_descr(char const*, char const*)", referenced from: | |
| gparams_register_modules() in gparams_register_modules.o | |
| "gparams::set(char const*, char const*)", referenced from: | |
| _Z3_global_param_set in api_config_params.o | |
| "gparams::init()", referenced from: | |
| mem_initialize() in mem_initializer.o | |
| "gparams::reset()", referenced from: | |
| _Z3_global_param_reset_all in api_config_params.o | |
| "gparams::finalize()", referenced from: | |
| mem_finalize() in mem_initializer.o | |
| "gparams::get_value(char const*)", referenced from: | |
| _Z3_global_param_get in api_config_params.o | |
| "pb_util::mk_at_most_k(unsigned int, expr* const*, unsigned int)", referenced from: | |
| _Z3_mk_atmost in api_pb.o | |
| "pb_util::mk_at_least_k(unsigned int, expr* const*, unsigned int)", referenced from: | |
| _Z3_mk_atleast in api_pb.o | |
| "pb_util::mk_eq(unsigned int, rational const*, expr* const*, rational const&)", referenced from: | |
| _Z3_mk_pbeq in api_pb.o | |
| "pb_util::mk_ge(unsigned int, rational const*, expr* const*, rational const&)", referenced from: | |
| _Z3_mk_pbge in api_pb.o | |
| "pb_util::mk_le(unsigned int, rational const*, expr* const*, rational const&)", referenced from: | |
| _Z3_mk_pble in api_pb.o | |
| "qe_lite::qe_lite(ast_manager&, params_ref const&, bool)", referenced from: | |
| _Z3_qe_lite in api_qe.o | |
| "qe_lite::~qe_lite()", referenced from: | |
| _Z3_qe_lite in api_qe.o | |
| "qe_lite::operator()(ref_vector<app, ast_manager>&, obj_ref<expr, ast_manager>&)", referenced from: | |
| _Z3_qe_lite in api_qe.o | |
| "zstring::zstring(zstring::encoding)", referenced from: | |
| _Z3_get_string in api_seq.o | |
| "zstring::zstring(char const*, zstring::encoding)", referenced from: | |
| _Z3_mk_string in api_seq.o | |
| "datatype::decl::plugin::mk_datatypes(unsigned int, datatype::def* const*, unsigned int, sort* const*, ref_vector<sort, ast_manager>&)", referenced from: | |
| _Z3_mk_tuple_sort in api_datatype.o | |
| _Z3_mk_enumeration_sort in api_datatype.o | |
| _Z3_mk_list_sort in api_datatype.o | |
| _Z3_mk_datatype in api_datatype.o | |
| _Z3_mk_datatypes in api_datatype.o | |
| "datatype::util::is_recursive(sort*)", referenced from: | |
| _Z3_get_tuple_sort_mk_decl in api_datatype.o | |
| _Z3_get_tuple_sort_num_fields in api_datatype.o | |
| _Z3_get_tuple_sort_field_decl in api_datatype.o | |
| "datatype::util::get_constructor_is(func_decl*)", referenced from: | |
| _Z3_mk_enumeration_sort in api_datatype.o | |
| _Z3_mk_list_sort in api_datatype.o | |
| _Z3_query_constructor in api_datatype.o | |
| _Z3_get_datatype_sort_recognizer in api_datatype.o | |
| "datatype::util::get_constructor_accessors(func_decl*)", referenced from: | |
| _Z3_mk_tuple_sort in api_datatype.o | |
| _Z3_mk_list_sort in api_datatype.o | |
| _Z3_query_constructor in api_datatype.o | |
| _Z3_get_datatype_sort_constructor_accessor in api_datatype.o | |
| _Z3_get_tuple_sort_num_fields in api_datatype.o | |
| _Z3_get_tuple_sort_field_decl in api_datatype.o | |
| "datatype::util::get_datatype_constructors(sort*)", referenced from: | |
| _Z3_mk_tuple_sort in api_datatype.o | |
| _Z3_mk_enumeration_sort in api_datatype.o | |
| _Z3_mk_list_sort in api_datatype.o | |
| _Z3_mk_datatype in api_datatype.o | |
| _Z3_mk_datatypes in api_datatype.o | |
| _Z3_get_datatype_sort_num_constructors in api_datatype.o | |
| _get_datatype_sort_constructor_core in api_datatype.o | |
| ... | |
| "datatype::util::get_datatype_num_constructors(sort*)", referenced from: | |
| _Z3_get_tuple_sort_mk_decl in api_datatype.o | |
| _Z3_get_tuple_sort_num_fields in api_datatype.o | |
| _Z3_get_tuple_sort_field_decl in api_datatype.o | |
| "datatype::util::util(ast_manager&)", referenced from: | |
| _Z3_mk_list_sort in api_datatype.o | |
| _Z3_query_constructor in api_datatype.o | |
| _Z3_mk_datatype in api_datatype.o | |
| _Z3_mk_datatypes in api_datatype.o | |
| "datatype::util::~util()", referenced from: | |
| _Z3_mk_list_sort in api_datatype.o | |
| _Z3_query_constructor in api_datatype.o | |
| _Z3_mk_datatype in api_datatype.o | |
| _Z3_mk_datatypes in api_datatype.o | |
| "expr2var::expr2var(ast_manager&)", referenced from: | |
| _Z3_solver_from_file in api_solver.o | |
| "expr2var::~expr2var()", referenced from: | |
| _Z3_solver_from_file in api_solver.o | |
| "expr_map::expr_map(ast_manager&)", referenced from: | |
| _Z3_qe_model_project_skolem in api_qe.o | |
| "expr_map::~expr_map()", referenced from: | |
| _Z3_qe_model_project_skolem in api_qe.o | |
| "fpa_util::mk_float_sort(unsigned int, unsigned int)", referenced from: | |
| _Z3_mk_fpa_sort in api_fpa.o | |
| "fpa_util::mk_nan(unsigned int, unsigned int)", referenced from: | |
| _Z3_mk_fpa_nan in api_fpa.o | |
| "fpa_util::mk_ninf(unsigned int, unsigned int)", referenced from: | |
| _Z3_mk_fpa_inf in api_fpa.o | |
| "fpa_util::mk_pinf(unsigned int, unsigned int)", referenced from: | |
| _Z3_mk_fpa_inf in api_fpa.o | |
| "fpa_util::mk_nzero(unsigned int, unsigned int)", referenced from: | |
| _Z3_mk_fpa_zero in api_fpa.o | |
| "fpa_util::mk_pzero(unsigned int, unsigned int)", referenced from: | |
| _Z3_mk_fpa_zero in api_fpa.o | |
| "fpa_util::fpa_util(ast_manager&)", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| "fpa_util::~fpa_util()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| api::context::~context() in api_context.o | |
| "rational::initialize()", referenced from: | |
| mem_initialize() in mem_initializer.o | |
| "rational::power_of_two(unsigned int)", referenced from: | |
| _Z3_mk_bv_numeral in api_numeral.o | |
| "rational::g_mpq_manager", referenced from: | |
| bv_util::mk_numeral(unsigned long long, unsigned int) const in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_bv in api_fpa.o | |
| _Z3_mk_real in api_arith.o | |
| _Z3_get_algebraic_number_lower in api_arith.o | |
| _Z3_get_algebraic_number_upper in api_arith.o | |
| _Z3_get_numerator in api_arith.o | |
| _Z3_get_denominator in api_arith.o | |
| ... | |
| "rational::finalize()", referenced from: | |
| mem_finalize() in mem_initializer.o | |
| "reslimit::dec_cancel()", referenced from: | |
| _Z3_fixedpoint_query in api_datalog.o | |
| cancel_eh<reslimit>::~cancel_eh() in api_datalog.o | |
| _Z3_fixedpoint_query_relations in api_datalog.o | |
| _Z3_fixedpoint_query_from_lvl in api_datalog.o | |
| cancel_eh<reslimit>::~cancel_eh() in api_datalog.o | |
| _Z3_optimize_check in api_opt.o | |
| cancel_eh<reslimit>::~cancel_eh() in api_opt.o | |
| ... | |
| "reslimit::inc_cancel()", referenced from: | |
| cancel_eh<reslimit>::operator()(event_handler_caller_t) in api_datalog.o | |
| cancel_eh<reslimit>::operator()(event_handler_caller_t) in api_opt.o | |
| cancel_eh<reslimit>::operator()(event_handler_caller_t) in api_algebraic.o | |
| cancel_eh<reslimit>::operator()(event_handler_caller_t) in api_tactic.o | |
| cancel_eh<reslimit>::operator()(event_handler_caller_t) in api_ast.o | |
| cancel_eh<reslimit>::operator()(event_handler_caller_t) in api_polynomial.o | |
| cancel_eh<reslimit>::operator()(event_handler_caller_t) in api_solver.o | |
| ... | |
| "reslimit::inc()", referenced from: | |
| _Z3_optimize_check in api_opt.o | |
| _solver_check(_Z3_context*, _Z3_solver*, unsigned int, _Z3_ast* const*) in api_solver.o | |
| "reslimit::pop()", referenced from: | |
| _Z3_fixedpoint_query in api_datalog.o | |
| _Z3_fixedpoint_query_from_lvl in api_datalog.o | |
| _Z3_optimize_check in api_opt.o | |
| _solver_check(_Z3_context*, _Z3_solver*, unsigned int, _Z3_ast* const*) in api_solver.o | |
| _Z3_solver_get_consequences in api_solver.o | |
| _Z3_solver_cube in api_solver.o | |
| "reslimit::push(unsigned int)", referenced from: | |
| _Z3_fixedpoint_query in api_datalog.o | |
| _Z3_fixedpoint_query_from_lvl in api_datalog.o | |
| _Z3_optimize_check in api_opt.o | |
| _solver_check(_Z3_context*, _Z3_solver*, unsigned int, _Z3_ast* const*) in api_solver.o | |
| _Z3_solver_get_consequences in api_solver.o | |
| _Z3_solver_cube in api_solver.o | |
| "reslimit::cancel()", referenced from: | |
| api::context::interrupt() in api_context.o | |
| _Z3_interrupt in api_context.o | |
| "reslimit::reslimit()", referenced from: | |
| api::context::context(context_params*, bool) in api_context.o | |
| "sat2goal::sat2goal()", referenced from: | |
| _Z3_solver_from_file in api_solver.o | |
| "sat2goal::operator()(sat::solver&, atom2bool_var const&, params_ref const&, goal&, ref<sat2goal::mc>&)", referenced from: | |
| _Z3_solver_from_file in api_solver.o | |
| "seq_util::re::mk_full_seq(sort*)", referenced from: | |
| _Z3_mk_re_full in api_seq.o | |
| "seq_util::re::mk_loop(expr*, unsigned int)", referenced from: | |
| _Z3_mk_re_loop in api_seq.o | |
| "seq_util::re::mk_loop(expr*, unsigned int, unsigned int)", referenced from: | |
| _Z3_mk_re_loop in api_seq.o | |
| "seq_util::re::mk_empty(sort*)", referenced from: | |
| _Z3_mk_re_empty in api_seq.o | |
| "seq_util::str::mk_string(zstring const&)", referenced from: | |
| _Z3_mk_string in api_seq.o | |
| "parameter::~parameter()", referenced from: | |
| _Z3_mk_array_sort in api_array.o | |
| _Z3_mk_array_sort_n in api_array.o | |
| _Z3_mk_map in api_array.o | |
| _Z3_mk_const_array in api_array.o | |
| _mk_app_array_core in api_array.o | |
| _Z3_mk_as_array in api_array.o | |
| vector<parameter, true, unsigned int>::expand_vector() in api_array.o | |
| ... | |
| "qi_params::updt_params(params_ref const&)", referenced from: | |
| qi_params::qi_params(params_ref const&) in api_context.o | |
| "var_subst::operator()(expr*, unsigned int, expr* const*)", referenced from: | |
| _Z3_substitute_vars in api_ast.o | |
| "params_ref::display(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| _Z3_params_to_string in api_params.o | |
| "params_ref::get_sym(char const*, symbol const&) const", referenced from: | |
| _Z3_solver_set_params in api_solver.o | |
| "params_ref::get_bool(char const*, params_ref const&, bool) const", referenced from: | |
| _Z3_model_to_string in api_model.o | |
| _Z3_benchmark_to_smtlib_string in api_ast.o | |
| "params_ref::get_bool(char const*, bool) const", referenced from: | |
| _tactic_apply(_Z3_context*, _Z3_tactic*, _Z3_goal*, params_ref) in api_tactic.o | |
| simplify(_Z3_context*, _Z3_ast*, _Z3_params*) in api_ast.o | |
| _Z3_solver_set_params in api_solver.o | |
| _solver_check(_Z3_context*, _Z3_solver*, unsigned int, _Z3_ast* const*) in api_solver.o | |
| _Z3_solver_get_consequences in api_solver.o | |
| _Z3_solver_cube in api_solver.o | |
| "params_ref::get_uint(char const*, unsigned int) const", referenced from: | |
| _Z3_fixedpoint_query in api_datalog.o | |
| _Z3_fixedpoint_query_relations in api_datalog.o | |
| _Z3_fixedpoint_query_from_lvl in api_datalog.o | |
| _Z3_optimize_check in api_opt.o | |
| _tactic_apply(_Z3_context*, _Z3_tactic*, _Z3_goal*, params_ref) in api_tactic.o | |
| simplify(_Z3_context*, _Z3_ast*, _Z3_params*) in api_ast.o | |
| _solver_check(_Z3_context*, _Z3_solver*, unsigned int, _Z3_ast* const*) in api_solver.o | |
| ... | |
| "polynomial::manager::m() const", referenced from: | |
| _Z3_algebraic_roots in api_algebraic.o | |
| _Z3_algebraic_eval in api_algebraic.o | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "statistics::display_smt2(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| _Z3_stats_to_string in api_stats.o | |
| "statistics::get_uint_value(unsigned int) const", referenced from: | |
| _Z3_stats_get_uint_value in api_stats.o | |
| "statistics::get_double_value(unsigned int) const", referenced from: | |
| _Z3_stats_get_double_value in api_stats.o | |
| "statistics::size() const", referenced from: | |
| _Z3_stats_size in api_stats.o | |
| _Z3_stats_get_key in api_stats.o | |
| _Z3_stats_is_uint in api_stats.o | |
| _Z3_stats_is_double in api_stats.o | |
| _Z3_stats_get_uint_value in api_stats.o | |
| _Z3_stats_get_double_value in api_stats.o | |
| "statistics::get_key(unsigned int) const", referenced from: | |
| _Z3_stats_get_key in api_stats.o | |
| "statistics::is_uint(unsigned int) const", referenced from: | |
| _Z3_stats_is_uint in api_stats.o | |
| _Z3_stats_is_double in api_stats.o | |
| _Z3_stats_get_uint_value in api_stats.o | |
| _Z3_stats_get_double_value in api_stats.o | |
| "ast_manager::get_plugin(int) const", referenced from: | |
| _Z3_fpa_get_numeral_sign in api_fpa.o | |
| _Z3_fpa_get_numeral_sign_bv in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_bv in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_string in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_uint64 in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_string in api_fpa.o | |
| _Z3_fpa_get_numeral_exponent_int64 in api_fpa.o | |
| ... | |
| "ast_manager::is_pattern(expr const*) const", referenced from: | |
| _Z3_get_pattern_num_terms in api_quant.o | |
| _Z3_get_pattern in api_quant.o | |
| "ast_manager::check_sorts(ast const*) const", referenced from: | |
| api::context::check_sorts(ast*) in api_context.o | |
| "ast_manager::is_unique_value(expr*) const", referenced from: | |
| _Z3_get_ast_kind in api_ast.o | |
| "ast_manager::is_bool(expr const*) const", referenced from: | |
| _Z3_fixedpoint_assert in api_datalog.o | |
| _Z3_fixedpoint_add_rule in api_datalog.o | |
| _Z3_fixedpoint_update_rule in api_datalog.o | |
| _Z3_optimize_assert in api_opt.o | |
| _Z3_optimize_assert_soft in api_opt.o | |
| _Z3_goal_assert in api_goal.o | |
| _Z3_solver_assert in api_solver.o | |
| ... | |
| "cmd_context::find_psort_decl(symbol const&) const", referenced from: | |
| _parse_smtlib2_stream in api_parsers.o | |
| "mpq_manager<false>::to_string(mpq const&) const", referenced from: | |
| _Z3_get_decl_rational_parameter in api_ast.o | |
| _Z3_mk_bv2int in api_bv.o | |
| _Z3_get_numeral_string in api_numeral.o | |
| _Z3_get_numeral_decimal_string in api_numeral.o | |
| "mpz_manager<false>::get_uint64(mpz const&) const", referenced from: | |
| _Z3_fpa_get_numeral_significand_uint64 in api_fpa.o | |
| api::context::mk_numeral_core(rational const&, sort*) in api_context.o | |
| _Z3_get_numeral_uint64 in api_numeral.o | |
| "mpz_manager<false>::is_int64(mpz const&) const", referenced from: | |
| _Z3_get_numeral_small in api_numeral.o | |
| _Z3_get_numeral_int64 in api_numeral.o | |
| _Z3_get_numeral_rational_int64 in api_numeral.o | |
| "mpz_manager<false>::get_int64(mpz const&) const", referenced from: | |
| _Z3_get_numeral_small in api_numeral.o | |
| _Z3_get_numeral_int64 in api_numeral.o | |
| _Z3_get_numeral_rational_int64 in api_numeral.o | |
| "mpz_manager<false>::is_uint64(mpz const&) const", referenced from: | |
| _Z3_fpa_get_numeral_significand_uint64 in api_fpa.o | |
| api::context::mk_numeral_core(rational const&, sort*) in api_context.o | |
| _Z3_get_numeral_uint64 in api_numeral.o | |
| "realclosure::manager::display_decimal(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, realclosure::num const&, unsigned int) const", referenced from: | |
| _Z3_rcf_num_to_decimal_string in api_rcf.o | |
| "realclosure::manager::qm() const", referenced from: | |
| _Z3_rcf_mk_rational in api_rcf.o | |
| "realclosure::manager::display(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, realclosure::num const&, bool, bool) const", referenced from: | |
| _Z3_rcf_num_to_string in api_rcf.o | |
| "param_descrs::get_param_name(unsigned int) const", referenced from: | |
| _Z3_param_descrs_get_name in api_params.o | |
| _Z3_param_descrs_to_string in api_params.o | |
| "param_descrs::size() const", referenced from: | |
| _Z3_param_descrs_size in api_params.o | |
| _Z3_param_descrs_get_name in api_params.o | |
| _Z3_param_descrs_to_string in api_params.o | |
| "param_descrs::display(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, unsigned int, bool, bool) const", referenced from: | |
| _Z3_fixedpoint_get_help in api_datalog.o | |
| _Z3_optimize_get_help in api_opt.o | |
| _Z3_tactic_get_help in api_tactic.o | |
| _Z3_simplify_get_help in api_ast.o | |
| _Z3_solver_get_help in api_solver.o | |
| "param_descrs::get_kind(symbol const&) const", referenced from: | |
| _Z3_param_descrs_get_kind in api_params.o | |
| "param_descrs::get_descr(symbol const&) const", referenced from: | |
| _Z3_param_descrs_get_documentation in api_params.o | |
| "z3_exception::has_error_code() const", referenced from: | |
| api::context::handle_exception(z3_exception&) in api_context.o | |
| "bv_recognizers::is_bv_sort(sort const*) const", referenced from: | |
| is_bv_sort(_Z3_context*, _Z3_sort*) in api_fpa.o | |
| is_bv(_Z3_context*, _Z3_ast*) in api_fpa.o | |
| _Z3_mk_fpa_fp in api_fpa.o | |
| _Z3_mk_fpa_to_fp_bv in api_fpa.o | |
| _Z3_mk_fpa_to_fp_signed in api_fpa.o | |
| _Z3_mk_fpa_to_fp_unsigned in api_fpa.o | |
| "bv_recognizers::is_numeral(expr const*, rational&, unsigned int&) const", referenced from: | |
| _Z3_get_numeral_rational in api_numeral.o | |
| "family_manager::has_family(symbol const&) const", referenced from: | |
| api::fixedpoint_context::set_state(void*) in api_datalog.o | |
| "family_manager::get_family_id(symbol const&) const", referenced from: | |
| api::fixedpoint_context::set_state(void*) in api_datalog.o | |
| "tactic_manager::find_probe(symbol const&) const", referenced from: | |
| _Z3_mk_probe in api_tactic.o | |
| _Z3_probe_get_descr in api_tactic.o | |
| "tactic_manager::find_tactic_cmd(symbol const&) const", referenced from: | |
| _Z3_mk_tactic in api_tactic.o | |
| _Z3_tactic_get_descr in api_tactic.o | |
| "expr2polynomial::get_mapping() const", referenced from: | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "expr2polynomial::is_var(expr*) const", referenced from: | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "model_evaluator::get_model_completion() const", referenced from: | |
| _Z3_model_eval in api_model.o | |
| "algebraic_numbers::manager::display_decimal(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, algebraic_numbers::anum const&, unsigned int) const", referenced from: | |
| _Z3_get_numeral_decimal_string in api_numeral.o | |
| "arith_decl_plugin::am() const", referenced from: | |
| _Z3_get_algebraic_number_lower in api_arith.o | |
| _Z3_get_algebraic_number_upper in api_arith.o | |
| _Z3_algebraic_sign in api_algebraic.o | |
| _Z3_algebraic_add in api_algebraic.o | |
| _Z3_algebraic_sub in api_algebraic.o | |
| _Z3_algebraic_mul in api_algebraic.o | |
| _Z3_algebraic_div in api_algebraic.o | |
| ... | |
| "arith_recognizers::is_numeral(expr const*, rational&, bool&) const", referenced from: | |
| _Z3_get_numerator in api_arith.o | |
| _Z3_get_denominator in api_arith.o | |
| get_rational(_Z3_context*, _Z3_ast*) in api_algebraic.o | |
| _Z3_get_numeral_rational in api_numeral.o | |
| _Z3_get_numeral_decimal_string in api_numeral.o | |
| "arith_recognizers::is_irrational_algebraic_numeral(expr const*) const", referenced from: | |
| _Z3_is_algebraic_number in api_arith.o | |
| _Z3_get_algebraic_number_lower in api_arith.o | |
| _Z3_get_algebraic_number_upper in api_arith.o | |
| _Z3_algebraic_is_value_core in api_algebraic.o | |
| _Z3_algebraic_is_value in api_algebraic.o | |
| _Z3_algebraic_sign in api_algebraic.o | |
| _Z3_algebraic_add in api_algebraic.o | |
| ... | |
| "opt::context::to_string() const", referenced from: | |
| _Z3_optimize_to_string in api_opt.o | |
| "goal::display_dimacs(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| _Z3_goal_to_dimacs_string in api_goal.o | |
| "goal::is_decided_sat() const", referenced from: | |
| _Z3_goal_is_decided_sat in api_goal.o | |
| "goal::is_decided_unsat() const", referenced from: | |
| _Z3_goal_is_decided_unsat in api_goal.o | |
| "goal::is_cnf() const", referenced from: | |
| _Z3_goal_to_dimacs_string in api_goal.o | |
| "goal::display(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) const", referenced from: | |
| _Z3_apply_result_to_string in api_tactic.o | |
| _Z3_goal_to_string in api_goal.o | |
| "goal::num_exprs() const", referenced from: | |
| _Z3_goal_num_exprs in api_goal.o | |
| "goal::translate(ast_translation&) const", referenced from: | |
| _Z3_goal_translate in api_goal.o | |
| "model::has_uninterpreted_sort(sort*) const", referenced from: | |
| _Z3_model_get_sort_universe in api_model.o | |
| "model::copy() const", referenced from: | |
| _Z3_goal_convert_model in api_goal.o | |
| "model::translate(ast_translation&) const", referenced from: | |
| _Z3_model_translate in api_model.o | |
| "symbol::str() const", referenced from: | |
| _Z3_mk_tuple_sort in api_datatype.o | |
| _Z3_mk_enumeration_sort in api_datatype.o | |
| _Z3_fixedpoint_get_rule_names_along_trace in api_datalog.o | |
| "bv_util::mk_numeral(rational const&, sort*) const", referenced from: | |
| api::context::mk_numeral_core(rational const&, sort*) in api_context.o | |
| "bv_util::mk_numeral(rational const&, unsigned int) const", referenced from: | |
| bv_util::mk_numeral(unsigned long long, unsigned int) const in api_fpa.o | |
| _Z3_fpa_get_numeral_significand_bv in api_fpa.o | |
| "datalog::dl_decl_util::is_numeral(expr const*, unsigned long long&) const", referenced from: | |
| _Z3_get_numeral_rational in api_numeral.o | |
| "datalog::dl_decl_util::try_get_size(sort const*, unsigned long long&) const", referenced from: | |
| _Z3_get_finite_domain_sort_size in api_datalog.o | |
| api::context::mk_numeral_core(rational const&, sort*) in api_context.o | |
| "datalog::dl_decl_util::is_numeral_ext(expr*) const", referenced from: | |
| _Z3_is_numeral_ast in api_numeral.o | |
| "datalog::context::collect_statistics(statistics&) const", referenced from: | |
| _Z3_fixedpoint_get_statistics in api_datalog.o | |
| "zstring::encode() const", referenced from: | |
| _Z3_get_string in api_seq.o | |
| "datatype::decl::plugin::u() const", referenced from: | |
| _Z3_mk_tuple_sort in api_datatype.o | |
| _Z3_mk_enumeration_sort in api_datatype.o | |
| _Z3_mk_list_sort in api_datatype.o | |
| mk_datatype_decl(_Z3_context*, _Z3_symbol*, unsigned int, _Z3_constructor**) in api_datatype.o | |
| _Z3_get_datatype_sort_num_constructors in api_datatype.o | |
| _get_datatype_sort_constructor_core in api_datatype.o | |
| _Z3_get_datatype_sort_recognizer in api_datatype.o | |
| ... | |
| "expr2var::to_var(expr*) const", referenced from: | |
| _Z3_polynomial_subresultants in api_polynomial.o | |
| "fpa_util::get_ebits(sort*) const", referenced from: | |
| _Z3_mk_fpa_nan in api_fpa.o | |
| _Z3_mk_fpa_inf in api_fpa.o | |
| _Z3_mk_fpa_zero in api_fpa.o | |
| _Z3_mk_fpa_numeral_float in api_fpa.o | |
| _Z3_mk_fpa_numeral_double in api_fpa.o | |
| _Z3_mk_fpa_numeral_int in api_fpa.o | |
| _Z3_mk_fpa_numeral_int_uint in api_fpa.o | |
| ... | |
| "fpa_util::get_sbits(sort*) const", referenced from: | |
| _Z3_mk_fpa_nan in api_fpa.o | |
| _Z3_mk_fpa_inf in api_fpa.o | |
| _Z3_mk_fpa_zero in api_fpa.o | |
| _Z3_mk_fpa_numeral_float in api_fpa.o | |
| _Z3_mk_fpa_numeral_double in api_fpa.o | |
| _Z3_mk_fpa_numeral_int in api_fpa.o | |
| _Z3_mk_fpa_numeral_int_uint in api_fpa.o | |
| ... | |
| "seq_util::str::is_string(expr const*, zstring&) const", referenced from: | |
| _Z3_get_string in api_seq.o | |
| "typeinfo for z3_exception", referenced from: | |
| GCC_except_table0 in api_array.o | |
| GCC_except_table2 in api_array.o | |
| GCC_except_table3 in api_array.o | |
| GCC_except_table4 in api_array.o | |
| GCC_except_table5 in api_array.o | |
| GCC_except_table6 in api_array.o | |
| GCC_except_table7 in api_array.o | |
| ... | |
| "typeinfo for rewriter_core", referenced from: | |
| typeinfo for rewriter_tpl<beta_reducer_cfg> in api_ast.o | |
| "typeinfo for default_exception", referenced from: | |
| vector<parameter, true, unsigned int>::expand_vector() in api_array.o | |
| vector<expr*, false, unsigned int>::expand_vector() in api_array.o | |
| vector<sort*, false, unsigned int>::expand_vector() in api_array.o | |
| vector<datatype::accessor*, false, unsigned int>::expand_vector() in api_datatype.o | |
| vector<unsigned int, false, unsigned int>::expand_vector() in api_datatype.o | |
| vector<datatype::constructor*, false, unsigned int>::expand_vector() in api_datatype.o | |
| vector<symbol, false, unsigned int>::expand_vector() in api_datatype.o | |
| ... | |
| "typeinfo for z3_error", referenced from: | |
| z3_replayer::imp::parse() in z3_replayer.o | |
| GCC_except_table33 in z3_replayer.o | |
| "vtable for default_exception", referenced from: | |
| vector<parameter, true, unsigned int>::expand_vector() in api_array.o | |
| default_exception::~default_exception() in api_array.o | |
| vector<expr*, false, unsigned int>::expand_vector() in api_array.o | |
| vector<sort*, false, unsigned int>::expand_vector() in api_array.o | |
| vector<datatype::accessor*, false, unsigned int>::expand_vector() in api_datatype.o | |
| default_exception::~default_exception() in api_datatype.o | |
| vector<unsigned int, false, unsigned int>::expand_vector() in api_datatype.o | |
| ... | |
| NOTE: a missing vtable usually means the first non-inline virtual member function has no definition. | |
| "vtable for z3_error", referenced from: | |
| z3_replayer::imp::parse() in z3_replayer.o | |
| NOTE: a missing vtable usually means the first non-inline virtual member function has no definition. | |
| "operator<<(std::__1::basic_ostream<char, std::__1::char_traits<char> >&, mk_ismt2_pp const&)", referenced from: | |
| _Z3_ast_map_to_string in api_ast_map.o | |
| _Z3_ast_vector_to_string in api_ast_vector.o | |
| _Z3_ast_to_string in api_ast.o | |
| api::context::check_sorts(ast*) in api_context.o | |
| ld: symbol(s) not found for architecture x86_64 | |
| clang: error: linker command failed with exit code 1 (use -v to see invocation) | |
| make: *** [libz3.dylib] Error 1 | |
| error: Unable to build Z3. | |
| ---------------------------------------- | |
| Command "/usr/local/opt/python/bin/python3.7 -u -c "import setuptools, tokenize;__file__='/private/tmp/pip-install-am0j8884/z3-solver/setup.py';f=getattr(tokenize, 'open', open)(__file__);code=f.read().replace('\r\n', '\n');f.close();exec(compile(code, __file__, 'exec'))" install --record /private/tmp/pip-record-5clbyaoq/install-record.txt --single-version-externally-managed --compile --user --prefix=" failed with error code 1 in /private/tmp/pip-install-am0j8884/z3-solver/ | |
| ``` |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment