Subversion Repositories RISCAL

Compare Revisions

Ignore whitespace Rev 1468 → Rev 1469

/trunk/src/riscal/smt/ExpressionPreprocessor.java
3,7 → 3,7
// A class which is dedicated to translate expressions to an intermediate format.
//
// Author: Franz Reichl <franz.x.reichl@gmail.com>
// $Id: ExpressionPreprocessor.java,v 1.14 2020/10/07 12:17:46 schreine Exp $
// $Id: ExpressionPreprocessor.java,v 1.15 2020/11/21 12:00:15 schreine Exp schreine $
//
// Author: Franz Reichl <franz.x.reichl@gmail.com>
// Copyright (C) 2019-, Research Institute for Symbolic Computation (RISC)
367,7 → 367,7
* Extracts and processes the QuantifiedVariableCore from the given QuantifiedVariable.
* IdentifierSetQuantifiedVar are transformed into IdentifierTypeQuantifiedVar.
* Moreover all conditions part of qVar and the QuantifiedVariableCore are
* extracted, this includes condition generated by the transformation of
* extracted, this includes conditions generated by the transformation of
* IdentifierSetQuantifiedVar.
* Note: The expressions representing the conditions are not yet
* processed.
388,9 → 388,23
{
currentBound.add((ValueSymbol) qvcore.ident.getSymbol());
Expression wexp=qvcore.wexp;
Set<ValueSymbol> free=new HashSet<ValueSymbol>();
if(wexp!=null)
{
Set<ValueSymbol> free=TypedFreeVariables.compute(wexp);
free.addAll(TypedFreeVariables.compute(wexp));
}
if(qvcore instanceof IdentifierSetQuantifiedVar)
{
Expression set=((IdentifierSetQuantifiedVar)qvcore).exp;
Identifier setIdent=new Identifier(qvcore.ident.string);
setIdent.setSymbol(qvcore.ident.getSymbol());
wexp=AST.and(wexp, new InSetExp(new IdentifierExp(setIdent), set));
free.addAll(TypedFreeVariables.compute(set));
free.add((ValueSymbol) qvcore.ident.getSymbol());
}
if(wexp!=null)
{
free.retainAll(currentBound);
condsWithFreeVars.add(new Utilities.Pair<AST.Expression, Set<ValueSymbol>>(wexp, free));
}
410,16 → 424,7
expPremise=AST.and(expPremise, p.first);
it.remove();
}
}
if(qvcore instanceof IdentifierSetQuantifiedVar)
{
String qVarName=variableRenamings.get(qvcore.ident.getSymbol());
if(qVarName==null)
qVarName=qvcore.ident.string;
Expression set=((IdentifierSetQuantifiedVar)qvcore).exp;
Expression inSet=new InSetExp(new IdentifierExp(new Identifier(qVarName)), set);
expPremise=AST.and(expPremise, inSet);
}
}
premises.add(expPremise);
}
if(qVar.exp!=null)
/trunk/src/riscal/smt/RCS/ExpressionPreprocessor.java,v
1,11 → 1,16
head 1.14;
head 1.15;
access;
symbols;
locks
schreine:1.14; strict;
schreine:1.15; strict;
comment @# @;
 
 
1.15
date 2020.11.21.12.00.15; author schreine; state Exp;
branches;
next 1.14;
 
1.14
date 2020.10.07.12.17.46; author schreine; state Exp;
branches;
82,9 → 87,9
@
 
 
1.14
1.15
log
@(empty)
@*** empty log message ***
@
text
@// ---------------------------------------------------------------------------
92,7 → 97,7
// A class which is dedicated to translate expressions to an intermediate format.
//
// Author: Franz Reichl <franz.x.reichl@@gmail.com>
// $Id: ExpressionPreprocessor.java,v 1.13 2020/07/30 10:21:24 schreine Exp $
// $Id: ExpressionPreprocessor.java,v 1.14 2020/10/07 12:17:46 schreine Exp $
//
// Author: Franz Reichl <franz.x.reichl@@gmail.com>
// Copyright (C) 2019-, Research Institute for Symbolic Computation (RISC)
456,7 → 461,7
* Extracts and processes the QuantifiedVariableCore from the given QuantifiedVariable.
* IdentifierSetQuantifiedVar are transformed into IdentifierTypeQuantifiedVar.
* Moreover all conditions part of qVar and the QuantifiedVariableCore are
* extracted, this includes condition generated by the transformation of
* extracted, this includes conditions generated by the transformation of
* IdentifierSetQuantifiedVar.
* Note: The expressions representing the conditions are not yet
* processed.
477,9 → 482,23
{
currentBound.add((ValueSymbol) qvcore.ident.getSymbol());
Expression wexp=qvcore.wexp;
Set<ValueSymbol> free=new HashSet<ValueSymbol>();
if(wexp!=null)
{
Set<ValueSymbol> free=TypedFreeVariables.compute(wexp);
free.addAll(TypedFreeVariables.compute(wexp));
}
if(qvcore instanceof IdentifierSetQuantifiedVar)
{
Expression set=((IdentifierSetQuantifiedVar)qvcore).exp;
Identifier setIdent=new Identifier(qvcore.ident.string);
setIdent.setSymbol(qvcore.ident.getSymbol());
wexp=AST.and(wexp, new InSetExp(new IdentifierExp(setIdent), set));
free.addAll(TypedFreeVariables.compute(set));
free.add((ValueSymbol) qvcore.ident.getSymbol());
}
if(wexp!=null)
{
free.retainAll(currentBound);
condsWithFreeVars.add(new Utilities.Pair<AST.Expression, Set<ValueSymbol>>(wexp, free));
}
499,16 → 518,7
expPremise=AST.and(expPremise, p.first);
it.remove();
}
}
if(qvcore instanceof IdentifierSetQuantifiedVar)
{
String qVarName=variableRenamings.get(qvcore.ident.getSymbol());
if(qVarName==null)
qVarName=qvcore.ident.string;
Expression set=((IdentifierSetQuantifiedVar)qvcore).exp;
Expression inSet=new InSetExp(new IdentifierExp(new Identifier(qVarName)), set);
expPremise=AST.and(expPremise, inSet);
}
}
premises.add(expPremise);
}
if(qVar.exp!=null)
1960,6 → 1970,35
@
 
 
1.14
log
@(empty)
@
text
@d6 1
a6 1
// $Id: ExpressionPreprocessor.java,v 1.13 2020/07/30 10:21:24 schreine Exp $
d370 1
a370 1
* extracted, this includes condition generated by the transformation of
d391 15
a407 1
Set<ValueSymbol> free=TypedFreeVariables.compute(wexp);
d427 1
a427 10
}
if(qvcore instanceof IdentifierSetQuantifiedVar)
{
String qVarName=variableRenamings.get(qvcore.ident.getSymbol());
if(qVarName==null)
qVarName=qvcore.ident.string;
Expression set=((IdentifierSetQuantifiedVar)qvcore).exp;
Expression inSet=new InSetExp(new IdentifierExp(new Identifier(qVarName)), set);
expPremise=AST.and(expPremise, inSet);
}
@
 
 
1.13
log
@(empty)