Added C# testing functions and first regressions.

Signed-off-by: Christoph M. Wintersteiger <[email protected]>

old-regressions/cs/arith.1.cs → regressions/cs/arith.1.cs

@@ -19,8 +19,9 @@ public void Run()
  IntExpr s, r;
  s = ctx.MkIntConst("s");
  r = ctx.MkIntConst("r");
- Console.WriteLine(ctx.MkAdd(x, ctx.MkInt2Real(y), ctx.MkReal(1), ctx.MkAdd(a, ctx.MkInt2Real(s))));
- Console.WriteLine(ctx.MkAdd(ctx.MkInt2Real(y), c));
+ TestDriver.CheckString(ctx.MkAdd(x, ctx.MkInt2Real(y), ctx.MkReal(1), ctx.MkAdd(a, ctx.MkInt2Real(s))),
+ "(+ x (to_real y) 1.0 a (to_real s))");
+ TestDriver.CheckString(ctx.MkAdd(ctx.MkInt2Real(y), c), "(+ (to_real y) c)");
  }
  }
 }

old-regressions/cs/bit.1.cs → regressions/cs/bit.1.cs

@@ -25,16 +25,15 @@ public void Run()
  foreach (BitVecExpr p in powers)
  slow = ctx.MkOr(slow, ctx.MkEq(x, p));
 
-  Console.WriteLine(fast);
+  TestDriver.CheckString(fast, "(and (not (= x #x00000000)) (= (bvand x (bvsub x #x00000001)) #x00000000))");
 
  Solver s = ctx.MkSolver();
  s.Assert(ctx.MkNot(ctx.MkEq(fast, slow)));
- Console.WriteLine(s.Check());
+ TestDriver.CheckUNSAT(s.Check());
 
- Console.WriteLine("buggy version");
  s = ctx.MkSolver();
  s.Assert(ctx.MkNot(step_zero));
- Console.WriteLine(s.Check());
+ TestDriver.CheckSAT(s.Check());
  }
  }
 }

regressions/cs/driver.cs

@@ -0,0 +1,45 @@
+using Microsoft.Z3;
+using System;
+
+class TestDriver
+{
+ class TestFailedException : Exception
+ {
+ public TestFailedException() : base() { }
+ public TestFailedException(string s) : base(s) { }
+ }
+
+ public static void CheckString(Expr e, string s)
+ {
+ if (e.ToString() != s)
+ throw new TestFailedException("strings don't match");
+ }
+
+ public static void CheckSAT(Status s)
+ {
+ if (s != Status.SATISFIABLE)
+ throw new TestFailedException("result was not SATISFIABLE");
+ }
+
+ public static void CheckUNSAT(Status s)
+ {
+ if (s != Status.UNSATISFIABLE)
+ throw new TestFailedException("result was not UNSATISFIABLE");
+ }
+
+ public static int Main()
+ {
+ try
+ {
+ Test test = new Test();
+ test.Run();
+ }
+ catch (Exception e)
+ {
+ Console.WriteLine("Test failed; Exception: " + e.Message);
+ return 1;
+ }
+
+ return 0;
+ }
+}

scripts/bigtest.py

@@ -25,6 +25,8 @@ def bigtest():
  util.test_benchmarks_using_latest('regressions/smt2-debug', branch=b, debug=d, clang=c)
  util.test_benchmarks_using_latest('regressions/smt2-extra', branch=b, debug=d, clang=c)
  util.test_pyscripts_using_latest('regressions/python', branch=b, debug=d, clang=c)
+ if util.is_windows():
+ util.test_cs_using_latest('regressions/cs', branch=b, debug=d, clang=False)
  util.buildz3(branch='mcsat', everything=True, clean=True, debug=True, java=False, static=False, jobs=config.NUMJOBS, clang=False)
  util.test_pyscripts_using_latest('regressions/mcsat', branch='mcsat', debug=True, clang=False)
  # util.test_benchmarks_using_latest('regressions/smt2', branch='mcsat', debug=True, clang=False)

scripts/config.py

@@ -17,3 +17,7 @@
 JAVA="java"
 BUILDDIR="build"
 
+# C#
+CSC="csc.exe"
+CSDRIVER="driver.cs"
+CSTEMP="cstest.exe"

scripts/smalltest.py

@@ -17,7 +17,9 @@ def smalltest(b="unstable"):
  util.test_benchmarks_using_latest('regressions/smt2-debug', branch=b, debug=d, clang=False)
  util.test_benchmarks_using_latest('regressions/smt2', branch=b, debug=d, clang=False)
  util.test_pyscripts_using_latest('regressions/python', branch=b, debug=d, clang=False)
-
+ if util.is_windows():
+ util.test_cs_using_latest('regressions/cs', branch=b, debug=d, clang=False)
+
 if __name__ == "__main__":
  smalltest()
  exit(0)

scripts/test_cs.py

@@ -0,0 +1,5 @@
+from util import *
+import sys
+# Usage: z3-lib-dir benchmark-dir
+test_cs(sys.argv[1], sys.argv[2], ext="cs", timeout_duration=60.0)
+exit(0)

scripts/util.py

@@ -308,6 +308,62 @@ def test_pyscripts_using_latest(scriptdir, branch="unstable", debug=True, clang=
  bdir = get_builddir(branch, debug, clang)
  test_pyscripts(os.path.join(z3dir, bdir), scriptdir, ext, timeout_duration)
 
+def exec_cs_compile(args):
+ if subprocess.call(args) != 0:
+ raise Exception("Compilation of '%s' failed" % file)
+ return True
+
+def exec_cs():
+ if subprocess.call(config.CSTEMP) != 0:
+ raise Exception("Execution of '%s' failed" % (config.CSTEMP))
+ return True
+
+def test_cs(z3libdir, csdir, ext="cs", VS64=False, timeout_duration=60.0):
+ print "Testing C# at", csdir, "using", z3libdir
+ error = False
+ platform_arg = "/platform:x86"
+ if VS64:
+ platform_arg = "/platform:x64"
+ shutil.copyfile("%s/Microsoft.Z3.dll" % z3libdir, "Microsoft.Z3.dll")
+ with setenv('PATH', os.getenv("PATH") + ";" + z3libdir):
+ for file in filter(lambda f: f.endswith(ext), os.listdir(csdir)):
+ if file == config.CSDRIVER:
+ continue
+ file = os.path.join(csdir, file)
+ print "Testing", file
+ try:
+ # Compile.
+ if timeout(exec_cs_compile,
+ args=[[config.CSC, "/nologo", 
+ "/reference:%s\Microsoft.Z3.dll" % z3libdir, 
+ "/out:%s" % (config.CSTEMP), 
+ platform_arg, 
+ "%s\%s" % (csdir, config.CSDRIVER), 
+ file]],
+ timeout_duration=timeout_duration,
+ default=False) == False:
+ raise Exception("Timeout compiling '%s' at '%s' using '%s'" % (file, csdir, z3libdir))
+ # Run.
+ if timeout(exec_cs,
+ args=[],
+ timeout_duration=timeout_duration,
+ default=False) == False:
+ raise Exception("Timeout executing '%s' at '%s' using '%s'" % (file, csdir, z3libdir)) 
+ except Exception as ex:
+ print "Failed"
+ print ex
+ error = True
+ os.remove(config.CSTEMP)
+ os.remove("Microsoft.Z3.dll")
+ if error:
+ raise Exception("Found errors testing C# at '%s' using '%s'" % (csdir, z3libdir))
+
+
+def test_cs_using_latest(csdir, branch="unstable", debug=True, clang=False, ext="cs", VS64=False, timeout_duration=60.0):
+ z3dir = find_z3depot()
+ bdir = get_builddir(branch, debug, clang)
+ test_cs(os.path.join(z3dir, bdir), csdir, ext, VS64, timeout_duration)
+
 # buildz3(java=True, everything=True)
 # testjavaex() 
 # testz3ex('cpp_example', "unstable", True, True)

scripts/win64test.py

@@ -19,6 +19,7 @@ def win64test(b="unstable"):
  if d:
  util.test_benchmarks_using_latest('regressions/smt2-debug', branch=b, debug=d, clang=False)
  util.test_pyscripts_using_latest('regressions/python', branch=b, debug=d, clang=False)
+ util.test_cs_using_latest('regressions/python', branch=b, debug=d, VS64=True, clang=False)
 
 if __name__ == "__main__":
  win64test()