Nikolaj Bjorner
d0ef5948aa
nits
2022-04-02 17:49:03 -07:00
Nikolaj Bjorner
25feb0ebed
#5938 catch also rewriter_exception that can be raised on cancelation and memory pressure
2022-04-02 17:43:12 -07:00
Nikolaj Bjorner
ef28f0e2f0
#5778
...
deal with recursive calls to internalization with the same formula
2022-04-02 01:28:58 -07:00
Nikolaj Bjorner
2fedcbd41e
#5778
2022-04-02 01:27:56 -07:00
Nikolaj Bjorner
229ea569f1
#5778
2022-04-02 00:56:51 -07:00
Nikolaj Bjorner
97115e5ebd
#5778
...
add new clauses created during propagation to use-list
2022-04-02 00:14:59 -07:00
Nikolaj Bjorner
4cc33277fa
#5778
2022-04-01 14:27:40 -07:00
Nikolaj Bjorner
c7922d69ac
#5778
2022-04-01 14:17:45 -07:00
Nikolaj Bjorner
81084b8232
#5778 #5937
2022-04-01 13:07:17 -07:00
Nikolaj Bjorner
5154295202
#5932
2022-03-31 23:18:03 -07:00
Nikolaj Bjorner
28e94583da
break self recursion #5937
2022-03-31 21:49:08 -07:00
Nikolaj Bjorner
dd27f7e937
#5935
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-30 17:47:48 -10:00
Nikolaj Bjorner
431c3af409
fix #5929 - add parameter bv_le2extract to allow disabling the disassembly to extract
2022-03-27 18:23:41 -10:00
Clemens Eisenhofer
7bb969ab52
Fixed problem with registering bitvector functions ( #5923 )
2022-03-26 16:36:15 -10:00
Nikolaj Bjorner
3828130791
fix #5922 use 0u to help type inference
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-24 14:05:14 -10:00
Nikolaj Bjorner
32233e1bf1
set default to true to avoid regression failures
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-23 12:20:53 -07:00
Nikolaj Bjorner
365b8f3281
change default to _not_ include auxiliary functions in model as this seems to break fewer'
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-23 09:51:06 -07:00
Nikolaj Bjorner
d790523c59
#5917
...
Add model.user_functions (default true) to control whether user functions are added to the model.
2022-03-23 09:49:44 -07:00
John Fleisher
ce04c16a6f
Jfleisher/nightlynuget ( #5916 )
...
* WiP: Test nightly version number change
* Fix debug assert
* WiP: test nuget publish to AzDo feed for nightly build
* WiP: Make Nuget deploy separate stage
* WiP: fix nightly stage name
* change nuget push to vstsfeed
* Try case sensitive name for artifacts
* WiP: use artifact folder names
* add Rev version to package
* WiP: build def variation on nightly build version
* WiP: use Build_BuildNumber and Build_DefinitionName
* WiP: using hyphen in nightly version
* Tag nightly packages with datetime
* fix commit
* Build.BuildId and Build.DefinitionName
* WiP: change suffix format to lead with alpha
* test z3public feed publish
* revert public publish test
* WiP: test build# versioning scheme
* WiP: another variant on version number for nightly
Co-authored-by: jfleisher <jofleish@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-22 12:19:58 -07:00
Nikolaj Bjorner
815c971c9a
#5778
...
regression when tracking literal explanations
2022-03-22 01:55:43 -07:00
Nikolaj Bjorner
4b1419261f
#5778
2022-03-21 16:23:43 -07:00
Nikolaj Bjorner
20bd59bb20
#5778 - missed tracking literal assignment justification
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-21 10:15:00 -07:00
Nikolaj Bjorner
f1806d32d6
remove buggy code, close, fix #5825
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 13:25:44 -07:00
Nikolaj Bjorner
b4873d226c
fix #5907
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 11:40:19 -07:00
Nikolaj Bjorner
f053daa051
fix #5906
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 11:24:42 -07:00
Nikolaj Bjorner
bbb27775ed
ensure that objects in callback are of sort Ast.
2022-03-20 11:24:42 -07:00
Nikolaj Bjorner
b5b9c85c40
call it UbuntuBuild
2022-03-19 15:24:53 -07:00
Nikolaj Bjorner
dfa65443e9
fix name for artifact
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-19 13:51:58 -07:00
Nikolaj Bjorner
964e513353
re-add bv_eq_axioms, fix #5842
2022-03-19 12:37:01 -07:00
Nikolaj Bjorner
cfe02edda5
remove stale return
2022-03-19 12:26:48 -07:00
Nikolaj Bjorner
86af723db7
remove left-over debug output
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-19 09:40:29 -07:00
Nikolaj Bjorner
6d836e7e2f
expose model update
2022-03-19 09:23:08 -07:00
Nikolaj Bjorner
a9d7026724
add note about transform
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 19:13:35 -07:00
Nikolaj Bjorner
669a1d63da
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 16:36:16 -07:00
Nikolaj Bjorner
6010d751ed
fix #5903
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 16:21:47 -07:00
Nikolaj Bjorner
41d1c34067
remove else case
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-17 12:33:15 -07:00
Nikolaj Bjorner
1fa373d6c2
old bug: unit of xor is false
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-17 08:21:22 -07:00
Matt Thornton
4e0a2f5968
Dispose of intermediate Z3Objects created in dotnet api. ( #5901 )
...
* Dispose of intermediate Z3Objects created in dotnet api.
* Set C# LangVersion to 8.0.
* Fix build errors.
* Fix warning about empty using statement.
* Fix Xor to only dispose of objects that it creates internally.
2022-03-17 08:08:05 -07:00
Jan Vraný
bdf7de1703
Care for root index being undefine while calling Z3_algebraic_get_i() ( #5888 )
...
In some cases, Z3_algebraic_get_i() returned 0. For example, in the following
Python snippet, the last assert would fail:
import z3
x = z3.Real('x')
s = z3.Solver()
s.add( (x * x) - 2 == 0, x <= 0)
s.check()
val_x = s.model().get_interp(x)
assert val_x.index() == 1
The problem was that `algebraic_numbers::manager:👿 :get_i()` did not
check whether the root index was properly initialized.
This commit fixes this issue by checking whether root index is initialized
the same way various other routines do.
Fixes issue #5807 .
Signed-off-by: Jan Vrany <jan.vrany@labware.com>
2022-03-16 19:28:03 -07:00
Nikolaj Bjorner
0b230ee703
move some functions to using var pattern #5900
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-16 16:29:54 -07:00
Nikolaj Bjorner
a1517251dd
call dispose on sorts #5900 , missing charSort
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-16 07:28:05 -07:00
Nikolaj Bjorner
cd5e114ed3
call dispose on sorts #5900
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-16 07:24:33 -07:00
Nikolaj Bjorner
cb9dcb799f
add regex power to API and for Java per request
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-16 06:17:31 -07:00
Nikolaj Bjorner
e1929ca9b9
add regex power to API and for Java per request
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-15 19:18:33 -07:00
Nikolaj Bjorner
706d7ea893
native context uses legacy mk_context
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-15 16:01:05 -07:00
Nikolaj Bjorner
545341e699
fix #5895
2022-03-12 09:17:13 -08:00
Nikolaj Bjorner
c51ca86203
add another constant folding case
2022-03-10 17:39:40 -08:00
Nikolaj Bjorner
e839e18381
minimal addition to rewrite bit-vector to character conversion using constant folding.
2022-03-10 17:31:17 -08:00
Nikolaj Bjorner
8f2ea90db1
Merge branch 'master' of https://github.com/Z3Prover/z3
2022-03-10 17:09:36 -08:00
Nikolaj Bjorner
081c62d006
allow range comparison for bit-vectors and int/real
2022-03-10 17:08:49 -08:00
Nikolaj Bjorner
580012e19f
fix #5894
...
expp is not implemented. This is the second time a fuzz bug reports it. Instead of closing the bug, just disable code path as fuzzers are not considering the comment from previous bug.
2022-03-10 09:45:09 -08:00
Hari Govind V K
f26c12a9ad
fix #5882 . Use model true when inlining ( #5892 )
2022-03-09 12:31:39 -08:00
Nuno Lopes
43f7636826
remove some copies/moves
2022-03-09 12:46:41 +00:00
Nikolaj Bjorner
1d224d1bcd
na
2022-03-08 08:51:00 -08:00
Nikolaj Bjorner
c6f8ee33d4
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-08 08:36:19 -08:00
Nikolaj Bjorner
3293aeb7c7
na
2022-03-08 08:36:19 -08:00
John Fleisher
97c7ce63b5
Clean up build warnings ( #5884 )
...
* Clean up warnings in compile for documentation notes
* remove snk from local build
Co-authored-by: jfleisher <jofleish@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-07 12:55:30 -08:00
Lorenzo Veronese
e3568d5b47
Handle additional cases in rule_properties::check_accessor ( #5821 )
...
* Handle additional cases in rule_properties::check_accessor
* Walk parents depth first in rule_properties::check_accessor
2022-03-07 07:49:59 -08:00
Nikolaj Bjorner
882fc31aea
doc strings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 15:25:05 -08:00
Nikolaj Bjorner
b0c0f4d1f4
fix #5876
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 15:07:45 -08:00
Nikolaj Bjorner
3e51b69a9a
no fun!
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 15:03:02 -08:00
Nikolaj Bjorner
87e6f103c6
commenting
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 14:00:07 -08:00
Nikolaj Bjorner
676ba78600
fix else case: it is first argument of const array
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 13:10:02 -08:00
John Fleisher
35d26bc282
NativeModel: TryGetArrayValue ( #5881 )
...
* WiP: Disposable, MkAdd, MkApp, MkBool, MkBoolSort, MkBound, MkBvSort, MkFalse, MkTrue, MkIntSort
* WiP: Native z3 mk_ functions
* WiP: mk_ functions for NativeContext
* WiP: add utility functions for getting values
* WiP: Adding more native utility functions
* native model pull
* WiP: NativeContext additions for array access
* WiP: use Z3_symbol in place of managed Symbol
* WiP: add solver, model, and array methods
* WiP: MkSimpleSolver, MkReal
* WiP: GetDomain GetRange
* WiP: MkExists
* Override for MkFuncDecl
* MkConstArray, MkSelect
* WiP: code cleanup
* migrate Context reference to NativeContext
* remove local signing from PR
* minor code cleanup
* Sorts to properties, fix usings,
* make IntSort property
* sort using
* IntSort, RealSort - properties
* WiP: get array value update
Co-authored-by: jfleisher <jofleish@microsoft.com>
2022-03-03 13:06:30 -08:00
Nikolaj Bjorner
248a3676af
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 11:40:29 -08:00
Nikolaj Bjorner
e1e8d15827
stub out array serialization
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 11:38:23 -08:00
Nikolaj Bjorner
cd324a4734
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 11:07:00 -08:00
Nikolaj Bjorner
8d1276fa60
using directives
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 11:03:31 -08:00
John Fleisher
a08be497f7
NativeContext, NativeSolver, NativeModel - updates for Pex ( #5878 )
...
* WiP: Disposable, MkAdd, MkApp, MkBool, MkBoolSort, MkBound, MkBvSort, MkFalse, MkTrue, MkIntSort
* WiP: Native z3 mk_ functions
* WiP: mk_ functions for NativeContext
* WiP: add utility functions for getting values
* WiP: Adding more native utility functions
* native model pull
* WiP: NativeContext additions for array access
* WiP: use Z3_symbol in place of managed Symbol
* WiP: add solver, model, and array methods
* WiP: MkSimpleSolver, MkReal
* WiP: GetDomain GetRange
* WiP: MkExists
* Override for MkFuncDecl
* MkConstArray, MkSelect
* WiP: code cleanup
* migrate Context reference to NativeContext
* remove local signing from PR
* minor code cleanup
Co-authored-by: jfleisher <jofleish@microsoft.com>
2022-03-03 10:41:12 -08:00
Nikolaj Bjorner
811cd9d48d
add example
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 09:14:47 -08:00
Nikolaj Bjorner
ee18c5070c
add stubs for injective function axioms, add some parameter functions
2022-03-03 09:09:03 -08:00
Nikolaj Bjorner
757cf7622d
sketch ArrayValue, add statistics
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-02 10:59:19 -08:00
Nikolaj Bjorner
80506dfdfa
sketch ArrayValue, add statistics
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-02 10:55:39 -08:00
Nikolaj Bjorner
bf14aeb1bd
stub out nativesolver
2022-03-02 10:06:38 -08:00
Nikolaj Bjorner
bbadd17d56
fix #5874
2022-03-02 08:46:28 -08:00
Nikolaj Bjorner
5f79a977fb
use conventions from Context
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-01 14:27:57 -08:00
Nikolaj Bjorner
c812d1e890
update native func interp
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-01 14:07:20 -08:00
Nikolaj Bjorner
61d2654770
quantifier
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-01 13:18:18 -08:00
Nikolaj Bjorner
deeb5e9921
finish NativeModel
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-01 12:40:03 -08:00
Nikolaj Bjorner
c0826d58bf
add stubs for native model and func interp
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-01 12:11:10 -08:00
Nikolaj Bjorner
deaad86d6a
nit
2022-03-01 12:11:10 -08:00
Nikolaj Bjorner
2b6dadcbc6
fix #5869
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-28 17:02:13 -08:00
Nikolaj Bjorner
302c0d178c
fix #5867
2022-02-26 09:52:23 -08:00
Clemens Eisenhofer
412b05076c
User-functions fix ( #5868 )
2022-02-26 09:21:01 -08:00
Nuno Lopes
689e2d41de
remove a bunch of unneeded memory allocations
2022-02-25 16:08:23 +00:00
Nikolaj Bjorner
7f149a36d7
refining model update rules for del_rule #5865 #5866
2022-02-25 08:03:46 -08:00
Nikolaj Bjorner
30a2f2fd9d
initial stab at NativeContext
2022-02-25 07:56:36 -08:00
Nikolaj Bjorner
f2e712b0d6
throttle is_compatible to check variables at most once
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-23 08:45:22 -08:00
Nikolaj Bjorner
7b4f1ed530
missing initialization of m_user_propagator, disable unsound in-processing in pb_solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-23 04:49:42 -08:00
Nikolaj Bjorner
6be0a66b38
fix #5863
2022-02-22 13:00:20 -08:00
Nikolaj Bjorner
6af170b058
fix #5861
...
sigh
2022-02-22 11:26:09 -08:00
Nikolaj Bjorner
c2f1bdc099
fix #5862
2022-02-22 08:05:05 -08:00
Nikolaj Bjorner
11030fc81d
disable unsound mk_seq_butlast
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-21 18:56:49 -08:00
Nikolaj Bjorner
ea0876b6d6
add lambda definitions during ast translation #5820
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-21 18:05:29 -08:00
Nikolaj Bjorner
d06c51d517
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-21 17:46:54 -08:00
Nikolaj Bjorner
061e94d723
#5858
...
COI model converter has to use constraints from the body and work in disjunctive mode. It needs a pre-condition that the body does not depend on other rules, in the case that it is used in a different pre-processing step for in-lining. The in-lined occurrence of the predicate has to correspond to the model construction version.
2022-02-21 17:45:00 -08:00
Nikolaj Bjorner
e8d4804dbb
Revert "use horn_subsume_model_converter in coi filter ( #5844 )" ( #5859 )
...
This reverts commit 09da87dc85
.
2022-02-21 04:33:52 -08:00
Nikolaj Bjorner
b843618051
fix #5798
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-20 13:54:15 -08:00
Nikolaj Bjorner
5c2624950b
#5849
2022-02-20 09:52:42 -08:00
Nikolaj Bjorner
1e463955c2
#4889 avoid double internalize of bvle
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-20 09:09:28 -08:00