From ffb1fc37dfa5ce4b9608b5e0c881f3dde113b184 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 25 Feb 2013 15:37:33 +0000 Subject: [PATCH 1/7] Java API: New JDK detection routines. Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 190 ++++++++++++++++++++++----------------------- 1 file changed, 94 insertions(+), 96 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 5d2fb4e17..c70b1d527 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -30,13 +30,12 @@ CC=getenv("CC", None) CPPFLAGS=getenv("CPPFLAGS", "") CXXFLAGS=getenv("CXXFLAGS", "") LDFLAGS=getenv("LDFLAGS", "") -JAVA=getenv("JAVA", "java") -JAVAC=getenv("JAVAC", "javac") -JAVA_HOME=getenv("JAVA_HOME", None) +JDK_HOME=getenv("JDK_HOME", None) JNI_HOME=getenv("JNI_HOME", None) CXX_COMPILERS=['g++', 'clang++'] C_COMPILERS=['gcc', 'clang'] +JAVAC=None PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib() BUILD_DIR='build' REV_BUILD_DIR='..' @@ -207,24 +206,6 @@ def test_openmp(cc): t.commit() return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0 -def check_java(): - t = TempFile('Hello.java') - t.add('public class Hello { public static void main(String[] args) { System.out.println("Hello, World"); }}\n') - t.commit() - if is_verbose(): - print("Testing %s..." % JAVAC) - r = exec_cmd([JAVAC, 'Hello.java']) - if r != 0: - raise MKException('Failed testing Java compiler. Set environment variable JAVAC with the path to the Java compiler') - if is_verbose(): - print("Testing %s..." % JAVA) - r = exec_cmd([JAVA, 'Hello']) - rmf('Hello.class') - if r != 0: - raise MKException('Failed testing Java program. Set environment variable JAVA with the path to the Java virtual machine') - find_java_home() - find_jni_home() - def find_jni_h(path): for root, dirs, files in os.walk(path): for f in files: @@ -232,76 +213,97 @@ def find_jni_h(path): return root return False -def find_java_home(): - global JAVA_HOME - if JAVA_HOME != None: - if IS_WINDOWS: - ind = '%s%s' % (JAVA_HOME, '\\bin\\java.exe') - else: - ind = '%s%s' % (JAVA_HOME, '/bin/java') - if not os.path.exists(ind): - raise MKException("Failed to detect java at '%s'.Possible solution: set JAVA_HOME with the path to JDK." % os.path.join(JAVA_HOME)) - else: - return - if is_verbose(): - print("Finding JAVA_HOME...") - t = TempFile('output') - null = open(os.devnull, 'wb') - try: - subprocess.call([JAVA, '-verbose'], stdout=t.fname, stderr=null) - t.commit() - except: - raise MKException('Failed to find JAVA_HOME') - open_pat = re.compile("\[Opened (.*)\]") - t = open('output', 'r') - for line in t: - m = open_pat.match(line) - if m: - # Remove last 3 directives from m.group(1) - tmp = m.group(1).split(os.sep) - path = string.join(tmp[:len(tmp) - 3], os.sep) - if IS_WINDOWS: - ind = '%s%s' % (path, '\\bin\\java.exe') - else: - ind = '%s%s' % (path, '/bin/java') - if os.path.exists(ind): - JAVA_HOME = path - return - if IS_OSX: - path = '%s%s' % (path, '/Contents/Home/') - ind = '%s%s' % (path, 'bin/java') - if os.path.exists(ind): - JAVA_HOME = path - return - raise MKException("Failed to detect java at '%s'.Possible solution: set JAVA_HOME with the path to JDK." % os.path.join(path)) - return - raise MKException('Failed to find JAVA_HOME') - -def find_jni_home(): +def check_java(): + global JDK_HOME global JNI_HOME - if JNI_HOME != None: - if is_verbose(): - print("Checking jni.h...") - path = JNI_HOME - fn = os.path.join(path, 'jni.h') - print("Checking for jni.h in %s..." % JNI_HOME) - if os.path.exists(fn): - return + global JAVAC + + if is_verbose(): + print("Finding JDK_HOME...") + + if JDK_HOME != None: + if IS_WINDOWS: + JAVAC = os.path.join(JDK_HOME, 'bin', 'javac.exe') + else: + JAVAC = os.path.join(JDK_HOME, 'bin', 'javac') + + if not os.path.exists(JAVAC): + raise MKException("Failed to detect javac at '%s/bin'; the environment variable JDK_HOME is probably set to the wrong path." % os.path.join(JDK_HOME)) else: - path = '%s%s' % (JAVA_HOME, '/include/') - fn = '%s%s' % (path, 'jni.h') - print("Checking for jni.h in %s..." % path) - if os.path.exists(fn): - JNI_HOME = find_jni_h(path) - elif IS_OSX: - # Apparently Apple knows best where to put stuff... - path = '/System/Library/Frameworks/JavaVM.framework/Headers/' - fn = '%s%s' % (path, 'jni.h') - print("Checking for jni.h in %s..." % path) - if os.path.exists(fn): - JNI_HOME = find_jni_h(path) - if JNI_HOME == None: - raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.") + # Search for javac in the path. + ind = 'javac'; + if IS_WINDOWS: + ind = ind + '.exe' + paths = os.getenv('path', None) + spaths = paths.split(os.pathsep) + for i in range(0, len(spaths)): + cmb = os.path.join(spaths[i], ind) + if os.path.exists(cmb): + JAVAC = cmb + break + + if JAVAC == None: + raise MKException('No java compiler in the path, please adjust your PATH or set JDK_HOME to the location of the JDK.') + + if is_verbose(): + print("Testing %s..." % JAVAC) + + t = TempFile('Hello.java') + t.add('public class Hello { public static void main(String[] args) { System.out.println("Hello, World"); }}\n') + t.commit() + + oo = TempFile('output') + eo = TempFile('errout') + try: + subprocess.call([JAVAC, 'Hello.java', '-verbose'], stdout=oo.fname, stderr=eo.fname) + oo.commit() + eo.commit() + except: + raise MKException('Found, but failed to run Java compiler at %s' % (JAVAC)) + + os.remove('Hello.class') + + if is_verbose(): + print("Finding jni.h...") + + if JNI_HOME != None: + if not os.path.exists(path.join(JNI_HOME, 'jni.h')): + raise MKException("Failed to detect jni.h '%s'; the environment variable JNI_HOME is probably set to the wrong path." % os.path.join(JNI_HOME)) + else: + # Search for jni.h in the library directories... + t = open('errout', 'r') + open_pat = re.compile("\[search path for class files: (.*)\]") + cdirs = [] + for line in t: + m = open_pat.match(line) + if m: + libdirs = m.group(1).split(',') + for libdir in libdirs: + q = os.path.dirname(libdir) + if cdirs.count(q) == 0: + cdirs.append(q) + + # ... plus some heuristic ones. + extra_dirs = [] + + # For the libraries, even the JDK usually uses a JRE that comes with it. To find the + # headers we have to go a little bit higher up. + for dir in cdirs: + extra_dirs.append(os.path.abspath(os.path.join(dir, '..'))) + + if IS_OSX: # Apparently Apple knows best where to put stuff... + extra_dirs.append('/System/Library/Frameworks/JavaVM.framework/Headers/') + + cdirs[len(cdirs):] = extra_dirs + + for dir in cdirs: + print dir + q = find_jni_h(dir) + if q != False: + JNI_HOME = q + + if JNI_HOME == None: + raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.") def is64(): return sys.maxsize >= 2**32 @@ -436,9 +438,7 @@ def display_help(exit_code): print(" LDFLAGS Linker flags, e.g., -L if you have libraries in a non-standard directory") print(" CPPFLAGS Preprocessor flags, e.g., -I if you have header files in a non-standard directory") print(" CXXFLAGS C++ compiler flags") - print(" JAVA Java virtual machine (only relevant if -j or --java option is provided)") - print(" JAVAC Java compiler (only relevant if -j or --java option is provided)") - print(" JAVA_HOME JDK installation directory (only relevant if -j or --java option is provided)") + print(" JDK_HOME JDK installation directory (only relevant if -j or --java option is provided)") print(" JNI_HOME JNI bindings directory (only relevant if -j or --java option is provided)") exit(exit_code) @@ -1425,10 +1425,9 @@ def mk_config(): if is_verbose(): print('64-bit: %s' % is64()) if is_java_enabled(): - print('Java Home: %s' % JAVA_HOME) + print('JDK Home: %s' % JDK_HOME) print('JNI Home: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) - print('Java VM: %s' % JAVA) else: global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS ARITH = "internal" @@ -1530,10 +1529,9 @@ def mk_config(): print('gprof: enabled') print('Python version: %s' % distutils.sysconfig.get_python_version()) if is_java_enabled(): - print('Java Home: %s' % JAVA_HOME) + print('JDK Home: %s' % JDK_HOME) print('JNI Home: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) - print('Java VM: %s' % JAVA) def mk_install(out): out.write('install:\n') From f5cdc14737b9ef3e23eb7754eee4e78637d942a6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 25 Feb 2013 15:44:54 +0000 Subject: [PATCH 2/7] Java API: build system bugfixes Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 28 +++++++++++++--------------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index c70b1d527..5b41eced4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -30,7 +30,6 @@ CC=getenv("CC", None) CPPFLAGS=getenv("CPPFLAGS", "") CXXFLAGS=getenv("CXXFLAGS", "") LDFLAGS=getenv("LDFLAGS", "") -JDK_HOME=getenv("JDK_HOME", None) JNI_HOME=getenv("JNI_HOME", None) CXX_COMPILERS=['g++', 'clang++'] @@ -214,12 +213,13 @@ def find_jni_h(path): return False def check_java(): - global JDK_HOME global JNI_HOME global JAVAC + + JDK_HOME = getenv('JDK_HOME', None) # we only need to check this locally. if is_verbose(): - print("Finding JDK_HOME...") + print("Finding javac ...") if JDK_HOME != None: if IS_WINDOWS: @@ -234,13 +234,14 @@ def check_java(): ind = 'javac'; if IS_WINDOWS: ind = ind + '.exe' - paths = os.getenv('path', None) - spaths = paths.split(os.pathsep) - for i in range(0, len(spaths)): - cmb = os.path.join(spaths[i], ind) - if os.path.exists(cmb): - JAVAC = cmb - break + paths = os.getenv('PATH', None) + if paths: + spaths = paths.split(os.pathsep) + for i in range(0, len(spaths)): + cmb = os.path.join(spaths[i], ind) + if os.path.exists(cmb): + JAVAC = cmb + break if JAVAC == None: raise MKException('No java compiler in the path, please adjust your PATH or set JDK_HOME to the location of the JDK.') @@ -297,7 +298,6 @@ def check_java(): cdirs[len(cdirs):] = extra_dirs for dir in cdirs: - print dir q = find_jni_h(dir) if q != False: JNI_HOME = q @@ -1425,8 +1425,7 @@ def mk_config(): if is_verbose(): print('64-bit: %s' % is64()) if is_java_enabled(): - print('JDK Home: %s' % JDK_HOME) - print('JNI Home: %s' % JNI_HOME) + print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) else: global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS @@ -1529,8 +1528,7 @@ def mk_config(): print('gprof: enabled') print('Python version: %s' % distutils.sysconfig.get_python_version()) if is_java_enabled(): - print('JDK Home: %s' % JDK_HOME) - print('JNI Home: %s' % JNI_HOME) + print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) def mk_install(out): From 14f582eca5f1429d145a3794d69fa9d6c213ac2d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 25 Feb 2013 16:03:57 +0000 Subject: [PATCH 3/7] Java API: added automatic detection of jar Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 5b41eced4..09aada950 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -35,6 +35,7 @@ JNI_HOME=getenv("JNI_HOME", None) CXX_COMPILERS=['g++', 'clang++'] C_COMPILERS=['gcc', 'clang'] JAVAC=None +JAR=None PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib() BUILD_DIR='build' REV_BUILD_DIR='..' @@ -215,6 +216,7 @@ def find_jni_h(path): def check_java(): global JNI_HOME global JAVAC + global JAR JDK_HOME = getenv('JDK_HOME', None) # we only need to check this locally. @@ -246,6 +248,17 @@ def check_java(): if JAVAC == None: raise MKException('No java compiler in the path, please adjust your PATH or set JDK_HOME to the location of the JDK.') + if is_verbose(): + print("Finding jar ...") + + if IS_WINDOWS: + JAR = os.path.join(os.path.dirname(JAVAC), 'jar.exe') + else: + JAR = os.path.join(os.path.dirname(JAVAC), 'jar') + + if not os.path.exists(JAR): + raise MKException("Failed to detect jar at '%s'; the environment variable JDK_HOME is probably set to the wrong path." % os.path.join(JDK_HOME)) + if is_verbose(): print("Testing %s..." % JAVAC) @@ -1120,6 +1133,9 @@ class JavaDLLComponent(Component): self.manifest_file = manifest_file def mk_makefile(self, out): + global JAVAC + global JAR + if is_java_enabled(): mk_dir(os.path.join(BUILD_DIR, 'api', 'java', 'classes')) dllfile = '%s$(SO_EXT)' % self.dll_name @@ -1146,6 +1162,9 @@ class JavaDLLComponent(Component): deps += '%s ' % os.path.join(self.to_src_dir, 'enumerations', jfile) out.write(deps) out.write('\n') + if IS_WINDOWS: + JAVAC = '"%s"' % JAVAC + JAR = '"%s"' % JAR t = ('\t%s %s.java -d %s\n' % (JAVAC, os.path.join(self.to_src_dir, 'enumerations', '*'), os.path.join('api', 'java', 'classes'))) out.write(t) t = ('\t%s -cp %s %s.java -d %s\n' % (JAVAC, @@ -1153,7 +1172,7 @@ class JavaDLLComponent(Component): os.path.join(self.to_src_dir, '*'), os.path.join('api', 'java', 'classes'))) out.write(t) - out.write('\tjar cfm %s.jar %s -C %s .\n' % (self.package_name, + out.write('\t%s cfm %s.jar %s -C %s .\n' % (JAR, self.package_name, os.path.join(self.to_src_dir, 'manifest'), os.path.join('api', 'java', 'classes'))) out.write('java: %s.jar\n\n' % self.package_name) From b2810592e6bbd84c521b821a47fd0f33c75f4a96 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Feb 2013 08:29:01 -0800 Subject: [PATCH 4/7] Add enumeration_sort method to C++ API. Add as_expr method to goal class in C++ API. Add enum_sort_example to C++ examples/c++/example.cpp Signed-off-by: Leonardo de Moura --- examples/c++/example.cpp | 24 ++++++++++++++++++++ src/api/c++/z3++.h | 48 +++++++++++++++++++++++++++++++++++----- 2 files changed, 66 insertions(+), 6 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 1f127e8e4..ab5d0132c 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -883,6 +883,29 @@ void incremental_example3() { std::cout << s.check(a2) << "\n"; } +void enum_sort_example() { + std::cout << "enumeration sort example\n"; + context ctx; + const char * enum_names[] = { "a", "b", "c" }; + func_decl_vector enum_consts(ctx); + func_decl_vector enum_testers(ctx); + sort s = ctx.enumeration_sort("enumT", 3, enum_names, enum_consts, enum_testers); + // enum_consts[0] is a func_decl of arity 0. + // we convert it to an expression using the operator() + expr a = enum_consts[0](); + expr b = enum_consts[1](); + expr x = ctx.constant("x", s); + expr test = (x==a) && (x==b); + std::cout << "1: " << test << std::endl; + tactic qe(ctx, "ctx-solver-simplify"); + goal g(ctx); + g.add(test); + expr res(ctx); + apply_result result_of_elimination = qe.apply(g); + goal result_goal = result_of_elimination[0]; + std::cout << "2: " << result_goal.as_expr() << std::endl; +} + int main() { try { demorgan(); std::cout << "\n"; @@ -917,6 +940,7 @@ int main() { incremental_example1(); std::cout << "\n"; incremental_example2(); std::cout << "\n"; incremental_example3(); std::cout << "\n"; + enum_sort_example(); std::cout << "\n"; std::cout << "done\n"; } catch (exception & ex) { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 5af4bf60b..3382b8b00 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -63,6 +63,11 @@ namespace z3 { class statistics; class apply_result; class fixedpoint; + template class ast_vector_tpl; + typedef ast_vector_tpl ast_vector; + typedef ast_vector_tpl expr_vector; + typedef ast_vector_tpl sort_vector; + typedef ast_vector_tpl func_decl_vector; inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); } inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); } @@ -190,7 +195,13 @@ namespace z3 { Example: Given a context \c c, c.array_sort(c.int_sort(), c.bool_sort()) is an array sort from integer to Boolean. */ sort array_sort(sort d, sort r); - + /** + \brief Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. + \c cs and \c ts are output parameters. The method stores in \c cs the constants corresponding to the enumerated elements, + and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration. + */ + sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts); + func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range); func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range); func_decl function(char const * name, sort const & domain, sort const & range); @@ -414,6 +425,7 @@ namespace z3 { bool is_const() const { return arity() == 0; } + expr operator()() const; expr operator()(unsigned n, expr const * args) const; expr operator()(expr const & a) const; expr operator()(int a) const; @@ -1020,11 +1032,6 @@ namespace z3 { friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; } }; - typedef ast_vector_tpl ast_vector; - typedef ast_vector_tpl expr_vector; - typedef ast_vector_tpl sort_vector; - typedef ast_vector_tpl func_decl_vector; - class func_entry : public object { Z3_func_entry m_entry; void init(Z3_func_entry e) { @@ -1261,6 +1268,19 @@ namespace z3 { unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); } bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; } bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; } + expr as_expr() const { + unsigned n = size(); + if (n == 0) + return ctx().bool_val(false); + else if (n == 1) + return operator[](0); + else { + array args(n); + for (unsigned i = 0; i < n; i++) + args[i] = operator[](i); + return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr())); + } + } friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; } }; @@ -1437,6 +1457,17 @@ namespace z3 { inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); } inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); } inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); } + inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) { + array _enum_names(n); + for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); } + array _cs(n); + array _ts(n); + Z3_symbol _name = Z3_mk_string_symbol(*this, name); + sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr())); + check_error(); + for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); } + return s; + } inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) { array args(arity); @@ -1538,6 +1569,11 @@ namespace z3 { return expr(ctx(), r); } + inline expr func_decl::operator()() const { + Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0); + ctx().check_error(); + return expr(ctx(), r); + } inline expr func_decl::operator()(expr const & a) const { check_context(*this, a); Z3_ast args[1] = { a }; From 5fe58c2f2db10b864b21f53df1b9bbbda0d1d6a0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 26 Feb 2013 19:13:48 +0000 Subject: [PATCH 5/7] Java API: renamed assert_(...) to add(...) .NET API: added alias Add(...) for Assert(...) Signed-off-by: Christoph M. Wintersteiger --- examples/java/JavaExample.java | 80 +++++++++++++++++----------------- src/api/dotnet/Fixedpoint.cs | 8 ++++ src/api/dotnet/Goal.cs | 8 ++++ src/api/dotnet/Solver.cs | 8 ++++ src/api/java/Fixedpoint.java | 2 +- src/api/java/Goal.java | 2 +- src/api/java/Solver.java | 2 +- 7 files changed, 67 insertions(+), 43 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index c2743ece8..48395d8c2 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -197,7 +197,7 @@ class JavaExample TestFailedException { Solver s = ctx.mkSolver(); - s.assert_(f); + s.add(f); if (s.check() != sat) throw new TestFailedException(); if (sat == Status.SATISFIABLE) @@ -213,7 +213,7 @@ class JavaExample System.out.println("\nTactical solver: " + s); for (BoolExpr a : g.getFormulas()) - s.assert_(a); + s.add(a); System.out.println("Solver: " + s); if (s.check() != sat) @@ -266,8 +266,8 @@ class JavaExample p.add("mbqi", useMBQI); s.setParameters(p); for (BoolExpr a : assumptions) - s.assert_(a); - s.assert_(ctx.mkNot(f)); + s.add(a); + s.add(ctx.mkNot(f)); Status q = s.check(); switch (q) @@ -299,8 +299,8 @@ class JavaExample p.add("mbqi", useMBQI); s.setParameters(p); for (BoolExpr a : assumptions) - s.assert_(a); - s.assert_(ctx.mkNot(f)); + s.add(a); + s.add(ctx.mkNot(f)); Status q = s.check(); switch (q) @@ -326,9 +326,9 @@ class JavaExample ArithExpr yr = (ArithExpr) ctx.mkConst(ctx.mkSymbol("y"), ctx.mkRealSort()); Goal g4 = ctx.mkGoal(true, false, false); - g4.assert_(ctx.mkGt(xr, ctx.mkReal(10, 1))); - g4.assert_(ctx.mkEq(yr, ctx.mkAdd(xr, ctx.mkReal(1, 1)))); - g4.assert_(ctx.mkGt(yr, ctx.mkReal(1, 1))); + g4.add(ctx.mkGt(xr, ctx.mkReal(10, 1))); + g4.add(ctx.mkEq(yr, ctx.mkAdd(xr, ctx.mkReal(1, 1)))); + g4.add(ctx.mkGt(yr, ctx.mkReal(1, 1))); ApplyResult ar = applyTactic(ctx, ctx.mkTactic("simplify"), g4); if (ar.getNumSubgoals() == 1 @@ -345,7 +345,7 @@ class JavaExample Solver s = ctx.mkSolver(); for (BoolExpr e : ar.getSubgoals()[0].getFormulas()) - s.assert_(e); + s.add(e); Status q = s.check(); System.out.println("Solver says: " + q); System.out.println("Model: \n" + s.getModel()); @@ -367,7 +367,7 @@ class JavaExample ctx.mkBitVecSort(32)); ArrayExpr aex = (ArrayExpr) ctx.mkConst(ctx.mkSymbol("MyArray"), asort); Expr sel = ctx.mkSelect(aex, ctx.mkInt(0)); - g.assert_(ctx.mkEq(sel, ctx.mkBV(42, 32))); + g.add(ctx.mkEq(sel, ctx.mkBV(42, 32))); Symbol xs = ctx.mkSymbol("x"); IntExpr xc = (IntExpr) ctx.mkConst(xs, ctx.getIntSort()); @@ -377,11 +377,11 @@ class JavaExample Expr[] fargs = { ctx.mkConst(xs, ctx.getIntSort()) }; IntExpr fapp = (IntExpr) ctx.mkApp(fd, fargs); - g.assert_(ctx.mkEq(ctx.mkAdd(xc, fapp), ctx.mkInt(123))); + g.add(ctx.mkEq(ctx.mkAdd(xc, fapp), ctx.mkInt(123))); Solver s = ctx.mkSolver(); for (BoolExpr a : g.getFormulas()) - s.assert_(a); + s.add(a); System.out.println("Solver: " + s); Status q = s.check(); @@ -574,8 +574,8 @@ class JavaExample ctx.mkEq(X[i][j], ctx.mkInt(instance[i][j])))); Solver s = ctx.mkSolver(); - s.assert_(sudoku_c); - s.assert_(instance_c); + s.add(sudoku_c); + s.add(instance_c); if (s.check() == Status.SATISFIABLE) { @@ -798,14 +798,14 @@ class JavaExample BoolExpr nontrivial_eq = ctx.mkEq(fapp, fapp2); Goal g = ctx.mkGoal(true, false, false); - g.assert_(trivial_eq); - g.assert_(nontrivial_eq); + g.add(trivial_eq); + g.add(nontrivial_eq); System.out.println("Goal: " + g); Solver solver = ctx.mkSolver(); for (BoolExpr a : g.getFormulas()) - solver.assert_(a); + solver.add(a); if (solver.check() != Status.SATISFIABLE) throw new TestFailedException(); @@ -820,7 +820,7 @@ class JavaExample if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat()) throw new TestFailedException(); - g.assert_(ctx.mkEq(ctx.mkNumeral(1, ctx.mkBitVecSort(32)), + g.add(ctx.mkEq(ctx.mkNumeral(1, ctx.mkBitVecSort(32)), ctx.mkNumeral(2, ctx.mkBitVecSort(32)))); ar = applyTactic(ctx, ctx.mkTactic("smt"), g); if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat()) @@ -832,7 +832,7 @@ class JavaExample throw new TestFailedException(); g2 = ctx.mkGoal(true, true, false); - g2.assert_(ctx.mkFalse()); + g2.add(ctx.mkFalse()); ar = applyTactic(ctx, ctx.mkTactic("smt"), g2); if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat()) throw new TestFailedException(); @@ -840,10 +840,10 @@ class JavaExample Goal g3 = ctx.mkGoal(true, true, false); Expr xc = ctx.mkConst(ctx.mkSymbol("x"), ctx.getIntSort()); Expr yc = ctx.mkConst(ctx.mkSymbol("y"), ctx.getIntSort()); - g3.assert_(ctx.mkEq(xc, ctx.mkNumeral(1, ctx.getIntSort()))); - g3.assert_(ctx.mkEq(yc, ctx.mkNumeral(2, ctx.getIntSort()))); + g3.add(ctx.mkEq(xc, ctx.mkNumeral(1, ctx.getIntSort()))); + g3.add(ctx.mkEq(yc, ctx.mkNumeral(2, ctx.getIntSort()))); BoolExpr constr = ctx.mkEq(xc, yc); - g3.assert_(constr); + g3.add(constr); ar = applyTactic(ctx, ctx.mkTactic("smt"), g3); if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat()) throw new TestFailedException(); @@ -1110,13 +1110,13 @@ class JavaExample // Use a solver for QF_BV Solver s = ctx.mkSolver("QF_BV"); - s.assert_(eq); + s.add(eq); Status res = s.check(); System.out.println("solver result: " + res); // Or perhaps a tactic for QF_BV Goal g = ctx.mkGoal(true, false, false); - g.assert_(eq); + g.add(eq); Tactic t = ctx.mkTactic("qfbv"); ApplyResult ar = t.apply(g); @@ -1139,7 +1139,7 @@ class JavaExample BoolExpr q = ctx.mkEq(x, y); Goal g = ctx.mkGoal(true, false, false); - g.assert_(q); + g.add(q); Tactic t1 = ctx.mkTactic("qfbv"); Tactic t2 = ctx.mkTactic("qfbv"); @@ -1341,7 +1341,7 @@ class JavaExample /* assert x >= "big number" */ BoolExpr c1 = ctx.mkGe(x, big_number); System.out.println("assert: x >= 'big number'"); - solver.assert_(c1); + solver.add(c1); /* create a backtracking point */ System.out.println("push"); @@ -1350,7 +1350,7 @@ class JavaExample /* assert x <= 3 */ BoolExpr c2 = ctx.mkLe(x, three); System.out.println("assert: x <= 3"); - solver.assert_(c2); + solver.add(c2); /* context is inconsistent at this point */ if (solver.check() != Status.UNSATISFIABLE) @@ -1375,7 +1375,7 @@ class JavaExample /* assert y > x */ BoolExpr c3 = ctx.mkGt(y, x); System.out.println("assert: y > x"); - solver.assert_(c3); + solver.add(c3); /* the context is still consistent. */ if (solver.check() != Status.SATISFIABLE) @@ -1911,10 +1911,10 @@ class JavaExample Solver solver = ctx.mkSolver(); /* assert x < y */ - solver.assert_(ctx.mkLt(x, y)); + solver.add(ctx.mkLt(x, y)); /* assert x > 2 */ - solver.assert_(ctx.mkGt(x, two)); + solver.add(ctx.mkGt(x, two)); /* find model for the constraints above */ Model model = null; @@ -1964,9 +1964,9 @@ class JavaExample Solver solver = ctx.mkSolver(); /* assert tup1 != tup2 */ - solver.assert_(ctx.mkNot(ctx.mkEq(tup1, tup2))); + solver.add(ctx.mkNot(ctx.mkEq(tup1, tup2))); /* assert first tup1 = first tup2 */ - solver.assert_(ctx.mkEq(ctx.mkApp(first, tup1), ctx.mkApp(first, tup2))); + solver.add(ctx.mkEq(ctx.mkApp(first, tup1), ctx.mkApp(first, tup2))); /* find model for the constraints above */ Model model = null; @@ -2014,7 +2014,7 @@ class JavaExample // Assert all feasible bounds. for (int i = 0; i < num_Exprs; ++i) { - solver.assert_(ctx.mkBVULE(to_minimize[i], + solver.add(ctx.mkBVULE(to_minimize[i], ctx.mkBV(upper[i], 32))); } @@ -2050,7 +2050,7 @@ class JavaExample { last_upper = (upper[i] + lower[i]) / 2; last_index = i; - solver.assert_(ctx.mkBVULE(to_minimize[i], + solver.add(ctx.mkBVULE(to_minimize[i], ctx.mkBV(last_upper, 32))); some_work = true; break; @@ -2074,7 +2074,7 @@ class JavaExample Solver solver = ctx.mkSolver(); - solver.assert_(ctx.mkBVULE(x, ctx.mkBVAdd(y, z))); + solver.add(ctx.mkBVULE(x, ctx.mkBVAdd(y, z))); checkSmall(ctx, solver, x, y, z); } @@ -2120,10 +2120,10 @@ class JavaExample BoolExpr f3 = ctx.mkOr(ctx.mkNot(pa), ctx.mkNot(pc)); BoolExpr f4 = pd; - solver.assert_(ctx.mkOr(f1, p1)); - solver.assert_(ctx.mkOr(f2, p2)); - solver.assert_(ctx.mkOr(f3, p3)); - solver.assert_(ctx.mkOr(f4, p4)); + solver.add(ctx.mkOr(f1, p1)); + solver.add(ctx.mkOr(f2, p2)); + solver.add(ctx.mkOr(f3, p3)); + solver.add(ctx.mkOr(f4, p4)); Status result = solver.check(assumptions); if (result == Status.UNSATISFIABLE) diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 8d13fcb43..8c6e6c4c6 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -78,6 +78,14 @@ namespace Microsoft.Z3 } } + /// + /// Alias for Assert. + /// + public void Add(params BoolExpr[] constraints) + { + Assert(constraints); + } + /// /// Register predicate as recursive relation. /// diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index e648ac80c..b108683c9 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -90,6 +90,14 @@ namespace Microsoft.Z3 } } + /// + /// Alias for Assert. + /// + public void Add(params BoolExpr[] constraints) + { + Assert(constraints); + } + /// /// Indicates whether the goal contains `false'. /// diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 8c07ef31e..274f8dc4a 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -117,6 +117,14 @@ namespace Microsoft.Z3 } } + /// + /// Alias for Assert. + /// + public void Add(params BoolExpr[] constraints) + { + Assert(constraints); + } + /// /// Assert multiple constraints into the solver, and track them (in the unsat) core /// using the Boolean constants in ps. diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 6a8cafae2..4710368aa 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -51,7 +51,7 @@ public class Fixedpoint extends Z3Object * * @throws Z3Exception **/ - public void assert_(BoolExpr ... constraints) throws Z3Exception + public void add(BoolExpr ... constraints) throws Z3Exception { getContext().checkContextMatch(constraints); for (BoolExpr a : constraints) diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index 520a7af15..c486a57b3 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -65,7 +65,7 @@ public class Goal extends Z3Object * * @throws Z3Exception **/ - public void assert_(BoolExpr ... constraints) throws Z3Exception + public void add(BoolExpr ... constraints) throws Z3Exception { getContext().checkContextMatch(constraints); for (BoolExpr c : constraints) diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index c60d3f88c..3827de07a 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -94,7 +94,7 @@ public class Solver extends Z3Object * * @throws Z3Exception **/ - public void assert_(BoolExpr... constraints) throws Z3Exception + public void add(BoolExpr... constraints) throws Z3Exception { getContext().checkContextMatch(constraints); for (BoolExpr a : constraints) From e8140f5c1fe143bd1017b3dff1c444eea494a59c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Feb 2013 12:34:52 -0800 Subject: [PATCH 6/7] Fix compilation problems when using Visual Studio 32 bit compiler Signed-off-by: Leonardo de Moura --- src/api/c++/z3++.h | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 3382b8b00..43975fd04 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -251,8 +251,8 @@ namespace z3 { array(unsigned sz):m_size(sz) { m_array = new T[sz]; } ~array() { delete[] m_array; } unsigned size() const { return m_size; } - T & operator[](unsigned i) { assert(i < m_size); return m_array[i]; } - T const & operator[](unsigned i) const { assert(i < m_size); return m_array[i]; } + T & operator[](int i) { assert(0 <= i); assert(static_cast(i) < m_size); return m_array[i]; } + T const & operator[](int i) const { assert(0 <= i); assert(static_cast(i) < m_size); return m_array[i]; } T const * ptr() const { return m_array; } T * ptr() { return m_array; } }; @@ -1016,7 +1016,7 @@ namespace z3 { ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); } operator Z3_ast_vector() const { return m_vector; } unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); } - T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast()(ctx(), r); } + T operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast()(ctx(), r); } void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); } void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); } T back() const { return operator[](size() - 1); } @@ -1112,7 +1112,10 @@ namespace z3 { func_decl get_const_decl(unsigned i) const { Z3_func_decl r = Z3_model_get_const_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); } func_decl get_func_decl(unsigned i) const { Z3_func_decl r = Z3_model_get_func_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); } unsigned size() const { return num_consts() + num_funcs(); } - func_decl operator[](unsigned i) const { return i < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts()); } + func_decl operator[](int i) const { + assert(0 <= i); + return static_cast(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts()); + } expr get_const_interp(func_decl c) const { check_context(*this, c); @@ -1260,7 +1263,7 @@ namespace z3 { } void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); } unsigned size() const { return Z3_goal_size(ctx(), m_goal); } - expr operator[](unsigned i) const { Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); } + expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); } Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); } bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; } unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); } @@ -1303,8 +1306,7 @@ namespace z3 { return *this; } unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); } - goal operator[](unsigned i) const { Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); } - goal operator[](int i) const { assert(i >= 0); return this->operator[](static_cast(i)); } + goal operator[](int i) const { assert(0 <= i); Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); } model convert_model(model const & m, unsigned i = 0) const { check_context(*this, m); Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m); From 5598f334d406905fc1717a2cdbb9c9e484d19094 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Feb 2013 17:01:49 -0800 Subject: [PATCH 7/7] optimizations to Hilbert basis Signed-off-by: Nikolaj Bjorner --- src/muz_qe/hilbert_basis.cpp | 112 +++++++++++++++++++++-------------- src/muz_qe/hilbert_basis.h | 16 ++--- src/test/hilbert_basis.cpp | 2 + 3 files changed, 77 insertions(+), 53 deletions(-) diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index 49bf20746..59b513d8d 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -192,19 +192,9 @@ class hilbert_basis::value_index2 { checker m_checker; vector m_keys; -#if 1 numeral const* get_keys(values const& vs) { return vs()-1; } -#else - numeral const* get_keys(values const& vs) { - unsigned sz = m_keys.size(); - for (unsigned i = 0; i < sz; ++i) { - m_keys[sz-i-1] = vs()[i-1]; - } - return m_keys.c_ptr(); - } -#endif public: value_index2(hilbert_basis& hb): hb(hb), m_init(false) { @@ -506,7 +496,11 @@ class hilbert_basis::passive2 { } }; hilbert_basis& hb; - svector const& m_sos; + svector m_pos_sos; + svector m_neg_sos; + vector m_pos_sos_sum; + vector m_neg_sos_sum; + vector m_sum_abs; unsigned_vector m_psos; svector m_pas; vector m_weight; @@ -527,40 +521,59 @@ class hilbert_basis::passive2 { public: passive2(hilbert_basis& hb): hb(hb), - m_sos(hb.m_sos), m_lt(&m_this), m_heap(10, m_lt) { m_this = this; } + void init(svector const& I) { + for (unsigned i = 0; i < I.size(); ++i) { + numeral const& w = hb.vec(I[i]).weight(); + if (w.is_pos()) { + m_pos_sos.push_back(I[i]); + m_pos_sos_sum.push_back(sum_abs(I[i])); + } + else { + m_neg_sos.push_back(I[i]); + m_neg_sos_sum.push_back(sum_abs(I[i])); + } + } + } + void reset() { m_heap.reset(); m_free_list.reset(); m_psos.reset(); m_pas.reset(); + m_sum_abs.reset(); + m_pos_sos.reset(); + m_neg_sos.reset(); + m_pos_sos_sum.reset(); + m_neg_sos_sum.reset(); m_weight.reset(); } void insert(offset_t idx, unsigned offset) { - SASSERT(!m_sos.empty()); + SASSERT(!m_pos_sos.empty()); unsigned v; - numeral w = sum_abs(idx) + sum_abs(m_sos[0]); if (m_free_list.empty()) { v = m_pas.size(); m_pas.push_back(idx); m_psos.push_back(offset); - m_weight.push_back(w); + m_weight.push_back(numeral(0)); m_heap.set_bounds(v+1); + m_sum_abs.push_back(sum_abs(idx)); } else { v = m_free_list.back(); m_free_list.pop_back(); m_pas[v] = idx; m_psos[v] = offset; - m_weight[v] = w; + m_weight[v] = numeral(0); + m_sum_abs[v] = sum_abs(idx); } - next_resolvable(v); + next_resolvable(hb.vec(idx).weight().is_pos(), v); } bool empty() const { @@ -570,12 +583,13 @@ public: unsigned pop(offset_t& sos, offset_t& pas) { SASSERT (!empty()); unsigned val = static_cast(m_heap.erase_min()); - unsigned psos = m_psos[val]; - sos = m_sos[psos]; pas = m_pas[val]; - m_psos[val]++; - next_resolvable(val); numeral old_weight = hb.vec(pas).weight(); + bool is_positive = old_weight.is_pos(); + unsigned psos = m_psos[val]; + sos = is_positive?m_neg_sos[psos]:m_pos_sos[psos]; + m_psos[val]++; + next_resolvable(is_positive, val); numeral new_weight = hb.vec(sos).weight() + old_weight; if (new_weight.is_pos() != old_weight.is_pos()) { psos = 0; @@ -599,7 +613,7 @@ public: public: iterator(passive2& p, unsigned i): p(p), m_idx(i) { fwd(); } offset_t pas() const { return p.m_pas[m_idx]; } - offset_t sos() const { return p.m_sos[p.m_psos[m_idx]]; } + offset_t sos() const { return (p.hb.vec(pas()).weight().is_pos()?p.m_neg_sos:p.m_pos_sos)[p.m_psos[m_idx]]; } iterator& operator++() { ++m_idx; fwd(); return *this; } iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; } bool operator==(iterator const& it) const {return m_idx == it.m_idx; } @@ -614,12 +628,14 @@ public: return iterator(*this, m_pas.size()); } private: - void next_resolvable(unsigned v) { + void next_resolvable(bool is_positive, unsigned v) { offset_t pas = m_pas[v]; - while (m_psos[v] < m_sos.size()) { - offset_t sos = m_sos[m_psos[v]]; - if (hb.can_resolve(sos, pas)) { - m_weight[v] = sum_abs(pas) + sum_abs(sos); + svector const& soss = is_positive?m_neg_sos:m_pos_sos; + while (m_psos[v] < soss.size()) { + unsigned psos = m_psos[v]; + offset_t sos = soss[psos]; + if (hb.can_resolve(sos, pas, false)) { + m_weight[v] = m_sum_abs[v] + (is_positive?m_neg_sos_sum[psos]:m_pos_sos_sum[psos]); m_heap.insert(v); return; } @@ -745,7 +761,7 @@ unsigned hilbert_basis::get_num_vars() const { } hilbert_basis::values hilbert_basis::vec(offset_t offs) const { - return values(m_store.c_ptr() + (get_num_vars() + 1)*offs.m_offset); + return values(m_ineqs.size(), m_store.c_ptr() + offs.m_offset); } void hilbert_basis::init_basis() { @@ -804,6 +820,9 @@ lbool hilbert_basis::saturate_orig(num_vector const& ineq, bool is_eq) { offset_t idx = *it; values v = vec(idx); v.weight() = get_weight(v, ineq); + for (unsigned k = 0; k < m_current_ineq; ++k) { + v.weight(k) = get_weight(v, m_ineqs[k]); + } add_goal(idx); if (m_use_support) { support.insert(idx.m_offset); @@ -823,7 +842,7 @@ lbool hilbert_basis::saturate_orig(num_vector const& ineq, bool is_eq) { continue; } for (unsigned i = 0; !m_cancel && i < m_active.size(); ++i) { - if ((!m_use_support || support.contains(m_active[i].m_offset)) && can_resolve(idx, m_active[i])) { + if ((!m_use_support || support.contains(m_active[i].m_offset)) && can_resolve(idx, m_active[i], true)) { resolve(idx, m_active[i], j); if (add_goal(j)) { j = alloc_vector(); @@ -874,6 +893,9 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { offset_t idx = m_basis[i]; values v = vec(idx); v.weight() = get_weight(v, ineq); + for (unsigned k = 0; k < m_current_ineq; ++k) { + v.weight(k) = get_weight(v, m_ineqs[k]); + } m_index->insert(idx, v); if (v.weight().is_zero()) { m_zero.push_back(idx); @@ -886,6 +908,7 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { } } m_basis.resize(init_basis_size); + m_passive2->init(m_sos); // ASSERT basis is sorted by weight. // initialize passive @@ -902,7 +925,7 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { offset_t sos, pas; TRACE("hilbert_basis", display(tout); ); unsigned offset = m_passive2->pop(sos, pas); - SASSERT(can_resolve(sos, pas)); + SASSERT(can_resolve(sos, pas, true)); resolve(sos, pas, idx); if (is_subsumed(idx)) { continue; @@ -933,14 +956,6 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { m_free_list.push_back(m_basis.back()); m_basis.pop_back(); } - for (unsigned i = 0; i < init_basis_size; ++i) { - offset_t idx = m_basis[i]; - if (vec(idx).weight().is_neg()) { - m_basis[i] = m_basis.back(); - m_basis.pop_back(); - - } - } m_basis.append(m_zero); std::sort(m_basis.begin(), m_basis.end(), vector_lt_t(*this)); m_zero.reset(); @@ -1051,6 +1066,9 @@ void hilbert_basis::resolve(offset_t i, offset_t j, offset_t r) { u[k] = v[k] + w[k]; } u.weight() = v.weight() + w.weight(); + for (unsigned k = 0; k < m_current_ineq; ++k) { + u.weight(k) = v.weight(k) + w.weight(k); + } TRACE("hilbert_basis_verbose", display(tout, i); display(tout, j); @@ -1061,10 +1079,11 @@ void hilbert_basis::resolve(offset_t i, offset_t j, offset_t r) { hilbert_basis::offset_t hilbert_basis::alloc_vector() { if (m_free_list.empty()) { - unsigned num_vars = get_num_vars(); - unsigned idx = m_store.size(); - m_store.resize(idx + 1 + num_vars); - return offset_t(idx/(1+num_vars)); + unsigned sz = m_ineqs.size() + get_num_vars(); + unsigned idx = m_store.size(); + m_store.resize(idx + sz); + // std::cout << "alloc vector: " << idx << " " << sz << " " << m_store.c_ptr() + idx << " " << m_ineqs.size() << "\n"; + return offset_t(idx); } else { offset_t result = m_free_list.back(); @@ -1099,10 +1118,11 @@ bool hilbert_basis::is_subsumed(offset_t idx) { return false; } -bool hilbert_basis::can_resolve(offset_t i, offset_t j) const { - if (get_sign(i) == get_sign(j)) { +bool hilbert_basis::can_resolve(offset_t i, offset_t j, bool check_sign) const { + if (check_sign && get_sign(i) == get_sign(j)) { return false; } + SASSERT(get_sign(i) != get_sign(j)); values const& v1 = vec(i); values const& v2 = vec(j); if (v1[0].is_one() && v2[0].is_one()) { @@ -1121,7 +1141,7 @@ bool hilbert_basis::can_resolve(offset_t i, offset_t j) const { } hilbert_basis::sign_t hilbert_basis::get_sign(offset_t idx) const { - numeral val = vec(idx).weight(); + numeral const& val = vec(idx).weight(); if (val.is_pos()) { return pos; } @@ -1265,7 +1285,7 @@ bool hilbert_basis::is_subsumed(offset_t i, offset_t j) const { n >= m && (!m.is_neg() || n == m) && is_geq(v, w); for (unsigned k = 0; r && k < m_current_ineq; ++k) { - r = get_weight(vec(i), m_ineqs[k]) >= get_weight(vec(j), m_ineqs[k]); + r = v.weight(k) >= w.weight(k); } CTRACE("hilbert_basis", r, display(tout, i); diff --git a/src/muz_qe/hilbert_basis.h b/src/muz_qe/hilbert_basis.h index 78d4d7cec..bad4b1fbd 100644 --- a/src/muz_qe/hilbert_basis.h +++ b/src/muz_qe/hilbert_basis.h @@ -56,12 +56,14 @@ private: class values { numeral* m_values; public: - values(numeral* v):m_values(v) {} - numeral& weight() { return m_values[0]; } // value of a*x - numeral& operator[](unsigned i) { return m_values[i+1]; } // value of x_i - numeral const& weight() const { return m_values[0]; } // value of a*x - numeral const& operator[](unsigned i) const { return m_values[i+1]; } // value of x_i - numeral const* operator()() const { return m_values + 1; } + values(unsigned offset, numeral* v): m_values(v+offset) { } + numeral& weight() { return m_values[-1]; } // value of a*x + numeral const& weight() const { return m_values[-1]; } // value of a*x + numeral& weight(int i) { return m_values[-2-i]; } // value of b_i*x for 0 <= i < current inequality. + numeral const& weight(int i) const { return m_values[-2-i]; } // value of b_i*x + numeral& operator[](unsigned i) { return m_values[i]; } // value of x_i + numeral const& operator[](unsigned i) const { return m_values[i]; } // value of x_i + numeral const* operator()() const { return m_values; } }; vector m_ineqs; // set of asserted inequalities @@ -114,7 +116,7 @@ private: bool is_subsumed(offset_t idx); bool is_subsumed(offset_t i, offset_t j) const; void recycle(offset_t idx); - bool can_resolve(offset_t i, offset_t j) const; + bool can_resolve(offset_t i, offset_t j, bool check_sign) const; sign_t get_sign(offset_t idx) const; bool add_goal(offset_t idx); offset_t alloc_vector(); diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index e2d1d337e..69d733f68 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -521,6 +521,8 @@ void tst_hilbert_basis() { tst2(); tst3(); tst4(); + tst4(); + tst4(); tst5(); tst6(); tst7();