Rec z3solver

src/main/scala/org/allenai/iqclid/api/TreeApi.scala

@@ -47,6 +47,7 @@ object Evaluator {
       case I() => index
       case T(i) =>
         if (index - i < 0) {
+          println("Wrong index of T(i): " + (index-i))
           throw new BadTreeException()
         }
         seqSoFar(index - i)
@@ -61,23 +62,30 @@ object Evaluator {
           case (Div(), Seq(el1, el2)) =>
             val denom = evaluateInternal(el2, seqSoFar, index)
             if (denom == 0) {
+              println("Unknown operation: " + Apply(op, args))
               throw new BadTreeException()
             } else {
               evaluateInternal(el1, seqSoFar, index) / evaluateInternal(el2, seqSoFar, index)
             }
           case (Mod(), Seq(el1, el2)) =>
             val denom = evaluateInternal(el2, seqSoFar, index)
             if (denom == 0) {
+              println("Unknown operation: " + Apply(op, args))
               throw new BadTreeException()
             } else {
               evaluateInternal(el1, seqSoFar, index) % evaluateInternal(el2, seqSoFar, index)
             }
           case (Pow(), Seq(el1, el2)) =>
             Math.pow(
               evaluateInternal(el1, seqSoFar, index), evaluateInternal(el2, seqSoFar, index)).toInt
-          case _ => throw new BadTreeException()
+          case _ => {
+            println("Unknown operation: " + Apply(op, args))
+            throw new BadTreeException()
+          }
         }
-      case _ => throw new BadTreeException()
+      case _ =>
+        println("Unknown tree: " + tree)
+        throw new BadTreeException()
     }
   }
 }

src/main/scala/org/allenai/iqclid/z3/SmtSolver.scala

@@ -0,0 +1,38 @@
+package org.allenai.iqclid.z3
+
+import org.allenai.iqclid.NumberSequence
+import org.allenai.iqclid.api._
+import org.allenai.iqclid.z3.ThreadSafeDependencies.Z3Module
+import org.allenai.iqclid.api.{Evaluator, Tree}
+
+class SmtSolver extends Solver {
+  override def solve(s: NumberSequence): Seq[Solution]= {
+    val seq = s.seq
+
+    val solutionSet = {
+      val sol = ThreadSafeDependencies.withZ3Module {
+        z3Module =>
+          new Z3Interface(z3Module, true).solveSequence(seq, 1)
+      }
+      if (!sol.isEmpty) {
+        sol
+      } else {
+        val sol2 = ThreadSafeDependencies.withZ3Module {
+          z3Module =>
+            new Z3Interface(z3Module, true).solveSequence(seq, 3)
+        }
+        if (!sol2.isEmpty) {
+          sol2
+        } else {
+          ThreadSafeDependencies.withZ3Module {
+            z3Module =>
+              new Z3Interface(z3Module, true).solveSequence(seq, 2)
+          }
+        }
+      }
+    }
+    println(solutionSet)
+    println(Evaluator.evaluate(solutionSet.head.tree, s.baseCases, s.seq.length + 1))
+    solutionSet
+  }
+}