Move test filters to helpers file

Author: sankalpgambhir

src/it/scala/smtlib/it/TestHelpers.scala

@@ -12,6 +12,12 @@ import parser.Parser
 import lexer.Lexer
 import printer.RecursivePrinter
 import interpreters._
+import smtlib.trees.Commands.*
+import smtlib.trees.Terms.Term
+import smtlib.trees.Tree
+import smtlib.trees.TreesOps
+import smtlib.theories.FixedSizeBitVectors.BitVectorSort
+import smtlib.theories.FloatingPoint.FloatingPointSort
 
 /** Provide helper functions to test solver interfaces and files.
   *
@@ -91,5 +97,43 @@ trait TestHelpers {
     Seq("bitwuzla", "-v", "0", "--lang", "--smt2", file.getPath) ! ProcessLogger(f, s => ())
   }
 
+  ////////////////////////////////////////////////////////////////
+  // Solver specific helpers
+
+  /**
+  * Is test in the fragment supported by bitwuzla?
+  * 
+  * May not contain ints, reals, arrays, ADTs
+  *
+  */
+  def testIsBitwuzlaCompatible(cmds: Seq[Command], formula: Term): Boolean =
+    def isCompat(term: Term): Boolean =
+      def violatingTerm(term: Tree, children: Seq[Boolean]): Boolean = {
+        import smtlib.theories.*
+        term match
+          case FixedSizeBitVectors.BitVectorConstant(_, _) => false // internally contains IntNumeral, but in a valid place
+          case Ints.NumeralLit(_) => true
+          case Reals.DecimalLit(_) => true
+          case FixedSizeBitVectors.Int2BV(_, _) => true
+          case FixedSizeBitVectors.BV2Nat(_) => true
+          // this is enough to rule out the current problematic tests, 
+          // but may need refinement
+          case _ => children.contains(true)
+      }
+      !TreesOps.fold(violatingTerm)(term)
+    
+    def compatibleCommand(cmd: Command): Boolean =
+      cmd match
+        case DeclareFun(_, paramSorts, sort) => (sort +: paramSorts).forall {
+            case BitVectorSort(_) => true
+            case FloatingPointSort(_, _) => true
+            case _ => false
+        }
+        case DeclareSort(_, _) => false
+        case DeclareDatatypes(_) => false
+        case Assert(term) => isCompat(term)
+        case _ => true // may need refinement
+    cmds.forall(compatibleCommand) && (isCompat(formula))
+
 }
 

src/it/scala/smtlib/it/TheoriesBuilderTests.scala

@@ -5,11 +5,6 @@ import org.scalatest.funsuite.AnyFunSuite
 import smtlib.trees.Commands._
 import smtlib.trees.CommandsResponses._
 import smtlib.trees.Terms._
-import smtlib.theories.FloatingPoint.FloatingPointSort
-import smtlib.theories.FixedSizeBitVectors.BitVectorSort
-import smtlib.trees.TreesOps
-import smtlib.trees.Tree
-import smtlib.theories.FixedSizeBitVectors
 
 /** Checks that formula build with theories module are correctly handled by solvers */
 class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
@@ -62,43 +57,8 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
       ignore(cvc5Test) {}
     }
 
-    /**
-      * Is test in the fragment supported by bitwuzla?
-      * 
-      * May not contain ints, reals, arrays, ADTs
-      *
-      */
-    def testIsBitwuzlaCompatible: Boolean =
-      def isCompat(term: Term): Boolean =
-        def violatingTerm(term: Tree, children: Seq[Boolean]): Boolean = {
-          import smtlib.theories.*
-          term match
-            case FixedSizeBitVectors.BitVectorConstant(_, _) => false // internally contains IntNumeral, but in a valid place
-            case Ints.NumeralLit(_) => true
-            case Reals.DecimalLit(_) => true
-            case FixedSizeBitVectors.Int2BV(_, _) => true
-            case FixedSizeBitVectors.BV2Nat(_) => true
-            // this is enough to rule out the current problematic tests, 
-            // but may need refinement
-            case _ => children.contains(true)
-        }
-        !TreesOps.fold(violatingTerm)(term)
-      
-      def compatibleCommand(cmd: Command): Boolean =
-        cmd match
-          case DeclareFun(_, paramSorts, sort) => (sort +: paramSorts).forall {
-              case BitVectorSort(_) => true
-              case FloatingPointSort(_, _) => true
-              case _ => false
-          }
-          case DeclareSort(_, _) => false
-          case DeclareDatatypes(_) => false
-          case Assert(term) => isCompat(term)
-          case _ => true // may need refinement
-      cmds.forall(compatibleCommand) && (isCompat(formula))
-
     val bitwuzlaTest = prefix + ": with Bitwuzla"
-    if (isBitwuzlaAvailable && testIsBitwuzlaCompatible) {
+    if (isBitwuzlaAvailable && testIsBitwuzlaCompatible(cmds, formula)) {
       test(bitwuzlaTest) {
         runAndCheck(getBitwuzlaInterpreter)
       }