mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
9419 commits 24 branches 48 tags 158 MiB
Commit graph

1393 commits

Author SHA1 Message Date
Arie Gurfinkel
27fc564d09 Remove bad assertion 2018-07-02 23:23:58 -04: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
5e3303ae85 let HORN solver know about cardinality constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 11:46:03 -07:00
Nuno Lopes
a73d030321 invertible_tactic: add partial support for shifts 2018-07-02 18:29:34 +01:00
Nikolaj Bjorner
080bf79fe6
Merge pull request #1705 from trinhmt/master 
created pull from Trinh's seq solver
 2018-06-30 04:53:14 -07:00
Nikolaj Bjorner
f1d27cd487 workaround non-deterministic behavior of is_irrational_numeral test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 18:16:32 -07:00
Nuno Lopes
bc8cd7ff55 remove a few random mem allocs 2018-06-29 18:34:17 +01:00
Nikolaj Bjorner
cbc5aaad2c strengthen simplification of to_int such that #1608 is handled during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 09:44:54 -07:00
Nuno Lopes
5de6628a5d remove spurious copies and inc_refs around ref_vector 2018-06-28 10:31:38 +01:00
Nikolaj Bjorner
eabe91cdef Merge branch 'master' of https://github.com/z3prover/z3 2018-06-27 17:05:52 -07:00
Nikolaj Bjorner
7844476a7d fixes to term-graph, add proof-checker routines for PR_BIND, remove orphaned file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 17:04:47 -07:00
Nikolaj Bjorner
91ef84b8c9 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-27 11:25:04 -07:00
Nikolaj Bjorner
20fc573d5b add laxer check for oeq_quant_intro 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 11:24:56 -07:00
Nikolaj Bjorner
06c9a9f3e1 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 08:51:22 -07:00
Nikolaj Bjorner
5762be2a0f fix 1703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 08:49:52 -07:00
trinhmt
54a9482716
Merge pull request #8 from Z3Prover/master 
merge with Z3Prover/z3
 2018-06-27 18:10:54 +08:00
Nuno Lopes
2b31024dab add obj_ref::operator=(obj_ref &&) + a few explicit uses 2018-06-26 17:00:56 +01:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:23:04 -07:00
Thai Trinh
aacb7289be merge with Z3Prover/master 2018-06-25 19:44:46 +08:00
Nikolaj Bjorner
8a29c2803c improvements to arithmetic preprocessing simplificaiton and axiom generation for #1683 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 07:04:39 -07:00
Nikolaj Bjorner
c3b27903f8 fix #1677 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 11:22:01 -07:00
Nikolaj Bjorner
b6c43f6143 move files for build script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:13:55 -07:00
Nikolaj Bjorner
2a6b7e5482 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
bc8ddedc54 fix a few build regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
49279d7047 debugging mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
7714d05c1a fill out qe_solve_plugin functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
dda65fdd2e mk_not: fix clang compilation issue 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
e6468726f5 more code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
c3fb863ad1 formatting/reviewing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
fca0442487 Fix proof_checker to use is_int_expr 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
8b689ae27f Moved is_int_expr into arith_recognizers 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
aa77a918cd Optimizing qe_lite 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
6514741e3f proof-checker: replace match_negated with ast_manager::is_complement 
is_complement matches true and false, while match_negated does not

Necessary to handle uses of true-axiom
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
9550fd1ec4 proof-checker: handle true-axiom 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
7931bd1dfc updates to mbqi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
ff0f257102 remove iff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel
10106e8e12 Minor fixes to ast_pp_dot 2018-06-14 16:08:48 -07:00
Arie Gurfinkel
6818eb3340 Improve factor equalities 2018-06-14 16:08:47 -07:00
Nikolaj Bjorner
63a1b2e714 fix #1665 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-08 10:30:20 -07:00
Nikolaj Bjorner
0d668e1428 fix #1661 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-30 03:18:22 -07:00
Nikolaj Bjorner
434ff31629
Merge pull request #1646 from NikolajBjorner/master 
Remove depedencies on interp
 2018-05-25 10:25:31 -07:00
Nikolaj Bjorner
753b9dd734 fix #1650 fix #1648 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-25 08:56:13 -07:00
Nikolaj Bjorner
4f5775c531 remove interpolation and duality dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-24 08:33:48 -07:00
Nikolaj Bjorner
0708ecb543 dealing with compilers that don't take typename in non-template classes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-23 09:11:33 -07:00
Nikolaj Bjorner
c963f6f2df merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-23 08:02:16 -07:00
Nikolaj Bjorner
50c93d1ad4 merge with 4.7.1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-22 17:10:36 -07:00
Nikolaj Bjorner
6938c76950
Merge pull request #1630 from danielschemmel/warnings 
Fix GCC Warnings
 2018-05-20 10:24:05 -07:00
Daniel Schemmel
5134c16833
NULL-initialize pointers to help GCC static analyzer Fixes: variable may be used uninitialized 2018-05-19 03:45:05 +02:00
Nikolaj Bjorner
925867dc3e fix #1621 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-18 14:14:00 -07:00
Nikolaj Bjorner
1e143971c3 tune for unit test, delay initialize re-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-13 11:49:33 -07:00