mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity
9698 commits 23 branches 48 tags 157 MiB
Commit graph

9698 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes cd482c683e invertible tactic: fix bugs with shift 2018-07-03 17:18:00 +01:00
Nikolaj Bjorner e37954d87b simplify code fix for #1725 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 09:16:52 -07:00
Nikolaj Bjorner ec6260342b fix #1725 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 09:13:02 -07:00
Nikolaj Bjorner 026265f9a3 fix memory leak in proof production in theory_pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 08:55:26 -07:00
Nikolaj Bjorner a4dfde4671 fix pointer deref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 06:56:37 -07:00
Nikolaj Bjorner 810d63c246 put mpz_cell under ifdef _NO_GMP 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 06:54:50 -07:00
Nikolaj Bjorner 6981918c33 Merge branch 'master' of https://github.com/z3prover/z3 into lev 2018-07-03 06:51:08 -07:00
Nikolaj Bjorner c749dba76f
Merge pull request #1724 from levnach/lev 
make lp_tst optional
 2018-07-03 06:47:48 -07:00
Nikolaj Bjorner 282b781d88
Merge pull request #1723 from agurfinkel/deep_space 
Deep space
 2018-07-03 06:47:34 -07:00
Arie Gurfinkel 27fc564d09 Remove bad assertion 2018-07-02 23:23:58 -04:00
Lev Nachmanson 8b4223fef2 make lp_tst optional 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-02 19:50:29 -07:00
Arie Gurfinkel 8502f1fe36 Fix in proof_util:elim_aux_assertions 
Replace assertions/hypotheses of aux variables with PR_TRUE.
Rebuild unit resolution as needed.
This makes the transformation stable against new proof rules.
 2018-07-02 21:37:30 -04:00
Nikolaj Bjorner 3a4200ae5f null -> nullptr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 18:32:03 -07:00
Nikolaj Bjorner ace4dbe32b fix memory leak exposed by tan.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 18:15:39 -07:00
Nikolaj Bjorner c06ed77ff1 fix merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 15:37:33 -07:00
Nikolaj Bjorner 03ed33ac02 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 15:31:26 -07:00
Nikolaj Bjorner 4e657b5b7e rename mpz_ptr to mpz_large 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 15:29:57 -07:00
Arie Gurfinkel 5d1149adb2 Transformation to eliminate term-ite expressions from DL rules 2018-07-02 17:09:56 -04:00
Arie Gurfinkel 6d75c31468 First draft of elim_term_ite xform. Not working. 2018-07-02 17:09:56 -04:00
Arie Gurfinkel 7acea2791d -tr:spacer.expand-add --> -tr:spacer_progress 2018-07-02 17:09:56 -04:00
Nikolaj Bjorner dc8ec50137 enable proof objects for PB 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 13:53:55 -07:00
Nikolaj Bjorner cf8618bf3c
Merge pull request #1721 from levnach/lev 
changed in for loops for terms
 2018-07-02 12:17:54 -07:00
Lev Nachmanson fbf0d0d7b2 changed in for loops for terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-02 11:46:46 -07:00
Nikolaj Bjorner 5e3303ae85 let HORN solver know about cardinality constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 11:46:03 -07:00
Nikolaj Bjorner fcd9936e88 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-02 11:10:42 -07:00
Nikolaj Bjorner e13b61eae8 work around regression with use of mk_app_core, returning BR_FAILED if nothing is rewritten 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 11:10:37 -07:00
Nuno Lopes a73d030321 invertible_tactic: add partial support for shifts 2018-07-02 18:29:34 +01:00
Nikolaj Bjorner 648a531950 update java example to bypass bit-rot 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 09:50:29 -07:00
Nikolaj Bjorner 370abf602c fix java API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 09:32:58 -07:00
Nikolaj Bjorner a406b8e93a Merge branch 'master' of https://github.com/z3prover/z3 2018-07-02 09:10:13 -07:00
Nikolaj Bjorner 1f5d182f6a update java bindings for arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 09:09:57 -07:00
Nuno Lopes cef17c22a1 remove some allocs from exceptions 2018-07-02 17:08:02 +01:00
Nikolaj Bjorner ca3c076394 fixed reduce 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 08:26:10 -07:00
Nikolaj Bjorner 05738702d6 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 08:10:47 -07:00
Nikolaj Bjorner 4820e51c53 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 08:10:14 -07:00
Nuno Lopes 8791f61aa7 reduce mem allocation in tactic API 2018-07-02 13:41:44 +01:00
Nikolaj Bjorner 61d887b36f use for pattern 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 04:35:22 -07:00
Nikolaj Bjorner 88dd9ac668 add back get_value that uses solver model, have assume_eqs only use those variables (not the impqs) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 04:29:54 -07:00
Nikolaj Bjorner 46ea054784 merge get_value and get_ivalue that produced different results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 03:55:40 -07:00
Nuno Lopes fc8193828d minor simplifications to symbol class 2018-07-02 11:43:00 +01:00
Nikolaj Bjorner 0d4b4b30b1 change storage layout of .Net binding Z3_bool to byte to deal with uninitialized memory reads on larger allocation sizes. Bug introduced when switching from defining Z3_bool as int to the bool type from stdbool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 02:58:06 -07:00
Nikolaj Bjorner 2ab0681381 deal with unintialized variable in debug code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 19:34:27 -07:00
Nikolaj Bjorner b38abf64d7 use expr_ref on mk_concat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 19:30:46 -07:00
Nikolaj Bjorner 8895ed7122 remove unintialized variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 18:34:02 -07:00
Nikolaj Bjorner b6054b8406 add has_value utility to retrieve value from solver state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 17:03:58 -07:00
Nikolaj Bjorner 13413d0529 update for int return value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 15:08:16 -07:00
Nikolaj Bjorner 593a6e5139 update smt_setup and default parameters to only use new solver consveratively 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 12:52:50 -07:00
Nikolaj Bjorner fad1e611aa build warnings, updates to reduce-invertible, change is_algebraic tester to use int return type 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 12:34:55 -07:00
Nikolaj Bjorner 5a2a8d7d5c
Merge pull request #1715 from levnach/master 
merge lar_solver/int_solver
 2018-07-01 12:20:02 -07:00
Nikolaj Bjorner b8b70c53fa update invertible tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 09:17:20 -07:00