Nikolaj Bjorner
|
96e157e201
|
fix warnings for unused variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-17 13:54:22 -07:00 |
|
Nikolaj Bjorner
|
6f5785338a
|
add line/pos information for pattern warnings. Issue #607
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-16 08:59:58 -07:00 |
|
Nikolaj Bjorner
|
e29adbf304
|
fix issues #581: nested timeouts canceled each-other
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-04-30 11:18:34 -07:00 |
|
Nikolaj Bjorner
|
d383fd851a
|
move vector<std::string to std::vector<std::string
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-04-16 09:34:27 -07:00 |
|
Nikolaj Bjorner
|
a021e51a9c
|
make parse error a bit more informative
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-01-19 19:09:41 +01:00 |
|
Nikolaj Bjorner
|
9909c056f0
|
add range / loop handling for re. Fix regression reading mixed numerals reported by Trentin
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-01-13 00:49:31 -08:00 |
|
Nikolaj Bjorner
|
131f9e2247
|
change queries to take function names instead of arbitrary predicates. This allows to bypass issues with having arbitrary query expressions compiled in arbitrary ways to auxiliary predicates where names of bound variables are reshuffled. See also Stackoverflow http://stackoverflow.com/questions/34693719/bug-in-z3-datalog
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-01-10 20:43:41 -08:00 |
|
Nikolaj Bjorner
|
3c50508762
|
use ADT for strings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-12 20:46:28 -08:00 |
|
Nikolaj Bjorner
|
75359c580e
|
add basic rewriting to strings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-05 12:02:33 -08:00 |
|
Nikolaj Bjorner
|
a8e366aa24
|
add basic string factory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-04 15:24:29 -08:00 |
|
Nikolaj Bjorner
|
75c935a4cb
|
add tokens to parse strings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-04 12:09:15 -08:00 |
|
Nikolaj Bjorner
|
e2565d8d82
|
add some of the SMT2.5 features
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-02 18:41:10 -08:00 |
|
Nikolaj Bjorner
|
ac3edbbaaa
|
add line/position information to unsupported command reports per zeph pull request
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-10-30 19:23:31 -07:00 |
|
Christoph M. Wintersteiger
|
2e071e89b0
|
tabs
|
2015-09-17 13:16:35 +01:00 |
|
Nikolaj Bjorner
|
655b44c07b
|
make :weight understand both decimal and integral values, remove dweight, remove deprecated commands for optimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-08-15 00:48:22 +02:00 |
|
Nikolaj Bjorner
|
3e0e9c7f3c
|
parse also bit-vector constants with set-info. Reported by David Cok
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-03-19 20:30:58 -07:00 |
|
Nikolaj Bjorner
|
a00a9fbdfd
|
generate error on duplicated data-type accessors. Issue 85
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-03-02 17:10:48 -08:00 |
|
Nikolaj Bjorner
|
83add2bd9b
|
fix bugs reported by Filip Konecny <filip.konecny@epfl.ch> in PDR
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-04-25 13:39:11 -07:00 |
|
Leonardo de Moura
|
607fab486c
|
Fix incorrect uses of set_cancel()
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-17 18:48:10 -08:00 |
|
Leonardo de Moura
|
9b7946e52d
|
added method for creating ast_manager based on context_params configuration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-09 14:24:37 -08:00 |
|
Leonardo de Moura
|
9754ccf8a1
|
fixing problems with the new parameter framework
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-04 11:16:42 -08:00 |
|
Leonardo de Moura
|
589f096e6e
|
working on new parameter framework
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-01 15:54:34 -08:00 |
|
Leonardo de Moura
|
4c98b567e1
|
old_params ==> front_end_params. Isolated abstract solver interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 11:28:14 -07:00 |
|
Leonardo de Moura
|
cb8a6db51b
|
minor fixes after feedback from regression tests...
|
2012-10-30 09:20:28 -07:00 |
|
Leonardo de Moura
|
ad9bad9cc1
|
created parsers folder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-26 18:25:15 -07:00 |
|