mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity
17817 commits 24 branches 48 tags 158 MiB
Commit graph

1982 commits

Author SHA1 Message Date
Jakob Rath
613b0db4cc fix refcount issue 2022-03-19 04:19:16 +01:00
Jakob Rath
d41d3fa6ea fix some bugs 2022-03-18 16:05:51 +01:00
Jakob Rath
fd353bff17 unsat core 2022-03-18 15:49:44 +01:00
Jakob Rath
509a007ed7 Integrate univariate solver in polysat 2022-03-18 15:43:06 +01:00
Jakob Rath
9d47d7959d helper functions to add constraints to univariate_solver 2022-03-17 14:08:00 +01:00
Jakob Rath
edeba9b56a support op_constraint in univariate solver 2022-03-17 14:03:42 +01:00
Jan Vraný
bdf7de1703
Care for root index being undefine while calling Z3_algebraic_get_i() (#5888) 
In some cases, Z3_algebraic_get_i() returned 0. For example, in the following
Python snippet, the last assert would fail:

    import z3
    x = z3.Real('x')
    s = z3.Solver()
    s.add( (x * x) - 2 == 0, x <= 0)
    s.check()
    val_x = s.model().get_interp(x)
    assert val_x.index() == 1

The problem was that `algebraic_numbers::manager:👿:get_i()` did not
check whether the root index was properly initialized.

This commit fixes this issue by checking whether root index is initialized
the same way various other routines do.

Fixes issue #5807.

Signed-off-by: Jan Vrany <jan.vrany@labware.com>
 2022-03-16 19:28:03 -07:00
Jakob Rath
c4370eb7e6 univariate solver seems to work 2022-03-11 18:06:32 +01:00
Jakob Rath
1de51da67e get univariate coefficients 2022-03-11 18:03:39 +01:00
Jakob Rath
74281fa830 compile 2022-03-11 08:33:10 +01:00
Jakob Rath
8b1f1d0e11 begin univariate solver impl 2022-03-10 17:58:37 +01:00
Jakob Rath
78028bedae use solver_factory 2022-03-10 16:57:08 +01:00
Jakob Rath
4a86c3fb67 looks like QF_BV is handled by inc_sat_solver 2022-03-10 16:19:35 +01:00
Jakob Rath
c648b57493 forbidden intervals only used by viable 2022-03-10 16:12:13 +01:00
Jakob Rath
afc711d6ec move into separate component 2022-03-10 16:10:56 +01:00
Jakob Rath
d4a28d4553 implementation stub 2022-03-10 11:13:06 +01:00
Jakob Rath
6aee62ef2f Univariate solver interface 2022-03-10 11:01:57 +01:00
Jakob Rath
9b20f17f9c compile 2022-03-10 10:57:49 +01:00
Jakob Rath
22411f8b43 one more special case 2022-03-10 10:32:23 +01:00
Nikolaj Bjorner
1faccffd0d add smul over and underflow predicate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-20 11:39:45 +02:00
Nikolaj Bjorner
dc3b921712 eq explain 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 19:00:24 +02:00
Nikolaj Bjorner
8c9835bca6 smul no overflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 18:55:07 +02:00
Nikolaj Bjorner
89d6f1c191 update mk_project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-02 18:04:52 -08:00
Nikolaj Bjorner
4c4f916917 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-02 08:24:58 -08:00
Nikolaj Bjorner
32edbfa28e two bugs: check for always false, adjust start of list was incorrect during re-insert 2022-02-02 07:37:35 -08:00
Nikolaj Bjorner
18291543d6 fixing corner cases for viable intervals 2022-02-01 13:21:51 -08:00
Nikolaj Bjorner
c48f14e537 updated conflict state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-01 11:47:33 -08:00
Nikolaj Bjorner
486cc632d0 notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-31 09:16:48 -08:00
Jakob Rath
5ee02ec5df Merge remote-tracking branch 'origin/polysat' into polysat 2022-01-31 15:36:22 +01:00
Jakob Rath
15854301b2 Generalize refine_disequal_lin 2022-01-31 15:35:25 +01:00
Jakob Rath
f80eb6237d includes shouldn't depend on debug/release mode 2022-01-31 15:29:25 +01:00
Nikolaj Bjorner
697b561c7a update comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-30 17:34:00 -08:00
Nikolaj Bjorner
b488a1fadd WIP revamp conflict state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-29 16:17:58 -08:00
Nikolaj Bjorner
60248d0981 resolution is still wrong 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-29 09:32:14 -08:00
Jakob Rath
67647433ba log justifications during conflict resolution 2022-01-28 15:52:52 +01:00
Nikolaj Bjorner
0eb0306ae2 update comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 17:47:27 -08:00
Nikolaj Bjorner
93541ccdf2 enable try-push-block 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 17:42:33 -08:00
Nikolaj Bjorner
0677eb1c05 fixing up missing dependencies during resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 16:58:16 -08:00
Nikolaj Bjorner
1264fe462d merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 14:33:38 -08:00
Nikolaj Bjorner
ff4b471f93 resurrect Booelan decisions to deal with quot-rem and similar axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 14:26:41 -08:00
Jakob Rath
4236830a8e Also check clauses when returning SAT 2022-01-27 12:23:57 +01:00
Nikolaj Bjorner
be790b8892 add back minimize vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 18:01:26 -08:00
Nikolaj Bjorner
6df23fbce3 add note about a bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 16:58:00 -08:00
Nikolaj Bjorner
0eaf5a8510 factor cache pointers are invalid if the table is resized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 16:18:18 -08:00
Nikolaj Bjorner
d1fcc41c7f merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 21:53:10 +01:00
Nikolaj Bjorner
ff93c03972 integrate polysat into bv solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 20:20:45 +01:00
Jakob Rath
d7548f6867 Now we can have a working binary add_eq/add_diseq 2022-01-26 11:50:49 +01:00
Jakob Rath
645f190e35 Add wrapper for external dependencies to prevent accidental conversions 2022-01-26 11:44:01 +01:00
Jakob Rath
cbed3bfde4 fi: match_non_zero_linear 2022-01-26 11:09:37 +01:00
Nikolaj Bjorner
3f5df04dc4 prepare polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 06:19:24 +01:00