From 0a002b3201e6308917d4d1837e3ab3fe7f94e883 Mon Sep 17 00:00:00 2001 From: Mark Thom Date: Wed, 7 Oct 2020 17:38:34 -0600 Subject: [PATCH 1/7] add heuristic warning for variables in Naf formulas The heuristic prints a warning to the screen if the variables of a Naf formula do not first appear in non-Naf formulas. The warning condition is detected during schemaless checking. --- .../ruleml/psoa/analyzer/SchemalessChecker.g | 35 +++++++++++++++++-- 1 file changed, 33 insertions(+), 2 deletions(-) diff --git a/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g b/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g index dd0534b..0455cce 100644 --- a/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g +++ b/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g @@ -41,7 +41,10 @@ options private boolean m_forallWrap; private Set m_freeVars = new HashSet(); - private Set m_quantifiedVars = new HashSet(); + private Set m_quantifiedVars = new HashSet(); + private Set m_nonNafVars = new HashSet(); + + private int m_nafLevels = 0; private void recordExistentialVar(Set existVars, String v) { if (!m_quantifiedVars.contains(v)) { @@ -105,6 +108,7 @@ rule { m_hasForall = false; + m_nonNafVars.clear(); m_quantifiedVars.clear(); m_freeVars.clear(); } @@ -175,6 +179,25 @@ scope { ; naf_formula +scope +{ + Set nafVars; +} +@init +{ + ++m_nafLevels; + $naf_formula::nafVars = new HashSet(); +} +@after +{ + --m_nafLevels; + + $naf_formula::nafVars.removeAll(m_nonNafVars); + + if (!$naf_formula::nafVars.isEmpty()) { + printErrln("Warning: Variable(s): ?" + String.join(", ?", $naf_formula::nafVars) + " may not be bound in a conjunct preceding the Naf: \n" + $naf_formula.text + "\n"); + } +} : ^(NAF formula) ; @@ -198,7 +221,15 @@ subclass term : constant - | VAR_ID { if (!$VAR_ID.text.isEmpty() && !m_quantifiedVars.contains($VAR_ID.text)) m_freeVars.add($VAR_ID.text); } + | VAR_ID + { if (!$VAR_ID.text.isEmpty() && !m_quantifiedVars.contains($VAR_ID.text)) + m_freeVars.add($VAR_ID.text); + + if (m_nafLevels > 0) + $naf_formula::nafVars.add($VAR_ID.text); + else if (m_isRuleBody) // never deem variables in rule conclusions as non-NAF variables. + m_nonNafVars.add($VAR_ID.text); + } | psoa | external ; From a598be030bb49ba0085c563121fdd02912828136 Mon Sep 17 00:00:00 2001 From: Mark Thom Date: Tue, 13 Oct 2020 16:18:24 -0600 Subject: [PATCH 2/7] add warning for rule conclusion variables appearing in Naf formulas that do not precede the formulas in non-Naf condition formulas --- .../org/ruleml/psoa/analyzer/SchemalessChecker.g | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g b/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g index 0455cce..446e8fc 100644 --- a/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g +++ b/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g @@ -43,6 +43,7 @@ options private Set m_freeVars = new HashSet(); private Set m_quantifiedVars = new HashSet(); private Set m_nonNafVars = new HashSet(); + private Set m_headVars = new HashSet(); private int m_nafLevels = 0; @@ -111,6 +112,7 @@ rule m_nonNafVars.clear(); m_quantifiedVars.clear(); m_freeVars.clear(); + m_headVars.clear(); } @after { @@ -193,6 +195,11 @@ scope --m_nafLevels; $naf_formula::nafVars.removeAll(m_nonNafVars); + $naf_formula::nafVars.removeAll(m_headVars); + + if (!m_nonNafVars.containsAll(m_headVars)) { + printErrln("Warning: Conclusion variable(s): ?" + String.join(", ?", m_headVars) + " do(es) not appear in a conjunct preceding the Naf: \n" + $naf_formula.text + "\n"); + } if (!$naf_formula::nafVars.isEmpty()) { printErrln("Warning: Variable(s): ?" + String.join(", ?", $naf_formula::nafVars) + " may not be bound in a conjunct preceding the Naf: \n" + $naf_formula.text + "\n"); @@ -224,11 +231,13 @@ term | VAR_ID { if (!$VAR_ID.text.isEmpty() && !m_quantifiedVars.contains($VAR_ID.text)) m_freeVars.add($VAR_ID.text); - + if (m_nafLevels > 0) $naf_formula::nafVars.add($VAR_ID.text); else if (m_isRuleBody) // never deem variables in rule conclusions as non-NAF variables. m_nonNafVars.add($VAR_ID.text); + else + m_headVars.add($VAR_ID.text); } | psoa | external From b7163180ec6a36da06a8d45660f3a8906082b5ff Mon Sep 17 00:00:00 2001 From: Mark Thom Date: Wed, 14 Oct 2020 16:38:02 -0600 Subject: [PATCH 3/7] change conclusion variable warning message, only about conclusion variables contained in Naf formulas only --- .../org/ruleml/psoa/analyzer/SchemalessChecker.g | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g b/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g index 446e8fc..d661775 100644 --- a/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g +++ b/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g @@ -194,15 +194,19 @@ scope { --m_nafLevels; - $naf_formula::nafVars.removeAll(m_nonNafVars); - $naf_formula::nafVars.removeAll(m_headVars); + HashSet headNafVars = new HashSet(m_headVars); + headNafVars.retainAll($naf_formula::nafVars); - if (!m_nonNafVars.containsAll(m_headVars)) { - printErrln("Warning: Conclusion variable(s): ?" + String.join(", ?", m_headVars) + " do(es) not appear in a conjunct preceding the Naf: \n" + $naf_formula.text + "\n"); + if (!m_nonNafVars.containsAll(headNafVars)) { + headNafVars.removeAll(m_nonNafVars); + printErrln("Warning: Conclusion variable(s): ?" + String.join(", ?", headNafVars) + " do(es) not appear in a conjunct preceding the Naf: \n" + $naf_formula.text + "\n"); } + $naf_formula::nafVars.removeAll(m_nonNafVars); + $naf_formula::nafVars.removeAll(m_headVars); + if (!$naf_formula::nafVars.isEmpty()) { - printErrln("Warning: Variable(s): ?" + String.join(", ?", $naf_formula::nafVars) + " may not be bound in a conjunct preceding the Naf: \n" + $naf_formula.text + "\n"); + printErrln("Warning: Variable(s): ?" + String.join(", ?", $naf_formula::nafVars) + " is not bound in a conjunct preceding the Naf: \n" + $naf_formula.text + "\n"); } } : ^(NAF formula) From c13503cdda1ca2404e6b3c030d84546479306113 Mon Sep 17 00:00:00 2001 From: Mark Thom Date: Fri, 16 Oct 2020 13:28:26 -0600 Subject: [PATCH 4/7] edit Warning messages about possibly floundering variables in Naf formulas to be more descriptive --- .../antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g b/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g index d661775..e8b1d43 100644 --- a/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g +++ b/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g @@ -199,14 +199,19 @@ scope if (!m_nonNafVars.containsAll(headNafVars)) { headNafVars.removeAll(m_nonNafVars); - printErrln("Warning: Conclusion variable(s): ?" + String.join(", ?", headNafVars) + " do(es) not appear in a conjunct preceding the Naf: \n" + $naf_formula.text + "\n"); + printErrln("Warning: Conclusion variable(s): ?" + String.join(", ?", headNafVars) + "\n" + + "do(es) not occur in a conjunct preceding the Naf, which should be instantiated " + + "to prevent floundering: \n" + $naf_formula.text + "\n"); } $naf_formula::nafVars.removeAll(m_nonNafVars); $naf_formula::nafVars.removeAll(m_headVars); if (!$naf_formula::nafVars.isEmpty()) { - printErrln("Warning: Variable(s): ?" + String.join(", ?", $naf_formula::nafVars) + " is not bound in a conjunct preceding the Naf: \n" + $naf_formula.text + "\n"); + + printErrln("Warning: Variable(s): ?" + String.join(", ?", $naf_formula::nafVars) + "\n" + + "do(es) not occur in a conjunct preceding the Naf, which should be instantiated " + + "to prevent floundering: \n" + $naf_formula.text + "\n"); } } : ^(NAF formula) From a7e592d0362e2f77c1d67eb49f630001f7a961cf Mon Sep 17 00:00:00 2001 From: Mark Thom Date: Tue, 20 Oct 2020 14:52:44 -0600 Subject: [PATCH 5/7] add special Finding for anonymous variables in Naf formulas --- .../ruleml/psoa/analyzer/SchemalessChecker.g | 29 ++++++++++++++----- 1 file changed, 21 insertions(+), 8 deletions(-) diff --git a/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g b/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g index e8b1d43..6cb5bae 100644 --- a/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g +++ b/PSOACore/src/main/antlr3/org/ruleml/psoa/analyzer/SchemalessChecker.g @@ -105,8 +105,13 @@ query ; rule +scope +{ + String text; +} @init { + $rule::text = $rule.text; m_hasForall = false; m_nonNafVars.clear(); @@ -184,11 +189,13 @@ naf_formula scope { Set nafVars; + boolean containsAnonymousVariables; } @init { ++m_nafLevels; $naf_formula::nafVars = new HashSet(); + $naf_formula::containsAnonymousVariables = false; } @after { @@ -201,17 +208,20 @@ scope headNafVars.removeAll(m_nonNafVars); printErrln("Warning: Conclusion variable(s): ?" + String.join(", ?", headNafVars) + "\n" + "do(es) not occur in a conjunct preceding the Naf, which should be instantiated " + - "to prevent floundering: \n" + $naf_formula.text + "\n"); + "to prevent floundering: \n" + $rule::text + "\n"); } $naf_formula::nafVars.removeAll(m_nonNafVars); $naf_formula::nafVars.removeAll(m_headVars); if (!$naf_formula::nafVars.isEmpty()) { - - printErrln("Warning: Variable(s): ?" + String.join(", ?", $naf_formula::nafVars) + "\n" + - "do(es) not occur in a conjunct preceding the Naf, which should be instantiated " + - "to prevent floundering: \n" + $naf_formula.text + "\n"); + printErrln("Finding: Variable(s): ?" + String.join(", ?", $naf_formula::nafVars) + "\n" + + "do(es) not occur in a conjunct preceding the Naf: \n" + $rule::text + "\n"); + } + + if ($naf_formula::containsAnonymousVariables) { + printErrln("Finding: A Naf in the rule: \n" + $rule::text + "\n" + + "contains an anonymous variable.\n"); } } : ^(NAF formula) @@ -240,10 +250,13 @@ term | VAR_ID { if (!$VAR_ID.text.isEmpty() && !m_quantifiedVars.contains($VAR_ID.text)) m_freeVars.add($VAR_ID.text); - + if (m_nafLevels > 0) - $naf_formula::nafVars.add($VAR_ID.text); - else if (m_isRuleBody) // never deem variables in rule conclusions as non-NAF variables. + if ($VAR_ID.text.isEmpty()) + $naf_formula::containsAnonymousVariables = true; + else + $naf_formula::nafVars.add($VAR_ID.text); + else if (m_isRuleBody) // Non-empty difference of Naf variables with union of head and pre-Naf-condition variables m_nonNafVars.add($VAR_ID.text); else m_headVars.add($VAR_ID.text); From c2e36f495ff1c2b3116ed5ee3c793e0f91fa5e68 Mon Sep 17 00:00:00 2001 From: Mark Thom Date: Tue, 20 Oct 2020 14:55:51 -0600 Subject: [PATCH 6/7] add comment in naf_trivia_query1.psoa explaining the query fails for earlier versions of the SWI Prolog backend --- PSOATransRun/test-basic/test-naf/naf_trivia/naf_trivia-KB.psoa | 2 +- .../test-basic/test-naf/naf_trivia/naf_trivia-query1.psoa | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/PSOATransRun/test-basic/test-naf/naf_trivia/naf_trivia-KB.psoa b/PSOATransRun/test-basic/test-naf/naf_trivia/naf_trivia-KB.psoa index 6b66d7d..7336aba 100644 --- a/PSOATransRun/test-basic/test-naf/naf_trivia/naf_trivia-KB.psoa +++ b/PSOATransRun/test-basic/test-naf/naf_trivia/naf_trivia-KB.psoa @@ -15,7 +15,7 @@ RuleML( Forall ?X ?Y ( greater-than-or-equal(?X ?Y) :- - Naf(pred:numeric-less-than(?X ?Y)) + Naf(External(pred:numeric-less-than(?X ?Y))) ) Forall ?X ( diff --git a/PSOATransRun/test-basic/test-naf/naf_trivia/naf_trivia-query1.psoa b/PSOATransRun/test-basic/test-naf/naf_trivia/naf_trivia-query1.psoa index 266018a..24d5f03 100644 --- a/PSOATransRun/test-basic/test-naf/naf_trivia/naf_trivia-query1.psoa +++ b/PSOATransRun/test-basic/test-naf/naf_trivia/naf_trivia-query1.psoa @@ -1,4 +1,7 @@ % Two queries of two query files merged into one conjunction of one query file % to avoid possible order dependency w.r.t. answers % containing free variables coded as Var0, Var1, ... values + +% This query does not work as expected under SWI Prolog version 7.6.4, although +% it does work correctly on version 7.7.15. And(unifiable(?X1 ?Y1) check_unifiability_without_unifying(?X2 ?Y2)) From da29c0633ad48935d8a998dbccc0c22eaa3f1232 Mon Sep 17 00:00:00 2001 From: Mark Thom Date: Tue, 20 Oct 2020 15:22:31 -0600 Subject: [PATCH 7/7] add further systematic and exploratory naf tests --- .../naf_psoa_premise/naf_psoa_premise-KB.psoa | 314 +++++++++++ .../naf_psoa_premise-answer1.psoa | 1 + .../naf_psoa_premise-answer2.psoa | 1 + .../naf_psoa_premise-answer3.psoa | 1 + .../naf_psoa_premise-answer4.psoa | 1 + .../naf_psoa_premise-answer5.psoa | 1 + .../naf_psoa_premise-query1.psoa | 1 + .../naf_psoa_premise-query2.psoa | 1 + .../naf_psoa_premise-query3.psoa | 1 + .../naf_psoa_premise-query4.psoa | 1 + .../naf_psoa_premise-query5.psoa | 1 + .../naf_psoa_query/naf_psoa_query-KB.psoa | 513 ++++++++++++++++++ .../naf_psoa_query-answer1.psoa | 1 + .../naf_psoa_query-answer2.psoa | 1 + .../naf_psoa_query-answer3.psoa | 1 + .../naf_psoa_query-answer4.psoa | 1 + .../naf_psoa_query-answer5.psoa | 1 + .../naf_psoa_query-answer6.psoa | 1 + .../naf_psoa_query/naf_psoa_query-query1.psoa | 1 + .../naf_psoa_query/naf_psoa_query-query2.psoa | 1 + .../naf_psoa_query/naf_psoa_query-query3.psoa | 1 + .../naf_psoa_query/naf_psoa_query-query4.psoa | 1 + .../naf_psoa_query/naf_psoa_query-query5.psoa | 1 + .../naf_psoa_query/naf_psoa_query-query6.psoa | 1 + .../naf_relationship_premise-KB.psoa | 99 ++++ .../naf_relationship_premise-answer1.psoa | 1 + .../naf_relationship_premise-answer2.psoa | 1 + .../naf_relationship_premise-answer3.psoa | 1 + .../naf_relationship_premise-answer4.psoa | 1 + .../naf_relationship_premise-answer5.psoa | 1 + .../naf_relationship_premise-answer6.psoa | 1 + .../naf_relationship_premise-query1.psoa | 1 + .../naf_relationship_premise-query2.psoa | 1 + .../naf_relationship_premise-query3.psoa | 1 + .../naf_relationship_premise-query4.psoa | 1 + .../naf_relationship_premise-query5.psoa | 1 + .../naf_relationship_premise-query6.psoa | 1 + 37 files changed, 960 insertions(+) create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-KB.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer1.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer2.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer3.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer4.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer5.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query1.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query2.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query3.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query4.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query5.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-KB.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer1.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer2.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer3.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer4.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer5.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer6.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query1.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query2.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query3.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query4.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query5.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query6.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-KB.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer1.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer2.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer3.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer4.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer5.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer6.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query1.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query2.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query3.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query4.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query5.psoa create mode 100644 PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query6.psoa diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-KB.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-KB.psoa new file mode 100644 index 0000000..f532d8c --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-KB.psoa @@ -0,0 +1,314 @@ +RuleML( + Assert( + + /* + Selection of Explored Psoa Atoms in (Rule) Premises Already in PSOATransRun 1.5.1 + */ + + % Shelfships + q_ss(-[sr1 tr1]) + q_ss(-[sr2 tr1]) + + Forall ?x ( + p_ss(-[tr1 ?x]) :- And(?x=sr1 Naf(q_ss(-[?x tr1]))) + ) + + p1_ss(-[s1 t1] -[s2 t2 u2]) + p2_ss(-[s1 t1 u1]) + p3_ss(-[#p4_ss(-[s]) #p5_ss(-[t])]) + + p5_ss(-[s1 t1] -[s2 t2 u2]) + + Forall ?x ( + p4_ss(-[?x s1] -[t2 ?x u2]) :- Or(And(p5_ss(-[s1 ?x]) Naf(p5_ss(-[?x t2 u2]))) + And(p5_ss(-[?x t2 u2]) Naf(p5_ss(-[s1 ?x])))) + ) + + % Queries: + % p_ss(-[tr1 ?x]) % No + % p_ss(-[tr1 sr2]) % No + % p4_ss(-[?x s1] -[t2 ?y u2]) % Yes + % p4_ss(-[?x s1] -[t2 ?x u2]) % Yes + % p4_ss(-[?x s1]) % Yes + % p4_ss(-[t2 ?x u2]) % Yes + % p4_ss(-[t3 ?x u2]) % No + % p4_ss(-[s2 s1]) % Yes + + + % Shelfpoints + o_sp#q_sp(-[s1 t1]) + + Forall ?o ?x ( + ?o#p_sp(-[t1 ?x]) :- ?o#q_sp(-[?x t1]) + ) + + Forall ?t2 ( + o_sp#p1_sp(-[s1 ?t2]) + ) + + o_sp#p1_sp(-[s1 t2]) + o_sp#p1_sp(-[t2 s1]) + o_sp#p1_sp(-[s1 t1] -[s2 t2 u2]) + + Forall ?o1 ?s1 ?t1 ( + ?o1#p1_sp(-[?s1 ?t1 u1]) :- + And(?o1#p_sp(-[?s1 ?t1]) + Naf(?o1#p1_sp(-[?t1 ?s1]))) + ) + + % Queries: + % ?o1#p1_sp(-[?s1 ?t1]) % Yes + % ?o1#p1_sp(-[?s1 ?t1 u1]) % No + % ?o1#p1_sp(-[?s1 ?t1 u3]) % No + % o_sp#p1_sp % Yes + % o_sp1#p1_sp % No + + + % Frameships + q_fs(sps1->tps1) + + Forall ?x ( + p_fs(tps1->?x) :- q_fs(?x->tps1) + ) + + p2_fs(s1->f1) + p2_fs(s1->#p4_fs()) + p2_fs(s1->#p5_fs()) + + Forall ?s1 ?f1 ?o ( + p1_fs(?s1->f1 s2->f2 s3->?o) :- + And(p2_fs(?s1->?o) + Naf(p_fs(?s1->f1))) + ) + + % Queries: + % p1_fs(?s1->f1) % Yes + % p1_fs(s1->f1) % Yes + % p1_fs(s2->f1) % No + % p1_fs(s1->?f1) % Yes + % p1_fs(s3->f1) % Yes + % p1_fs(s3->?o) % Yes + % p1_fs(s1->?f1 s3->?f1) % Yes + % p1_fs(s1->?f1 s4->?f1) % No + + + % Framepoints + o_fp#q_fp(sp1->tp1) + + Forall ?o ?x ( + ?o#p_fp(tp1->?x) :- ?o#q_fp(?x->tp1) + ) + + Forall ?o1 ?o2 ?s1 ?f1 ( + ?o1#p1_fp(?s1->?f1) :- + And(?o1#p2_fs(?s1->?f1) + Naf(?o1#p_fp(?s1->#p3_fs()))) + ) + + % Queries: + % ?o1#p1_fp % Yes + % ?o1#p1_fp(?s1->?f1) % Yes + % ?o1#p1_fp(?s1->f2) % No + % ?o1#p1_fp(s3->?f3) % No + + + % Shelframeships + p1_sfs(-[t1 u1] s1->f1 -[t2 u2 v2] s2->f2) + + Forall ?o1_sfs ( + ?o1_sfs#p2_sfs(s1->f1 -[s1 t1]) :- ?o1_sfs#p3_sfs + ) + + o1_sfs#p3_sfs + q_sfs(-[s1 t1] s1->f1) + + Forall ?x ?v ( + p_sfs(-[t1 ?x] s1->?v) :- + And(p1_sfs(-[?x u1] s2->?v) + Naf(q_sfs(-[?x t1] s1->?v))) + ) + + % Queries: + % p_sfs(-[t1 ?x] s1->?v) % Yes + % p_sfs(-[t2 ?x] s1->?v) % No + + + % Shelframepoints + o1_sfp#p1_sfp(-[t1 u1] -[t1 s1] s1->f1 -[t2 u2 v2] s2->f2) + o1_sfp#p1_sfp(-[t1 s1] -[t1 u1] s1->f1) + + Forall ?o1 ?s1 ?u2 ( + ?o1#p1_sfp(-[t1 u1] ?s1->f1 -[t2 ?u2 v2] s2->f2) :- + And(?o1#p1_sfp(?s1->f1) + ?o1#p1_sp(-[?s1 t1 u1])) + ) + + o_sfp#q_sfp(-[s1 t1] s1->f1) + + Forall ?o ?x ?v ( + ?o#p_sfp(-[t1 ?x] s1->?v) :- + And(?o#q_sfp(-[?x t1] s1->?v) + Naf(o1_sfp#p1_sfp(-[t1 ?x] s1->?v))) + ) + + % Queries: + % ?o#p_sfp(-[t1 ?x] s1->?v) % No + % ?o#q_sfp(-[?x t1] s1->?v) % Yes + % And(o1_sfp#p1_sfp(-[t1 ?x] -[t1 u1] s1->?v) ?o#p_sfp(-[t1 ?x] s1->?v)) % No + % And(?o#q_sfp(-[?x t1] s1->?v) ?o#p_sfp(-[t1 ?x] s1->?v)) % No + + + % Relationships + q_rs(+[sr1 tr1]) + q_rs(+[sr2 tr1]) + + Forall ?x ( + p_rs(+[tr1 ?x]) :- And(?x=sr1 Naf(q_rs(+[?x tr1]))) + ) + + p1_rs(+[s1 t1] +[s2 t2 u2]) + p2_rs(+[s1 t1 u1]) + p3_rs(+[#p4_rs(+[s]) #p5_rs(+[t])]) + + p5_rs(+[s1 t1] +[s2 t2 u2]) + + Forall ?x ( + p4_rs(+[?x s1] +[t2 ?x u2]) :- Or(And(p5_rs(+[s1 ?x]) Naf(p5_rs(+[?x t2 u2]))) + And(p5_rs(+[?x t2 u2]) Naf(p5_rs(+[s1 ?x])))) + ) + + % Queries: + % p_rs(+[tr1 ?x]) % No + % p_rs(+[tr1 sr2]) % No + % p4_rs(+[?x s1] +[t2 ?y u2]) % Yes + % p4_rs(+[?x s1] +[t2 ?x u2]) % Yes + % p4_rs(+[?x s1]) % Yes + % p4_rs(+[t2 ?x u2]) % Yes + % p4_rs(+[t3 ?x u2]) % No + % p4_rs(+[s2 s1]) % Yes + + + % Relationpoints + o_rrp#q_rrp(+[s1 t1]) + + Forall ?o ?x ( + ?o#p_rrp(+[t1 ?x]) :- ?o#q_rrp(+[?x t1]) + ) + + Forall ?t2 ( + o_rrp#p1_rrp(+[s1 ?t2]) + ) + + o_rrp#p1_rrp(+[s1 t2]) + o_rrp#p1_rrp(+[t2 s1]) + o_rrp#p1_rrp(+[s1 t1] +[s2 t2 u2]) + + Forall ?o1 ?s1 ?t1 ( + ?o1#p1_rrp(+[?s1 ?t1 u1]) :- + And(?o1#p_rrp(+[?s1 ?t1]) + Naf(?o1#p1_rrp(+[?t1 ?s1]))) + ) + + % Queries: + % ?o1#p1_rrp(+[?s1 ?t1]) % Yes + % ?o1#p1_rrp(+[?s1 ?t1 u1]) % No + % ?o1#p1_rrp(+[?s1 ?t1 u3]) % No + % o_rrp#p1_rrp % Yes + % o_rrp1#p1_rrp % No + + + % Pairships + q_ps(sps1+>tps1) + + Forall ?x ( + p_ps(tps1+>?x) :- q_ps(?x+>tps1) + ) + + p2_ps(s1+>f1) + p2_ps(s1+>#p4_ps()) + p2_ps(s1+>#p5_ps()) + + Forall ?s1 ?f1 ?o ( + p1_ps(?s1+>f1 s2+>f2 s3+>?o) :- + And(p2_ps(?s1+>?o) + Naf(p_ps(?s1+>f1))) + ) + + % Queries: + % p1_ps(?s1+>f1) % Yes + % p1_ps(s1+>f1) % Yes + % p1_ps(s2+>f1) % No + % p1_ps(s1+>?f1) % Yes + % p1_ps(s3+>f1) % Yes + % p1_ps(s3+>?o) % Yes + % p1_ps(s1+>?f1 s3+>?f1) % Yes + % p1_ps(s1+>?f1 s4+>?f1) % No + + + % Pairpoints + o_pp#q_pp(sp1+>tp1) + + Forall ?o ?x ( + ?o#p_pp(tp1+>?x) :- ?o#q_pp(?x+>tp1) + ) + + Forall ?o1 ?o2 ?s1 ?f1 ( + ?o1#p1_pp(?s1+>?f1) :- + And(?o1#p2_ps(?s1+>?f1) + Naf(?o1#p_pp(?s1+>#p3_fs()))) + ) + + % Queries: + % ?o1#p1_pp % Yes + % ?o1#p1_pp(?s1+>?f1) % Yes + % ?o1#p1_pp(?s1+>f2) % No + % ?o1#p1_pp(s3+>?f3) % No + + + % Relpairships + p1_rps(+[t1 u1] s1+>f1 +[t2 u2 v2] s2+>f2) + + Forall ?o1_rps ( + ?o1_rps#p2_rps(s1+>f1 +[s1 t1]) :- ?o1_rps#p3_rps + ) + + o1_rps#p3_rps + q_rps(+[s1 t1] s1+>f1) + + Forall ?x ?v ( + p_rps(+[t1 ?x] s1+>?v) :- + And(p1_rps(+[?x u1] s2+>?v) + Naf(q_rps(+[?x t1] s1+>?v))) + ) + + % Queries: + % p_rps(+[t1 ?x] s1+>?v) % Yes + % p_rps(+[t2 ?x] s1+>?v) % No + + + % Relpairpoints + o1_rpps#p1_rpps(+[t1 u1] +[t1 s1] s1+>f1 +[t2 u2 v2] s2+>f2) + o1_rpps#p1_rpps(+[t1 s1] +[t1 u1] s1+>f1) + + Forall ?o1 ?s1 ?u2 ( + ?o1#p1_rpps(+[t1 u1] ?s1+>f1 +[t2 ?u2 v2] s2+>f2) :- + And(?o1#p1_rpps(?s1+>f1) + ?o1#p1_rrp(+[?s1 t1 u1])) + ) + + o_rpps#q_rpps(+[s1 t1] s1+>f1) + + Forall ?o ?x ?v ( + ?o#p_rpps(+[t1 ?x] s1+>?v) :- + And(?o#q_rpps(+[?x t1] s1+>?v) + Naf(o1_rpps#p1_rpps(+[t1 ?x] s1+>?v))) + ) + + % Queries: + % ?o#p_rpps(+[t1 ?x] s1+>?v) % No + % ?o#q_rpps(+[?x t1] s1+>?v) % Yes + % And(o1_rpps#p1_rpps(+[t1 ?x] +[t1 u1] s1+>?v) ?o#p_rpps(+[t1 ?x] s1+>?v)) % No + % And(?o#q_rpps(+[?x t1] s1+>?v) ?o#p_rpps(+[t1 ?x] s1+>?v)) % No + + ) +) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer1.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer1.psoa new file mode 100644 index 0000000..0a25ee5 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer1.psoa @@ -0,0 +1 @@ +?f1=_f1 ?f2=_f2 diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer2.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer2.psoa new file mode 100644 index 0000000..cf45697 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer2.psoa @@ -0,0 +1 @@ +No diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer3.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer3.psoa new file mode 100644 index 0000000..aecbdd8 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer3.psoa @@ -0,0 +1 @@ +?s1=_s1 diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer4.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer4.psoa new file mode 100644 index 0000000..c06da67 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer4.psoa @@ -0,0 +1 @@ +?x=_t1 ?s1=_s1 ?v=_f2 diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer5.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer5.psoa new file mode 100644 index 0000000..cf45697 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-answer5.psoa @@ -0,0 +1 @@ +No diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query1.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query1.psoa new file mode 100644 index 0000000..05f6da7 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query1.psoa @@ -0,0 +1 @@ +p1_ps(s1+>?f1 s2+>?f2) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query2.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query2.psoa new file mode 100644 index 0000000..e56987d --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query2.psoa @@ -0,0 +1 @@ +p_ss(-[tr1 sr3]) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query3.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query3.psoa new file mode 100644 index 0000000..abc95e0 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query3.psoa @@ -0,0 +1 @@ +p1_fp(?s1->f1) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query4.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query4.psoa new file mode 100644 index 0000000..eb8157b --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query4.psoa @@ -0,0 +1 @@ +p_sfs(-[t1 ?x] ?s1->?v) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query5.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query5.psoa new file mode 100644 index 0000000..4fd2e8b --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_premise/naf_psoa_premise-query5.psoa @@ -0,0 +1 @@ +p_sfs(-[t1 ?x] s2->?v) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-KB.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-KB.psoa new file mode 100644 index 0000000..40d1b95 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-KB.psoa @@ -0,0 +1,513 @@ +RuleML ( + Assert ( + + % Testing the Naf_Psoa_Query Systematics + + %% TODO: + + % 1. Write commit message for first disjunct (TL). + + /* 1. + + add instructive examples of top-level Naf queries, including several + entailing unexpected/undesired behavior + + */ + + % 2. Farm out several of these queries to queryN/answerN pairs. (DONE) + % 3. Move this file into the test suite as a -KB file, + % under a folder designated as applying to the first disjunct. (DONE) + + + /* + Independent Atoms + */ + + % Shelfships + q_ss(-[sr1 tr1]) + + Forall ?x ( + p_ss(-[tr1 ?x]) :- q_ss(-[?x tr1]) + ) + + p1_ss(-[s1 t1] -[s2 t2 u2]) + p2_ss(-[s1 t1 u1]) + p3_ss(-[#p4_ss(-[s]) #p5_ss(-[t])]) + + Forall ?x ?y ( + p4_ss(-[?x s1] -[t2 ?y u2]) :- p5_ss(-[s1 ?x] -[?y t2 u2]) + ) + + p5_ss(-[s1 t1] -[s2 t2 u2]) + + Forall ?v1 ?v2 ?v3 ( + p6_ss(-[?v1 ?v2 ?v3]) :- p7_ss(-[?v1 ?v2 ?v3]) + ) + + p7_ss(-[a1 b1 c1]) + + % Queries: + % Naf(q_ss(-[sr1 tr1])) % No + % Naf(q_ss(-[sr1 tr2])) % Yes + % Naf(p_ss(-[tr1 sr1])) % No + % Naf(p_ss(-[tr1 sr2])) % Yes + % Naf(p3_ss(-[a1 b1 b1])) % Yes + % Naf(p3_ss(-[a1 b1 c1])) % Yes + % Naf( p4_ss(-[t1 s1] -[t2 s2 u2]) ) % No + % Naf( p4_ss(-[t1 s1] -[t2 s2 u3]) ) % Yes + % Naf( p4_ss(-[t1 s1] -[t2 s3 u2]) ) % Yes + % Naf( p6_ss(-[a1 b1 c1]) ) % No + % Naf( p1_ss(-[s1 t1] -[s2 t2 u2]) ) % No + % Naf( p1_ss(-[s1 t1] -[s2 ?t2 u3]) ) % Yes, ?t2 free + % Naf( p1_ss(-[s1 t1] -[s2 ?t2 u2]) ) % No + % Naf( p1_ss(-[s1 t1] -[s2 t2 u2]) ) % No + % Naf( p1_ss(-[s1 t1] -[s2 ?t2 u3]) ) % Yes, ?t2 free + % Naf( Naf( p1_ss(-[?s1 t1] -[s2 ?t2 u2]) ) ) % Yes, ?s1, ?t2 free + % Naf( Exists ?s ( p2_ss(-[?s t1 u1]) ) ) % No + % Naf( Exists ?s ( p2_ss(-[?s t1 u2]) ) ) % Yes + % Exists ?s ( Naf( p2_ss(-[?s t1]) ) ) % Yes + % Naf( p2_ss(-[s1 t1 u1]) ) % No + % Naf( p2_ss(-[s1 t1 u2] ) ) % Yes + % Naf( p3_ss(-[#p4_ss(-[s]) #p5_ss(-[t])]) ) % No + % Naf( p3_ss(-[#p4_ss(-[s]) #p5_ss(-[t]) #p6_ss()]) ) % Yes + % Naf( And(p3_ss(-[#p4_ss(-[s])]) p3_ss(-[#p6_ss()])) ) % Yes + % Naf( Or(p3_ss(-[#p4_ss(-[s])]) p3_ss(-[#p6_ss()])) ) % Yes + + + % Shelfpoints + o_sp#q_sp(-[srp1 trp1]) + + Forall ?o ?x ( + ?o#p_sp(-[trp1 ?x]) :- ?o#q_sp(-[?x trp1]) + ) + + o1_sp#p1_sp(-[s1 t1] -[s2 t2 u2]) + + Forall ?o1 ?o2 ?s1 ?t1 ( + ?o1#p1_sp(-[?s1 ?t1 u1]) :- + And( ?o1#p1_fs(s1->f1 -[?s1 ?t1]) + p2_fs(s1->#p3_fs() ?o2->f2) ) + ) + + % Queries: + % Naf(o_sp#q_sp(-[srp1 trp1])) % No + % Naf(o_sp#q_sp(-[srp1 trp3])) % Yes + % Naf(o_sp#p_sp(-[trp1 srp1])) % No + % Naf(o_sp#p_sp(-[trp1 srp2])) % Yes + % Naf(?o1#p1_sp) % No + + % And(?o1#p1_sp ?o1#Top(-[?s1 ?t1 ?]) Naf(?o1#p1_sp(-[?s1 ?t1 u1]))) % Yes + + % Naf( o1_sp#p1_sp(-[s1 t1]) ) % No + % Naf( o1_sp#p1_sp(-[s1 t1] -[s2 t2 u2]) ) % No + % Naf( #p1_sp(-[s1 t1]) ) % No + % Naf( #p1_sp(-[t1 u1]) ) % Yes + % Naf( #p1_sp(-[s1 t2]) ) % Yes + % Naf( ?o#p1_sp ) % No + % Naf( o1_sp#p1_sp) % No + % Naf( o1_sp#p1_sp(-[s1 t1]) ) % No + % Naf( o2_sp#p1_sp(-[s1 t1]) ) % Yes + + + % Frameships + q_fs(sps1->tps1) + + Forall ?x ( + p_fs(tps1->?x) :- q_fs(?x->tps1) + ) + + p1_fs(s1->f1 s2->f2) + p2_fs(s1->f1) + p3_fs(s1->#p4_fs() #p5_fs->f2) + + p1_fs(s1->f1 s2->f2) :- p2_fs(s1->f1) + p2_fs(s1->#p3_fs() #p4_fs->f2) + + % Queries: + % Naf(p_fs(tps1->sps1)) % No + % Naf(p_fs(tps1->sps2)) % Yes + % Naf(q_fs(sps1->tps1)) % No + % Naf(q_fs(sps1->tps2)) % Yes + % Naf( p2_fs(s1->#p3_fs() #p4_fs->f2) ) % No + % Naf( p2_fs(s1->o#p3_fs() #p4_fs->f2) ) % Yes + % Naf( p2_fs(s1->#p3_fs() #p4_fs->f3) ) % Yes + % Naf( p1_fs(s1->f1) ) % No + % Naf( p1_fs(s2->f2) ) % No + % Naf( And(p1_fs(s2->f2) p1_fs(s1->f1)) ) % No + % Naf( And(p1_fs(s2->f2) p1_fs(s1->f2)) ) % No + % Naf( Or(p1_fs(s2->f2) p1_fs(s1->f1)) ) % No + % Naf( Or(p1_fs(s2->f2) p1_fs(s1->f2)) ) % No + % Naf( Exists ?1 ( p1_fs(s1->?1 s2->f2) ) ) % No + % Naf( Exists ?1 ( p1_fs(s1->?1 s1->f2) ) ) % No + % Naf( Naf( Exists ?1 ( p1_fs(s1->?1 s2->f2) ) ) ) % Yes + % Naf( Naf( Exists ?1 ( p1_fs(s1->?1 s2->f3) ) ) ) % Yes + % Naf( p1_fs(s1->f1 s2->f2) ) % No + % Naf( p1_fs(s1->?f1 s2->f2) ) % No + % Naf( p1_fs(s1->f1 s3->f2) ) % No + % Naf( p1_fs(s1->?f1 ?s2->f2) ) % No + % Naf( p1_fs(s1->f1) ) % No + % Naf( p3_fs(s1->#p4_fs()) ) % No + % Naf( p3_fs(s1->#p5_fs()) ) % No + % Naf( p3_fs(#p4_fs()->f2) ) % Yes + % Naf( p3_fs(#p5_fs()->f2) ) % No + % Naf( And(p3_fs(s1->#p4_fs()) p3_fs(#p5_fs->f3)) ) % Yes + % Naf( Or(p3_fs(s1->#p4_fs()) p3_fs(s2->#p5_fs())) ) % No + % Naf( Or(p3_fs(s1->#p3_fs()) p3_fs(s2->#p2_fs())) ) % No + % Naf( Exists ?1 (p3_fs(s1->?1#p3_fs)) ) % No + % Naf( Exists ?1 (p3_fs(s1->?1#p4_fs)) ) % No + + + % Framepoints + Forall ?o1 ?o2 ?s1 ?f1 ( + ?o1#p1_fp(?s1->?f1) :- + And(Or(?o1#p1_fs(s1->f1) + p2_fs(?s1->#p3_fs()))) + ) + + o_fp#q_fp(sp1->tp1) + + Forall ?o ?x ( + ?o#p_fp(tp1->?x) :- ?o#q_fp(?x->tp1) + ) + + % Queries: + % Naf(o_fp#p_fp(tp1->sp1)) % No + % Naf(o_fp#p_fp(tp1->sp2)) % Yes + % Naf(o_fp#q_fp(sp1->tp1)) % No + % Naf(o_fp#q_fp(sp1->tp2)) % Yes + % Naf(?#p1_fp) % No + % Naf(?o1#p1_fp(?s1->?f1)) % No + % Naf(Naf(?o1#p1_fp)) % Yes, ?o1 free + % Naf(Naf(?o1#p1_fp)) % Yes, ?o1 free + % And(?o1#p1_fp(?s1->?f1) Naf(Naf(?o1#p1_fp))) % Yes + + % Shelframeships + p1_sfs(-[t1 u1] s1->f1 -[t2 u2 v2] s2->f2) + Forall ?o1_sfs ( + ?o1_sfs#p2_sfs(s1->f1 -[s1 t1]) :- ?o1_sfs#p3_sfs + ) + + o1_sfs#p3_sfs + q_sfs(-[srps1 trps1] slrps1->vlrps1) + + Forall ?x ?v ( + p_sfs(-[trps1 ?x] slrps1->?v) :- q_sfs(-[?x trps1] slrps1->?v) + ) + + % Queries: + % Naf(q_sfs(-[srps1 trps1] slrps1->vlrps1)) % No + % Naf(q_sfs(-[srps1 trps2] slrps1->vlrps1)) % Yes + % Naf(q_sfs(-[srps1 trps1] slrps1->vlrps2)) % Yes + % Naf(p_sfs(-[trps1 srps1] slrps1->vlrps1)) % No + % Naf(p_sfs(-[trps1 srps2] slrps1->vlrps1)) % Yes + % Naf(p_sfs(-[trps1 srps1] slrps1->vlrps2)) % Yes + % Naf(?o#p1_sfs) % No + % Naf(?o#p1_sfs(s1->f1)) % No + % Naf(?o#p2_sfs) % No + % Naf(o#p2_sfs) % Yes + % Naf(?o#p2_sfs(-[s1 t1])) % No + % And(?o#p2_sfs Naf(?o#p2_sfs(-[s1 t2]))) % Yes + + % Naf(o1_sfs#p2_sfs(-[s1 t1])) % No + % Naf(o2_sfs#p2_sfs(-[s1 t1])) % Yes + % Naf( And(p1_sfs(-[t1 u1]) p1_sfs(s1->f1)) ) % No + % Naf( And(p1_sfs(-[t1 u1]) p1_sfs(s2->f1)) ) % Yes + % Naf( And(p1_sfs(-[t1 u1]) p1_sfs(s1->f2)) ) % No + % Naf( Or(p1_sfs(-[t2 u2 v2]) p1_sfs(-[t1 u1])) ) % No + % Naf( Or(p1_sfs(-[t2 u2 v3]) p1_sfs(-[t1 u1])) ) % No + % Naf( Or(p1_sfs(-[t2 u2 v3]) p1_sfs(-[t1 u2])) ) % Yes + % Naf( Or(p1_sfs(-[t2 u2 v2]) p1_sfs(-[t1 u1] s2->f2)) ) % No + % Naf( Or(p1_sfs(-[t2 u2 v2]) p1_sfs(-[t1 u1] s3->f2)) ) % No + % Naf( And(p1_sfs(-[t2 u2 v2]) p1_sfs(-[t1 u1] s3->f2)) ) % Yes + + + % Shelframepoints + o1_sfp#p1_sfp(-[t1 u1] s1->f1 -[t2 u2 v2] s2->f2) + + Forall ?o1 ?s1 ?u2 ( + ?o1#p1_sfp(-[t1 u1] ?s1->f1 -[t2 ?u2 v2] s2->f2) :- + And(?o1#p1_sfp(?s1->f1) + ?o1#p1_sp(-[?s1 t1 u1])) + ) + + o_sfp#q_sfp(-[srpp1 trpp1] slrpp1->vlrpp1) + + Forall ?o ?x ?v ( + ?o#p_sfp(-[trpp1 ?x] slrpp1->?v) :- ?o#q_sfp(-[?x trpp1] slrpp1->?v) + ) + + % Queries: + % Naf(o_sfp#q_sfp(-[srpp1 trpp1] slrpp1->vlrpp1)) % No + % Naf(o_sfp#q_sfp(-[srpp1 trpp2] slrpp1->vlrpp1)) % Yes + % Naf(o_sfp#q_sfp(-[srpp1 trpp1] slrpp1->vlrpp2)) % Yes + % Naf(Naf(o_sfp#p_sfp(-[trpp1 srpp1] slrpp1->vlrpp1))) % Yes + % Naf(?o1#p1_sfp) % No + % Naf(?o1#p1_sfp(-[t1 u1])) % No + % Naf(?o1#p1_sfp(?s1->f1)) % No + % Naf(?o1#p1_sfp(?s1->?f1 -[t1 u1])) % No + % Naf(?o1#p1_sfp(-[t1 u1] ?s1->?f1 -[t2 ?u2 v2])) % No + % Naf( o1_sfp#p1_sfp(-[t1 u1] s1->f1) ) % No + % Naf( o1_sfp#p1_sfp(s1->f1 -[t1 u1]) ) % No + % Naf( #p1_sfp(s1->f1 -[t1 u1]) ) % No + % Naf( #p1_sfp(s1->f2 -[t1 u1]) ) % No + % Naf( #p1_sfp(s1->f1 -[t1 u2]) ) % Yes + % Naf( #p1_sfp(s1->f1 -[t2 u2 v2]) ) % No + % Naf( #p1_sfp(s1->f2 -[t2 u2 v2]) ) % No + % Naf( #p1_sfp(s1->f1 -[t2 u2 v3]) ) % Yes + % Naf( And( #p1_sfp(s1->f1) ?o#p1_sfp(-[t2 u2 v2]) ) ) % No + % Naf( And( #p1_sfp(s1->f2) ?o#p1_sfp(-[t2 u2 v2]) ) ) % No + % And( ?o#p1_sfp Naf( And( #p1_sfp(s1->f1) ?o#p1_sfp(-[t2 u2 v3]) ) ) ) % Yes + + % Naf( Or( #p1_sfp(s1->f1) ?o#p1_sfp(-[t2 u2 v2]) ) ) % No + % Naf( Or( #p1_sfp(s1->f2) ?o#p1_sfp(-[t2 u2 v2]) ) ) % No + % Naf( Or( #p1_sfp(s1->f1) ?o#p1_sfp(-[t2 u2 v3]) ) ) % No + % And( ?o#p1_sfp Naf( Or( #p1_sfp(s2->f1) ?o#p1_sfp(-[t2 u2 v3]) ) ) ) % Yes + + /* + Dependent Atoms + */ + + % Relationships + q_rs(+[sr1 tr1]) + + Forall ?x ( + p_rs(+[tr1 ?x]) :- q_rs(+[?x tr1]) + ) + + p1_rs(+[s1 t1]) + p1_rs(+[s2 t2 u2]) + p2_rs(+[s1 t1 u1]) + p3_rs(+[#p4_rs(+[s]) #p5_rs(+[t])]) + + Forall ?x ?y ( + p4_rs(+[?x s1]) :- And(p5_rs(+[s1 ?x]) p5_rs(+[?y t2 u2])) + ) + + Forall ?x ?y ( + p4_rs(+[t2 ?y u2]) :- And(p5_rs(+[s1 ?x]) p5_rs(+[?y t2 u2])) + ) + + p5_rs(+[s1 t1]) + p5_rs(+[s2 t2 u2]) + + Forall ?v1 ?v2 ?v3 ( + p6_rs(+[?v1 ?v2 ?v3]) :- p7_rs(+[?v1 ?v2 ?v3]) + ) + + p7_rs(+[a1 b1 c1]) + + % Queries: + % Naf(q_rs(+[sr1 tr1])) % No + % Naf(q_rs(+[sr1 tr2])) % Yes + % Naf(p_rs(+[tr1 sr1])) % No + % Naf(p_rs(+[tr1 sr2])) % Yes + % Naf(p3_rs(+[a1 b1 b1])) % Yes + % Naf(p3_rs(+[a1 b1 c1])) % Yes + % Naf( And(p4_rs(+[t1 s1]) p4_rs(+[t2 s2 u2])) ) % No + % Naf( And(p4_rs(+[t1 s1]) p4_rs(+[t2 s2 u3])) ) % Yes + % Naf( And(p4_rs(+[t1 s1]) p4_rs(+[t2 s3 u2])) ) % Yes + % Naf( p6_rs(+[a1 b1 c1]) ) % No + % Naf( And(p1_rs(+[s1 t1]) p1_rs(+[s2 t2 u2])) ) % No + % And( p1_rs(+[s2 ?t2 u2]) Naf( And(p1_rs(+[s1 t1]) p1_rs(+[s2 ?t2 u3]) ) ) ) % Yes + % Naf( And(p1_rs(+[s1 t1]) p1_rs(+[s2 ?t2 u2])) ) % No + % Naf( And(p1_rs(+[s1 t1]) p1_rs(+[s2 t2 u2])) ) % No + % And( p1_rs(+[?s1 t1]) ?t2=t2 Naf( Naf( p1_rs(+[s2 ?t2 u2]) ) ) ) % Yes + % Naf( Exists ?s ( p2_rs(+[?s t1 u1]) ) ) % No + % Naf( Exists ?s ( p2_rs(+[?s t1 u2]) ) ) % Yes + % Exists ?s ( Naf( p2_rs(+[?s t1]) ) ) % Yes + % Naf( p2_rs(+[s1 t1 u1]) ) % No + % Naf( p2_rs(+[s1 t1 u2] ) ) % Yes + % Naf( p3_rs(+[#p4_rs(+[s]) #p5_rs(+[t])]) ) % No + % Naf( p3_rs(+[#p4_rs(+[s]) #p5_rs(+[t]) #p6_rs()]) ) % Yes + % Naf( And(p3_rs(+[#p4_rs(+[s])]) p3_rs(+[#p6_rs()])) ) % Yes + % Naf( Or(p3_rs(+[#p4_rs(+[s])]) p3_rs(+[#p6_rs()])) ) % Yes + + + % Relationpoints + o_rrp#q_rrp(+[srp1 trp1]) + + Forall ?o ?x ( + ?o#p_rrp(+[trp1 ?x]) :- ?o#q_rrp(+[?x trp1]) + ) + + o1_rrp#p1_rrp(+[s1 t1] +[s2 t2 u2]) + + Forall ?o1 ?o2 ?s1 ?t1 ( + ?o1#p1_rrp(+[?s1 ?t1 u1]) :- + And( ?o1#p1_fs(s1+>f1 +[?s1 ?t1]) + p2_fs(s1+>#p3_fs() ?o2+>f2) ) + ) + + % Queries: + % Naf(o_rrp#q_rrp(+[srp1 trp1])) % No + % Naf(o_rrp#q_rrp(+[srp1 trp3])) % Yes + % Naf(o_rrp#p_rrp(+[trp1 srp1])) % No + % Naf(o_rrp#p_rrp(+[trp1 srp2])) % Yes + % Naf(?o1#p1_rrp) % No + % And(?o1#p1_rrp ?s1=s2 ?t1=t2 Naf(?o1#p1_rrp(+[?s1 ?t1 u1]))) % Yes + % Naf(?o1#p1_rrp) % No + % Naf( o1_rrp#p1_rrp(+[s1 t1]) ) % No + % Naf( o1_rrp#p1_rrp(+[s1 t1] +[s2 t2 u2]) ) % No + % Naf( #p1_rrp(+[s1 t1]) ) % No + % Naf( #p1_rrp(+[t1 u1]) ) % Yes + % Naf( #p1_rrp(+[s1 t2]) ) % Yes + % Naf( ?o#p1_rrp ) % No + % Naf( o1_rrp#p1_rrp) % No + % Naf( o1_rrp#p1_rrp(+[s1 t1]) ) % No + % Naf( o2_rrp#p1_rrp(+[s1 t1]) ) % Yes + + + % Pairships + q_ps(sps1+>tps1) + + Forall ?x ( + p_ps(tps1+>?x) :- q_ps(?x+>tps1) + ) + + p1_ps(s1+>f1 s2+>f2) + p2_ps(s1+>f1) + p3_ps(s1+>#p4_ps() #p5_ps+>f2) + + p1_ps(s1+>f1 s2+>f2) :- p2_ps(s1+>f1) + p2_ps(s1+>#p3_ps() #p4_ps+>f2) + + % Queries: + % Naf(p_ps(tps1+>sps1)) % No + % Naf(p_ps(tps1+>sps2)) % Yes + % Naf(q_ps(sps1+>tps1)) % No + % Naf(q_ps(sps1+>tps2)) % Yes + % Naf( p2_ps(s1+>#p3_ps() #p4_ps+>f2) ) % No + % Naf( p2_ps(s1+>o#p3_ps() #p4_ps+>f2) ) % Yes + % Naf( p2_ps(s1+>#p3_ps() #p4_ps+>f3) ) % Yes + % Naf( p1_ps(s1+>f1) ) % No + % Naf( p1_ps(s2+>f2) ) % No + % Naf( And(p1_ps(s2+>f2) p1_ps(s1+>f1)) ) % No + % Naf( And(p1_ps(s2+>f2) p1_ps(s1+>f2)) ) % Yes + % Naf( Or(p1_ps(s2+>f2) p1_ps(s1+>f1)) ) % No + % Naf( Or(p1_ps(s2+>f2) p1_ps(s1+>f2)) ) % No + % Naf( Exists ?1 ( p1_ps(s1+>?1 s2+>f2) ) ) % No + % Naf( Exists ?1 ( p1_ps(s1+>?1 s1+>f2) ) ) % Yes + % Naf( Naf( Exists ?1 ( p1_ps(s1+>?1 s2+>f2) ) ) ) % Yes + % Naf( Naf( Exists ?1 ( p1_ps(s1+>?1 s2+>f3) ) ) ) % No + % Naf( p1_ps(s1+>f1 s2+>f2) ) % No + % Naf( p1_ps(s1+>?f1 s2+>f2) ) % No + % Naf( p1_ps(s1+>f1 s3+>f2) ) % Yes + % Naf( p1_ps(s1+>?f1 ?s2+>f2) ) % No + % Naf( p1_ps(s1+>f1) ) % No + % Naf( p3_ps(s1+>#p4_ps()) ) % No + % Naf( p3_ps(s1+>#p5_ps()) ) % Yes + % Naf( p3_ps(#p4_ps()+>f2) ) % Yes + % Naf( p3_ps(#p5_ps()+>f2) ) % No + % Naf( And(p3_ps(s1+>#p4_ps()) p3_ps(#p5_ps+>f3)) ) % Yes + % Naf( Or(p3_ps(s1+>#p4_ps()) p3_ps(s2+>#p5_ps())) ) % No + % Naf( Or(p3_ps(s1+>#p3_ps()) p3_ps(s2+>#p2_ps())) ) % Yes + % Naf( Exists ?1 (p3_ps(s1+>?1#p3_ps)) ) % Yes + % Naf( Exists ?1 (p3_ps(s1+>?1#p4_ps)) ) % No + + + % Pairpoints + Forall ?o1 ?o2 ?s1 ?f1 ( + ?o1#p1_pp(?s1+>?f1) :- + And(Or(?o1#p_pp(?s1+>?f1) + p2_pp(?s1+>#p3_pp()))) + ) + + o_pp#q_pp(sp1+>tp1) + + Forall ?o ?x ( + ?o#p_pp(tp1+>?x) :- ?o#q_pp(?x+>tp1) + ) + + % Queries: + % Naf(o_pp#p_pp(tp1+>sp1)) % No + % Naf(o_pp#p_pp(tp1+>sp2)) % Yes + % Naf(o_pp#q_pp(sp1+>tp1)) % No + % Naf(o_pp#q_pp(sp1+>tp2)) % Yes + % Naf(?#p1_pp) % No + % And(?o1#p1_pp ?s1=tp1 ?f1=sp1 Naf(?o1#p1_pp(?s1+>?f1))) % No + % And(?o1=o_pp Naf(Naf(?o1#p1_pp))) % Yes + % And(?o1=o_pp ?s1=tp1 ?f1=sp1 Naf(Naf(?o1#p1_pp(?s1+>?f1)))) % Yes + + + % Relpairships + p1_rps(+[t1 u1] s1+>f1 +[t2 u2 v2] s2+>f2) + Forall ?o1_rps ( + ?o1_rps#p2_rps(s1+>f1 +[s1 t1]) :- ?o1_rps#p3_rps + ) + + o1_rps#p3_rps + q_rps(+[srps1 trps1] slrps1+>vlrps1) + + Forall ?x ?v ( + p_rps(+[trps1 ?x] slrps1+>?v) :- q_rps(+[?x trps1] slrps1+>?v) + ) + + % Queries: + % Naf(q_rps(+[srps1 trps1] slrps1+>vlrps1)) % No + % Naf(q_rps(+[srps1 trps2] slrps1+>vlrps1)) % Yes + % Naf(q_rps(+[srps1 trps1] slrps1+>vlrps2)) % Yes + % Naf(p_rps(+[trps1 srps1] slrps1+>vlrps1)) % No + % Naf(p_rps(+[trps1 srps2] slrps1+>vlrps1)) % Yes + % Naf(p_rps(+[trps1 srps1] slrps1+>vlrps2)) % Yes + % Naf(?o#p1_rps) % No + % Naf(?o#p1_rps(s1+>f1)) % No + % Naf(?o#p2_rps) % No + % Naf(o#p2_rps) % No + % Naf(?o#p2_rps(+[s1 t1])) % No + % Naf(?o#p2_rps(+[s1 t2])) % Yes, ?o free + % Naf(o1_rps#p2_rps(+[s1 t1])) % No + % Naf(o2_rps#p2_rps(+[s1 t1])) % Yes + % Naf( And(p1_rps(+[t1 u1]) p1_rps(s1+>f1)) ) % No + % Naf( And(p1_rps(+[t1 u1]) p1_rps(s2+>f1)) ) % Yes + % Naf( And(p1_rps(+[t1 u1]) p1_rps(s1+>f2)) ) % Yes + % Naf( Or(p1_rps(+[t2 u2 v2]) p1_rps(+[t1 u1])) ) % No + % Naf( Or(p1_rps(+[t2 u2 v3]) p1_rps(+[t1 u1])) ) % No + % Naf( Or(p1_rps(+[t2 u2 v3]) p1_rps(+[t1 u2])) ) % Yes + % Naf( Or(p1_rps(+[t2 u2 v2]) p1_rps(+[t1 u1] s2+>f2)) ) % No + % Naf( Or(p1_rps(+[t2 u2 v2]) p1_rps(+[t1 u1] s3+>f2)) ) % No + % Naf( And(p1_rps(+[t2 u2 v2]) p1_rps(+[t1 u1] s3+>f2)) ) % Yes + + + % Relpairpoints + o1_rpps#p1_rpps(+[t1 u1] s1+>f1 +[t2 u2 v2] s2+>f2) + + Forall ?o1 ?s1 ?u2 ( + ?o1#p1_rpps(+[t1 u1] ?s1+>f1 +[t2 ?u2 v2] s2+>f2) :- + And(?o1#p1_rpps(?s1+>f1) + ?o1#p1_sp(+[?s1 t1 u1])) + ) + + o_rpps#q_rpps(+[srpp1 trpp1] slrpp1+>vlrpp1) + + Forall ?o ?x ?v ( + ?o#p_rpps(+[trpp1 ?x] slrpp1+>?v) :- ?o#q_rpps(+[?x trpp1] slrpp1+>?v) + ) + + % Queries: + % Naf(o_rpps#q_rpps(+[srpp1 trpp1] slrpp1+>vlrpp1)) % No + % Naf(o_rpps#q_rpps(+[srpp1 trpp2] slrpp1+>vlrpp1)) % Yes + % Naf(o_rpps#q_rpps(+[srpp1 trpp1] slrpp1+>vlrpp2)) % Yes + % Naf(Naf(o_rpps#p_rpps(+[trpp1 srpp1] slrpp1+>vlrpp1))) % Yes + % Naf(?o1#p1_rpps) % No + % Naf(?o1#p1_rpps(+[t1 u1])) % No + % Naf(?o1#p1_rpps(?s1+>f1)) % No + % Naf(?o1#p1_rpps(?s1+>?f1 +[t1 u1])) % No + % Naf(?o1#p1_rpps(+[t1 u1] ?s1+>?f1 +[t2 ?u2 v2])) % No + % Naf( o1_rpps#p1_rpps(+[t1 u1] s1+>f1) ) % No + % Naf( o1_rpps#p1_rpps(s1+>f1 +[t1 u1]) ) % No + % Naf( #p1_rpps(s1+>f1 +[t1 u1]) ) % No + % Naf( #p1_rpps(s1+>f2 +[t1 u1]) ) % Yes + % Naf( #p1_rpps(s1+>f1 +[t1 u2]) ) % Yes + % Naf( #p1_rpps(s1+>f1 +[t2 u2 v2]) ) % No + % Naf( #p1_rpps(s1+>f2 +[t2 u2 v2]) ) % Yes + % Naf( #p1_rpps(s1+>f1 +[t2 u2 v3]) ) % Yes + % Naf( And( #p1_rpps(s1+>f1) ?o#p1_rpps(+[t2 u2 v2]) ) ) % No + % And( ?o#p1_rpps(+[t2 u2 v2]) Naf( And( #p1_rpps(s1+>f2) ?o#p1_rpps(+[t2 u2 v2]) ) ) ) % Yes + % And( ?o#p1_rpps Naf( And( #p1_rpps(s1+>f1) ?o#p1_rpps(+[t2 u2 v3]) ) ) ) % Yes + % Naf( Or( #p1_rpps(s1+>f1) ?o#p1_rpps(+[t2 u2 v2]) ) ) % No + % Naf( Or( #p1_rpps(s1+>f2) ?o#p1_rpps(+[t2 u2 v2]) ) ) % No + % Naf( Or( #p1_rpps(s1+>f1) ?o#p1_rpps(+[t2 u2 v3]) ) ) % No + % And( ?o#p1_rpps Naf(#p1_rpps(s2+>f1)) Naf(?o#p1_rpps(+[t2 u2 v3])) ) % Yes + + ) +) \ No newline at end of file diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer1.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer1.psoa new file mode 100644 index 0000000..dcd7a5d --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer1.psoa @@ -0,0 +1 @@ +Yes diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer2.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer2.psoa new file mode 100644 index 0000000..dcd7a5d --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer2.psoa @@ -0,0 +1 @@ +Yes diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer3.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer3.psoa new file mode 100644 index 0000000..dcd7a5d --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer3.psoa @@ -0,0 +1 @@ +Yes diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer4.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer4.psoa new file mode 100644 index 0000000..dcd7a5d --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer4.psoa @@ -0,0 +1 @@ +Yes diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer5.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer5.psoa new file mode 100644 index 0000000..cf45697 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer5.psoa @@ -0,0 +1 @@ +No diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer6.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer6.psoa new file mode 100644 index 0000000..dcd7a5d --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-answer6.psoa @@ -0,0 +1 @@ +Yes diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query1.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query1.psoa new file mode 100644 index 0000000..1f92e89 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query1.psoa @@ -0,0 +1 @@ +Naf( p1_ss(-[s1 t1] -[s2 t2 u3]) ) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query2.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query2.psoa new file mode 100644 index 0000000..63e861a --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query2.psoa @@ -0,0 +1 @@ +Naf( p2_ss(-[s1 t1 u2] ) ) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query3.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query3.psoa new file mode 100644 index 0000000..b420157 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query3.psoa @@ -0,0 +1 @@ +Naf( And(p3_rs(+[#p4_rs(+[s])]) p3_rs(+[#p6_rs()])) ) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query4.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query4.psoa new file mode 100644 index 0000000..6510076 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query4.psoa @@ -0,0 +1 @@ +Naf(p3_rs(+[a1 b1 b1])) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query5.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query5.psoa new file mode 100644 index 0000000..2e2f09e --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query5.psoa @@ -0,0 +1 @@ +Naf(p_rps(+[trps1 srps1] slrps1+>vlrps1)) diff --git a/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query6.psoa b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query6.psoa new file mode 100644 index 0000000..578df04 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_psoa_query/naf_psoa_query-query6.psoa @@ -0,0 +1 @@ +Naf(Naf(o_rpps#p_rpps(+[trpp1 srpp1] slrpp1+>vlrpp1))) diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-KB.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-KB.psoa new file mode 100644 index 0000000..4280d39 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-KB.psoa @@ -0,0 +1,99 @@ +RuleML( + Assert( + + q1(a b) + q1(c d) + + Forall ?v1 ?v2 ( + p1(a b c) :- Naf(q1(?v1 ?v2)) + ) + + % Queries: + % p1(a b c) % No + + r2(a b) + + q2(a b) + q2(a c) + + Forall ?v1 ?v2 ( + p2(a b c) :- And(r2(?v2 ?v1) Naf(q2(?v1 ?v2))) + ) + + % Queries: + % p2(?v1 ?v2 ?v3) % Yes + % p2(a ?v c) % Yes + % p2(a ?v b) % No + + r3(a) + q3(a b) + + Forall ?v1 ?v2 ( + p3(a b c) :- And(r3(?v2) Naf(q3(?v1 ?v2))) + ) + + % Queries: + % p3(a b c) % Yes + + r4(a) + r4(b) + + Forall ?v1 ?v2 ( + % This case isn't covered by the naf heuristic. + p4(a ?v2 c) :- Or(r4(?v2) Naf(q3(?v1 ?v2))) + ) + + % Queries: + % p4(a b c) % Yes + % p4(a a c) % Yes + % p4(a c c) % Yes + + Forall ?v1 ?v2 ?v3 ( + p6(+[?v1 ?v2 ?v3]) :- And(?v1=a1 ?v2=b1 ?v3=c1 + Naf(p5(+[?v1 ?v2 ?v3]))) + ) + + p5(+[a1 b1 c1]) + + % Queries: + % p5(+[a1 b1 b1]) % No + % p6(+[a1 b1 b1]) % No + % p6(+[a1 b1 c1]) % No + + Forall ?v1 ?v2 ( + p7(?v1 ?v2) :- And(?v2=a Naf(p5(+[?v2 ?v1 c]))) + ) + + % Queries: + % And(?v1=b p7(?v1 ?v2)) % Yes + % p7(c b) % No + % p7(a b) % No + % p7(b a) % Yes + % p7(a a) % Yes + + Forall ?v1 ?v2 ( + p8(?v1 ?v2) :- And(Naf(p5(+[?v2 ?v1 c])) ?v2=a) + ) + + % Queries: + % And(p8(?v1 ?v2) ?v1=a) % Yes + % And(p8(?v1 ?v2) ?v2=a ?v1=b) % Yes + % And(p8(?v1 ?v2) ?v2=b) % No + % And(?v1=a p8(?v1 ?v2)) % Yes + % And(?v2=a ?v1=b p8(?v1 ?v2)) % Yes + % And(?v2=b p8(?v1 ?v2)) % No + + Forall ?v1 ?v2 ( + p9(?v1 ?v2) :- And(q2(?v1 ?v2) Naf(r2(?v1 ?v2))) + ) + + Forall ?v1 ?v2 ( + p10(?v1) :- And(?v1=?v2 Naf(?v1=a)) + ) + + Forall ?v1 ?v2 ( + p11(?v1) :- And(?v1=?v2 Naf(Or(?v1=a ?v1=b)) ?v2=d) + ) + + ) +) diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer1.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer1.psoa new file mode 100644 index 0000000..f22a1d4 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer1.psoa @@ -0,0 +1 @@ +?v1=_a ?v2=_c diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer2.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer2.psoa new file mode 100644 index 0000000..cf45697 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer2.psoa @@ -0,0 +1 @@ +No diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer3.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer3.psoa new file mode 100644 index 0000000..dcd7a5d --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer3.psoa @@ -0,0 +1 @@ +Yes diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer4.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer4.psoa new file mode 100644 index 0000000..cf45697 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer4.psoa @@ -0,0 +1 @@ +No diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer5.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer5.psoa new file mode 100644 index 0000000..cf45697 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer5.psoa @@ -0,0 +1 @@ +No diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer6.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer6.psoa new file mode 100644 index 0000000..dcd7a5d --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-answer6.psoa @@ -0,0 +1 @@ +Yes diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query1.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query1.psoa new file mode 100644 index 0000000..7d54a0e --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query1.psoa @@ -0,0 +1 @@ +p9(?v1 ?v2) diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query2.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query2.psoa new file mode 100644 index 0000000..4147459 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query2.psoa @@ -0,0 +1 @@ +p10(?v1) diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query3.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query3.psoa new file mode 100644 index 0000000..d9856af --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query3.psoa @@ -0,0 +1 @@ +p10(b) diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query4.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query4.psoa new file mode 100644 index 0000000..1bff7ac --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query4.psoa @@ -0,0 +1 @@ +p11(?v1) diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query5.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query5.psoa new file mode 100644 index 0000000..de00c02 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query5.psoa @@ -0,0 +1 @@ +p11(a) diff --git a/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query6.psoa b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query6.psoa new file mode 100644 index 0000000..c207799 --- /dev/null +++ b/PSOATransRun/test-basic/test-naf/naf_relationship_premise/naf_relationship_premise-query6.psoa @@ -0,0 +1 @@ +p11(d)