Commit 7f949f70 authored by Sebastian Voss's avatar Sebastian Voss
Browse files

added YICES quantifier

parent 3a2edc48
......@@ -94,6 +94,15 @@
<eStructuralFeatures xsi:type="ecore:EReference" name="expression" lowerBound="1"
eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"/>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="Forall" eSuperTypes="platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm">
<eStructuralFeatures xsi:type="ecore:EReference" name="memberTypes" upperBound="-1"
eType="#//types/YicesTypeBase"/>
<eStructuralFeatures xsi:type="ecore:EAttribute" name="memberNames" upperBound="-1"
eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"
defaultValueLiteral=""/>
<eStructuralFeatures xsi:type="ecore:EReference" name="expression" lowerBound="1"
eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"/>
</eClassifiers>
</eSubpackages>
<eSubpackages name="run" nsURI="http://www.fortiss.org/af3/tools/yices/run" nsPrefix="org-fortiss-af3-tools-yices-run">
<eClassifiers xsi:type="ecore:EClass" name="YicesResult">
......
......@@ -101,6 +101,13 @@
<genFeatures notify="false" createChild="false" propertySortChoices="true"
ecoreFeature="ecore:EReference yices.ecore#//commands/Lambda/expression"/>
</genClasses>
<genClasses ecoreClass="yices.ecore#//commands/Forall">
<genFeatures notify="false" createChild="false" propertySortChoices="true"
ecoreFeature="ecore:EReference yices.ecore#//commands/Forall/memberTypes"/>
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute yices.ecore#//commands/Forall/memberNames"/>
<genFeatures notify="false" createChild="false" propertySortChoices="true"
ecoreFeature="ecore:EReference yices.ecore#//commands/Forall/expression"/>
</genClasses>
</nestedGenPackages>
<nestedGenPackages prefix="AF3YicesRun" basePackage="org.fortiss.af3.tools.yices.model"
disposableProviderFactory="true" ecorePackage="yices.ecore#//run">
......
......@@ -25,6 +25,7 @@ import org.fortiss.af3.project.model.typesystem.ITerm;
import org.fortiss.af3.tools.yices.model.commands.AF3YicesCommandsFactory;
import org.fortiss.af3.tools.yices.model.commands.Assert;
import org.fortiss.af3.tools.yices.model.commands.Check;
import org.fortiss.af3.tools.yices.model.commands.Forall;
import org.fortiss.af3.tools.yices.model.commands.Function;
import org.fortiss.af3.tools.yices.model.commands.Lambda;
import org.fortiss.af3.tools.yices.model.run.AF3YicesRunFactory;
......@@ -56,7 +57,7 @@ import org.fortiss.af3.tools.yices.model.types.YicesTypeBase;
* @author ratiu
* @author $Author: ratiu $
* @version $Rev: 1270 $
* @ConQAT.Rating GREEN Hash: EC8B6BF6768BA8F74513F05E63A64274
* @ConQAT.Rating GREEN Hash: 53B44D1DCB6C5BB7F36BCDDD2860362E
*/
public class YicesModelFactory {
......@@ -237,6 +238,16 @@ public class YicesModelFactory {
return lambda;
}
/** Factory for {@link Function} objects. */
public static Forall createForall(List<YicesTypeBase> memberTypes, List<String> memberNames,
IExpressionTerm name) {
Forall forall = AF3YicesCommandsFactory.eINSTANCE.createForall();
forall.getMemberTypesList().addAll(memberTypes);
forall.getMemberNamesList().addAll(memberNames);
forall.setExpression(name);
return forall;
}
/** Factory for {@link Function} objects. */
public static IfThenElse createIfThenElse(IExpressionTerm guard, IExpressionTerm thenStatement,
IExpressionTerm elseStatement) {
......
......@@ -40,6 +40,7 @@ import org.fortiss.af3.tools.yices.model.YicesFileContent;
import org.fortiss.af3.tools.yices.model.commands.Assert;
import org.fortiss.af3.tools.yices.model.commands.Check;
import org.fortiss.af3.tools.yices.model.commands.ExtendedAssert;
import org.fortiss.af3.tools.yices.model.commands.Forall;
import org.fortiss.af3.tools.yices.model.commands.Function;
import org.fortiss.af3.tools.yices.model.commands.Lambda;
import org.fortiss.af3.tools.yices.model.types.BoolType;
......@@ -65,7 +66,7 @@ import org.fortiss.af3.tools.yices.model.types.YicesTypeBase;
* @author ratiu
* @author $Author: hoelzl $
* @version $Rev: 18709 $
* @ConQAT.Rating GREEN Hash: CE3AA29E92685996D5C859825BD4211A
* @ConQAT.Rating GREEN Hash: 3821093B26C7FCA05BAD69FA1A4F326B
*/
public class YicesTextGenerator implements ITextGenerator<YicesFile> {
......@@ -132,9 +133,22 @@ public class YicesTextGenerator implements ITextGenerator<YicesFile> {
generateText(w, (Lambda)type);
} else if(type instanceof IfThenElse) {
generateText(w, (IfThenElse)type);
} else if(type instanceof Forall) {
generateText(w, (Forall)type);
}
}
/** generate text for FORALL quantifier */
private void generateText(Writer w, Forall forall) throws IOException,
UnknownLanguageFragmentException {
w.append("(forall (");
for(int i = 0; i < forall.getMemberNamesLength(); i++) {
w.append(" " + forall.getMemberNames(i)).append("::");
generateText(w, forall.getMemberTypes(i));
}
w.append(")" + convertExpressionToString(forall.getExpression()) + ")");
}
/**
* Generate text for lambda
*
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment