Skip to content

Commit

Permalink
#295, fiddling around with freeze var literals, weaken assertion in C…
Browse files Browse the repository at this point in the history 
…ongruenceClosure.assertHasOnlyWeqVarConstraints(..)
  • Loading branch information
@alexandernutz
alexandernutz committed Jan 28, 2018
1 parent 6c736d0 commit 5361639
Show file tree
Hide file tree
Showing 22 changed files with 403 additions and 113 deletions.
56 changes: 49 additions & 7 deletions ...ltimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqPredicate.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,12 +29,17 @@
import java.util.Collections;
import java.util.Objects;
import java.util.Set;
import java.util.function.Predicate;

import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.EqDisjunctiveConstraint;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.EqNode;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.EqNodeAndFunctionFactory;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.IIcfgSymbolTable;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SubTermFinder;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.predicates.IPredicate;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.predicates.TermVarsProc;
Expand All @@ -51,38 +56,75 @@ public class EqPredicate implements IPredicate {
private final Set<IProgramVar> mVars;
private final Term mClosedFormula;
private final Term mFormula;
private EqNodeAndFunctionFactory mEqNodeAndFunctionFactory;

public EqPredicate(final EqDisjunctiveConstraint<EqNode> constraint, final Set<IProgramVar> vars,
final String[] procedures, final IIcfgSymbolTable symbolTable, final ManagedScript mgdScript) {
final String[] procedures, final IIcfgSymbolTable symbolTable, final ManagedScript mgdScript,
final EqNodeAndFunctionFactory eqNodeAndFunctionFactory) {
assert vars != null;
assert vars.stream().allMatch(Objects::nonNull);
mConstraint = constraint;
mVars = vars;
mProcedures = procedures;


final Term constraintFormula = constraint.getTerm(mgdScript.getScript());
final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(constraintFormula, mgdScript.getScript(),
symbolTable);
mClosedFormula = tvp.getClosedFormula();
mFormula = tvp.getFormula();

// final Term literalDisequalities = getLiteralDisequalities(constraint, mgdScript);
final Term literalDisequalities = eqNodeAndFunctionFactory.getNonTheoryLiteralDisequalities();;

mClosedFormula = SmtUtils.and(mgdScript.getScript(), literalDisequalities, tvp.getClosedFormula());
mFormula = SmtUtils.and(mgdScript.getScript(), literalDisequalities, tvp.getFormula());
}



public EqPredicate(final Term formula, final Set<IProgramVar> vars, final String[] procedures,
final IIcfgSymbolTable symbolTable, final ManagedScript mgdScript) {
final IIcfgSymbolTable symbolTable, final ManagedScript mgdScript,
final EqNodeAndFunctionFactory eqNodeAndFunctionFactory) {
mConstraint = null;
assert vars.stream().allMatch(Objects::nonNull);
mVars = vars;
mProcedures = procedures;

mEqNodeAndFunctionFactory = eqNodeAndFunctionFactory;


final Term acc = formula;
final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(acc, mgdScript.getScript(), symbolTable);
mClosedFormula = tvp.getClosedFormula();
mFormula = tvp.getFormula();

// final Term literalDisequalities = getLiteralDisequalities(constraint, mgdScript);

// final Term literalDisequalities = SmtUtils.and(mgdScript.getScript(),
// CongruenceClosureSmtUtils.createDisequalityTermsForNonTheoryLiterals(mgdScript.getScript(),
// collectLiteralsInFormula(formula)));
final Term literalDisequalities = eqNodeAndFunctionFactory.getNonTheoryLiteralDisequalities();;

mClosedFormula = SmtUtils.and(mgdScript.getScript(), literalDisequalities, tvp.getClosedFormula());
mFormula = SmtUtils.and(mgdScript.getScript(), literalDisequalities, tvp.getFormula());
// mClosedFormula = tvp.getClosedFormula();
// mFormula = tvp.getFormula();

}

private Set<Term> collectLiteralsInFormula(final Term formula) {
final Predicate<Term> pred = term -> term instanceof ConstantTerm
|| mEqNodeAndFunctionFactory.getNonTheoryLiterals().contains(term);
return new SubTermFinder(pred).findMatchingSubterms(formula);
}

// @Deprecated
// private Term getLiteralDisequalities(final EqDisjunctiveConstraint<EqNode> constraint,
// final ManagedScript mgdScript) {
// final Term literalDisequalities = SmtUtils.and(mgdScript.getScript(),
// CongruenceClosureSmtUtils.createDisequalityTermsForNonTheoryLiterals(
// mgdScript.getScript(),
// constraint.getAllLiteralNodes().stream()
// .map(node -> node.getTerm()).collect(Collectors.toSet())));
// return literalDisequalities;
// }


@Override
public String[] getProcedures() {
Expand Down
10 changes: 7 additions & 3 deletions ...mate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqStateFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,12 +112,14 @@ public ManagedScript getManagedScript() {
}

public EqPredicate stateToPredicate(final EqState state) {
// TODO: what procedures does the predicate need?
return new EqPredicate(
getEqConstraintFactory().getDisjunctiveConstraint(Collections.singleton(state.getConstraint())),
state.getConstraint().getVariables(getSymbolTable()),
null,
getSymbolTable(),
getManagedScript()); // TODO: what procedures does the predicate need?
getManagedScript(),
mEqNodeAndFunctionFactory);
}

public EqPredicate statesToPredicate(final List<EqState> states) {
Expand All @@ -129,18 +131,20 @@ public EqPredicate statesToPredicate(final List<EqState> states) {
constraints.add(state.getConstraint());
}

// TODO: what procedures does the predicate need?
return new EqPredicate(
getEqConstraintFactory().getDisjunctiveConstraint(constraints),
variables,
null,
getSymbolTable(),
getManagedScript()); // TODO: what procedures does the predicate need?
getManagedScript(),
mEqNodeAndFunctionFactory);
}

public EqPredicate termToPredicate(final Term spPrecise,
final IPredicate postConstraint) {
return new EqPredicate(spPrecise, postConstraint.getVars(), postConstraint.getProcedures(), mSymbolTable,
mMgdScript);
mMgdScript, mEqNodeAndFunctionFactory);

}

Expand Down
21 changes: 17 additions & 4 deletions .../analysis/abstractinterpretationv2/domain/transformula/vp/TransFormulaConverterCache.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transitions.UnmodifiableTransFormula;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.ProgramVarUtils;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.Substitution;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair;
Expand Down Expand Up @@ -98,6 +99,7 @@ private EqTransitionRelation convertTransformulaToEqTransitionRelation(final Tra

protected Pair<Term, Term> makeShiftVariableSubstitution(final ManagedScript mgdScript, final TransFormula tf,
final EqDisjunctiveConstraint<EqNode> resultConstraint) {

final Map<Term, Term> substitutionMapping = new HashMap<>();

for (final Entry<IProgramVar, TermVariable> iv : tf.getOutVars().entrySet()) {
Expand All @@ -107,9 +109,6 @@ protected Pair<Term, Term> makeShiftVariableSubstitution(final ManagedScript mgd
substitutionMapping.put(iv.getValue(), iv.getKey().getDefaultConstant());
}
for (final TermVariable auxVar : tf.getAuxVars()) {
// final String constName = "tf2EqTR_" + auxVar.getName();
// mgdScript.declareFun(this, constName, new Sort[0], auxVar.getSort());
// substitutionMapping.put(auxVar, mgdScript.term(this, constName));
final Term auxVarConst = ProgramVarUtils.getAuxVarConstant(mgdScript, auxVar);
substitutionMapping.put(auxVar, auxVarConst);
}
Expand All @@ -120,7 +119,21 @@ protected Pair<Term, Term> makeShiftVariableSubstitution(final ManagedScript mgd
assert rcClosed.getFreeVars().length == 0;

final Term tfClosed = ((UnmodifiableTransFormula) tf).getClosedFormula();
return new Pair<>(tfClosed, rcClosed);


// final Set<Term> literalTerms = resultConstraint.getAllLiteralNodes().stream()
// .map(node -> node.getTerm())
// .collect(Collectors.toSet());
// final List<Term> nontheoryLiteralDisequalities =
// CongruenceClosureSmtUtils.createDisequalityTermsForNonTheoryLiterals(mgdScript.getScript(),
// literalTerms);

// we have to stregthen the transFormula with the disequalities between the "literals" we introduced ourselves
final Term ante = SmtUtils.and(mgdScript.getScript(), tfClosed,
// SmtUtils.and(mgdScript.getScript(), nontheoryLiteralDisequalities));
SmtUtils.and(mgdScript.getScript(), mEqNodeAndFunctionFactory.getNonTheoryLiteralDisequalities()));

return new Pair<>(ante, rcClosed);
}

private boolean transformulaImpliesResultConstraint(final TransFormula tf,
Expand Down
13 changes: 7 additions & 6 deletions ...k/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/VPDomain.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.EqConstraintFactory;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.EqNode;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.EqNodeAndFunctionFactory;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.WeqCcManager;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.WeqSettings;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.CfgSmtToolkit;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.IIcfgSymbolTable;
Expand All @@ -61,15 +62,13 @@
public class VPDomain<ACTION extends IIcfgTransition<IcfgLocation>>
implements IAbstractDomain<EqState, ACTION> {

public static final boolean DEBUG = true;

private final EqPostOperator<ACTION> mPost;
private final VPMergeOperator mMerge;
private final ILogger mLogger;

private final ManagedScript mManagedScript;
private final IIcfgSymbolTable mSymboltable;
private final boolean mDebugMode = true;
private final boolean mDebugMode;

private final EqConstraintFactory<EqNode> mEqConstraintFactory;
private final EqNodeAndFunctionFactory mEqNodeAndFunctionFactory;
Expand All @@ -84,23 +83,25 @@ public class VPDomain<ACTION extends IIcfgTransition<IcfgLocation>>
* @param logger
* @param services
* @param csToolkit
* @param additionalLiterals
* @param nonTheoryLiterals
* This set of program constants will be viewed as "literals" by the analysis. Literals are constants that
* are unequal from all other constants.
*/
public VPDomain(final ILogger logger, final IUltimateServiceProvider services, final CfgSmtToolkit csToolkit,
final Set<IProgramConst> additionalLiterals) {
final Set<IProgramConst> nonTheoryLiterals) {
mLogger = logger;
mManagedScript = csToolkit.getManagedScript();
mMerge = new VPMergeOperator();
mSymboltable = csToolkit.getSymbolTable();
mCsToolkit = csToolkit;
mServices = services;

mDebugMode = WeqCcManager.areAssertsEnabled();


final IPreferenceProvider ups = mServices.getPreferenceProvider(Activator.PLUGIN_ID);

mEqNodeAndFunctionFactory = new EqNodeAndFunctionFactory(services, mManagedScript, additionalLiterals);
mEqNodeAndFunctionFactory = new EqNodeAndFunctionFactory(services, mManagedScript, nonTheoryLiterals);
mEqConstraintFactory = new EqConstraintFactory<>(mEqNodeAndFunctionFactory, mServices, mManagedScript,
prepareWeqSettings(ups), mDebugMode);
mEqStateFactory = new EqStateFactory(mEqNodeAndFunctionFactory, mEqConstraintFactory, mSymboltable,
Expand Down
25 changes: 18 additions & 7 deletions ...er/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/IcfgTransitionTransformer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,8 @@ private void process() {

private void processGraph() {
// we need to create new return transitions after new call transitions have been created
final List<Triple<OUTLOC, OUTLOC, IcfgEdge>> rtrTransitions = new ArrayList<>();
// final List<Triple<OUTLOC, OUTLOC, IcfgEdge>> rtrTransitions = new ArrayList<>();
final List<Triple<OUTLOC, OUTLOC, IcfgEdge>> oldReturnTransitions = new ArrayList<>();

final IcfgLocationIterator<INLOC> iter = new IcfgLocationIterator<>(mInputIcfg.getInitialNodes());
while (iter.hasNext()) {
Expand All @@ -99,19 +100,29 @@ private void processGraph() {
@SuppressWarnings("unchecked")
final OUTLOC newTarget = mTransformedIcfgBuilder.createNewLocation((INLOC) oldTransition.getTarget());

if (oldTransition instanceof IIcfgReturnTransition<?, ?>) {
oldReturnTransitions.add(new Triple<>(newSource, newTarget, oldTransition));
continue;
}

final IcfgEdge transformedTransition = transform(oldTransition, newSource, newTarget);

if (oldTransition instanceof IIcfgReturnTransition<?, ?>) {
rtrTransitions.add(new Triple<>(newSource, newTarget, transformedTransition));
} else {
// if (oldTransition instanceof IIcfgReturnTransition<?, ?>) {
// rtrTransitions.add(new Triple<>(newSource, newTarget, transformedTransition));
// } else {
mTransformedIcfgBuilder.createNewTransitionWithNewProgramVars(newSource, newTarget,
transformedTransition);
}
// }
}
}

rtrTransitions.forEach(
a -> mTransformedIcfgBuilder.createNewTransitionWithNewProgramVars(a.getFirst(), a.getSecond(), a.getThird()));
for (final Triple<OUTLOC, OUTLOC, IcfgEdge> returnTrans : oldReturnTransitions) {
final IcfgEdge transformedTransition = transform(returnTrans.getThird(), returnTrans.getFirst(), returnTrans.getSecond());
mTransformedIcfgBuilder.createNewTransitionWithNewProgramVars(returnTrans.getFirst(),
returnTrans.getSecond(), transformedTransition);
}
// rtrTransitions.forEach(
// a -> mTransformedIcfgBuilder.createNewTransitionWithNewProgramVars(a.getFirst(), a.getSecond(), a.getThird()));
}

/**
Expand Down
36 changes: 21 additions & 15 deletions .../uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/FreezeVarInitializer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramNonOldVar;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils;
import de.uni_freiburg.informatik.ultimate.util.datastructures.CrossProducts;
import de.uni_freiburg.informatik.ultimate.util.datastructures.DataStructureUtils;

/**
Expand Down Expand Up @@ -79,18 +80,12 @@ protected IcfgEdge transform(final IcfgEdge oldTransition, final OUTLOC newSourc
final ComputeInitializingTerm cit =
new ComputeInitializingTerm(mFreezeVarTofreezeVarLit, mValidArray, oldTransformula);

// if (!freezeVarTofreezeVarLit.isEmpty()) {
// mFreezeVarInVars.put(validArray, validArray.getTermVariable());
// mFreezeVarOutVars.put(validArray, validArray.getTermVariable());
// }

final Map<IProgramVar, TermVariable> newInVars = new HashMap<>(oldTransformula.getInVars());
newInVars.putAll(cit.getFreezeVarInVars());
// newInVars.putAll(mFreezeVarInVars);

final Map<IProgramVar, TermVariable> newOutVars = new HashMap<>(oldTransformula.getOutVars());
newOutVars.putAll(cit.getFreezeVarOutVars());
// newOutVars.putAll(mFreezeVarOutVars);

/*
* Note that the symbol table will be automatically updated with the new constants by the
Expand All @@ -105,6 +100,9 @@ protected IcfgEdge transform(final IcfgEdge oldTransition, final OUTLOC newSourc
oldTransformula.getAuxVars().isEmpty());

// TODO: do we need to lock the mgdscript here??
/*
* conjoin the original transformula with the initializing term
*/
final Term newFormula = SmtUtils.and(script, oldTransformula.getFormula(), cit.getInitializingTerm());

newTfBuilder.setFormula(newFormula);
Expand Down Expand Up @@ -173,20 +171,28 @@ private void computeInitializingTerm(final Map<IProgramNonOldVar, IProgramConst>
*/
// TODO have to get the valid Termvariable from the Transformula or make a new one!
final Term select = SmtUtils.select(mMgdScript.getScript(), validArrayTv, frzLit);
// TODO -- is this the right way to get a constant?
// final Term one = Rational.ONE.toTerm(mMgdScript.getScript().sort("Real"));
// final Term trueTerm = mMgdScript.term(this, "true");
// final Term one = mMgdScript.getScript().numeral(BigInteger.ONE);
// final AffineTerm at = new AffineTerm(select.getSort(), Rational.ONE);
// final Term one = at.toTerm(mMgdScript.getScript());
final Term one = SmtUtils.constructIntValue(mMgdScript.getScript(), BigInteger.ONE);


// initializingEquations.add(SmtUtils.binaryEquality(mMgdScript.getScript(), select, trueTerm));
initializingEquations.add(SmtUtils.binaryEquality(mMgdScript.getScript(), select, one));
}

mInitializingTerm = SmtUtils.and(mMgdScript.getScript(), initializingEquations);

/*
* furthermore add disequalities between all freeze var literals
*/
final List<Term> freezeLitDisequalities = new ArrayList<>();
if (HeapSepSettings.ASSUME_FREEZE_VAR_LIT_DISEQUALITIES_AT_INIT_EDGES) {
for (final Entry<IProgramConst, IProgramConst> en : CrossProducts.binarySelectiveCrossProduct(
new HashSet<>(freezeVarTofreezeVarLit.values()), false, false)) {
freezeLitDisequalities.add(
mMgdScript.getScript().term("not",
mMgdScript.term(this, "=", en.getKey().getTerm(), en.getValue().getTerm())));
}
}

mInitializingTerm = SmtUtils.and(mMgdScript.getScript(),
SmtUtils.and(mMgdScript.getScript(), initializingEquations),
SmtUtils.and(mMgdScript.getScript(), freezeLitDisequalities));

mMgdScript.unlock(this);

Expand Down
Loading

0 comments on commit 5361639

Please sign in to comment.