Skip to content

Commit

Permalink
towards new variable handling in TreeAutomizer, #143
Browse files Browse the repository at this point in the history
  • Loading branch information
@alexandernutz
alexandernutz committed Aug 5, 2017
1 parent 9f46346 commit be2d5f0
Show file tree
Hide file tree
Showing 5 changed files with 548 additions and 649 deletions.
176 changes: 0 additions & 176 deletions ...rary-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HCInVar.java
View file

This file was deleted.

85 changes: 54 additions & 31 deletions ...reeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HCSymbolTable.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,38 +3,42 @@
import java.math.BigInteger;
import java.util.Arrays;
import java.util.List;
import java.util.Map;

import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
import de.uni_freiburg.informatik.ultimate.logic.SMTLIBException;
import de.uni_freiburg.informatik.ultimate.logic.Sort;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.DefaultIcfgSymbolTable;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramConst;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVarOrConst;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.ProgramVarUtils;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.TermTransferrer;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.NestedMap2;
import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.NestedMap3;

public class HCSymbolTable extends DefaultIcfgSymbolTable {

private final ManagedScript mManagedScript;

private final NestedMap2<String, List<Sort>, HornClausePredicateSymbol> mNameToSortsToHornClausePredicateSymbol;
private final NestedMap3<Integer, Integer, Sort, HCInVar> mInPredPosToArgPosToSortToHcInVar;
// private final NestedMap3<Integer, Integer, Sort, HCInVar> mInPredPosToArgPosToSortToHcInVar;
private final NestedMap2<Integer, Sort, HCOutVar> mArgPosToSortToHcOutVar;

// final NestedMap2<HornClausePredicateSymbol, Integer, HCVar> mHCPredSymbolToPositionToHCVar;
private HornClausePredicateSymbol mFalseHornClausePredSym;
private HornClausePredicateSymbol mDontCareHornClausePredSym;
private HornClausePredicateSymbol mTrueHornClausePredSym;

private Map<TermVariable, ApplicationTerm> mTermVarToConst;


public HCSymbolTable(ManagedScript mgdScript) {
super();
mNameToSortsToHornClausePredicateSymbol = new NestedMap2<>();
mInPredPosToArgPosToSortToHcInVar = new NestedMap3<>();
// mInPredPosToArgPosToSortToHcInVar = new NestedMap3<>();
mArgPosToSortToHcOutVar = new NestedMap2<>();
// mHCPredSymbolToPositionToHCVar = new NestedMap2<>();
mManagedScript = mgdScript;
Expand All @@ -47,34 +51,34 @@ public HCSymbolTable(ManagedScript mgdScript) {
mManagedScript.unlock(this);
}

public HCInVar getOrConstructHCInVar(int predPos, int argPos, Sort sort) {
HCInVar result = mInPredPosToArgPosToSortToHcInVar.get(predPos, argPos, sort);

if (result == null) {
final String varName = String.format("HcInVar_%d_%d_%s", predPos, argPos, sort);

mManagedScript.lock(this);
final TermVariable variable = mManagedScript.variable(varName, sort);
final ApplicationTerm defaultConstant = ProgramVarUtils.constructDefaultConstant(mManagedScript, this, sort,
varName);
final ApplicationTerm primedConstant = ProgramVarUtils.constructPrimedConstant(mManagedScript, this, sort,
varName);
mManagedScript.unlock(this);

result = new HCInVar(
predPos,
argPos,
sort,
variable,
defaultConstant,
primedConstant);
mInPredPosToArgPosToSortToHcInVar.put(predPos, argPos, sort, result);
add(result);
}
assert result.getTermVariable().getSort() == sort;

return result;
}
// public HCInVar getOrConstructHCInVar(int predPos, int argPos, Sort sort) {
// HCInVar result = mInPredPosToArgPosToSortToHcInVar.get(predPos, argPos, sort);
//
// if (result == null) {
// final String varName = String.format("HcInVar_%d_%d_%s", predPos, argPos, sort);
//
// mManagedScript.lock(this);
// final TermVariable variable = mManagedScript.variable(varName, sort);
// final ApplicationTerm defaultConstant = ProgramVarUtils.constructDefaultConstant(mManagedScript, this, sort,
// varName);
// final ApplicationTerm primedConstant = ProgramVarUtils.constructPrimedConstant(mManagedScript, this, sort,
// varName);
// mManagedScript.unlock(this);
//
// result = new HCInVar(
// predPos,
// argPos,
// sort,
// variable,
// defaultConstant,
// primedConstant);
// mInPredPosToArgPosToSortToHcInVar.put(predPos, argPos, sort, result);
// add(result);
// }
// assert result.getTermVariable().getSort() == sort;
//
// return result;
// }
public HCOutVar getOrConstructHCOutVar(int argPos, Sort sort) {
HCOutVar result = mArgPosToSortToHcOutVar.get(argPos, sort);

Expand Down Expand Up @@ -171,5 +175,24 @@ private Sort[] transferSorts(Sort[] sorts) {
}
return result;
}

/**
* We store a constant for each TermVariable (so we can use the constant for HoareTripleChecks later).
* Here we update the internal store, and declare the constant.
*/
public void registerTermVariable(TermVariable tv) {
assert tv == new TermTransferrer(mManagedScript.getScript()).transform(tv);
mManagedScript.lock(this);
final ApplicationTerm constant = ProgramVarUtils.constructDefaultConstant(mManagedScript, this, tv.getSort(),
tv.getName());
mManagedScript.unlock(this);
mTermVarToConst.put(tv, constant);
}

public Term getConstForTermVar(TermVariable fv) {
final ApplicationTerm res = mTermVarToConst.get(fv);
assert res != null;
return res;
}

}
Loading

0 comments on commit be2d5f0

Please sign in to comment.