mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
8143 commits 49 branches 53 tags 182 MiB
Commit graph

8143 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
3ce82ea8ce merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-02 10:37:22 -07:00
Nikolaj Bjorner
efd5727676 add shorthand for enumerating constants in a model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-02 10:35:09 -07:00
Nikolaj Bjorner
0ac80fc042 have parser produce ast-vector instead of single ast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 21:21:05 -07:00
Nikolaj Bjorner
e37a6dd809 add tracking for reason unknown 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 17:04:37 -07:00
Nikolaj Bjorner
833a910d57 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-06-01 15:03:55 -07:00
Nikolaj Bjorner
538411c67f remove dependencies on fd_tactic.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 15:03:34 -07:00
Nikolaj Bjorner
55ba1e9178 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-06-01 14:50:37 -07:00
Nikolaj Bjorner
4e65c13726 adding lookahead and lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 14:49:54 -07:00
Nikolaj Bjorner
2908ab4069 fix reference count issue with pinning to expr_ref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:56:25 -07:00
Nikolaj Bjorner
e9ed3af455 fix regression in str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:35:35 -07:00
Nikolaj Bjorner
fda59f5a24 expose operator kinds for internal functions using their sequence variants. Issue #1051 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:32:17 -07:00
Nikolaj Bjorner
1fa60f4893 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-06-01 09:11:09 -07:00
Nikolaj Bjorner
52e0f3b539 add string accessors to managed APIs #1051 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:10:49 -07:00
Christoph M. Wintersteiger
596652ed36 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-31 18:35:52 +01:00
Christoph M. Wintersteiger
4f0a87299c Fixed signed/unsigned comparison warnings 2017-05-31 18:35:06 +01:00
Christoph M. Wintersteiger
a7d5bb7b36 Tabs 2017-05-31 12:18:00 +01:00
Nikolaj Bjorner
7d245be4e1 enable exposing internal solver state on interrupted solvers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-30 17:33:27 -07:00
Nikolaj Bjorner
546d22e77a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-30 11:18:43 -07:00
Nikolaj Bjorner
415824b600 put temporaries on trail 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-30 11:18:33 -07:00
Nikolaj Bjorner
2cfb9eec3d Merge pull request #1050 from pathawks/fix-markdown 
Fix Markdown heading
 2017-05-30 11:03:07 -07:00
Pat Hawks
e6d3b732e9 Remove tab 2017-05-30 12:53:55 -05:00
Nikolaj Bjorner
870017e2ce Merge pull request #1049 from chaserhkj/java-api-update-fix 
`Expr.update()` in java API should not return super class
 2017-05-29 18:14:54 -07:00
KangJing Huang (Chaserhkj)
8092dd5aa3 Fix Expr.update in java API returning superclass 2017-05-29 20:51:42 -04:00
Nikolaj Bjorner
4cbf938cf3 enable get-unsat-assumptions command per request in #1048 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-29 16:26:22 -07:00
Nikolaj Bjorner
2de80b5ce9 add pb built in ops for logic ALL #1045 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-29 10:08:50 -07:00
Nikolaj Bjorner
d95ac58bad remove throw in reason-unknown #1043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 12:09:35 -07:00
Nikolaj Bjorner
f80a622a8f add colon to assertion stack levels #1046 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 11:10:46 -07:00
Nikolaj Bjorner
e0a86ccc1a add lrb/chb and experiment with them 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 10:48:31 -07:00
Nikolaj Bjorner
1654ad7059 adding escape characters to reason-unknown #1043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-27 14:56:38 -07:00
Nikolaj Bjorner
c28f26c17d merge and update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-25 14:17:19 -07:00
Nikolaj Bjorner
e306287d7b updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-25 14:04:48 -07:00
Nikolaj Bjorner
d2b2aedef3 Merge branch 'dev' of https://github.com/nikolajbjorner/z3 2017-05-25 08:54:00 -07:00
Nikolaj Bjorner
1086eaaa1f debugging nra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-24 21:46:19 -07:00
Lev Nachmanson
73e919c002 test 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-05-24 17:31:17 -07:00
Nikolaj Bjorner
b18dc7d052 adding nra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-24 17:24:36 -07:00
Nikolaj Bjorner
4726d32e2f Dev (#51) 
* initial skeletons for nra solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* initial skeletons for nra solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* adding more nlsat

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* nlsat integration

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* adding constraints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* adding nra solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add missing initialization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* adding nra solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-24 16:32:14 -07:00
Nikolaj Bjorner
7a809fe4f0 adding nra solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-24 14:56:59 -07:00
Nikolaj Bjorner
80bb084611 add missing initialization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-24 14:47:09 -07:00
Nikolaj Bjorner
d45c56da3f adding nra solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-24 14:44:16 -07:00
Nikolaj Bjorner
fc53c5b638 adding nra solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-24 14:41:02 -07:00
Lev Nachmanson
09530bb6bc adding some content to the new check_int_feasibility() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-05-24 10:12:42 -07:00
Nikolaj Bjorner
dcc6284557 adding constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-24 08:57:10 -07:00
Nikolaj Bjorner
b9ca8b435f nlsat integration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 20:45:58 -07:00
Nikolaj Bjorner
f3a0b7e0cd change command-line experience for pareto fronts. It now requires multiple check-sat calls to loop over the fronts. This allows querying each model in turn. #1008 2017-05-23 20:05:10 -07:00
Nikolaj Bjorner
e231f4bc87 adding more nlsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 18:50:18 -07:00
Lev Nachmanson
93a3c486b0 small fix in lar_solver.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-05-23 18:32:08 -07:00
Nikolaj Bjorner
8ecd8a2a52 Dev (#50) 
* initial skeletons for nra solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* initial skeletons for nra solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 18:07:58 -07:00
Nikolaj Bjorner
db54cab8b2 initial skeletons for nra solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 16:26:46 -07:00
Nikolaj Bjorner
f1ca1de408 initial skeletons for nra solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 16:12:46 -07:00
Lev Nachmanson
1f425824ff adding stub check_int_feasibility() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-05-23 15:46:53 -07:00