Nikolaj Bjorner
f66a082de9
fix #6595
2023-02-18 14:11:48 -08:00
Ding Fei
828ff98c77
fix tpl instantiation issue for mingw ( #6597 )
2023-02-17 09:26:45 -08:00
Nikolaj Bjorner
bd10ddf6ae
wip - local search - use dispatch model from bool local search instead of separate phases.
2023-02-16 09:17:11 -08:00
Nikolaj Bjorner
ac068888e7
add trichotomy for sequence comparison. #6586
2023-02-16 08:59:55 -08:00
Nikolaj Bjorner
554a9e8efe
fix #6346
2023-02-16 08:53:08 -08:00
Nikolaj Bjorner
7c08e53e94
fixes for #6590
2023-02-15 15:11:44 -08:00
Nikolaj Bjorner
c1ecc49021
wip - local search - move to plugin model
2023-02-15 13:32:30 -08:00
Nikolaj Bjorner
a1f73d3805
wip - local search - fix build
2023-02-15 08:48:37 -08:00
Nikolaj Bjorner
4f20b8e2ba
wip - local search
2023-02-15 08:36:10 -08:00
Nikolaj Bjorner
8ce0c56ff5
fix #6590
2023-02-15 08:36:01 -08:00
Nikolaj Bjorner
c2fe76569f
remove dependency on bool-rewriter in hoist rewriter
...
deal with regression reported in
cac5052685 (commitcomment-100606067)
and unit tests doc.cpp
2023-02-14 17:48:02 -08:00
Nikolaj Bjorner
a976b781a0
fix #6585
2023-02-14 15:33:17 -08:00
Nikolaj Bjorner
44fcf60a72
wip experiments with sls
2023-02-14 15:06:26 -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
Nikolaj Bjorner
3dc91de531
fix #6582
2023-02-13 13:21:30 -08:00
Nikolaj Bjorner
2b77012993
fix build
2023-02-13 08:36:12 -08:00
Nikolaj Bjorner
52804b5c8f
save on dtt
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-13 08:29:32 -08:00
Nikolaj Bjorner
7956cf1201
annotate arith_sls
2023-02-12 20:55:44 -08:00
Nikolaj Bjorner
bb81bc5452
fix #6580
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-12 20:21:53 -08:00
Nikolaj Bjorner
102eee77dc
patch regressions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-12 20:12:01 -08:00
Nikolaj Bjorner
cac5052685
fixes related to #6577
...
- enforce elim-and in bool-rewriter when invoking hoisting.
- make cnf tactic more resilient to non-normalized input.
- enable eliminate predicates on ground formulas
2023-02-12 13:43:44 -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
5e30323b1a
wip - bounded local search for arithmetic
2023-02-11 15:46:39 -08:00
Nikolaj Bjorner
4b2c166e8b
fixes to build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-11 10:19:24 -08:00
Nikolaj Bjorner
7bef2f3e6f
wip - local search for euf/arithmetic
2023-02-11 09:33:43 -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
Nikolaj Bjorner
d22e4aa525
wip - integrating arithmetic local search
2023-02-11 09:33:42 -08:00
Nikolaj Bjorner
1b0c76e3f0
fixes to mbqi in the new core based on #6575
2023-02-10 16:56:06 -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
Nikolaj Bjorner
02d48adae5
fix #6573
2023-02-08 08:24:52 -08:00
Nikolaj Bjorner
a8335f2d5e
use phase
2023-02-07 19:50:45 -08:00
Nikolaj Bjorner
b3ebce3966
fix compilation
2023-02-07 19:30:45 -08:00
Nikolaj Bjorner
96d815b904
adding arith sls
2023-02-07 19:27:19 -08:00
Nikolaj Bjorner
6a2d60a6ba
fix #6571
...
most solvers don't support background properties
2023-02-07 11:04:58 -08:00
Nikolaj Bjorner
601e506d54
remove debug out
2023-02-07 10:40:49 -08:00
Nikolaj Bjorner
a150e58893
update release script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-07 09:21:02 -08:00
Nikolaj Bjorner
90a75866fb
elaborating on local-search rephase strategy
2023-02-07 03:17:52 -08:00
Nikolaj Bjorner
f3ae7692ca
update stage name
2023-02-06 16:08:14 -08:00
Nikolaj Bjorner
c1cadd37cc
update stage name
2023-02-06 16:07:12 -08:00
Nikolaj Bjorner
a7231027c3
try side-by-side nightly
2023-02-06 16:04:54 -08:00
Nikolaj Bjorner
c1c26f0726
restart after sat solution
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-06 09:21:35 -08:00
Nikolaj Bjorner
03a4920f3d
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-05 21:41:07 -08:00
Nikolaj Bjorner
75c573877d
updates to ddfw, initial local search phase option
2023-02-05 21:35:22 -08:00
Nikolaj Bjorner
992793bd56
update nuget packaging targets #6570
2023-02-05 21:35:22 -08:00
Nikolaj Bjorner
3712cbdbfd
fix #6559
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-04 13:33:40 -08:00
Jakob Rath
d69155b9e9
Shared features from polysat branch ( #6567 )
...
* Allow setting default debug action
* Fix dlist and add iterator
* Add var_queue iterator
* Add some helpers
* rational: machine_div2k and pseudo_inverse
* Basic support for non-copyable types in map
* tbv helpers
* pdd updates
* Remove duplicate functions
gcc doesn't like having both versions
2023-02-03 13:08:47 -08:00
Frederick Robinson
be44ace995
fix typo ( #6569 )
2023-02-03 13:08:35 -08:00
Nikolaj Bjorner
cb72b962d1
Merge branch 'master' of https://github.com/z3prover/z3
2023-02-02 20:50:58 -08:00
Nikolaj Bjorner
839f87a10c
don't apply tactics in parse mode
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-02 20:50:53 -08:00
Nikolaj Bjorner
39d2818923
compiler warnings/bugs
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-02 19:36:22 -08:00