MainSolver: Small cleanup

usi-verification-and-security · Mar 4, 2024 · 533226b · 533226b
1 parent a5b37a4
commit 533226b
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 21 deletions.
diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc
@@ -279,12 +279,12 @@ sstat MainSolver::giveToSolver(PTRef root, FrameId push_id) {
     };
     ClauseCallBack callBack;
     ts.setClauseCallBack(&callBack);
-    ts.Cnfizer::cnfize(root, push_id.id);
+    ts.Cnfizer::cnfize(root, push_id);
     bool keepPartitionsSeparate = getConfig().produce_inter();
-    Lit frameLit = push_id.id == 0 ? Lit{} : term_mapper->getOrCreateLit(frameTerms[push_id.id]);
+    Lit frameLit = push_id == 0 ? Lit{} : term_mapper->getOrCreateLit(frameTerms[push_id]);
     int partitionIndex = keepPartitionsSeparate ? pmanager.getPartitionIndex(root) : -1;
     for (auto & clause : callBack.clauses) {
-        if (push_id.id != 0) {
+        if (push_id != 0) {
             clause.push(frameLit);
         }
         opensmt::pair<CRef, CRef> iorefs{CRef_Undef, CRef_Undef};
@@ -371,8 +371,8 @@ sstat MainSolver::solve_(vec<FrameId> const & enabledFrames) {
     // 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);
+        assumps[fid] = ~assumps[fid];
+        smt_solver->mapEnabledFrameIdToVar(var(assumps[fid]), fid, prevId);
     }
     // Drop the assumption variable for the base frame (it is at the first place)
     for (int i = 1; i < assumps.size(); ++i) {

diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h
@@ -49,18 +49,11 @@ const sstat s_Undef = toSstat( 0);
 const sstat s_Error = toSstat( 2);
 
 
-class MainSolver
-{
+class MainSolver {
 protected: /** Helper classes to deal with assertion stack, preprocessing and substitutions **/
-    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; }
-    };
+    using FrameId = uint32_t;
 
     struct PushFrame {
-
     private:
         FrameId id;
 
@@ -74,7 +67,7 @@ class MainSolver
 
         PushFrame(PushFrame const &) = delete;
         PushFrame(PushFrame &&) = default;
-        explicit PushFrame(uint32_t id) : id({id}), unsat(false) {}
+        explicit PushFrame(uint32_t id) : id(id), unsat(false) {}
     };
 
     class AssertionStack {
@@ -145,8 +138,8 @@ class MainSolver
     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);
+        assert(frameId != 0);
+        auto name = std::string(Logic::s_framev_prefix) + std::to_string(frameId);
         PTRef frameTerm = logic.mkBoolVar(name.c_str());
         Lit l = term_mapper->getOrCreateLit(frameTerm);
         term_mapper->setFrozen(var(l));
@@ -201,8 +194,6 @@ class MainSolver
 
     static std::unique_ptr<SimpSMTSolver> createInnerSolver(SMTConfig& config, THandler& thandler);
 
-
-  public:
     MainSolver(Logic& logic, SMTConfig& conf, std::string name);
 
     MainSolver(std::unique_ptr<Theory> th, std::unique_ptr<TermMapper> tm, std::unique_ptr<THandler> thd,

diff --git a/src/cnfizers/Cnfizer.h b/src/cnfizers/Cnfizer.h
@@ -50,7 +50,7 @@ class Cnfizer
         virtual void operator()(vec<Lit> &&) = 0;
     };
 protected:
-    using FrameId = uint32_t; // TODO: Unify this with FrameId of MainSolver
+    using FrameId = uint32_t;
 
     class Cache {
         using CacheEntry = std::pair<PTRef, FrameId>;

diff --git a/src/parallel/MainSplitter.cc b/src/parallel/MainSplitter.cc
@@ -41,7 +41,7 @@ sstat MainSplitter::solve_(vec<FrameId> const & enabledFrames) {
         }
         for (int i = 0; i < enabledFrames.size(); i++) {
             if (i > 0)
-                getSplitter().addBranchToFrameId(opensmt::span<opensmt::pair<int, int> const>(solverBranch.begin(), i), enabledFrames[i].id);
+                getSplitter().addBranchToFrameId(opensmt::span<opensmt::pair<int, int> const>(solverBranch.begin(), i), enabledFrames[i]);
         }
     }
     sstat res = MainSolver::solve_(enabledFrames);