diff --git a/src/org/sosy_lab/java_smt/api/FormulaManager.java b/src/org/sosy_lab/java_smt/api/FormulaManager.java index 0b3c7e697b..a13602c230 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FormulaManager.java @@ -193,6 +193,9 @@ default BooleanFormula makeDistinct(Formula... pArgs) { default BooleanFormula parse(String s) throws IllegalArgumentException { List formulas = parseAll(s); checkArgument(!formulas.isEmpty(), "No assertion found in the SMTLIB string."); + checkArgument( + formulas.size() == 1, + "More than one assertion found in the SMT-LIB string, " + "please use parseAll(String)."); return Objects.requireNonNull(Iterables.getOnlyElement(formulas)); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index 1bb109f98f..ad7ae15547 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -10,6 +10,12 @@ import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; +import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.SMTLIB2ProgramState.ASSERT_MODE; +import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.SMTLIB2ProgramState.EXITED_STATE; +import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.SMTLIB2ProgramState.RESULT_MODE; +import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.SMTLIB2ProgramState.SAT_MODE; +import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.SMTLIB2ProgramState.START_MODE; +import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.SMTLIB2ProgramState.UNSAT_MODE; import com.google.common.annotations.VisibleForTesting; import com.google.common.base.CharMatcher; @@ -396,21 +402,38 @@ private String sanitize(String formulaStr) { List tokens = Tokenizer.tokenize(formulaStr); StringBuilder builder = new StringBuilder(); - int pos = 0; // index of the current token + + // SMTLIB2ProgramState tracks that the SMTLIB2 query conforms to the rules outlined in the + // standard. SMTLIB2ProgramStateMachine models the + SMTLIB2ProgramStateMachine smtLibStateMachine = new SMTLIB2ProgramStateMachine(false); for (String token : tokens) { - if (Tokenizer.isSetLogicToken(token)) { - // Skip the (set-logic ...) command at the beginning of the input - Preconditions.checkArgument(pos == 0); + if (Tokenizer.isSetInfoToken(token)) { + // set-info call is allowed to be the very first command in the benchmark, but can also + // appear repeatedly throughout a SMT2 program + // Technically it is even required to be the very first command, and it must set the + // :smt-lib-version attribute. See SMT-LIB 2.7 ยง3.11.3 + // TODO: check that version >= 2 for attribute :smt-lib-version? + smtLibStateMachine.applyGSIOCommand(); + + } else if (Tokenizer.isSetLogicToken(token)) { + // (set-logic ...) commands must appear before an assertion is made. They may appear + // throughout an SMT-LIB2 program to set the 'current logic' to a new logic, but the 'reset' + // command has to be used before doing so every time. + // The logic 'ALL' is the logic describing all available logics of a solver. + // The following commands are allowed to be used before the very first 'set-logic': + // echo, reset, reset-assertions, get-info, get-option, set-info, set-option + smtLibStateMachine.applySetLogicCommand(); } else if (Tokenizer.isExitToken(token)) { // Skip the (exit) command at the end of the input - Preconditions.checkArgument(pos == tokens.size() - 1); + smtLibStateMachine.applyExitCommand(); } else if (Tokenizer.isDeclarationToken(token) || Tokenizer.isDefinitionToken(token) || Tokenizer.isAssertToken(token)) { // Keep only declaration, definitions and assertion + smtLibStateMachine.applyAssertDeclareCommands(); builder.append(token).append('\n'); } else if (Tokenizer.isForbiddenToken(token)) { @@ -421,16 +444,20 @@ private String sanitize(String formulaStr) { // moment. If needed, this feature can still be added later. String message; if (Tokenizer.isPushToken(token)) { + smtLibStateMachine.applyPCommand(); message = "(push ...)"; } else if (Tokenizer.isPopToken(token)) { + smtLibStateMachine.applyPCommand(); message = "(pop ...)"; } else if (Tokenizer.isResetAssertionsToken(token)) { + smtLibStateMachine.applyResetAssertionsCommand(); message = "(reset-assertions)"; } else if (Tokenizer.isResetToken(token)) { + smtLibStateMachine.applyResetCommand(); message = "(reset)"; } else { // Should be unreachable - throw new UnsupportedOperationException(); + throw new UnsupportedOperationException("Unknown token " + checkNotNull(token)); } throw new IllegalArgumentException( String.format("SMTLIB command '%s' is not supported when parsing formulas.", message)); @@ -438,8 +465,8 @@ private String sanitize(String formulaStr) { } else { // Remove everything else, such as unknown or solver-specific commands, comments, etc. } - pos++; } + return builder.toString(); } @@ -811,4 +838,213 @@ public final String unescape(String pVar) { } return pVar; // unchanged } + + public enum SMTLIB2ProgramState { + /** Initial state. Can be re-entered using the 'reset' command. */ + START_MODE, + /** + * Mode entered after the initial setup is done by executing the 'set-logic' command. In this + * state, formulas can be defined/asserted etc. + */ + ASSERT_MODE, + /** Mode entered after SAT has been returned after calling 'check-set'. */ + SAT_MODE, + /** Mode entered after UNSAT has been returned after calling 'check-set'. */ + UNSAT_MODE, + /** + * Joined alternative to SAT_MODE and UNSAT_MODE. Used if we don't solve, i.e. don't know + * whether we are in a SAT/UNSAT state after 'check-sat'. + */ + RESULT_MODE, + /** + * State after 'exit' has been called. No operations are possible anymore and everything ends in + * an error. + */ + EXITED_STATE + } + + /** + * As defined by the SMT-LIB2 standard + * an SMT-LIB2 program is allowed to utilize certain commands only if certain preconditions are + * met. This state-machine models this in two ways: + * + *

- a lenient parse mode, that replaces the SAT_MODE and UNSAT_MODE with a joined RESULT_MODE, + * as we are only interested in the resulting {@link BooleanFormula}s and don't solve the queries, + * hence we can't decide whether we are in SAT/UNSAT_MODE. + * + *

- parsing including solving utilizes the SAT_MODE and UNSAT_MODE after 'check-sat'. + * + *

All methods return either the new state (which may be equal to the old), or throw a {@link + * IllegalArgumentException} with an error message explaining the problem. + */ + static class SMTLIB2ProgramStateMachine { + + private SMTLIB2ProgramState state = START_MODE; + + private final boolean strictLogicSelectionRequired; + + // TODO: track current logic + // private LOGIC currentLogic; + + private static final String EXIT_ERROR_MSG = + "It is not allowed to call any more SMT-LIB2 commands " + "after 'exit' has been used"; + + /** + * Creates a new SMTLIB2ProgramStateMachine for a new SMTLIB2 query (parsing or dumping). + * + * @param pRequiresStrictLogicSelection if false, no logic has to be set before switching to + * assertion mode, assuming logic 'ALL' implicitly. If true, logic selection is strictly + * required before defining, declaring or asserting terms etc., as specified by the SMT-LIB2 + * standard. + */ + SMTLIB2ProgramStateMachine(boolean pRequiresStrictLogicSelection) { + strictLogicSelectionRequired = pRequiresStrictLogicSelection; + } + + /** + * Transitions into the SMTLIB2 program state after the 'exit' command, that disallows any + * further commands. + */ + void applyExitCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + state = EXITED_STATE; + } + + /** + * Used to get the new SMTLIB2 program state for commands: 'declare-*', 'define-*', and + * 'assert'. + */ + void applyAssertDeclareCommands() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + if (state != START_MODE) { + state = ASSERT_MODE; + } else if (!strictLogicSelectionRequired) { + checkArgument(state == START_MODE); + // Not part of the logic above as we still want to reject later 'set-logic' commands! + state = ASSERT_MODE; + } else { + throw new IllegalArgumentException( + "SMT-LIB2 command 'assert', or any of the 'declare-*' and 'define-*' commands are only" + + " allowed to be used after a logic has been set via the 'set-logic' command"); + } + } + + /** Used to get the new SMTLIB2 program state for command: 'check-sat'. */ + void applyCheckSatCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + if (state != START_MODE || !strictLogicSelectionRequired) { + // Switches to SAT or UNSAT mode, but we don't solve, we parse, + // hence we use a collective state. + // Also, if we allow implicit logic selection, no assertion is required for trivial results + state = RESULT_MODE; + } else { + throw new IllegalArgumentException( + "SMT-LIB2 command 'check-sat' is only allowed to be used after a logic has been set via" + + " the 'set-logic' command"); + } + } + + /** + * Used to get the new SMTLIB2 program state for the 'echo' command. This options transition + * always into the current state and calling this method is not necessary. + */ + void applyEchoCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + } + + /** Used to transition into the new SMTLIB2 program state for the 'get-assertion' command. */ + void applyGetAssertionCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + // Funnily, you are allowed to use 'get-assertion' without asserting something. + // TODO: Section 4.1.7 of the standard (2.6) says: + // "The command can be issued only if the :produce-assertions option, which is set to + // false by default, is set to true." + checkArgument( + state != START_MODE || !strictLogicSelectionRequired, + "SMT-LIB2 command 'get-assertion' is only allowed to be used after a logic has been set" + + " via the 'set-logic' command"); + /* + checkArgument(options.contains(PRODUCE_ASSERTIONS), + "SMT-LIB2 command 'get-assertion' is only allowed to be used after the " + + ":produce-assertions option has been set"); + */ + } + + /** + * Used to transition into the new SMTLIB2 program state for commands: 'get-assignment', + * 'get-model', and 'get-value'. + */ + void applyGAMVCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + checkArgument( + state == SAT_MODE || state == RESULT_MODE, + "SMT-LIB2 commands 'get-model', 'get-assignment', and 'get-value' are only allowed to be" + + " used after 'check-sat' has been called and returned SAT"); + } + + /** + * Used to transition into the new SMTLIB2 program state for commands: 'get-info', 'get-option', + * 'set-info', 'set-option'. These options transition always into the current state and calling + * this method is not necessary. + */ + void applyGSIOCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + } + + /** + * Used to transition into the new SMTLIB2 program state for commands: 'get-unsat-*', + * 'get-proof'. + */ + void applyGPUCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + checkArgument( + state == UNSAT_MODE || state == RESULT_MODE, + "SMT-LIB2 command 'get-proof' and all 'get-unsat-*' commands are only allowed to be" + + " used after 'check-sat' has been called and returned UNSAT"); + } + + /** Used to transition into the new SMTLIB2 program state for the 'push' and 'pop' commands. */ + void applyPCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + if (state != START_MODE || !strictLogicSelectionRequired) { + state = ASSERT_MODE; + } else { + throw new IllegalArgumentException( + "SMT-LIB2 commands 'push' and 'pop' are only allowed to " + + "be used once a logic has been set"); + } + } + + /** Used to transition into the new SMTLIB2 program state for the 'reset' command. */ + void applyResetCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + state = START_MODE; + } + + /** Used to transition into the new SMTLIB2 program state for the 'reset-assertions' command. */ + void applyResetAssertionsCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + if (state != START_MODE && state != ASSERT_MODE) { + state = ASSERT_MODE; + } + } + + /** Used to transition into the new SMTLIB2 program state for the 'set-logic' command. */ + void applySetLogicCommand() { + checkArgument(state != EXITED_STATE, EXIT_ERROR_MSG); + if (state == START_MODE) { + state = ASSERT_MODE; + } else if (!strictLogicSelectionRequired) { + // We allowed implicit logic selection and assumed 'ALL' already (by asserting or defining) + throw new IllegalArgumentException( + "SMT-LIB2 command 'set-logic' is not allowed to be used after declaring, defining or " + + "asserting terms"); + } else { + throw new IllegalArgumentException( + "SMT-LIB2 command 'set-logic' is not allowed to be used more than once without calling" + + " 'reset' first"); + } + } + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java index e549657947..979af71955 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java +++ b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java @@ -155,6 +155,10 @@ public static boolean isSetLogicToken(String token) { return matchesOneOf(token, "set-logic"); } + public static boolean isSetInfoToken(String token) { + return matchesOneOf(token, "set-info"); + } + /** * Check if the token is a function or variable declaration. * diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java index 2af48115d8..2e5c50809e 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java @@ -163,6 +163,11 @@ static void loadLibrary(Consumer pLoader) { */ private static Options setFurtherOptions(Options pOptions, String pFurtherOptions) throws InvalidConfigurationException { + + if (pFurtherOptions.isEmpty()) { + return pOptions; + } + MapSplitter optionSplitter = Splitter.on(',') .trimResults() diff --git a/src/org/sosy_lab/java_smt/test/SanitizerTest.java b/src/org/sosy_lab/java_smt/test/SanitizerTest.java index d57f3a1545..2c9d53170e 100644 --- a/src/org/sosy_lab/java_smt/test/SanitizerTest.java +++ b/src/org/sosy_lab/java_smt/test/SanitizerTest.java @@ -36,19 +36,53 @@ public void logicTest() throws SolverException, InterruptedException { String wrongLogic = "(set-logic QF_UF)" + "(declare-const v Int)" + "(assert (= v 3))"; assertThatFormula(mgr.parse(wrongLogic)).isEquivalentTo(expected); - // Try setting the logic when it's not the beginning of the input string + // Try setting the logic when it's not the beginning of the input string (this is allowed as + // long as nothing has been declared/defined/asserted) String logicAfterOption = "(set-option :produce-models true)" + "(set-logic ALL)" + "(declare-const v Int)" + "(assert (= v 3))"; - assertThrows(IllegalArgumentException.class, () -> mgr.parse(logicAfterOption)); + assertThatFormula(mgr.parse(logicAfterOption)).isEquivalentTo(expected); + } + // 'set-logic' may only be used once without calling 'reset', and has to be called before + // certain other commands are used (according to the standard). But we allow some leniency due + // to many solvers not sticking to this and assume logic 'ALL' if none has been chosen before + // the first define/declare/assert command. + @Test + public void logicSelectionFailingTest() { // Try setting the logic when it's already been set + // First try broadest followed by more strict logic String logicTwice = - "(set-logic ALL)" + "(declare-const v Int)" + "(set-logic QF_UF)" + " (assert (= v 3))"; + "(set-logic ALL)" + "(set-logic QF_UF)" + "(declare-const v Int)" + " (assert (= v 3))"; assertThrows(IllegalArgumentException.class, () -> mgr.parse(logicTwice)); + // Try the reverse (restricted logic to more broad) + String logicTwice2 = + "(set-logic QF_UF)" + "(set-logic ALL)" + "(declare-const v Int)" + " (assert (= v 3))"; + assertThrows(IllegalArgumentException.class, () -> mgr.parse(logicTwice2)); + + // Try setting the logic when it's already been set after something has been declared + String logicAfterDeclareDouble = + "(set-logic ALL)" + "(declare-const v Int)" + "(set-logic QF_UF)" + " (assert (= v 3))"; + assertThrows(IllegalArgumentException.class, () -> mgr.parse(logicAfterDeclareDouble)); + + // Try setting the logic after something has been declared (i.e. logic set implicitly) + String logicAfterDeclare = "(declare-const v Int)" + "(set-logic QF_UF)" + " (assert (= v 3))"; + assertThrows(IllegalArgumentException.class, () -> mgr.parse(logicAfterDeclare)); + + // Try setting the logic after something has been asserted + String logicAfterAssert = "(declare-const v Int)" + " (assert (= v 3))" + "(set-logic QF_UF)"; + assertThrows(IllegalArgumentException.class, () -> mgr.parse(logicAfterAssert)); + + // Try setting the logic after something has been defined + String logicAfterDefine = "(define-const v Int)" + "(set-logic QF_UF)" + " (assert (= v 3))"; + assertThrows(IllegalArgumentException.class, () -> mgr.parse(logicAfterDefine)); + } + + @Test + public void resetTest() { // Call (reset) and *then* set the logic again // FIXME: We currently don't support the (reset) command and expect and exception to be thrown // here diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index 61b70bb433..484992fe22 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -541,6 +541,13 @@ public void testBoolVariableDump() { @Test public void testEqBoolVariableDump() { // FIXME: Rewrite test? Most solvers will simplify the formula to `true`. + + // What is happening internally is that the input is returned as "(= java-smt java-smt)", + // which is thrown away by our sanitization due to no assertion + assume() + .withMessage("Boolector simplifies the input so much that it gives out no " + "assertions") + .that(solverToUse()) + .isNotEqualTo(Solvers.BOOLECTOR); for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); if (var != null) {