Implement basic sygus, only possible in --manual mode for now
Split SMTLIBSolver to Solver+Target to allow things other than leon solvers to talk SMT.
Showing
- build.sbt 1 addition, 1 deletionbuild.sbt
- src/main/scala/leon/solvers/RawArray.scala 9 additions, 9 deletionssrc/main/scala/leon/solvers/RawArray.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala 8 additions, 8 deletions...ain/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala 2 additions, 107 deletions...cala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala 118 additions, 0 deletions...cala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala 3 additions, 129 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala 133 additions, 0 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala 9 additions, 50 deletions...in/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala 52 additions, 0 deletions...in/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala 39 additions, 720 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala 818 additions, 0 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBUnsupportedError.scala 10 additions, 0 deletions...in/scala/leon/solvers/smtlib/SMTLIBUnsupportedError.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala 3 additions, 65 deletions.../scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala 76 additions, 0 deletions.../scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala 5 additions, 166 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala 183 additions, 0 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
- src/main/scala/leon/solvers/sygus/CVC4SygusSolver.scala 29 additions, 0 deletionssrc/main/scala/leon/solvers/sygus/CVC4SygusSolver.scala
- src/main/scala/leon/solvers/sygus/SygusSolver.scala 131 additions, 0 deletionssrc/main/scala/leon/solvers/sygus/SygusSolver.scala
- src/main/scala/leon/synthesis/Rules.scala 1 addition, 1 deletionsrc/main/scala/leon/synthesis/Rules.scala
- src/main/scala/leon/synthesis/Solution.scala 4 additions, 0 deletionssrc/main/scala/leon/synthesis/Solution.scala
Loading
Please register or sign in to comment