search

ravel-net / pyotr

Apache License 2.0
0 stars 0 forks source link

Domain of c-variables not added when treating rule as a program #3

Closed mudbri closed 2 years ago

mudbri commented 2 years ago

Currently, we convert the conditions in a rule to SQL where clauses. However, we do not take into account the domain of c-variables, which should also be converted to SQL where clauses for correctness.

Moreover, when we treat variables as constants (when instantiating body), should we make sure that the instantiated constants are different from the domain of c-variables and all other constants? Specifically, it's unclear what instantiating to "Distinct Constants" mean.

mudbri commented 2 years ago

@lanfangping, is the domain of c-variables automatically considered when doing any kind of reasoning with the object z3SMTTools?

lanfangping commented 2 years ago

@lanfangping, is the domain of c-variables automatically considered when doing any kind of reasoning with the object z3SMTTools?

Yes. It sets domains of c-variables when instantiating an object of z3SMTTools. See line 68-70. Then we use push/pop to update constraints which to be reasoned in Z3 Solver.