cleanings and small improvements for enabling advanced evidence

refs 954

org.fortiss.af3.tools/trunk/model/yices.ecore

@@ -56,10 +56,6 @@
           eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
       <eStructuralFeatures xsi:type="ecore:EReference" name="lambda" eType="#//commands/Lambda"/>
     </eClassifiers>
-    <eClassifiers xsi:type="ecore:EClass" name="SelectTerm" eSuperTypes="platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm">
-      <eStructuralFeatures xsi:type="ecore:EAttribute" name="identifier" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
-      <eStructuralFeatures xsi:type="ecore:EAttribute" name="field" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
-    </eClassifiers>
     <eClassifiers xsi:type="ecore:EClass" name="Subrange" eSuperTypes="#//types/YicesTypeBase">
       <eStructuralFeatures xsi:type="ecore:EReference" name="ExpressionMembers" lowerBound="1"
           upperBound="-1" eType="ecore:EClass platform:/plugin/org.fortiss.af3.project/model/project.ecore#//typesystem/ITerm"/>
@@ -69,6 +65,20 @@
       <eStructuralFeatures xsi:type="ecore:EReference" name="ThenStatement" eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"/>
       <eStructuralFeatures xsi:type="ecore:EReference" name="ElseStatement" eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"/>
     </eClassifiers>
+    <eSubpackages name="constructor" nsURI="http://www.fortiss.org/af3/tools/yices/constructors"
+        nsPrefix="org-fortiss-af3-tools-yices-constructors">
+      <eClassifiers xsi:type="ecore:EClass" name="MkRecord" eSuperTypes="platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm">
+        <eStructuralFeatures xsi:type="ecore:EAttribute" name="memberNames" upperBound="-1"
+            eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+        <eStructuralFeatures xsi:type="ecore:EReference" name="memberExpressions"
+            upperBound="-1" eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"
+            containment="true"/>
+      </eClassifiers>
+      <eClassifiers xsi:type="ecore:EClass" name="SelectTerm" eSuperTypes="platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm">
+        <eStructuralFeatures xsi:type="ecore:EAttribute" name="identifier" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+        <eStructuralFeatures xsi:type="ecore:EAttribute" name="field" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+      </eClassifiers>
+    </eSubpackages>
   </eSubpackages>
   <eSubpackages name="commands" nsURI="http://www.fortiss.org/af3/tools/yices/commands"
       nsPrefix="org-fortiss-af3-tools-yices-commands">
@@ -85,7 +95,6 @@
           eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"/>
       <eStructuralFeatures xsi:type="ecore:EReference" name="name" eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"/>
     </eClassifiers>
-    <eClassifiers xsi:type="ecore:EClass" name="Select" eSuperTypes="#//YicesFileContent"/>
     <eClassifiers xsi:type="ecore:EClass" name="Lambda" eSuperTypes="platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm">
       <eStructuralFeatures xsi:type="ecore:EAttribute" name="memberNames" upperBound="-1"
           eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
@@ -113,6 +122,10 @@
     <eClassifiers xsi:type="ecore:EClass" name="EvidenceEntry">
       <eStructuralFeatures xsi:type="ecore:EAttribute" name="variable" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
       <eStructuralFeatures xsi:type="ecore:EAttribute" name="value" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
+      <eStructuralFeatures xsi:type="ecore:EReference" name="lhs" eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"
+          containment="true"/>
+      <eStructuralFeatures xsi:type="ecore:EReference" name="rhs" eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"
+          containment="true"/>
     </eClassifiers>
   </eSubpackages>
 </ecore:EPackage>

org.fortiss.af3.tools/trunk/model/yices.genmodel

@@ -58,12 +58,6 @@
         <genFeatures notify="false" createChild="false" propertySortChoices="true"
             ecoreFeature="ecore:EReference yices.ecore#//types/DependentFunctionType/lambda"/>
       </genClasses>
-      <genClasses ecoreClass="yices.ecore#//types/SelectTerm">
-        <genFeatures notify="false" createChild="false" propertySortChoices="true"
-            ecoreFeature="ecore:EAttribute yices.ecore#//types/SelectTerm/identifier"/>
-        <genFeatures notify="false" createChild="false" propertySortChoices="true"
-            ecoreFeature="ecore:EAttribute yices.ecore#//types/SelectTerm/field"/>
-      </genClasses>
       <genClasses ecoreClass="yices.ecore#//types/Subrange">
         <genFeatures createChild="false" ecoreFeature="ecore:EReference yices.ecore#//types/Subrange/ExpressionMembers"/>
       </genClasses>
@@ -75,6 +69,17 @@
         <genFeatures notify="false" createChild="false" propertySortChoices="true"
             ecoreFeature="ecore:EReference yices.ecore#//types/IfThenElse/ElseStatement"/>
       </genClasses>
+      <nestedGenPackages prefix="AF3YicesConstructor" basePackage="org.fortiss.af3.tools.yices.model.types"
+          disposableProviderFactory="true" ecorePackage="yices.ecore#//types/constructor">
+        <genClasses ecoreClass="yices.ecore#//types/constructor/MkRecord">
+          <genFeatures createChild="false" ecoreFeature="ecore:EAttribute yices.ecore#//types/constructor/MkRecord/memberNames"/>
+          <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference yices.ecore#//types/constructor/MkRecord/memberExpressions"/>
+        </genClasses>
+        <genClasses ecoreClass="yices.ecore#//types/constructor/SelectTerm">
+          <genFeatures createChild="false" ecoreFeature="ecore:EAttribute yices.ecore#//types/constructor/SelectTerm/identifier"/>
+          <genFeatures createChild="false" ecoreFeature="ecore:EAttribute yices.ecore#//types/constructor/SelectTerm/field"/>
+        </genClasses>
+      </nestedGenPackages>
     </nestedGenPackages>
     <nestedGenPackages prefix="AF3YicesCommands" basePackage="org.fortiss.af3.tools.yices.model"
         disposableProviderFactory="true" ecorePackage="yices.ecore#//commands">
@@ -93,7 +98,6 @@
             ecoreFeature="ecore:EReference yices.ecore#//commands/Function/values"/>
         <genFeatures createChild="false" ecoreFeature="ecore:EReference yices.ecore#//commands/Function/name"/>
       </genClasses>
-      <genClasses ecoreClass="yices.ecore#//commands/Select"/>
       <genClasses ecoreClass="yices.ecore#//commands/Lambda">
         <genFeatures createChild="false" ecoreFeature="ecore:EAttribute yices.ecore#//commands/Lambda/memberNames"/>
         <genFeatures notify="false" createChild="false" propertySortChoices="true"
@@ -118,6 +122,8 @@
       <genClasses ecoreClass="yices.ecore#//run/EvidenceEntry">
         <genFeatures createChild="false" ecoreFeature="ecore:EAttribute yices.ecore#//run/EvidenceEntry/variable"/>
         <genFeatures createChild="false" ecoreFeature="ecore:EAttribute yices.ecore#//run/EvidenceEntry/value"/>
+        <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference yices.ecore#//run/EvidenceEntry/lhs"/>
+        <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference yices.ecore#//run/EvidenceEntry/rhs"/>
       </genClasses>
     </nestedGenPackages>
   </genPackages>

org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/yices/model/YicesModelAccessFacade.java

@@ -27,7 +27,6 @@ import static org.fortiss.af3.tools.yices.model.YicesModelFactory.createEvidence
 import org.fortiss.af3.project.model.typesystem.ITerm;
 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.Select;
 import org.fortiss.af3.tools.yices.model.run.EvidenceEntry;
 import org.fortiss.af3.tools.yices.model.run.YicesResult;
 import org.fortiss.af3.tools.yices.model.types.DefineType;
@@ -70,11 +69,6 @@ public class YicesModelAccessFacade {
 		return addLine(logicalFile, createAssert(expression));
 	}
 
-	/** Creates an {@link Assert} and adds it to the file. */
-	public static YicesFile addSelect(YicesFile logicalFile, Select select) {
-		return addLine(logicalFile, select);
-	}
-
 	/** Creates an {@link Check} and adds it to the file. */
 	public static YicesFile addCheck(YicesFile logicalFile) {
 		return addLine(logicalFile, createCheck());

org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/yices/model/YicesModelFactory.java

@@ -43,11 +43,13 @@ import org.fortiss.af3.tools.yices.model.types.NatType;
 import org.fortiss.af3.tools.yices.model.types.RealType;
 import org.fortiss.af3.tools.yices.model.types.RecordType;
 import org.fortiss.af3.tools.yices.model.types.ScalarType;
-import org.fortiss.af3.tools.yices.model.types.SelectTerm;
 import org.fortiss.af3.tools.yices.model.types.SubType;
 import org.fortiss.af3.tools.yices.model.types.Subrange;
 import org.fortiss.af3.tools.yices.model.types.UserType;
 import org.fortiss.af3.tools.yices.model.types.YicesTypeBase;
+import org.fortiss.af3.tools.yices.model.types.constructor.AF3YicesConstructorFactory;
+import org.fortiss.af3.tools.yices.model.types.constructor.MkRecord;
+import org.fortiss.af3.tools.yices.model.types.constructor.SelectTerm;
 
 /**
  * Factory methods for the Yices model. These methods are advanced wrappers for
@@ -157,6 +159,15 @@ public class YicesModelFactory {
 		return rt;
 	}
 
+	/** Factory for {@link MkRecord} objects. */
+	public static MkRecord createMkRecord(List<IExpressionTerm> memberExpressions,
+			List<String> memberNames) {
+		MkRecord rt = AF3YicesConstructorFactory.eINSTANCE.createMkRecord();
+		rt.getMemberExpressionsList().addAll(memberExpressions);
+		rt.getMemberNamesList().addAll(memberNames);
+		return rt;
+	}
+
 	/** Factory for {@link YicesResult} objects. */
 	public static YicesResult createYicesResult(boolean isSatisfiable) {
 		YicesResult yt = AF3YicesRunFactory.eINSTANCE.createYicesResult();
@@ -207,7 +218,7 @@ public class YicesModelFactory {
 
 	/** Factory for {@link SelectTerm} objects. */
 	public static SelectTerm createSelectTerm(String identifier, String field) {
-		SelectTerm select = AF3YicesTypesFactory.eINSTANCE.createSelectTerm();
+		SelectTerm select = AF3YicesConstructorFactory.eINSTANCE.createSelectTerm();
 		select.setIdentifier(identifier);
 		select.setField(field);
 		return select;

org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/yices/textgen/YicesTextGenerator.java

@@ -54,11 +54,12 @@ import org.fortiss.af3.tools.yices.model.types.NatType;
 import org.fortiss.af3.tools.yices.model.types.RealType;
 import org.fortiss.af3.tools.yices.model.types.RecordType;
 import org.fortiss.af3.tools.yices.model.types.ScalarType;
-import org.fortiss.af3.tools.yices.model.types.SelectTerm;
 import org.fortiss.af3.tools.yices.model.types.SubType;
 import org.fortiss.af3.tools.yices.model.types.Subrange;
 import org.fortiss.af3.tools.yices.model.types.UserType;
 import org.fortiss.af3.tools.yices.model.types.YicesTypeBase;
+import org.fortiss.af3.tools.yices.model.types.constructor.MkRecord;
+import org.fortiss.af3.tools.yices.model.types.constructor.SelectTerm;
 
 /**
  * Generates Yices interpretable text from a Yices logical file.
@@ -138,7 +139,7 @@ public class YicesTextGenerator implements ITextGenerator<YicesFile> {
 		}
 	}
 
-	/** generate text for FORALL quantifier */
+	/** Generate text for FORALL quantifier */
 	private void generateText(Writer w, Forall forall) throws IOException,
 			UnknownLanguageFragmentException {
 		w.append("(forall (");
@@ -266,18 +267,25 @@ public class YicesTextGenerator implements ITextGenerator<YicesFile> {
 	private void generateText(Writer w, Assert assertCommand) throws IOException,
 			UnknownLanguageFragmentException {
 		w.append("(assert ");
-		if(!(assertCommand.getExpression() instanceof Forall)) {
-			w.append(convertExpressionToString(assertCommand.getExpression()));
+		generateText(w, assertCommand.getExpression());
+		w.append(")\n");
+	}
+
+	/** Generate text for Expression. */
+	private void generateText(Writer w, ITerm expression) throws IOException,
+			UnknownLanguageFragmentException {
+		if(expression instanceof Forall) {
+			generateText(w, (Forall)expression);
 		} else {
-			generateText(w, (Forall)assertCommand.getExpression());
+			w.append(convertExpressionToString(expression));
 		}
-		w.append(")\n");
 	}
 
 	/** Generate text for extended-assert command. */
 	private void generateText(Writer w, ExtendedAssert extendedAssert) throws IOException,
 			UnknownLanguageFragmentException {
-		w.append("(assert+ " + convertExpressionToString(extendedAssert.getExpression()));
+		w.append("(assert+ ");
+		generateText(w, extendedAssert.getExpression());
 		w.append(" " + extendedAssert.getWeight());
 		w.append(")\n");
 	}
@@ -333,6 +341,15 @@ public class YicesTextGenerator implements ITextGenerator<YicesFile> {
 			sb.append(st.getIdentifier() + ") " + st.getField() + ")");
 			return sb.toString();
 
+		} else if(term instanceof MkRecord) {
+			StringBuffer sb = new StringBuffer("(mk-record ");
+			MkRecord mkrecord = (MkRecord)term;
+			for(int i = 0; i < mkrecord.getMemberNamesLength(); i++) {
+				sb.append(" " + mkrecord.getMemberNames(i)).append("::");
+				sb.append(convertExpressionToString(mkrecord.getMemberExpressions(i)));
+			}
+			sb.append(")");
+			return sb.toString();
 		} else if(term instanceof Function) {
 			StringBuffer sb = new StringBuffer("(");
 			Function function = (Function)term;
@@ -342,11 +359,8 @@ public class YicesTextGenerator implements ITextGenerator<YicesFile> {
 				sb.append(convertExpressionToString(arg)).append(" ");
 			}
 			sb.append(") ");
-
 			return sb.toString();
-		}
-
-		else if(term instanceof Var) {
+		} else if(term instanceof Var) {
 			return ((Var)term).getIdentifier();
 		}
 		throw new UnknownLanguageFragmentException(term.toString());

org.fortiss.af3.tools/trunk/test-src/test/org/fortiss/af3/tools/yices/base/YicesTestBase.java

@@ -20,6 +20,7 @@ package test.org.fortiss.af3.tools.yices.base;
 import static org.fortiss.af3.tools.yices.model.YicesModelFactory.createYicesFile;
 
 import org.fortiss.af3.expression.language.Compiler;
+import org.fortiss.af3.project.model.typesystem.ITerm;
 import org.fortiss.af3.tools.yices.model.YicesFile;
 import org.fortiss.af3.tools.yices.model.YicesModelAccessFacade;
 import org.fortiss.af3.tools.yices.model.run.YicesResult;
@@ -71,6 +72,11 @@ public class YicesTestBase {
 		YicesModelAccessFacade.addAssert(currentFile, compiler.compileTerm(expressionString));
 	}
 
+	/** Adds an assert command with expression as ITerm. */
+	protected void addAssert(ITerm expression) {
+		YicesModelAccessFacade.addAssert(currentFile, expression);
+	}
+
 	/** Adds a constant declaration. */
 	protected void addConstantDeclaration(String name, YicesTypeBase type) {
 		YicesModelAccessFacade.addConstantDeclaration(currentFile, name, type);

org.fortiss.af3.tools/trunk/test-src/test/org/fortiss/af3/tools/yices/tests/ExpressionsTest.java

@@ -17,13 +17,27 @@ $Id: IntType.java 1270 2011-08-29 08:55:46Z ratiu $
 +--------------------------------------------------------------------------*/
 package test.org.fortiss.af3.tools.yices.tests;
 
+import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.boolConst;
+import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.equal;
+import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.intConst;
+import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.var;
+import static org.fortiss.af3.tools.yices.model.YicesModelFactory.createBoolType;
 import static org.fortiss.af3.tools.yices.model.YicesModelFactory.createIntType;
+import static org.fortiss.af3.tools.yices.model.YicesModelFactory.createMkRecord;
+import static org.fortiss.af3.tools.yices.model.YicesModelFactory.createRecordType;
 import static org.junit.Assert.assertEquals;
 import static org.junit.Assert.assertNotNull;
 import static org.junit.Assert.assertSame;
 import static org.junit.Assert.assertTrue;
 
+import java.util.ArrayList;
+import java.util.List;
+
+import org.fortiss.af3.expression.model.terms.IExpressionTerm;
+import org.fortiss.af3.tools.base.ToolRunnerBase;
 import org.fortiss.af3.tools.yices.model.run.YicesResult;
+import org.fortiss.af3.tools.yices.model.types.YicesTypeBase;
+import org.fortiss.af3.tools.yices.model.types.constructor.MkRecord;
 import org.junit.Test;
 
 import test.org.fortiss.af3.tools.yices.base.YicesTestBase;
@@ -66,10 +80,10 @@ public class ExpressionsTest extends YicesTestBase {
 		assertTrue(result.isSatisfiable());
 	}
 
-	/** Test whiteness. */
+	/** Test simple whiteness. */
 	@Test
-	public void testWhitness() {
-		newYicesFile("testWhitness");
+	public void testSimpleWhitness() {
+		newYicesFile("testSimpleWhitness");
 		addConstantDeclaration("x", createIntType());
 		addAssert("(x > -1) && (0 >= x)");
 		addCheck();
@@ -80,4 +94,37 @@ public class ExpressionsTest extends YicesTestBase {
 		assertSame(1, result.getEvidenceList().size());
 		assertEquals("0", getValue(result, "x"));
 	}
+
+	/** Test complex whiteness. */
+	@Test
+	public void testComplexWhitness() {
+		newYicesFile("testComplexWhitness");
+
+		List<YicesTypeBase> tps = new ArrayList<YicesTypeBase>();
+		tps.add(createBoolType());
+		tps.add(createIntType());
+		List<String> names = new ArrayList<String>();
+		names.add("aBool");
+		names.add("anInt");
+		addConstantDeclaration("aRecord", createRecordType(tps, names));
+
+		List<IExpressionTerm> exps = new ArrayList<IExpressionTerm>();
+		exps.add(boolConst(true));
+		exps.add(intConst(3));
+
+		List<String> recordNames = new ArrayList<String>();
+		recordNames.add("flag");
+		recordNames.add("x");
+		MkRecord rec = createMkRecord(exps, recordNames);
+
+		addAssert(equal(var("aRecord"), rec));
+		addCheck();
+
+		ToolRunnerBase.DEBUG = true;
+		YicesResult result = runYices();
+		assertNotNull(result);
+		assertTrue(result.isSatisfiable());
+		assertSame(1, result.getEvidenceList().size());
+		assertEquals("0", getValue(result, "x"));
+	}
 }