Fixed python regressions. Added missing tactic.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

scripts/mk_util.py

@@ -188,6 +188,15 @@ def set_z3py_dir(p):
     if not os.path.exists(full):
         raise MKException("Python bindings directory '%s' does not exist" % full)
     Z3PY_SRC_DIR = full
+    compileall.compile_dir(Z3PY_SRC_DIR, force=1)
+    for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(Z3PY_SRC_DIR)):
+        try:
+            os.remove('%s/%s' % (BUILD_DIR, pyc))
+        except:
+            pass
+        os.rename('%s/%s' % (Z3PY_SRC_DIR, pyc), '%s/%s' % (BUILD_DIR, pyc))
+        if is_verbose():
+            print "Generated '%s'" % pyc
     if VERBOSE:
         print "Python bindinds directory was detected."
 
@@ -703,11 +712,6 @@ def mk_install(out):
     out.write('\t@mkdir -p $(PREFIX)/lib\n')
     for c in _Components:
         c.mk_install(out)
-    compileall.compile_dir(Z3PY_SRC_DIR, force=1)
-    for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(Z3PY_SRC_DIR)):
-        os.rename('%s/%s' % (Z3PY_SRC_DIR, pyc), '%s/%s' % (BUILD_DIR, pyc))
-        if is_verbose():
-            print "Generated '%s'" % pyc
     out.write('\t@cp z3*.pyc %s\n' % PYTHON_PACKAGE_DIR)
     out.write('\t@echo Z3 was successfully installed.\n')
     out.write('\n')    

src/bindings/python/z3.py

@@ -24,7 +24,7 @@ Small example:
 >>> s.check()
 sat
 >>> s.model()
-[x = 1, y = 2]
+[y = 2, x = 1]
 
 Z3 exceptions:
 
@@ -1698,9 +1698,9 @@ def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
     >>> q
     Exists([x, y], f(x, y) >= x)
     >>> Tactic('nnf')(q)
-    [[f(x!foo!2, y!foo!1) >= x!foo!2]]
+    [[f(x!foo!1, y!foo!0) >= x!foo!1]]
     >>> Tactic('nnf')(q).as_expr()
-    f(x!foo!4, y!foo!3) >= x!foo!4
+    f(x!foo!3, y!foo!2) >= x!foo!3
     """
     return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
 
@@ -6908,7 +6908,7 @@ def solve(*args, **keywords):
     
     >>> a, b = Ints('a b')
     >>> solve(a + b == 3, Or(a == 0, a == 1), a != 0)
-    [a = 1, b = 2]
+    [b = 2, a = 1]
     """
     s = Solver()
     s.set(**keywords)

src/tactic/core/propagate_values_tactic.h

@@ -27,7 +27,7 @@ class tactic;
 tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p = params_ref());
 
 /*
-    ADD_TACTIC_CMD("propagate-values", "propagate constants.", "mk_propagate_values_tactic(m, p)")
+  ADD_TACTIC("propagate-values", "propagate constants.", "mk_propagate_values_tactic(m, p)")
 */
 
 #endif