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

172 commits

Author SHA1 Message Date
Nikolaj Bjorner
62a4737d77 disable code in dl_query that depends on hard-wired file path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:30:12 -07:00
Nikolaj Bjorner
074ff58739 include rlimit in nlsat, include dedicated error message, for issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 09:27:34 -07:00
Christoph M. Wintersteiger
0cf18ab18e Propagated rlimit changes to sat::solver into sat_user_scope tests 2015-09-29 11:50:10 +01:00
Nikolaj Bjorner
ad16cc0ce2 fix unit test for datalog parser, fixes issue #224 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 11:16:55 -07:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Nikolaj Bjorner
e2adcc19ec fix unit test for default exception 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-06 22:52:44 -07:00
Nikolaj Bjorner
c3e666bc44 fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 07:40:23 +02:00
Nikolaj Bjorner
18374aa12a deal with unit test failure cases, fixes #132 #133 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-17 17:30:10 -07:00
Matthias Schlaipfer
32a00a7062 Fixed a bug in udoc_relation's join project 
An optimization was applied in too many cases and led to wrong results.

Signed-off-by: Matthias Schlaipfer <t-matsch@microsoft.com>
 2015-06-17 17:14:23 +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
Nikolaj Bjorner
b08ccc7816 added missing Copyright forms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:54:02 -07: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
Nuno Lopes
08b5635327 fix unaligned load in hash_string() 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-23 12:13:39 +01:00
Nuno Lopes
4c7fea7e55 fix 'make test' for newer gcc versions 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-19 13:48:14 +01:00
Nikolaj Bjorner
4d3d9f7602 include compression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-11 20:32:39 -07:00
Nikolaj Bjorner
c96c4c7af7 Merge branch 'opt' of https://github.com/Z3Prover/z3 into opt 2015-05-11 17:12:04 -07:00
Nikolaj Bjorner
bf6ab3fc03 local state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-11 17:11:52 -07:00
Nikolaj Bjorner
e53462c1c1 update ddnf experiment code 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-11 17:11:21 -07:00
Nikolaj Bjorner
1a4e8f89bd fix release build failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-10 14:53:05 -07:00
Nikolaj Bjorner
839e3fbb7c add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-09 19:40:34 -07:00
Nikolaj Bjorner
9377779e58 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-30 10:40:03 -07:00
Nikolaj Bjorner
620c11932b type check distinct operator. fixes #62 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-27 11:10:37 -07:00
Nuno Lopes
f7d9438e7b add failing test for issue #62 (mk_distinct doesnt type check) 
Signed-off-by: Nuno Lopes <nlopes@MSRC-3617536.europe.corp.microsoft.com>
 2015-04-27 17:44:38 +01:00
Nikolaj Bjorner
9978cba5a8 Codeplex issue 191: inconsistent results from PDR engine. The report exposed bugs in the implementation of the priority queue leaving unexplored leaves durin search. The priority queue has now been revised to address the exposed bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 16:27:15 -07:00
Nuno Lopes
a211fcfb9e muZ/datalog/udoc: fix bug in join_project 
The bug was that we could project out don't care columns and don't take copied bits into account.
Bug reported by Ari Fogel

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-12-28 17:05:17 +00:00
Nuno Lopes
60aad7a662 DoC: verify the result of a bunch of unit tests with SMT 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-09 09:44:27 +01:00
Nikolaj Bjorner
d038c7bf89 fixing udoc/adding tuned join_project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 22:07:19 -07:00
Nikolaj Bjorner
2362e01a9f add unit test for join-project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 17:17:14 -07:00
Nuno Lopes
de73a4d893 DoC: fix bug in filter_project with '(not (= c1 c2))' style constraints 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-08 11:12:41 +01:00
Nuno Lopes
985ad30349 DoC: reuse code in unit tests from relation checker 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-08 10:06:39 +01:00
Nikolaj Bjorner
7ef311acd3 updated check_relation test for join-project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-06 13:05:53 -07:00
Nuno Lopes
893d51eae8 DoC: implement slow path of filter_negated using join+project. 
disable fast path since it's broken

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-06 18:10:03 +01:00
Nikolaj Bjorner
f3d2535b46 another unit test for Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-03 16:58:46 -07:00
Nikolaj Bjorner
93a757f45b add two failing test cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 10:38:43 -07:00
Nuno Lopes
9828b26379 DoC: fix slow path of filter_by_negation when columns are repeated in tgt relation 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-02 09:56:06 +01:00
Nikolaj Bjorner
bb15ddbf15 update unit tests to use filter_by_negation verifier from check_relation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-01 15:21:42 -07:00
Nuno Lopes
04b5d436b3 DoC: fix fast path of filter_negated 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-01 18:03:59 +01:00
Nuno Lopes
cbe23c428f fix build of unit tests 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-01 16:08:44 +01:00
Nikolaj Bjorner
e6725b2344 merge unstable into opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 12:12:24 -07:00
Nikolaj Bjorner
74053275cf consolidate rule checking in separate class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-25 19:05:49 -07:00
Nikolaj Bjorner
16f80fce92 add check_relation for integrity checking of relational operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-24 01:06:58 -07:00
Nikolaj Bjorner
1111c0494f adding validation code to doc/udoc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-23 17:10:00 -07:00
Nikolaj Bjorner
54506408f9 fix overflow bugs in doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-22 22:03:59 -07:00
Nikolaj Bjorner
83e7107485 fix bugs in doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-22 17:45:01 -07:00
Nikolaj Bjorner
4cf8905a8f fixing join 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-22 11:08:23 -07:00
Nikolaj Bjorner
75b11d2b75 fix bugs in doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-22 03:22:26 -07:00
Nikolaj Bjorner
22808a039d working on udoc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-21 20:25:11 -07:00
Nikolaj Bjorner
a50cbef877 testing doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-20 19:01:15 -07:00
Nikolaj Bjorner
2552c1530b doc unit tests pass 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-20 10:19:54 -07:00
Nikolaj Bjorner
f94bdf4035 updated unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-20 01:05:43 -07:00