mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-24 03:57:51 +00:00
Code Activity

improve error handling of parameters and remove work notes from udoc_relation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-08 11:05:38 -07:00
parent 06c7f3f246
commit 00555def4d
3 changed files with 16 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/muz/rel/udoc_relation.cpp
View file

@ -20,40 +20,6 @@ Revision History:
Notes:
Current pending items:
- Profile and fix bottlnecks:
- Potential bottleneck in projection exercised in some benchmarks.
Projection is asymptotically very expensive. We are here interested in
handling common/cheap cases efficiently.
- Simplification of udoc and utbv (from negated tails) after operations such as join and union.
- The current simplification is between cheap and expensive. Some low-cost simplification
based on sorting + coallescing and detecting empty docs could be used.
- There are several places where code copies a sequence of bits from one vector to another.
Any such places in udoc_relation should be shifted down to 'doc_manager'. Loops in 'doc_manager'
should be shifted down to 'tbv_manager' and loops there should be moved to 'fixed_bitvector_manager'.
Finally, more efficient and general implementations of non-aligned copies are useful where such
bottlnecks show up on the radar.
- Fix filter_by_negated.
Current implementation seems incorrect. The fast path seems right, but the slow path does not.
Recall the semantics:
filter_by_negation(tgt, neg, columns in tgt: c1,...,cN,
corresponding columns in neg: d1,...,dN):
tgt := {x: x\in tgt_0 && ! \exists y: ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) }
We are given tgt, and neg as two udocs.
The fast pass removes doc's t from tgt where we can establish
that for every x in t there is a n in neg and a y in n,
such that projections(x) = projections(y).
This is claimed to be the case if projections(n) contains projections(t).
The slow pass uses the projection to create a doc n' from each n that has the same signature as tgt.
It then subtracts each n'. The way n' is created is by copying bits from n.
This seems wrong, for example if the projection contains overlapping regions.
Here is a possible corrected version:
define join_project(tgt, neg, c1, .., cN, d1, .. , dN) as
exists y : y \in neg & x in tgt & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) )
return tgt \ join_project(tgt, neg, c1, .., cN, d1, .. , dN)
We have most of the facilities required for a join project operation.
For example, the filter_project function uses both equalities and deleted columns.
--*/
#include "udoc_relation.h"
#include "dl_relation_manager.h"