From a5b37a415e555c6498adcaaf01f5c9ed0a284840 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Fri, 23 Feb 2024 16:56:04 +0100 Subject: [PATCH] Preprocessing: Apply substitutions from previous frames --- src/api/MainSolver.cc | 215 +++++++++++++++++++++++++++---------- src/api/MainSolver.h | 182 ++++++++++++++----------------- src/api/PartitionManager.h | 1 + src/logics/ArrayTheory.cc | 16 ++- src/logics/ArrayTheory.h | 3 +- src/logics/CMakeLists.txt | 1 - src/logics/LATheory.h | 31 ++---- src/logics/Theory.cc | 72 ------------- src/logics/Theory.h | 23 ++-- src/logics/UFLATheory.cc | 15 +-- src/logics/UFLATheory.h | 3 +- src/logics/UFTheory.cc | 27 ++--- 12 files changed, 275 insertions(+), 314 deletions(-) delete mode 100644 src/logics/Theory.cc diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 905066d1a..f3027b8d0 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -1,28 +1,10 @@ -/********************************************************************* -Author: Antti Hyvarinen - -OpenSMT2 -- Copyright (C) 2012 - 2014 Antti Hyvarinen - -Permission is hereby granted, free of charge, to any person obtaining a -copy of this software and associated documentation files (the -"Software"), to deal in the Software without restriction, including -without limitation the rights to use, copy, modify, merge, publish, -distribute, sublicense, and/or sell copies of the Software, and to -permit persons to whom the Software is furnished to do so, subject to -the following conditions: - -The above copyright notice and this permission notice shall be included -in all copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS -OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF -MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE -LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION -OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION -WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -*********************************************************************/ - +/* + * Copyright (c) 2012 - 2022, Antti Hyvarinen + * Copyright (c) 2022 - 2024, Martin Blicha + * + * SPDX-License-Identifier: MIT + * + */ #include "MainSolver.h" #include "BoolRewriting.h" @@ -37,12 +19,48 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include "IteHandler.h" #include "RDLTHandler.h" #include "IDLTHandler.h" +#include "Substitutor.h" #include -#include namespace opensmt { bool stop; } +MainSolver::MainSolver(Logic& logic, SMTConfig& conf, std::string name) + : + theory(createTheory(logic, conf)), + term_mapper(new TermMapper(logic)), + thandler(new THandler(getTheory(), *term_mapper)), + smt_solver(createInnerSolver(conf, *thandler)), + logic(thandler->getLogic()), + pmanager(logic), + config(conf), + ts(logic, *term_mapper), + solver_name {std::move(name)} +{ + conf.setUsedForInitiliazation(); + initialize(); +} + +MainSolver::MainSolver(std::unique_ptr th, std::unique_ptr tm, std::unique_ptr thd, + std::unique_ptr ss, Logic & logic, SMTConfig & conf, std::string name) + : + theory(std::move(th)), + term_mapper(std::move(tm)), + thandler(std::move(thd)), + smt_solver(std::move(ss)), + logic(thandler->getLogic()), + pmanager(logic), + config(conf), + ts(logic,*term_mapper), + solver_name {std::move(name)} +{ + conf.setUsedForInitiliazation(); + initialize(); +} + void MainSolver::initialize() { + frames.push(); + frameTerms.push(logic.getTerm_true()); + substitutions.push(); smt_solver->initialize(); opensmt::pair iorefs{CRef_Undef, CRef_Undef}; smt_solver->addOriginalSMTClause({term_mapper->getOrCreateLit(logic.getTerm_true())}, iorefs); @@ -52,17 +70,16 @@ void MainSolver::initialize() { if (iorefs.first != CRef_Undef) { pmanager.addClauseClassMask(iorefs.first, 1); } } -void -MainSolver::push() +void MainSolver::push() { bool alreadyUnsat = isLastFrameUnsat(); frames.push(); + substitutions.push(); frameTerms.push(newFrameTerm(frames.last().getId())); if (alreadyUnsat) { rememberLastFrameUnsat(); } } -bool -MainSolver::pop() +bool MainSolver::pop() { if (frames.frameCount() > 1) { if (config.produce_inter() > 0) { @@ -76,6 +93,7 @@ MainSolver::pop() pmanager.invalidatePartitions(mask); } frames.pop(); + substitutions.pop(); firstNotSimplifiedFrame = std::min(firstNotSimplifiedFrame, frames.frameCount()); if (not isLastFrameUnsat()) { getSMTSolver().restoreOK(); @@ -85,49 +103,43 @@ MainSolver::pop() return false; } -PTRef MainSolver::newFrameTerm(MainSolver::FrameId frameId) { - assert(frameId.id != 0); - auto name = std::string(Logic::s_framev_prefix) + std::to_string(frameId.id); - PTRef frameTerm = logic.mkBoolVar(name.c_str()); - Lit l = term_mapper->getOrCreateLit(frameTerm); - term_mapper->setFrozen(var(l)); - smt_solver->addAssumptionVar(var(l)); - return frameTerm; -} +PartitionManager & MainSolver::getPartitionManager() { return pmanager; } + +sstat MainSolver::getStatus() const { return status; } void MainSolver::insertFormula(PTRef fla) { if (logic.getSortRef(fla) != logic.getSort_bool()) { throw OsmtApiException("Top-level assertion sort must be Bool, got " + logic.printSort(logic.getSortRef(fla))); } - // TODO: Move this to preprocessing of the formulas fla = IteHandler(logic, getPartitionManager().getNofPartitions()).rewrite(fla); if (getConfig().produce_inter()) { // MB: Important for HiFrog! partition index is the index of the formula in an virtual array of inserted formulas, // thus we need the old value of count. TODO: Find a good interface for this so it cannot be broken this easily - unsigned int partition_index = inserted_formulas_count++; + unsigned int partition_index = insertedFormulasCount++; pmanager.assignTopLevelPartitionIndex(partition_index, fla); assert(pmanager.getPartitionIndex(fla) != -1); } - else { - ++inserted_formulas_count; - } + else { ++insertedFormulasCount; } frames.add(fla); firstNotSimplifiedFrame = std::min(firstNotSimplifiedFrame, frames.frameCount() - 1); } -sstat MainSolver::simplifyFormulas() -{ +sstat MainSolver::simplifyFormulas() { status = s_Undef; - bool keepPartitionsSeparate = getConfig().produce_inter(); - // Process (and simplify) not yet processed frames. Stop processing if solver is in UNSAT state already for (std::size_t i = firstNotSimplifiedFrame; i < frames.frameCount() && status != s_False; i++) { - if (keepPartitionsSeparate) { - vec frameFormulas = getTheory().simplifyIndividually(frames[i].formulas, pmanager, i == 0); - firstNotSimplifiedFrame = i + 1; + PreprocessingContext context {.frameCount = i, .perPartition = getConfig().produce_inter() }; + firstNotSimplifiedFrame = i + 1; + if (context.perPartition) { + vec frameFormulas; + for (PTRef fla : frames[i].formulas) { + PTRef processed = theory->preprocessAfterSubstitutions(fla, context); + pmanager.transferPartitionMembership(fla, processed); + frameFormulas.push(processed); + } if (frameFormulas.size() == 0 or std::all_of(frameFormulas.begin(), frameFormulas.end(), [&](PTRef fla) { return fla == logic.getTerm_true(); })) { continue; } @@ -146,10 +158,16 @@ sstat MainSolver::simplifyFormulas() if (status == s_False) { break; } } } else { - PTRef frameFormula = getTheory().simplifyTogether(frames[i].formulas, i == 0); - firstNotSimplifiedFrame = i + 1; + PTRef frameFormula = logic.mkAnd(frames[i].formulas); + if (context.frameCount > 0) { + frameFormula = applyLearntSubstitutions(frameFormula); + } + frameFormula = theory->preprocessBeforeSubstitutions(frameFormula, context); + frameFormula = substitutionPass(frameFormula, context); + frameFormula = theory->preprocessAfterSubstitutions(frameFormula, context); + if (logic.isFalse(frameFormula)) { - giveToSolver(getLogic().getTerm_false(), frames[i].getId()); + giveToSolver(logic.getTerm_false(), frames[i].getId()); status = s_False; break; } @@ -167,6 +185,18 @@ sstat MainSolver::simplifyFormulas() return status; } +void MainSolver::printFramesAsQuery(std::ostream & s) const { + logic.dumpHeaderToFile(s); + for (std::size_t i = 0; i < frames.frameCount(); ++i) { + if (i > 0) + s << "(push 1)\n"; + for (PTRef assertion : frames[i].formulas) { + logic.dumpFormulaToFile(s, assertion); + } + } + logic.dumpChecksatToFile(s); +} + // Replace subtrees consisting only of ands / ors with a single and / or term. // Search a maximal section of the tree consisting solely of ands / ors. The @@ -239,7 +269,7 @@ void MainSolver::printFramesAsQuery() const free(base_name); } -sstat MainSolver::giveToSolver(PTRef root, MainSolver::FrameId push_id) { +sstat MainSolver::giveToSolver(PTRef root, FrameId push_id) { struct ClauseCallBack : public Cnfizer::ClauseCallBack { std::vector> clauses; @@ -328,7 +358,7 @@ sstat MainSolver::solve() } sstat MainSolver::solve_(vec const & enabledFrames) { - assert(frameTerms.size() > 0 and frameTerms[0] == logic.getTerm_true()); + assert(frameTerms.size() > 0 and frameTerms[0] == getLogic().getTerm_true()); vec assumps; // Initialize so that by default frames are disabled for (PTRef tr : frameTerms) { @@ -419,7 +449,7 @@ std::unique_ptr MainSolver::createTheory(Logic & logic, SMTConfig & conf break; } case Logic_t::UNDEF: - throw OsmtApiException{"Error in creating reasoning engine: Engige type not specified"}; + throw OsmtApiException{"Error in creating reasoning engine: Engine type not specified"}; break; default: assert(false); @@ -429,3 +459,74 @@ std::unique_ptr MainSolver::createTheory(Logic & logic, SMTConfig & conf return std::unique_ptr(theory); } + +PTRef MainSolver::applyLearntSubstitutions(PTRef fla) { + Logic::SubstMap knownSubst = substitutions.current(); + PTRef res = Substitutor(getLogic(), knownSubst).rewrite(fla); + return res; +} + +PTRef MainSolver::substitutionPass(PTRef fla, PreprocessingContext const& context) { + if (not config.do_substitutions()) { return fla; } + auto res = computeSubstitutions(fla); + vec args; + const auto & entries = res.usedSubstitution.getKeys(); + for (auto entry : entries) { + auto target = res.usedSubstitution[entry]; + args.push(logic.mkEq(entry, target)); + } + args.push(res.result); + PTRef withSubs = logic.mkAnd(std::move(args)); + + substitutions.set(context.frameCount, std::move(res.usedSubstitution)); + return withSubs; +} + +MainSolver::SubstitutionResult MainSolver::computeSubstitutions(PTRef fla) { + SubstitutionResult result; + assert(getConfig().do_substitutions() and not getConfig().produce_inter()); + PTRef root = fla; + Logic::SubstMap allsubsts; + while (true) { + // update the current simplification formula + PTRef simp_formula = root; + // l_True : exists and is valid + // l_False : exists but has been disabled to break symmetries + MapWithKeys new_units; + vec current_units_vec; + bool rval = logic.getNewFacts(simp_formula, new_units); + if (not rval) { + return SubstitutionResult{{}, logic.getTerm_false()}; + } + // Add the newly obtained units to the list of all substitutions + // Clear the previous units + const auto & new_units_vec = new_units.getKeys(); + for (PTRef key : new_units_vec) { + current_units_vec.push(PtAsgn{key, new_units[key]}); + } + + auto [res, newsubsts] = logic.retrieveSubstitutions(current_units_vec); + logic.substitutionsTransitiveClosure(newsubsts); + + + // remember the substitutions for models + for (PTRef key : newsubsts.getKeys()) { + if (!allsubsts.has(key)) { + const auto target = newsubsts[key]; + allsubsts.insert(key, target); + } + } + + if (res != l_Undef) + root = (res == l_True ? logic.getTerm_true() : logic.getTerm_false()); + + PTRef new_root = Substitutor(logic, newsubsts).rewrite(root); + + bool cont = new_root != root; + root = new_root; + if (!cont) break; + } + result.result = root; + result.usedSubstitution = std::move(allsubsts); + return result; +} \ No newline at end of file diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index 610c9d450..7c4ca3a75 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -1,27 +1,10 @@ -/********************************************************************* -Author: Antti Hyvarinen - -OpenSMT2 -- Copyright (C) 2012 - 2014 Antti Hyvarinen - -Permission is hereby granted, free of charge, to any person obtaining a -copy of this software and associated documentation files (the -"Software"), to deal in the Software without restriction, including -without limitation the rights to use, copy, modify, merge, publish, -distribute, sublicense, and/or sell copies of the Software, and to -permit persons to whom the Software is furnished to do so, subject to -the following conditions: - -The above copyright notice and this permission notice shall be included -in all copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS -OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF -MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE -LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION -OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION -WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -*********************************************************************/ +/* + * Copyright (c) 2012 - 2022, Antti Hyvarinen + * Copyright (c) 2022 - 2024, Martin Blicha + * + * SPDX-License-Identifier: MIT + * + */ #ifndef MAINSOLVER_H #define MAINSOLVER_H @@ -68,7 +51,7 @@ const sstat s_Error = toSstat( 2); class MainSolver { -public: +protected: /** Helper classes to deal with assertion stack, preprocessing and substitutions **/ struct FrameId { uint32_t id; @@ -76,7 +59,6 @@ class MainSolver bool operator!= (const FrameId other) const { return id != other.id; } }; -protected: struct PushFrame { private: @@ -131,6 +113,73 @@ class MainSolver } }; + class Substitutions { + std::vector perFrameSubst; + + public: + void push() { perFrameSubst.emplace_back(); } + void pop() { perFrameSubst.pop_back(); } + + void set(std::size_t level, Logic::SubstMap && subs) { + perFrameSubst.at(level) = std::move(subs); + } + + Logic::SubstMap current() { + Logic::SubstMap allSubst; + for (auto const & subs : perFrameSubst) { + for (PTRef key : subs.getKeys()) { + assert(not allSubst.has(key)); + allSubst.insert(key, subs[key]); + } + } + return allSubst; + } + }; +/** Actual MainSolver members **/ +protected: + AssertionStack frames; + Substitutions substitutions; + vec frameTerms; + std::size_t firstNotSimplifiedFrame = 0; + unsigned int insertedFormulasCount = 0; + sstat status = s_Undef; // The status of the last solver call + + PTRef newFrameTerm(FrameId frameId) { + assert(frameId.id != 0); + auto name = std::string(Logic::s_framev_prefix) + std::to_string(frameId.id); + PTRef frameTerm = logic.mkBoolVar(name.c_str()); + Lit l = term_mapper->getOrCreateLit(frameTerm); + term_mapper->setFrozen(var(l)); + smt_solver->addAssumptionVar(var(l)); + return frameTerm; + } + bool isLastFrameUnsat() const { return frames.last().unsat; } + void rememberLastFrameUnsat() { frames.last().unsat = true; } + void rememberUnsatFrame(std::size_t frameIndex) { + assert(frameIndex < frames.frameCount()); + for (; frameIndex < frames.frameCount(); ++frameIndex) { + frames[frameIndex].unsat = true; + } + } + + PTRef rewriteMaxArity(PTRef root); + + virtual sstat solve_(vec const & enabledFrames); + + sstat giveToSolver(PTRef root, FrameId push_id); + + struct SubstitutionResult { + Logic::SubstMap usedSubstitution; + PTRef result {PTRef_Undef}; + }; + + PTRef applyLearntSubstitutions(PTRef fla); + + PTRef substitutionPass(PTRef fla, PreprocessingContext const& context); + + SubstitutionResult computeSubstitutions(PTRef fla); + +public: std::unique_ptr theory; std::unique_ptr term_mapper; std::unique_ptr thandler; @@ -139,95 +188,25 @@ class MainSolver PartitionManager pmanager; SMTConfig& config; Tseitin ts; - AssertionStack frames; - vec frameTerms; - - std::size_t firstNotSimplifiedFrame = 0; - - opensmt::OSMTTimeVal query_timer; // How much time we spend solving. std::string solver_name; // Name for the solver int check_called = 0; // A counter on how many times check was called. - sstat status = s_Undef; // The status of the last solver call - unsigned int inserted_formulas_count = 0; // Number of formulas that has been inserted to this solver sstat solve(); - virtual sstat solve_(vec const & enabledFrames); - - sstat giveToSolver(PTRef root, FrameId push_id); - - PTRef rewriteMaxArity(PTRef); - [[nodiscard]] PTRef currentRootInstance() const; - // helper private methods - PTRef newFrameTerm(FrameId frameId); - bool isLastFrameUnsat() const { return frames.last().unsat; } - void rememberLastFrameUnsat() { frames.last().unsat = true; } - void rememberUnsatFrame(std::size_t frameIndex) { - assert(frameIndex < frames.frameCount()); - for (; frameIndex < frames.frameCount(); ++frameIndex) { - frames[frameIndex].unsat = true; - } - } - - void printFramesAsQuery(std::ostream & s) const - { - logic.dumpHeaderToFile(s); - for (std::size_t i = 0; i < frames.frameCount(); ++i) { - if (i > 0) - s << "(push 1)\n"; - for (PTRef assertion : frames[i].formulas) { - logic.dumpFormulaToFile(s, assertion); - } - } - logic.dumpChecksatToFile(s); - } + void printFramesAsQuery(std::ostream & s) const; static std::unique_ptr createInnerSolver(SMTConfig& config, THandler& thandler); public: - - MainSolver(Logic& logic, SMTConfig& conf, std::string name) - : - theory(createTheory(logic, conf)), - term_mapper(new TermMapper(logic)), - thandler(new THandler(getTheory(), *term_mapper)), - smt_solver(createInnerSolver(conf, *thandler)), - logic(thandler->getLogic()), - pmanager(logic), - config(conf), - ts(logic, *term_mapper), - solver_name {std::move(name)} - { - conf.setUsedForInitiliazation(); - // Special handling of zero-level frame - frames.push(); - frameTerms.push(logic.getTerm_true()); - initialize(); - } + MainSolver(Logic& logic, SMTConfig& conf, std::string name); MainSolver(std::unique_ptr th, std::unique_ptr tm, std::unique_ptr thd, - std::unique_ptr ss, Logic & logic, SMTConfig & conf, std::string name) - : - theory(std::move(th)), - term_mapper(std::move(tm)), - thandler(std::move(thd)), - smt_solver(std::move(ss)), - logic(thandler->getLogic()), - pmanager(logic), - config(conf), - ts(logic,*term_mapper), - solver_name {std::move(name)} - { - conf.setUsedForInitiliazation(); - frames.push(); - frameTerms.push(logic.getTerm_true()); - initialize(); - } + std::unique_ptr ss, Logic & logic, SMTConfig & conf, std::string name); virtual ~MainSolver() = default; MainSolver (const MainSolver&) = delete; @@ -243,7 +222,8 @@ class MainSolver Logic &getLogic() { return logic; } Theory &getTheory() { return *theory; } const Theory &getTheory() const { return *theory; } - PartitionManager &getPartitionManager() { return pmanager; } + PartitionManager & getPartitionManager(); + void push(); bool pop(); void insertFormula(PTRef fla); @@ -255,7 +235,7 @@ class MainSolver sstat simplifyFormulas(); void printFramesAsQuery() const; - sstat getStatus () const { return status; } + [[nodiscard]] sstat getStatus() const; // Values lbool getTermValue (PTRef tr) const; diff --git a/src/api/PartitionManager.h b/src/api/PartitionManager.h index 9d5b75527..a3230870b 100644 --- a/src/api/PartitionManager.h +++ b/src/api/PartitionManager.h @@ -59,6 +59,7 @@ class PartitionManager { unsigned getNofPartitions() const { return partitionInfo.getNoOfPartitions(); } void transferPartitionMembership(PTRef old, PTRef new_ptref) { + if (new_ptref == old) { return; } this->addIPartitions(new_ptref, getIPartitions(old)); partitionInfo.transferPartitionMembership(old, new_ptref); } diff --git a/src/logics/ArrayTheory.cc b/src/logics/ArrayTheory.cc index 70cd56a55..4dc9b329e 100644 --- a/src/logics/ArrayTheory.cc +++ b/src/logics/ArrayTheory.cc @@ -1,5 +1,5 @@ /* - * Copyright (c) 2021, Martin Blicha + * Copyright (c) 2021 - 2024, Martin Blicha * * SPDX-License-Identifier: MIT */ @@ -9,14 +9,10 @@ #include "ArrayHelpers.h" #include "DistinctRewriter.h" -PTRef ArrayTheory::simplifyTogether(const vec & assertions, bool) { +PTRef ArrayTheory::preprocessAfterSubstitutions(PTRef fla, PreprocessingContext const & context) { + if (context.perPartition) { throw OsmtInternalException("Interpolation not supported for logics with arrays yet"); } // TODO: simplify select over store on the same index - PTRef frameFormula = getLogic().mkAnd(assertions); - frameFormula = rewriteDistincts(getLogic(), frameFormula); - frameFormula = instantiateReadOverStore(getLogic(), frameFormula); - return frameFormula; -} - -vec ArrayTheory::simplifyIndividually(const vec &, PartitionManager &, bool) { - throw OsmtInternalException("Interpolation not supported for logics with arrays yet"); + fla = rewriteDistincts(getLogic(), fla); + fla = instantiateReadOverStore(getLogic(), fla); + return fla; } diff --git a/src/logics/ArrayTheory.h b/src/logics/ArrayTheory.h index e2450c0ee..3ce3cc2cc 100644 --- a/src/logics/ArrayTheory.h +++ b/src/logics/ArrayTheory.h @@ -26,8 +26,7 @@ class ArrayTheory : public Theory { virtual ArrayTHandler& getTSolverHandler() override { return tshandler; } virtual const ArrayTHandler& getTSolverHandler() const { return tshandler; } - virtual PTRef simplifyTogether(vec const & assertions, bool) override; - virtual vec simplifyIndividually(vec const & assertions, PartitionManager & pmanager, bool) override; + virtual PTRef preprocessAfterSubstitutions(PTRef, PreprocessingContext const &) override; }; diff --git a/src/logics/CMakeLists.txt b/src/logics/CMakeLists.txt index 37c53b921..d08709b74 100644 --- a/src/logics/CMakeLists.txt +++ b/src/logics/CMakeLists.txt @@ -11,7 +11,6 @@ target_sources(logics PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/ArrayHelpers.cc" PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/ArithLogic.h" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/ArithLogic.cc" - PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Theory.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Theory.h" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFLATheory.h" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFLATheory.cc" diff --git a/src/logics/LATheory.h b/src/logics/LATheory.h index 9bd8740dd..20f2b1f2d 100644 --- a/src/logics/LATheory.h +++ b/src/logics/LATheory.h @@ -29,8 +29,7 @@ class LATheory : public Theory virtual const LinAlgLogic& getLogic() const override { return lalogic; } virtual LinAlgTHandler& getTSolverHandler() override { return latshandler; } - virtual PTRef simplifyTogether(vec const & assertions, bool isBaseFrame) override; - virtual vec simplifyIndividually(vec const & assertions, PartitionManager & pmanager, bool isBaseFrame) override; + virtual PTRef preprocessAfterSubstitutions(PTRef, PreprocessingContext const &) override; }; namespace { @@ -46,33 +45,15 @@ PTRef rewriteDivMod(ArithLogic & logic, PTRef fla) { } - template -PTRef LATheory::simplifyTogether(const vec & assertions, bool) { - PTRef frameFormula = getLogic().mkAnd(assertions); - frameFormula = applySubstitutionBasedSimplificationIfEnabled(frameFormula); - frameFormula = rewriteDistincts(getLogic(), frameFormula); - frameFormula = rewriteDivMod(lalogic, frameFormula); +PTRef LATheory::preprocessAfterSubstitutions(PTRef fla, PreprocessingContext const &) { + fla = rewriteDistincts(getLogic(), fla); + fla = rewriteDivMod(lalogic, fla); ArithmeticEqualityRewriter equalityRewriter(lalogic); - frameFormula = equalityRewriter.rewrite(frameFormula); - return frameFormula; + fla = equalityRewriter.rewrite(fla); + return fla; } -template -vec LATheory::simplifyIndividually(const vec & assertions, PartitionManager & pmanager, bool) { - ArithmeticEqualityRewriter equalityRewriter(lalogic); - vec rewrittenAssertions; - assertions.copyTo(rewrittenAssertions); - for (PTRef & fla : rewrittenAssertions) { - PTRef old = fla; - fla = rewriteDistincts(getLogic(), fla); - fla = rewriteDivMod(lalogic, fla); - fla = equalityRewriter.rewrite(fla); - pmanager.transferPartitionMembership(old, fla); - } - return rewrittenAssertions; - -} #endif //OPENSMT_LATHEORY_H diff --git a/src/logics/Theory.cc b/src/logics/Theory.cc deleted file mode 100644 index 144bbad36..000000000 --- a/src/logics/Theory.cc +++ /dev/null @@ -1,72 +0,0 @@ -#include "Theory.h" -#include "Substitutor.h" - - -Theory::SubstitutionResult Theory::computeSubstitutions(const PTRef fla) -{ - SubstitutionResult result; - assert(config.do_substitutions() && !config.produce_inter()); - PTRef root = fla; - // l_True : exists and is valid - // l_False : exists but has been disabled to break symmetries - Logic::SubstMap allsubsts; - // This computes the new unit clauses to curr_frame.units until closure - while (true) { - // update the current simplification formula - PTRef simp_formula = root; - MapWithKeys new_units; - vec current_units_vec; - // Get U_i - bool rval = getLogic().getNewFacts(simp_formula, new_units); - if (not rval) { - return SubstitutionResult{{}, getLogic().getTerm_false()}; - } - // Add the newly obtained units to the list of all substitutions - // Clear the previous units - const auto & new_units_vec = new_units.getKeys(); - for (PTRef key : new_units_vec) { - current_units_vec.push(PtAsgn{key, new_units[key]}); - } - - auto [res, newsubsts] = getLogic().retrieveSubstitutions(current_units_vec); - getLogic().substitutionsTransitiveClosure(newsubsts); - - - // remember the substitutions for models - for (PTRef key : newsubsts.getKeys()) { - if (!allsubsts.has(key)) { - const auto target = newsubsts[key]; - allsubsts.insert(key, target); - } - } - - if (res != l_Undef) - root = (res == l_True ? getLogic().getTerm_true() : getLogic().getTerm_false()); - - PTRef new_root = Substitutor(getLogic(), newsubsts).rewrite(root); - - bool cont = new_root != root; - root = new_root; - if (!cont) break; - } - result.result = root; - result.usedSubstitution = std::move(allsubsts); - return result; -} - - -PTRef Theory::flaFromSubstitutionResult(const Theory::SubstitutionResult & sr) { - Logic & logic = getLogic(); - vec args; - const auto & entries = sr.usedSubstitution.getKeys(); - for (auto entry : entries) { - auto target = sr.usedSubstitution[entry]; - args.push(logic.mkEq(entry, target)); - } - args.push(sr.result); - return logic.mkAnd(std::move(args)); -} - -PTRef Theory::applySubstitutionBasedSimplificationIfEnabled(PTRef root) { - return config.do_substitutions() ? flaFromSubstitutionResult(computeSubstitutions(root)) : root; -} diff --git a/src/logics/Theory.h b/src/logics/Theory.h index f2432466a..6240266b6 100644 --- a/src/logics/Theory.h +++ b/src/logics/Theory.h @@ -36,13 +36,14 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include "PartitionManager.h" +struct PreprocessingContext { + std::size_t frameCount {0}; + bool perPartition {false}; +}; + class Theory { protected: - struct SubstitutionResult { - Logic::SubstMap usedSubstitution; - PTRef result; - }; SMTConfig & config; @@ -50,21 +51,15 @@ class Theory inline bool keepPartitions() const { return config.produce_inter(); } - /* Computes the final formula from substitution result. - * The formula is the computed formula with all substitutions conjoined in form of equalities - */ - PTRef flaFromSubstitutionResult(const SubstitutionResult & sr); - PTRef applySubstitutionBasedSimplificationIfEnabled(PTRef); public: virtual Logic &getLogic() = 0; virtual const Logic &getLogic() const = 0; virtual TSolverHandler &getTSolverHandler() = 0; - virtual PTRef simplifyTogether(vec const & assertions, bool isBaseFrame) = 0; - virtual vec simplifyIndividually(vec const & assertions, PartitionManager & pmanager, bool isBaseFrame) = 0; + virtual PTRef preprocessBeforeSubstitutions(PTRef fla, PreprocessingContext const &) { return fla; } + virtual PTRef preprocessAfterSubstitutions(PTRef, PreprocessingContext const &) = 0; - SubstitutionResult computeSubstitutions(PTRef fla); virtual ~Theory() = default; }; @@ -83,8 +78,8 @@ class UFTheory : public Theory virtual const Logic& getLogic() const override { return uflogic; } virtual UFTHandler& getTSolverHandler() override { return tshandler; } virtual const UFTHandler& getTSolverHandler() const { return tshandler; } - virtual PTRef simplifyTogether(vec const & assertions, bool isBaseFrame) override; - virtual vec simplifyIndividually(vec const & assertions, PartitionManager & pmanager, bool isBaseFrame) override; + virtual PTRef preprocessBeforeSubstitutions(PTRef, PreprocessingContext const &) override; + virtual PTRef preprocessAfterSubstitutions(PTRef, PreprocessingContext const &) override; }; #endif diff --git a/src/logics/UFLATheory.cc b/src/logics/UFLATheory.cc index 5fd914c8f..714068233 100644 --- a/src/logics/UFLATheory.cc +++ b/src/logics/UFLATheory.cc @@ -8,12 +8,11 @@ #include "Substitutor.h" #include "TreeOps.h" -PTRef UFLATheory::simplifyTogether(vec const & assertions, bool) { - PTRef frameFormula = getLogic().mkAnd(assertions); - frameFormula = applySubstitutionBasedSimplificationIfEnabled(frameFormula); - frameFormula = rewriteDistincts(getLogic(), frameFormula); - frameFormula = rewriteDivMod(logic, frameFormula); - PTRef purified = purify(frameFormula); +PTRef UFLATheory::preprocessAfterSubstitutions(PTRef fla, PreprocessingContext const & context) { + if (context.perPartition) { throw OsmtInternalException("Mode not supported for QF_UFLRA yet"); } + fla = rewriteDistincts(getLogic(), fla); + fla = rewriteDivMod(logic, fla); + PTRef purified = purify(fla); if (logic.hasArrays()) { purified = instantiateReadOverStore(logic, purified); } @@ -22,10 +21,6 @@ PTRef UFLATheory::simplifyTogether(vec const & assertions, bool) { return noArithmeticEqualities; } -vec UFLATheory::simplifyIndividually(vec const &, PartitionManager &, bool) { - throw OsmtInternalException("Mode not supported for QF_UFLRA yet"); -} - namespace { bool isArithmeticSymbol(ArithLogic const & logic, SymRef sym) { return logic.isPlus(sym) or logic.isTimes(sym) or logic.isLeq(sym); diff --git a/src/logics/UFLATheory.h b/src/logics/UFLATheory.h index b8229e154..eabc410c1 100644 --- a/src/logics/UFLATheory.h +++ b/src/logics/UFLATheory.h @@ -45,8 +45,7 @@ class UFLATheory : public Theory virtual const ArithLogic& getLogic() const override { return logic; } virtual UFLATHandler& getTSolverHandler() override { return uflatshandler; } - virtual PTRef simplifyTogether(vec const & assertions, bool isBaseFrame) override; - virtual vec simplifyIndividually(vec const & assertions, PartitionManager & pmanager, bool isBaseFrame) override; + virtual PTRef preprocessAfterSubstitutions(PTRef, PreprocessingContext const &) override; protected: PTRef purify(PTRef fla); diff --git a/src/logics/UFTheory.cc b/src/logics/UFTheory.cc index ee96c5fb3..7b231b39e 100644 --- a/src/logics/UFTheory.cc +++ b/src/logics/UFTheory.cc @@ -2,27 +2,14 @@ #include "TreeOps.h" #include "DistinctRewriter.h" -PTRef UFTheory::simplifyTogether(vec const & assertions, bool isBaseFrame) { - PTRef frameFormula = getLogic().mkAnd(assertions); - PTRef trans = getLogic().learnEqTransitivity(frameFormula); - frameFormula = getLogic().mkAnd(frameFormula, trans); - frameFormula = applySubstitutionBasedSimplificationIfEnabled(frameFormula); - frameFormula = isBaseFrame ? rewriteDistinctsKeepTopLevel(getLogic(), frameFormula) - : rewriteDistincts(getLogic(), frameFormula); - AppearsInUfVisitor(getLogic()).visit(frameFormula); - return frameFormula; +PTRef UFTheory::preprocessBeforeSubstitutions(PTRef fla, PreprocessingContext const & context) { + return context.perPartition ? fla : getLogic().mkAnd(fla, getLogic().learnEqTransitivity(fla)); } -vec UFTheory::simplifyIndividually(vec const& formulas, PartitionManager &, bool isBaseFrame) -{ - vec rewrittenFormulas; - formulas.copyTo(rewrittenFormulas); - AppearsInUfVisitor visitor(getLogic()); - - for (PTRef & fla : rewrittenFormulas) { - fla = isBaseFrame ? rewriteDistinctsKeepTopLevel(getLogic(), fla) : rewriteDistincts(getLogic(), fla); - visitor.visit(fla); - } - return rewrittenFormulas; +PTRef UFTheory::preprocessAfterSubstitutions(PTRef fla, PreprocessingContext const & context) { + fla = context.frameCount == 0 ? rewriteDistinctsKeepTopLevel(getLogic(), fla) + : rewriteDistincts(getLogic(), fla); + AppearsInUfVisitor(getLogic()).visit(fla); + return fla; }