Merge pull request #629 from vprover/test-additions

UnitTest additions
vprover · Dec 12, 2024 · 5dbcc50 · 5dbcc50
2 parents 5417943 + fa64d60
commit 5dbcc50
Show file tree

Hide file tree

Showing 16 changed files with 765 additions and 452 deletions.
diff --git a/Inferences/TheoryInstAndSimp.cpp b/Inferences/TheoryInstAndSimp.cpp
@@ -970,11 +970,6 @@ SimplifyingGeneratingInference::ClauseGenerationResult TheoryInstAndSimp::genera
 std::ostream& operator<<(std::ostream& out, Solution const& self) 
 { return out << "Solution(" << (self.sat ? "sat" : "unsat") << ", " << self.subst << ")"; }
 
-TheoryInstAndSimp::~TheoryInstAndSimp()
-{
-  delete _solver;
-}
-
 }
 
 #endif
diff --git a/Inferences/TheoryInstAndSimp.hpp b/Inferences/TheoryInstAndSimp.hpp
@@ -48,8 +48,8 @@ class TheoryInstAndSimp
 {
 public:
   using SortId = SAT::Z3Interfacing::SortId;
-  ~TheoryInstAndSimp();
   TheoryInstAndSimp() : TheoryInstAndSimp(*env.options) {}
+  TheoryInstAndSimp(TheoryInstAndSimp&&) = default;
 
   TheoryInstAndSimp(Options& opts);
   TheoryInstAndSimp(Options::TheoryInstSimp mode, bool thiTautologyDeletion, bool showZ3, bool generalisation, std::string const& exportSmtlib);
@@ -135,9 +135,7 @@ class TheoryInstAndSimp
   Options::TheoryInstSimp const _mode;
   bool const _thiTautologyDeletion;
   SAT2FO _naming;
-  volatile char padding00[1024];
-  Z3Interfacing* _solver;
-  volatile char padding01[1024];
+  std::unique_ptr<Z3Interfacing> _solver;
   Map<SortId, bool> _supportedSorts;
   bool _generalisation;
   ConstantCache _instantiationConstants;

diff --git a/Saturation/ClauseContainer.hpp b/Saturation/ClauseContainer.hpp
@@ -168,7 +168,7 @@ class ActiveClauseContainer
 : public RandomAccessClauseContainer
 {
 public:
-  ActiveClauseContainer(const Shell::Options& opt) {}
+  ActiveClauseContainer() {}
 
   void add(Clause* c) override;
   void remove(Clause* c) override;

diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp
@@ -233,7 +233,7 @@ SaturationAlgorithm::SaturationAlgorithm(Problem& prb, const Options& opt)
   else {
     _passive = makeLevel4(true, opt, "");
   }
-  _active = new ActiveClauseContainer(opt);
+  _active = new ActiveClauseContainer();
 
   _active->attach(this);
   _passive->attach(this);

diff --git a/Test/ClausePattern.hpp b/Test/ClausePattern.hpp
@@ -34,48 +34,49 @@ struct AnyOf
  * A Clause matches a pattern Clause, if they are equal.
  * A Clause matches an AnyOf pattern if it matches both of the subpatterns.
  */
-class ClausePattern : Coproduct<Kernel::Clause const*, AnyOf>
+class ClausePattern : Coproduct<Kernel::Clause*, AnyOf>
 {
+  using Copro =  Coproduct<Kernel::Clause*, AnyOf>;
 public:
-  ClausePattern(Kernel::Clause const* clause) 
-    : Coproduct<Kernel::Clause const*, AnyOf>(clause) {}
+  ClausePattern(Kernel::Clause* clause) 
+    : Copro(clause) {}
 
-  ClausePattern(ClausePattern l, ClausePattern r) : Coproduct<Kernel::Clause const*, AnyOf>(AnyOf {
+  ClausePattern(ClausePattern l, ClausePattern r) : Copro(AnyOf {
         std::make_unique<ClausePattern>(std::move(l)),
         std::make_unique<ClausePattern>(std::move(r))
       }) {}
 
   template<class EqualityOperator>
-  bool matches(EqualityOperator& equality, Kernel::Clause const* result);
+  bool matches(EqualityOperator& equality, Kernel::Clause* result);
   friend std::ostream& operator<<(std::ostream& out, ClausePattern const& self);
 };
 
 inline std::ostream& operator<<(std::ostream& out, ClausePattern const& self) 
 {
   return self.match(
-      [&](Kernel::Clause const* const& self) -> std::ostream&
+      [&](Kernel::Clause* const& self) -> std::ostream&
       { return out << pretty(self); },
 
       [&](AnyOf const& self)  -> std::ostream&
       { return out << pretty(self.lhs) << " or " << pretty(self.rhs); });
 }
 
 template<class EqualityOperator>
-bool ClausePattern::matches(EqualityOperator& equality, Kernel::Clause const* result)
+bool ClausePattern::matches(EqualityOperator& equality, Kernel::Clause* result)
 {
   return match(
-      [&](Kernel::Clause const*& self) 
+      [&](Kernel::Clause* self) 
       { return equality.eq(result, self); },
 
       [&](AnyOf& self) 
       { return self.lhs->matches(equality, result) || self.rhs->matches(equality, result); });
 }
 
-inline ClausePattern anyOf(Kernel::Clause const* lhs) 
+inline ClausePattern anyOf(Kernel::Clause* lhs) 
 { return ClausePattern(lhs); }
 
 template<class... As>
-inline ClausePattern anyOf(Kernel::Clause const* lhs, Kernel::Clause const* rhs, As... rest) 
+inline ClausePattern anyOf(Kernel::Clause* lhs, Kernel::Clause* rhs, As... rest) 
 { return ClausePattern(lhs, anyOf(rhs, rest...)); }