Commit 05b56780 authored by Daniel Ratiu's avatar Daniel Ratiu
Browse files

first steps to enhance the evidence with more structure

refs 954
parent 1948df2a
......@@ -120,8 +120,6 @@
eType="#//run/EvidenceEntry" containment="true"/>
</eClassifiers>
<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"
......
......@@ -120,8 +120,6 @@
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference yices.ecore#//run/YicesResult/evidence"/>
</genClasses>
<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>
......
......@@ -24,6 +24,7 @@ import static org.fortiss.af3.tools.yices.model.YicesModelFactory.createDefineTy
import static org.fortiss.af3.tools.yices.model.YicesModelFactory.createDefinedType;
import static org.fortiss.af3.tools.yices.model.YicesModelFactory.createEvidenceEntry;
import org.fortiss.af3.expression.model.terms.IExpressionTerm;
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;
......@@ -81,19 +82,10 @@ public class YicesModelAccessFacade {
}
/** Adds an evidence entry. */
public static YicesResult addEvidenceEntry(YicesResult result, String var, String val) {
EvidenceEntry ee = createEvidenceEntry(var, val);
public static YicesResult addEvidenceEntry(YicesResult result, IExpressionTerm lhs,
IExpressionTerm rhs) {
EvidenceEntry ee = createEvidenceEntry(lhs, rhs);
result.getEvidenceList().add(ee);
return result;
}
/** Returns the value of the variable as given by the evidence. */
public static String getValue(YicesResult result, String variableName) {
for(EvidenceEntry ee : result.getEvidenceList()) {
if(ee.getVariable().equals(variableName)) {
return ee.getValue();
}
}
return null;
}
}
......@@ -176,10 +176,10 @@ public class YicesModelFactory {
}
/** Factory for {@link EvidenceEntry} objects. */
public static EvidenceEntry createEvidenceEntry(String var, String val) {
public static EvidenceEntry createEvidenceEntry(IExpressionTerm lhs, IExpressionTerm rhs) {
EvidenceEntry ee = AF3YicesRunFactory.eINSTANCE.createEvidenceEntry();
ee.setVariable(var);
ee.setValue(val);
ee.setLhs(lhs);
ee.setRhs(rhs);
return ee;
}
......
......@@ -17,12 +17,18 @@ $Id: IntType.java 1270 2011-08-29 08:55:46Z ratiu $
+--------------------------------------------------------------------------*/
package org.fortiss.af3.tools.yices.run;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.boolConst;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.divide;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.intConst;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.stringConst;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.var;
import static org.fortiss.af3.tools.yices.model.YicesModelAccessFacade.addEvidenceEntry;
import static org.fortiss.af3.tools.yices.model.YicesModelFactory.createYicesResult;
import java.util.List;
import java.util.StringTokenizer;
import org.fortiss.af3.expression.model.terms.IExpressionTerm;
import org.fortiss.af3.tools.ToolsActivator;
import org.fortiss.af3.tools.base.IResultBuilder;
import org.fortiss.af3.tools.yices.model.run.YicesResult;
......@@ -51,14 +57,41 @@ public class YicesResultBuilder implements IResultBuilder<YicesResult> {
result = createYicesResult(false);
for(int i = 1; i < lines.size(); i++) {
String line = lines.get(i);
if(line.startsWith("(")) {
if(line.startsWith("(=")) {
StringTokenizer st = new StringTokenizer(line, "() =");
String variableName = st.nextToken();
String variableValue = st.nextToken();
addEvidenceEntry(result, variableName, variableValue);
IExpressionTerm val = parseExpression(variableValue);
addEvidenceEntry(result, var(variableName), val);
}
}
return result;
}
/** Parses a sub-string of the Yices evidence into an expression. */
private IExpressionTerm parseExpression(String expString) {
IExpressionTerm res = null;
if(expString.equals("true") || expString.equals("false")) {
res = boolConst(Boolean.parseBoolean(expString));
} else {
try {
int tmp = Integer.parseInt(expString);
res = intConst(tmp);
} catch(Exception e) {
if(expString.contains("/")) {
int idx = expString.indexOf("/");
IExpressionTerm divident = parseExpression(expString.substring(0, idx));
IExpressionTerm divisor = parseExpression(expString.substring(idx + 1));
res = divide(divident, divisor);
} else {
res = stringConst(expString);
}
}
}
return res;
}
}
......@@ -81,9 +81,4 @@ public class YicesTestBase {
protected void addConstantDeclaration(String name, YicesTypeBase type) {
YicesModelAccessFacade.addConstantDeclaration(currentFile, name, type);
}
/** Returns the value of the variable as given by evidence. */
protected String getValue(YicesResult result, String variableName) {
return YicesModelAccessFacade.getValue(result, variableName);
}
}
......@@ -35,6 +35,7 @@ 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.EvidenceEntry;
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;
......@@ -92,7 +93,7 @@ public class ExpressionsTest extends YicesTestBase {
assertNotNull(result);
assertTrue(result.isSatisfiable());
assertSame(1, result.getEvidenceList().size());
assertEquals("0", getValue(result, "x"));
assertEquals("0", result.getEvidence(0).getRhs().toString());
}
/** Test complex whiteness. */
......@@ -124,7 +125,14 @@ public class ExpressionsTest extends YicesTestBase {
YicesResult result = runYices();
assertNotNull(result);
assertTrue(result.isSatisfiable());
assertSame(1, result.getEvidenceList().size());
assertEquals("0", getValue(result, "x"));
assertSame(6, result.getEvidenceList().size());
EvidenceEntry ee0 = result.getEvidence(0);
assertTrue(ee0.getLhs() instanceof MkRecord);
MkRecord mkRec = (MkRecord)ee0.getLhs();
assertEquals("aBool", mkRec.getMemberNames(0));
assertEquals(boolConst(false), mkRec.getMemberExpressions(0));
assertEquals("anInt", mkRec.getMemberNames(1));
assertEquals(intConst(4), mkRec.getMemberExpressions(1));
}
}
Supports Markdown
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