Commit 34d7096e authored by Sebastian Voss's avatar Sebastian Voss
Browse files

adapted YicesTextGenerator, w.r.t to quantifiers

parent f6775458
......@@ -66,7 +66,7 @@ import org.fortiss.af3.tools.yices.model.types.YicesTypeBase;
* @author ratiu
* @author $Author: hoelzl $
* @version $Rev: 18709 $
* @ConQAT.Rating GREEN Hash: 3821093B26C7FCA05BAD69FA1A4F326B
* @ConQAT.Rating GREEN Hash: 798C4ED603A0B219119F22E36AC5B0A2
*/
public class YicesTextGenerator implements ITextGenerator<YicesFile> {
......@@ -266,7 +266,11 @@ public class YicesTextGenerator implements ITextGenerator<YicesFile> {
private void generateText(Writer w, Assert assertCommand) throws IOException,
UnknownLanguageFragmentException {
w.append("(assert ");
w.append(convertExpressionToString(assertCommand.getExpression()));
if(!(assertCommand.getExpression() instanceof Forall)) {
w.append(convertExpressionToString(assertCommand.getExpression()));
} else {
generateText(w, (Forall)assertCommand.getExpression());
}
w.append(")\n");
}
......@@ -326,10 +330,9 @@ public class YicesTextGenerator implements ITextGenerator<YicesFile> {
} else if(term instanceof SelectTerm) {
StringBuffer sb = new StringBuffer("(select (");
SelectTerm st = (SelectTerm)term;
sb.append(st.getIdentifier() + ") " + st.getField() + ")");
return sb.toString();
} else if(term instanceof Function) {
StringBuffer sb = new StringBuffer("(");
Function function = (Function)term;
......
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