1		% Heinrich Heine Universitaet Duesseldorf
2		% (c) 2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(prover_interface, [use_prover/3, use_prover/4, prover_command/2]).
6
7		:- use_module(probsrc(module_information),[module_info/2]).
8		:- module_info(group,sequent_prover).
9		:- module_info(description,'This module provides available predicates for proving a sequent').
10
11		:- use_module(library(lists)).
12		:- use_module(probsrc(b_ast_cleanup),[clean_up_pred_or_expr/3]).
13		:- use_module(probsrc(translate),[transform_raw/2]).
14
15
16		% use_prover/3 -----------------------------------
17		use_prover(Cmd,RawHyps,RawGoal) :-
18		prover_command(Cmd,ProverList),
19		maplist(transform_raw,RawHyps,THyps),
20		transform_raw(RawGoal,TGoal),
21		maplist(clean_up_pred_or_expr(_NonGroundExceptions1),THyps,CleanTHyps),
22		clean_up_pred_or_expr(_NonGroundExceptions2,TGoal,CleanTGoal), % TODO: exceptions
23		(bsyntaxtree:is_truth(CleanTGoal)
24		-> true % if ast_cleanup gives a true goal, we don't have to call a prover
25		; prove_sequent(ProverList,CleanTHyps,CleanTGoal)
26		).
27
28		prove_sequent(prob_wd_prover,THyps,TGoal) :- !,
29		well_def_analyser:prove_sequent(proving,TGoal,THyps).
30		prove_sequent(ProverList,THyps,TGoal) :-
31		atelierb_provers_interface:prove_predicate_with_provers(ProverList,THyps,TGoal,proved).
32
33		prover_command(ml_pp,[ml,pp]).
34		prover_command(ml,[ml]).
35		prover_command(pp,[pp]).
36		prover_command(prob_wd_prover,prob_wd_prover).
37
38
39		% use_prover/4 -----------------------------------
40		use_prover(prob_disprover,RawHyps,RawGoal,Result) :-
41		AllHyps = RawHyps, SelectedHyps = RawHyps, Timeout = 1000,
42		% TO DO: pass information about top-level types, new deferred sets, ...
43		disprover:disprove(RawGoal,AllHyps,SelectedHyps,Timeout,Result).
44
45		use_prover(z3,RawHyps,RawGoal,Result) :-
46		list_to_conj_raw([negation(unknown,RawGoal)|RawHyps],RawAst),
47		bmachine:b_type_check_raw_expr(RawAst,[],Typed,open(no_quantifier)),
48		smt_solvers_interface:smt_solve_predicate(z3,Typed,_,Result).
49
50		% get a conjunction from a list of raw expressions
51		list_to_conj_raw([X],Res) :- !, Res=X.
52		list_to_conj_raw([H|T],conjunct(unknown,H,R)) :- list_to_conj_raw(T,R).