C++ API for Datalog engine missing declare_vars #1832
Comments
|
add_var is a function implemented on the python side for convenience. From C++ you would have to create rules as quantified formulas, binding all relevant variables. Use the function expr forall(expr_vector const & xs, expr const & b) to bind the variables that are used in each rule. |
|
Thanks a lot! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hello,
I tried to use the C++ API for Z3's datalog engine following the Python examples at http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/fixedpoints-examples.htm. I couldn't find a declare_vars method of the fixedpoint class. I believe that absence of this method creates the following issue: When I create a number of rules and facts and pose a query, my program crashes due to an exception. The error I get says:
failed: Uninterpreted 'b' in directCall:
calls(#0,#1) :-
cgedge(#2,#3),
(= (:var 3) b),
(= (:var 2) a),
(= (:var 1) b),
(= (:var 0) a).
I would appreciate any feedback. Thanks.
Tuba
The text was updated successfully, but these errors were encountered: