Jakob Rath
1d0ad1ccc0
fix build (add conversion operator)
2023-01-10 17:18:56 +01:00
Jakob Rath
0c799524e8
try splitting x-intervals
2023-01-10 16:25:28 +01:00
Jakob Rath
49848a4298
extract function update_bounds_for_xs
2023-01-10 15:16:24 +01:00
Jakob Rath
abbe139abb
Use M for 2^N
2023-01-10 14:50:11 +01:00
Jakob Rath
913aa9f43e
debugging output
2023-01-10 14:33:48 +01:00
Jakob Rath
0f43c1c71d
adjust_bound fails if [min,max] contains a multiple of N
2023-01-10 13:32:36 +01:00
Nikolaj Bjorner
a4d4e2e483
track assertions
2023-01-09 15:18:33 -08:00
Nikolaj Bjorner
64ec8acd30
fix model reconstruction ordering for elim_unconstrained
2023-01-09 15:18:19 -08:00
Nikolaj Bjorner
eda25e0ebb
get-assignment
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-09 10:14:19 -08:00
Nikolaj Bjorner
30e0f78c16
remove exit
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-09 10:00:36 -08:00
Jakob Rath
b6ea9e31e5
output
2023-01-09 17:20:40 +01:00
Jakob Rath
181995a4fb
extend invariant check
2023-01-09 17:16:56 +01:00
Jakob Rath
c55d316c6a
Rename to get_assignment to prevent clash with class name
2023-01-09 17:15:40 +01:00
Jakob Rath
3f5e6a4bfa
bugfix: don't intersect forbidden intervals if variable is already assigned
2023-01-09 17:10:18 +01:00
Clemens Eisenhofer
aafd9039db
Bugfix
2023-01-09 14:14:19 +01: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
49ee570b09
split into separate function
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-08 19:16:46 -08:00
Nuno Lopes
5899fe3cea
Add rewrite for array selects of chain of stores of a same value ( #6526 )
...
* Add rewrite for array selects of chain of stores of a same value
Example:
```smt
(declare-fun mem () (Array (_ BitVec 4) (_ BitVec 4)))
(declare-const x (_ BitVec 4))
(declare-const y (_ BitVec 4))
; simplifies to #x1
(simplify (select (store (store (store mem #x1 #x1) y #x1) x #x1) #x1))
```
* Update array_rewriter.cpp
* Update array_rewriter.cpp
2023-01-08 19:09:01 -08:00
Nikolaj Bjorner
1ddef117a2
several fixes to proof logging in legacy solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-08 16:11:31 -08:00
Nikolaj Bjorner
61b90e64b2
disable new simplifcation for multiplier until really understood
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-08 14:17:49 -08:00
Nikolaj Bjorner
fcea32344e
add missing tactic descriptions, add rewrite for tamagochi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-08 13:32:26 -08:00
Nikolaj Bjorner
95cb06d8cf
add quasi macro detection
2023-01-06 19:53:55 -08:00
Nikolaj Bjorner
991acb0d72
add diagnostics for assertion violations
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-06 13:29:24 -08:00
Nikolaj Bjorner
25112e47b4
bugfix to flatten-clases simplifier
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-05 20:59:28 -08:00
Nikolaj Bjorner
c07b6ab38f
more tactic descriptions
2023-01-05 20:23:01 -08:00
Clemens Eisenhofer
b1239d5276
Missing file
2023-01-05 18:05:08 +01:00
Clemens Eisenhofer
0c1c9c64eb
Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat
2023-01-05 18:03:43 +01:00
Clemens Eisenhofer
4a6053b289
Missing univariate for pseudo-inverse
2023-01-05 18:02:21 +01:00
Jakob Rath
1002538565
insert_eval?
2023-01-05 17:41:08 +01:00
Jakob Rath
aeb6138c25
No result if there is no other interval
2023-01-05 17:21:25 +01:00
Jakob Rath
a406e01fb8
e0 instead of first?
2023-01-05 16:44:45 +01:00
Jakob Rath
6f18335604
need y0 value
2023-01-05 16:43:23 +01:00
Jakob Rath
ffa12eb37c
flip args to match description
2023-01-05 16:43:01 +01:00
Jakob Rath
55a50ea461
ule rewrites
2023-01-05 14:41:21 +01:00
Nikolaj Bjorner
0d8a472aac
pass sign into literal definition for pbge
2023-01-04 16:55:44 -08:00
Nikolaj Bjorner
81ce57b5a8
#6429
2023-01-04 15:38:13 -08:00
Nikolaj Bjorner
e0099150ca
#6429
2023-01-04 15:28:57 -08:00
Nikolaj Bjorner
380c701cbe
restore debug clang/gcc build
2023-01-04 15:01:40 -08:00
Nikolaj Bjorner
21362c0b98
make case-def and recfun-num-rounds re-parsable for logging
2023-01-04 15:00:25 -08:00
Nikolaj Bjorner
ef10119005
#6429 fixes
2023-01-04 13:05:45 -08:00
Nikolaj Bjorner
aa080a6b19
update ignore-int handling #6429
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-04 12:22:38 -08:00
Nikolaj Bjorner
8d0d6d8f04
Merge branch 'master' of https://github.com/z3prover/z3
2023-01-04 11:56:38 -08:00
Nikolaj Bjorner
6f95c77023
fix bugs in flatten_clauses simplifier, switch proof/fml
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-04 11:56:28 -08:00
Jakob Rath
0daf444cec
Actually revert boolean decisions
2023-01-04 17:20:34 +01:00
Nikolaj Bjorner
db1be0f247
unit test for bench 13 scenario
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-03 12:23:14 -08:00
Clemens Eisenhofer
075b548089
Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat
2023-01-03 17:48:21 +01:00
Clemens Eisenhofer
79e7380ffc
Pseudo-inverse op_constraint
2023-01-03 17:47:54 +01:00
Jakob Rath
283e60a5cb
compile
2023-01-03 14:55:50 +01:00
Nuno Lopes
e448191212
array rewriter: expand select of store with const array into an ite
...
This:
(simplify (select (store ((as const (Array (_ BitVec 4) (_ BitVec 4))) #x0) x #x1) y))
=>
(ite (= x y) #x1 #x0)
2023-01-03 11:08:57 +00:00
Nuno Lopes
e508ef17f6
fix Alive bug #875 : bit blaster not respecting soft memory limit
2023-01-03 10:39:28 +00:00
