mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
4399 commits 46 branches 52 tags 178 MiB
Commit graph

4399 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alex Horn
c8a123b7dd Disable a few rule transformations 
For this prototype, we need to disable three rule transformations,
namely coi_filter, similarity_compressor, rule_inliner. But
disabling the inliner causes problems with the tracer in the
datalog interpreter. Since a new proprocessor is underway, we
skip the problematic trace outputs for now.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-11 16:16:47 +01:00
Christoph M. Wintersteiger
d3df473279 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-11 12:53:31 +01:00
Christoph M. Wintersteiger
5bd55420a4 C API parameter annotation fix 2015-06-11 12:53:22 +01:00
Alex Horn
565c0f785f Fix memory leaks 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-11 09:20:52 +01:00
Alex Horn
bd57994f78 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into minimum 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>

Conflicts:
	src/test/dl_table.cpp
 2015-06-10 20:35:28 +01:00
Alex Horn
132f984d51 Add syntactical min checker 
The purpose of this patch is to find out more about the "shape" of
the constraints in our benchmarks. In particular, we would like to
determine whether aggregation and negation, together, appear in
recursive rules.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 20:19:14 +01:00
Alex Horn
9b7c5658c8 Ignore min aggregation functions in compiler for now 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 20:06:09 +01:00
Nikolaj Bjorner
e0068e4065 C/right on python scripts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 12:01:47 -07:00
Alex Horn
e6ffa5d2a5 Enable datalog plugin for AST extensions 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 19:59:57 +01:00
Nikolaj Bjorner
d469a16bb8 add more Copyright notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:59:21 -07:00
Nikolaj Bjorner
b08ccc7816 added missing Copyright forms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:54:02 -07:00
Aleksandar Zeljic
08b3f9b46e Removed the fpa2bv_porec model converter which was outdated and causing evaluation bugs. 2015-06-10 19:57:32 +02:00
Alex Horn
140fb7942d Add datalog infrastructure for min aggregation function 
This patch adds an instruction to the datalog interpreter and
constructs a new AST node for min aggregation functions.

The compiler is currently still work in progress and depends on
changes made to the handling of simple joins and the preprocessor.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 18:14:14 +01:00
Christoph M. Wintersteiger
004bf1471f Added conversion function for Goal to Expr conversion in .NET, Java, ML 2015-06-10 13:17:34 +01:00
Aleksandar Zeljic
a37ec41370 Buggy version, a full model is found but evaluation finds it to be invalid. 2015-06-09 21:16:53 +02:00
Christoph M. Wintersteiger
98f2de3216 Added Z3_fpa_get_numeral_significand_uint64 to .NET, Java, and ML APIs. 2015-06-09 12:57:19 +01:00
Christoph M. Wintersteiger
da3243fb07 FPA API bugfix 2015-06-09 12:29:05 +01:00
Christoph M. Wintersteiger
eb3d499888 documentation fix 2015-06-09 12:28:52 +01:00
Christoph M. Wintersteiger
d39969f0a0 Added extraction of uint64 significand bits from FP numerals. 2015-06-09 12:28:23 +01:00
Christoph M. Wintersteiger
624cc8a874 Bugfixes for FPA API. Thanks to Christian Dernehl for reporting these. 2015-06-09 11:53:43 +01:00
Nikolaj Bjorner
fd0c86ec7d remove tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-08 08:44:30 -07:00
Christoph M. Wintersteiger
f920644892 Parameter fix for the qflia default tactic 2015-06-08 15:37:17 +01:00
Christoph M. Wintersteiger
24a5ff825a Fixed collect_param_descrs in pb2bv tactic. 2015-06-08 15:36:00 +01:00
Christoph M. Wintersteiger
3e1042c680 Exported the quasi-pb probe as per user request. 2015-06-08 15:35:29 +01:00
Nuno Lopes
0997d0d2b5 add new C API function: Z3_finalize_memory() 
Useful to debug memory leaks in Z3 and in client applications

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-07 14:55:15 +01:00
aleze648
444dc0ed0a Added missing cases for positive zero, negative zero and is positive. 2015-06-07 05:31:10 -07:00
Nuno Lopes
6217804ed5 fix another UB in bit_vector 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-07 12:07:24 +01:00
Nuno Lopes
2733899c01 remove unused var 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-05 09:30:44 +01:00
Nuno Lopes
b65d5797f8 optimize expr_safe_replace for when a subexpression has no substitutions 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-03 17:21:01 +01:00
AleksandarZeljic
575dc20d22 Merge pull request #1 from wintersteiger/bugfixes 
Bugfixes
 2015-06-03 16:50:26 +02:00
Nikolaj Bjorner
9734407cde disable throttle on unbounded objectives in shared theories. It may violate an interface equality, to fix issue #120 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 11:14:59 -07:00
Christoph M. Wintersteiger
5c67db8dc6 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into bugfixes 2015-06-02 19:00:15 +01:00
Nikolaj Bjorner
171ef5c8e3 Merge pull request #117 from mschlaipfer/unstable 
Missing input format option "-dl" and non-deterministic behaviour in fixpoint engine
 2015-06-02 10:48:17 -07:00
Nikolaj Bjorner
c09ac5422b fix by anomaly detection, issue #118 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 10:42:03 -07:00
Christoph M. Wintersteiger
bee22a306e Merge branch 'unstable' of https://github.com/Z3Prover/z3 into bugfixes 2015-06-02 18:41:28 +01:00
Christoph M. Wintersteiger
c910ed2eae fpa2bv_approx: bugfix for fp.abs 2015-06-02 18:40:11 +01:00
Nikolaj Bjorner
bb210d225a Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-02 10:38:50 -07:00
Nikolaj Bjorner
d06207f072 remove ite terms from objectives to synchronize values in tableau with objective value. Fixes part of (three repros) from issue #120 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 10:38:22 -07:00
Christoph M. Wintersteiger
a93bb92240 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into bugfixes 2015-06-02 18:36:45 +01:00
Christoph M. Wintersteiger
81218c0983 Bugfix for fp.fma 2015-06-02 18:36:19 +01:00
Christoph M. Wintersteiger
f68469173f Merge branch 'unstable' of https://github.com/Z3Prover/z3 into bugfixes 2015-06-02 18:32:01 +01:00
Christoph M. Wintersteiger
3f32732ec9 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-02 18:31:31 +01:00
Christoph M. Wintersteiger
a7b12e6321 Bugfix for fp.fma with sbits <= 3 2015-06-02 18:31:09 +01:00
Christoph M. Wintersteiger
610c549104 fpa2bv_approx: added fp.abs, fixed rounding mode model extraction 2015-06-02 18:17:49 +01:00
Christoph M. Wintersteiger
65a6845945 Bugfix for fpa2bv_converter_prec 2015-06-02 17:19:31 +01:00
Christoph M. Wintersteiger
599e5b6838 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into bugfixes 2015-06-02 17:16:42 +01:00
Nikolaj Bjorner
ffff006945 remove old files 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 09:15:08 -07:00
Christoph M. Wintersteiger
a07cba72bc eliminated unused variables 2015-06-02 17:15:07 +01:00
Christoph M. Wintersteiger
8f388d83a2 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-02 17:00:44 +01:00
Nikolaj Bjorner
7161d6c150 fixes crash from issue #119 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 08:48:37 -07:00