 % This is the common part of the tester, hidden in modules solX, i.e., solX imports this file
 % last line calls compileTimePreparationsOfSolution which calls sol_X_at_compile_time from solX.pl

 :- set_prolog_flag(protect_static_code, true). % this time OK

 :- use_module(library(clpfd)).



 % ----- begin of old comments ------------
 % Equivalence tester 2021
 %
 % Main idea: as before (2019 and 2020)
 %
 % Main properties:
 %
 % 0. tester21 can performs all tests via doTestQs or
 %    test a single query only via testN
 %    doTestQs writes to a file:
 %    noK*.txt if at least one test fails
 %    oK*.txt if all tests are o.K.
 %
 %    Idea: automated testing via script file for 100 students
 %    -> all files with noK*.txt can be identified automatically
 %       and feedback can be given earlier
 %
 %    The feedback file for the students constains only summary messages, i.e,
 %    some lout messages are f = to be written to file
 %    other lout messages are u = to be written to user only
 %
 %
 % 1. naming convention:
 %    a1.pl, a2.pl, ... assignments to students
 %    sol1.pl, ...      hidden solutions
 %    stud1.pl, ...     simulated student's wrong solution
 %    v20tester, ...    the internal tester version 20 (used in WS2020)
 %    tester1.pl, ...   a tester main program
 %
 %    a1x.pl, ...       later: student solution by student x
 %    ex1.pl, ...       example programs
 %
 % 2. only a single unique file v21tester.pl for all assignments (this file)
 %
 % 3. Module concept:
 %    main program (e.g. module24.pl) , program tester21.pl, and student's program live in module user
 %    v21tester.pl and solution (e.g. sol4.pl) are in a different module (sol4)
 %
 %    v21tester.pl and tester21.pl shall be unique, but solution files differ
 %      ==> main file module calls common file tester21.pl (also in module user) which loads sutudent's file
 %          and loads solution file (e.g. sol4) which finally loads
 %          v21tester.pl
 %
 % 4. The reason for the module concept is the reimplementation of computing differences by prepare_diff and diff
 %    Earlier versions (before 10.5.2020) had name clashes, i.e.  for
 %        ..., same_functor_and_arity(GQ,HQ), diff(GQ,HQ), ...
 %        diff(GQ,HQ) :- GQ , \+ HQ .
 %    GQ and HQ were both taken from module user,
 %    such that GQ=HQ and diff always failed.
 %
 %
 % 5. Time limit for program executions is commented out because it had some non-reproducable unsystematic errors
 %    in version 8.1.26.
 %    Beforehand, (for Assignment 3) time limit was fixed to 800 sec.
 %    Later, with a new SWI-Prolog version time limit may work correctly.
 %
 % 6. For tester4,
 %    test cases (test/2) are generated from the correct solution as follows.
 %
 %    We require that the students implementation of puzzle X uses
 %    procedures moveX/2, lidmX/1, and adfsmpX/1.
 %
 %    We consider each state Si on each shortest path P from S to D,
 %    where P is precomputed by genTestX/1 from the hidden solution.
 %    For each such state Si, genTestX/1 generates a test moveX(Si,_).
 %    So for each correct state, we check that the student's program
 %    generates exactly the same successor states (and thereby is
 %    correct).
 %    If the student's program does not generate a correct successor
 %    state of any state Si, the tester reports an error for Si.
 %    Similarly, if the student's program generates an illegal successor
 %    state of any state Si, the tester reports an error for Si.
 %
 %    Furthermore, we also have to exclude that student solutions are too less constrained.
 %    Therefore, e.g. illegal moves between legal states have been added,
 %    such that the tester also checks that these moves are rejected.
 %
 % 7. (30.5.2020) Predicate counting corrected
 %
 % 8. In tester5, predicate counting at compiletime encoded per
 %    individual test procedure (and not per test as such)
 %
 % 9. In tester6, in diff(...), first find elements of wanted solution missing
 %    in students solution, such that students can get an idea of the wanted solution, e.g.,
 %       [sven,is,a,student,'.']
 %    and do not just get your answer
 %       the result  [sven,is,a,student]  is shown in your program's output, but not in the wanted solution.
 %
 % 10. Assignment1 includes to find database states with certain properties.
 %     to test these states v21tester.pl contains a procedure stateTask/1 .
 %     This procedure is currently not needed in Assignment 2-6.
 %     In order to avoid "undefined procedure" errors, assignments 2-6 contain a rule
 %           stateTask(_) :- false .




 % What could be improved (status of 8.6.2021):

 % 1. A student's program for Subtask 4.61 was
 %         evalfinal( L , -Points ) :-
 %             Points#=L+1,        %The lastElement + 1 determine the Points
 %             L#>=0,L#=<3.        %A lastElement can only be between 0 and 3 because or minimum pick is 4.
 %    The tester4 returned NOT equivalent, because here evalfinal( 3, N ) --> N= - 4
 %    and in the tester,                                evalfinal( 3, N ) --> N= -4
 %    and  - 4 \= -4   !
 %    We could use   - 4  #=  -4    or   -4  is  - 4   ,  but not  - 4  is  -4  .
 %    However, in principle, this mist be encoded arbitrarily deep in the diff procedure,
 %    i.e. for each integer argument, it might happen that a student solution uses - 4 where -4 is in the wanted solution.

 % 2. Tests for Subtask 4.60, 4.6, and 4.61 are somehow odd mixed - do we really need a Subtask 4.61.?





 % How to use equivalence tester:
 %
 % students' programs, e.g. called stud4.pl must contain queries
 % q1(S):- ... . etc.
 % To test a student's solution of a query q1, the student must
 % call the compiled version of the tester4 program (which internal
 % calls the sol4.pl program which itself calls the v21tester program) by
 %
 % ./tester4 stud4 1         (in Unix) or
 % tester4 stud4 1           (in Windows)

 % The MacOS executable tester4 has to be generated by
 %
 % swipl --goal=main -o tester4 -c tester4.pl
 %
 % The Windows executable tester4.exe has to be generated by
 % copying this file, tester4.pl, sol4.pl to Windows and by
 %
 % swipl --goal=main -o tester4.exe -c tester4.pl
 %
 %
 % To count goals correctly, e.g. when library clpfd is used,
 % ?- read_file_to_terms('long3stud.pl',Cs,[]) , member((H:-T),Cs),
 %    H=..[go33|As].
 % check for goals imported_from(M) ...

 % ------------ end of old comments ---



 usesForbiddenGoals :-                                % student file uses forbidden goals?
    getForbiddenGoals(ForbiddenGoals),                % file should not contain any forbidden goals as defined in solX
    findall(T,user:clauses(T),Ts),                    % read clauses from student's program in module user into list Ts
    sub_term(S,Ts),                                   % look at every sub term
    nonvar(S),                                        % whether it is nonvar
    member(S,ForbiddenGoals)                          % and equal to one of the forbidden goals
    -> functor(S,F,A) ,                               % if goal is forbidden
       lout( f,0 , ['The goal ', F, '/', A,
                  ' should not be used in any solution to this exercise!']),
       lout( f,0 , ['However, it occurs in: ',S]) ,
       true
    ;  fail.                                          % student program does not use forbidden goal



 % --------------------------------

 :- dynamic feedback/2 .   % collect feedback to solutions

 % ---------------- part for testXall --------------

 % doTestQs_(+student's file without .pl , +subtask N)  with N\=0
 doTestQs_(Filename,N) :-                             % perform 1 or all test queries
    testQs_(TestQs) ,                                 % get list of numbers [1,...Nmax] of subtasks in SolutionFile
    (   N < 0                                         % if N<0 , test all queries
        ->  doTestQs_1( TestQs, Filename )            % 4a. perform all subtask tests on solX
        ;   member(N,TestQs)                          % if subtask 6.N is part of the assignment 6
            ->  testN(N)                              % 4b. perform tests of only this subtask on solX
            ;   lout(u,N, ['subtask is not part of this assignment.'])    % tester was called for non-existing subtask
    ) .

 % doTestQs_1(+list of IDs of test queries, +student's filename)
 doTestQs_1( TestQs, Filename ) :-                    % perform all test queries on file Filename
    retractall( feedback(_,_) ) ,                     % forget previous feedback
    atomic_list_concat( ['\nTesting file ', Filename, '.pl'], TestFile ) ,
    lout(f,0, [TestFile]) ,                           % via PANDA filename is unique per user
    ( forall( member(N,TestQs) , testN(N) )           % perform all tests
        -> true; true ) ,                             % is this (true;true) really needed in order to get feedback?
    give_feedback(TestQs,Filename) .                  % return summarized feedback

 % give_feedback(+list of IDs of test queries, +student's filename)
 give_feedback(TestQs,Filename) :-
    (   forall(
            (member(N,TestQs),        % except 1.25
             feedback(N,F)                            % if N=3, get feedback F to e.g. task 6.3
            ) ,
            (   F=['Your solution is most likely equivalent to the wanted solution.']  % all tests passed + solution size oK
              ; append( [_,_] , ['shows that a solution to query'|_] , F )
            )
        )
        ->  Prefix = 'oK_'                            % file prefix is "oK_"
        ;   Prefix = 'not_oK_'                        % file prefix is "not_oK_"
    ) ,
    atomic_list_concat( [Prefix,Filename,'.txt'] , FileOut ) ,
    open(FileOut,write,Out),                          % print feedback for all tests test_(N)
    write('Just tested file '),write(Filename),write('.pl\n'),   % via PANDA filename is unique per user
  % Error: prints feedback 25.1 twice:   (   forall( feedback(N,_) , print_feedback(N,Out) ) -> true ; true ) ,
    print_all_feedback(Out) ,
    close(Out),
    true.

 %  print_feed_all_back( +FeedbackOutputFile Out )
    print_all_feedback(Out) :-
        feedback(N,F) ,
        ( N>0 , N<25                                  % only if N!=0 and N<25 print "query N:"
           ->  write( Out,'Query') , write( Out, N ) , write( Out, ': ')
           ;   true
        ) ,
        flout( Out ,F ) , fail .
    print_all_feedback(_) .



 %  print_feedback( +Subtask, +FeedbackOutputFile Out )
    print_feedback( N, Out ) :-                       % print the feedback for subtask N to file Out
        feedback(N,F) ,                               % read the feedback for subtask N
        ( N=0                                         % only if N!=0 print "query N:"
           ->  true
           ;   write( Out,'Query') , write( Out, N ) , write( Out, ': ')
        ) ,
        flout( Out ,F ) .                             % print the feedback line to file Out

        flout(Out,[]) :- writeln(Out,' ') .           % print list to file Out
        flout(Out,[H|T]) :- write(Out,H) , write(Out,' ') , flout(Out,T) .



 % ---------------- part for prepare testing an individual subtasks N --------------

 % % Here subtask N has to be translated into one testcase group N (e.g. in Assignment 2+3) or multiple testcase groups (A1,A4-A6)
 % % Maybe, we need a table subtask2testcasegroups, s2t for short, with
 % % s2t(a61,[a611=if/2,a612=isolate_final/2]).
 % % s2t(a62,[a621=sentence/3,a622=move/3,a623=question/3,...]).
 % % the generated tests could then be encoded as   test(621,sentence(...,...,...)).
 % % the variable N used in the following represents one testcase group (e.g. 621 for sentence/3 in A6.2. or 622 for move/3)


 % testN(+SubtaskID) - e.g. N=3 for subtask 6.3 - prepare correctness test of student's queries GQ1,...,GQk of subtask N
 %                       by comparing student queries GQ1,...,GQk with hidden queries HQ1,...,HQk
 testN(N) :-          %  do all tests of a subtask  % may become additionally: including all test case groups
  stateTask(N)        % "find a state task", e.g. 1.25
  -> q(N)
  ;  procForQNundefined(N,GQ)      % if no clause GQ:-Tail and no DCG rule for hidden query N is in student's file
    ->  lout(f,N, ['rule  ' , GQ, ' :- ...  not found in your program.'])     % f = print feedback also to file
    ;   do_testGQHQ(N) .                          % does the real test


    procForQNundefined(N,GQ) :-           % find in student's file a clause (GQ:-Tail) or a DCG rule for hidden query N
        test(N,HQ)  ,
      %  ! ,                         NO!  % one test is enough to get functor and arity of hidden query HQ for subtask N
        functor(HQ, F, A) ,               % there may be multiple queries per subtask !?!
        functor(GQ, F, A) ,
        \+ dcgORpl_rules_in_File(F/A,_,_) .   % lookup user:clauses/1 for clauses or DCG rules matching HQ of subtask N


    % --------------------------------
    % lout(+PrintToWhere,+SubtaskID,+FeedbackMessage) - print to user and optionally also to file
    % PrintToWhere: File=f : print also to file , File=u : print only to user output
    % SubtaskID: queryID = 0 : do NOT print Assignment.SubtaskID, e.g. used for extra lines in feedback about too long solutions
    % QueryID = 3 : feedback to Query with ID 6.3 in Assignment6

    lout(File,QueryID,Message) :-
        ( File = f -> assert( feedback( QueryID, Message ) ) ; true ) ,  % prepare feedback
        QueryID = 0                                   % if QueryID is 0 , i.e. NOT 6.3
        ->  lout( Message )                           % print extra line of output without task name
        ;   taskname(QueryID,TaskN) ,                 % construct task name TaskN 6.3. to be used in lout
            lout( ['\nSubtask ', TaskN, ' : ' | Message ] ) .  % add TaskN, e.g. 6.3, to message


 lout([]) :- nl .                                     % print list to a line
 lout([H|T]) :- write(H), write(' '), lout(T).


 % ---------------- part for doing the real test of an individual subtasks N --------------

 % do_testGQHQ(+N) :- % test all test cases for query N and give feedback

 do_testGQHQ(N) :-                                    % test all test cases for query N and give feedback
    are_different(N)                                  % find and print a counterexample for Nth subtask with GQ<>HQ
    ->  true                                          % counter example info printed as part of are_different/1
    ;                                                 % solution is logically correct
        solutionIsTooLong(N)                          % check whether student's solution is too long and if so, tell why
        ->  true
        ;   lout( f, N , ['Your solution is most likely equivalent to the wanted solution.']) .

 %  are_different(+N)                       % test all test cases in one or in more states (depending on the assignment)
    are_different(N) :-                               % find and print a counterexample for Nth subtask with GQ<>HQ
        assignment(Ass) ,                             % get Assignment number, e.g. 6
        ( Ass > 1 ->                                  % for assignments 2,3,4,5,6 do
            prepare_diff(N,Q,LG,LH),                  % create solution set LG and LH
            diff(N,Q,LG,LH)                           % find and print a counterexample for Nth Goal with GQ<>HQ
         ;  counterexample_on_db(N)                   % for Assignment 1, counterexample search on databases with
                                                      % side effects modifying a database
        ) .



 % -------------------------------------------------------


  % taskname(+N,-TaskN)  - transform e.g. N=9 to TaskN=2.9 for Assingment 2 - to be used in diff and elsewhere
    taskname(N,TaskN) :-
        assignment(Assignment) ,                      % get ID of assignment, e.g. 6
        atomic_list_concat( [Assignment,'.',N] , TaskN ) .     % concat them to task name 2.9


  % prepare_diff(+N,-Q,-LG,-LH) - create solution set LG for student's query GQ and LH for hidden query HQ
  %                               for test case Q of subtask N
    prepare_diff(N,Q,LG,LH) :-  % create solution set LG and LH for 2 independent test queries (GQ,HQ) for Q
        test(N,Q) ,                                   % pick the next test case Q for subtask N (choice point!)
  % writeln( testcase: Q ) ,
  % gtrace ,
        copy(Q,GQ) ,                                  % GQ has same parameter bindings as Q, but different variables
        copy(Q,HQ) ,                                  % HQ has same parameter bindings as Q, but different variables
        findall(GQ,user:GQ,LG) ,                      % LG = all solutions for GQ to test query Q
        V11HQ = HQ ,                                  % call HQ(...) in module v11tester to find all solutions,
            % was :  V11HQ = (v11tester:HQ) ,
        findall(HQ,V11HQ,LH) .                        % but return solutions of v11tester:HQ(...) as HQ(...) via LH to diff

        :- dynamic pred/1.
        copy(Goal,G) :-                               % copy Goal to G
              assert(pred(Goal)),                     % without binding variables in Goal to variables in G
              retract(pred(G)) .



  % diff/4 is used in two different modes: for Assignment 1, Q is a database state to be printed
  %                                        for assignments 2..6, Q is a query with specific parameters
  % diff( +Subtask ,+TestCase_OR_DatabaseState, +AllSolutionsToStudentProcedure, +AllSolutionsToHiddenProcedure )
  % find and print a difference, i.e., find and print a binding (=counterexample) for Nth Goal with GQ<>HQ
    diff(N,Q,LG,LH) :-                                % find and print differences between query results LG and HQ
        taskname(N,TaskN) ,                           % construct task name TaskN to be used in diff
        member(H,LH), \+ member(H,LG) ,               % does LH have a solution H not provided by LG ?
        lout( f, N, ['Your solution to subtask',TaskN,'is NOT equal to the wanted solution',TaskN,'.\n',
                     'For example, for', Q , '\n',
                     H, '\n' ,                        % show a solution of HGoal, not found by Goal
                     'is shown by the wanted solution, but not in your program''s output']) .

    diff(N,Q,LG,LH) :-                                % find difference in the lists LG and LH of answers to Q
        taskname(N,TaskN) ,                           % construct task name TaskN to be used in diff
        member(G,LG), \+ member(G,LH) ,               % does LG have a solution G not provided by LH ?
        lout( f, N, ['Your solution to subtask',TaskN,'is NOT equal to the wanted solution',TaskN,'.\n',
                     'For example, for', Q , '\n',
                     G, '\n' ,                        % show a solution of Goal, not found by HGoal
                     'is shown in your program''s output, but not by the wanted solution']) .

    diff(N,Q,LG,LH) :-                                % do we get unwanted duplicate answers ?
        taskname(N,TaskN) ,                           % construct task name TaskN to be used in diff
        length(LG,Gs), length(LH,Hs),
        \+Gs=Hs ,                                     % different number of answers
        append( [ [ 'Your solution to subtask',TaskN,'does NOT have the same size as that of the wanted solution',TaskN,'.\n',
                    'For', Q ,'your solution to subtask',TaskN,'returns:\n'  | LG ] ,
                  [ '\n',     'and the wanted solution returns:\n'           | LH ] , [ '\n' ]
                ] , NotSameSize ) ,
        lout( f, N, NotSameSize ) .


 %------------- counter example search for database states --------

    counterexample_on_db(N) :-                        % construct one counterexample for qN using a database
        clearDB ,                                     % start with empty DB to keep counter examples small (from sol1)
        clearDBintern ,                                     % start with empty DB to keep counter examples small (from sol1)
        counterex_on_db(N) ,                          % test on empty database
        ! .                                           % one counter example found is enough, no more atest (cut unnecessary)
    counterexample_on_db(N) :-                        % construct one counterexample for qN using a database
        atest(N,AdditionalTuple) ,                    % choice point: get additional test tuple from sol1
        add(N,AdditionalTuple) ,                      % add test tuple to DB + find counter example_on_DB
        ! .                                           % one counter example found is enough, no more atest (cut unnecessary)

    add(N,Tuple) :-                                   % add Tuple to DB, thereby change DB state
        assert(user:Tuple),
        assert(sol1:Tuple),         % to module sol1
        counterex_on_db(N) .

    counterex_on_db(N):-
        prepare_diff(N,_,LG,LH) , % create solution set LG and LH for 2 independent test queries (GQ,HQ) for Q
        dumpDB(DB_Dump) ,                             % dump database into a printable table (from sol1)
        diff(N,DB_Dump,LG,LH) .


 %------------- check whether database state proposed by student has desired properties --------

 % q(+Task) - check whether a student's database state (e.g. state(25,club(hsv,1880)),state(25,...) )
 %            is collected appropriately to show the expected difference between two queries, where
 %            the expected difference between two queries is stored in sol1 e.g. as
 %            diffType(25,q20(_),q21(_),both).
 %            instead of 'both' the ExpectedDiffType could also be 'notHQ1inHQ2' or 'notHQ2inHQ1'

 q(N) :- diffType(N,HQ1,HQ2,ExpectedDiffType) ,       % read expected answer on difference type
         clearDBintern ,                              % start with empty DB to keep counter examples small (from sol1)
         loadDB(N) ,                                  % load student's DB for task N into module user
         findall(HQ1,HQ1,LHQ1) ,                      % LHQ1 = all solutions for HQ1 on DB state
         findall(HQ2,HQ2,LHQ2) ,                      % LHQ2 = all solutions for HQ1 on DB state
         diffAsExpected(N,LHQ1,LHQ2,HQ1,HQ2,ExpectedDiffType) .

                                                      % should also delete base relations (footballer, ...)
    loadDB(N) :- user:state(N,Fact), assert(Fact), fail.   % load student's DB for task N into module user
    loadDB(_).


    diffAsExpected(N,LHQ1,LHQ2,HQ1,HQ2,notHQ1inHQ2) :-
        noSubset(LHQ1,LHQ2)
        -> lout( f, N, ['OK: Your database state to subtask',N,'shows that a solution to query',HQ1,
                         'returns a result that is not returned by a solution to query',HQ2,'.\n'])
        ;  lout( f, N, ['not OK: Your database state to subtask',N,'fails to show that a solution to query',HQ1,
                         'returns a result that is not returned by a solution to query',HQ2,'.\n']) .

    diffAsExpected(N,LHQ1,LHQ2,HQ1,HQ2,notHQ2inHQ1) :-
        diffAsExpected(N,LHQ2,LHQ1,HQ2,HQ1,notHQ1inHQ2) .

    diffAsExpected(N,LHQ1,LHQ2,HQ1,HQ2,both) :-
        diffAsExpected(N,LHQ1,LHQ2,HQ1,HQ2,notHQ1inHQ2) ,
        diffAsExpected(N,LHQ1,LHQ2,HQ1,HQ2,notHQ2inHQ1) .


    noSubset(LHQ1,LHQ2) :- member(G,LHQ1) , \+ member(G,LHQ2) . % could show that LHQ1 is not subset of LHQ2




 % ---------------- part for computing feedback on solution size for subtasks N --------------

    % give feedback on size (Rules and Goals) of student's solution to Subtask, but ignore StopPredicates
    % give feedback about too long solution only if the RuleTolerance/GoalTolerance is exceeded

 solutionIsTooLong(N) :-                              % check whether student's solution is too long and if so, tell why
    givenHidden(N,GQ,HQ) ,                               % use test cases to find name/arity of Goal and hidden HGoal
    procSize(GQ,GQClauses,GQGoals) ,                   % ** count clauses and goals of GQ in student file **
    compiletimeProcSize(N,HQ,HQClauses,HQGoals),   % ** use number of clauses+goals counted at compile time **
    getSizeTolerance(N,ClauseTol,GoalTol) ,              % ClauseTol/GoalTol, i.e. how many more clauses/goals are o.K. for task N
    ( HQClauses+ClauseTol#<GQClauses, HQGoals#=< GQGoals ;  % student solution has too many (>ClauseTol additional) clauses
      HQClauses+HQGoals+1 #< GQClauses ;                 % student solution has e.g. everything encoded as facts
      HQClauses#=<GQClauses, HQGoals+GoalTol#<GQGoals    % student solution has too many (>GoalTol additional) goals
    ) ,                                                  % ** now we know that student's solution is too long **
    functor( HQ,FHQ,AHQ ) ,                              % tell why student's solution is tool long
    lout( f, N , ['Your solution to this subtask is most likely equivalent to the wanted solution.\n',
                  'However,the wanted solution for ', FHQ/AHQ, ' is shorter than yours!\n',
                  'The wanted solution has', HQClauses, 'clauses and', HQGoals, 'goals,\n' ,
                  'and your solution has', GQClauses, 'clauses and', GQGoals, 'goals.']) .

    getSizeTolerance(N,ClauseTol,GoalTol) :-             % ClauseTol/GoalTol, i.e. how many more clauses/goals are o.K. for task N
        sizeTolerance(N,ClauseTol,GoalTol)               % if ClauseTolerance/GoalTolreance is predefined
        ->  true                                         % take it
        ;   ClauseTol=0 , GoalTol=0 .                    % otherwise no tolerance is granted


 % givenHidden(+N,-Goal,-HGoal)
 givenHidden(N,Goal,HGoal) :-                            % find name of Goal and hidden HGoal for subtask N
    test(N,Pred) ,                                       % use test cases for subtask N to find names of Goal and hidden HGoal
  %  ! ,                                                  % ?one test case is enough - do not generate a choice point??
  %                                                       % No! In Assignment 5 and 6, we have different procs per test
    functor(Pred,F,A) ,
    functor(Goal,F,A) ,
    functor(HGoal,F,A) .



 :- dynamic compiletimeProcSize/4 . % precompute number of rules and goals of Proc in SolutionFile at compile time

 precomputeSolutionSizes :-                              % changed for sol5 - which has multiple queries per test (also good for tester1)
    retractall( compiletimeProcSize(_,_,_,_) ) ,   % delete all counters #Rules / #Goals of hidden query of any subtask
    testQs_(Subtasks),                                   % get all subtasks based on info from solX
    member(QID,Subtasks) ,                               % for each subtask N=QID,
    givenHidden(QID,_,HQopen) ,                          % use test cases to reconstruct open hidden query HQopen=hN
    procSize(HQopen,HQClauses,HQGoals) ,                 % count clauses and goals of hidden HQopen and
    assert( compiletimeProcSize( QID , HQopen, HQClauses, HQGoals ) ) ,     % assert counts for runtime
    fail.
 precomputeSolutionSizes.



 % ================================================================
 % program size computation with stop predicates
 %    For hidden solution, program size is computed at compile time,
 %    for student's query, program size is computed at run time.
 %
 %    We compute the program size used for computing a particular Goal=Pred/Arity,
 %    independently of the goal's actual parameters
 %    procSize reads the top goal (Goal) of a student's file or of a solution file
 %    (the clauses of which have been asserted to clauses/1),
 %    and counts the number of clauses and goals directly or indirectly called from Goal=Pred/Arity.
 %
 %    ++ :) We have a program that can estimate the simplicity of a solution


 % procSize( +Goal, -Clauses, -Goals) - count Clauses and Goals used by Goal, except inside stopPredicates
 procSize(Goal,Clauses,Goals) :-                     % count #Clauses and #Goals used by Goal, except inside Stop
                                                     % do not search further in Stop predicates
    initProcSize ,                                   % clear dynamic tables query/1 and calls/2
    collectAllPredicateNames(Goal,pl) ,              % collect all predicate names in clauses/1
                                                     % called (in)directly in query, stop at Stop predicates
    findAllRules(Clauses,Goals) .                    % sum up Clauses&Goals used for each predicate in clauses/1


 isBuiltInOrLibrary( Goal ) :-
    predicate_property( Goal , imported_from(M) ) ,  % Goal is defined in module M
    \+ M=user ,                                      % M is not module user (i.e. student's file)
    \+ solutionFile(M) .                             % M is not solX (e.g. not sol4)

 isStopPredicate(P/A) :-
    functor(Goal,P,A) ,
    isBuiltInOrLibrary( Goal ) .                     % do not count inside builtins or called library preds
 isStopPredicate(P/A) :-
    stopPredicates( Stop ) ,                         % do not search further in solX specific Stop predicates
    member(P/A,Stop) .

 isStopGoal(Goal):-                                  % do not count inside builtins, library preds, and solX stop goals
    functor(Goal,P,A) ,
 isStopPredicate(P/A) .


 initProcSize :- retractall(calls(_,_)) , retractall(query(_)) .

    % query/1 stores previously found queries in the query table - avoid counting reused code twice
    :- dynamic query/1.

    % calls/2 counts found calls in the counts table -
    % currently count calls per goal (could have been total counts instead)
    :- dynamic calls/2.


 % ----- Part 1 of size computation: -------

 /* collectAllPredicates shall collect all the predicates called (in)directly
  * by a Goal without counting how often they are called.
  * Extra procedure needed as findCalledPredicates/2 produces choice
  * points (by error in findCalledPredicates/2 ?)
  */

 collectAllPredicateNames(Goal,pl) :-
    findCalledPredicates(Goal,pl) ,                  % collect all predicate names in clauses/1
    fail.
 collectAllPredicateNames(_,_) .


 /* findCalledPredicates shall collect all the predicates called (in)directly
  * by a Goal without counting how often they are called.
  * dynamic query/1 stores the Functor/Arity pair of an (in)directly
  * called goal. We store Functor/Arity pairs as we do not want
  * to distinguish goals or queries by their actual parameters.
  * query/1 is used in the next procedure, findAllRules, for really
  *  counting rules and goals of a called predicate.

  * The main challenge is that there are two kinds of goals and
  * two kinds of rules, i.e., Prolog rules and DCG rules, which can call
  * or be called, i.e. Prolog rules can call DCG rules and vice versa.
  * In findCalledPredicates, we distuingh them by Kind=pl or Kind=dcg.
  *
  * To map both kinds of goals and rules to each other and to simplify
  * further processing, the procedure singleGoal internally represents a
  * Goal by its Prolog Functor/Arity pair. Also, dynamic query/1 stores
  * the Prolog Functor/Arity pair of a called goal, even if it is
  * called inside a DCG rule.

  * However, because Goal may be e.g. (Goal1,Goal2) and Goal2 may be
  * (Goal21,Goal22), in findCalledPredicates, we need the Goal itself, and
  * not only its Functor/Arity pair while processing the Goal.
  * Processing the Goal is done in findCalledPredicates and in bui.
  * For finding rule heads that match a Goal, Pred/Arity is sufficient,
  * however we need the full rule Body to catch builtins like "," , ";"
  * , "->" ...

  * Limitation: does not find procedure names for some goals constructed
  * at run time, e.g. Goal=.. [...] , Goal
  *
  * ToDo: Can we combine the implementation of findCalledPredicates and
  *       findAllRules into a singke procedure with extra parameters?
  *       (difficult, i.e. nearly impossible, because first stops if and
  *       only if Goal is not new)
  *
  * ToDo: Can we do better than using assert/retract on query and
  *       clauses?

  */

 % stop predicate search if Goal is a stopPredicate of solX (e.g. lidm/4,adfsmp/4, ...)
 % +Kind=pl if Goal is called as a Prolog goal, and +Kind=dcg if Goal is called as a DCG rule goal
 % findCalledPredicates(+Goal,+Kind)               % read clauses/1 to collect all pairs predicate Pred/Arity
                                                   % called (in)directly in Goal, stop at Stop predicates
 findCalledPredicates(Goal,Kind) :-                % collect all predicate names called (in)directly by Goal
    var(Goal)                                      % goals like Move, after Move =.. ... are not expanded
    -> true                                        % -> Goals constructed at runtime are not considered
    ;  ( Goal=({_}) ; isStopGoal(Goal) )           % if goal is StopGoal (i.e. builtin!) or is {...}
    -> bui(Goal,Kind)                              % for built-ins, special treatment %% How to note (,)/4 in DCGs??
    ;  functor(Goal,Fun,Arg),
       plArgsOfKind(Arg,Kind,ArgPl) ,              % ArgPl is number of arguments in Prolog version of Goal
       singleGoal(Fun/ArgPl) .                     % find called Predicates for single Goal=Functor(Args in Prolog)


  % bui(+Goal,+Kind) - special treatment of findCalledPredicates for built-ins and for {...}
    bui(Goal,Kind) :-
        (   Goal = (Body1,Body2)                   % for ',' ';' '->' collect Predicate names in left part and right part
        ;   Goal = (Body1;Body2)
        ;   Goal = (Body1->Body2)
        )
        ->  findCalledPredicates(Body1,Kind) ,
            findCalledPredicates(Body2,Kind)

        ;   Goal = (\+Body)                        % for negation as failure, ignore \+, but with embedded Body,
        ->  findCalledPredicates(Body,pl)          % collect builtins and user defined predicates within Body

        ;   Goal = findall(_,Body,_)               % for findall/3
        ->  findCalledPredicates(Body,pl)          % collect builtins and user defined predicates within 2nd arguments

        ;   Goal =.. [maplist,Func|As] ,           % for maplist/? , e.g. for maplist(add,R,S,T) : Func= add
            Func =.. [F|FAs] ,                     % e.g. for maplist( add(7),L1,L2 ) , we have Func=add(7)
            append( FAs,As,FAsAs ) ,               % e.g. for maplist( add(7),L1,L2 ) , we have FAsAs=[7,L1,L2]
            Pred =.. [F|FAsAs]           % ERROR   % now check add( 7, L1, L2 )  % NOT CLEAN ! should be elem(L1)
        ->  findCalledPredicates(Pred,pl)          % collect builtins and user defined predicates within 2nd arguments

        ;   Goal = ({Body})                        % for {Goal}, do not collect {}, but
        ->  findCalledPredicates(Body,pl)          % collect builtins and user defined predicates within included Goal

        ;   true .                                 % do not expand other builtins (Move=..[F\As],[word]


  % plArgsOfKind(+#Args,+Kind,-#Args of Prolog version of rule) - we need number of arguments of Prolog version of rule
    plArgsOfKind(Arg,pl,Arg).
    plArgsOfKind(Arg,dcg,ArgPl) :- ArgPl#=Arg+2.   % ArgPl is number of arguments in Prolog version of Goal


 % singleGoal(Fun/ArgPl) - a single proc only to find all DCG or PL rules matching Goal=Functor(Args in Prolog)
 singleGoal(Fun/ArgPl) :-                          % find called Predicates for single Goal=Functor(Args in Prolog)
    ( query(Fun/ArgPl)                             % if Goal with same Functor and Arity has already been processed OR
    ; isStopPredicate(Fun/ArgPl)                   % if Goal is a Stop predicate, stop search for called Predicates
    )
    -> true                                        % stop recursive search for (in)directly called Predicates
    ;  assert( query(Fun/ArgPl) ) ,                % store in query-table that we found and treated Goal
       dcgORpl_rules_in_File(Fun/ArgPl,Body,Kind), % find all pl rules and dcg rules for Goal
       doBody(Body,Kind).                          % recursively search called predicates in Body of Kind2 pl or dcg

    doBody(true,_).                                % terminate search successfully for facts
    doBody(Goal,Kind) :-                           % recursively search in Body
        \+ Goal=true ,                             % if Body exists
        findCalledPredicates(Goal,Kind).           % recursively search in Body


 % ----- common part of size computation: ---------------------------------------------------

 % Kind=pl:Body is Prolog rule body , Kind=dcg:Body is DCG rule body

  % dcgORpl_rules_in_File(+Fun/+Arg,-Body,-Kind)   % find all clauses for Goal
    dcgORpl_rules_in_File(Fun/ArgPl,Body,pl) :-    % find all clauses for Goal
        functor(HeadPl,Fun,ArgPl),
        clauses_in_File(HeadPl,Body,pl) .          % search for Prolog rules matching Goal

    dcgORpl_rules_in_File(Fun/ArgPl,Body,dcg) :-   % find all dcg rules for Goal
        ArgDcg #= ArgPl-2 ,                        % matching dcg rules have 2 arguments less than Prolog goal
        ArgDcg #>= 0 ,                             % DCG rule can not have less than 0 arguments
        functor(HeadDcg,Fun,ArgDcg),
        clauses_in_File(HeadDcg,Body,dcg) .        % search for dcg rules matching goal



 % for a given Head of the form p(_,...,_) find clauses one by one,
 % return Body and Kind, i.e., Kind=pl for a Prolog rule or Kind=dcg for a DCG rule
 % return Body=true for facts and for empty DCG rules
 % clauses_in_File( +Head, -Body, -Kind )          % find bodies for that head and return Kind (dcg or pl) of rule
 clauses_in_File( Head, Body, Kind ) :-            % find bodies for that head
    user:clauses(C) ,                              % read a clause (OR a DCG rule!) from student's program in module user
 %    \+ C=(:-_) ,                                   % ignore directives
    get_body(C,Head,Body,Kind) .                   % return body of actual rule matching head and kind (=pl/dcg/fact)

 % get_body( +ClauseInFile, +HeadOfClause, -BodyOfClause, -KindOfClause ) - get Body matching given Head and Kind
 get_body(C,Head,Body,pl) :-  C=(Head:-Body) .     % for ordinary rules, return body of actual rule matching head
 get_body(C,Head,Body,dcg) :- C=(Head-->Body) ,    % for DCG rules too,
                              \+ Body=[] .         % if Body <> []
 get_body(C,C,true,pl) :-     \+ C=(_:-_) ,        % Head=C, Body=true for Prolog facts, i.e., neither rules,
                              \+ C=(_-->_) ,       % nor DCG rules,
                              \+ C=(:-_) .         % nor directives
 get_body(C,Head,true,dcg) :- C=(Head-->[]) .      % Head=C, Body=true for empty DCG rules


 % ----- Part 2 of size computation: -------


 % findAllRules( -NumberOfClauses, -NumberOfGoals )
 findAllRules(_,_) :-                 % sum up clauses and goals for each called predicate stored in query(P/A)
    query( P/A ) ,                                 % a called predicate
    \+ isStopPredicate(P/A),                       % do not count inside list of stop predicates
    dcgORpl_rules_in_File(P/A,Body,_) ,            % find each clause/each dcg rule and corresponding Body for P/A
    incCalls(clauses) ,                            % one more clause just found and now counted in dynamic calls/2
    count_goals( Body ) ,                          % count tree of body by counting each goal in body
    fail .

 findAllRules(Clauses,Goals) :-                    % final sum computation and return of Clauses+Goals
    DontCount=[true,nl] ,                          % do not count true as "fact." is passed as "fact:-true."
    findall(N,(calls(Goal,N),\+member(Goal,DontCount)),Ns),  % find all clauses and goals not in DontCount
    sum_Of_List(Ns,Sum),                           % Sum = #Clauses + #Goals
    calls(clauses,Clauses),                        % do not count clauses as goals
    Goals is Sum-Clauses.                          % do not count clauses (facts and rules) as goals


    sum_Of_List([],0) .
    sum_Of_List([H|T],N) :- sum_Of_List(T,N1) , N is N1 + H .


  % count DCG bodies as if they were Prolog Bodies (a hack to catch goal Move)
  % we do not need a special case for maplist/3: it simlpy counts as 1 goal , findAllPredicates finds the nested goal

 % count_goals( +Body )  = count number of goals of rule body, increment value in dynamic calls/2
 count_goals( Body ) :-                   % count number of goals of ordinary pl rule Body or dcg rule Body
        var(Body)                                  % e.g. for goals like "Move" after Move=..[F|As]
    ->  incCalls(pgmcall(Body))                    % count a call to Move (e.g. in sol4) as 1
    ;   (   Body = (Body1,Body2)                   % for goal sequences count both parts
        ;   Body = (Body1;Body2)                   % for goal alternatives count both parts
        ;   Body = (Body1->Body2)                  % count goals in if part and in then part
        )
    ->  count_goals( Body1 ) ,                     % count actual goal of a clause - a hack: count them as Prolog goals
        count_goals( Body2 )                       % and remaining goals
    ;   Body = (\+Goal)                            % do not count \+ itself, but
    ->  count_goals(Goal)                          % count negated goal
    ;   Body = findall(_,Goal,_)                   % if goal is a findall/3 call
    ->  incCalls(findall) ,                        % count findall itself
        count_goals(Goal)                          % count 2nd argument of findall
    ;   Body = ({PlGoal})                          % do not count {...} itself,
    ->  count_goals(PlGoal)                        % count goals inside {...} - as Prolog goals
    ;   incCalls(Body) .                           % count ordinary goals as 1


 incCalls(Goal) :-                                 % increment the number of calls to Goal in dynamic calls/2
    functor(Goal,F,A) ,                            % only structure (F/A) of Goal has to be stored in order to
    functor(Goal2,F,A) ,                           % avoid counting different calls of same goal twice
    (   retract(calls(Goal2,Old))
        ->  New is Old+1 ,
            assert(calls(Goal2,New))
        ;   assert(calls(Goal2,1))
    ) ,
    true .


 % ----- Part 2b of size computation at compile time: -------


 compileTimePreparationOfSolution :-               % at compile time ...
    solutionFile(SolutionFile) ,                   % get the name of the solutionFile
    user:pl_file_to_clauses(SolutionFile) ,        % transform solution file to clauses in order to ...
    solX_at_compile_time ,                         % steps to be done in solX at compile time,
                                                   % in Assignment 1: init test(2)
                                                   % in Assignment 4: e.g. solving the mug puzzle
    precomputeSolutionSizes .                      % compute solution sizes for assignments
                                                   % (i.e. test procedures) of solution

    solutionFile(SolutionFile) :-                  % get file name of solution file,
                                                   % needed e.g. to precompute solution sizes at compile time
        assignment(N) ,                            % get ID of assignment, e.g. 6
        atom_concat(sol,N,SolutionFile) .          % generate SolutionFilename, e.g. sol6 (without .pl)


 :- compileTimePreparationOfSolution .             % steps to be done in v11tester

