Nikolaj Bjorner
e9a085a0e2
enable LRA
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 08:23:43 -07:00
Nikolaj Bjorner
b9a695633d
fix build issues part 4
2017-05-11 08:18:20 -07:00
Nikolaj Bjorner
6e021781cd
fix build issues part 3
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 07:49:41 -07:00
Nikolaj Bjorner
fcfaedd9ec
fix build issues part 2
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 07:39:56 -07:00
Nikolaj Bjorner
2a905e02c8
fix build issues part 1
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 07:38:52 -07:00
Nikolaj Bjorner
714dfaded3
Merge pull request #1017 from levnach/123
...
123
2017-05-11 07:31:40 -07:00
Lev Nachmanson
1d5fafd558
disable lev's solver
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-05-10 21:18:20 -07:00
Nikolaj Bjorner
d1cfc53495
fix for #1015
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-10 19:40:00 -07:00
Lev Nachmanson
b08f094620
merging with the lp fork
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-05-10 16:53:25 -07:00
Nikolaj Bjorner
f03f471f02
fix for #1016
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-10 15:13:04 -07:00
Lev Nachmanson
cf695ab876
taking changes from the fork
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-05-10 10:43:01 -07:00
Nikolaj Bjorner
74ac58de2b
enable generic parameters with smt-tactic
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-10 10:18:50 -07:00
Christoph M. Wintersteiger
284436aa5a
Merge branch 'master' of https://github.com/Z3Prover/Z3
2017-05-10 12:47:15 +01:00
Christoph M. Wintersteiger
248dd601ae
Whitespace, newlines
2017-05-10 12:44:25 +01:00
Nikolaj Bjorner
f572c79cdb
add instances
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 19:55:24 -07:00
Nikolaj Bjorner
a64a73255e
make source directory relative to build directory
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 15:46:24 -07:00
Nikolaj Bjorner
f4544eb060
disambiguating arguments to unordered map erase and dealing with unused and uninitialized variables
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 15:35:00 -07:00
Nikolaj Bjorner
d43c12413d
add disambiguation, avoid uninitialzed variable passing in debug mode
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 15:27:42 -07:00
Nikolaj Bjorner
445a2280d3
missing file
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 15:18:15 -07:00
Nikolaj Bjorner
f12f83af83
fix warnings, avoid class qualification in static function
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:56:38 -07:00
Nikolaj Bjorner
7731163d11
use forward slash on src include
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:42:43 -07:00
Nikolaj Bjorner
561522f882
missing file
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:20:13 -07:00
Nikolaj Bjorner
c5f1f8ba59
missing files
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:14:58 -07:00
Nikolaj Bjorner
905cf08e5d
missing files
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:11:33 -07:00
Nikolaj Bjorner
e0ac5bd585
Merge pull request #1013 from NikolajBjorner/master
...
Integrate new LRA solver capabilities by Lev Nachmanson.
The LRA solver relies on a portfolio of Simplex implementations.
For large problems it resorts to revised Simplex with different search options. It uses doubles for large systems. For smaller problems it uses a Dual Simplex tableau representation that outperforms the scalable solver when many small calls are used. It uses infinite precision rationals by default.
The theory_lra class provides the interface to the scalable Simplex solver.
2017-05-09 14:07:33 -07:00
Nikolaj Bjorner
2a63c56ae0
A faster and more scalable LRA solver by Lev Nachmanson. It is disabled in the initial merge pending a few bug fixes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:03:30 -07:00
Nikolaj Bjorner
911b24784a
merge LRA
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 10:46:11 -07:00
Nikolaj Bjorner
085d31dca2
mpq/mpz features from LRA
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 09:18:59 -07:00
Nikolaj Bjorner
60725f5384
use vector fixes from LRA branch
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 09:13:27 -07:00
Nikolaj Bjorner
42ea2d1ea5
LRA changes to rational
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 09:06:41 -07:00
Nikolaj Bjorner
d8c3b273d3
adding benign initialization
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-08 10:50:06 -07:00
Nikolaj Bjorner
579b914d78
add configuration per Dan Liew's comment
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-08 10:02:09 -07:00
Nikolaj Bjorner
51e6d8a28d
Merge branch 'master' of https://github.com/Z3Prover/z3
2017-05-08 09:55:03 -07:00
Nikolaj Bjorner
99474eb44a
integrate Dan Liew's patch for language selection
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-08 09:46:40 -07:00
Nikolaj Bjorner
921d0309a4
Merge pull request #1010 from mtrberzi/warning-nits
...
Fix warnings in theory_str.cpp
2017-05-07 15:37:33 -07:00
Murphy Berzish
6b2a800c7f
fix warnings: unused variables, string constants
2017-05-07 18:23:47 -04:00
Nikolaj Bjorner
3ae722025f
relaxing condition for assumptions, add theory-assumption to skolem functions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-07 14:54:47 -07:00
Nikolaj Bjorner
e02392c0e3
use skolem function to avoid exposing temporary variables in models
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-07 14:03:24 -07:00
Nikolaj Bjorner
82bdd26817
clean up some warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-06 13:40:53 -04:00
Nikolaj Bjorner
de69c42e4d
Merge pull request #1007 from mtrberzi/formatting
...
Code formatting for theory_str
2017-05-05 19:42:32 -04:00
Murphy Berzish
f904b033ad
formatting theory_str.h
2017-05-05 19:29:53 -04:00
Murphy Berzish
21c8f4aae0
formatting theory_str.cpp
2017-05-05 19:26:15 -04:00
Nikolaj Bjorner
8eb26e25c2
add new files to cmakelist.txt files
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-05 17:03:03 -04:00
Nikolaj Bjorner
a9fbad53a0
Merge pull request #907 from mtrberzi/release-1.0
...
theory_str for Z3 based on the Z3str2 framework
2017-05-05 16:55:43 -04:00
Murphy Berzish
7ddd43e16d
first-class re.range support in theory_str
2017-05-05 15:29:58 -04:00
Murphy Berzish
75ba4d5a4d
remove unneeded include
2017-05-05 14:54:36 -04:00
Murphy Berzish
8029b6b889
Merge branch 'upstream-master' into develop
2017-05-05 14:44:29 -04:00
Nikolaj Bjorner
7cb0237ab2
Merge branch 'master' of https://github.com/Z3Prover/z3
2017-05-05 10:59:58 -04:00
Nikolaj Bjorner
7e1fae418a
fix #1005 , disable expansion of regular expression range to union as it degrades performance significantly
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-05 10:59:47 -04:00
Christoph M. Wintersteiger
79dcf03a42
Enabled C++11 in GCC and Clang
2017-05-05 15:01:10 +01:00