Convert Prolog Rationals (#11)

Support rationals and large integers. Can use `mk_rational`, or use Prolog rationals (e.g. `3r4`) that are expanded in the C code calling Prolog from C.

Renaming some functions for clarity.

README.md

@@ -50,7 +50,6 @@ swipl
 ?- use_module(z3).
 Installing Z3 package
 Using Z3 version Z3 4.12.5.0
-Initializing global context
 true.
 ```
 

make.sh

@@ -4,7 +4,9 @@
 
 # Change the -I path to point to your Z3 install and build:
 
-swipl-ld -O1 -I/Users/uribe/git/z3/src/api/ -L. -o z3_swi_foreign -shared z3_swi_foreign.c -lz3
+swipl-ld -O3 -Wall -I/Users/uribe/git/z3/src/api/ -L. -o z3_swi_foreign -shared z3_swi_foreign.c -lz3
+
+# test including gmp; needs a link or copy of libgmp.dylib:
+# swipl-ld -O1 -I/Users/uribe/git/z3/src/api/ -I/opt/homebrew/Cellar/gmp/6.3.0/include/ -L. -o z3_swi_foreign -shared z3_swi_foreign.c -lz3 -lgmp
 
-# swipl-ld -O3 -Wall -I/Users/uribe/git/z3/src/api/ -L. -o z3_swi_foreign -shared z3_swi_foreign.c -lz3
 

quickexplain.pl

@@ -1,18 +1,19 @@
 %%% -*- Mode: Prolog; Module: quickexplain; -*-
 
 :- module(quickexplain, [
+              % These assume that Base+Constraints is unsatisfiable:
               qexplain/4, % +AssertPredicate, +Base, +Constraints, -Result
               qexplain/3, % +AssertPredicate, +Constraints, -Result   (empty Base)
 
               qrelax/4,   % +AssertPredicate, +Base, +Constraints, -Result
               qrelax/3,   % +AssertPredicate, +Constraints, -Result   (empty Base)
 
-              % use these if you want a consistency check at the start:
-              top_explain/4,   % +AssertPredicate, +Base, +Constraints, -Result
-              top_explain/3,   % +AssertPredicate, +Constraints, -Result   (empty Base)
+              % Use these if you want a consistency check at the start:
+              check_explain/4,   % +AssertPredicate, +Base, +Constraints, -Result
+              check_explain/3,   % +AssertPredicate, +Constraints, -Result   (empty Base)
 
-              top_relax/4,   % +AssertPredicate, +Base, +Constraints, -Result
-              top_relax/3    % +AssertPredicate, +Constraints, -Result   (empty Base)
+              check_relax/4,   % +AssertPredicate, +Base, +Constraints, -Result
+              check_relax/3    % +AssertPredicate, +Constraints, -Result   (empty Base)
 
           ]).
 
@@ -30,10 +31,10 @@
 :- meta_predicate qrelax(1, ?, ?).
 :- meta_predicate qrelax(1, ?, ?, ?).
 
-:- meta_predicate top_explain(1, ?, ?).
-:- meta_predicate top_explain(1, ?, ?, ?).
-:- meta_predicate top_relax(1, ?, ?).
-:- meta_predicate top_relax(1, ?, ?, ?).
+:- meta_predicate check_explain(1, ?, ?).
+:- meta_predicate check_explain(1, ?, ?, ?).
+:- meta_predicate check_relax(1, ?, ?).
+:- meta_predicate check_relax(1, ?, ?, ?).
 
 :- use_module(utils).
 
@@ -44,7 +45,7 @@
 
 %% Both explain and relax assume that Base + Constraints are, together, inconsistent;
 %% if they are not, Output = Constraints, which is fine for relax but confusing for explain.
-%% use the "top_" procedures to check consistency first.
+%% use the "check_" procedures to check consistency first.
 
 qexplain(_Assert, _Base, [], Output) :- !, Output = [].
 qexplain(Assert, Base, Constraints, Output) :-
@@ -65,9 +66,9 @@
         )
      )).
 
-top_explain(Assert, Base, Constraints, Output) :-
+check_explain(Assert, Base, Constraints, Output) :-
     consistent(Assert, Base, Constraints) -> Output = "consistent"; qexplain(Assert, Base, Constraints, Output).
-top_explain(Assert, Constraints, Output) :- top_explain(Assert, [], Constraints, Output).
+check_explain(Assert, Constraints, Output) :- check_explain(Assert, [], Constraints, Output).
 
 qrelax(_Assert, _B, [], Result) :- !, Result = [].
 qrelax(Assert, B, Constraints, Result) :-
@@ -87,9 +88,9 @@
         append(Delta1, Delta2, Result)
      )))).
 
-top_relax(Assert, Base, Constraints, Output) :-
+check_relax(Assert, Base, Constraints, Output) :-
     consistent(Assert, Base, Constraints) -> Output = "consistent"; qrelax(Assert, Base, Constraints, Output).
-top_relax(Assert, Constraints, Output) :- top_relax(Assert, [], Constraints, Output).
+check_relax(Assert, Constraints, Output) :- check_relax(Assert, [], Constraints, Output).
 
 
 inconsistent(Assert, L) :- \+ checksat(Assert, L).
@@ -150,18 +151,18 @@
     qexplain(call, [(X + Y) #>= 10], [X#<5, Y#<5, X#>2, X#>4], R),
     R =@= [X#<5, Y#<5].
 
-test(topexplain1) :-
-    top_explain(call, [(X + Y) #>= 10], [X#<5, Y#<5, X#>2, X#>4], R),
+test(check_explain1) :-
+    check_explain(call, [(X + Y) #>= 10], [X#<5, Y#<5, X#>2, X#>4], R),
     R =@= [X#<5, Y#<5].
 
-test(topexplain2, [true(R == "consistent")]) :-
-    top_explain(call, [Y #> 0], [X#<5, Y#<5, X#>2], R).
+test(check_explain2, [true(R == "consistent")]) :-
+    check_explain(call, [Y #> 0], [X#<5, Y#<5, X#>2], R).
 
-test(toprelax, true(R == [(X #> 2), (X#>4), (Y#<5)])) :-
-    top_relax(call, [(X + Y) #>= 10], [X#<5, Y#<5, X#>2, X#>4], R).
+test(check_relax, true(R == [(X #> 2), (X#>4), (Y#<5)])) :-
+    check_relax(call, [(X + Y) #>= 10], [X#<5, Y#<5, X#>2, X#>4], R).
 
-test(toprelax2, [true(R == "consistent")]) :-
-    top_relax(call, [Y #> 0], [X#<5, Y#<5, X#>2], R).
+test(check_relax2, [true(R == "consistent")]) :-
+    check_relax(call, [Y #> 0], [X#<5, Y#<5, X#>2], R).
 
 
 :- end_tests(quickexplain_tests).

stateful_repl.pl

@@ -10,8 +10,8 @@
               scopes/1,
               decl/1,
               implies/1,
-              is_implied/1,
-              is_consistent/1,
+              implied/1,
+              consistent/1,
 
               save_state/1,
               read_state/1,
@@ -36,19 +36,21 @@
                   z3_assert/2,
                   z3_declarations/2,
                   z3_free_handle/1,
-                  z3_model_map/2,
+                  z3_model_lists/2,
                   z3_new_handle/1,
                   z3_remove_declaration/3,
                   z3_check/2,
                   z3_solver_pop/3,
                   z3_solver_push/2,
-                  z3_solver_scopes/2
+                  z3_solver_scopes/2,
+                  z3_model_assocs/2
               ]).
 
 :- use_module(z3_utils, [
                   z3_declare_types_for_symbols/3,
                   ground_version/3,
-                  remove_type_annotations/2
+                  remove_type_annotations/2,
+                  z3_expand_term/2
               ]).
 
 :- use_module(type_inference, [
@@ -59,9 +61,15 @@
 
 % TODO: allow adding inconsistencies, add explain/relax?
 
-z3_help :- writeln("Z3 repl help\n"),
-           writeln("add(F)\t\tAdd formula F"),
-           writeln("reset\t\tReset all declarations"),
+z3_help :- format(
+          "Z3 repl help:
+           add(F)              Add formula F
+           consistent(F)       Check if F is consistent with what has been added so far
+           implies(F)          Check if F is implied by what has been added so far
+           formulas(L)         Get list of formulas asserted so far
+           status(S)           Get solver status (l_sat, l_unsat, l_undef)
+           model(M)            Get a model for formulas added so far, if possible
+           reset               Reset all declarations"),
            true.
 
 % z3.pl shares no state between queries, except for enum declarations.
@@ -90,23 +98,24 @@
 % we should call reset_globals if there is a chance for the context to be invalidated
 % before we do a reset. Otherwise, we'll have an old invalid pointer as the solver.
 
-clear_handle :- nb_current(repl_handle, H), !,
+clear_globals :- nb_current(repl_handle, H), !,
                 z3_free_handle(H),
-                nb_delete(repl_handle).
-clear_handle :- true.
+                nb_delete(repl_handle),
+                set_type_map(t),
+                set_recorded_formulas([]).
+clear_globals :- true.
 
 
-reset_globals :- clear_handle,
+reset_globals :- clear_globals,
                  z3_new_handle(H),
                  nb_setval(repl_handle, H),
-                 set_type_map(t),
-                 set_recorded_formulas([]),
                  true.
 
 push_formula(Formula, NewMap, NewSymbols, Status) :-
     %% must_be(ground, Formula),
     get_type_map(OldAssoc),
-    ground_version(Formula, FG, Symbols),
+    z3_expand_term(Formula, FormulaTransformed),
+    ground_version(FormulaTransformed, FG, Symbols),
     (typecheck(FG, bool, OldAssoc, NewMap) -> true ;
      print_message(error, z3_message("Type error for %w", [FG])),
      fail
@@ -171,26 +180,31 @@
 %! model(-Model)
 %  Get a Z3 model of formulas asserted so far.
 model(Model) :- get_repl_handle(H),
-                z3_model_map(H, Model).
+                z3_model_lists(H, Model).
 
-scopes(N) :- get_repl_handle(S),
-             z3_solver_scopes(S, N).
+model_assoc(Model) :- get_repl_handle(H),
+                      z3_model_assocs(H, Model).
+
+scopes(N) :- get_repl_handle(H),
+             z3_solver_scopes(H, N).
 
 push_check_and_pop(F, Status) :-
     push_formula(F, _NewMap, NewSymbols, Status),
-    get_repl_handle(Solver),
-    z3_solver_pop(Solver, 1, _),
+    get_repl_handle(H),
+    z3_solver_pop(H, 1, _),
     remove_declarations(NewSymbols).
 
-is_implied(F) :- push_check_and_pop(not(F), Status),
-                 Status == l_false.
+implied(F) :- push_check_and_pop(not(F), Status),
+              Status == l_false.
 
 %% todo: handle l_undef
-is_consistent(F) :- push_check_and_pop(F, Status),
-                    Status == l_true.
-
+consistent(F) :- push_check_and_pop(F, Status),
+                 Status == l_true.
+
+implies(X) :- implied(X).
 
-implies(X) :- is_implied(X).
+status(Status) :- get_repl_handle(H),
+                  z3_check(H, Status).
 
 /****
 %% give option to pop last asserted thing? But types remain...
@@ -216,7 +230,7 @@
     maplist(add, L).
 
 :- begin_tests(repl_tests,
-               [setup(reset), cleanup(clear_handle)]
+               [setup(reset), cleanup(clear_globals)]
               ).
 
 test(instantiate_type) :-

type_inference.pl

@@ -201,6 +201,8 @@
 % isoneof(x, v1, v2, ...) is expanded to (x = v1 or x = v2 or ...):
 :- declare(isoneof, T, all(T)).
 
+:- declare(mk_rational, [int, int], real).
+
 sub_type(int, real).
 sub_type(bool, int).
 sub_type(bool, real).

utils.pl

@@ -4,7 +4,8 @@
 	      split_list/3,
 	      subterm_list/2,
               repeat_string/3,
-              readable_bytes/2
+              readable_bytes/2,
+              pair_list_to_assoc/2
     ] ).
 
 /** <module> Basic utils
@@ -43,6 +44,19 @@
 readable_bytes(Bytes, Output) :- gig(G), assertion(Bytes > G), !, Gigs is Bytes/G, swritef(Output, "%w Gigs", [Gigs]).
 
 
+add_pair(Pair, A1, A2) :-
+    Pair =.. [_, K, V],
+    put_assoc(K,A1,V,A2).
+
+/**
+pair_list_to_assoc([], t).
+pair_list_to_assoc([X|Rest], M) :- % TODO: better recursion here.
+    pair_list_to_assoc(Rest, M1),
+    add_pair(X, M1, M).
+**/
+
+pair_list_to_assoc(L, R) :- foldl(add_pair, L, t, R).
+
 :- begin_tests(util_tests).
 
 test(empty) :-