Permalink
Browse files

Z3: Upgrade to version 4.5.0

Use Z3 nightly from frozen repo
  • Loading branch information...
marcogario committed Aug 17, 2017
1 parent 9f6eb3b commit ab17a36b4c71023b61c122a141a3f94f4bededd5
Showing with 41 additions and 31 deletions.
  1. +3 −3 appveyor.yml
  2. +6 −3 pysmt/cmd/install.py
  3. +2 −2 pysmt/cmd/installers/base.py
  4. +8 −13 pysmt/cmd/installers/z3.py
  5. +2 −2 pysmt/constants.py
  6. +7 −4 pysmt/solvers/z3.py
  7. +13 −4 pysmt/test/test_nlira.py
View
@@ -75,10 +75,10 @@ install:
- "%CMD_IN_ENV% python install.py --confirm-agreement"
# Set the pythonpath
- "python install.py --env > bindings_path.txt"
- "SET /p BINDINGS_CMD=<bindings_path.txt"
- "%BINDINGS_CMD%"
- "python install.py --env > bindings_path.bat"
- call ./bindings_path.bat
- ECHO "PythonPath=%PYTHONPATH%"
- ECHO "Path=%PATH%"
build: false
View
@@ -32,8 +32,8 @@
# Build a list of installers, one for each solver
Installer = namedtuple("Installer", ["InstallerClass", "version", "extra_params"])
INSTALLERS = [Installer(MSatInstaller, "5.3.13", {}),
Installer(Z3Installer, "4.4.1", {"osx": "10.11"}),
Installer(CVC4Installer, "1.5", {"git_version" : "05663e0d338c2bab30b5f19820de01788ec2b276"}),
Installer(Z3Installer, "4.5.1", {"osx": "10.11", "git_version": "082936bca6fb"}),
Installer(YicesInstaller, "2.5.2", {"yicespy_version": "f0768ffeec15ea310f830d10878971c9998454ac"}),
Installer(BtorInstaller, "2.4.1", {"lingeling_version": "bbc"}),
Installer(PicoSATInstaller, "965", {"pypicosat_minor_version" : "1708010052"}),
@@ -56,6 +56,9 @@ def get_requested_solvers():
def check_installed(required_solvers, install_dir, bindings_dir, mirror_link):
"""Checks which solvers are visible to pySMT."""
# Check which solvers are accessible from the Factory
pypath_solvers = get_env().factory.all_solvers()
global_solvers_status = []
print("Installed Solvers:")
for i in INSTALLERS:
@@ -70,8 +73,6 @@ def check_installed(required_solvers, install_dir, bindings_dir, mirror_link):
global_solvers_status.append((solver, is_installed, version))
del installer_
# Check which solvers are accessible from the Factory
pypath_solvers = get_env().factory.all_solvers()
for solver in required_solvers:
if solver not in pypath_solvers:
raise PysmtException("Was expecting to find %s installed" % solver)
@@ -219,8 +220,10 @@ def main():
bindings_dir= os.path.expanduser(options.bindings_path)
if platform.system().lower() == "windows":
print("set PYTHONPATH=" + bindings_dir + ";%PYTHONPATH%")
print("set PATH=" + bindings_dir + ";%PATH%")
else:
print("export PYTHONPATH=\"" + bindings_dir + ":${PYTHONPATH}\"")
print("export LD_LIBRARY_PATH=\"" + bindings_dir + ":${LD_LIBRARY_PATH}\"")
else:
if len(solvers_to_install) == 0:
@@ -90,9 +90,9 @@ def python_version(self):
def download_links(self):
if self.mirror_link is not None:
yield self.mirror_link.format(archive_name=self.archive_name)
yield self.mirror_link.format(archive_name=self.archive_name, solver_version=self.solver_version)
if self.native_link is not None:
yield self.native_link.format(archive_name=self.archive_name)
yield self.native_link.format(archive_name=self.archive_name, solver_version=self.solver_version)
def download(self):
"""Downloads the archive from one of the mirrors"""
View
@@ -25,7 +25,7 @@ class Z3Installer(SolverInstaller):
SOLVER = "z3"
def __init__(self, install_dir, bindings_dir, solver_version,
mirror_link=None, osx=None):
mirror_link=None, osx=None, git_version=None):
arch = self.architecture
if arch == "x86_64":
arch = "x64"
@@ -38,8 +38,12 @@ def __init__(self, install_dir, bindings_dir, solver_version,
elif system == "windows":
system = "win"
archive_name = "z3-%s-%s-%s.zip" % (solver_version, arch, system)
native_link = "https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/{archive_name}"
# Stable versions template
# archive_name = "z3-%s-%s-%s.zip" % (solver_version, arch, system)
#
# Nightly build template
archive_name = "z3-%s.%s-%s-%s.zip" % (solver_version, git_version, arch, system)
native_link = "https://github.com/pysmt/Z3bin/blob/master/nightly/{archive_name}?raw=true"
SolverInstaller.__init__(self, install_dir=install_dir,
bindings_dir=bindings_dir,
@@ -50,16 +54,7 @@ def __init__(self, install_dir, bindings_dir, solver_version,
def move(self):
bpath = os.path.join(self.extract_path, "bin")
files = ["z3consts.py",
"z3core.py",
"z3num.py",
"z3poly.py",
"z3printer.py",
"z3.py",
"z3rcf.py",
"z3test.py",
"z3types.py",
"z3util.py"]
files = ["python/z3"]
if self.os_name == "linux":
files += [ "libz3.so" ]
elif self.os_name == "darwin":
View
@@ -183,13 +183,13 @@ def pysmt_fraction_from_rational(value):
USE_Z3 = False
try:
import z3num
import z3.z3num
USE_Z3 = True
except ImportError:
pass
if USE_Z3:
class Numeral(z3num.Numeral):
class Numeral(z3.z3num.Numeral):
"""Represents a Number (Algebraic)"""
def __hash__(self):
return hash(self.sexpr())
View
@@ -143,7 +143,10 @@ def __init__(self, environment, logic, **options):
environment=environment,
logic=logic,
**options)
self.z3 = z3.SolverFor(str(logic))
try:
self.z3 = z3.SolverFor(str(logic))
except z3.Z3Exception:
self.z3 = z3.Solver()
self.options(self)
self.declarations = set()
self.converter = Z3Converter(environment, z3_ctx=self.z3.ctx)
@@ -902,7 +905,7 @@ def __init__(self, environment, logic=None):
QuantifierEliminator.__init__(self)
self.environment = environment
self.logic = logic
self.converter = Z3Converter(environment, z3._get_ctx(None))
self.converter = Z3Converter(environment, z3.main_ctx())
def eliminate_quantifiers(self, formula):
logic = get_logic(formula, self.environment)
@@ -918,7 +921,7 @@ def eliminate_quantifiers(self, formula):
s = simplifier(f, elim_and=True,
pull_cheap_ite=True,
ite_extra_rules=True).as_expr()
res = eliminator(s, eliminate_variables_as_block=True).as_expr()
res = eliminator(f).as_expr()
pysmt_res = None
try:
@@ -948,7 +951,7 @@ def __init__(self, environment, logic=None):
Interpolator.__init__(self)
self.environment = environment
self.logic = logic
self.converter = Z3Converter(environment, z3_ctx=z3._get_ctx(None))
self.converter = Z3Converter(environment, z3_ctx=z3.main_ctx())
def _check_logic(self, formulas):
for f in formulas:
View
@@ -99,13 +99,22 @@ def test_integer(self):
def test_div_pow(self):
x = FreshSymbol(REAL)
f = Equals(Times(Real(4), Pow(x, Real(-1))), Real(2))
self.assertTrue(is_sat(f))
try:
self.assertTrue(is_sat(f))
except SolverReturnedUnknownResultError:
pass
f = Equals(Div(Real(4), x), Real(2))
self.assertTrue(is_sat(f, solver_name="z3"))
f = Equals(Times(x, x), Real(16))
self.assertTrue(is_sat(f))
try:
self.assertTrue(is_sat(f, solver_name="z3"))
except SolverReturnedUnknownResultError:
pass
f = Equals(Times(x, x), Real(16))
try:
self.assertTrue(is_sat(f))
except SolverReturnedUnknownResultError:
pass
if __name__ == "__main__":
main()

0 comments on commit ab17a36

Please sign in to comment.