Skip to content
Snippets Groups Projects
Commit d920a174 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Update to latest scala-smtlib

parent 572ea63f
Branches
Tags
No related merge requests found
...@@ -142,7 +142,7 @@ def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${versi ...@@ -142,7 +142,7 @@ def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${versi
lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539") lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "6b74fb332416d470e0be7bf6e94ebc18fd300c2f") lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "cee5129e483515d7011134df669b450b92e6f871")
lazy val root = (project in file(".")). lazy val root = (project in file(".")).
configs(RegressionTest). configs(RegressionTest).
......
...@@ -9,7 +9,7 @@ import Definitions._ ...@@ -9,7 +9,7 @@ import Definitions._
import Constructors._ import Constructors._
import DefOps.typedTransitiveCallees import DefOps.typedTransitiveCallees
import smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _} import smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
import smtlib.parser.Terms.{Exists => SMTExists, ForAll => SMTForall, _ } import smtlib.parser.Terms.{Exists => SMTExists, Forall => SMTForall, _ }
import smtlib.theories.Core.Equals import smtlib.theories.Core.Equals
// This solver utilizes the define-funs-rec command of SMTLIB-2.5 to define mutually recursive functions. // This solver utilizes the define-funs-rec command of SMTLIB-2.5 to define mutually recursive functions.
......
...@@ -14,7 +14,7 @@ import Extractors._ ...@@ -14,7 +14,7 @@ import Extractors._
import Constructors._ import Constructors._
import Types._ import Types._
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, ForAll => SMTForall, _} import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Forall => SMTForall, _}
import _root_.smtlib.parser.Commands._ import _root_.smtlib.parser.Commands._
import _root_.smtlib.interpreters.CVC4Interpreter import _root_.smtlib.interpreters.CVC4Interpreter
import _root_.smtlib.theories._ import _root_.smtlib.theories._
......
...@@ -18,7 +18,7 @@ import _root_.smtlib.common._ ...@@ -18,7 +18,7 @@ import _root_.smtlib.common._
import _root_.smtlib.printer.{RecursivePrinter => SMTPrinter} import _root_.smtlib.printer.{RecursivePrinter => SMTPrinter}
import _root_.smtlib.parser.Commands.{Constructor => SMTConstructor, FunDef => _, Assert => SMTAssert, _} import _root_.smtlib.parser.Commands.{Constructor => SMTConstructor, FunDef => _, Assert => SMTAssert, _}
import _root_.smtlib.parser.Terms.{ import _root_.smtlib.parser.Terms.{
ForAll => SMTForall, Forall => SMTForall,
Exists => SMTExists, Exists => SMTExists,
Identifier => SMTIdentifier, Identifier => SMTIdentifier,
Let => SMTLet, Let => SMTLet,
......
...@@ -9,7 +9,7 @@ import Definitions._ ...@@ -9,7 +9,7 @@ import Definitions._
import Expressions._ import Expressions._
import Constructors._ import Constructors._
import smtlib.parser.Commands.{Assert => SMTAssert} import smtlib.parser.Commands.{Assert => SMTAssert}
import smtlib.parser.Terms.{ForAll => SMTForall, SSymbol} import smtlib.parser.Terms.{Forall => SMTForall, SSymbol}
/** /**
* This solver models function definitions as universally quantified formulas. * This solver models function definitions as universally quantified formulas.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment