Nikolaj Bjorner
3293aeb7c7
na
2022-03-08 08:36:19 -08:00
Nikolaj Bjorner
e7ded9cdbd
update to 2022
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
2b71d8bc08
doc macros
2022-03-03 14:59:38 -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
Clemens Eisenhofer
35fb95648b
Updated user-propagator example ( #5879 )
2022-03-03 10:42:06 -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
Emma Jane Bonestell
dc110f10a4
Update mk_util.py ( #5864 )
...
Fix dynamic -lib opam builds on MSYS2
2022-02-23 03:36:46 -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
456b8ee682
nightly
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-21 04:18:05 -08:00
Nikolaj Bjorner
c47e5aff60
multi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-20 14:03:13 -08:00
Nikolaj Bjorner
cfe9846f0c
multi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-20 13:59:42 -08:00
Nikolaj Bjorner
b843618051
fix #5798
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-20 13:54:15 -08:00
