mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity
19464 commits 23 branches 48 tags 157 MiB
Commit graph

2586 commits

Author SHA1 Message Date
Nuno Lopes fcc7b25c19 remove a few string copies 2023-12-19 14:34:37 +00:00
Nikolaj Bjorner 575538d325 follow error message to put dependencies in setup args 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-08 18:38:29 -08:00
Nikolaj Bjorner 4123405d17 add version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-08 15:50:09 -08:00
Nikolaj Bjorner 6282f40255 try add name to project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-08 14:57:45 -08:00
Nikolaj Bjorner 7e716f7cfe try fix suggested in #7041 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-08 13:12:05 -08:00
Nikolaj Bjorner 6cd619d377 kludge to fixup osver in python for Mac 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-08 11:39:55 -08:00
Nikolaj Bjorner 111ce01702 update path reference to readme 2023-12-05 13:47:05 -08:00
Nikolaj Bjorner d566eb3df7 include readme in package 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-05 13:04:25 -08:00
Nikolaj Bjorner 76c05f171a specify a readme file with the nuget package 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-05 12:32:30 -08:00
Asger Hautop Drewsen a9513c1998
Improve BoolRef addition (#7045) 2023-12-05 09:12:25 -08:00
Asger Hautop Drewsen 764f0d54a4
Overload xor operator for BoolRef (#7043) 2023-12-05 07:48:57 -08:00
Andrey Andreyevich Bienkowski 18f14921ba
Clarify optimizer guarantees (#7030) 
* Clarify optimizer guarantees (python)

* Clarify optimization guarantees (OCaml)

* Clarify optimizer guarantees (java)

* Clarify optimizer guarantees (.net)
 2023-12-04 09:32:26 -08:00
Alper Altuntas d540d881ef
Add __enter__ and __exit__ methods to Solver class (#7025) 
To enable the usage of the with statement for the Solver class
instances, this commit adds __enter__ and __exit__ methods.
The with statement should offer a more concise and safer
alternative to explicit usage of push() and pop() methods.
 2023-11-30 08:35:08 -08:00
Nikolaj Bjorner f36f21fa8c add comments for API versions of bit-vector overflow/underflow checks for #7011 2023-11-28 13:36:41 -08:00
Nikolaj Bjorner f90b10a0c8 fix #7012 
omitting constructor, simplifying operator definitions, omitting incorrect type annotations
 2023-11-28 13:26:10 -08:00
Bruce Mitchener 9d1ceab1f2
cmake: Use FindPython3. (#7019) 
`FindPythonInterp` has been deprecated for a long time and is more
verbal about that deprecation now.

The build system no longer uses `PYTHON_EXECUTABLE` but instead uses
`Python3_EXECUTABLE`.
 2023-11-27 11:20:21 +01:00
Bruce Mitchener 2354998cd2
z3.h: Don't include stdio.h (#7014) 
This doesn't seem to actually be used or needed here.
 2023-11-24 16:46:32 +01:00
Christoph M. Wintersteiger 16753e43f1
Add accessors for RCF numeral internals (#7013) 2023-11-23 17:54:23 +01:00
Nikolaj Bjorner 9382b96a32 add API to access symbols associated with quantifiers 2023-11-19 16:30:09 -08:00
Nikolaj Bjorner 32f8705ac3 #7001 - align is_numeral without to behavior if is_numeral with return numeral. 2023-11-19 10:43:14 -08:00
Nikolaj Bjorner 35bc522dae #7003 
minor tweaks to gomory and reset n3 within loop (but the entire function is dead code).
 2023-11-19 09:59:44 -08:00
Christoph M. Wintersteiger 36382ccb57
Fix memory and concurrency issues in OCaml API (#6992) 
* Fix memory and concurrency issues in OCaml API

* Undo locking changes
 2023-11-16 18:28:12 -08:00
Nikolaj Bjorner f1a39b8884 add comment regarding usage model for flush_objects() to relate with pr #6992 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-15 11:54:59 -08:00
Nikolaj Bjorner 37b283fab9 use python3 in nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-14 08:54:10 -08:00
Christoph M. Wintersteiger 3af2b36cd7
Add Z3_solver_interrupt to OCaml API (#6976) 2023-10-31 08:48:06 -07:00
Bruce Mitchener 236afeb8cb
docs: More intra-doc linking, bit of formatting. (#6963) 2023-10-25 10:07:03 -07:00
dependabot[bot] 8b04049069
Bump @babel/traverse from 7.19.4 to 7.23.2 in /src/api/js (#6954) 
Bumps [@babel/traverse](https://github.com/babel/babel/tree/HEAD/packages/babel-traverse) from 7.19.4 to 7.23.2.
- [Release notes](https://github.com/babel/babel/releases)
- [Changelog](https://github.com/babel/babel/blob/main/CHANGELOG.md)
- [Commits](https://github.com/babel/babel/commits/v7.23.2/packages/babel-traverse)

---
updated-dependencies:
- dependency-name: "@babel/traverse"
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2023-10-23 15:29:42 -07:00
LufyCZ 19e921290e
increase wasm stack size (#6931) 2023-10-06 11:49:54 +09:00
Christoph M. Wintersteiger 23de8056d7
Add RCF functions to OCaml API (#6932) 2023-10-06 11:49:22 +09:00
Nuno Lopes ff33fa355a fix debug single-thread build 2023-09-18 09:44:37 +01:00
Bruce Mitchener 8cc6969510
Remove Z3_literals remnants. (#6829) 
The bulk of the functionality using these was removed between
Z3 4.4.1 and 4.5.0, back in 2015.

Co-authored-by: Bruce Mitchener <bruce.mitchener@configura.com>
 2023-07-23 19:38:57 -07:00
Nikolaj Bjorner e8a38c5482 build fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-18 19:14:45 -07:00
Nikolaj Bjorner 3d8f75b3d8 enable on-clause with dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-18 16:59:02 -07:00
Nikolaj Bjorner 939bf1c725 wip - alpha support for polymorphism 
An initial update to support polymorphism from SMTLIB3 and the API (so far C, Python).

The WIP SMTLIB3 format is assumed to be supporting the following declaration

```
(declare-type-var A)
```
Whenever A is used in a type signature of a function/constant or bound quantified variable, it is taken to mean that all instantiations of A are included in the signature and assertions.
For example, if the function f is declared with signature A -> A, then there is a version of f for all instances of A.
The semantics of polymorphism appears to follow previous proposals: the instances are effectively different functions.
This may clash with some other notions, such as the type signature forall 'a . 'a -> 'a would be inhabited by a unique function (the identity), while this is not enforced in this version (and hopefully never because it is more busy work).

The C API has the function 'Z3_mk_type_variable' to create a type variable and applying functions modulo polymorphic type signatures is possible.
The kind Z3_TYPE_VAR is added to sort discriminators.

This version is considered as early alpha. It passes a first rudimentary unit test involving quantified axioms, declare-fun, define-fun, and define-fun-rec.
 2023-07-12 18:09:02 -07:00
THE Spellchecker dc0887db5a
Typo Fixes (#6803) 2023-07-09 11:56:10 -07:00
Clemens Eisenhofer 4cb158a79b
User Propagator: Return if propagated lemma is redundant (#6791) 
* Give users ability to see if propagation failed

* Skip propagations in the new core if they are already satisfied
 2023-07-07 09:58:41 -07:00
Nikolaj Bjorner 68663fd97a fix indentation for python file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-06 09:02:58 -07:00
Nikolaj Bjorner 3782eb1be4 fix #6785 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-05 19:50:07 -07:00
Clemens Eisenhofer d42693d5b5
Equalities in C# UP-Propagation (#6786) 
* Query Boolean Assignment in the UP

* UP's decide ref arguments => next_split

* Fixed wrapper

* More fixes

* Equalities in C# UP-Propagation

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-26 10:59:57 -07:00
Nikolaj Bjorner b451735aa0 fix #6778 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-25 21:08:13 -07:00
Nikolaj Bjorner 81068981aa fix #6746, fix type errors in java bindings 2023-06-03 09:41:29 +02:00
Clemens Eisenhofer 82667bd86b
Fix UP's decide callback (#6707) 
* Query Boolean Assignment in the UP

* UP's decide ref arguments => next_split

* Fixed wrapper

* More fixes
 2023-06-02 09:52:54 +02:00
Nikolaj Bjorner 621f1f8a85 sanity check parameters #6737 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-30 09:44:06 +02:00
Manuel Carrasco 230306ddfc
Add solver::interrupt to Python's API. (#6739) 2023-05-28 21:04:36 +02:00
ditto 11264c38d8
Java user propagator interface (#6733) 
* Java API: user propagator interface

* Java API: improved user propagator interface

* Java API: Add UserPropagatorBase.java

* Remove redundant header file

* Initialize `JavaInfo` object and error handling

* Native.UserPropagatorBase implements AutoCloseable

* Add Override annotation
 2023-05-24 18:27:28 +01:00
Nikolaj Bjorner 2c21072c99 remove stub class, it may as well go into NativeStatic.txt as C++ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-22 18:23:10 +01:00
Nikolaj Bjorner b93529997e more stubs #6097 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-22 16:25:54 +01:00
Nikolaj Bjorner 7963ecaf63 stubs for #6097 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-22 16:21:34 +01:00
Guillaume Bagan 0c9a5f69fd
JS/TS: add Optimize class (#6712) 
* implement  Optimize class for the high level Typescript API

* javascript and wasm: add _malloc to exported functions

fix the bug https://github.com/Z3Prover/z3/issues/6709

* javascript: add tests for the Optimize class

* javascript: no reason that minimize and optimize must be constants
 2023-05-06 11:53:43 -07:00
Nikolaj Bjorner f17691715b make default argument to ensure_def and mk_def explicit 
- insert also macro definitions into models
 2023-05-02 12:18:31 -07:00
Nikolaj Bjorner ccc4f2d382 fix #6682 2023-04-11 05:10:03 -07:00
Nikolaj Bjorner b386b84f34 #6658 2023-03-31 02:56:44 -07:00
권승완 6670807103
update ocaml binding to support more string apis (#6656) 2023-03-29 05:49:33 -07:00
Patrick LaFontaine 0a59617bac
Fix Ocaml bindings FuncEntry to_string (#6639) 
Hello, I was looking at the different api string conversions for FuncEntry and I believe that the ml version is incorrect? Clearly we want the argument(`c`) to be comma separated from the accumulated string `p`. The current implementation just so happens to have most of the arguments separated, but the order is flipped and one of the commas is misplaced.
 2023-03-27 13:04:32 -07:00
Nikolaj Bjorner b4ad747e0b fix #6644 2023-03-27 09:00:38 -07:00
Nikolaj Bjorner cd2ea6b703 add parameter access to C++ API 2023-03-25 18:14:08 +01:00
Nikolaj Bjorner d1c7ff1a36 add unconstrained elimination for sequences 2023-03-20 17:07:04 +01:00
Declan Hwang cf4df08fd0
fix typo (#6628) 2023-03-09 09:29:30 -08:00
Bram V 1612b57e1a
Make all methods show in java API (#6626) 
* Make all methods show in java API

* Add final modifier to all generic methods
 2023-03-08 13:43:51 -08:00
Julian Parsert 6e7d80633d
Documentation on how to add z3 to CMake project using FetchContent and documentation to recdef function. (#6613) 
* Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort*

* added documentation to recdef function

* added a section in the README-CMake.md that explains how z3 can be added to a CMake project as a dependency

---------

Co-authored-by: Julian Parsert <julian.parsert@uibk.ac.at>
 2023-02-28 11:44:21 -08:00
Nikolaj Bjorner 9ce5fe707d track assumptions when parsing into a solver. This enables solver.from_file/solver.from_string to support assumptions/cores #6587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-14 11:09:11 -08:00
Walden Yan ede9e5ffc2
[WIP] More TS Binding Features (#6412) 
* feat: basic quantfier support

* feat: added isQuantifier

* feat: expanded functions

* wip: (lambda broken)

* temp fix to LambdaImpl typing issue

* feat: function type inference

* formatting with prettier

* fix: imported from invalid module

* fix isBool bug and dumping to smtlib

* substitution and model.updateValue

* api to add custom func interps to model

* fix: building

* properly handling uint32 -> number conversion in z3 TS wrapper

* added simplify

* remame Add->Sum and Mul->Product

* formatting
 2023-02-11 15:48:29 -08:00
Nikolaj Bjorner 46c8d78ece fixes for #6577 
- the literal false should not appear in clauses
- the literal true forces a tautology
- fix early return in is_cnf check. It should check all clauses for nested Booleans.
 2023-02-11 09:33:42 -08:00
Julian Parsert d52e893528
Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort* (#6576) 
Co-authored-by: Julian Parsert <julian.parsert@uibk.ac.at>
 2023-02-10 10:00:26 -08:00
Frederick Robinson be44ace995
fix typo (#6569) 2023-02-03 13:08:35 -08:00
Nikolaj Bjorner 4143c54257 add simplifier to java API 2023-02-02 19:06:26 -08:00
Nikolaj Bjorner 2e068e3f56 add simplifiers to .net API 2023-02-02 17:41:00 -08:00
Nikolaj Bjorner 19fed09122 protecting add_simplifier API against mis-use 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 08:35:32 -08:00
Nikolaj Bjorner 63c0f35978 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:27:17 -08:00
Nikolaj Bjorner d51d518f96 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:24:45 -08:00
Nikolaj Bjorner 1289937d1a update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:19:41 -08:00
Nikolaj Bjorner 9a94a9aa6f update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:14:24 -08:00
Nikolaj Bjorner 17bae9b4c1 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:09:37 -08:00
Nikolaj Bjorner 162fa3dc96 disambiguate overloaded with for Julia bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:06:20 -08:00
Nikolaj Bjorner 4c6d44f974 add ocaml signature for simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 18:58:18 -08:00
Nikolaj Bjorner 550619bfcf add API for creating and attaching simplifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 17:06:03 -08:00
Nikolaj Bjorner d263b373ed update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 12:19:33 -08:00
Nikolaj Bjorner 971b9d4081 fix #6564 
fixes to simplifier command front-end
 2023-01-31 09:32:34 -08:00
Nikolaj Bjorner 6a7343aab4 update julia bindings to use 64-bit mk_real (real_val) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 13:06:41 -08:00
Nikolaj Bjorner fa72ec5405 switch to expose fresh function instead of changing legacy function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 13:05:34 -08:00
Nikolaj Bjorner 3f1b7866ca convert caml mk_real to int64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 03:53:42 -08:00
Nikolaj Bjorner 4601d1d664 fix #6550 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 03:37:09 -08:00
Nikolaj Bjorner 7d364bf786 Allow building AC functions without requiring arity check from API 2023-01-22 14:39:58 -08:00
Nikolaj Bjorner 523a3f34b0 change to manylinux2014 in setup.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-19 17:27:07 -08:00
dependabot[bot] a4f2a1bb2e
Bump json5 from 2.2.1 to 2.2.3 in /src/api/js (#6527) 
Bumps [json5](https://github.com/json5/json5) from 2.2.1 to 2.2.3.
- [Release notes](https://github.com/json5/json5/releases)
- [Changelog](https://github.com/json5/json5/blob/main/CHANGELOG.md)
- [Commits](https://github.com/json5/json5/compare/v2.2.1...v2.2.3)

---
updated-dependencies:
- dependency-name: json5
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
 2023-01-09 09:16:55 +00:00
Nikolaj Bjorner d4490738bc Merge branch 'master' of https://github.com/z3prover/z3 2023-01-02 16:49:43 -08:00
Nikolaj Bjorner ea0d09b6c8 add pointer to build parameters to README #6518 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-02 16:49:31 -08:00
Walden Yan dbf93c5fbd
Fixing array select for lambda expressions in Python API (#6516) 
* fix: making array select work for lambda expressions

* more elegant solution
 2023-01-01 15:27:54 -08:00
Nikolaj Bjorner f6d411d54b experimental feature to access congruence closure of SimpleSolver 
This update includes an experimental feature to access a congruence closure data-structure after search.
It comes with several caveats as pre-processing is free to eliminate terms. It is therefore necessary to use a solver that does not eliminate the terms you want to track for congruence of. This is partially addressed by using SimpleSolver or incremental mode solving.

```python
from z3 import *
s = SimpleSolver()
x, y, z = Ints('x y z')
s.add(x == y)
s.add(y == z)
s.check()
print(s.root(x), s.root(y), s.root(z))
print(s.next(x), s.next(y), s.next(z))
```
 2022-12-30 21:41:27 -08:00
Nikolaj Bjorner 7cc58c9cc3 Merge branch 'master' of https://github.com/z3prover/z3 2022-12-27 20:19:39 -08:00
Nikolaj Bjorner ec74a87423 fix #6510 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-27 20:19:26 -08:00
Nikolaj Bjorner 3e8cbb6611 #5884 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-27 18:07:57 -08:00
Nikolaj Bjorner 8d332cc3a1
#6508 (#6509) 2022-12-26 15:42:04 -08:00
Nikolaj Bjorner 6fab4fec23
#6508 2022-12-26 15:36:58 -08:00
Nikolaj Bjorner 8efaaaf249 Fix #6503 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-25 17:29:06 -08:00
Nikolaj Bjorner c4b2acac24 add missing error checking #6492 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-14 09:27:43 -08:00
Nikolaj Bjorner cd3d38caf7 sort out terminology/add explanations, add shortcut to C++, fix #6491 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-13 16:17:38 -08:00
Nikolaj Bjorner 1434c7d394 #6059 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-09 08:50:32 -08:00
Nikolaj Bjorner 4a451b10d8 add custom coercion for floats. fix #6482 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-07 09:07:13 -08:00
Nikolaj Bjorner 5c5673bc09 make sure parser context within solver object has its parameters updated 
this is to enable use cases like:

```
from z3 import *

s = Solver()
OnClause(s, print)
s.set("solver.proof.check", False)
s.from_file("../satproof.smt2")
```

instead of setting global parameters before the proof replay is initialized.
 2022-11-23 11:37:23 +07:00
Nikolaj Bjorner fcaa85d7a8 #6456 - elaborate on error message 2022-11-20 11:27:39 +07:00
Nikolaj Bjorner 86f3702403 prevent re-declaration of enumeration sort names 
preventing redeclaration of all ADT cases is not part of this update.
 2022-11-19 19:46:34 +07:00
Nikolaj Bjorner 3f2bbe5589 harness del_object #6452 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-14 08:54:08 -08:00
Nikolaj Bjorner ff68df3451 update output of z3 doc 2022-11-08 16:10:50 -08:00
Nikolaj Bjorner 4c1a3fab64 fix #6442 2022-11-05 23:15:03 -07:00
Nikolaj Bjorner 84af521514 fixes #6439 #6436 2022-11-04 09:36:06 -07:00
Facundo Domínguez 91cdc082c4
Optimize calls to Z3_eval_smtlib2_string (#6422) 
* Allow reseting the stream of smt2::scanner

* Put the parser of parse_smt2_commands in the cmd_context

* Move parser streams to cmd_context

* Move parser fields from cmd_context to api::context

* Move forward declarations from cmd_context.h to api_context.h

* Change parse_smt2_commands_with_parser to use *& instead of **

* Add tests for Z3_eval_smtlib2_string

* Don't reuse the streams in Z3_eval_smtlib2_string

* Fix indentation

* Add back unnecessary deleted line

Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
 2022-10-28 13:57:22 -07:00
Nuno Lopes 1720addc4e remove a bunch of string copies in the API 
thanks to C++20
 2022-10-26 18:22:55 +01:00
Nikolaj Bjorner 2f1514a259 initialization of proof_cmds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 08:38:23 -07:00
Nikolaj Bjorner 65ea4925b3 initialization of proof_cmds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 08:37:21 -07:00
Nikolaj Bjorner f6595c161f add examples with proof replay 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-19 17:43:56 -07:00
Nikolaj Bjorner 4c79e63c1b Update parse-api.ts 2022-10-19 12:52:58 -07:00
Nikolaj Bjorner 07dd1065db added API to monitor clause inferences 
See RELEASE_NOTES for more information
examples pending.
 2022-10-19 08:34:55 -07:00
Walden Yan f175fcbb54
JS/TS API Array support (#6393) 
* feat: basic array support

Still need deeper type support for Arrays

* fixed broken format rules

* spaces inside curly

* feat: range sort type inference

* feat: better type inference in model eval

* doc: fixed some incorrect documentation

* feat: domain type inference

* feat: addressed suggestions

* feat: addressed suggestions

* chore: moved ts-expect from deps to dev-deps

* test: added z3guide examples

* fix: removed ts-expect from dependencies again

* docs: fixed some documentation
 2022-10-17 11:10:36 -07:00
Nikolaj Bjorner 541aba308c fix #6401 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-17 10:27:15 -07:00
Nikolaj Bjorner ddf4895c2f admit timeouts and other resource limits for get-core #6310 2022-10-12 12:09:52 +02:00
Nuno Lopes 24ff0f2d36 attempt to fix cmake build 2022-10-01 21:48:27 +01:00
Nikolaj Bjorner 107981f099 update proof formats for new core 
- update proof format for quantifier instantiation to track original literals
- update proof replay tools with ability to extract proof object

The formats and features are subject to heavy revisions.

Example
```
(set-option :sat.euf true)
(set-option :sat.smt.proof eufproof.smt2)
(declare-fun f (Int) Int)
(declare-const x Int)
(assert (or (= (f (f (f x))) x) (= (f (f x)) x)))
(assert (not (= (f (f (f (f (f (f x)))))) x)))
(check-sat)
```

eufproof.smt2 is:
```
(declare-fun x () Int)
(declare-fun f (Int) Int)
(define-const $24 Int (f x))
(define-const $25 Int (f $24))
(define-const $26 Int (f $25))
(define-const $27 Bool (= $26 x))
(define-const $28 Bool (= $25 x))
(assume $27 $28)
(define-const $30 Int (f $26))
(define-const $31 Int (f $30))
(define-const $32 Int (f $31))
(define-const $33 Bool (= $32 x))
(assume (not $33))
(declare-fun rup () Proof)
(infer (not $33) rup)
(declare-fun euf (Bool Bool Proof Proof Proof Proof) Proof)
(declare-fun cc (Bool) Proof)
(define-const $42 Bool (= $32 $30))
(define-const $43 Proof (cc $42))
(define-const $40 Bool (= $31 $24))
(define-const $41 Proof (cc $40))
(define-const $38 Bool (= $30 $25))
(define-const $39 Proof (cc $38))
(define-const $36 Bool (= $24 $26))
(define-const $37 Proof (cc $36))
(define-const $34 Bool (not $33))
(define-const $44 Proof (euf $34 $28 $37 $39 $41 $43))
(infer (not $28) $33 $44)
(infer (not $28) rup)
(infer $27 rup)
(declare-fun euf (Bool Bool Proof Proof Proof) Proof)
(define-const $49 Bool (= $32 $26))
(define-const $50 Proof (cc $49))
(define-const $47 Bool (= $31 $25))
(define-const $48 Proof (cc $47))
(define-const $45 Bool (= $24 $30))
(define-const $46 Proof (cc $45))
(define-const $51 Proof (euf $34 $27 $46 $48 $50))
(infer $33 $51)
(infer rup)
```

Example of inspecting proof from Python:

```
from z3 import *

def parse(file):
    s = Solver()
    set_option("solver.proof.save", True)
    set_option("solver.proof.check", False)
    s.from_file(file)
    for step in s.proof().children():
        print(step)

parse("../eufproof.smt2")
```

Proof checking (self-validation) is on by default.
Proof saving is off by default.

You can use the proof logs and the proof terms to retrieve quantifier instantiations from the new core.

The self-checker contains a few built-in tuned checkers but falls back to self-checking inferred clauses using SMT.
 2022-09-28 10:40:43 -07:00
Clemens Eisenhofer a67fe054d5
Memory leak in .NET user-propagator (#6360) 
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
 2022-09-22 13:26:08 -05:00
Peter Bruch 58fad41dfa
Dotnet Api: Fix infinite finalization of Context (#6361) 
* Dotnet Api: suppress GC finalization of dotnet context in favor of re-registering finalization

* Dotnet Api: enable concurrent dec-ref even if context is created without parameters.

* Dotnet Api: removed dead code.
 2022-09-22 13:25:17 -05:00
Nikolaj Bjorner af258d1720 add method for accessing i'th domain sort in array #6344 2022-09-15 07:38:02 -07:00
Nuno Lopes 16ef89905d fix infinite loop in internalize 2022-09-14 11:50:53 +01:00
Nikolaj Bjorner a5ad109707 suppress debug warnings when concurrent dec-ref is enabled. The contract with the client is that it doesn't invoke methods on auxiliary objects after the context is deleted. The client is not required to decrement reference counts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-11 19:06:23 -07:00
Nikolaj Bjorner edeeded4ea
remove DecRefQueue, use Z3_enable_concurrent_dec_ref (#6332) 
The notion of reference counted contexts never worked.
The reference count to a context only ends up being 0 if the GC kicks in and disposes the various z3 objects. A call to Dispose on Context should free up all resources associated with that context. In exchange none of the resources are allowed any other operation than DecRef. The invocations of DecRef are protected by a lock and test on the context that the native pointer associated with the context is non-zero. Dispose sets the native pointer to zero.

Z3_enable_concurrent_dec_ref ensures that:

- calls to decref are thread safe. Other threads can operate on the context without interference.

The Z3_context ensures that
- z3objects allocated, but not disposed during the lifetime of Z3_context are freed when Z3_context is deleted (it triggers a debug warning, but this is now benign).
 2022-09-11 18:59:00 -07:00
Clemens Eisenhofer 25b5b985e6
Missing overload for conflict (#6329) 2022-09-07 09:02:06 -07:00
Nikolaj Bjorner 5322d4f241 fix #6326 2022-09-06 23:48:21 -07:00
Nuno Lopes b9ddb11701 add static love 2022-09-04 11:57:43 +01:00
Clemens Eisenhofer a0ca5d745e
Fixed nested user-propagator callbacks in .NET (#6307) 
* Fixed nested user-propagator callbacks in .NET

* Typo
 2022-08-28 17:49:15 -07:00
Nikolaj Bjorner 2f8b13368d add redirect for warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-23 15:55:55 -07:00
Nikolaj Bjorner f6e4a45f4b Merge branch 'master' of https://github.com/z3prover/z3 2022-08-21 18:28:19 -07:00
Nikolaj Bjorner daa24ef4ce add missing error check 2022-08-21 18:26:53 -07:00
Clemens Eisenhofer 56fb161532
ADT-constructor generation crashed in .NET/Java when no (= default) fields are given (#6287) 2022-08-21 12:40:38 -07:00
Bruce Mitchener 6ba9ada1e2
Fix typos. (#6291) 2022-08-21 12:40:07 -07:00
Nikolaj Bjorner 08bf7a6293 fix name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-19 18:22:42 -07:00
Nikolaj Bjorner 665ef2c6ba add missing new 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-19 18:21:03 -07:00
Nikolaj Bjorner b26420ed99 #6285 2022-08-19 18:17:16 -07:00
Nikolaj Bjorner 19da3c7086 fix closing parnetheses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 13:26:29 -07:00
Nikolaj Bjorner d094f6a856 fixing interface and test' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 13:00:46 -07:00
Nikolaj Bjorner c7eda4e687 fixing interface and test' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 12:59:00 -07:00
Nikolaj Bjorner 6fb7a049ea test fromString 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 12:41:02 -07:00
Nikolaj Bjorner 53e168879a add fromString method 2022-08-18 12:33:10 -07:00
Bruce Mitchener 72f4ee9230 api: Correctly map OP_BSREM0 to Z3_BSREM0. 2022-08-12 14:40:16 -04:00
Nikolaj Bjorner 78eaefe5a8 move solver-params to params 2022-08-08 11:34:41 +03:00
Bruce Mitchener 5014b1a34d Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
Bruce Mitchener 6835522a7f z3++.h: No longer include unused sstream. 
This makes some code using the C++ API have to include `<sstream>`
if they used the functionality but didn't include it themselves.
 2022-08-05 09:41:49 +03:00
Bruce Mitchener 8a3556e5ba cmake: Remove dep on mk_util.py for update_api.py calls. 
update_api.py doesn't depend on mk_util.py any longer, so these
dependencies can go away.
 2022-08-04 07:54:26 +03:00
Bruce Mitchener 42f5047463 cmake: Cleanup remnants of workaround for USES_TERMINAL. 
In older versions, this was dependent upon the version of cmake,
but when it was updated for newer cmake, these remnants were
left.
 2022-08-02 17:39:10 +03:00
Bruce Mitchener fe1e301735 Remove Z3_bool, Z3_TRUE, Z3_FALSE from the API. 
These have just been aliases for the standard type `bool` and
values `true` and `false` for a long time now.
 2022-08-01 14:25:00 +03:00
Bruce Mitchener 77e5d6ab19 Use nullptr consistently instead of 0 or NULL. 2022-08-01 14:24:32 +03:00
Bruce Mitchener 5d0dea05aa
Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00