Nikolaj Bjorner
e2f4fc2307
overhaul of proof format for new solver
...
This commit overhauls the proof format (in development) for the new core.
NOTE: this functionality is work in progress with a long way to go.
It is shielded by the sat.euf option, which is off by default and in pre-release state.
It is too early to fuzz or use it. It is pushed into master to shed light on road-map for certifying inferences of sat.euf.
It retires the ad-hoc extension of DRUP used by the SAT solver.
Instead it relies on SMT with ad-hoc extensions for proof terms.
It adds the following commands (consumed by proof_cmds.cpp):
- assume - for input clauses
- learn - when a clause is learned (or redundant clause is added)
- del - when a clause is deleted.
The commands take a list of expressions of type Bool and the
last argument can optionally be of type Proof.
When the last argument is of type Proof it is provided as a hint
to justify the learned clause.
Proof hints can be checked using a self-contained proof
checker. The sat/smt/euf_proof_checker.h class provides
a plugin dispatcher for checkers.
It is instantiated with a checker for arithmetic lemmas,
so far for Farkas proofs.
Use example:
```
(set-option :sat.euf true)
(set-option :tactic.default_tactic smt)
(set-option :sat.smt.proof f.proof)
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const u Int)
(assert (< x y))
(assert (< y z))
(assert (< z x))
(check-sat)
```
Run z3 on a file with above content.
Then run z3 on f.proof
```
(verified-smt)
(verified-smt)
(verified-smt)
(verified-farkas)
(verified-smt)
```
2022-08-28 17:44:33 -07:00
Nikolaj Bjorner
49064252ac
fix issues for user-propagator from new core
2022-08-09 14:56:27 +03:00
Bruce Mitchener
5d0dea05aa
Remove empty leaf destructors. ( #6211 )
2022-07-30 10:07:03 +01:00
Nikolaj Bjorner
386c511f54
core opt
2022-05-21 10:27:37 -04:00
Nikolaj Bjorner
ef28f0e2f0
#5778
...
deal with recursive calls to internalization with the same formula
2022-04-02 01:28:58 -07:00
Nikolaj Bjorner
4392b88718
return negated literal when expression is "not"
2022-01-31 12:00:00 -08:00
Nikolaj Bjorner
d1fb831030
relevancy overhaul
2022-01-04 16:03:31 -08:00
Nikolaj Bjorner
8e3185ffe3
remove dual solver approach
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-03 14:08:01 -08:00
Nikolaj Bjorner
1f964eea90
na
2022-01-03 11:12:28 -08:00
Nikolaj Bjorner
2944449884
#5641
2022-01-03 11:12:09 -08:00
Jamey Sharp
426306376f
CNF conversion refactoring ( #5547 )
...
* split sat2goal out of goal2sat
These two classes need different things out of the sat::solver class,
and separating them makes it easier to fiddle with their dependencies
independently.
I also fiddled with some headers to make it possible to include
sat_solver_core.h instead of sat_solver.h.
* limit solver_core methods to those needed by goal2sat
And switch sat2goal and sat_tactic over to relying on the derived
sat::solver class instead. There were no other uses of solver_core.
I'm hoping this makes it feasible to reuse goal2sat's CNF conversion
from places like the tseitin-cnf tactic, so they can be unified into a
single implementation.
2021-09-20 08:53:10 -07:00
Nikolaj Bjorner
e05ef8ece9
account for updating scoped state by goal2sat #5528
2021-09-02 04:20:19 -07:00
Nikolaj Bjorner
fc36fb115f
format
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-02 13:45:23 -07:00
Nikolaj Bjorner
d3194bb8a8
#5445
2021-08-02 11:07:28 -07:00
Nikolaj Bjorner
e3be25dad6
#5445
2021-08-01 16:48:25 -07:00
Nikolaj Bjorner
924ea6ab31
#5429 again
2021-08-01 12:00:22 -07:00
Nikolaj Bjorner
ed27ce5526
fix regression in goal2sat
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-31 11:41:55 -07:00
Nikolaj Bjorner
6a9241ff0f
#5429
2021-07-31 11:00:12 -07:00
Nikolaj Bjorner
77cd82a5ca
flatten if-then-else
2021-07-30 23:28:30 -07:00
Nikolaj Bjorner
442d1d28ea
#5429
2021-07-27 19:11:16 -07:00
Nikolaj Bjorner
76427cd281
#5427
2021-07-22 11:33:47 -07:00
Nikolaj Bjorner
8a4b292f3e
#5422
2021-07-21 06:25:30 -07:00
Nikolaj Bjorner
34fc0cdd5c
#5324
2021-06-06 16:23:27 -07:00
Nikolaj Bjorner
4d41db2920
#5223
...
unreachable code in dual solver
2021-05-29 09:49:47 -07:00
Nikolaj Bjorner
abe3ef2382
#5215
2021-05-19 10:33:23 -07:00
Nikolaj Bjorner
a61e9d6b49
#5260
2021-05-10 10:33:43 -07:00
Nikolaj Bjorner
4a6083836a
call it data instead of c_ptr for approaching C++11 std::vector convention.
2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
c629f09f21
fix #5139
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-29 15:46:47 -07:00
Nikolaj Bjorner
dfb696becf
fix #5119
2021-03-28 16:47:56 -07:00
Nikolaj Bjorner
8412ecbdbf
fixes to new solver, add mode for using nlsat solver eagerly from nla_core
2021-03-14 13:57:04 -07:00
Nikolaj Bjorner
e398959732
move eq solver functionality to common place, fixes to goal2sat
2021-03-04 07:57:31 -08:00
Nikolaj Bjorner
79ababb00a
force push
2021-03-03 11:38:33 -08:00
Nikolaj Bjorner
69070a7486
align translation cache with scopes and variable elimination
2021-03-03 11:22:17 -08:00
Nikolaj Bjorner
026065ff71
streamline pb solver interface and naming after removal of xor
2021-02-28 12:32:04 -08:00
Nikolaj Bjorner
4455f6caf8
move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail
2021-02-02 03:58:19 -08:00
Nikolaj Bjorner
bb56443e71
more #4932
2021-01-08 15:24:12 -08:00
Nikolaj Bjorner
cd77a4d9a5
fix #4909
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-12-20 11:53:19 -08:00
Nikolaj Bjorner
4d55f83654
misc
2020-12-04 16:59:13 -08:00
Nikolaj Bjorner
12198d13ac
fix #4794
2020-12-02 12:24:35 -08:00
Nikolaj Bjorner
85a20791db
fix relevancy tracking in new solver
2020-11-16 11:20:17 -08:00
Nikolaj Bjorner
7e68d546ba
na
2020-11-11 17:37:07 -08:00
Nikolaj Bjorner
8d76470a8a
fixes to mostly solver arith/euf and backtracking scopes
2020-10-26 11:06:41 -07:00
Nikolaj Bjorner
72d407a49f
mbp ( #4741 )
...
* adding dt-solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* dt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move mbp to self-contained module
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Create CMakeLists.txt
* dt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* rename to bool_var2expr to indicate type class
* mbp
* na
* add projection
* na
* na
* na
* na
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* deps
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* testing arith/q
* na
* newline for model printing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-10-21 15:48:40 -07:00
Nikolaj Bjorner
44679d8f5b
arith_solver ( #4733 )
...
* porting arithmetic solver
* integrating arithmetic
* lp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-10-16 10:49:46 -07:00
Nikolaj Bjorner
a414480274
mbi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-29 15:49:48 -07:00
Nikolaj Bjorner
367e5fdd52
delay internalize ( #4714 )
...
* adding array solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use default in model construction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* debug delay internalization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* get rid of implied values and bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* redo egraph
* remove out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-28 19:24:16 -07:00
Nikolaj Bjorner
7c2bdfe3fb
delay internalization, relevancy ( #4707 )
...
* delay evaluation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update bv_solver.cpp
* delay internalize
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove gc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add bv delay option
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-23 17:12:01 -07:00
Nikolaj Bjorner
6f63f8761c
optimizations to bv-solver and euf-egraph ( #4698 )
...
* additional bit-vector propagators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* rename restrict (not a keyword, but well) #4694 , tune euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add pb rewriting to pb2bv #4697
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-20 06:47:27 -07:00
Nikolaj Bjorner
8691ef1d4d
additional bit-vector propagators ( #4695 )
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-18 12:38:29 -07:00
Nikolaj Bjorner
549753845e
bv and gc of literals ( #4692 )
...
* bv and gc of literals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* overload
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* diseq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* diseq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-17 14:24:07 -07:00
