logicmoo.base.examples.fol.FOL_CARDINAITY_AXIOMITIZED_01 JUnit

[TeamSPoon]

trafficstars

(cd /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol ; timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "['fol_cardinaity_axiomitized_01.pfc.pl']")

% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/fol_cardinaity_axiomitized_01.pfc.pl % JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/FOL_CARDINAITY_AXIOMITIZED_01/ % ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3AFOL_CARDINAITY_AXIOMITIZED_01 % ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/607

%~ init_phase(after_load)
%~ init_phase(restore_state)
%
%~ init_why(after_boot,program)
%~ after_boot.
%~ Dont forget to ?- logicmoo_i_cyc_xform.
running('/var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_cardinaity_axiomitized_01.pfc.pl'),
%~ /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl:93 
%~ this_test_might_need( :-( use_module( library(logicmoo_plarkc))))



% Tests that you can express regular semweb cardinatility though in FOL

/*
EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/family_regress_01.pfc.pl 
JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/FAMILY_REGRESS_01/ 
PREVIOUS: https://jenkins.logicmoo.org/job/logicmoo_workspace/69/testReport/logicmoo.base.examples.fol/FAMILY_REGRESS_01/ 
ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3AFAMILY_REGRESS_01 
GITLAB: https://gitlab.logicmoo.org/gitlab/logicmoo/logicmoo_workspace/-/blob/013514de819eead21c818af170c91f9052a89466/packs_sys/logicmoo_base/t/examples/fol/family_regress_01.pfc.pl 
GITHUB: https://github.com/logicmoo/logicmoo_workspace/commit/013514de819eead21c818af170c91f9052a89466 


#import: written-on(word,paper).


my-minus-one(N,M) <gt;->  (N > 1)  &  (M = N-1)


legal-pad(paper) <gt;-> min-elements(1, paper)

exactly-n-elements(1,paper) <gt;->
(exists paper word.  
    (   written-on(word,paper) 
      & ~(exists other-word.
           (  written-on(other-word,paper) 
             & ~same(other-word,word)))))

exactly-n-elements(2,paper) <gt;->
(exists paper word1 word2. 
  (  written-on(word1,paper) 
   & written-on(word2,paper) 
   & ~same(word1,word2)   
   & ~ (exists other-word. 
         (   written-on(other-word,paper) 
          & ~same(other-word,word1) 
          & ~same(other-word,word2)))))

exactly-n-elements(N,paper) <gt;-> 
   range-elements(N,N,paper)  

range-elements(N,M,paper) <gt;-> 
 (exists paper.
  ( min-elements(N,paper) 
    & max-elements(M,paper)))

min-elements(1,paper) <gt;-> 
 (exists paper word1.
     (written-on(word1,paper)))

min-elements(2,paper) <gt;->
 (exists paper word1 word2. 
   (  written-on(word1,paper) 
    & written-on(word2,paper)
    & ~same(word1,word2)))

max-elements(2,paper) <gt;->  
(exists paper word1 word2. 
   (  written-on(word1,paper) 
    & written-on(word2,paper) 
    &  ~(exists other-word.
          (  written-on(other-word,paper) 
            & ~same(other-word,word1)
            & ~same(other-word,word2)))))

% exists a paper with no elements
exactly-n-elements(0,paper) <gt;->
  (exists paper
     ~(exists word1. written-on(word1,paper)))

max-elements(1,paper) <gt;->
 exactly-n-elements(0,paper) v exactly-n-elements(1,paper)

containsAtLeastOneUnique(paper1,paper2) <gt;->
  (exists word. (written-on(word,paper1) -> ~written-on(word,paper2)))

disjoint(paper1,paper2) <gt;->
  ~(exists word. (written-on(word,paper1) & written-on(word,paper2)))

subset(paper1,paper2) <gt;-> 
    (forall word.
      written-on(word,paper1) -> written-on(word,paper2) )

union(paper1,paper2,paper) <gt;->
 (forall word.
   (written-on(word,paper) <gt;-> 
       (written-on(word,paper1) v written-on(word,paper2))))

union(paper1,paper2,paper) <gt;->
  (exists scratchpad. 
      union(paper1,paper2,scratchpad)
     & ~containsAtLeastOneUnique(paper,scratchpad))


union-disjoint(paper1,paper2,paper) <gt;-> 
   (   union(paper1,paper2,paper) 
     & disjoint(paper1,paper2))


min-elements(4,paper) <gt;-> 
  (exists paper1 paper2.
     min-elements(2,paper1) 
   & min-elements(2,paper2)
   & union-disjoint(paper1,paper2))

min-elements(N,paper) <gt;-> 
  (exists paper1 paper2.
     min-elements(1,paper1) 
   & min-elements(M,paper2)
   & legal-pad(paper2)
   & union-disjoint(paper1,paper2)
   & my-minus-one(N,M))


max-elements(N,paper) <gt;-> 
  (exists paper1 paper2.
     max-elements(1,paper1) 
   & max-elements(M,paper2)
   & legal-pad(paper2)
   & union-disjoint(paper1,paper2)
   & my-minus-one(N,M))


equal_papers_v2(paper1,paper2) <gt;->
   ( ~containsAtLeastOneUnique(paper1,paper2)
     & ~containsAtLeastOneUnique(paper2,paper1)
     & legal-pad(paper1)
     & legal-pad(paper2))

equal_papers_v1(paper1,paper2) <gt;->
 ( legal-pad(paper1)
   & (forall word. 
      (written-on(word,paper1) <gt;-> written-on(word,paper2))))



*/


:- debug_logicmoo(_).
/*~
~*/

:- nodebug_logicmoo(http(_)).

/*~
~*/


:- expects_dialect(pfc).


/*~
~*/



house(red_house).
/*~
~*/

house(blue_house).
% house(green_house).

/*~
~*/

% house(green_house).

:- must((existing_count(X,house(X),EC),EC==2)).

/*~
%~ ?-( mpred_test( "Test_0001_Line_0000__house_1",
%~       baseKB : existing_count(X,house(X),EC),EC==2)).
%~ make_dynamic_here(baseKB,existing_count(_496,house(_496),_500))
failure=info((why_was_true(baseKB:(\+ (existing_count(_496,house(_496),_500),_500==2))),nop(ftrace(baseKB:(existing_count(_496,house(_496),_500),_500==2)))))
no_proof_for(\+ (existing_count(House,house(House),Count),Count==2)).

no_proof_for(\+ (existing_count(House,house(House),Count),Count==2)).

no_proof_for(\+ (existing_count(House,house(House),Count),Count==2)).

	name	=	'logicmoo.base.examples.fol.FOL_CARDINAITY_AXIOMITIZED_01-Test_0001_Line_0000__house_1'. 
	JUNIT_CLASSNAME	=	'logicmoo.base.examples.fol.FOL_CARDINAITY_AXIOMITIZED_01'. 
	JUNIT_CMD	=	'timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'fol_cardinaity_axiomitized_01.pfc.pl\']"'. 
% saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace@2/test_results/jenkins/Report-logicmoo-base-examples-fol-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_examples_fol_FOL_CARDINAITY_AXIOMITIZED_01_Test_0001_Line_0000_house_1-junit.xml
~*/


singleValuedInArg(existing_count,1).

/*~
~*/


exists_count(3,X,house(X)).

/*~
~*/


exists_count(N,X,G),{(need_plugs(X,G,EP); EP=0),existing_count(X,G,EC),Need is N-(EC-EP), copy_term(G,GG)}
  ==>
    (need_plugs(Need,X,G),
    (\+ GG ==> exists_count(N,X,G)),
    (   GG ==> exists_count(N,X,G))).

/*~
~*/


need_plugs(EP,X,G) ==> {between(1,EP,Plug),copy_term(G,GG,_),X=skFn(Plug,GG)},G.

/*~
~*/


:- listing(exists_count).
/*~
%~ skipped( listing(exists_count))
~*/

:- listing(need_plugs).
/*~
%~ skipped( listing(need_plugs))
~*/

:- listing(house).

/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_cardinaity_axiomitized_01.pfc.pl:168 
%~ skipped( listing(house))
~*/


/*

exists_count(3, A, house(A)).


need_plugs(1, A, house(A)).

house(red_house).
house(blue_house).
house(skFn(1, house(_))).

*/



:- must((existing_count(X,house(X),EC),EC==3)).
/*~
%~ ?-( mpred_test( "Test_0002_Line_0000__house_1",
%~       baseKB : existing_count(X,house(X),EC),EC==3)).
failure=info((why_was_true(baseKB:(\+ (existing_count(_552,house(_552),_556),_556==3))),nop(ftrace(baseKB:(existing_count(_552,house(_552),_556),_556==3)))))
no_proof_for(\+ (existing_count(House,house(House),Count),Count==3)).

no_proof_for(\+ (existing_count(House,house(House),Count),Count==3)).

no_proof_for(\+ (existing_count(House,house(House),Count),Count==3)).

	name	=	'logicmoo.base.examples.fol.FOL_CARDINAITY_AXIOMITIZED_01-Test_0002_Line_0000__house_1'. 
	JUNIT_CLASSNAME	=	'logicmoo.base.examples.fol.FOL_CARDINAITY_AXIOMITIZED_01'. 
	JUNIT_CMD	=	'timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'fol_cardinaity_axiomitized_01.pfc.pl\']"'. 
% saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace@2/test_results/jenkins/Report-logicmoo-base-examples-fol-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_examples_fol_FOL_CARDINAITY_AXIOMITIZED_01_Test_0002_Line_0000_house_1-junit.xml
~*/

:- break.

% ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/607
/*~
%~ skipped(blocks_on_input,break)
~*/
%~ unused(no_junit_results)
Test_0001_Line_0000__house_1	result	=	failure. 
Test_0002_Line_0000__house_1	result	=	failure. 

%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_cardinaity_axiomitized_01.pfc.pl:189 
%~ test_completed_exit(8)

totalTime=1.000

FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k fol_cardinaity_axiomitized_01.pfc.pl (returned 8) Add_LABELS='' Rem_LABELS='Skipped,Skipped,Errors,Warnings,Overtime,Skipped'