From fa4ff2a069e1c3184f7cd48be182c3091ade2a00 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 2 Mar 2026 09:37:47 +0100 Subject: [PATCH 1/5] Add a test for parsing quoted symbols --- .../sosy_lab/java_smt/test/ParserTest.java | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/ParserTest.java b/src/org/sosy_lab/java_smt/test/ParserTest.java index 18b13e945e..863565ac37 100644 --- a/src/org/sosy_lab/java_smt/test/ParserTest.java +++ b/src/org/sosy_lab/java_smt/test/ParserTest.java @@ -11,6 +11,7 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; +import static org.sosy_lab.java_smt.api.FormulaType.BooleanType; import com.google.common.collect.ImmutableList; import com.google.common.collect.Iterables; @@ -265,4 +266,23 @@ public void testParseAll_invalid_reservedKeyword() throws SolverException, Inter assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt)); } } + + @Test + public void testParseall_quotedSymbol() { + // Capture a variable from the context + var f = mgr.makeVariable(BooleanType, "my variable"); + var g = mgr.parse("(assert |my variable|)"); + + assertThat(g).isEqualTo(f); + } + + @Test + public void testParseall_quotedSymbol_reparse() { + // Parse a variable that was already defined in the context + var f = mgr.makeVariable(BooleanType, "my variable"); + var str = mgr.dumpFormula(f).toString(); + var g = mgr.parse(str); + + assertThat(g).isEqualTo(f); + } } From 5d4d646a303864e4abe5c04e9351a3ccbbb5e2f7 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 2 Mar 2026 09:41:00 +0100 Subject: [PATCH 2/5] CVC5: Fix parsing issue with quoted symbols We need to always remove quotes before accessing the variable cache. Otherwise, duplicate variables will be created for "|var|" and "var" --- src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java | 2 +- .../sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java | 2 +- src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java | 4 ++-- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index b14646b6f1..1c365064a5 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -583,7 +583,7 @@ public Object convertValue( } /** Variable names (symbols) can be wrapped with "|". This function removes those chars. */ - protected static String dequote(String s) { + public String dequote(String s) { int l = s.length(); if (s.charAt(0) == '|' && s.charAt(l - 1) == '|') { return s.substring(1, l - 1); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 70f6c9d9b5..70e4b86ffa 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -299,7 +299,7 @@ protected RegexFormula encapsulateRegex(Expr pTerm) { return new CVC4RegexFormula(pTerm); } - static String getName(Expr e) { + String getName(Expr e) { checkState(!e.isNull()); if (!e.isConst() && !e.isVariable()) { e = e.getOperator(); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java index 5770ee0f05..8bc8be20e6 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java @@ -120,7 +120,7 @@ private ValueAssignment getAssignmentForUfInstantiation(Expr pKeyExpr) { creator.encapsulateWithTypeOf(pKeyExpr), creator.encapsulateWithTypeOf(valueExpr), creator.encapsulateBoolean(creator.getEnv().mkExpr(Kind.EQUAL, pKeyExpr, valueExpr)), - CVC4FormulaCreator.getName(pKeyExpr), + ((CVC4FormulaCreator) creator).getName(pKeyExpr), creator.convertValue(pKeyExpr, valueExpr), argumentInterpretationBuilder.build()); } @@ -211,7 +211,7 @@ private List getAssignments(Expr pKeyExpr) { creator.encapsulateWithTypeOf(pKeyExpr), creator.encapsulateWithTypeOf(valueExpr), creator.encapsulateBoolean(creator.getEnv().mkExpr(Kind.EQUAL, pKeyExpr, valueExpr)), - CVC4FormulaCreator.getName(pKeyExpr), + ((CVC4FormulaCreator) creator).getName(pKeyExpr), creator.convertValue(pKeyExpr, valueExpr), argumentInterpretationBuilder.build())); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java index 48a822b980..4986e37978 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java @@ -251,7 +251,7 @@ private Map getSymbolSubstitutions( * cached one is recorded in the given substitutions map. */ private void registerNewTermSymbols(Term declaration, Map substitutions) { - final String parsedTermString = declaration.toString(); + final String parsedTermString = creator.dequote(declaration.toString()); final Sort parsedSort = declaration.getSort(); final String parsedSortString = parsedSort.toString(); From deae4b68db5c8e2ea799794e04cbf5f63f563fb6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 15 Mar 2026 15:37:56 +0100 Subject: [PATCH 3/5] Use constant String as parser input --- src/org/sosy_lab/java_smt/test/ParserTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/ParserTest.java b/src/org/sosy_lab/java_smt/test/ParserTest.java index 863565ac37..46d5348b15 100644 --- a/src/org/sosy_lab/java_smt/test/ParserTest.java +++ b/src/org/sosy_lab/java_smt/test/ParserTest.java @@ -280,7 +280,7 @@ public void testParseall_quotedSymbol() { public void testParseall_quotedSymbol_reparse() { // Parse a variable that was already defined in the context var f = mgr.makeVariable(BooleanType, "my variable"); - var str = mgr.dumpFormula(f).toString(); + var str = "(declare-fun |my variable| () Bool) (assert |my variable|)"; var g = mgr.parse(str); assertThat(g).isEqualTo(f); From 83e01bb2942aa2d2b7ced9edbd31ae018fc33de7 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 15 Mar 2026 15:47:37 +0100 Subject: [PATCH 4/5] Rename parseAll tests --- .../sosy_lab/java_smt/test/ParserTest.java | 50 +++++++++---------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/ParserTest.java b/src/org/sosy_lab/java_smt/test/ParserTest.java index 46d5348b15..b7d5ad7a77 100644 --- a/src/org/sosy_lab/java_smt/test/ParserTest.java +++ b/src/org/sosy_lab/java_smt/test/ParserTest.java @@ -32,13 +32,13 @@ public void setUp() { } @Test - public void testParseAll_valid_simpleBoolean() { + public void parseAllSimpleBooleanTest() { String smt = "(assert true)"; assertThat(mgr.parseAll(smt)).containsExactly(bmgr.makeTrue()); } @Test - public void testParseAll_valid_simpleInteger() { + public void parseAllSimpleIntegerTest() { requireIntegers(); String smt = "(declare-fun x () Int)(assert (= x 1))"; assertThat(mgr.parseAll(smt)) @@ -46,7 +46,7 @@ public void testParseAll_valid_simpleInteger() { } @Test - public void testParseAll_valid_defineFun() throws SolverException, InterruptedException { + public void parseAllDefineFunTest() throws SolverException, InterruptedException { requireIntegers(); assume() .withMessage("Solver %s does not support parsing function definitions", solverToUse()) @@ -80,7 +80,7 @@ public void testParseAll_valid_defineFun() throws SolverException, InterruptedEx } @Test - public void testParseAll_valid_multipleAssertions() { + public void parseAllMultipleAssertionsTest() { requireIntegers(); String smt = "(declare-fun x () Int)(assert (> x 0))(assert (< x 10))"; BooleanFormula gt = imgr.greaterThan(imgr.makeVariable("x"), imgr.makeNumber(0)); @@ -89,7 +89,7 @@ public void testParseAll_valid_multipleAssertions() { } @Test - public void testParseAll_valid_differentTypes() { + public void parseAllDifferentTypesTest() { requireIntegers(); String smt = "(declare-fun x () Int)(declare-fun y () Bool)(assert (= x 1))(assert y)"; BooleanFormula intEq = imgr.equal(imgr.makeVariable("x"), imgr.makeNumber(1)); @@ -98,7 +98,7 @@ public void testParseAll_valid_differentTypes() { } @Test - public void testParseAll_valid_functionApplication() { + public void parseAllFunctionApplicationTest() { requireIntegers(); String smt = "(declare-fun f (Int) Int)(declare-fun x () Int)(assert (= (f x) 1))"; IntegerFormula x = imgr.makeVariable("x"); @@ -108,7 +108,7 @@ public void testParseAll_valid_functionApplication() { } @Test - public void testParseAll_valid_bitvector() throws SolverException, InterruptedException { + public void parseAllBitvectorTest() throws SolverException, InterruptedException { requireBitvectors(); String smt = "(declare-fun x () (_ BitVec 8))(assert (= x #x01))"; List parsed = mgr.parseAll(smt); @@ -118,7 +118,7 @@ public void testParseAll_valid_bitvector() throws SolverException, InterruptedEx } @Test - public void testParseAll_valid_quantifier() { + public void parseAllQuantifierTest() { requireQuantifiers(); requireIntegers(); String smt = "(declare-fun p (Int) Bool)(assert (forall ((x Int)) (p x)))"; @@ -130,7 +130,7 @@ public void testParseAll_valid_quantifier() { } @Test - public void testParseAll_valid_string() throws SolverException, InterruptedException { + public void parseAllStringTest() throws SolverException, InterruptedException { requireStrings(); assume() .withMessage("Solver %s does not support parsing strings", solverToUse()) @@ -145,7 +145,7 @@ public void testParseAll_valid_string() throws SolverException, InterruptedExcep } @Test - public void testParseAll_valid_floatingPointFromInt() { + public void parseAllFloatingPointFromIntTest() { requireFloats(); requireIntegers(); String smt = "(declare-fun x () Int)(assert (= x 1.0))"; @@ -154,7 +154,7 @@ public void testParseAll_valid_floatingPointFromInt() { } @Test - public void testParseAll_valid_floatingPointFromReal() { + public void parseAllFloatingPointFromRealTest() { requireFloats(); requireRationals(); String smt = "(declare-fun x () Real)(assert (= x 1.0))"; @@ -163,7 +163,7 @@ public void testParseAll_valid_floatingPointFromReal() { } @Test - public void testParseAll_valid_complexNested() { + public void parseAllComplexNestedTest() { requireIntegers(); String smt = "(declare-fun x () Int)(declare-fun y () Int)(assert (or (= x 1) (and (> y 0) (< y 10))))"; @@ -178,7 +178,7 @@ public void testParseAll_valid_complexNested() { } @Test - public void testParseAll_valid_letBinding() { + public void parseAllLetBindingTest() { requireIntegers(); String smt = "(declare-fun x () Int)(assert (let ((a x)) (= a 1)))"; // For now, just check if it parses without error and returns a formula. @@ -188,19 +188,19 @@ public void testParseAll_valid_letBinding() { } @Test - public void testParseAll_invalid_syntaxError() { + public void parseAllSyntaxErrorTest() { String smt = "(assert (= x 1)"; // Missing closing parenthesis assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt)); } @Test - public void testParseAll_invalid_undeclaredVariable() { + public void parseAllUndeclaredVariableTest() { String smt = "(assert (= x 1))"; // 'x' not declared assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt)); } @Test - public void testParseAll_invalid_typeMismatch() throws SolverException, InterruptedException { + public void parseAllTypeMismatchTest() throws SolverException, InterruptedException { requireIntegers(); String smt = "(declare-fun x () Int)(assert (= x true))"; // Int vs Bool if (solverToUse() == Solvers.Z3) { @@ -215,45 +215,45 @@ public void testParseAll_invalid_typeMismatch() throws SolverException, Interrup } @Test - public void testParseAll_invalid_unknownCommandWithAssertion() { + public void parseAllUnknownCommandWithAssertionTest() { String smt = "(unknown-command)(assert true)"; assertThat(mgr.parseAll(smt)).hasSize(1); assertThat(mgr.parseAll(smt).get(0)).isEqualTo(bmgr.makeTrue()); } @Test - public void testParseAll_invalid_unknownCommand() { + public void parseAllUnknownCommandTest() { String smt = "(unknown-command)"; assertThat(mgr.parseAll(smt)).isEmpty(); } @Test - public void testParseAll_invalid_emptyString() { + public void parseAllEmptyStringTest() { String smt = ""; assertThat(mgr.parseAll(smt)).isEmpty(); } @Test - public void testParseAll_invalid_emptyString2() { + public void parseAllEmptyString2Test() { String smt = " "; assertThat(mgr.parseAll(smt)).isEmpty(); } @Test - public void testParseAll_invalid_emptyString3() { + public void parseAllEmptyString3Test() { String smt = "\n\t \n"; assertThat(mgr.parseAll(smt)).isEmpty(); } @Test - public void testParseAll_invalid_incorrectFunctionArity() { + public void parseAllIncorrectFunctionArityTest() { requireIntegers(); String smt = "(declare-fun f (Int) Int)(assert (f))"; // f expects 1 arg, got 0 assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt)); } @Test - public void testParseAll_invalid_reservedKeyword() throws SolverException, InterruptedException { + public void parseAllReservedKeywordTest() throws SolverException, InterruptedException { requireIntegers(); // 'assert' is a reserved keyword, cannot be used as a function name in most solvers String smt = "(declare-fun assert () Int)(assert (= assert 1))"; @@ -268,7 +268,7 @@ public void testParseAll_invalid_reservedKeyword() throws SolverException, Inter } @Test - public void testParseall_quotedSymbol() { + public void parseAllQuotedSymbolTest() { // Capture a variable from the context var f = mgr.makeVariable(BooleanType, "my variable"); var g = mgr.parse("(assert |my variable|)"); @@ -277,7 +277,7 @@ public void testParseall_quotedSymbol() { } @Test - public void testParseall_quotedSymbol_reparse() { + public void parseAllQuotedSymbolRedefinitionTest() { // Parse a variable that was already defined in the context var f = mgr.makeVariable(BooleanType, "my variable"); var str = "(declare-fun |my variable| () Bool) (assert |my variable|)"; From ca35ed9fd766d9cd07c4a712ad427ce2efd5ed25 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 15 Mar 2026 16:02:12 +0100 Subject: [PATCH 5/5] Move dequote() to Tokenizer --- src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java | 9 --------- src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java | 9 +++++++++ .../java_smt/solvers/cvc4/CVC4FormulaCreator.java | 5 +++-- src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java | 4 ++-- .../java_smt/solvers/cvc5/CVC5FormulaCreator.java | 7 ++++--- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java | 3 ++- .../java_smt/solvers/opensmt/OpenSmtFormulaCreator.java | 3 ++- .../solvers/smtinterpol/SmtInterpolFormulaCreator.java | 5 +++-- 8 files changed, 25 insertions(+), 20 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index 1c365064a5..4d82d77fb4 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -581,13 +581,4 @@ public Object convertValue( @SuppressWarnings("unused") TFormulaInfo pAdditionalF, TFormulaInfo pF) { return convertValue(pF); } - - /** Variable names (symbols) can be wrapped with "|". This function removes those chars. */ - public String dequote(String s) { - int l = s.length(); - if (s.charAt(0) == '|' && s.charAt(l - 1) == '|') { - return s.substring(1, l - 1); - } - return s; - } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java index e549657947..0d7c3912ff 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java +++ b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java @@ -23,6 +23,15 @@ public final class Tokenizer { private Tokenizer() {} + /** Variable names (symbols) can be wrapped with "|". This function removes those chars. */ + public static String dequote(String s) { + int l = s.length(); + if (s.charAt(0) == '|' && s.charAt(l - 1) == '|') { + return s.substring(1, l - 1); + } + return s; + } + /** * Split up a sequence of lisp expressions. * diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 70e4b86ffa..3621dc4feb 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -56,6 +56,7 @@ import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl; +import org.sosy_lab.java_smt.basicimpl.Tokenizer; import org.sosy_lab.java_smt.solvers.cvc4.CVC4Formula.CVC4ArrayFormula; import org.sosy_lab.java_smt.solvers.cvc4.CVC4Formula.CVC4BitvectorFormula; import org.sosy_lab.java_smt.solvers.cvc4.CVC4Formula.CVC4BooleanFormula; @@ -299,12 +300,12 @@ protected RegexFormula encapsulateRegex(Expr pTerm) { return new CVC4RegexFormula(pTerm); } - String getName(Expr e) { + static String getName(Expr e) { checkState(!e.isNull()); if (!e.isConst() && !e.isVariable()) { e = e.getOperator(); } - return dequote(e.toString()); + return Tokenizer.dequote(e.toString()); } @SuppressWarnings("deprecation") diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java index 8bc8be20e6..5770ee0f05 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java @@ -120,7 +120,7 @@ private ValueAssignment getAssignmentForUfInstantiation(Expr pKeyExpr) { creator.encapsulateWithTypeOf(pKeyExpr), creator.encapsulateWithTypeOf(valueExpr), creator.encapsulateBoolean(creator.getEnv().mkExpr(Kind.EQUAL, pKeyExpr, valueExpr)), - ((CVC4FormulaCreator) creator).getName(pKeyExpr), + CVC4FormulaCreator.getName(pKeyExpr), creator.convertValue(pKeyExpr, valueExpr), argumentInterpretationBuilder.build()); } @@ -211,7 +211,7 @@ private List getAssignments(Expr pKeyExpr) { creator.encapsulateWithTypeOf(pKeyExpr), creator.encapsulateWithTypeOf(valueExpr), creator.encapsulateBoolean(creator.getEnv().mkExpr(Kind.EQUAL, pKeyExpr, valueExpr)), - ((CVC4FormulaCreator) creator).getName(pKeyExpr), + CVC4FormulaCreator.getName(pKeyExpr), creator.convertValue(pKeyExpr, valueExpr), argumentInterpretationBuilder.build())); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 40f5a9f5b1..f6e50beaa1 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -65,6 +65,7 @@ import org.sosy_lab.java_smt.api.visitors.TraversalProcess; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl; +import org.sosy_lab.java_smt.basicimpl.Tokenizer; import org.sosy_lab.java_smt.solvers.cvc5.CVC5Formula.CVC5ArrayFormula; import org.sosy_lab.java_smt.solvers.cvc5.CVC5Formula.CVC5BitvectorFormula; import org.sosy_lab.java_smt.solvers.cvc5.CVC5Formula.CVC5BooleanFormula; @@ -383,10 +384,10 @@ String getName(Term e) { // Functions are packaged like this: (functionName arg1 arg2 ...) // But can use |(name)| to enable () inside of the variable name // TODO what happens for function names containing whitespace? - String dequoted = dequote(repr); + String dequoted = Tokenizer.dequote(repr); return Iterables.get(Splitter.on(' ').split(dequoted.substring(1)), 0); } else { - return dequote(repr); + return Tokenizer.dequote(repr); } } @@ -457,7 +458,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { return visitor.visitQuantifier((BooleanFormula) formula, quant, freeVars, fBody); } else if (f.getKind() == Kind.CONSTANT) { - return visitor.visitFreeVariable(formula, dequote(f.toString())); + return visitor.visitFreeVariable(formula, Tokenizer.dequote(f.toString())); } else if (f.getKind() == Kind.APPLY_CONSTRUCTOR) { checkState( diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java index 4986e37978..e42964c8e1 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java @@ -34,6 +34,7 @@ import java.util.regex.Matcher; import java.util.regex.Pattern; import org.sosy_lab.common.collect.Collections3; +import org.sosy_lab.java_smt.basicimpl.Tokenizer; class CVC5Parser { @@ -251,7 +252,7 @@ private Map getSymbolSubstitutions( * cached one is recorded in the given substitutions map. */ private void registerNewTermSymbols(Term declaration, Map substitutions) { - final String parsedTermString = creator.dequote(declaration.toString()); + final String parsedTermString = Tokenizer.dequote(declaration.toString()); final Sort parsedSort = declaration.getSort(); final String parsedSortString = parsedSort.toString(); diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaCreator.java index e2600642d6..5b6484410d 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaCreator.java @@ -21,6 +21,7 @@ import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl; +import org.sosy_lab.java_smt.basicimpl.Tokenizer; import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtFormula.OpenSmtArrayFormula; import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtFormula.OpenSmtBooleanFormula; import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtFormula.OpenSmtIntegerFormula; @@ -358,7 +359,7 @@ public R visit(FormulaVisitor visitor, Formula formula, PTRef f) { if (logic.isVar(f)) { String varName = logic.getSymName(logic.getSymRef(f)); - return visitor.visitFreeVariable(formula, dequote(varName)); + return visitor.visitFreeVariable(formula, Tokenizer.dequote(varName)); } String varName = logic.getSymName(logic.getSymRef(f)); diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java index 43ba707c08..0bd9bda03f 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java @@ -33,6 +33,7 @@ import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl; +import org.sosy_lab.java_smt.basicimpl.Tokenizer; class SmtInterpolFormulaCreator extends FormulaCreator { @@ -212,7 +213,7 @@ public R visit(FormulaVisitor visitor, Formula f, final Term input) { } else if (app.equals(environment.getTheory().mFalse)) { return visitor.visitConstant(f, false); } else if (func.getDefinition() == null) { - return visitor.visitFreeVariable(f, dequote(input.toString())); + return visitor.visitFreeVariable(f, Tokenizer.dequote(input.toString())); } else { throw new UnsupportedOperationException("Unexpected nullary function " + input); } @@ -254,7 +255,7 @@ String getName(Term t) { assert t instanceof ApplicationTerm; return ((ApplicationTerm) t).getFunction().getName(); } else { - return dequote(t.toString()); + return Tokenizer.dequote(t.toString()); } }