Skip to content

Commit

Permalink
Princess: Renamed list of (non-boolean) variables in PrincessAbstract…
Browse files Browse the repository at this point in the history
…Prover from intSymbols` to `theorySymbols` as it may not only contain integer variables.
  • Loading branch information
daniel-raffler committed Sep 10, 2024
1 parent 96c4d61 commit 296d8e4
Showing 1 changed file with 6 additions and 6 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ protected void popImpl() {
// we have to recreate symbols on lower levels, because JavaSMT assumes "global" symbols.
Level level = trackingStack.pop();
api.addBooleanVariables(asScala(level.booleanSymbols));
api.addConstants(asScala(level.intSymbols));
api.addConstants(asScala(level.theorySymbols));
level.functionSymbols.forEach(api::addFunction);
if (!trackingStack.isEmpty()) {
trackingStack.peek().mergeWithHigher(level);
Expand Down Expand Up @@ -213,12 +213,12 @@ void addSymbol(IFormula f) {
}
}

/** add external definition: integer variable. */
/** add external definition: theory variable (integer, rational, string, etc). */
void addSymbol(ITerm f) {
Preconditions.checkState(!closed);
api.addConstant(f);
if (!trackingStack.isEmpty()) {
trackingStack.peek().intSymbols.add(f);
trackingStack.peek().theorySymbols.add(f);
}
}

Expand All @@ -233,21 +233,21 @@ void addSymbol(IFunction f) {

static class Level {
final List<IFormula> booleanSymbols = new ArrayList<>();
final List<ITerm> intSymbols = new ArrayList<>();
final List<ITerm> theorySymbols = new ArrayList<>();
final List<IFunction> functionSymbols = new ArrayList<>();

Level() {}

/** add higher level to current level, we keep the order of creating symbols. */
void mergeWithHigher(Level other) {
this.booleanSymbols.addAll(other.booleanSymbols);
this.intSymbols.addAll(other.intSymbols);
this.theorySymbols.addAll(other.theorySymbols);
this.functionSymbols.addAll(other.functionSymbols);
}

@Override
public String toString() {
return String.format("{%s, %s, %s}", booleanSymbols, intSymbols, functionSymbols);
return String.format("{%s, %s, %s}", booleanSymbols, theorySymbols, functionSymbols);
}
}
}

0 comments on commit 296d8e4

Please sign in to comment.