From cea1ad700bc4cff0d9fcfb0f14c8908e24bbc8c2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 22 Apr 2021 21:18:13 -0500 Subject: [PATCH] Enable strings exp by default for strings specific logics (#6424) One of the main motivations for this PR is to simplify our process for doing SMT-LIB wide runs. --- src/smt/set_defaults.cpp | 6 ++++++ src/theory/quantifiers/fmf/full_model_check.cpp | 5 +++++ 2 files changed, 11 insertions(+) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 117fbbd4b..047dbfea6 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -284,6 +284,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // Set default options associated with strings-exp. We also set these options // if we are using eager string preprocessing, which may introduce quantified // formulas at preprocess time. + if (!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS)) + { + // If the user explicitly set a logic that includes strings, but is not + // the generic "ALL" logic, then enable stringsExp. + options::stringExp.set(true); + } if (options::stringExp() || !options::stringLazyPreproc()) { // We require quantifiers since extended functions reduce using them. diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 841cd4ab9..da220be18 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -332,6 +332,11 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) { i++) { Node q = fm->getAssertedQuantifier(i); + registerQuantifiedFormula(q); + if (!isHandled(q)) + { + continue; + } // make sure all types are set for (const Node& v : q[0]) { -- 2.30.2