Nikolaj Bjorner
a38bf3e22f
port to inherit from std::exception
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-04 13:25:14 -08:00
Nikolaj Bjorner
29a2838bc9
#5338 #5349
2021-06-16 16:01:42 -05:00
Nikolaj Bjorner
f95d0b7216
#5349 #5338
2021-06-16 16:01:42 -05:00
Nikolaj Bjorner
3ae4c6e9de
refactor get_sort
2021-02-02 04:45:54 -08:00
Nuno Lopes
d79692b185
remove unused file & hide a few symbols
2020-01-31 17:13:28 +00:00
Nikolaj Bjorner
d4f2215024
revert restriction to nira test, move to tuned version of grobner
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-27 16:38:35 -08:00
Nikolaj Bjorner
dd07d21f6c
fix #2821
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-27 12:16:28 -08:00
Nikolaj Bjorner
feff1f7f96
fix #2609
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-10-02 14:40:11 -07:00
Nikolaj Bjorner
c744b19bce
resort to only supporting ground non-linear division for nra_tactic/nra_probe #2372 #2376
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-04 07:08:47 +07:00
Nikolaj Bjorner
49141c7813
remove left-over break assert
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-07-16 08:33:41 +01:00
Nikolaj Bjorner
d00ffdda82
strengthen filter for specialized tactic conditions, add flag to disable hnf to lp_params
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-07-15 22:35:47 -07:00
Bruce Mitchener
b7d1753843
Use override rather than virtual.
2018-02-09 21:19:27 +07:00
Nikolaj Bjorner
43e47271f7
have quantified tactics work with bound Boolean variables. Adding stubs for match
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-09-18 15:58:09 -07:00
Nikolaj Bjorner
b19f94ae5b
make include paths uniformly use path relative to src. #534
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
baee4225a7
reworking cancellation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 16:21:24 -08:00
Nikolaj Bjorner
e8811748d3
fix regressions in nl/smt
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-16 19:08:37 +01:00
Nikolaj Bjorner
2e627e78bc
filter tactic on proofs and cores
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-10 14:55:28 -07:00
Nikolaj Bjorner
f5c048775b
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-10 09:42:11 -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
Christoph M. Wintersteiger
d20c7bc9ee
Added is_qfaufbv_probe and is_qfauflia_probe.
...
Potential performance disruption for some users:
Changed default_tactic to call the respective tactics,
where previously they would have run the default 'smt'
tactic.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 18:19:43 +00:00
Leonardo de Moura
97bf9418f7
Add new probes for arithmetic. Check for LIA and LRA (and activate qe if applicable). Modify echo tactic to send results to the regular stream.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-02-20 13:41:08 -08:00
Leonardo de Moura
0990a2e045
using a consistent naming convention for naming tactic subfolders
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-24 15:11:44 -07:00
