mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity
17296 commits 23 branches 48 tags 157 MiB
Commit graph

14599 commits

Author SHA1 Message Date
Nikolaj Bjorner e141759768 init solve_eqs 2022-11-03 03:35:29 -07:00
Clemens Eisenhofer 6790f18132
Added limit to "visit" to allow detecting multiple visits (#6435) 
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation

* Added limit to "visit" to allow detecting multiple visits

* Putting visit in a separate class
(Reason: We will probably need two of them in the sat::solver)

* Bugfix
 2022-11-03 03:34:52 -07:00
Nikolaj Bjorner e0bbe8dfc0 Merge branch 'master' of https://github.com/z3prover/z3 2022-11-02 17:32:32 -07:00
Nikolaj Bjorner df71e83428 remove incorrect assertion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-02 17:32:09 -07:00
Clemens Eisenhofer ae707ffff7
Added 64-bit "1" counting (#6434) 
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation

* Added 64-bit "1" counting
 2022-11-02 10:02:29 -07:00
Nikolaj Bjorner 0d97d2214c adding virtual destructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-02 09:37:55 -07:00
Nikolaj Bjorner 41b87b4c42 Create bv_slice_tactic.cpp 
missing file
 2022-11-02 08:51:43 -07:00
Nikolaj Bjorner e57674490f adding simplifiers layer 
simplifiers layer is a common substrate for global non-incremental and incremental processing.
The first two layers are new, but others are to be ported form tactics.

- bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values.
- euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization.

The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized.
 2022-11-02 08:51:30 -07:00
Nikolaj Bjorner 1646a41b2f minor fixes 
- ensure mk_extract performs simplification to distribute over extract and removing extract if the range is the entire bit-vector
- ensure bool_rewriter simplifeis disjunctions when applicable.
 2022-11-02 08:44:55 -07:00
Nikolaj Bjorner 9fc4015c46 remove ternary clause optimization 
Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured.
 2022-10-30 03:57:39 -07:00
Nikolaj Bjorner 0da0fa2b27 #6429 2022-10-29 13:43:07 -07:00
Nikolaj Bjorner 0e651eee04 #6421 2022-10-28 14:12:28 -07:00
Facundo Domínguez 91cdc082c4
Optimize calls to Z3_eval_smtlib2_string (#6422) 
* Allow reseting the stream of smt2::scanner

* Put the parser of parse_smt2_commands in the cmd_context

* Move parser streams to cmd_context

* Move parser fields from cmd_context to api::context

* Move forward declarations from cmd_context.h to api_context.h

* Change parse_smt2_commands_with_parser to use *& instead of **

* Add tests for Z3_eval_smtlib2_string

* Don't reuse the streams in Z3_eval_smtlib2_string

* Fix indentation

* Add back unnecessary deleted line

Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
 2022-10-28 13:57:22 -07:00
Nikolaj Bjorner a409a4a677 enforce flat within QF_BV tactic, cap in-processing var-elim loops 2022-10-27 20:10:55 -07:00
Nikolaj Bjorner 1fae3aa152 rename set-flat to set-flat-and-or to allow to differentiate parameters 2022-10-27 11:22:57 -07:00
Nikolaj Bjorner fe1b4bf5ce disable ternary, fixes to propagation, make bv_rewrites for multiplier n-ary 2022-10-26 23:44:38 -07:00
Nikolaj Bjorner 5352a0106d fix #6426 2022-10-26 12:20:55 -07:00
Nikolaj Bjorner 2258b9b9b6 #6423 2022-10-26 12:06:11 -07:00
Nuno Lopes 1720addc4e remove a bunch of string copies in the API 
thanks to C++20
 2022-10-26 18:22:55 +01:00
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 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 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
Nikolaj Bjorner 541aba308c fix #6401 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-17 10:27:15 -07:00
Nikolaj Bjorner dc1bce33f6 Merge branch 'master' of https://github.com/z3prover/z3 2022-10-17 10:17:40 -07:00
Nikolaj Bjorner 98fe2e637a add generic theory lemma in default case. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-17 10:17:08 -07:00
Gleb Popov 5b76a7c2f2
Enable HAS_MALLOC_USABLE_SIZE on FreeBSD (#6402) 2022-10-17 10:14:04 -07:00
Nikolaj Bjorner a25247aa7b wip - remove stale skaffolding for retrieving sub-hints. 2022-10-16 17:18:08 -07:00
Nikolaj Bjorner d88384fd51 fix compiler warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-16 15:03:46 -07:00
Nikolaj Bjorner 3ed791b16a fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-16 15:01:42 -07:00
Nikolaj Bjorner ac1552d194 wip - updates to proof logging and self-checking 
move self-checking functionality to inside sat/smt so it can be used on-line and not just off-line.

when self-validation fails, use vs, not clause, to check. It allows self-validation without checking and maintaining RUP validation.

new options sat.smt.proof.check_rup, sat.smt.proof.check for online validation.

z3 sat.smt.proof.check=true sat.euf=true /v:1 sat.smt.proof.check_rup=true /st file.smt2 sat.smt.proof=p.smt2
 2022-10-16 23:33:30 +02:00
Nikolaj Bjorner 993ff40826 fixes to proof logging and checking 2022-10-15 12:42:50 +02:00
Nikolaj Bjorner 4388719848 adjust logging 2022-10-14 18:56:18 +02:00
Nikolaj Bjorner e2cfc53c9f #6364 
skip proof hint unless proofs are on
 2022-10-13 15:31:58 +02:00
Nikolaj Bjorner 9bf5e3f5fc fixes for #6388 2022-10-13 15:22:19 +02:00
Nikolaj Bjorner 2449ba93c5 add (disabled) experiment to use quot-rem instead of division circuit 2022-10-13 15:20:43 +02:00
Nikolaj Bjorner 8a30128933 formatting updates 2022-10-13 15:20:24 +02:00
Nikolaj Bjorner 93e1db0b0b fix #6398 2022-10-13 11:16:14 +02:00
Nikolaj Bjorner ddf4895c2f admit timeouts and other resource limits for get-core #6310 2022-10-12 12:09:52 +02:00
Nuno Lopes a7f018aa03 fix compiler warnings 2022-10-12 10:02:21 +01:00
Nuno Lopes 8ad480ab59 fix compiler warnings 2022-10-12 09:43:50 +01:00
Nikolaj Bjorner a2e0646eed wip - proof checker 2022-10-12 09:34:49 +02:00
Nikolaj Bjorner ace727ee0f fix #6391 2022-10-12 09:34:49 +02:00
Nuno Lopes a41520acf1 mpf: fix some string copies 2022-10-11 11:59:29 +01:00
Nikolaj Bjorner 1b3684c9c1 wip - fixes to implied-eq proof hints 2022-10-11 09:54:00 +02:00
Nikolaj Bjorner ffeb8f4572 wip - tseitin check 
```
(set-option :sat.euf true)
(set-option :sat.smt.proof tseitinproof.smt2)
(set-option :tactic.default_tactic smt)

(declare-const a1 Bool)
(declare-const a2 Bool)
(declare-const a3 Bool)
(declare-const a4 Bool)
(declare-const a5 Bool)
(declare-const a6 Bool)
(declare-const a7 Bool)
(declare-const a8 Bool)
(declare-const a9 Bool)

(declare-const a10 Bool)
(declare-const a11 Bool)
(declare-const a12 Bool)
(declare-const a13 Bool)
(declare-const a14 Bool)
(declare-const a15 Bool)
(declare-const a16 Bool)
(declare-const a17 Bool)
(declare-const a18 Bool)
(declare-const a19 Bool)

(declare-const x1 Bool)
(declare-const x2 Bool)
(declare-const x3 Bool)
(declare-const x4 Bool)
(declare-const x5 Bool)
(declare-const x6 Bool)
(declare-const x7 Bool)
(declare-const x8 Bool)
(declare-const x9 Bool)

(declare-const b1 Int)
(declare-const b2 Int)
(declare-const b3 Int)
(declare-const b4 Int)

(assert (= x1 (and a1 a2)))
(assert (= x2 (or a3 a4)))
(assert (= x3 (=> a5 a6)))
(assert (= x4 (=  a7 a8)))
(assert (= x5 (if a9 a10 a11)))
(assert (= x6 (=> a12 a13)))
(assert (= x7 (xor a1 a2 a3)))
(assert (= x7 (xor a1 a2 a3 a4 a5 (not a6))))
(assert (= x8 (= (ite a1 b1 b2) b3)))
(check-sat)
(exit)

```
 2022-10-11 09:21:36 +02:00
Nikolaj Bjorner 62438da0f5 wip - add xor and non-bool ite tseitin rules 2022-10-11 09:15:18 +02:00
Nikolaj Bjorner cd8b8b603a tseitin rule checking - wip 
Unit test

```
(set-option :sat.euf true)
(set-option :sat.smt.proof tseitinproof.smt2)

(declare-const a1 Bool)
(declare-const a2 Bool)
(declare-const a3 Bool)
(declare-const a4 Bool)
(declare-const a5 Bool)
(declare-const a6 Bool)
(declare-const a7 Bool)
(declare-const a8 Bool)
(declare-const a9 Bool)

(declare-const a10 Bool)
(declare-const a11 Bool)
(declare-const a12 Bool)
(declare-const a13 Bool)
(declare-const a14 Bool)
(declare-const a15 Bool)
(declare-const a16 Bool)
(declare-const a17 Bool)
(declare-const a18 Bool)
(declare-const a19 Bool)

(declare-const x1 Bool)
(declare-const x2 Bool)
(declare-const x3 Bool)
(declare-const x4 Bool)
(declare-const x5 Bool)
(declare-const x6 Bool)
(declare-const x7 Bool)
(declare-const x8 Bool)
(declare-const x9 Bool)

(assert (= x1 (and a1 a2)))
(assert (= x2 (or a3 a4)))
(assert (= x3 (=> a5 a6)))
(assert (= x4 (=  a7 a8)))
(assert (= x5 (if a9 a10 a11)))
(assert (= x6 (=> a12 a13)))

(check-sat)
```

Output proof

```
(declare-fun a1 () Bool)
(declare-fun a2 () Bool)
(define-const $26 Bool (and a1 a2))
(declare-fun tseitin (Bool Bool) Proof)
(define-const $60 Bool (not $26))
(define-const $61 Proof (tseitin $60 a1))
(infer a1 (not $26) $61)
(define-const $62 Proof (tseitin $60 a2))
(infer a2 (not $26) $62)
(declare-fun tseitin (Bool Bool Bool) Proof)
(define-const $64 Bool (not a2))
(define-const $63 Bool (not a1))
(define-const $65 Proof (tseitin $63 $64 $26))
(infer (not a1) (not a2) $26 $65)
(declare-fun x1 () Bool)
(assume (not x1) $26)
(assume x1 (not $26))
(declare-fun a3 () Bool)
(declare-fun a4 () Bool)
(define-const $31 Bool (or a3 a4))
(define-const $66 Bool (not a3))
(define-const $67 Proof (tseitin $66 $31))
(infer (not a3) $31 $67)
(define-const $68 Bool (not a4))
(define-const $69 Proof (tseitin $68 $31))
(infer (not a4) $31 $69)
(define-const $70 Bool (not $31))
(define-const $71 Proof (tseitin a3 a4 $70))
(infer a3 a4 (not $31) $71)
(declare-fun x2 () Bool)
(assume (not x2) $31)
(assume x2 (not $31))
(declare-fun a6 () Bool)
(declare-fun a5 () Bool)
(define-const $38 Bool (not a5))
(define-const $39 Bool (or a6 $38))
(define-const $72 Bool (not a6))
(define-const $73 Proof (tseitin $72 $39))
(infer (not a6) $39 $73)
(define-const $74 Proof (tseitin a5 $39))
(infer a5 $39 $74)
(define-const $75 Bool (not $39))
(define-const $76 Proof (tseitin a6 $38 $75))
(infer a6 (not a5) (not $39) $76)
(declare-fun x3 () Bool)
(assume (not x3) $39)
(assume x3 (not $39))
(declare-fun a7 () Bool)
(declare-fun a8 () Bool)
(define-const $44 Bool (= a7 a8))
(define-const $78 Bool (not a7))
(define-const $77 Bool (not $44))
(define-const $79 Proof (tseitin $77 a8 $78))
(infer (not a7) a8 (not $44) $79)
(define-const $80 Bool (not a8))
(define-const $81 Proof (tseitin $77 $80 a7))
(infer a7 (not a8) (not $44) $81)
(define-const $82 Proof (tseitin $44 a8 a7))
(infer a7 a8 $44 $82)
(define-const $83 Proof (tseitin $44 $80 $78))
(infer (not a7) (not a8) $44 $83)
(declare-fun x4 () Bool)
(assume (not x4) $44)
(assume x4 (not $44))
(declare-fun a9 () Bool)
(declare-fun a10 () Bool)
(declare-fun a11 () Bool)
(define-const $50 Bool (ite a9 a10 a11))
(define-const $85 Bool (not a9))
(define-const $84 Bool (not $50))
(define-const $86 Proof (tseitin $84 $85 a10))
(infer (not a9) a10 (not $50) $86)
(define-const $87 Proof (tseitin $84 a9 a11))
(infer a9 a11 (not $50) $87)
(define-const $88 Bool (not a10))
(define-const $89 Proof (tseitin $50 $85 $88))
(infer (not a9) (not a10) $50 $89)
(define-const $90 Bool (not a11))
(define-const $91 Proof (tseitin $50 a9 $90))
(infer a9 (not a11) $50 $91)
(define-const $92 Proof (tseitin $88 $90 $50))
(infer (not a10) (not a11) $50 $92)
(define-const $93 Proof (tseitin a10 a11 $84))
(infer a10 a11 (not $50) $93)
(declare-fun x5 () Bool)
(assume (not x5) $50)
(assume x5 (not $50))
(declare-fun a13 () Bool)
(declare-fun a12 () Bool)
(define-const $57 Bool (not a12))
(define-const $58 Bool (or a13 $57))
(define-const $94 Bool (not a13))
(define-const $95 Proof (tseitin $94 $58))
(infer (not a13) $58 $95)
(define-const $96 Proof (tseitin a12 $58))
(infer a12 $58 $96)
(define-const $97 Bool (not $58))
(define-const $98 Proof (tseitin a13 $57 $97))
(infer a13 (not a12) (not $58) $98)
(declare-fun x6 () Bool)
(assume (not x6) $58)
(assume x6 (not $58))

```
 2022-10-10 23:44:03 +02:00
Nikolaj Bjorner fceedf60dc wip - proofs 2022-10-10 16:41:09 +02:00
Nikolaj Bjorner de69874076 wip - adding proof checkers, fixes to quantifier proof certificates 2022-10-10 09:46:22 +02:00
Nikolaj Bjorner 4623117af8 wip - proof hints 2022-10-08 20:12:57 +02:00
Nikolaj Bjorner 6796ea7e49 add new files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-07 19:22:36 +02:00
Nikolaj Bjorner 35639c5ac0 adding q proof hints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-07 19:21:21 +02:00
Nuno Lopes 661a1624b4 avoid string copying in mpf_manager::set 2022-10-07 14:03:13 +01:00
Nikolaj Bjorner 5c9f69829b fixes to trim 2022-10-07 09:58:12 +02:00
Nuno Lopes a792251a82 remove old compat code 2022-10-06 17:22:17 +01:00
Nikolaj Bjorner 9f78a96c1d wip - trim 2022-10-06 18:19:03 +02:00
Nikolaj Bjorner 4e780d0cc8 trim 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-05 05:43:48 +02:00
Nikolaj Bjorner f8ca692dee fixes to trim 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-05 04:32:00 +02:00
Nikolaj Bjorner c1c659dc93 trying trim 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-04 16:25:40 +02:00
Nikolaj Bjorner d22c86f9fe init spacer_iuc_solver properly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-03 15:53:58 -04:00
Nikolaj Bjorner 6e05162df0 update solver only if there is a manager 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-03 15:27:26 -04:00
Nikolaj Bjorner b03d4e4fc2 update solver only if there is a manager 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-03 15:26:10 -04:00
Nikolaj Bjorner 5b71f7cf9e Merge branch 'master' of https://github.com/z3prover/z3 2022-10-03 15:19:01 -04:00
Nuno Lopes be3c7d7115 delete dead code 2022-10-02 21:44:08 +01:00
Nuno Lopes 1eed058b98 use std::move 2022-10-02 21:34:17 +01:00
Nikolaj Bjorner ad49dd739b initialize variables to avoid warning messages whether real or spurious 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-01 17:08:02 -04:00
Nikolaj Bjorner cffe5fe1a5 remove debug print 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-01 17:05:36 -04:00
Nuno Lopes 24ff0f2d36 attempt to fix cmake build 2022-10-01 21:48:27 +01:00
Naxaes 49ebca6c1c
Fix clang build (#6378) 2022-10-01 14:01:36 +01:00
Nuno Lopes 47e44c5538 fix build 2022-10-01 12:17:15 +01:00
Nikolaj Bjorner 903cddcaaa fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-30 17:10:18 -04:00
Nikolaj Bjorner ab045f0645 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-30 16:52:19 -04:00
Nikolaj Bjorner 876ca2f1a5 fix #6371 2022-09-30 14:51:28 -04:00
Nikolaj Bjorner b9cba82531 work on proof checking 
- add outline of trim routine
- streamline how proof terms are checked and how residue units are extracted.
 2022-09-30 13:04:19 -04:00
Nikolaj Bjorner ccda49bad5 fix #6376 
have solver throw an exception when user supplies a non-propositional assumption
 2022-09-30 13:03:34 -04: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 9782d4a730 #5261 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-26 05:04:02 -07:00
Nikolaj Bjorner 7b982a812e fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-25 18:09:32 -07:00
Nikolaj Bjorner 3df8b9c7e2 Merge branch 'master' of https://github.com/z3prover/z3 2022-09-25 18:03:26 -07:00
Nikolaj Bjorner d7b9cc70d0 smc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-25 18:03:16 -07:00
Nikolaj Bjorner 9be8fc7857 Add EUF (congruence closure) proof hints and checker to the new core 
EUF proofs are checked modulo union-find.
Equalities are added to to union-find if they are assumptions or if they can be derived using congruence closure. The congruence closure assumptions are added as proof-hints.
Note that this proof format does not track equality inferences, symmetry and transitivity. Instead they are handled by assuming a union-find based checker.
 2022-09-25 14:26:20 -07:00
Nikolaj Bjorner 6f2fde87d1 move has-default up before merge of parents 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-24 14:40:30 -07:00
Clemens Eisenhofer 5ca53f37c0
Throw an exception if the variable in decide-callback is already assigned (#6362) 
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation
 2022-09-24 09:54:14 -07:00
Nikolaj Bjorner 3dfff3d7a1 tracing for fpa 2022-09-23 22:48:54 -07:00
Nikolaj Bjorner 1f150ecd52 #6319 
#6319 - fix incompleteness in propagation of default to all array terms in the equivalence class.

Fix bug with q_mbi where domain restrictions are not using values because the current model does not evaluate certain bound variables to values. Set model completion when adding these bound variables to the model to ensure their values are not missed.

Add better propagation of diagnostics when tactics and the new solver return unknown. The reason for unknown can now be traced to what theory was culprit (currently no additional information)
 2022-09-23 22:22:34 -05:00
Nikolaj Bjorner 6226875283 fix regression with uninitialized variable 2022-09-23 15:51:26 -05:00
Nikolaj Bjorner c41b6da6bb #6319 
using a queue for disequality propagaiton was a regression: values of numerals can change along the same stack so prior passing the filter does not mean it passes later.
 2022-09-23 14:47:48 -05:00
Nikolaj Bjorner 79b4357442 #6363 2022-09-23 14:32:01 -05:00
Nikolaj Bjorner 3d9512b93c fix #6363 2022-09-23 14:32:01 -05:00
Nikolaj Bjorner de74e342c6
#5261 2022-09-23 13:19:55 -05:00
Nikolaj Bjorner 4c6d7158cb extended debugging for sat.euf 2022-09-22 17:05:32 -05:00
Nikolaj Bjorner c24d445886 fix #6355 
conversion from AIG to expressions should always use the optimized conversion function.

the aig-tactic should throttle regarding output bloat from AIG.
If the expression after AIG simpification, for whatever reason, is bloated the rewrite does not take place.
 2022-09-22 17:05:32 -05:00
gmh5225 b0d0c36b11
Add option 'MSVC_STATIC' (#6358) 
* Add option 'MSVC_STATIC'

* Update CMakeLists.txt

* Update CMakeLists.txt

* Upload msvc-static-build.yml
 2022-09-22 15:55:40 -05:00
Clemens Eisenhofer a67fe054d5
Memory leak in .NET user-propagator (#6360) 
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
 2022-09-22 13:26:08 -05:00
Peter Bruch 58fad41dfa
Dotnet Api: Fix infinite finalization of Context (#6361) 
* Dotnet Api: suppress GC finalization of dotnet context in favor of re-registering finalization

* Dotnet Api: enable concurrent dec-ref even if context is created without parameters.

* Dotnet Api: removed dead code.
 2022-09-22 13:25:17 -05: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
Nikolaj Bjorner eba5a5d141 Merge branch 'master' of https://github.com/z3prover/z3 2022-09-20 20:32:07 -07:00
Nikolaj Bjorner 4518f4fe02 fix #6352 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-20 20:31:55 -07:00
Nikolaj Bjorner 20250b200f #6319 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-19 20:31:36 -07:00
Nikolaj Bjorner 7caf6a682b #6319 resolve for unsat core when using assumptions 2022-09-19 20:10:53 -07:00
Nikolaj Bjorner f4bea58852 #6319 
ensure unknown when a lambda is not in beta redex
 2022-09-19 03:19:47 -07:00
Nikolaj Bjorner fce4d2ad90 #6319 2022-09-19 03:07:51 -07:00
Nikolaj Bjorner d6d34a8962 #6319 2022-09-19 02:32:04 -07:00
Nikolaj Bjorner 13f43ea107 bug fix for #6319 
literals that are replayed need to be registered with respective theories, otherwise, they will not propagate with the theories (the enode have to be attached with relevant theory variables).
 2022-09-18 17:23:00 -07:00
Nikolaj Bjorner e54635e0ed rename statistics to something more meaningful: instantiations from MBQI are tagged with mbi 2022-09-18 17:23:00 -07:00
Nikolaj Bjorner 2b4ba5e170 updated header file for arithmetic solver 2022-09-18 17:23:00 -07:00
Nikolaj Bjorner 0b9c9cbbce add a queue head to delay propagation 
delay propagation on each disequality/equality should suffice once. It adds relevant inequalities to ensure the arithmetic solver is coherent about disequalities.
 2022-09-18 17:23:00 -07:00