mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 05:48:44 +00:00
commit
20f85111f9
|
@ -300,7 +300,7 @@ namespace datalog {
|
||||||
/**
|
/**
|
||||||
Register datalog relation.
|
Register datalog relation.
|
||||||
|
|
||||||
If names is true, we associate the predicate with its name, so that it can be
|
If named is true, we associate the predicate with its name, so that it can be
|
||||||
retrieved by the try_get_predicate_decl() function. Auxiliary predicates introduced
|
retrieved by the try_get_predicate_decl() function. Auxiliary predicates introduced
|
||||||
e.g. by rule transformations do not need to be named.
|
e.g. by rule transformations do not need to be named.
|
||||||
*/
|
*/
|
||||||
|
|
|
@ -88,7 +88,7 @@ namespace datalog {
|
||||||
typedef typename Traits::signature signature; //this must be a vector-like type
|
typedef typename Traits::signature signature; //this must be a vector-like type
|
||||||
|
|
||||||
/**
|
/**
|
||||||
The client submits an initial class to be used as a base for signature. Then we excend it by
|
The client submits an initial class to be used as a base for signature. Then we extend it by
|
||||||
the common signature methods into a signature_base class which then the client inherits from
|
the common signature methods into a signature_base class which then the client inherits from
|
||||||
to obtain the actual signature class.
|
to obtain the actual signature class.
|
||||||
*/
|
*/
|
||||||
|
@ -470,7 +470,7 @@ namespace datalog {
|
||||||
\brief fast emptiness check. This may be partial.
|
\brief fast emptiness check. This may be partial.
|
||||||
The requirement is that if fast_empty returns true
|
The requirement is that if fast_empty returns true
|
||||||
then the table or relation is in fact empty.
|
then the table or relation is in fact empty.
|
||||||
It is allowed to return false even if the relation is non-empty.
|
It is allowed to return false even if the relation is empty.
|
||||||
*/
|
*/
|
||||||
virtual bool fast_empty() const { return empty(); }
|
virtual bool fast_empty() const { return empty(); }
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue