diff --git a/src/api/Interpret.cc b/src/api/Interpret.cc index 6e336e417..dd3827478 100644 --- a/src/api/Interpret.cc +++ b/src/api/Interpret.cc @@ -161,7 +161,6 @@ void Interpret::interp(ASTNode& n) { } initializeLogic(logic_type); main_solver = createMainSolver(logic_name); - main_solver->initialize(); notify_success(); } break; diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 5d86390a0..905066d1a 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -42,32 +42,42 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. namespace opensmt { bool stop; } +void MainSolver::initialize() { + smt_solver->initialize(); + opensmt::pair iorefs{CRef_Undef, CRef_Undef}; + smt_solver->addOriginalSMTClause({term_mapper->getOrCreateLit(logic.getTerm_true())}, iorefs); + if (iorefs.first != CRef_Undef) { pmanager.addClauseClassMask(iorefs.first, 1); } + + smt_solver->addOriginalSMTClause({~term_mapper->getOrCreateLit(logic.getTerm_false())}, iorefs); + if (iorefs.first != CRef_Undef) { pmanager.addClauseClassMask(iorefs.first, 1); } +} + void MainSolver::push() { bool alreadyUnsat = isLastFrameUnsat(); - frames.push(pfstore.alloc()); + frames.push(); + frameTerms.push(newFrameTerm(frames.last().getId())); if (alreadyUnsat) { rememberLastFrameUnsat(); } } bool MainSolver::pop() { - if (frames.size() > 1) { + if (frames.frameCount() > 1) { if (config.produce_inter() > 0) { - auto toPop = frames.last(); - auto& partitionsToInvalidate = pfstore[toPop].formulas; + auto const & partitionsToInvalidate = frames.last().formulas; ipartitions_t mask = 0; - for (int i = 0; i < partitionsToInvalidate.size(); ++i) { - PTRef part = partitionsToInvalidate[i]; - auto index = pmanager.getPartitionIndex(part); + for (PTRef partition : partitionsToInvalidate) { + auto index = pmanager.getPartitionIndex(partition); assert(index != -1); opensmt::setbit(mask, static_cast(index)); } pmanager.invalidatePartitions(mask); } frames.pop(); - if (!isLastFrameUnsat()) { + firstNotSimplifiedFrame = std::min(firstNotSimplifiedFrame, frames.frameCount()); + if (not isLastFrameUnsat()) { getSMTSolver().restoreOK(); } return true; @@ -75,55 +85,53 @@ 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; +} -void MainSolver::insertFormula(PTRef root) +void MainSolver::insertFormula(PTRef fla) { - if (logic.getSortRef(root) != logic.getSort_bool()) { - throw OsmtApiException("Top-level assertion sort must be Bool, got " + logic.printSort(logic.getSortRef(root))); + if (logic.getSortRef(fla) != logic.getSort_bool()) { + throw OsmtApiException("Top-level assertion sort must be Bool, got " + logic.printSort(logic.getSortRef(fla))); } - root = logic.conjoinExtras(root); - root = IteHandler(logic, getPartitionManager().getNofPartitions()).rewrite(root); + // 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++; - pmanager.assignTopLevelPartitionIndex(partition_index, root); - assert(pmanager.getPartitionIndex(root) != -1); + pmanager.assignTopLevelPartitionIndex(partition_index, fla); + assert(pmanager.getPartitionIndex(fla) != -1); } else { ++inserted_formulas_count; } - PushFrame& lastFrame = pfstore[frames.last()]; - lastFrame.push(root); - lastFrame.root = PTRef_Undef; - // New formula has been added to the last frame. If the frame has been simplified before, we need to do it again - frames.setSimplifiedUntil(std::min(frames.getSimplifiedUntil(), frames.size() - 1)); + frames.add(fla); + firstNotSimplifiedFrame = std::min(firstNotSimplifiedFrame, frames.frameCount() - 1); } sstat MainSolver::simplifyFormulas() { status = s_Undef; - - vec coll_f; 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 = frames.getSimplifiedUntil(); i < frames.size() && status != s_False; i++) { - getTheory().simplify(frames.getFrameReferences(), pmanager, i); - frames.setSimplifiedUntil(i + 1); - const PushFrame & frame = pfstore[frames.getFrameReference(i)]; - + for (std::size_t i = firstNotSimplifiedFrame; i < frames.frameCount() && status != s_False; i++) { if (keepPartitionsSeparate) { - vec const & flas = frame.formulas; - if (flas.size() == 0 or std::all_of(flas.begin(), flas.end(), [&](PTRef fla) { return fla == logic.getTerm_true(); })) { - pmanager.assignTopLevelPartitionIndex(0, logic.getTerm_true()); - status = giveToSolver(logic.getTerm_true(), frame.getId()); + vec frameFormulas = getTheory().simplifyIndividually(frames[i].formulas, pmanager, i == 0); + firstNotSimplifiedFrame = i + 1; + if (frameFormulas.size() == 0 or std::all_of(frameFormulas.begin(), frameFormulas.end(), [&](PTRef fla) { return fla == logic.getTerm_true(); })) { continue; } - for (int j = 0; j < flas.size() && status != s_False; ++j) { - PTRef fla = flas[j]; + for (PTRef fla : frameFormulas) { if (fla == logic.getTerm_true()) { continue; } assert(pmanager.getPartitionIndex(fla) != -1); // Optimize the dag for cnfization @@ -134,25 +142,27 @@ sstat MainSolver::simplifyFormulas() } assert(pmanager.getPartitionIndex(fla) != -1); pmanager.propagatePartitionMask(fla); - status = giveToSolver(fla, frame.getId()); + status = giveToSolver(fla, frames[i].getId()); + if (status == s_False) { break; } } } else { - PTRef root = frame.root; - if (logic.isFalse(root)) { - giveToSolver(getLogic().getTerm_false(), frame.getId()); + PTRef frameFormula = getTheory().simplifyTogether(frames[i].formulas, i == 0); + firstNotSimplifiedFrame = i + 1; + if (logic.isFalse(frameFormula)) { + giveToSolver(getLogic().getTerm_false(), frames[i].getId()); status = s_False; break; } // Optimize the dag for cnfization - if (logic.isBooleanOperator(root)) { - root = rewriteMaxArity(root); + if (logic.isBooleanOperator(frameFormula)) { + frameFormula = rewriteMaxArity(frameFormula); } - root_instance.setRoot(root); - status = giveToSolver(root, frame.getId()); + status = giveToSolver(frameFormula, frames[i].getId()); } } if (status == s_False) { - rememberUnsatFrame(frames.getSimplifiedUntil() - 1); + assert(firstNotSimplifiedFrame > 0); + rememberUnsatFrame(firstNotSimplifiedFrame - 1); } return status; } @@ -177,12 +187,22 @@ std::unique_ptr MainSolver::getModel() { if (status != s_True) { throw OsmtApiException("Model cannot be created if solver is not in SAT state"); } ModelBuilder modelBuilder {logic}; - ts.solver.fillBooleanVars(modelBuilder); + smt_solver->fillBooleanVars(modelBuilder); thandler->fillTheoryFunctions(modelBuilder); return modelBuilder.build(); } +lbool MainSolver::getTermValue(PTRef tr) const { + if (logic.getSortRef(tr) != logic.getSort_bool()) { return l_Undef; } + if (not term_mapper->hasLit(tr)) { return l_Undef; } + + Lit l = term_mapper->getLit(tr); + auto val = smt_solver->modelValue(l); + assert(val != l_Undef); + return val; +} + std::unique_ptr MainSolver::getInterpolationContext() { if (status != s_False) { throw OsmtApiException("Interpolation context cannot be created if solver is not in UNSAT state"); } return std::make_unique( @@ -190,27 +210,72 @@ std::unique_ptr MainSolver::getInterpolationContext() { ); } +PTRef MainSolver::currentRootInstance() const { + vec assertions; + for (auto i = 0u; i < frames.frameCount(); i++) { + auto const & frameAssertions = frames[i].formulas; + for (PTRef assertion : frameAssertions) { + assertions.push(assertion); + } + } + return logic.mkAnd(std::move(assertions)); +} + void MainSolver::printFramesAsQuery() const { char* base_name = config.dump_query_name(); if (base_name == NULL) - getTheory().printFramesAsQuery(frames.getFrameReferences(), std::cout); + printFramesAsQuery(std::cout); else { char* s_file_name; int chars_written = asprintf(&s_file_name, "%s-%d.smt2", base_name, check_called); (void)chars_written; std::ofstream stream; stream.open(s_file_name); - getTheory().printFramesAsQuery(frames.getFrameReferences(), stream); + printFramesAsQuery(stream); stream.close(); free(s_file_name); } free(base_name); } +sstat MainSolver::giveToSolver(PTRef root, MainSolver::FrameId push_id) { + + struct ClauseCallBack : public Cnfizer::ClauseCallBack { + std::vector> clauses; + void operator()(vec && c) override { + clauses.push_back(std::move(c)); + } + }; + ClauseCallBack callBack; + ts.setClauseCallBack(&callBack); + ts.Cnfizer::cnfize(root, push_id.id); + bool keepPartitionsSeparate = getConfig().produce_inter(); + Lit frameLit = push_id.id == 0 ? Lit{} : term_mapper->getOrCreateLit(frameTerms[push_id.id]); + int partitionIndex = keepPartitionsSeparate ? pmanager.getPartitionIndex(root) : -1; + for (auto & clause : callBack.clauses) { + if (push_id.id != 0) { + clause.push(frameLit); + } + opensmt::pair iorefs{CRef_Undef, CRef_Undef}; + bool res = smt_solver->addOriginalSMTClause(std::move(clause), iorefs); + if (keepPartitionsSeparate) { + CRef ref = iorefs.first; + if (ref != CRef_Undef) { + ipartitions_t parts = 0; + assert(partitionIndex != -1); + opensmt::setbit(parts, static_cast(partitionIndex)); + pmanager.addClauseClassMask(ref, parts); + } + } + if (not res) { return s_False; } + } + return s_Undef; +} + sstat MainSolver::check() { - check_called ++; + ++check_called; if (config.timeQueries()) { printf("; %s query time so far: %f\n", solver_name.c_str(), query_timer.getTime()); opensmt::StopWatch sw(query_timer); @@ -218,7 +283,6 @@ sstat MainSolver::check() if (isLastFrameUnsat()) { return s_False; } - initialize(); sstat rval = simplifyFormulas(); if (config.dump_query()) @@ -245,12 +309,17 @@ sstat MainSolver::solve() return s_False; } + // FIXME: Find a better way to deal with Bools in UF + for (PTRef tr : logic.propFormulasAppearingInUF) { + Lit l = term_mapper->getOrCreateLit(tr); + smt_solver->addVar(var(l)); + } + vec en_frames; - for (std::size_t i = 0; i < frames.size(); i++) { - const PushFrame& frame = pfstore[frames.getFrameReference(i)]; - en_frames.push(frame.getId()); + for (std::size_t i = 0; i < frames.frameCount(); ++i) { + en_frames.push(frames[i].getId()); } - status = sstat(solve_(en_frames)); + status = solve_(en_frames); if (status == s_True && config.produce_models()) thandler->computeModel(); @@ -258,6 +327,31 @@ sstat MainSolver::solve() return status; } +sstat MainSolver::solve_(vec const & enabledFrames) { + assert(frameTerms.size() > 0 and frameTerms[0] == logic.getTerm_true()); + vec assumps; + // Initialize so that by default frames are disabled + for (PTRef tr : frameTerms) { + assumps.push(term_mapper->getOrCreateLit(tr)); + } + + // Enable the terms which are listed in enabledFrames + // At this point assumps has the same size as frame_terms and the + // elements are in the same order. We simply invert the + // corresponding literals + uint32_t prevId = UINT32_MAX; + for (FrameId fid : enabledFrames) { + assumps[fid.id] = ~assumps[fid.id]; + smt_solver->mapEnabledFrameIdToVar(var(assumps[fid.id]), fid.id, prevId); + } + // Drop the assumption variable for the base frame (it is at the first place) + for (int i = 1; i < assumps.size(); ++i) { + assumps[i-1] = assumps[i]; + } + assumps.pop(); + return smt_solver->solve(assumps, !config.isIncremental(), config.isIncremental()); +} + std::unique_ptr MainSolver::createInnerSolver(SMTConfig & config, THandler & thandler) { if (config.sat_pure_lookahead()) { return std::make_unique(config, thandler); diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index a7952f208..610c9d450 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -68,35 +68,69 @@ const sstat s_Error = toSstat( 2); class MainSolver { - protected: +public: + struct FrameId + { + uint32_t id; + bool operator== (const FrameId other) const { return id == other.id; } + bool operator!= (const FrameId other) const { return id != other.id; } + }; + +protected: + struct PushFrame { - class PushFramesWrapper { private: - vec frames; - std::size_t simplified_until = 0; // The frame have been simplified up to (excluding) frames[simplified_until]. + FrameId id; + public: - PFRef last() const { assert(frames.size() > 0); return frames.last(); } + FrameId getId() const { return id; } + int size() const { return formulas.size(); } + void push(PTRef tr) { formulas.push(tr); } + PTRef operator[](int i) const { return formulas[i]; } + vec formulas; + bool unsat; // If true then the stack of frames with this frame at top is UNSAT + + PushFrame(PushFrame const &) = delete; + PushFrame(PushFrame &&) = default; + explicit PushFrame(uint32_t id) : id({id}), unsat(false) {} + }; - std::size_t size() const { return frames.size_(); } + class AssertionStack { + private: + std::vector frames; + uint32_t frameId = 0; - const vec& getFrameReferences() const { return frames; } + public: + [[nodiscard]] PushFrame const & last() const { + assert(not frames.empty()); + return frames.back(); + } + [[nodiscard]] PushFrame & last() { + assert(not frames.empty()); + return frames.back(); + } - PFRef getFrameReference(std::size_t i) const { return frames[i]; } + [[nodiscard]] std::size_t frameCount() const { return frames.size(); } - std::size_t getSimplifiedUntil() const { return simplified_until; } + PushFrame const & operator[](std::size_t i) const { + assert(i < frames.size()); + return frames[i]; + } + PushFrame & operator[](std::size_t i) { + assert(i < frames.size()); + return frames[i]; + } - void setSimplifiedUntil(std::size_t n) { simplified_until = n; } + void push() { frames.emplace_back(frameId++); } - void push(PFRef frame_ref) { frames.push(frame_ref); } + void pop() { frames.pop_back(); } - void pop() { - frames.pop(); - if (simplified_until > size()) { simplified_until = size(); } + void add(PTRef fla) { + assert(frameCount() > 0); + last().push(fla); } - }; - std::unique_ptr theory; std::unique_ptr term_mapper; std::unique_ptr thandler; @@ -104,49 +138,52 @@ class MainSolver Logic& logic; PartitionManager pmanager; SMTConfig& config; - PushFrameAllocator& pfstore; Tseitin ts; - PushFramesWrapper frames; + 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; // A counter on how many times check was called. - sstat status; // The status of the last solver call (initially s_Undef) + 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 - class FContainer { - PTRef root; - - public: - FContainer(PTRef r) : root(r) {} - void setRoot (PTRef r) { root = r; } - PTRef getRoot () const { return root; } - }; - - FContainer root_instance; // Contains the root of the instance once simplifications are done - - sstat solve (); + sstat solve(); - virtual sstat solve_(vec & enabledFrames) { - return ts.solve(enabledFrames); - } + virtual sstat solve_(vec const & enabledFrames); - sstat giveToSolver(PTRef root, FrameId push_id) { - if (ts.cnfizeAndGiveToSolver(root, push_id) == l_False) return s_False; - return s_Undef; } + sstat giveToSolver(PTRef root, FrameId push_id); PTRef rewriteMaxArity(PTRef); + [[nodiscard]] PTRef currentRootInstance() const; + // helper private methods - PushFrame& getLastFrame() const { return pfstore[frames.last()]; } - bool isLastFrameUnsat() const { return getLastFrame().unsat; } - void rememberLastFrameUnsat() { getLastFrame().unsat = true; } + 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.size()); - for (; frameIndex < frames.size(); ++frameIndex) { - pfstore[frames.getFrameReference(frameIndex)].unsat = true; + 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); } static std::unique_ptr createInnerSolver(SMTConfig& config, THandler& thandler); @@ -163,17 +200,14 @@ class MainSolver logic(thandler->getLogic()), pmanager(logic), config(conf), - pfstore(getTheory().pfstore), - ts( config, logic, pmanager, *term_mapper, *smt_solver ), - solver_name {std::move(name)}, - check_called(0), - status(s_Undef), - root_instance(logic.getTerm_true()) + ts(logic, *term_mapper), + solver_name {std::move(name)} { conf.setUsedForInitiliazation(); - frames.push(pfstore.alloc()); - PushFrame& last = pfstore[frames.last()]; - last.push(logic.getTerm_true()); + // Special handling of zero-level frame + frames.push(); + frameTerms.push(logic.getTerm_true()); + initialize(); } MainSolver(std::unique_ptr th, std::unique_ptr tm, std::unique_ptr thd, @@ -186,17 +220,13 @@ class MainSolver logic(thandler->getLogic()), pmanager(logic), config(conf), - pfstore(getTheory().pfstore), - ts( config, logic, pmanager, *term_mapper, *smt_solver ), - solver_name {std::move(name)}, - check_called(0), - status(s_Undef), - root_instance(logic.getTerm_true()) + ts(logic,*term_mapper), + solver_name {std::move(name)} { conf.setUsedForInitiliazation(); - frames.push(pfstore.alloc()); - PushFrame& last = pfstore[frames.last()]; - last.push(logic.getTerm_true()); + frames.push(); + frameTerms.push(logic.getTerm_true()); + initialize(); } virtual ~MainSolver() = default; @@ -206,7 +236,7 @@ class MainSolver MainSolver& operator = (MainSolver&&) = delete; SMTConfig& getConfig() { return config; } - SimpSMTSolver& getSMTSolver() { return *smt_solver; } + SimpSMTSolver & getSMTSolver() { return *smt_solver; } SimpSMTSolver const & getSMTSolver() const { return *smt_solver; } THandler &getTHandler() { return *thandler; } @@ -218,7 +248,7 @@ class MainSolver bool pop(); void insertFormula(PTRef fla); - void initialize() { ts.solver.initialize(); ts.initialize(); } + void initialize(); virtual sstat check(); // A wrapper for solve which simplifies the loaded formulas and initializes the solvers // Simplify frames (not yet simplified) until all are simplified or the instance is detected unsatisfiable. @@ -226,15 +256,14 @@ class MainSolver void printFramesAsQuery() const; sstat getStatus () const { return status; } - bool solverEmpty () const { return ts.solverEmpty(); } // Values - lbool getTermValue (PTRef tr) const { return ts.getTermValue(tr); } + lbool getTermValue (PTRef tr) const; // Returns model of the last query (must be in satisfiable state) std::unique_ptr getModel(); - void stop() { ts.solver.stop = true; } + void stop() { smt_solver->stop = true; } // Returns interpolation context for the last query (must be in UNSAT state) std::unique_ptr getInterpolationContext(); @@ -242,4 +271,4 @@ class MainSolver static std::unique_ptr createTheory(Logic & logic, SMTConfig & config); }; -#endif // +#endif // MAINSOLVER_H diff --git a/src/api/Opensmt.cc b/src/api/Opensmt.cc index 40c7b1e7a..034c01512 100644 --- a/src/api/Opensmt.cc +++ b/src/api/Opensmt.cc @@ -52,7 +52,6 @@ Opensmt::Opensmt(opensmt_logic _logic, const char* name) config = std::unique_ptr(new SMTConfig()); logic.reset(opensmt::LogicFactory::getInstance(convert(_logic))); mainSolver = std::unique_ptr(new MainSolver(*logic, *config, name)); - mainSolver->initialize(); } Opensmt::Opensmt(opensmt_logic logic_, const char* name, std::unique_ptr config_) @@ -60,5 +59,4 @@ Opensmt::Opensmt(opensmt_logic logic_, const char* name, std::unique_ptrconfig = std::move(config_); logic.reset(opensmt::LogicFactory::getInstance(convert(logic_))); mainSolver = std::unique_ptr(new MainSolver(*logic, *this->config, name)); - mainSolver->initialize(); } diff --git a/src/cnfizers/Cnfizer.cc b/src/cnfizers/Cnfizer.cc index 221679ba8..73ce628eb 100644 --- a/src/cnfizers/Cnfizer.cc +++ b/src/cnfizers/Cnfizer.cc @@ -41,272 +41,92 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #define TRACE_FLA_VEC(v) #endif // PEDANTIC_DEBUG -using namespace std; +Cnfizer::Cnfizer(Logic & logic, TermMapper & tmap) + : logic(logic), tmap(tmap) {} -Cnfizer::Cnfizer ( SMTConfig &config_ - , Logic &logic_ - , PartitionManager &pmanager_ - , TermMapper &tmap - , SimpSMTSolver &solver_ - ) : - solver (solver_) - , config (config_ ) - , logic (logic_) - , pmanager (pmanager_) - , tmap (tmap) - , s_empty (true) - , alreadyAsserted(logic.getTerm_true()) - , frame_terms({logic.getTerm_true()}) // Frame 0 does not have an enabling var - , current_frame_term(frame_terms[0]) -{ } -void Cnfizer::initialize() -{ - // TODO: MB: why is all this initialization necessary? - currentPartition = 0; - vec c; - Lit l = this->getOrCreateLiteralFor (logic.getTerm_true()); - c.push (l); - addClause(c); - c.pop(); - l = this->getOrCreateLiteralFor (logic.getTerm_false()); - c.push (~l); - addClause(c); - currentPartition = -1; -} - -lbool -Cnfizer::solve(vec& en_frames) -{ - vec assumps; - // Initialize so that by default frames are disabled - for (PTRef tr : frame_terms) { - assumps.push(this->getOrCreateLiteralFor(tr)); - } - - // Enable the terms which are listed in en_frames - // At this point assumps has the same size as frame_terms and the - // elements are in the same order. We simply invert the - // corresponding literals - uint32_t prevId = UINT32_MAX; - for (FrameId fid : en_frames) { - assumps[fid.id] = ~assumps[fid.id]; - solver.mapEnabledFrameIdToVar(var(assumps[fid.id]), fid.id, prevId); - } - - // Filter out the lit_Trues and lit_Falses used as empty values - Lit lit_true = this->getOrCreateLiteralFor(logic.getTerm_true()); - int i, j; - for (i = j = 0; i < assumps.size(); i++) { - if (assumps[i] != lit_true && assumps[i] != ~lit_true) - assumps[j++] = assumps[i]; - } - assumps.shrink(i-j); - return solver.solve(assumps, !config.isIncremental(), config.isIncremental()); - -} - -void Cnfizer::setFrameTerm(FrameId frame_id) -{ - while (static_cast(frame_terms.size()) <= frame_id.id) { - frame_terms.push(logic.getTerm_true()); - } - // frame_id == {0} is for the bottom frame and we don't want to add - // literals to it since it is never retracted. - if (frame_id != FrameId_bottom && frame_terms[frame_id.id] == logic.getTerm_true()) { - std::string name {Logic::s_framev_prefix}; - name += std::to_string(frame_id.id); - PTRef frame_term = logic.mkBoolVar(name.c_str()); - frame_terms[frame_id.id] = frame_term; - } - - current_frame_term = frame_terms[frame_id.id]; -} - -// // Main Routine. Examine formula and give it to the solver -// -lbool Cnfizer::cnfizeAndGiveToSolver(PTRef formula, FrameId frame_id) -{ - // Get the variable for the incrementality. - setFrameTerm(frame_id); - - if (!solver.isOK()) return l_False; - - assert ( formula != PTRef_Undef); +void Cnfizer::cnfize(PTRef formula, FrameId frame_id) { + currentFrameId = frame_id; + assert(formula != PTRef_Undef and logic.getSortRef(formula) == logic.getSort_bool()); TRACE("cnfizerAndGiveToSolver: " << logic.printTerm (formula)) - if (keepPartitionInfo()) { - assert(pmanager.getPartitionIndex(formula) != -1); - currentPartition = pmanager.getPartitionIndex(formula); - } - // Retrieve top-level formulae - this is a list constructed from a conjunction - vec top_level_formulae = topLevelConjuncts(logic, formula); + vec top_level_formulae = ::topLevelConjuncts(logic, formula); assert (top_level_formulae.size() != 0); TRACE("Top level formulae:") TRACE_FLA_VEC(top_level_formulae) - bool res = true; // For each top-level conjunct - for (unsigned i = 0 ; i < top_level_formulae.size_() && (res == true) ; i ++) + for (PTRef topLevelConjunct : top_level_formulae) { - PTRef f = top_level_formulae[i]; - assert(not logic.isAnd(f)); // Conjunction should have been split when retrieving top-level formulae - if (alreadyAsserted.contains(f, current_frame_term)) { + assert(not logic.isAnd(topLevelConjunct)); // Conjunction should have been split when retrieving top-level formulae + if (alreadyProcessed.contains(topLevelConjunct, frame_id)) { continue; } TRACE("Adding clause " << logic.printTerm (f)) // Give it to the solver if already in CNF - if (isClause(f)) { + if (isClause(topLevelConjunct)) { TRACE(" => Already a clause") - res = assertClause(f); - } else if (checkDeMorgan(f)) { + processClause(topLevelConjunct); + } else if (checkDeMorgan(topLevelConjunct)) { // Check whether it can be rewritten using deMorgan laws TRACE(" => Will be de Morganized") - res = deMorganize (f); + deMorganize(topLevelConjunct); } else { TRACE(" => proper cnfization") - res = cnfizeAndAssert (f); // Perform actual cnfization (implemented in subclasses) + cnfizeAndAssert(topLevelConjunct); // Perform actual cnfization (implemented in subclasses) } - alreadyAsserted.insert(f, current_frame_term); + alreadyProcessed.insert(topLevelConjunct, frame_id); } - s_empty = false; // solver no longer empty - if (res) { - vec nestedBoolRoots = getNestedBoolRoots(formula); - for (PTRef tr : nestedBoolRoots) { - res &= cnfize(tr); // cnfize the formula without asserting the top level - } - assert(res); - declareVars(logic.propFormulasAppearingInUF); + vec nestedBoolRoots = logic.getNestedBoolRoots(formula); + for (PTRef tr : nestedBoolRoots) { + cnfize(tr); // cnfize the formula without asserting the top level } - - currentPartition = -1; - return res == false ? l_False : l_Undef; } -bool Cnfizer::cnfizeAndAssert(PTRef formula) { - assert(formula != PTRef_Undef); - // Top level formula must not be and anymore - assert(!logic.isAnd(formula)); - bool res = true; +void Cnfizer::cnfizeAndAssert(PTRef formula) { + assert(formula != PTRef_Undef and not logic.isAnd(formula)); // Add the top level literal as a unit to solver. - vec clause; - clause.push(this->getOrCreateLiteralFor(formula)); - res &= addClause(clause); - - res &= cnfize(formula); - return res; -} - -void Cnfizer::declareVars(vec& vars) -{ - for (PTRef tr : vars) { - Lit l = tmap.getOrCreateLit(tr); - solver.addVar(var(l)); - } + addClause({this->getOrCreateLiteralFor(formula)}); + cnfize(formula); } -// // Apply simple de Morgan laws to the formula -// - -bool Cnfizer::deMorganize ( PTRef formula ) -{ - assert (!logic.isAnd (formula)); - Pterm &pt = logic.getPterm (formula); - - bool rval = true; - - // - // Case (not (and a b)) --> (or (not a) (not b)) - // - if (logic.isNot (formula) && logic.isAnd (pt[0])) - { - vec conjuncts; - vec clause; - - retrieveConjuncts (pt[0], conjuncts); - - for (PTRef tr : conjuncts) { - clause.push (~this->getOrCreateLiteralFor(tr)); - TRACE("(not " << logic.printTerm (tr) << ")") - } - - rval = addClause(clause); - } - - return rval; -} - - - -// -// Check whether a formula is in cnf -// - -bool Cnfizer::isCnf(PTRef e) { - return isConjunctionOfClauses(e); -} - - - -bool Cnfizer::isConjunctionOfClauses(PTRef e) { - if (isClause(e)) { // Single clause counts as a conjunction of clauses - return true; - } - if (not logic.isAnd(e)) { - return false; - } - vec to_process; - to_process.push (e); - - while (to_process.size() != 0) { - e = to_process.last(); - to_process.pop(); - - Pterm const & and_t = logic.getPterm(e); - - for (PTRef tr : and_t) { - if (logic.isAnd(tr)) { - to_process.push(tr); - } else if (not isClause(tr)) { - return false; - } - } +void Cnfizer::deMorganize(PTRef formula) { + assert(logic.isNot(formula)); + Pterm const & term = logic.getPterm(formula); + assert(logic.isAnd(term[0])); + vec conjuncts; + vec clause; + retrieveConjuncts(term[0], conjuncts); + for (PTRef tr : conjuncts) { + clause.push(~this->getOrCreateLiteralFor(tr)); + TRACE("(not " << logic.printTerm(tr) << ")") } - return true; + addClause(std::move(clause)); } - // // Check whether a formula is a clause // bool Cnfizer::isClause(PTRef e) { assert (e != PTRef_Undef); - if (isLiteral(e)) { // Single literals count as clauses return true; } - if (not logic.isOr(e)) { return false; } - vec to_process; - - to_process.push (e); - + to_process.push(e); while (to_process.size() != 0) { - e = to_process.last(); + PTRef current = to_process.last(); to_process.pop(); - - Pterm const & or_t = logic.getPterm (e); - - for (PTRef tr : or_t) { - if (logic.isOr(tr)) { - to_process.push(tr); + for (PTRef child : logic.getPterm(current)) { + if (logic.isOr(child)) { + to_process.push(child); } else { - if (not isLiteral(tr)) { + if (not isLiteral(child)) { return false; } } @@ -317,178 +137,92 @@ bool Cnfizer::isClause(PTRef e) { -// -// Check whether it can be easily put in clausal form by means of DeMorgan's Rules -// -bool Cnfizer::checkDeMorgan (PTRef e) -{ - Map > check_cache; - const Pterm ¬_t = logic.getPterm (e); - - if (logic.isNot (e) && checkPureConj (not_t[0], check_cache) ) return true; - else return false; +// Check if this is a negation of a clause +bool Cnfizer::checkDeMorgan(PTRef e) { + Pterm const & term = logic.getPterm(e); + if (not logic.isNot(term.symb())) return false; + Map> check_cache; + return checkPureConj(term[0], check_cache); } -// // Check whether it is a pure conjunction of literals -// -bool Cnfizer::checkPureConj (PTRef e, Map > &check_cache) -{ - if (check_cache.has (e)) - return true; +bool Cnfizer::checkPureConj(PTRef e, Map> & check_cache) { + if (check_cache.has(e)) return true; + if (not logic.isAnd(e)) return false; vec to_process; - to_process.push (e); - - // Topmost needs to be and - if (!logic.isAnd (e)) return false; - - while (to_process.size() != 0) - { - e = to_process.last(); + to_process.push(e); + while (to_process.size() != 0) { + PTRef current = to_process.last(); to_process.pop(); - Pterm &and_t = logic.getPterm (e); - if (logic.isAnd(e)) { - for (PTRef tr : and_t) { + if (logic.isAnd(current)) { + for (PTRef tr : logic.getPterm(current)) { to_process.push(tr); } - } else if (not isLiteral(e)) { + } else if (not isLiteral(current)) { return false; } - check_cache.insert (e, true); + check_cache.insert(current, true); } - return true; } -bool Cnfizer::addClause(const vec & c_in) +void Cnfizer::addClause(vec && clause) { - vec c; - c_in.copyTo(c); - if (current_frame_term != logic.getTerm_true()) { - Lit l = this->getOrCreateLiteralFor(current_frame_term); - Var v = var(l); - tmap.setFrozen(v); - solver.addAssumptionVar(v); - c.push(l); - } - -#ifdef PEDANTIC_DEBUG - cerr << "== clause start" << endl; - - for (int i = 0; i < c.size(); i++) - { - cerr << "(" << c[i].x << "," << var (c[i]) << ") * " << (sign (c[i]) ? "not " : "") - << logic.printTerm (tmap.varToPTRef (var (c[i]))) - << " "; - cerr << endl; - } - -#endif - opensmt::pair iorefs{CRef_Undef, CRef_Undef}; - bool res = solver.addOriginalSMTClause(c, iorefs); - if (keepPartitionInfo()) { - CRef ref = iorefs.first; - if (ref != CRef_Undef) { - ipartitions_t parts = 0; - assert(currentPartition != -1); - opensmt::setbit(parts, static_cast(currentPartition)); - pmanager.addClauseClassMask(ref, parts); - } - } - return res; + (*clauseCallBack)(std::move(clause)); } -// -// Give the formula to the solver -// -bool Cnfizer::assertClause (PTRef f) -{ - vec clause; - // - // A unit clause - // +void Cnfizer::processClause(PTRef f) { if (isLiteral(f)) { - clause.push(this->getOrCreateLiteralFor(f)); - return addClause(clause); + addClause({getOrCreateLiteralFor(f)}); + return; } - - // - // A clause - // - if (logic.isOr(f)) { - vec lits; - retrieveClause (f, lits); - - for (PTRef tr : lits) - clause.push(this->getOrCreateLiteralFor(tr)); - - return addClause(clause); + vec lits; + retrieveClause(f, lits); + addClause(std::move(lits)); + return; } throw OsmtInternalException("UNREACHABLE: Unexpected situation in Cnfizer"); } -// -// Retrieve a clause -// -void Cnfizer::retrieveClause ( PTRef f, vec &clause ) -{ - assert (isLiteral(f) || logic.isOr (f)); - +void Cnfizer::retrieveClause(PTRef f, vec & clause) { + assert(isLiteral(f) or logic.isOr(f)); if (isLiteral(f)) { - clause.push(f); - } else if ( logic.isOr (f) ) { - Pterm const &t = logic.getPterm (f); + clause.push(getOrCreateLiteralFor(f)); + } else if (logic.isOr(f)) { + Pterm const & t = logic.getPterm(f); for (PTRef tr : t) { retrieveClause(tr, clause); } } } -// -// Retrieve conjuncts -// -void Cnfizer::retrieveConjuncts ( PTRef f, vec &conjuncts ) -{ - assert (isLiteral(f) || logic.isAnd (f)); - +void Cnfizer::retrieveConjuncts(PTRef f, vec & conjuncts) { + assert(isLiteral(f) or logic.isAnd(f)); if (isLiteral(f)) { conjuncts.push(f); } else { - Pterm &t = logic.getPterm (f); - + Pterm const & t = logic.getPterm(f); for (PTRef tr : t) { retrieveConjuncts(tr, conjuncts); } } } - -lbool Cnfizer::getTermValue (PTRef tr) const -{ - assert (solver.isOK()); - if (tmap.hasLit(tr)) { - Lit l = tmap.getLit(tr); - lbool val = solver.modelValue(l); - assert (val != l_Undef); - return val; - } - else return l_Undef; -} - -bool Cnfizer::Cache::contains(PTRef term, PTRef frame_term) { - return cache.find(std::make_pair<>(term, frame_term)) != cache.end() - || ( frame_term != zeroLevelTerm && cache.find(std::make_pair<>(term, zeroLevelTerm)) != cache.end()); +bool Cnfizer::Cache::contains(PTRef term, FrameId frame) { + return cache.find({term, frame}) != cache.end() + or ( frame != baseFrame and cache.find({term, baseFrame}) != cache.end()); } -void Cnfizer::Cache::insert(PTRef term, PTRef frame_term) { - assert(!contains(term, frame_term)); - cache.insert(std::make_pair<>(term, frame_term)); +void Cnfizer::Cache::insert(PTRef term, FrameId frame) { + assert(!contains(term, frame)); + cache.insert({term, frame}); } +// TODO: Fix isAtom!!! (everything that is not a boolean connective should be considered as atom bool Cnfizer::isLiteral(PTRef ptr) const { return (logic.isNot(ptr) and logic.isAtom(logic.getPterm(ptr)[0])) or logic.isAtom(ptr); } diff --git a/src/cnfizers/Cnfizer.h b/src/cnfizers/Cnfizer.h index 793f1315e..66a7992bc 100644 --- a/src/cnfizers/Cnfizer.h +++ b/src/cnfizers/Cnfizer.h @@ -38,41 +38,47 @@ class SimpSMTSolver; class THandler; struct SMTConfig; + + // // Generic class for conversion into CNF // class Cnfizer { public: - SimpSMTSolver& solver; + struct ClauseCallBack { + virtual void operator()(vec &&) = 0; + }; protected: - SMTConfig& config; - Logic& logic; - PartitionManager& pmanager; - TermMapper& tmap; - bool s_empty; + using FrameId = uint32_t; // TODO: Unify this with FrameId of MainSolver class Cache { - PTRef zeroLevelTerm; - using CacheEntry = std::pair; - std::unordered_set cache; + using CacheEntry = std::pair; + + struct EntryHash { + std::size_t operator () (CacheEntry entry) const { + std::hash hasher; + return (hasher(entry.first.x) ^ hasher(entry.second)); + } + }; + + FrameId baseFrame = 0; + std::unordered_set cache; public: - Cache(PTRef zeroLevelTerm): zeroLevelTerm(zeroLevelTerm) {} - bool contains(PTRef term, PTRef frame_term); - void insert(PTRef term, PTRef frame_term); + Cache() = default; + bool contains(PTRef term, FrameId frame); + void insert(PTRef term, FrameId frame); }; - Cache alreadyAsserted; + Logic & logic; + TermMapper & tmap; + Cache alreadyProcessed; + ClauseCallBack * clauseCallBack; -public: - Cnfizer( SMTConfig & config_ - , Logic& logic_ - , PartitionManager& pmanager_ - , TermMapper& tmap_ - , SimpSMTSolver& solver_ - ); +public: + Cnfizer(Logic & logic, TermMapper & tmap); virtual ~Cnfizer() = default; Cnfizer (const Cnfizer&) = delete; @@ -80,53 +86,31 @@ class Cnfizer Cnfizer (Cnfizer&&) = default; Cnfizer& operator = (Cnfizer&&) = delete; - lbool cnfizeAndGiveToSolver (PTRef, FrameId frame_id); // Main routine - - lbool getTermValue(PTRef) const; - - void initialize (); - lbool solve (vec& en_frames); + void cnfize(PTRef, FrameId frame_id); - bool solverEmpty () const { return s_empty; } + void setClauseCallBack(ClauseCallBack * callback) { assert(callback); this->clauseCallBack = callback; } protected: + virtual void cnfize(PTRef) = 0; // Actual cnfization. To be implemented in derived classes + void cnfizeAndAssert(PTRef); // Cnfize and assert the top-level. - virtual bool cnfizeAndAssert ( PTRef ); // Cnfize and assert the top-level. - virtual bool cnfize ( PTRef ) = 0; // Actual cnfization. To be implemented in derived classes - bool deMorganize ( PTRef ); // Apply deMorgan rules whenever feasible - void declareVars (vec&); // Declare a set of Boolean atoms to the solver (without asserting them) + bool isClause(PTRef); + bool checkDeMorgan(PTRef); + void processClause(PTRef f); + void addClause(vec &&); + void deMorganize(PTRef); -public: - bool isClause (PTRef); - bool isCnf (PTRef); - bool checkDeMorgan ( PTRef ); // Check if formula can be deMorganized -protected: - - bool assertClause (PTRef f); // Gives formula to the SAT solver - - - bool addClause(const vec &); - - void retrieveClause ( PTRef, vec & ); // Retrieve a clause from a formula - void retrieveConjuncts ( PTRef, vec & ); // Retrieve the list of conjuncts + void retrieveClause(PTRef, vec &); + void retrieveConjuncts(PTRef, vec &); // Retrieve the list of conjuncts private: - - bool isConjunctionOfClauses (PTRef); - bool checkPureConj (PTRef, Map& check_cache); // Check if a formula is purely a conjuntion + bool checkPureConj(PTRef, Map & check_cache); // Check if a formula is purely a conjuntion protected: bool isLiteral(PTRef ptr) const; inline Lit getOrCreateLiteralFor(PTRef ptr) {return this->tmap.getOrCreateLit(ptr);} - inline vec getNestedBoolRoots(PTRef ptr) { return logic.getNestedBoolRoots(ptr); } - - bool keepPartitionInfo() const { return config.produce_inter(); } - - int currentPartition = -1; - vec frame_terms; - PTRef current_frame_term; - void setFrameTerm(FrameId frame_id); + FrameId currentFrameId = 0; }; #endif diff --git a/src/cnfizers/Tseitin.cc b/src/cnfizers/Tseitin.cc index 8a245d0a2..debeeb658 100644 --- a/src/cnfizers/Tseitin.cc +++ b/src/cnfizers/Tseitin.cc @@ -1,53 +1,23 @@ -/********************************************************************* -Author: Antti Hyvarinen +/* + * Copyright (c) 2008-2012, Roberto Bruttomesso + * Copyright (c) 2012-2022, Antti Hyvarinen + * Copyright (c) 2022-2023, Martin Blicha + * + * SPDX-License-Identifier: MIT + * + */ -OpenSMT2 -- Copyright (C) 2012 - 2014 Antti Hyvarinen - 2008 - 2012 Roberto Bruttomesso - -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. -*********************************************************************/ - -#include "Cnfizer.h" #include "Tseitin.h" - -// -// Performs the actual cnfization -// - - -bool Tseitin::cnfize(PTRef term) { - bool res = true; +void Tseitin::cnfize(PTRef term) { vec unprocessed_terms {term}; - // // Visit the DAG of the formula - // while (unprocessed_terms.size() != 0) { - PTRef ptr = unprocessed_terms.last(); unprocessed_terms.pop(); - // // Skip if the node has already been processed before - // - if (alreadyCnfized.contains(ptr, current_frame_term)){ + if (alreadyCnfized.contains(ptr, currentFrameId)){ continue; } @@ -55,303 +25,136 @@ bool Tseitin::cnfize(PTRef term) { // by calling findLit int sz = logic.getPterm(ptr).size(); if (logic.isAnd(ptr)) - res &= cnfizeAnd(ptr); + cnfizeAnd(ptr); else if (logic.isOr(ptr)) - res &= cnfizeOr(ptr); + cnfizeOr(ptr); else if (logic.isXor(ptr)) - res &= cnfizeXor(ptr); + cnfizeXor(ptr); else if (logic.isIff(ptr)) - res &= cnfizeIff(ptr); + cnfizeIff(ptr); else if (logic.isImplies(ptr)) - res &= cnfizeImplies(ptr); + cnfizeImplies(ptr); // Ites are handled through the ite manager system and treated here as variables // else if (logic.isIte(ptr)) // res &= cnfizeIfthenelse(ptr); - else if (!logic.isNot(ptr) && sz > 0) { + else if (!logic.isNot(ptr) && sz > 0) { // do not recurse into atoms goto tseitin_end; } - { - Pterm const& pt = logic.getPterm(ptr); - for (int i = 0; i < pt.size(); i++) { - unprocessed_terms.push(pt[i]); // Using the PTRef is safe if a reallocation happened - } + for (PTRef child : logic.getPterm(ptr)) { + unprocessed_terms.push(child); } tseitin_end: - alreadyCnfized.insert(ptr, current_frame_term); + alreadyCnfized.insert(ptr, currentFrameId); } - - return res; } - -bool Tseitin::cnfizeAnd(PTRef and_term) -{ -// assert( list ); -// assert( list->isList( ) ); - // +void Tseitin::cnfizeAnd(PTRef and_term) { // ( a_0 & ... & a_{n-1} ) - // // <=> - // // aux = ( -aux | a_0 ) & ... & ( -aux | a_{n-1} ) & ( aux & -a_0 & ... & -a_{n-1} ) - // Lit v = this->getOrCreateLiteralFor(and_term); - vec little_clause; vec big_clause; int size = logic.getPterm(and_term).size(); big_clause.capacity(size + 1); - little_clause.push(~v); - big_clause .push(v); - bool res = true; - for (int i = 0; i < size; i++) { + big_clause.push(v); + for (int i = 0; i < size; ++i) { PTRef arg = logic.getPterm(and_term)[i]; - little_clause.push( this->getOrCreateLiteralFor(arg) ); - big_clause .push(~this->getOrCreateLiteralFor(arg)); - res &= addClause(little_clause); // Adds a little clause to the solver - little_clause.pop(); + Lit argLit = this->getOrCreateLiteralFor(arg); + big_clause.push(~argLit); + addClause({~v, argLit}); } - res &= addClause(big_clause); // Adds a big clause to the solver - return res; + addClause(std::move(big_clause)); } - - -bool Tseitin::cnfizeOr(PTRef or_term) -{ - // +void Tseitin::cnfizeOr(PTRef or_term) { // ( a_0 | ... | a_{n-1} ) - // // <=> - // // aux = ( aux | -a_0 ) & ... & ( aux | -a_{n-1} ) & ( -aux | a_0 | ... | a_{n-1} ) - // - vec little_clause; - vec big_clause; Lit v = this->getOrCreateLiteralFor(or_term); - little_clause.push( v); - big_clause .push(~v); - bool res = true; - for (int i = 0 ; i < logic.getPterm(or_term).size(); i++) { - Lit arg = this->getOrCreateLiteralFor(logic.getPterm(or_term)[i]); - little_clause.push(~arg); - big_clause .push( arg); - - res &= addClause(little_clause); // Adds a little clause to the solver - - little_clause.pop(); + vec big_clause; + int size = logic.getPterm(or_term).size(); + big_clause.push(~v); + for (int i = 0; i < size; ++i) { + PTRef arg = logic.getPterm(or_term)[i]; + Lit argLit = this->getOrCreateLiteralFor(arg); + big_clause.push(argLit); + addClause({v,~argLit}); } - res &= addClause(big_clause); // Adds a big clause to the solver - return res; + addClause(std::move(big_clause)); } - -bool Tseitin::cnfizeXor(PTRef xor_term) -{ - // +void Tseitin::cnfizeXor(PTRef xor_term) { // ( a_0 xor a_1 ) - // // <=> - // // aux = ( -aux | a_0 | a_1 ) & ( -aux | -a_0 | -a_1 ) & // ( aux | -a_0 | a_1 ) & ( aux | a_0 | -a_1 ) - // Lit v = this->getOrCreateLiteralFor(xor_term); - Lit arg0 = this->getOrCreateLiteralFor(logic.getPterm(xor_term)[0]); Lit arg1 = this->getOrCreateLiteralFor(logic.getPterm(xor_term)[1]); - vec clause; - bool res = true; - - clause.push(~v); // First clause - clause.push(arg0); - clause.push(arg1); - - res &= addClause(clause); - clause.pop(); - clause.pop(); - + addClause({~v, arg0, arg1}); // Second clause - clause.push(~arg0); - clause.push(~arg1); - - res &= addClause(clause); - clause.pop(); - clause.pop(); - - clause.pop(); - clause.push(v); - + addClause({~v, ~arg0, ~arg1}); // Third clause - clause.push(~arg0); - clause.push( arg1); - - res &= addClause(clause); - - clause.pop(); - clause.pop(); - + addClause({v, ~arg0, arg1}); // Fourth clause - clause.push( arg0); - clause.push(~arg1); - - res &= addClause(clause); - return res; + addClause({v, arg0, ~arg1}); } -bool Tseitin::cnfizeIff(PTRef eq_term) -{ - - // +void Tseitin::cnfizeIff(PTRef eq_term) { // ( a_0 <-> a_1 ) - // // <=> - // // aux = ( -aux | a_0 | -a_1 ) & ( -aux | -a_0 | a_1 ) & // ( aux | a_0 | a_1 ) & ( aux | -a_0 | -a_1 ) - // assert(logic.getPterm(eq_term).size() == 2); Lit v = this->getOrCreateLiteralFor(eq_term); Lit arg0 = this->getOrCreateLiteralFor(logic.getPterm(eq_term)[0]); Lit arg1 = this->getOrCreateLiteralFor(logic.getPterm(eq_term)[1]); - vec clause; - bool res = true; - - clause.push(~v); // First clause - clause.push( arg0); - clause.push(~arg1); - - res &= addClause(clause); - - clause.pop(); - clause.pop(); - + addClause({~v, arg0, ~arg1}); // Second clause - clause.push(~arg0); - clause.push( arg1); - - res &= addClause(clause); - - clause.pop(); - clause.pop(); - - clause.pop(); - clause.push(v); - + addClause({~v, ~arg0, arg1}); // Third clause - clause.push(arg0); - clause.push(arg1); - - res &= addClause(clause); - - clause.pop(); - clause.pop(); - + addClause({v, arg0, arg1}); // Fourth clause - clause.push(~arg0); - clause.push(~arg1); - - res &= addClause(clause); - return res; + addClause({v, ~arg0, ~arg1}); } - -bool Tseitin::cnfizeIfthenelse(PTRef ite_term) -{ +void Tseitin::cnfizeIfthenelse(PTRef ite_term) { // (!a | !i | t) & (!a | i | e) & (a | !i | !t) & (a | i | !e) - // // ( if a_0 then a_1 else a_2 ) - // // <=> - // // aux = ( -aux | -a_0 | a_1 ) & // ( -aux | a_0 | a_2 ) & // ( aux | -a_0 | -a_1 ) & // ( aux | a_0 | -a_2 ) - // - Pterm& pt_ite = logic.getPterm(ite_term); - assert(pt_ite.size() == 3); - - Lit v = this->getOrCreateLiteralFor(ite_term); - Lit a0 = this->getOrCreateLiteralFor(pt_ite[0]); - Lit a1 = this->getOrCreateLiteralFor(pt_ite[1]); - Lit a2 = this->getOrCreateLiteralFor(pt_ite[2]); - - vec clause; - bool res = true; - - clause.push(~v); clause.push(~a0); clause.push(a1); - - res &= addClause(clause); - - clause.clear(); - - clause.push(~v); clause.push(a0); clause.push(a2); - res &= addClause(clause); - clause.clear(); - - clause.push(v); clause.push(~a0); clause.push(~a1); - res &= addClause(clause); - clause.clear(); - - clause.push(v); clause.push(a0); clause.push(~a2); - res &= addClause(clause); - return res; + assert(logic.getPterm(ite_term).size() == 3); + Lit v = this->getOrCreateLiteralFor(ite_term); + Lit a0 = this->getOrCreateLiteralFor(logic.getPterm(ite_term)[0]); + Lit a1 = this->getOrCreateLiteralFor(logic.getPterm(ite_term)[1]); + Lit a2 = this->getOrCreateLiteralFor(logic.getPterm(ite_term)[2]); + + addClause({~v, ~a0, a1}); + addClause({~v, a0, a2}); + addClause({v, ~a0, ~a1}); + addClause({v, a0, ~a2}); } - -bool Tseitin::cnfizeImplies(PTRef impl_term) -{ +void Tseitin::cnfizeImplies(PTRef impl_term) { // ( a_0 => a_1 ) - // // <=> - // // aux = ( -aux | -a_0 | a_1 ) & // ( aux | a_0 ) & // ( aux | -a_1 ) - // - - Pterm& pt_impl = logic.getPterm(impl_term); - assert(pt_impl.size() == 2); - - Lit v = this->getOrCreateLiteralFor(impl_term); - Lit a0 = this->getOrCreateLiteralFor(pt_impl[0]); - Lit a1 = this->getOrCreateLiteralFor(pt_impl[1]); - - vec clause; - bool res = true; - - clause.push(v); - - clause.push(a0); - - res &= addClause(clause); - - clause.pop(); - - clause.push(~a1); - - res &= addClause(clause); - - clause.clear(); - - clause.push(~v); clause.push(~a0); clause.push(a1); - - res &= addClause(clause); - return res; -} - -//void Tseitin::copyArgsWithCache(PTRef tr, vec& args, Map& cache) -//{ -// Pterm& t = logic.getPterm(tr); -// for (int i = 0; i < t.size(); i++) { -// if (cache.has(t[i])) -// args.push(cache[t[i]]); -// else -// args.push(t[i]); -// } -//} + assert(logic.getPterm(impl_term).size() == 2); + Lit v = this->getOrCreateLiteralFor(impl_term); + Lit a0 = this->getOrCreateLiteralFor(logic.getPterm(impl_term)[0]); + Lit a1 = this->getOrCreateLiteralFor(logic.getPterm(impl_term)[1]); + + addClause({v, a0}); + addClause({v, ~a1}); + addClause({~v, ~a0, a1}); +} \ No newline at end of file diff --git a/src/cnfizers/Tseitin.h b/src/cnfizers/Tseitin.h index 93db76116..7e72f781e 100644 --- a/src/cnfizers/Tseitin.h +++ b/src/cnfizers/Tseitin.h @@ -1,28 +1,11 @@ -/********************************************************************* -Author: Antti Hyvarinen - -OpenSMT2 -- Copyright (C) 2012 - 2014 Antti Hyvarinen - 2008 - 2012 Roberto Bruttomesso - -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) 2008-2012, Roberto Bruttomesso +* Copyright (c) 2012-2022, Antti Hyvarinen +* Copyright (c) 2022-2023, Martin Blicha +* +* SPDX-License-Identifier: MIT +* +*/ #ifndef TSEITIN_H #define TSEITIN_H @@ -33,34 +16,21 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. class Tseitin : public Cnfizer { public: - - Tseitin( SMTConfig& config_ - , Logic& logic_ - , PartitionManager &pmanager_ - , TermMapper& tmap_ - , SimpSMTSolver& solver_ - ) - : Cnfizer( config_ - , logic_ - , pmanager_ - , tmap_ - , solver_ ) - , alreadyCnfized(logic_.getTerm_true()) - {} + Tseitin(Logic & logic, TermMapper & tmap) + : Cnfizer(logic, tmap) {} private: // Cache of already cnfized terms. Note that this is different from Cnfizer cache of already processed top-level flas Cache alreadyCnfized; - bool cnfize (PTRef); // Cnfize the given term - bool cnfizeAnd (PTRef); // Cnfize conjunctions - bool cnfizeOr (PTRef); // Cnfize disjunctions - bool cnfizeIff (PTRef); // Cnfize iffs - bool cnfizeXor (PTRef); // Cnfize xors - bool cnfizeIfthenelse (PTRef); // Cnfize if then elses - bool cnfizeImplies (PTRef); // Cnfize if then elses -// void copyArgsWithCache(PTRef, vec&, Map&); + void cnfize(PTRef) override; // Cnfize the given term + void cnfizeAnd(PTRef); // Cnfize conjunctions + void cnfizeOr(PTRef); // Cnfize disjunctions + void cnfizeIff(PTRef); // Cnfize iffs + void cnfizeXor(PTRef); // Cnfize xors + void cnfizeIfthenelse(PTRef); // Cnfize if then elses + void cnfizeImplies(PTRef); // Cnfize implications }; #endif diff --git a/src/logics/ArrayTheory.cc b/src/logics/ArrayTheory.cc index 76afa5908..70cd56a55 100644 --- a/src/logics/ArrayTheory.cc +++ b/src/logics/ArrayTheory.cc @@ -8,18 +8,15 @@ #include "ArrayHelpers.h" #include "DistinctRewriter.h" -#include "TreeOps.h" - -bool ArrayTheory::simplify(vec const & formulas, PartitionManager &, int curr) -{ +PTRef ArrayTheory::simplifyTogether(const vec & assertions, bool) { // TODO: simplify select over store on the same index - auto & currentFrame = pfstore[formulas[curr]]; - if (this->keepPartitions()) { - std::logic_error("Not suppported yet"); - } - PTRef rewritten = rewriteDistincts(getLogic(), getCollateFunction(formulas, curr)); - rewritten = instantiateReadOverStore(getLogic(), rewritten); - currentFrame.root = rewritten; - return true; + 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"); } diff --git a/src/logics/ArrayTheory.h b/src/logics/ArrayTheory.h index 016a704f1..e2450c0ee 100644 --- a/src/logics/ArrayTheory.h +++ b/src/logics/ArrayTheory.h @@ -25,7 +25,9 @@ class ArrayTheory : public Theory { virtual const Logic& getLogic() const override { return logic; } virtual ArrayTHandler& getTSolverHandler() override { return tshandler; } virtual const ArrayTHandler& getTSolverHandler() const { return tshandler; } - virtual bool simplify(vec const &, PartitionManager &, int) override; + + virtual PTRef simplifyTogether(vec const & assertions, bool) override; + virtual vec simplifyIndividually(vec const & assertions, PartitionManager & pmanager, bool) override; }; diff --git a/src/logics/LATheory.h b/src/logics/LATheory.h index c961c55f7..9bd8740dd 100644 --- a/src/logics/LATheory.h +++ b/src/logics/LATheory.h @@ -1,6 +1,10 @@ -// -// Created by Antti on 10.03.21. -// +/* +* Copyright (c) 2021-2022, Antti Hyvarinen +* Copyright (c) 2023, Martin Blicha +* +* SPDX-License-Identifier: MIT +* +*/ #ifndef OPENSMT_LATHEORY_H #define OPENSMT_LATHEORY_H @@ -24,7 +28,9 @@ class LATheory : public Theory virtual LinAlgLogic& getLogic() override { return lalogic; } virtual const LinAlgLogic& getLogic() const override { return lalogic; } virtual LinAlgTHandler& getTSolverHandler() override { return latshandler; } - virtual bool simplify(const vec&, PartitionManager& pmanager, int) override; // Theory specific simplifications + + virtual PTRef simplifyTogether(vec const & assertions, bool isBaseFrame) override; + virtual vec simplifyIndividually(vec const & assertions, PartitionManager & pmanager, bool isBaseFrame) override; }; namespace { @@ -40,34 +46,33 @@ PTRef rewriteDivMod(ArithLogic & logic, PTRef fla) { } -// -// Unit propagate with simplifications and split equalities into -// inequalities. If partitions cannot mix, only do the splitting to -// inequalities. -// + template -bool LATheory::simplify(const vec& formulas, PartitionManager& pmanager, int curr) -{ - auto & currentFrame = pfstore[formulas[curr]]; +PTRef LATheory::simplifyTogether(const vec & assertions, bool) { + PTRef frameFormula = getLogic().mkAnd(assertions); + frameFormula = applySubstitutionBasedSimplificationIfEnabled(frameFormula); + frameFormula = rewriteDistincts(getLogic(), frameFormula); + frameFormula = rewriteDivMod(lalogic, frameFormula); ArithmeticEqualityRewriter equalityRewriter(lalogic); - if (this->keepPartitions()) { - vec & flas = currentFrame.formulas; - for (PTRef & fla : flas) { - PTRef old = fla; - fla = rewriteDistincts(getLogic(), fla); - fla = rewriteDivMod(lalogic, fla); - fla = equalityRewriter.rewrite(fla); - pmanager.transferPartitionMembership(old, fla); - } - currentFrame.root = getLogic().mkAnd(flas); - } else { - PTRef coll_f = getCollateFunction(formulas, curr); - PTRef finalFla = applySubstitutionBasedSimplificationIfEnabled(coll_f); - finalFla = rewriteDistincts(getLogic(), finalFla); - finalFla = rewriteDivMod(lalogic, finalFla); - currentFrame.root = equalityRewriter.rewrite(finalFla); + frameFormula = equalityRewriter.rewrite(frameFormula); + return frameFormula; +} + +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 true; + return rewrittenAssertions; + } + #endif //OPENSMT_LATHEORY_H diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index dd018b8d5..7c3db4042 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -210,8 +210,6 @@ bool Logic::isTheoryTerm(PTRef ptr) const { } bool Logic::isTheorySymbol(SymRef tr) const { - // True and False are special cases, we count them as theory symbols - if (tr == sym_TRUE || tr == sym_FALSE) return true; const Symbol& t = sym_store[tr]; // Boolean var if (t.rsort() == sort_BOOL && t.nargs() == 0) return false; @@ -1451,8 +1449,6 @@ Logic::collectStats(PTRef root, int& n_of_conn, int& n_of_eq, int& n_of_uf, int& } -PTRef Logic::conjoinExtras(PTRef root) { return root; } - // Fetching sorts SRef Logic::getSortRef (const PTRef tr) const { return getSortRef(getPterm(tr).symb()); } SRef Logic::getSortRef (const SymRef sr) const { return getSym(sr).rsort(); } diff --git a/src/logics/Logic.h b/src/logics/Logic.h index 080341554..f3f1d18a7 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -133,8 +133,6 @@ class Logic { Logic (Logic&&) = default; Logic& operator =(Logic&&) = delete; - virtual PTRef conjoinExtras(PTRef root); - virtual std::string const getName() const { return opensmt::QFLogicToProperties.at(logicType).name; } opensmt::Logic_t getLogic() const { return logicType; } diff --git a/src/logics/Theory.cc b/src/logics/Theory.cc index 95b6c0f44..144bbad36 100644 --- a/src/logics/Theory.cc +++ b/src/logics/Theory.cc @@ -1,36 +1,7 @@ #include "Theory.h" #include "Substitutor.h" -//#include "MainSolver.h" -//#include "logics/Logic.h" -// The Collate function is constructed from all frames up to the current -// one and will be used to simplify the formulas in the current frame -// formulas[curr]. -// (1) Construct the collate function as a conjunction of formulas up to curr. -// (2) From the coll function compute units_{curr} -// (3) Use units_1 /\ ... /\ units_{curr} to simplify formulas[curr] -// -// In addition we add the transitivie equalities as a further -// simplification (critical for the eq_diamond instances in QF_UF of -// smtlib). -// -PTRef Theory::getCollateFunction(const vec & formulas, int curr) -{ - assert(curr < formulas.size()); - // XXX -// getLogic().dumpHeaderToFile(std::cout); -// getLogic().dumpFormulaToFile(std::cout, pfstore[formulas[1]].formulas[0]); - vec coll_f_args; - // compute coll_f as (a_1^0 /\ ... /\ a_{n_1}^0) /\ ... /\ (a_1^{curr} /\ ... /\ a_{n_k}^{curr}) - for (int i = 0; i <= curr; i++) - { - for (int j = 0; j < pfstore[formulas[i]].size(); j++) - coll_f_args.push(pfstore[formulas[i]][j]); - } - return getLogic().mkAnd(std::move(coll_f_args)); -} - Theory::SubstitutionResult Theory::computeSubstitutions(const PTRef fla) { SubstitutionResult result; @@ -78,34 +49,11 @@ Theory::SubstitutionResult Theory::computeSubstitutions(const PTRef fla) root = new_root; if (!cont) break; } -#ifdef SIMPLIFY_DEBUG - cerr << "Number of substitutions: " << allsubsts.elems() << endl; - vec::Pair> subst_vec; - allsubsts.getKeysAndVals(subst_vec); - printf("Substitutions:\n"); - for (int i = 0; i < subst_vec.size(); i++) { - PTRef source = subst_vec[i].key; - PTRef target = subst_vec[i].data.tr; - lbool sgn = subst_vec[i].data.sgn; - printf(" %s -> %s (%s)\n", getLogic().printTerm(source), getLogic().printTerm(target), sgn == l_True ? "enabled" : "disabled"); - } -#endif result.result = root; result.usedSubstitution = std::move(allsubsts); return result; } -void -Theory::printFramesAsQuery(const vec & frames, std::ostream & s) const -{ - getLogic().dumpHeaderToFile(s); - for (int i = 0; i < frames.size(); i++) { - if (i > 0) - s << "(push 1)\n"; - getLogic().dumpFormulaToFile(s, pfstore[frames[i]].root); - } - getLogic().dumpChecksatToFile(s); -} PTRef Theory::flaFromSubstitutionResult(const Theory::SubstitutionResult & sr) { Logic & logic = getLogic(); diff --git a/src/logics/Theory.h b/src/logics/Theory.h index 5bede3f29..f2432466a 100644 --- a/src/logics/Theory.h +++ b/src/logics/Theory.h @@ -36,111 +36,6 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include "PartitionManager.h" -// Simplification in frames: -// A frame F_i consists of: -// P_i : a list of asserts given on this frame -// U_i : the unit clauses, or facts, implied by P_1 /\ ... /\ P_i -// R_i : P_i simplified with U_1, ..., U_i -// -// We require that U_i \cap U_j = \emptyset -// if U_1 /\ ... /\ U_i is unsatisfiable, then R_i must be false -// R_i must not be simplified with any U_j such that j > i. -// -// Some of the U_i might be theory equalities. These allow potentially -// more simplifications. For instance in arithmetics if (= a b) \in U_j, -// a may be substituted everywhere in U_k, j <= k <= i. These must be -// simplified using a theory specific simplifier. This will be part of -// the simplifications we do. -// -// The simplification has to use information from the theory solver and -// propositional structure to accomplish this. The unit clauses need to -// be derived in a closure. For the closure we need the problem P_i -// separately as input to computeSubstitutions. Hence the interface -// will be as follows: -// - units U_1 ... U_{curr-1} -// - conjunction of simplified problems R_i ... R_{curr-1} -// - The problem to be simplified P_{curr} -// - The last frame where the simplified problem R_{curr} and the new -// unit clauses U_{curr} will be placed -// -class PushFrameAllocator; - -struct FrameId -{ - uint32_t id; - bool operator== (const FrameId other) const { return id == other.id; } - bool operator!= (const FrameId other) const { return id != other.id; } -}; - -static struct FrameId FrameId_Undef = { INT32_MAX }; -static struct FrameId FrameId_bottom = { 0 }; - -struct PushFrame -{ - friend PushFrameAllocator; -private: - FrameId id; -public: - FrameId getId() const { return id; } - int size() const { return formulas.size(); } - void push(PTRef tr) { formulas.push(tr); } - PTRef operator[] (int i) const { return formulas[i]; } - PTRef root; - vec formulas; - bool unsat; // If true than the stack of frames with this frame at top is UNSAT - PushFrame(PushFrame& pf); - PushFrame() : id(FrameId_Undef), root(PTRef_Undef) {} // For pushing into vecs we need a default. - PushFrame operator= (PushFrame& other); - private: - PushFrame(uint32_t id) : id({id}), root(PTRef_Undef), unsat(false) {} -}; - -struct PFRef { - uint32_t x; - inline friend bool operator== (const PFRef& a1, const PFRef& a2) { return a1.x == a2.x; }; -}; - -static const struct PFRef PFRef_Undef = {INT32_MAX}; - -// No global variable for storing the push frame id. I decided to -// implement this as my own memory allocation. There's no free though -// at the moment, the implementation is very minimalistic. -class PushFrameAllocator : public RegionAllocator -{ -private: - int id_counter; - std::vector allocatedFrames; -public: - PushFrameAllocator() : id_counter(FrameId_bottom.id) {} - PushFrameAllocator(uint32_t init_capacity) : RegionAllocator(init_capacity), id_counter(FrameId_bottom.id) {} - - ~PushFrameAllocator() { - for (PFRef ref : allocatedFrames) { - lea(ref)->PushFrame::~PushFrame(); - } - } - - void moveTo(PushFrameAllocator& to) { - to.id_counter = id_counter; - RegionAllocator::moveTo(to); - to.allocatedFrames = std::move(allocatedFrames); - } - PFRef alloc() - { - uint32_t v = RegionAllocator::alloc(sizeof(PushFrame)/sizeof(uint32_t)); - PFRef r = {v}; - new (lea(r)) PushFrame(id_counter++); - allocatedFrames.push_back(r); - return r; - } - PushFrame& operator[](PFRef r) { return (PushFrame&)RegionAllocator::operator[](r.x); } - const PushFrame& operator[](PFRef r) const { return (PushFrame&)RegionAllocator::operator[](r.x); } - PushFrame* lea (PFRef r) { return (PushFrame*)RegionAllocator::lea(r.x); } - PFRef ael (const PushFrame* t) { RegionAllocator::Ref r = RegionAllocator::ael((uint32_t*)t); return { r }; } - -}; - - class Theory { protected: @@ -149,9 +44,8 @@ class Theory PTRef result; }; + SMTConfig & config; - SMTConfig & config; - PTRef getCollateFunction(const vec & formulas, int curr); Theory(SMTConfig &c) : config(c) { } inline bool keepPartitions() const { return config.produce_inter(); } @@ -163,13 +57,14 @@ class Theory PTRef applySubstitutionBasedSimplificationIfEnabled(PTRef); public: - PushFrameAllocator pfstore {1024}; virtual Logic &getLogic() = 0; virtual const Logic &getLogic() const = 0; virtual TSolverHandler &getTSolverHandler() = 0; - virtual bool simplify(const vec&, PartitionManager& pmanager, int) = 0; // Simplify a vector of PushFrames in an incrementality-aware manner + + virtual PTRef simplifyTogether(vec const & assertions, bool isBaseFrame) = 0; + virtual vec simplifyIndividually(vec const & assertions, PartitionManager & pmanager, bool isBaseFrame) = 0; + SubstitutionResult computeSubstitutions(PTRef fla); - void printFramesAsQuery(const vec & frames, std::ostream & s) const; virtual ~Theory() = default; }; @@ -188,7 +83,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 bool simplify(const vec&, PartitionManager& pmanager, int) override; + virtual PTRef simplifyTogether(vec const & assertions, bool isBaseFrame) override; + virtual vec simplifyIndividually(vec const & assertions, PartitionManager & pmanager, bool isBaseFrame) override; }; #endif diff --git a/src/logics/UFLATheory.cc b/src/logics/UFLATheory.cc index d17829b48..5fd914c8f 100644 --- a/src/logics/UFLATheory.cc +++ b/src/logics/UFLATheory.cc @@ -8,25 +8,22 @@ #include "Substitutor.h" #include "TreeOps.h" -bool UFLATheory::simplify(const vec& formulas, PartitionManager &, int curr) -{ - auto & currentFrame = pfstore[formulas[curr]]; - if (this->keepPartitions()) { - throw OsmtInternalException("Mode not supported for QF_UFLRA yet"); - } else { - PTRef coll_f = getCollateFunction(formulas, curr); - PTRef fla = applySubstitutionBasedSimplificationIfEnabled(coll_f); - fla = rewriteDistincts(getLogic(), fla); - fla = rewriteDivMod(logic, fla); - PTRef purified = purify(fla); - if (logic.hasArrays()) { - purified = instantiateReadOverStore(logic, purified); - } - PTRef noArithmeticEqualities = splitArithmeticEqualities(purified); - this->getTSolverHandler().setInterfaceVars(getInterfaceVars(noArithmeticEqualities)); - currentFrame.root = noArithmeticEqualities; +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); + if (logic.hasArrays()) { + purified = instantiateReadOverStore(logic, purified); } - return true; + PTRef noArithmeticEqualities = splitArithmeticEqualities(purified); + this->getTSolverHandler().setInterfaceVars(getInterfaceVars(noArithmeticEqualities)); + return noArithmeticEqualities; +} + +vec UFLATheory::simplifyIndividually(vec const &, PartitionManager &, bool) { + throw OsmtInternalException("Mode not supported for QF_UFLRA yet"); } namespace { diff --git a/src/logics/UFLATheory.h b/src/logics/UFLATheory.h index f3b78076d..b8229e154 100644 --- a/src/logics/UFLATheory.h +++ b/src/logics/UFLATheory.h @@ -44,7 +44,9 @@ class UFLATheory : public Theory virtual ArithLogic& getLogic() override { return logic; } virtual const ArithLogic& getLogic() const override { return logic; } virtual UFLATHandler& getTSolverHandler() override { return uflatshandler; } - virtual bool simplify(const vec&, PartitionManager&, int) override; + + virtual PTRef simplifyTogether(vec const & assertions, bool isBaseFrame) override; + virtual vec simplifyIndividually(vec const & assertions, PartitionManager & pmanager, bool isBaseFrame) override; protected: PTRef purify(PTRef fla); diff --git a/src/logics/UFTheory.cc b/src/logics/UFTheory.cc index 6cb3a4e47..ee96c5fb3 100644 --- a/src/logics/UFTheory.cc +++ b/src/logics/UFTheory.cc @@ -1,26 +1,28 @@ #include "Theory.h" #include "TreeOps.h" #include "DistinctRewriter.h" -// -// Simplify with unit propagation, add the diamond equalities if -// present. If partitions cannot mix, do no simplifications but just -// update the root. -// -bool UFTheory::simplify(const vec& formulas, PartitionManager &, int curr) + +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; +} + +vec UFTheory::simplifyIndividually(vec const& formulas, PartitionManager &, bool isBaseFrame) { - auto & currentFrame = pfstore[formulas[curr]]; - if (this->keepPartitions()) { - currentFrame.root = getLogic().mkAnd(currentFrame.formulas); - } - else { - PTRef coll_f = getCollateFunction(formulas, curr); - PTRef trans = getLogic().learnEqTransitivity(coll_f); - coll_f = getLogic().mkAnd(coll_f, trans); - currentFrame.root = applySubstitutionBasedSimplificationIfEnabled(coll_f); + vec rewrittenFormulas; + formulas.copyTo(rewrittenFormulas); + AppearsInUfVisitor visitor(getLogic()); + + for (PTRef & fla : rewrittenFormulas) { + fla = isBaseFrame ? rewriteDistinctsKeepTopLevel(getLogic(), fla) : rewriteDistincts(getLogic(), fla); + visitor.visit(fla); } - currentFrame.root = curr == 0 ? rewriteDistinctsKeepTopLevel(getLogic(), currentFrame.root) - : rewriteDistincts(getLogic(), currentFrame.root); - AppearsInUfVisitor(getLogic()).visit(currentFrame.root); - return true; + return rewrittenFormulas; } diff --git a/src/parallel/MainSplitter.cc b/src/parallel/MainSplitter.cc index 52554699d..ae1ba1796 100644 --- a/src/parallel/MainSplitter.cc +++ b/src/parallel/MainSplitter.cc @@ -19,7 +19,7 @@ void MainSplitter::notifyResult(sstat const & result) sstat MainSplitter::check() { if (getChannel().isSolverInParallelMode() and not config.sat_solver_limit()) { //push frames size should match with length of the solver branch - if (frames.size() != + if (frames.frameCount() != static_cast(getSplitter().getSolverBranch().size() + 1)) throw PTPLib::common::Exception(__FILE__, __LINE__, ";assert: Inconsistency in push frames size and length of the solver address"); @@ -30,7 +30,7 @@ sstat MainSplitter::check() { return res; } -sstat MainSplitter::solve_(vec & enabledFrames) { +sstat MainSplitter::solve_(vec const & enabledFrames) { if (getChannel().isSolverInParallelMode() and not config.sat_solver_limit()) { vec> const & solverBranch = getSplitter().getSolverBranch(); if (enabledFrames.size() > solverBranch.size() + 1) { @@ -121,7 +121,7 @@ bool MainSplitter::verifyPartitions(vec const & partitions) const { ok = false; } else { // Removing the models of the partial partitions from the root instance must yield unsat - if (not verifier.impliesInternal(logic.mkAnd(partitionCoverageQuery), logic.mkNot(root_instance.getRoot()))) { + if (not verifier.impliesInternal(logic.mkAnd(partitionCoverageQuery), logic.mkNot(currentRootInstance()))) { error += "[Non-covering partial partitioning: partial partitions do not contain all models of original instance] "; ok = false; } diff --git a/src/parallel/MainSplitter.h b/src/parallel/MainSplitter.h index c583bb983..e32a6394b 100644 --- a/src/parallel/MainSplitter.h +++ b/src/parallel/MainSplitter.h @@ -20,21 +20,21 @@ class MainSplitter : public MainSolver { private: - inline bool isSplitTypeScatter() const & { return dynamic_cast(ts.solver).isSplitTypeScatter(); } + inline bool isSplitTypeScatter() const & { return dynamic_cast(*smt_solver).isSplitTypeScatter(); } - inline bool isSplitTypeNone() const & { return dynamic_cast(ts.solver).isSplitTypeNone(); } + inline bool isSplitTypeNone() const & { return dynamic_cast(*smt_solver).isSplitTypeNone(); } inline PTPLib::net::Channel & getChannel() const { return getSplitter().getChannel(); } inline ScatterSplitter & getScatterSplitter() { return dynamic_cast(getSMTSolver()); } - inline Splitter & getSplitter() const { return dynamic_cast(ts.solver); } + inline Splitter & getSplitter() const { return dynamic_cast(*smt_solver); } void notifyResult(sstat const & result); vec addToConjunction(std::vector> const &) const; - sstat solve_(vec & enabledFrames) override; + sstat solve_(vec const & enabledFrames) override; sstat check() override; diff --git a/src/parallel/ScatterSplitter.cc b/src/parallel/ScatterSplitter.cc index fb13fe5f4..c2117d152 100644 --- a/src/parallel/ScatterSplitter.cc +++ b/src/parallel/ScatterSplitter.cc @@ -116,13 +116,13 @@ opensmt::pair ScatterSplitter::createSplitAndBlockAssumptions() } cancelUntil(0); - lbool res = excludeAssumptions(constraints_negated) ? l_Undef : l_False; + lbool res = excludeAssumptions(std::move(constraints_negated)) ? l_Undef : l_False; return {std::move(splitData), res}; } -bool ScatterSplitter::excludeAssumptions(vec const & neg_constrs) { - addOriginalClause(neg_constrs); +bool ScatterSplitter::excludeAssumptions(vec && neg_constrs) { + addOriginalClause(std::move(neg_constrs)); simplify(); return ok; } diff --git a/src/parallel/ScatterSplitter.h b/src/parallel/ScatterSplitter.h index cce08269b..5b39d3644 100644 --- a/src/parallel/ScatterSplitter.h +++ b/src/parallel/ScatterSplitter.h @@ -56,7 +56,7 @@ class ScatterSplitter : public SimpSMTSolver, public Splitter { protected: bool scatterLevel(); // Are we currently on a scatter level. opensmt::pair createSplitAndBlockAssumptions(); // Create a split formula and place it to the splits vector. - bool excludeAssumptions(vec const & neg_constrs); // Add a clause to the database and propagate + bool excludeAssumptions(vec && neg_constrs); // Add a clause to the database and propagate bool isAssumptionVar(Var v) const { return assumptionVars.find(v) != assumptionVars.end(); } lbool solve_() override; diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc index 8a48abca5..932565406 100644 --- a/src/smtsolvers/CoreSMTSolver.cc +++ b/src/smtsolvers/CoreSMTSolver.cc @@ -230,20 +230,18 @@ Var CoreSMTSolver::newVar(bool dvar) } -bool CoreSMTSolver::addOriginalClause_(const vec & _ps) +bool CoreSMTSolver::addOriginalClause_(vec && _ps) { opensmt::pair fake; - return addOriginalClause_(_ps, fake); + return addOriginalClause_(std::move(_ps), fake); } -bool CoreSMTSolver::addOriginalClause_(const vec & _ps, opensmt::pair & inOutCRefs) +bool CoreSMTSolver::addOriginalClause_(vec && ps, opensmt::pair & inOutCRefs) { assert(decisionLevel() == 0); inOutCRefs = {CRef_Undef, CRef_Undef}; if (!isOK()) { return false; } bool logsProofForInterpolation = this->logsProofForInterpolation(); - vec ps; - _ps.copyTo(ps); // Check if clause is satisfied and remove false/duplicate literals: sort(ps); std::vector resolvedUnits; diff --git a/src/smtsolvers/CoreSMTSolver.h b/src/smtsolvers/CoreSMTSolver.h index d82505b13..bb0d6ce94 100644 --- a/src/smtsolvers/CoreSMTSolver.h +++ b/src/smtsolvers/CoreSMTSolver.h @@ -106,21 +106,19 @@ class CoreSMTSolver virtual Var newVar(bool dvar); // Add a new variable with parameters specifying variable mode. public: void addVar(Var v); // Anounce the existence of a variable to the solver - bool addOriginalClause(const vec & ps); - bool addEmptyClause(); // Add the empty clause, making the solver contradictory. + bool addOriginalClause(vec && ps); bool addOriginalClause(Lit p); // Add a unit clause to the solver. bool addOriginalClause(Lit p, Lit q); // Add a binary clause to the solver. bool addOriginalClause(Lit p, Lit q, Lit r); // Add a ternary clause to the solver. protected: - bool addOriginalClause_(const vec & _ps); // Add a clause to the solver - bool addOriginalClause_(const vec & _ps, opensmt::pair & inOutCRefs); // Add a clause to the solver without making superflous internal copy. Will change the passed vector 'ps'. Write the new clause to cr + bool addOriginalClause_(vec && _ps); // Add a clause to the solver + bool addOriginalClause_(vec && _ps, opensmt::pair & inOutCRefs); // Add a clause to the solver and return the references for the added class before and after simplification public: // Solving: // bool simplify (); // Removes already satisfied clauses. void declareVarsToTheories(); // Declare the seen variables to the theories bool solve ( const vec< Lit > & assumps ); // Search for a model that respects a given set of assumptions. - void crashTest (int, Var, Var); // Stress test the theory solver void toDimacs (FILE* f, const vec& assumps); // Write CNF to file in DIMACS-format. void toDimacs (const char *file, const vec& assumps); @@ -350,7 +348,6 @@ class CoreSMTSolver vec seen; vec analyze_stack; vec analyze_toclear; - vec add_tmp; double max_learnts; double learntsize_adjust_confl; @@ -651,35 +648,22 @@ inline bool CoreSMTSolver::enqueue (Lit p, CRef from) return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } -inline bool CoreSMTSolver::addOriginalClause(const vec & ps) +inline bool CoreSMTSolver::addOriginalClause(vec && ps) { - return addOriginalClause_(ps); + return addOriginalClause_(std::move(ps)); } -inline bool CoreSMTSolver::addEmptyClause () -{ - add_tmp.clear(); - return addOriginalClause_(add_tmp); -} -inline bool CoreSMTSolver::addOriginalClause(Lit p) + +inline bool CoreSMTSolver::addOriginalClause(Lit p) { - add_tmp.clear(); - add_tmp.push(p); - return addOriginalClause_(add_tmp); + return addOriginalClause_({p}); } -inline bool CoreSMTSolver::addOriginalClause(Lit p, Lit q) +inline bool CoreSMTSolver::addOriginalClause(Lit p, Lit q) { - add_tmp.clear(); - add_tmp.push(p); - add_tmp.push(q); - return addOriginalClause_(add_tmp); + return addOriginalClause_({p,q}); } inline bool CoreSMTSolver::addOriginalClause(Lit p, Lit q, Lit r) { - add_tmp.clear(); - add_tmp.push(p); - add_tmp.push(q); - add_tmp.push(r); - return addOriginalClause_(add_tmp); + return addOriginalClause_({p,q,r}); } diff --git a/src/smtsolvers/SimpSMTSolver.cc b/src/smtsolvers/SimpSMTSolver.cc index 1cb97c862..d3a972c4c 100644 --- a/src/smtsolvers/SimpSMTSolver.cc +++ b/src/smtsolvers/SimpSMTSolver.cc @@ -180,7 +180,7 @@ lbool SimpSMTSolver::solve_(bool do_simp, bool turn_off_simp) //================================================================================================= // Added code -bool SimpSMTSolver::addOriginalSMTClause(const vec & smt_clause, opensmt::pair & inOutCRefs) +bool SimpSMTSolver::addOriginalSMTClause(vec && smt_clause, opensmt::pair & inOutCRefs) { inOutCRefs = {CRef_Undef, CRef_Undef}; assert( config.sat_preprocess_theory == 0 ); @@ -208,7 +208,7 @@ bool SimpSMTSolver::addOriginalSMTClause(const vec & smt_clause, opensmt::p std::cerr << "XXX skipped handling of unary theory literal?" << '\n'; } int nclauses = clauses.size(); - if (!CoreSMTSolver::addOriginalClause_(smt_clause, inOutCRefs)) + if (!CoreSMTSolver::addOriginalClause_(std::move(smt_clause), inOutCRefs)) return false; if (use_simplification && clauses.size() == nclauses + 1) @@ -614,11 +614,11 @@ bool SimpSMTSolver::eliminateVar(Var v) removeClause(cls[i]); // Produce clauses in cross product: - vec& resolvent = add_tmp; for (int i = 0; i < pos.size(); i++) { for (int j = 0; j < neg.size(); j++) { + vec resolvent; opensmt::pair dummy {CRef_Undef, CRef_Undef}; - if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addOriginalSMTClause(resolvent, dummy)) + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addOriginalSMTClause(std::move(resolvent), dummy)) return false; } } @@ -646,12 +646,11 @@ bool SimpSMTSolver::substitute(Var v, Lit x) setDecisionVar(v, false); const vec& cls = occurs.lookup(v); - vec& subst_clause = add_tmp; for (int i = 0; i < cls.size(); i++) { Clause& c = ca[cls[i]]; - subst_clause.clear(); + vec subst_clause; for (unsigned j = 0; j < c.size(); j++) { Lit p = c[j]; @@ -661,7 +660,7 @@ bool SimpSMTSolver::substitute(Var v, Lit x) removeClause(cls[i]); opensmt::pair dummy {CRef_Undef, CRef_Undef}; - if (!addOriginalSMTClause(subst_clause, dummy)) + if (!addOriginalSMTClause(std::move(subst_clause), dummy)) return ok = false; } diff --git a/src/smtsolvers/SimpSMTSolver.h b/src/smtsolvers/SimpSMTSolver.h index 7ecab5041..51563bccc 100644 --- a/src/smtsolvers/SimpSMTSolver.h +++ b/src/smtsolvers/SimpSMTSolver.h @@ -62,7 +62,7 @@ class SimpSMTSolver : public CoreSMTSolver // Var newVar (bool dvar = true) override; - bool addOriginalSMTClause(const vec & smt_clause, opensmt::pair & inOutCRefs); + bool addOriginalSMTClause(vec && smt_clause, opensmt::pair & inOutCRefs); public: bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). diff --git a/src/smtsolvers/TheoryIF.cc b/src/smtsolvers/TheoryIF.cc index c3ba42305..d3588b64c 100644 --- a/src/smtsolvers/TheoryIF.cc +++ b/src/smtsolvers/TheoryIF.cc @@ -31,53 +31,6 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include #include -// Stress test the theory solver -void CoreSMTSolver::crashTest(int rounds, Var var_true, Var var_false) -{ - srand(0); - for (int i = 1; i < nVars(); i++) - { - int stack_sz = 0; - vec tmp_trail; // <- add literals here - for (int j = 0; j < rounds; j++) - { - // clause lengths - for (int k = stack_sz; k < i; k++) - { - Var v = rand() % nVars(); - if (v == var_true) - { - tmp_trail.push(mkLit(v, false)); - } - else if (v == var_false) - { - tmp_trail.push(mkLit(v, true)); - } - else - { - tmp_trail.push(mkLit(v, rand() % 2)); - } - } - printf("Stack contains %d literals of which %d new\n", tmp_trail.size(), tmp_trail.size()-stack_sz); - stack_sz = tmp_trail.size_(); - bool res = theory_handler.assertLits(tmp_trail); - int new_stack_sz; - if (res == false) - { - printf("Conflict\n"); - new_stack_sz = 0; - } - else - new_stack_sz = rand() % (i+1); - - theory_handler.backtrack(new_stack_sz); - tmp_trail.shrink(stack_sz - new_stack_sz); - stack_sz = new_stack_sz; - assert(tmp_trail.size() == stack_sz); - } - } -} - namespace { std::vector sortByLastAssignedLevel(std::vector> & splitClauses, std::function getVarLevel) { if (splitClauses.size() == 1) { diff --git a/src/tsolvers/bvsolver/BitBlaster.cc b/src/tsolvers/bvsolver/BitBlaster.cc index 9fcd0dcb2..bcb7badff 100644 --- a/src/tsolvers/bvsolver/BitBlaster.cc +++ b/src/tsolvers/bvsolver/BitBlaster.cc @@ -142,7 +142,7 @@ BitBlaster::assertLit (PtAsgn pta) // vec< Lit > clause; clause.push( mkLit( act_var, (pta.sgn == l_True ? false : true) ) ); - bool res = addClause(clause); + bool res = addClause(std::move(clause)); return res; } @@ -1449,9 +1449,9 @@ BitBlaster::bbDistinct(PTRef tr) } bool -BitBlaster::addClause(vec & c) +BitBlaster::addClause(vec && c) { - return solverP.addOriginalClause(c); + return solverP.addOriginalClause(std::move(c)); } //============================================================================= diff --git a/src/tsolvers/bvsolver/BitBlaster.h b/src/tsolvers/bvsolver/BitBlaster.h index c111962b8..ff098e019 100644 --- a/src/tsolvers/bvsolver/BitBlaster.h +++ b/src/tsolvers/bvsolver/BitBlaster.h @@ -80,7 +80,7 @@ class BitBlaster THandler& thandler; SimpSMTSolver& solverP; // Solver with proof logger - bool addClause(vec & c); + bool addClause(vec && c); static const char* s_bbEq; static const char* s_bbAnd;