diff --git a/src/main/clojure/clj/bridge.clj b/src/main/clojure/clj/bridge.clj index edad7b6..6dd9b5b 100644 --- a/src/main/clojure/clj/bridge.clj +++ b/src/main/clojure/clj/bridge.clj @@ -44,7 +44,7 @@ ) (defn -search [n1 n2 box callable] - (println (str "Max generations: " (* n1 n2))) +;; (println (str "Max generations: " (* n1 n2))) (let [fitness (fn [tree] (.set box 0 (to-java tree)) (.call callable)) diff --git a/src/main/scala/org/allenai/iqclid/Demo.scala b/src/main/scala/org/allenai/iqclid/Demo.scala new file mode 100644 index 0000000..40bdf8c --- /dev/null +++ b/src/main/scala/org/allenai/iqclid/Demo.scala @@ -0,0 +1,23 @@ +package org.allenai.iqclid + +import org.allenai.iqclid.api.{AccuracyFirstFitness, Ensemble, Evaluator, MultipleRunSolver} + +object Demo { + + + def main(args: Array[String]): Unit = { + val fitness = new AccuracyFirstFitness(0.5) + val gpSolver = new MultipleRunSolver(new GPSolver(fitness), 10) + val smtSolver = new Z3Solver + val search = new BaselineSearch(0.01, 100, 30) + val ensemble = new Ensemble(Seq(gpSolver, smtSolver, search)) + + val numberSequence = new NumberSequence(Seq(7, 3, 84)) + + val tree = ensemble.solve(numberSequence).head.tree + println(tree) + println(Evaluator.evaluate(tree, numberSequence.baseCases(tree), 10)) + System.exit(0) + } + +} diff --git a/src/main/scala/org/allenai/iqclid/Evaluator.scala b/src/main/scala/org/allenai/iqclid/Evaluator.scala index 01e8403..161d373 100644 --- a/src/main/scala/org/allenai/iqclid/Evaluator.scala +++ b/src/main/scala/org/allenai/iqclid/Evaluator.scala @@ -1,6 +1,6 @@ package org.allenai.iqclid -import org.allenai.iqclid.api.{ Evaluator, Solver, Tree } +import org.allenai.iqclid.api.{Evaluator, I, Solver, Tree} case class Info( baseCases: Seq[Int], @@ -44,21 +44,41 @@ class Evaluator { seqs.toStream.map { seq => val results = solver.solve(seq.numberSequence) - val tree = results.head.tree - val actual = Info(seq.numberSequence.baseCases(tree), tree, results.head.fitness, seq.numberSequence.length, 1) - val answer = seq.answer - val expected = Info(seq.numberSequence.baseCases(answer), answer, 0, seq.numberSequence.length, 1) - Evaluation(actual, expected) + results match { + case Seq() => + val actual = Info(seq.numberSequence.baseCases(I()), I(), Double.MaxValue, seq + .numberSequence.length, 1) + val answer = seq.answer + val expected = Info(seq.numberSequence.baseCases(answer), answer, 0, seq.numberSequence.length, 1) + Evaluation(actual, expected) + case _ => + val tree = results.head.tree + val actual = Info(seq.numberSequence.baseCases(tree), tree, results.head.fitness, seq.numberSequence.length, 1) + val answer = seq.answer + val expected = Info(seq.numberSequence.baseCases(answer), answer, 0, seq.numberSequence.length, 1) + Evaluation(actual, expected) + } + + } } - def report(evals: Stream[Evaluation]) = { + def report(evals: Stream[Evaluation], datasetName: String, solver: String) = { evals.foreach { eval => - println(eval) - println +// println(eval) +// println } - val score = evals.count(_.isCorrect).toDouble / evals.size * 100 - println(f"Score: $score%1.2f %%") + val correct = evals.count(_.isCorrect) + val total = evals.size + val incorrect = total - correct + val score = correct.toDouble / total * 100 + println( + f"SOLVER: $solver\n" + + f"DATASET: $datasetName\n" + + f"CORRECT: $correct\n" + + f"INCORRECT: $incorrect\n" + + f"TOTAL: $total\n" + + f"SCORE: $score%1.2f %%\n\n") } } diff --git a/src/main/scala/org/allenai/iqclid/GPSolver.scala b/src/main/scala/org/allenai/iqclid/GPSolver.scala index 75f235d..41dda9e 100644 --- a/src/main/scala/org/allenai/iqclid/GPSolver.scala +++ b/src/main/scala/org/allenai/iqclid/GPSolver.scala @@ -18,7 +18,7 @@ object GPSolver { // val sequence = NumberSequence(Seq(1, 2, 3, 4, 5), 1) val evaluator = new Evaluator val evals = evaluator.eval(IqTest.easy ++ IqTest.medium, solver) - evaluator.report(evals) + evaluator.report(evals, "Easy and Med", "GP SOLVER") } catch { case ex: Exception => println(ex) diff --git a/src/main/scala/org/allenai/iqclid/Main.scala b/src/main/scala/org/allenai/iqclid/Main.scala index ee9674d..e04039b 100644 --- a/src/main/scala/org/allenai/iqclid/Main.scala +++ b/src/main/scala/org/allenai/iqclid/Main.scala @@ -1,15 +1,58 @@ package org.allenai.iqclid +import org.allenai.iqclid.api.{ AccuracyFirstFitness, Ensemble, MultipleRunSolver } +import org.allenai.iqclid.dataset.IqTest +import org.allenai.iqclid.z3.RonanSmtSolver + object Main { def main(args: Array[String]): Unit = { - val s = NumberSequence(Seq(2, 3, 4, 5, 6, 7, 8, 9, 10)) + try { + println("Hello world from Scala!") + println(clj.Bridge.greet) + // clj.Bridge.tutorial(15, 15) + val fitness = new AccuracyFirstFitness(0.5) + // val fitness = new SmallFirstFitness(0.1) + // val gpSolver = new MultipleRunSolver(new GPSolver(fitness), 3) + // val smtSolver = new Z3Solver + // val search = new MultipleRunSolver(new BaselineSearch(0.01, 100, 30), 3) + // val ensemble = new Ensemble(Seq(gpSolver, smtSolver, search)) + val ronan = new RonanSmtSolver + val evaluator = new Evaluator + + evaluator.report(evaluator.eval(IqTest.euclid, ronan), "euclid", "Ronan") + evaluator.report(evaluator.eval(IqTest.easy, ronan), "IQ easy", "Ronan") + evaluator.report(evaluator.eval(IqTest.medium, ronan), "IQ medium", "Ronan") + evaluator.report(evaluator.eval(IqTest.agiPaper, ronan), "agi", "Ronan") + + // evaluator.report(evaluator.eval(IqTest.euclid, gpSolver), "euclid", "GPSolver") + // evaluator.report(evaluator.eval(IqTest.easy, gpSolver), "IQ easy", "GPSolver") + // evaluator.report(evaluator.eval(IqTest.medium, gpSolver), "IQ medium", "GPSolver") + // evaluator.report(evaluator.eval(IqTest.agiPaper, gpSolver), "agi", "GPSolver") + // + // evaluator.report(evaluator.eval(IqTest.euclid, smtSolver), "euclid", "SMT") + // evaluator.report(evaluator.eval(IqTest.easy, smtSolver), "IQ easy", "SMT") + // evaluator.report(evaluator.eval(IqTest.medium, smtSolver), "IQ medium", "SMT") + // evaluator.report(evaluator.eval(IqTest.agiPaper, smtSolver), "agi", "SMT") + // + // evaluator.report(evaluator.eval(IqTest.euclid, search), "euclid", "Local Search") + // evaluator.report(evaluator.eval(IqTest.easy, search), "IQ easy", "Local Search") + // evaluator.report(evaluator.eval(IqTest.medium, search), "IQ medium", "Local Search") + // evaluator.report(evaluator.eval(IqTest.agiPaper, search), "agi", "Local Search") + // + // evaluator.report(evaluator.eval(IqTest.euclid, ensemble), "euclid", "Ensemble") + // evaluator.report(evaluator.eval(IqTest.easy, ensemble), "IQ easy", "Ensemble") + // evaluator.report(evaluator.eval(IqTest.medium, ensemble), "IQ medium", "Ensemble") + // evaluator.report(evaluator.eval(IqTest.agiPaper, ensemble), "agi", "Ensemble") - val search = new BaselineSearch(0.01, 100, 30) - val best = search.best(s) + } catch { + case ex: Exception => + println(ex) + } finally { + sys.exit(0) + } - println(best) } } diff --git a/src/main/scala/org/allenai/iqclid/NumberSequence.scala b/src/main/scala/org/allenai/iqclid/NumberSequence.scala index 778e485..a56c610 100644 --- a/src/main/scala/org/allenai/iqclid/NumberSequence.scala +++ b/src/main/scala/org/allenai/iqclid/NumberSequence.scala @@ -15,10 +15,10 @@ trait Dataset { generated == s.numberSequence.seq :+ s.nextTerm } } - } -case class DatasetSequence(numberSequence: NumberSequence, nextTerm: Int, answer: Tree) +case class DatasetSequence(numberSequence: NumberSequence, nextTerm: Int, answer: Tree, + numBaseCases: Int) /** Class representing a number sequence. numBaseCases represents the number of terms that need * to be fixed to generate the sequence. Ex: For Fibonacci, numBaseCases is 2. diff --git a/src/main/scala/org/allenai/iqclid/Search.scala b/src/main/scala/org/allenai/iqclid/Search.scala index 169eff1..5b460f8 100644 --- a/src/main/scala/org/allenai/iqclid/Search.scala +++ b/src/main/scala/org/allenai/iqclid/Search.scala @@ -19,7 +19,7 @@ abstract class BeamSearch(maxSteps: Int, bestk: Int) extends Search { override def solve(target: NumberSequence): Seq[Solution] = { (0 until maxSteps).foldLeft(Seq[Solution]()) { case (accSols, step) => - println(s"STEP: $step") +// println(s"STEP: $step") val accTrees = accSols.map(_.tree) val p = proposals(accTrees) val candidates = (accTrees ++ proposals(accTrees)) diff --git a/src/main/scala/org/allenai/iqclid/Z3Solver.scala b/src/main/scala/org/allenai/iqclid/Z3Solver.scala index c3e56cd..36c47d4 100644 --- a/src/main/scala/org/allenai/iqclid/Z3Solver.scala +++ b/src/main/scala/org/allenai/iqclid/Z3Solver.scala @@ -7,16 +7,13 @@ import org.allenai.iqclid.z3._ class Z3Solver extends Solver { def getFunctionTree(depth: Int, nSeq: NumberSequence, numBaseCases: Int): Seq[Tree] = { - var upper = 0 + var upper = 100 var lower = 0 var result: Seq[Tree] = Seq() var counter = 0 do { - println("UPPER: " + upper) - println("LOWER: " + lower) - println("RESULT " + result) val newBound = (upper + lower) / 2 counter += 1 try { diff --git a/src/main/scala/org/allenai/iqclid/api/Solver.scala b/src/main/scala/org/allenai/iqclid/api/Solver.scala index 803fbde..c9bfd45 100644 --- a/src/main/scala/org/allenai/iqclid/api/Solver.scala +++ b/src/main/scala/org/allenai/iqclid/api/Solver.scala @@ -16,7 +16,19 @@ trait Solver { class Ensemble(solvers: Seq[Solver]) extends Solver { override def solve(s: NumberSequence): Seq[Solution] = { val solutions = solvers.flatMap(_.solve(s)) - val maxScore = solutions.maxBy(x => x.fitness).fitness + val maxScore = solutions.minBy(x => x.fitness).fitness solutions.filter { x => x.fitness == maxScore } } } + +class MultipleRunSolver(solver: Solver, iterations: Int) extends Solver { + override def solve(s: NumberSequence): Seq[Solution] = { + val solutions = (0 until iterations).foldLeft(Seq[Solution]()) { + case (acc, _) => + acc ++ solver.solve(s) + } + val maxScore = solutions.minBy(x => x.fitness).fitness + solutions.filter { x => x.fitness == maxScore } + } + +} diff --git a/src/main/scala/org/allenai/iqclid/api/TreeApi.scala b/src/main/scala/org/allenai/iqclid/api/TreeApi.scala index 0269328..306e918 100644 --- a/src/main/scala/org/allenai/iqclid/api/TreeApi.scala +++ b/src/main/scala/org/allenai/iqclid/api/TreeApi.scala @@ -28,7 +28,7 @@ object Tree { case Pow() => 10 } thisNode + subTrees - case Number(i) => i + case Number(i) => Math.abs(i) case I() => 1 case T(i) => 2*i } diff --git a/src/main/scala/org/allenai/iqclid/dataset/IqTest.scala b/src/main/scala/org/allenai/iqclid/dataset/IqTest.scala index 5df25f2..4e21cb3 100644 --- a/src/main/scala/org/allenai/iqclid/dataset/IqTest.scala +++ b/src/main/scala/org/allenai/iqclid/dataset/IqTest.scala @@ -1,19 +1,13 @@ package org.allenai.iqclid.dataset -import org.allenai.iqclid.{ DatasetSequence, _ } +import org.allenai.iqclid.{DatasetSequence, _} import org.allenai.iqclid.api._ object IqTest extends Dataset { - val sequences = easy + override lazy val sequences = agiPaper val easy = Seq( - DatasetSequence( - NumberSequence(Seq(1, 1, 2, 3, 5, 8, 13)), - 21, - Apply(Plus(), Seq(T(1), T(2))) - ), - DatasetSequence( NumberSequence(Seq(2, 4, 9, 11, 16)), 18, @@ -22,30 +16,21 @@ object IqTest extends Dataset { Apply(Plus(), Seq( Apply(Times(), Seq( Apply(Mod(), Seq( - Apply(Plus(), Seq(I(), Number(1))), Number(2) - )), - Number(3) - )), - Number(2) - )) - )) - ), + Apply(Plus(), Seq(I(), Number(1))), Number(2))), + Number(3))), + Number(2))))), 1), DatasetSequence( NumberSequence(Seq(30, 28, 25, 21, 16)), 10, Apply(Minus(), Seq( - T(1), Apply(Plus(), Seq(I(), Number(1))) - )) - ), + T(1), Apply(Plus(), Seq(I(), Number(1))))), 1), DatasetSequence( NumberSequence(Seq(-972, 324, -108, 36, -12)), 4, Apply(Div(), Seq( - T(1), Apply(Minus(), Seq(Number(0), Number(3))) - )) - ), + T(1), Apply(Minus(), Seq(Number(0), Number(3))))), 1), // Commented out because we cannot handle decimals // DatasetSequence( @@ -58,20 +43,14 @@ object IqTest extends Dataset { NumberSequence(Seq(16, 22, 34, 52, 76)), 106, Apply(Plus(), Seq( - T(1), Apply(Times(), Seq(Number(6), I())) - )) - ), + T(1), Apply(Times(), Seq(Number(6), I())))), 1), DatasetSequence( NumberSequence(Seq(123, 135, 148, 160, 173)), 185, Apply(Plus(), Seq( - T(1), Apply(Plus(), Seq(Number(12), Apply(Mod(), Seq( - Apply(Plus(), Seq(I(), Number(1))), - Number(2) - )))) - )) - ), + T(1), Apply(Plus(), Seq(Number(12), Apply(Mod(), Seq(Apply(Plus(), Seq(I(), Number(1))), + Number(2))))))), 1), DatasetSequence( NumberSequence(Seq(4, 5, 7, 11, 19)), @@ -79,65 +58,46 @@ object IqTest extends Dataset { Apply(Plus(), Seq( T(1), Apply(Pow(), Seq( Number(2), Apply(Minus(), Seq( - I(), Number(1) - )) - )) - )) - ) - ) + I(), Number(1))))))), 1)) val medium = Seq( DatasetSequence( - NumberSequence(Seq(-2, 5, -4, 3, 6)), + NumberSequence(Seq(-2, 5, -4, 3, -6)), 1, Apply(Minus(), Seq( - T(2), Number(2) - )) - ), + T(2), Number(2))), 2), DatasetSequence( NumberSequence(Seq(1, 4, 9, 16, 25)), 36, Apply(Plus(), Seq( T(1), Apply(Plus(), Seq(Apply(Times(), Seq( - Number(2), I() - )), Number(1))) - )) - ), + Number(2), I())), Number(1))))), 1), - DatasetSequence( - NumberSequence(Seq(75, 15, 25, 5, 15)), - 3, - Apply( - Plus(), - Seq( - Apply(Div(), Seq( - Apply(Times(), Seq( - Apply(Mod(), Seq( - I(), Number(2) - )), - T(1) - )), - Number(5) - )), - Apply( - Plus(), - Seq( - Apply(Times(), Seq( - Apply(Mod(), Seq( - Apply(Plus(), Seq( - I(), Number(1) - )), - Number(2) - )), - T(1) - )), - Number(10) - ) - ) - ) - ) - ), + + // TODO(row11) fix it later + // DatasetSequence( + // NumberSequence(Seq(75, 15, 25, 5, 15), 1), + // 3, + // Apply(Plus(), + // Seq( + // Apply(Div(), Seq( + // Apply(Times(), + // Seq( + // Apply(Mod(), Seq(I(), Number(2))), + // T(1) + // ) + // ), + // Number(5)) + // ), + // Apply(Times(), + // Seq( + // Apply(Mod(), Seq( + // Apply(Plus(), Seq( + // I(), Number(1))), + // Number(2))), + // Number(10)) + // )))), DatasetSequence( NumberSequence(Seq(1, 2, 6, 24, 120)), @@ -145,8 +105,7 @@ object IqTest extends Dataset { Apply(Times(), Seq( T(1), Apply(Plus(), Seq(I(), Number(1))) - )) - ), + )), 1), // Too annoying to encode // DatasetSequence( @@ -160,8 +119,7 @@ object IqTest extends Dataset { Apply(Minus(), Seq( Apply(Times(), Seq(T(1), Number(3))), Apply(Times(), Seq(T(2), Number(2))) - )) - ), + )), 2), DatasetSequence( NumberSequence(Seq(17, 40, 61, 80, 97)), @@ -171,9 +129,7 @@ object IqTest extends Dataset { Apply(Times(), Seq(T(1), Number(2))), T(2) )), - Number(2) - )) - ), + Number(2))), 2), DatasetSequence( NumberSequence(Seq(55, 34, 21, 13, 8)), @@ -181,8 +137,7 @@ object IqTest extends Dataset { Apply(Minus(), Seq( T(2), T(1) - )) - ), + )), 2), DatasetSequence( NumberSequence(Seq(259, 131, 67, 35, 19)), @@ -190,20 +145,17 @@ object IqTest extends Dataset { Apply(Div(), Seq( Apply(Plus(), Seq(T(1), Number(3))), Number(2) - )) - ), + )), 1), + DatasetSequence( NumberSequence(Seq(93, 74, 57, 42, 29)), 18, - Apply( - Plus(), + Apply(Plus(), Seq( - Apply(Minus(), Seq(T(1), Number(19))), - Apply(Times(), Seq(I(), Number(2))) - ) - ) - ), + Apply(Minus(), Seq(Apply(Times(), Seq(Number(2), T(1))), T(2))), + Number(2) + )), 2), DatasetSequence( NumberSequence(Seq(7, 21, 14, 42, 28)), @@ -211,20 +163,16 @@ object IqTest extends Dataset { Apply(Times(), Seq( T(2), Number(2) - )) - ), + )), 2), DatasetSequence( NumberSequence(Seq(2, -12, -32, -58, -90)), -128, - Apply( - Minus(), + Apply(Plus(), Seq( - Apply(Minus(), Seq(T(1), Number(14))), - Apply(Times(), Seq(I(), Number(6))) - ) - ) - ), + Apply(Minus(), Seq(Apply(Times(), Seq(Number(2), T(1))), T(2))), + Number(-6) + )), 2), DatasetSequence( NumberSequence(Seq(0, 9, 36, 81, 144)), @@ -232,7 +180,161 @@ object IqTest extends Dataset { Apply(Pow(), Seq( Apply(Times(), Seq(Number(3), I())), Number(2) - )) + )), 2) + ) + + val euclid = Seq( + DatasetSequence( + NumberSequence(Seq(7, 14, 28, 56, 112)), + 224, + Apply(Times(), Seq(T(1), Number(2))), 1), + + DatasetSequence( + NumberSequence(Seq(-2, -1, 0, 1, 2, 1, 0, -1, -2, -1, 0, 1)), + 2, + Apply(Plus(), Seq(T(8), Number(0))), 8), + + DatasetSequence( + NumberSequence(Seq(1, 2, 3, 1, 2, 3, 1, 2)), + 3, + Apply(Plus(), Seq( + Number(1), + Apply( Mod(), Seq(I(), Number(3))) + )), 0), + + DatasetSequence( + NumberSequence(Seq(1, 2, 3, 1, 2, 3, 1, 2)), + 3, + Apply(Plus(), Seq( + Number(1), + Apply( Mod(), Seq(I(), Number(3))) + )), 0), + + DatasetSequence( + NumberSequence(Seq(-1, 0, 1, -1, 0, 1)), + -1, + Apply(Plus(), Seq( + Number(-1), + Apply( Mod(), Seq(I(), Number(3))) + )), 0), + + DatasetSequence( + NumberSequence(Seq(-1, 1, 2, -1, 1, 2, -1, 1, 2)), + -1, + Apply(Plus(), Seq( + Number(0), + T(3) + )), 3), + + DatasetSequence( + NumberSequence(Seq(1, 2, 1, 2, 1, 2)), + 1, + Apply(Plus(), Seq( + Number(1), + Apply( Mod(), Seq(I(), Number(2))) + )), 0) + ) + + + val agiPaper = Seq( + DatasetSequence( + NumberSequence(Seq(2,5,8,11,14,17,20)), + 23, + Apply(Plus(), Seq(T(1), Number(3))), 1), + + DatasetSequence( + NumberSequence(Seq(25,22,19,16,13,10,7)), + 4, + Apply(Plus(), Seq(T(1), Number(-3))), 1), + + DatasetSequence( + NumberSequence(Seq(8,12,16,20,24,28,32)), + 36, + Apply(Plus(), Seq(T(1), Number(4))), 1), + + DatasetSequence( + NumberSequence(Seq(54,48,42,36,30,24)), + 18, + Apply(Plus(), Seq(T(1), Number(-6))), 1), + + DatasetSequence( + NumberSequence(Seq(28,33,31,36,34,39)), + 37, + Apply(Plus(), Seq(T(2), Number(3))), 2), + + DatasetSequence( + NumberSequence(Seq(6,8,5,7,4,6,3)), + 5, + Apply(Plus(), Seq(T(2), Number(-1))), 2), + + DatasetSequence( + NumberSequence(Seq(9,20,6,17,3,14,0)), + 11, + Apply(Plus(), Seq(T(2), Number(-3))), 2), + + DatasetSequence( + NumberSequence(Seq( 12,15,8,11,4,7,0)), + 3, + Apply(Plus(), Seq(T(2), Number(-4))), 2), + + DatasetSequence( + NumberSequence(Seq(4,11,15,26,41,67)), + 108, + Apply(Plus(), Seq(T(2), T(1))), 2), + + DatasetSequence( + NumberSequence(Seq(3,6,12,24,48,96)), + 192, + Apply(Times(), Seq(T(1), Number(2))), 1), + + DatasetSequence( + NumberSequence(Seq(3,7,15,31,63,127)), + 255, + Apply (Plus(), Seq(Apply(Times(), Seq(T(1), Number(2))), Number(1))), 1), + + DatasetSequence( + NumberSequence(Seq(2,3,5,9,17,33,65)), + 129, + Apply (Plus(), Seq(Apply(Times(), Seq(T(1), Number(2))), Number(-1))), 1), + + DatasetSequence( + NumberSequence(Seq( 2,12,21,29,36,42,47)), + 51, + Apply (Plus(), Seq( + Apply(Plus(), Seq(T(1), Number(11))), + Apply(Times(), Seq(I(), Number(-1))) + ) + ), 1 + ), + + DatasetSequence( + NumberSequence(Seq(148,84,52,36,28,24)), + 22, + Apply (Plus(), Seq( + Apply(Div(), Seq(T(1), Number(2))), + Number(10) + ) + ), 1 + ), + + DatasetSequence( + NumberSequence(Seq(148,84,52,36,28,24)), + 22, + Apply (Plus(), Seq( + Apply(Div(), Seq(T(1), Number(2))), + Number(10) + ) + ), 1 + ), + + DatasetSequence( + NumberSequence(Seq(2,5,9,19,37,75,149)), + 299, + Apply (Plus(), Seq( + Apply(Times(), Seq(T(1), Number(2))), + Apply(Pow(), Seq(Number(-1), Apply(Minus(), Seq(I(), Number(1))))) + ) + ), 1 ) ) -} +} \ No newline at end of file diff --git a/src/main/scala/org/allenai/iqclid/z3/RonanSmtSolver.scala b/src/main/scala/org/allenai/iqclid/z3/RonanSmtSolver.scala new file mode 100644 index 0000000..36672a1 --- /dev/null +++ b/src/main/scala/org/allenai/iqclid/z3/RonanSmtSolver.scala @@ -0,0 +1,61 @@ +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 RonanSmtSolver extends Solver { + override def solve(s: NumberSequence): Seq[Solution] = { + try { + val seq = s.seq + + val solutionSet = { + val sol = + try { + ThreadSafeDependencies.withZ3Module { + z3Module => + new Z3Interface(z3Module, true).solveSequence(seq, 1) + } + } catch { + case _ => + Seq() + } + if (!sol.isEmpty) { + sol + } else { + val sol2 = try { + ThreadSafeDependencies.withZ3Module { + z3Module => + new Z3Interface(z3Module, true).solveSequence(seq, 3) + } + } catch { + case _ => + Seq() + } + if (!sol2.isEmpty) { + sol2 + } else { + try { + ThreadSafeDependencies.withZ3Module { + z3Module => + new Z3Interface(z3Module, true).solveSequence(seq, 2) + } + } catch { + case _ => + Seq() + } + } + } + } + println(solutionSet) + val tree = solutionSet.head.tree + println(Evaluator.evaluate(tree, s.baseCases(tree), s.seq.length + 1)) + + solutionSet + } catch { + case _ => + Seq() + } + } +} \ No newline at end of file diff --git a/src/main/scala/org/allenai/iqclid/z3/Z3Interface.scala b/src/main/scala/org/allenai/iqclid/z3/Z3Interface.scala index 92d7c9d..3239048 100644 --- a/src/main/scala/org/allenai/iqclid/z3/Z3Interface.scala +++ b/src/main/scala/org/allenai/iqclid/z3/Z3Interface.scala @@ -2,9 +2,10 @@ package org.allenai.iqclid.z3 import com.microsoft.z3._ import com.microsoft.z3.Symbol +import org.allenai.iqclid.api._ + import scala.collection.mutable import scala.collection.mutable.ArrayBuffer - import org.allenai.iqclid.z3.ThreadSafeDependencies.Z3Module /** various relevant status values after the SMT program is solved */ @@ -382,7 +383,6 @@ class Z3Interface(z3Module: Z3Module, isIntegerProgram: Boolean) { */ def extractModel(precision: Int): Map[String, String] = { val model = solver.getModel -// println("solution extracted: " + model.toString) // extract variable assignment in the solution found val solution = boolVarMap.mapValues(model.evaluate(_, false)) ++ intVarMap.mapValues(model.evaluate(_, false)) ++ @@ -407,15 +407,29 @@ class Z3Interface(z3Module: Z3Module, isIntegerProgram: Boolean) { } } - def solveSequence(s: Seq[Int]) = { - (new SequenceSolver(s)).solve() + def solveSequence(s: Seq[Int], strategy: Int): Seq[Solution] = { + strategy match { + case 1 => + (new SequenceSolver(s)).solve() + case 2 => + (new RecSequenceSolverOrder1(s)).solve() + case 3 => + (new RecSequenceSolverOrder2(s)).solve() + case _ => + (new SequenceSolver(s)).solve() + } } class SequenceSolver(s: Seq[Int]) { val seqDomain = ctx.mkFiniteDomainSort("Dom", s.size) - val unaOpDomain = ctx.mkFiniteDomainSort("Dom", 6) + val unaOpDomain = ctx.mkFiniteDomainSort("Dom", 7) val binOpDomain = ctx.mkFiniteDomainSort("Dom", 4) + val level = 3 + val leavesRange = (0 to (scala.math.pow(2,level).toInt-1)) + val lvl1Range = (0 to (scala.math.pow(2,level-1).toInt-1)) + val lvl2Range = (0 to (scala.math.pow(2,level-2).toInt-1)) + def mkSeqEq(fun: FuncDecl): BoolExpr = { val eqTerms = s.indices.map(i => ctx.mkEq(ctx.mkApp(fun, ctx.mkNumeral(i, seqDomain)).asInstanceOf[IntExpr], ctx.mkInt(s(i)))) mkAnd(eqTerms) @@ -438,56 +452,380 @@ class Z3Interface(z3Module: Z3Module, isIntegerProgram: Boolean) { } def UnaryOp(op: Expr, x: IntExpr): IntExpr = { - ctx.mkITE(ctx.mkEq(op, ctx.mkInt(0)), ctx.mkInt(0), - ctx.mkITE(ctx.mkEq(op, ctx.mkInt(1)), ctx.mkInt(1), - ctx.mkITE(ctx.mkEq(op, ctx.mkInt(2)), ctx.mkInt(2), - ctx.mkITE(ctx.mkEq(op, ctx.mkInt(3)), ctx.mkInt(3), - ctx.mkITE(ctx.mkEq(op, ctx.mkInt(4)), ctx.mkUnaryMinus(x), - x))))).asInstanceOf[IntExpr] + ctx.mkITE(ctx.mkLe(op.asInstanceOf[IntExpr], ctx.mkInt(5)), op.asInstanceOf[IntExpr], + x).asInstanceOf[IntExpr] + } + + def binOpToTree(op: Int, t1: Tree, t2: Tree): Tree = { + op match { + case 0 => + Apply(Plus(),Seq(t1,t2)) + case 1 => + Apply(Times(),Seq(t1,t2)) + case 2 => + Apply(Mod(),Seq(t1,t2)) + case _ => + t2 + } + } + + def unaOpToTree(op: Int): Tree = { + op match { + case n if n <= 5 => + Number(n) + case _ => + I() + } + } + + def formulaToTree(leafOps: Seq[Int], lvl1Ops: Seq[Int], lvl2Ops: Seq[Int], lvl3Op: Int): Tree = { + val leafs = leavesRange.map(i => unaOpToTree(leafOps(i))) + val lvl1Nodes = lvl1Range.map(i => binOpToTree(lvl1Ops(i),leafs(2*i),leafs(2*i+1))) + val lvl2Nodes = lvl2Range.map(i => binOpToTree(lvl2Ops(i),lvl1Nodes(2*i),lvl1Nodes(2*i+1))) + val lvl3Node = binOpToTree(lvl3Op, lvl2Nodes(0),lvl2Nodes(1)) + lvl3Node } def mkFormula(x: IntExpr): IntExpr = { - val unaop1 = mkIntVar("unaop1", 0, unaOpDomain.getSize.toInt - 1) - val unaop2 = mkIntVar("unaop2", 0, unaOpDomain.getSize.toInt - 1) - val unaop3 = mkIntVar("unaop3", 0, unaOpDomain.getSize.toInt - 1) - val unaop4 = mkIntVar("unaop4", 0, unaOpDomain.getSize.toInt - 1) - val unaop5 = mkIntVar("unaop5", 0, unaOpDomain.getSize.toInt - 1) - val unaop6 = mkIntVar("unaop6", 0, unaOpDomain.getSize.toInt - 1) - val unaop7 = mkIntVar("unaop7", 0, unaOpDomain.getSize.toInt - 1) - val binop1 = mkIntVar("binop1", 0, binOpDomain.getSize.toInt - 1) - val binop2 = mkIntVar("binop2", 0, binOpDomain.getSize.toInt - 1) - val binop3 = mkIntVar("binop3", 0, binOpDomain.getSize.toInt - 1) - - UnaryOp( - unaop1, - BinaryOp( - binop1, - UnaryOp( - unaop2, - BinaryOp( - binop2, - UnaryOp(unaop4, x), - UnaryOp(unaop5, x) - ) - ), - UnaryOp( - unaop3, - BinaryOp( - binop3, - UnaryOp(unaop6, x), - UnaryOp(unaop7, x) - ) - ) - ) - ) + val leafOps = leavesRange.map(i => mkIntVar(s"leafsOp${i}", 0, unaOpDomain.getSize.toInt - 1)) + val lvl1Ops = lvl1Range.map(i => mkIntVar(s"lvl1Op${i}", 0, binOpDomain.getSize.toInt - 1)) + val lvl2Ops = lvl2Range.map(i => mkIntVar(s"lvl2Op${i}", 0, binOpDomain.getSize.toInt - 1)) + val lvl3Op = mkIntVar(s"lvl3Op0", 0, binOpDomain.getSize.toInt - 1) + + val leaves = leavesRange.map(i => UnaryOp(leafOps(i), x)) + val lvl1Nodes = lvl1Range.map(i => BinaryOp(lvl1Ops(i),leaves(2*i),leaves(2*i+1))) + val lvl2Nodes = lvl2Range.map(i => BinaryOp(lvl2Ops(i),lvl1Nodes(2*i),lvl1Nodes(2*i+1))) + val lvl3Node = BinaryOp(lvl3Op,lvl2Nodes(0),lvl2Nodes(1)) + + lvl3Node + } + + // solve 1,2,3,4,5: f(i) = i + // solve 1,4,9,16,25: f(i) = i^2 + // solve 2,4,6,8,10: f(i) = 2*i + // solve 1,2,3,1,2,3: f(i) = (i mod 3) + 1 + def solve(): Seq[Solution] = { + solver.add(mkFormulaEq(mkFormula)) + solver.add(ctx.mkEq(mkIntVar("leafsOp0"),ctx.mkInt(0))) + solver.add(ctx.mkEq(mkIntVar("leafsOp2"),ctx.mkInt(0))) + solver.add(ctx.mkEq(mkIntVar("leafsOp4"),ctx.mkInt(0))) + solver.add(ctx.mkEq(mkIntVar("lvl1Op0"),ctx.mkInt(3))) + solver.add(ctx.mkEq(mkIntVar("lvl1Op1"),ctx.mkInt(3))) + solver.add(ctx.mkEq(mkIntVar("lvl1Op2"),ctx.mkInt(3))) + + val status = check() + val precision = 16 // number of digits of precision for real values in the model + status match { + case SmtUnknown(reason) => + println("Status unknown") + Seq.empty + case SmtUnsatisfiable => + println("No satisfying assignment found") + Seq.empty + case SmtSatisfiable => + val model = extractModel(precision) + val leafOps = leavesRange.map(i => model(s"leafsOp${i}").toInt) + val lvl1Ops = lvl1Range.map(i => model(s"lvl1Op${i}").toInt) + val lvl2Ops = lvl2Range.map(i => model(s"lvl2Op${i}").toInt) + val lvl3Op = model(s"lvl3Op0").toInt + + val tree = formulaToTree(leafOps, lvl1Ops, lvl2Ops, lvl3Op) + Seq(Solution(tree,1)) + case _ => throw new IllegalStateException("Unrecognized SMT status") + } + } + } + + class RecSequenceSolver(s: Seq[Int], order: Int) { + val seqDomain = ctx.mkFiniteDomainSort("Dom", s.size) + val unaOpDomain = ctx.mkFiniteDomainSort("Dom", 4) + val binOpDomain = ctx.mkFiniteDomainSort("Dom", 5) + + val level = 3 + val leavesRange = (0 to (scala.math.pow(2,level).toInt-1)) + val lvl1Range = (0 to (scala.math.pow(2,level-1).toInt-1)) + val lvl2Range = (0 to (scala.math.pow(2,level-2).toInt-1)) + + var id = 0 + def getNext(): String = { + id += 1 + s"x${id}" + } + + def mkSeqEq(fun: FuncDecl): BoolExpr = { + val eqTerms = s.indices.map(i => ctx.mkEq(ctx.mkApp(fun, ctx.mkNumeral(i, seqDomain)).asInstanceOf[IntExpr], ctx.mkInt(s(i)))) + mkAnd(eqTerms) + } + + def mkFormulaEq(formula: IntExpr => IntExpr): BoolExpr = { + val eqTerms = s.indices.filter(_>=order).map(i => { + val fi = mkIntVar(s"f_$i") + solver.add(ctx.mkEq(fi, formula(ctx.mkInt(i)))) + ctx.mkEq(fi, ctx.mkInt(s(i))) + }) + mkAnd(eqTerms) + } + + def PrevOp(x: IntExpr): IntExpr = { + val key = s"s_minus_1_${x}" + if( !intVarMap.contains(key) ) { + val Sminus1 = mkIntVar(s"s_minus_1_${x}") + intVarMap.put(key,Sminus1) + val zeroterms = s.indices.map(i => ctx.mkImplies(mkLe(Seq(x, ctx.mkInt(0))), ctx.mkEq(Sminus1, ctx.mkInt(0)))) + solver.add(zeroterms: _*) + val minus1terms = s.indices.filter(_>0).map(i => ctx.mkImplies(mkEq(Seq(x, ctx.mkInt(i))), ctx.mkEq(Sminus1, ctx.mkInt(s(i - 1))))) + solver.add(minus1terms: _*) + } + intVarMap(key) + } + + def SecondPrevOp(x: IntExpr): IntExpr = { + val key = s"s_minus_2_${x}" + if( !intVarMap.contains(key) ) { + val Sminus2 = mkIntVar(s"s_minus_2_${x}") + intVarMap.put(key,Sminus2) + val zeroterms = s.indices.map(i => ctx.mkImplies(mkLe(Seq(x, ctx.mkInt(1))), ctx.mkEq(Sminus2, zeroConst))) + solver.add(zeroterms: _*) + val minus2terms = s.indices.filter(_>1).map(i => ctx.mkImplies(mkEq(Seq(x, ctx.mkInt(i))), ctx.mkEq(Sminus2, ctx.mkInt(s(i - 2))))) + solver.add(minus2terms: _*) + } + intVarMap(key) + } + + def BinaryOp(op: Expr, x: IntExpr, y: IntExpr): IntExpr = { + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(0)), ctx.mkAdd(x, y), + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(1)), ctx.mkSub(x, y), + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(2)), ctx.mkMul(x, y), + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(3)), ctx.mkITE(ctx.mkLe(y, ctx.mkInt(0)), y, ctx.mkMod(x, y)), + y)))).asInstanceOf[IntExpr] + } + + def UnaryOp(opvar: String, op: Expr, x: IntExpr): IntExpr = { + var opvarval = ctx.mkIntConst(opvar) + solver.add(ctx.mkLe(opvarval,ctx.mkInt(9))) + solver.add(ctx.mkGe(opvarval,ctx.mkInt(-1))) + ctx.mkITE(ctx.mkEq(op.asInstanceOf[IntExpr], ctx.mkInt(0)), ctx.mkInt(0), + ctx.mkITE(ctx.mkEq(op.asInstanceOf[IntExpr], ctx.mkInt(1)), opvarval, + ctx.mkITE(ctx.mkEq(op.asInstanceOf[IntExpr], ctx.mkInt(2)), x, + PrevOp(x)))).asInstanceOf[IntExpr] + } + + def binOpToTree(op: Int, t1: Tree, t2: Tree): Tree = { + op match { + case 0 => + Apply(Plus(),Seq(t1,t2)) + case 1 => + Apply(Minus(),Seq(t1,t2)) + case 2 => + Apply(Times(),Seq(t1,t2)) + case 3 => + Apply(Mod(),Seq(t1,t2)) + case _ => + t2 + } + } + + def unaOpToTree(op: Int, opvarval: Int): Tree = { + op match { + case 0 => + Number(0) + case 1 => + Number(opvarval) + case 2 => + I() + case _ => + T(1) + } + } + + def formulaToTree(leafOps: Seq[Int],leafOpsVarVal: Seq[Int], lvl1Ops: Seq[Int], lvl2Ops: Seq[Int], lvl3Op: Int): Tree = { + val leafs = leavesRange.map(i => unaOpToTree(leafOps(i),leafOpsVarVal(i))) + val lvl1Nodes = lvl1Range.map(i => binOpToTree(lvl1Ops(i),leafs(2*i),leafs(2*i+1))) + val lvl2Nodes = lvl2Range.map(i => binOpToTree(lvl2Ops(i),lvl1Nodes(2*i),lvl1Nodes(2*i+1))) + val lvl3Node = binOpToTree(lvl3Op, lvl2Nodes(0),lvl2Nodes(1)) + lvl3Node + } + + def mkFormula(x: IntExpr): IntExpr = { + val leafOps = leavesRange.map(i => mkIntVar(s"leafsOp${i}", 0, unaOpDomain.getSize.toInt - 1)) + val lvl1Ops = lvl1Range.map(i => mkIntVar(s"lvl1Op${i}", 0, binOpDomain.getSize.toInt - 1)) + val lvl2Ops = lvl2Range.map(i => mkIntVar(s"lvl2Op${i}", 0, binOpDomain.getSize.toInt - 1)) + val lvl3Op = mkIntVar(s"lvl3Op0", 0, binOpDomain.getSize.toInt - 1) + + val leaves = leavesRange.map(i => UnaryOp(s"leafopvar${i}", leafOps(i), x)) + val lvl1Nodes = lvl1Range.map(i => BinaryOp(lvl1Ops(i),leaves(2*i),leaves(2*i+1))) + val lvl2Nodes = lvl2Range.map(i => BinaryOp(lvl2Ops(i),lvl1Nodes(2*i),lvl1Nodes(2*i+1))) + val lvl3Node = BinaryOp(lvl3Op,lvl2Nodes(0),lvl2Nodes(1)) + + lvl3Node + } + + // solve 1,2,3,4,5: f(i) = i + // solve 1,4,9,16,25: f(i) = i^2 + // solve 2,4,6,8,10: f(i) = 2*i + // solve 1,2,3,1,2,3: f(i) = (i mod 3) + 1 + def solve(): Seq[Solution] = { + leavesRange.foreach(i => solver.add(ctx.mkGe(mkIntVar(s"leafopvar${i}"),ctx.mkInt(-5)))) + solver.add(mkFormulaEq(mkFormula)) + solver.add(ctx.mkLe(mkIntVar("leafsOp0"),ctx.mkInt(1))) + solver.add(ctx.mkEq(mkIntVar("leafsOp1"),ctx.mkInt(3))) + solver.add(ctx.mkLe(mkIntVar("leafsOp2"),ctx.mkInt(1))) + solver.add(ctx.mkLe(mkIntVar("leafsOp3"),ctx.mkInt(1))) + solver.add(ctx.mkEq(mkIntVar("leafsOp4"),ctx.mkInt(2))) + solver.add(ctx.mkLe(mkIntVar("leafsOp5"),ctx.mkInt(1))) + solver.add(ctx.mkLe(mkIntVar("leafsOp6"),ctx.mkInt(1))) + solver.add(ctx.mkLe(mkIntVar("leafsOp7"),ctx.mkInt(1))) + //(4 to 7).foreach(i => solver.add(ctx.mkLe(mkIntVar(s"leafsOp${i}"),ctx.mkInt(2)))) + //solver.add(ctx.mkEq(mkIntVar("lvl1Op0"),ctx.mkInt(4))) + //solver.add(ctx.mkEq(mkIntVar("lvl1Op1"),ctx.mkInt(3))) + //solver.add(ctx.mkEq(mkIntVar("lvl1Op2"),ctx.mkInt(3))) + + val status = check() + val precision = 16 // number of digits of precision for real values in the model + status match { + case SmtUnknown(reason) => + println("Status unknown") + Seq.empty + case SmtUnsatisfiable => + println("No satisfying assignment found") + Seq.empty + case SmtSatisfiable => + val model = extractModel(precision) + println(model) + val leafOps = leavesRange.map(i => model(s"leafsOp${i}").toInt) + val leafOpsVarVal = leavesRange.map(i => model(s"leafopvar${i}").toInt) + val lvl1Ops = lvl1Range.map(i => model(s"lvl1Op${i}").toInt) + val lvl2Ops = lvl2Range.map(i => model(s"lvl2Op${i}").toInt) + val lvl3Op = model(s"lvl3Op0").toInt + + val tree = formulaToTree(leafOps, leafOpsVarVal, lvl1Ops, lvl2Ops, lvl3Op) + Seq(Solution(tree,1)) + case _ => throw new IllegalStateException("Unrecognized SMT status") + } + } + } + + class RecSequenceSolverOrder1(s: Seq[Int]) { + val a = mkIntVar("a",1,3) + val b = mkIntVar("b",-3,3) + solver.add(mkIsNonZero(b)) + + val seqDomain = ctx.mkFiniteDomainSort("Dom", s.size) + val unaOpDomain = ctx.mkFiniteDomainSort("Dom", 3) + val binOpDomain = ctx.mkFiniteDomainSort("Dom", 5) + + val level = 3 + val leavesRange = (0 to (scala.math.pow(2,level).toInt-1)) + val lvl1Range = (0 to (scala.math.pow(2,level-1).toInt-1)) + val lvl2Range = (0 to (scala.math.pow(2,level-2).toInt-1)) + + var id = 0 + def getNext(): String = { + id += 1 + s"x${id}" + } + + def mkSeqEq(fun: FuncDecl): BoolExpr = { + val eqTerms = s.indices.map(i => ctx.mkEq(ctx.mkApp(fun, ctx.mkNumeral(i, seqDomain)).asInstanceOf[IntExpr], ctx.mkInt(s(i)))) + mkAnd(eqTerms) + } + + def mkFormulaEq(formula: IntExpr => IntExpr): BoolExpr = { + val eqTerms = s.indices.filter(_>=1).map(i => { + val fi = mkIntVar(s"f_$i") + solver.add(ctx.mkEq(fi, formula(ctx.mkInt(i)))) + ctx.mkEq(fi, ctx.mkAdd(ctx.mkMul(a,ctx.mkInt(s(i))),ctx.mkMul(b,ctx.mkInt(s(i-1))))) + }) + mkAnd(eqTerms) + } + + def BinaryOp(op: Expr, x: IntExpr, y: IntExpr): IntExpr = { + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(0)), ctx.mkAdd(x, y), + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(1)), ctx.mkSub(x, y), + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(2)), ctx.mkMul(x, y), + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(3)), ctx.mkITE(ctx.mkLe(y, ctx.mkInt(0)), y, ctx.mkMod(x, y)), + y)))).asInstanceOf[IntExpr] + } + + def UnaryOp(opvar: String, op: Expr, x: IntExpr): IntExpr = { + var opvarval = ctx.mkIntConst(opvar) + solver.add(ctx.mkLe(opvarval,ctx.mkInt(9))) + solver.add(ctx.mkGe(opvarval,ctx.mkInt(-1))) + ctx.mkITE(ctx.mkEq(op.asInstanceOf[IntExpr], ctx.mkInt(0)), ctx.mkInt(0), + ctx.mkITE(ctx.mkEq(op.asInstanceOf[IntExpr], ctx.mkInt(1)), opvarval, + x)).asInstanceOf[IntExpr] + } + + def binOpToTree(op: Int, t1: Tree, t2: Tree): Tree = { + op match { + case 0 => + Apply(Plus(),Seq(t1,t2)) + case 1 => + Apply(Minus(),Seq(t1,t2)) + case 2 => + Apply(Times(),Seq(t1,t2)) + case 3 => + Apply(Mod(),Seq(t1,t2)) + case _ => + t2 + } + } + + def unaOpToTree(op: Int, opvarval: Int): Tree = { + op match { + case 0 => + Number(0) + case 1 => + Number(opvarval) + case 2 => + I() + case _ => + T(1) + } + } + + def formulaToTree(leafOps: Seq[Int],leafOpsVarVal: Seq[Int], lvl1Ops: Seq[Int], lvl2Ops: Seq[Int], lvl3Op: Int): Tree = { + val leafs = leavesRange.map(i => unaOpToTree(leafOps(i),leafOpsVarVal(i))) + val lvl1Nodes = lvl1Range.map(i => binOpToTree(lvl1Ops(i),leafs(2*i),leafs(2*i+1))) + val lvl2Nodes = lvl2Range.map(i => binOpToTree(lvl2Ops(i),lvl1Nodes(2*i),lvl1Nodes(2*i+1))) + val lvl3Node = binOpToTree(lvl3Op, lvl2Nodes(0),lvl2Nodes(1)) + lvl3Node + } + + def mkFormula(x: IntExpr): IntExpr = { + val leafOps = leavesRange.map(i => mkIntVar(s"leafsOp${i}", 0, unaOpDomain.getSize.toInt - 1)) + val lvl1Ops = lvl1Range.map(i => mkIntVar(s"lvl1Op${i}", 0, binOpDomain.getSize.toInt - 1)) + val lvl2Ops = lvl2Range.map(i => mkIntVar(s"lvl2Op${i}", 0, binOpDomain.getSize.toInt - 1)) + val lvl3Op = mkIntVar(s"lvl3Op0", 0, binOpDomain.getSize.toInt - 1) + + val leaves = leavesRange.map(i => UnaryOp(s"leafopvar${i}", leafOps(i), x)) + val lvl1Nodes = lvl1Range.map(i => BinaryOp(lvl1Ops(i),leaves(2*i),leaves(2*i+1))) + val lvl2Nodes = lvl2Range.map(i => BinaryOp(lvl2Ops(i),lvl1Nodes(2*i),lvl1Nodes(2*i+1))) + val lvl3Node = BinaryOp(lvl3Op,lvl2Nodes(0),lvl2Nodes(1)) + + lvl3Node } // solve 1,2,3,4,5: f(i) = i // solve 1,4,9,16,25: f(i) = i^2 // solve 2,4,6,8,10: f(i) = 2*i // solve 1,2,3,1,2,3: f(i) = (i mod 3) + 1 - def solve() = { + def solve(): Seq[Solution] = { + leavesRange.foreach(i => solver.add(ctx.mkGe(mkIntVar(s"leafopvar${i}"),ctx.mkInt(-5)))) solver.add(mkFormulaEq(mkFormula)) + solver.add(ctx.mkLe(mkIntVar("leafsOp0"),ctx.mkInt(1))) + solver.add(ctx.mkEq(mkIntVar("leafsOp1"),ctx.mkInt(2))) + solver.add(ctx.mkLe(mkIntVar("leafsOp2"),ctx.mkInt(1))) + solver.add(ctx.mkLe(mkIntVar("leafsOp3"),ctx.mkInt(1))) + solver.add(ctx.mkEq(mkIntVar("leafsOp4"),ctx.mkInt(0))) + solver.add(ctx.mkLe(mkIntVar("leafsOp5"),ctx.mkInt(0))) + solver.add(ctx.mkLe(mkIntVar("leafsOp6"),ctx.mkInt(0))) + solver.add(ctx.mkLe(mkIntVar("leafsOp7"),ctx.mkInt(0))) + //(4 to 7).foreach(i => solver.add(ctx.mkLe(mkIntVar(s"leafsOp${i}"),ctx.mkInt(2)))) + //solver.add(ctx.mkEq(mkIntVar("lvl1Op0"),ctx.mkInt(4))) + //solver.add(ctx.mkEq(mkIntVar("lvl1Op1"),ctx.mkInt(3))) + //solver.add(ctx.mkEq(mkIntVar("lvl1Op2"),ctx.mkInt(3))) + val status = check() val precision = 16 // number of digits of precision for real values in the model status match { @@ -498,9 +836,170 @@ class Z3Interface(z3Module: Z3Module, isIntegerProgram: Boolean) { Seq.empty case SmtSatisfiable => val model = extractModel(precision) -// println(model) -// println("SMT solution: " + model.mkString(", ")) - Seq(model) + println(model) + val leafOps = leavesRange.map(i => model(s"leafsOp${i}").toInt) + val leafOpsVarVal = leavesRange.map(i => model(s"leafopvar${i}").toInt) + val lvl1Ops = lvl1Range.map(i => model(s"lvl1Op${i}").toInt) + val lvl2Ops = lvl2Range.map(i => model(s"lvl2Op${i}").toInt) + val lvl3Op = model(s"lvl3Op0").toInt + + val aVal = model("a").toInt + val bVal = model("b").toInt + val tree = formulaToTree(leafOps, leafOpsVarVal, lvl1Ops, lvl2Ops, lvl3Op) + val sol = Apply(Div(),Seq(Apply(Minus(),Seq(tree,Apply(Times(),Seq(Number(bVal),T(1))))),Number(aVal))) + Seq(Solution(sol,1)) + case _ => throw new IllegalStateException("Unrecognized SMT status") + } + } + } + + class RecSequenceSolverOrder2(s: Seq[Int]) { + val a = mkIntVar("a",1,3) + val b = mkIntVar("b",-3,3) + val c = mkIntVar("c",-3,3) + solver.add(mkIsNonZero(b)) + solver.add(mkIsNonZero(c)) + + val seqDomain = ctx.mkFiniteDomainSort("Dom", s.size) + val unaOpDomain = ctx.mkFiniteDomainSort("Dom", 3) + val binOpDomain = ctx.mkFiniteDomainSort("Dom", 5) + + val level = 3 + val leavesRange = (0 to (scala.math.pow(2,level).toInt-1)) + val lvl1Range = (0 to (scala.math.pow(2,level-1).toInt-1)) + val lvl2Range = (0 to (scala.math.pow(2,level-2).toInt-1)) + + var id = 0 + def getNext(): String = { + id += 1 + s"x${id}" + } + + def mkSeqEq(fun: FuncDecl): BoolExpr = { + val eqTerms = s.indices.map(i => ctx.mkEq(ctx.mkApp(fun, ctx.mkNumeral(i, seqDomain)).asInstanceOf[IntExpr], ctx.mkInt(s(i)))) + mkAnd(eqTerms) + } + + def mkFormulaEq(formula: IntExpr => IntExpr): BoolExpr = { + val eqTerms = s.indices.filter(_>=2).map(i => { + val fi = mkIntVar(s"f_$i") + solver.add(ctx.mkEq(fi, formula(ctx.mkInt(i)))) + ctx.mkEq(fi, ctx.mkAdd(ctx.mkAdd(ctx.mkMul(a,ctx.mkInt(s(i))),ctx.mkMul(b,ctx.mkInt(s(i-1)))),ctx.mkMul(c,ctx.mkInt(s(i-2))))) + }) + mkAnd(eqTerms) + } + + def BinaryOp(op: Expr, x: IntExpr, y: IntExpr): IntExpr = { + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(0)), ctx.mkAdd(x, y), + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(1)), ctx.mkSub(x, y), + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(2)), ctx.mkMul(x, y), + ctx.mkITE(ctx.mkEq(op, ctx.mkInt(3)), ctx.mkITE(ctx.mkLe(y, ctx.mkInt(0)), y, ctx.mkMod(x, y)), + y)))).asInstanceOf[IntExpr] + } + + def UnaryOp(opvar: String, op: Expr, x: IntExpr): IntExpr = { + var opvarval = ctx.mkIntConst(opvar) + solver.add(ctx.mkLe(opvarval,ctx.mkInt(9))) + solver.add(ctx.mkGe(opvarval,ctx.mkInt(-1))) + ctx.mkITE(ctx.mkEq(op.asInstanceOf[IntExpr], ctx.mkInt(0)), ctx.mkInt(0), + ctx.mkITE(ctx.mkEq(op.asInstanceOf[IntExpr], ctx.mkInt(1)), opvarval, + x)).asInstanceOf[IntExpr] + } + + def binOpToTree(op: Int, t1: Tree, t2: Tree): Tree = { + op match { + case 0 => + Apply(Plus(),Seq(t1,t2)) + case 1 => + Apply(Minus(),Seq(t1,t2)) + case 2 => + Apply(Times(),Seq(t1,t2)) + case 3 => + Apply(Mod(),Seq(t1,t2)) + case _ => + t2 + } + } + + def unaOpToTree(op: Int, opvarval: Int): Tree = { + op match { + case 0 => + Number(0) + case 1 => + Number(opvarval) + case 2 => + I() + case _ => + T(1) + } + } + + def formulaToTree(leafOps: Seq[Int],leafOpsVarVal: Seq[Int], lvl1Ops: Seq[Int], lvl2Ops: Seq[Int], lvl3Op: Int): Tree = { + val leafs = leavesRange.map(i => unaOpToTree(leafOps(i),leafOpsVarVal(i))) + val lvl1Nodes = lvl1Range.map(i => binOpToTree(lvl1Ops(i),leafs(2*i),leafs(2*i+1))) + val lvl2Nodes = lvl2Range.map(i => binOpToTree(lvl2Ops(i),lvl1Nodes(2*i),lvl1Nodes(2*i+1))) + val lvl3Node = binOpToTree(lvl3Op, lvl2Nodes(0),lvl2Nodes(1)) + lvl3Node + } + + def mkFormula(x: IntExpr): IntExpr = { + val leafOps = leavesRange.map(i => mkIntVar(s"leafsOp${i}", 0, unaOpDomain.getSize.toInt - 1)) + val lvl1Ops = lvl1Range.map(i => mkIntVar(s"lvl1Op${i}", 0, binOpDomain.getSize.toInt - 1)) + val lvl2Ops = lvl2Range.map(i => mkIntVar(s"lvl2Op${i}", 0, binOpDomain.getSize.toInt - 1)) + val lvl3Op = mkIntVar(s"lvl3Op0", 0, binOpDomain.getSize.toInt - 1) + + val leaves = leavesRange.map(i => UnaryOp(s"leafopvar${i}", leafOps(i), x)) + val lvl1Nodes = lvl1Range.map(i => BinaryOp(lvl1Ops(i),leaves(2*i),leaves(2*i+1))) + val lvl2Nodes = lvl2Range.map(i => BinaryOp(lvl2Ops(i),lvl1Nodes(2*i),lvl1Nodes(2*i+1))) + val lvl3Node = BinaryOp(lvl3Op,lvl2Nodes(0),lvl2Nodes(1)) + + lvl3Node + } + + // solve 1,2,3,4,5: f(i) = i + // solve 1,4,9,16,25: f(i) = i^2 + // solve 2,4,6,8,10: f(i) = 2*i + // solve 1,2,3,1,2,3: f(i) = (i mod 3) + 1 + def solve(): Seq[Solution] = { + leavesRange.foreach(i => solver.add(ctx.mkGe(mkIntVar(s"leafopvar${i}"),ctx.mkInt(-5)))) + solver.add(mkFormulaEq(mkFormula)) + solver.add(ctx.mkLe(mkIntVar("leafsOp0"),ctx.mkInt(1))) + solver.add(ctx.mkEq(mkIntVar("leafsOp1"),ctx.mkInt(2))) + solver.add(ctx.mkLe(mkIntVar("leafsOp2"),ctx.mkInt(1))) + solver.add(ctx.mkLe(mkIntVar("leafsOp3"),ctx.mkInt(1))) + solver.add(ctx.mkEq(mkIntVar("leafsOp4"),ctx.mkInt(0))) + solver.add(ctx.mkLe(mkIntVar("leafsOp5"),ctx.mkInt(0))) + solver.add(ctx.mkLe(mkIntVar("leafsOp6"),ctx.mkInt(0))) + solver.add(ctx.mkLe(mkIntVar("leafsOp7"),ctx.mkInt(0))) + //(4 to 7).foreach(i => solver.add(ctx.mkLe(mkIntVar(s"leafsOp${i}"),ctx.mkInt(2)))) + //solver.add(ctx.mkEq(mkIntVar("lvl1Op0"),ctx.mkInt(4))) + //solver.add(ctx.mkEq(mkIntVar("lvl1Op1"),ctx.mkInt(3))) + //solver.add(ctx.mkEq(mkIntVar("lvl1Op2"),ctx.mkInt(3))) + + val status = check() + val precision = 16 // number of digits of precision for real values in the model + status match { + case SmtUnknown(reason) => + println("Status unknown") + Seq.empty + case SmtUnsatisfiable => + println("No satisfying assignment found") + Seq.empty + case SmtSatisfiable => + val model = extractModel(precision) + println(model) + val leafOps = leavesRange.map(i => model(s"leafsOp${i}").toInt) + val leafOpsVarVal = leavesRange.map(i => model(s"leafopvar${i}").toInt) + val lvl1Ops = lvl1Range.map(i => model(s"lvl1Op${i}").toInt) + val lvl2Ops = lvl2Range.map(i => model(s"lvl2Op${i}").toInt) + val lvl3Op = model(s"lvl3Op0").toInt + + val aVal = model("a").toInt + val bVal = model("b").toInt + val cVal = model("c").toInt + val tree = formulaToTree(leafOps, leafOpsVarVal, lvl1Ops, lvl2Ops, lvl3Op) + val sol = Apply(Div(),Seq(Apply(Minus(),Seq(Apply(Minus(),Seq(tree,Apply(Times(),Seq(Number(bVal),T(1))))),Apply(Times(),Seq(Number(cVal),T(2))))),Number(aVal))) + Seq(Solution(sol,1)) case _ => throw new IllegalStateException("Unrecognized SMT status") } } diff --git a/src/test/scala/Z3Spec.scala b/src/test/scala/Z3Spec.scala index 9b80bf8..e22324d 100644 --- a/src/test/scala/Z3Spec.scala +++ b/src/test/scala/Z3Spec.scala @@ -1,11 +1,10 @@ import org.allenai.common.testkit.UnitSpec -import org.allenai.iqclid.api.{Apply, I, Number, Plus} -import org.allenai.iqclid.{BaselineSearch, NumberSequence, Z3Solver} +import org.allenai.iqclid.{ NumberSequence, Z3Solver} class Z3Spec extends UnitSpec { "" should "" in { - val s = NumberSequence(Seq(1, 2, 3, 4, 5), 1) + val s = NumberSequence(Seq(1, 2, 3, 4, 5)) val solver = new Z3Solver println("ANSWER IS: "+ solver.solve(s).head) } diff --git a/src/test/scala/org/allenai/iqclid/z3/SmtSolverSpec.scala b/src/test/scala/org/allenai/iqclid/z3/SmtSolverSpec.scala new file mode 100644 index 0000000..1585679 --- /dev/null +++ b/src/test/scala/org/allenai/iqclid/z3/SmtSolverSpec.scala @@ -0,0 +1,57 @@ +package org.allenai.iqclid.z3 + +import org.allenai.common.testkit.UnitSpec +import org.allenai.common.testkit.UnitSpec +import org.allenai.iqclid.api._ +import org.allenai.iqclid.{BaselineSearch, NumberSequence} + +class SmtSolverSpec extends UnitSpec{ +// +// "smt" should "do 1 2 3 4 5" in { +// val s = NumberSequence(Seq(1, 2, 3, 4, 5, 6), 1) +// val smt = new RonanSmtSolver() +// smt.solve(s) +// } +// +// "smt" should "do 2 4 6 8" in { +// val s = NumberSequence(Seq(2,4,6,8), 1) +// val smt = new RonanSmtSolver() +// smt.solve(s) +// } +// +// val s = NumberSequence(Seq(1,2,3,1,2,3), 1) +// "smt" should "do 1 2 3 1 2 3" in { +// val smt = new RonanSmtSolver() +// smt.solve(s) +// } +// +// "smt" should "do 1 4 9 16 25" in { +// val s = NumberSequence(Seq(1,4,9,16,25), 1) +// val smt = new RonanSmtSolver() +// smt.solve(s) +// } +// +// "smt" should "do 16, 22, 34, 52, 76" in { +// val s = NumberSequence(Seq(16, 22, 34, 52, 76), 2) +// val smt = new RonanSmtSolver() +// smt.solve(s) +// } +// +// "smt" should "do 30, 28, 25, 21, 16" in { +// val s = NumberSequence(Seq(30, 28, 25, 21, 16), 2) +// val smt = new RonanSmtSolver() +// smt.solve(s) +// } +// +// "smt" should "do 123, 135, 148, 160, 173" in { +// val s = NumberSequence(Seq(123, 135, 148, 160, 173), 2) +// val smt = new RonanSmtSolver() +// smt.solve(s) +// } +// +// "smt" should "do 1, 1, 2, 3, 5, 8, 13, 21, 34" in { +// val s = NumberSequence(Seq(1, 1, 2, 3, 5, 8, 13, 21, 34), 2) +// val smt = new RonanSmtSolver() +// smt.solve(s) +// } +}