Implement containment circularity avoidance #20

2 files changed, 20 insertions, 4 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml
index 2381b84f..beaf5498 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml
@@ -1 +1,17 @@
-<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.4"?><plugin/>

+<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.4"?><plugin>

+  <extension id="ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries" point="org.eclipse.viatra.query.runtime.queryspecification">

+    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries" id="ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries">

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSComment"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSFofFormula"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSAnnotation"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSOr"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSAnd"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSEquivalent"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSFunction"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSExistentialQuantifier"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSUniversalQuantifier"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSUnaryNegation"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSInequality"/>

+    </group>

+  </extension>

+</plugin>

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql
index 2bc22f9e..ef61e4d1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql
@@ -48,9 +48,9 @@ pattern VLSInequality(term: VLSInequality){
         VLSInequality(term);

 }

 

-pattern VLSFunctionFof(term: VLSFunctionFof){

-        VLSFunctionFof(term);

-}

+//pattern VLSFunctionFof(term: VLSFunctionFof){

+//      VLSFunctionFof(term);

+//}

 

 //pattern VLSFofTerm(term: VLSFofTerm){

 //      VLSFofTerm(term);