 % This is the common part in module user of the equivalence tester for Prolog queries in SS2021
 % Main idea: as before
 %

 % Main differences:
 % 1. naming convention (SS2021):
 %    aX.pl             student program handed in for assignment X (module user)
 %    solX.pl           hidden solutions (separate module solX)
 %    studX.pl,         simulated student's wrong solution
 %    v21tester.pl      the common internal tester version 21 (module solX) for tester1-6
 %    tester21.pl       this common (!) program, contains main procedure of tester
 %    moduleX.pl,       top-most files importing tester1.pl and calling use_module(solX)
 %
 % 2. only two single unique files for all assignments (from WS 2020, with new namens in 2021):
 %    tester21.pl       in module user   and
 %    v21tester.pl      in modules solX
 %    However, sol1.pl, sol2.pl ... import v21tester,
 %    and module21.pl, module22.pl ... import tester21.pl and solX.pl
 %
 % 3. Module concept (from WS 2020):
 %    main program (module21.pl) calls different modules,
 %    common test program tester21.pl and student's program in module user
 %    different module (solX) used for both together: individual solutions file solX and common v21tester
 %
 %    Advantages of having modules:
 %    - solution file solX.pl and student's file studX.pl may use same procedure names
 %    - it is possible to protect code with :- set_prolog_flag(...)
 %
 %    tester shall be unique, but solution files differ
 %      ==> solution files sol1, sol2, ... include v21tester by :-[v21tester] .
 %          must be directive (NOT goal), because it must be executed at compile time
 %          must be last line because v21tester uses predicates defined in solX (e.g. sizetolerance)
 %    moduleX COMPILES (not loads!) SolutionFile solX.pl,
 %      because solution file is protected, i.e. must not be visible at run time
 %
 %    sol1, sol2,... contain all the solution specific aspects:
 %    - the solutions themselves, number of queries, forbidden goals
 %    - stop predicates, where goal and rule counting is stopped
 %      as we do not want to count goals inside precomiled CLPFD code (or database relations in Assignment1)
 %    - the assignment name (e.g. 6 for Assignment 6) to compute solutionfile name (sol6) for sizefeedback
 %
 %
 % 4. Reimplementation of computing differences diff of student query GQ and hidden query HQ (from WS 2020)
 %    Main ideas:
 %    4.1. Must compare number of solutions, therefore LG=(all answers to QG) and LH=(all answers to HQ)
 %    4.2. Test HQ-GQ first, because showing counter examples of HQ-GQ helps to understand what is expected (e.g., in a5.pl)
 %    4.3. Test GQ-HQ thereafter
 %
 %    Earlier version (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.
 %
 %    sol1 is changed (April 2021) in such a way that database tuples are generated in both modules (user and sol1).
 %
 %    For subtasks 1.X (find a counter example database state ...) all tuples are generated in sol1.
 %
 % 5. Time limit for program executions added, but NOT used.
 %    At the moment (for Assignment 3) time limit was orininally fixed to 800 sec.
 %    However, the time_limit had a bug in version 8.1.26 - the bug is fixed in a later swipl version,
 %    but installing this was too much effort.
 %
 % 6.  Generating test cases - partially automated
 %
 % 6.4. For tester4 search-based puzzles (only),
 %      test cases (test/2) are generated from correct solution as follows.
 %
 %      We require that the student's 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.
 %
 % 6.6. For 6.1 rewrite-rule systems (only)
 %      We generate most (but not all) of the equations containing 5 variables and
 %      require the '=' symbol to be 'in the middle', i.e. after 2nd or 3rd variable
 %
 %      For 6.2., we use the grammar as a generator of test cases

 % 7. From tester6 (of 30.7.2020), students can define further operators.
 %    Before, the tester6 did not know this and could not execute the
 %    students' programs !!
 %
 % 8. Key idea: have a single version of tester1.pl and v21tester.pl only for
 %    assignments 1,2,3,4,5,6 (solved from WS 2020)
 %
 % 9. sizeFeedback is completely reorganized (in WS 2020)
 %    9.HQ. at compile time, compute size of hidden queries HQ
 %    9.GQ. at runtime, compute size of student's queries GQ with the same procedures
 %
 %    9.1. assert rules of solution to clauses/1 at compile time
 %    9.2. assert all predicates (in)directy called by a Goal (avoid duplicate assertions) to query/1 as Pred/Args
 %    9.3. For a Goal, use all Pred/Args in query/1 to count #Clauses and #Goals in calls/2
 %
 %    9.F. Provide a size tolerance for solutions (in solution file, e.g. for subtask 2)
 %         Compare #Clauses and #Goal of GQ of student's solution with
 %                 #Clauses and #Goal of GQ of hidden solution  +  tolerance
 %
 % 10. Reorganized file output procedure lout/3 and its calls (WS2020).


 :- use_module(library(clpfd)) .


 main(Argv) :-                               % assume filename and query ID (=N) are given on command line
    set_prolog_flag(protect_static_code, true) ,  % suggested by Jan W. - does it protect the correct parts of code?
    getFileName(Argv,Filename,N,Found) ,     % 1.  get filename and query ID independently of OS
    ( Found                                  %
      -> style_check(-singleton) ,           %     be tolerant if student file contains singleton variables
         [Filename] ,                        % 2a. load student's file (needed for GQ in prepare_diff in v21tester)
                                             %     (may be, loading file could be avoided if prepare_diff reads clauses/1)
          pl_file_to_clauses(Filename) ,     % 2b. AND assert its rules to clauses/1 (for size check and to check that ...)
          (  \+ usesForbiddenGoals           % 3.  student file does not contain any forbidden goal
             -> doTestQs_(Filename,N)        % 4.  perform test for qN (or if N<0 for all queries)
             ; true                          %     feedback on forbidden goals in student file is given in v21tester.pl
          )
      ;  true
    ) .


 getFileName(Argv,Filename,N,Found) :-                   % get filename and query ID independently of OS
    append(_,[Filename,AN],Argv),                        % last two arguments of console input must be yourfile and queryID
    ( atom(AN)
      -> atom_number(AN,N)                               % e.g. AN = '12' , N=12 (int)
      ;  AN=N
    )                                                    % finally, Filename=a1 and N=12 (int) for testing q1
    -> ( N=0
         -> check_SWI_version ,
            Found=false
         ;  atom_concat( Filename, '.pl', FilenamePL ) ,
            exists_file( FilenamePL )                    % check whether file exists
            -> Found=true
            ;  write('file '), write(Filename), writeln('.pl does not exist') ,
               Found= false
       )
    ;  write('usage: last two arguments of console input must be your file without extension ".pl" '),
       writeln('and the subtask ID (1,2,...) , type e.g. "./tester1 a1 2" for query q2 of Assignment a1' ) ,
       Found=false .



 % ---------------- check SWI-Prolog Version -------------
    check_SWI_version :-                                 % just check that tester works on your system
        current_prolog_flag(version, Version),
        ( Version = 80126                                % requested SWI-Prolog version
          -> write('You have installed the desired SWI-Prolog version 8.1.26') , nl
          ;  ( Version > 80126 )
               -> write('You have installed a newer SWI-Prolog version than 8.1.26 ') , nl,
                  write('Test programs may fail. You can use it on your own risk.  ') , nl
               ;   write('You have installed an older SWI-Prolog version than 8.1.26 ') , nl,
                   write('Test programs may fail. If you use it, it is on your own risk.  ') , nl
        ) .



 :- dynamic clauses/1.                    % to store all non-directive clauses of student file and of solution file
                                          % clauses is used for size computation and (?) to execute student's program

 pl_file_to_clauses(Filename) :-          % get a list of terms (=clauses) from Filename.pl
    concat_atom([Filename,'.pl'],File) ,  % get student's or solution's .pl input file
    read_file_to_terms(File,Ts,[]) ,      % read all terms from student's  or solution's .pl input file into list Ts
    retractall(clauses(_)) ,              % start with empty clauses database
    add_clauses_for(Ts) .                 % add all non-directive clauses to dynamic relation clauses/1


 %  add_clauses_for(Ts) .                 % add all non-directive clauses in Ts to dynamic relation clauses/1
    add_clauses_for([]).
    add_clauses_for([(:-_)|Ts]) :- add_clauses_for(Ts).       % ignore directives (-Why??)
    add_clauses_for([T|Ts]) :-
        \+ T = (:-_) ,                    % for all other non-directive clauses,
        assert( clauses(T) ) ,            % copy the clauses to a dynamic and accessable relation
        add_clauses_for(Ts).



 % v20tester calls  pl_file_to_clauses(solutionFile)  at compile time !!

 % v20tester implements these procedures: getFN/3,usesForbiddenGoals/0,doTestQs_/2





