Nikolaj Bjorner
b40e3015ef
fix #7053
2023-12-13 19:25:18 -08:00
Nikolaj Bjorner
69f9640fdf
fix #7018
2023-11-28 13:14:44 -08:00
Nikolaj Bjorner
d8156aeff3
weird latent bug in wmax: init() succeeds and it returns undef
2023-04-24 21:14:42 -07:00
Nikolaj Bjorner
fdd5c923ed
use only maxres if there is a lexicographic objective, fix #6697
...
- maxlex.enable heuristic does not work if it is chained among multiple objectives. Only maxres is set up to commit the proper constraints.
2023-04-24 20:20:26 -07:00
Nikolaj Bjorner
f6d411d54b
experimental feature to access congruence closure of SimpleSolver
...
This update includes an experimental feature to access a congruence closure data-structure after search.
It comes with several caveats as pre-processing is free to eliminate terms. It is therefore necessary to use a solver that does not eliminate the terms you want to track for congruence of. This is partially addressed by using SimpleSolver or incremental mode solving.
```python
from z3 import *
s = SimpleSolver()
x, y, z = Ints('x y z')
s.add(x == y)
s.add(y == z)
s.check()
print(s.root(x), s.root(y), s.root(z))
print(s.next(x), s.next(y), s.next(z))
```
2022-12-30 21:41:27 -08:00
Nikolaj Bjorner
6297c001ee
remove legacy solve_eqs_tactic entirely
...
also, bug fixes to elim_unconstrained (elim_uncnstr2) which is to replace legacy tactic for eliminating unconstrained constants.
2022-11-14 18:57:16 -08:00
Nikolaj Bjorner
3a37cfca30
switch to solve_eqs2 tactic
2022-11-08 12:23:36 -08:00
Nikolaj Bjorner
1dca6402fb
move model and proof converters to self-contained module
2022-11-03 05:23:01 -07:00
Nikolaj Bjorner
0e651eee04
#6421
2022-10-28 14:12:28 -07:00
Nikolaj Bjorner
107981f099
update proof formats for new core
...
- update proof format for quantifier instantiation to track original literals
- update proof replay tools with ability to extract proof object
The formats and features are subject to heavy revisions.
Example
```
(set-option :sat.euf true)
(set-option :sat.smt.proof eufproof.smt2)
(declare-fun f (Int) Int)
(declare-const x Int)
(assert (or (= (f (f (f x))) x) (= (f (f x)) x)))
(assert (not (= (f (f (f (f (f (f x)))))) x)))
(check-sat)
```
eufproof.smt2 is:
```
(declare-fun x () Int)
(declare-fun f (Int) Int)
(define-const $24 Int (f x))
(define-const $25 Int (f $24))
(define-const $26 Int (f $25))
(define-const $27 Bool (= $26 x))
(define-const $28 Bool (= $25 x))
(assume $27 $28)
(define-const $30 Int (f $26))
(define-const $31 Int (f $30))
(define-const $32 Int (f $31))
(define-const $33 Bool (= $32 x))
(assume (not $33))
(declare-fun rup () Proof)
(infer (not $33) rup)
(declare-fun euf (Bool Bool Proof Proof Proof Proof) Proof)
(declare-fun cc (Bool) Proof)
(define-const $42 Bool (= $32 $30))
(define-const $43 Proof (cc $42))
(define-const $40 Bool (= $31 $24))
(define-const $41 Proof (cc $40))
(define-const $38 Bool (= $30 $25))
(define-const $39 Proof (cc $38))
(define-const $36 Bool (= $24 $26))
(define-const $37 Proof (cc $36))
(define-const $34 Bool (not $33))
(define-const $44 Proof (euf $34 $28 $37 $39 $41 $43))
(infer (not $28) $33 $44)
(infer (not $28) rup)
(infer $27 rup)
(declare-fun euf (Bool Bool Proof Proof Proof) Proof)
(define-const $49 Bool (= $32 $26))
(define-const $50 Proof (cc $49))
(define-const $47 Bool (= $31 $25))
(define-const $48 Proof (cc $47))
(define-const $45 Bool (= $24 $30))
(define-const $46 Proof (cc $45))
(define-const $51 Proof (euf $34 $27 $46 $48 $50))
(infer $33 $51)
(infer rup)
```
Example of inspecting proof from Python:
```
from z3 import *
def parse(file):
s = Solver()
set_option("solver.proof.save", True)
set_option("solver.proof.check", False)
s.from_file(file)
for step in s.proof().children():
print(step)
parse("../eufproof.smt2")
```
Proof checking (self-validation) is on by default.
Proof saving is off by default.
You can use the proof logs and the proof terms to retrieve quantifier instantiations from the new core.
The self-checker contains a few built-in tuned checkers but falls back to self-checking inferred clauses using SMT.
2022-09-28 10:40:43 -07:00
Nikolaj Bjorner
42945de240
#6319
...
align use of optsmt and the new core (they should not be used together)
2022-09-21 12:09:31 -07:00
Bruce Mitchener
5014b1a34d
Use = default for virtual constructors.
2022-08-05 18:11:46 +03:00
Bruce Mitchener
1d9345c3de
Fix typos.
2022-08-05 07:40:50 +03:00
Bruce Mitchener
5d0dea05aa
Remove empty leaf destructors. ( #6211 )
2022-07-30 10:07:03 +01:00
Nikolaj Bjorner
ac822acb0f
add parameter incremental to ensure preprocessing does not interefere with adding constraints during search
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-05 08:10:20 -07:00
Nikolaj Bjorner
94a2477fa0
totalizer
2022-06-30 19:49:19 -07:00
Nikolaj Bjorner
c3d2120bdd
add totalizer version of rc2
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-29 23:10:42 -07:00
Nikolaj Bjorner
5afcb489e0
adding totalizer
2022-06-29 08:20:01 -07:00
Nikolaj Bjorner
61f5489223
fix #6107
2022-06-27 16:53:18 -07:00
Nikolaj Bjorner
911134b3c7
add new heuristic rc2bin (to be tested) to maxsat
...
The rc2bin heuristic is a hybrid of rc2 and binary maxres.
It follows the suggestion by Nina to use rc2 on large cores after a single maxres relaxation step; otherwise maxres (binary) on smaller cores. In the design space of possible hybrids, this variant chooses to always apply a single layer of maxres and then rc2 for large cores.
2022-06-20 11:50:25 -07:00
Nuno Lopes
73a24ca0a9
remove '#include <iostream>' from headers and from unneeded places
...
It's harmful to have iostream everywhere as it injects functions in the compiled files
2022-06-17 14:10:19 +01:00
Christoph M. Wintersteiger
ed7db892f9
Fix a couple compiler warnings
2022-06-04 08:00:56 +01:00
Nikolaj Bjorner
b8532bec7e
remove pragma from cpp file
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 14:48:38 -07:00
Nikolaj Bjorner
c850259f89
rw
2022-05-22 07:54:27 -04:00
Nikolaj Bjorner
386c511f54
core opt
2022-05-21 10:27:37 -04:00
Nikolaj Bjorner
1e7a9e3e61
fix #6023
2022-05-08 12:03:13 -07:00
Nikolaj Bjorner
be653dab0e
init value
2022-05-01 15:26:57 -07:00
Nikolaj Bjorner
d1f1e4ce34
selectively enable dual strengthening
2022-05-01 15:26:57 -07:00
Nikolaj Bjorner
98e1c86128
na
2022-05-01 15:26:57 -07:00
Nikolaj Bjorner
9cc5f6901a
na
2022-05-01 15:26:57 -07:00
Nikolaj Bjorner
b5c7f000de
add option to "rotate" cores during core finding
...
enable to find multiple cores in a round and at the same time facilitate rotation around satisfiable subsets to explore neighborhoods for improved assignments.
2022-05-01 15:26:56 -07:00
Nikolaj Bjorner
0dd0fd26d4
remove buggy prototype
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-21 10:44:49 +01:00
Nikolaj Bjorner
d9f3625f93
change default output to print objective value
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-20 17:11:46 +01:00
Nikolaj Bjorner
ec57d3b15c
missing switch cases
2022-04-19 16:20:02 +01:00
Nikolaj Bjorner
df981666fd
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-18 16:27:46 +02:00
Nikolaj Bjorner
c727e2d048
add rc2 option
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-18 10:31:56 +02:00
Nikolaj Bjorner
4a59ae41b3
fixes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-16 19:19:05 +02:00
Nikolaj Bjorner
7496f11542
na
2022-04-16 18:30:35 +02:00
Nikolaj Bjorner
b5309d5fd0
na
2022-04-16 16:42:57 +02:00
Nikolaj Bjorner
c131eb4db1
build fix
2022-04-16 16:42:45 +02:00
Nikolaj Bjorner
f4c500c519
fix build
...
reference types are not part of C
2022-04-16 15:16:53 +02:00
Nikolaj Bjorner
807121aa03
wip
2022-04-16 14:55:43 +02:00
Nikolaj Bjorner
3cc9d7f443
improve pre-processing
2022-04-15 12:55:26 +02:00
Nikolaj Bjorner
3f5eb7fcf2
re-enable pre-process
2022-04-13 11:24:24 +02:00
Nikolaj Bjorner
ac55e29a56
disable propagation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-11 22:23:42 +02:00
Nikolaj Bjorner
c996a66da0
separate pre-processing, add callback parameter to push/pop in python API
2022-04-11 17:05:59 +02:00
Nikolaj Bjorner
405a26c585
allow adding constraints during on_model
2022-04-09 09:55:02 +02:00
Nikolaj Bjorner
d6d9b25c68
Allow adding constraints in the model_eh callback
2022-04-08 17:12:20 +02:00
Nikolaj Bjorner
994c7ef52d
format
2022-01-31 12:00:26 -08:00
Nikolaj Bjorner
7baa4f88b0
build failure
2022-01-06 15:17:57 -08:00
