Nikolaj Bjorner
a4ece21461
toggle enable-ternary to true
2022-10-25 10:44:23 -07:00
Nikolaj Bjorner
154fed7783
introduce globally visible macro for controlling use of ternary, turn them off
2022-10-25 10:30:18 -07:00
Nikolaj Bjorner
c62c5e9d23
add opportunistic, missing, bv rewrites
...
- x >> x logical = 0
- ~x = -1 -x
- x * (y << z) = (x * y) << z
2022-10-25 10:29:48 -07:00
Nikolaj Bjorner
09a2ba4931
remove artificial usage of function, it causes another compiler warning to refer to a function without arguments.
2022-10-25 10:28:25 -07:00
Nikolaj Bjorner
c672c3a250
fix regression introduced in #6143
2022-10-25 09:39:11 -07:00
Nikolaj Bjorner
e1a00f4917
remove unused experimental feature - diff
2022-10-24 16:13:24 -07:00
Nikolaj Bjorner
280887cc5a
remove deprecated theory aware drat functionality
...
it is handled by the on-clause callback that is owned by the smt solver.
2022-10-24 08:32:10 -07:00
Nuno Lopes
cb3c86736c
fix build
2022-10-24 10:23:50 +01:00
Nuno Lopes
4431fd17ce
memory_manager: add support for MacOS & Windows to the new size tracking system
2022-10-24 10:09:56 +01:00
Nikolaj Bjorner
a24b5a64e1
#6364 proviso for ignore int
2022-10-24 00:48:57 -07:00
Nikolaj Bjorner
5c7eaec566
#6364 - remove option of redundant clauses from internalization
...
gc-ing definitions leads to unsoundness when they are not replayed.
Instead of attempting to replay definitions theory internalization is irredundant by default.
This is also the old solver behavior where TH_LEMMA is essentially never used, but is valid for top-level theory lemmas.
2022-10-24 00:38:31 -07:00
Nikolaj Bjorner
c8e1e180ea
prefix Boolean variables in log with b
2022-10-23 11:05:50 -07:00
Nikolaj Bjorner
6393ed78d7
remove useless log
2022-10-23 11:05:33 -07:00
Nikolaj Bjorner
ddbca68270
minor formatting update
2022-10-23 11:05:09 -07:00
Nikolaj Bjorner
4a1d76cf49
#6418 - add best-effort for nested and/or (from ite literals)
2022-10-23 11:03:51 -07:00
Nikolaj Bjorner
071a1447e3
fix #6418
2022-10-23 11:03:00 -07:00
Nikolaj Bjorner
e3a44254c9
fix #6415
2022-10-22 11:18:16 -07:00
Nikolaj Bjorner
7eee7914bd
align format of quantifier instantiation with new core
...
So far the format is
(forall ((x Int)) body) (not (body[t/x]))
The alternative could be the clause
(not (forall ((x Int)) body)) body[t/x]
they just better be consistent between engines
2022-10-21 15:26:00 -07:00
Nikolaj Bjorner
53adc2afee
update debugging information for new core
2022-10-21 15:24:44 -07:00
Nikolaj Bjorner
ad5fa9433f
add experiment with quot-rem encoding
...
experiment seeks to determine whether quot-rem encoding can substitute the division circuit encoding.
A first test suggests it makes no difference.
2022-10-21 09:25:45 -07:00
Nikolaj Bjorner
31914d8ecf
simplify purified expressions
2022-10-21 03:47:57 -07:00
Nikolaj Bjorner
842e8057bc
log also quantifier generation (besides binding)
...
We add also logging for quantifier generation.
It is auxiliary information that is of use for diagnostics (axiom profiler).
2022-10-20 17:49:15 -07:00
Nikolaj Bjorner
c1b355f342
#6364
...
throttle on upwards propagation of default was too restrictive
2022-10-20 17:48:17 -07:00
Nikolaj Bjorner
6d6752b2aa
#6364
2022-10-20 16:39:43 -07:00
Nikolaj Bjorner
354bc50400
Update .gitignore
2022-10-20 13:15:43 -07:00
Nikolaj Bjorner
edad727cd5
#6364
...
ensure substitutions are applied to eliminate internal variables from results
2022-10-20 13:14:54 -07:00
Nikolaj Bjorner
5976978062
move std functions up for potential alignment issues
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-20 09:11:15 -07:00
Nikolaj Bjorner
fc30461828
unused variables
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-20 09:09:06 -07:00
Nikolaj Bjorner
6292b06c67
ensure that initialization order for euf_solver is aligned
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-20 08:48:15 -07: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
2842c27e92
#6364
2022-10-20 04:48:13 -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
88d10f7fe4
add example for monitoring proof logs
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-19 13:37:51 -07:00
Nikolaj Bjorner
a90c4f65cf
increment version per release notes
...
incrementing minor version because the API has a new function.
This breaks log replay against old dlls and inclusion against z3++.h.
2022-10-19 13:21:26 -07:00
dependabot[bot]
f6d554118f
Bump docker/build-push-action from 3.1.1 to 3.2.0 ( #6405 )
2022-10-19 21:14:43 +01:00
Nikolaj Bjorner
4c79e63c1b
Update parse-api.ts
2022-10-19 12:52:58 -07:00
Nikolaj Bjorner
b084852397
update release notes, fix bug in replay of Boolean variables in new core
2022-10-19 12:12:32 -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
Nikolaj Bjorner
77cbd89420
remove once pragma from cpp file
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-18 14:57:49 -07:00
Nikolaj Bjorner
eaf52f4c32
fix infinite loop issue in def::operator+, other issues remain though for #6404
...
The example from #6404 results in an incorrect result. It uses integer division on private variables where MBQI support is new and not tested for substitutions.
2022-10-18 14:52:30 -07:00
Nikolaj Bjorner
cdfab8cb13
wip - add bit-vector validator plugins and logging
2022-10-18 14:50:21 -07:00
Nikolaj Bjorner
464d52babe
fix #6410
...
regression after introducing beta-redex optimization
2022-10-18 12:34:45 -07:00
Nikolaj Bjorner
f0b85716a9
wip - proof logging fixes
2022-10-18 11:20:56 -07:00
Nikolaj Bjorner
1fc77c8c00
wip - proof checking
...
fixes to smt_theory_checker. Generalize it to apply to arrays and fpa.
Missing: bv
2022-10-18 09:02:50 -07:00
Nikolaj Bjorner
7b3a634b8d
wip - features and bug-fixes to proof logging
2022-10-18 07:54:49 -07:00
Nikolaj Bjorner
3bf1b606df
remove on-the fly ackerman reduction because it interferes with conflict resolution
2022-10-18 07:53:42 -07:00
Nikolaj Bjorner
b758d5b2b1
wip - proof checking, add support for distinct, other fixes
2022-10-17 17:51:10 -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
d4885abdc0
fix #6400
...
bi-implication was treated as an atomic formula leading to incorrect projection.
2022-10-17 11:00:21 -07:00
