From d13d6fecbf6d8251fb2bf5ca1a1fadd30bd6c463 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 30 Nov 2012 19:43:34 +0000 Subject: [PATCH 1/5] Java API: added correct error handling. Signed-off-by: Christoph M. Wintersteiger --- scripts/update_api.py | 17 ++++++++++++++--- src/api/java/Context.java | 33 +++------------------------------ 2 files changed, 17 insertions(+), 33 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 60ec37220..abd347a74 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -494,12 +494,12 @@ def mk_java(): java_native.write(' public static class IntPtr { public int value; }\n') java_native.write(' public static class LongPtr { public long value; }\n') java_native.write(' public static class StringPtr { public String value; }\n') - java_native.write(' public static class errorHandler { public long ptr; }\n') + java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n') if IS_WINDOWS: java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name) else: java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name - java_native.write('\n\n') + java_native.write('\n') for name, result, params in _dotnet_decls: java_native.write(' protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name))) first = True @@ -553,6 +553,7 @@ def mk_java(): java_native.write(' }\n\n') java_native.write('}\n') java_wrapper = open(java_wrapperf, 'w') + pkg_str = get_component('java').package_name.replace('.', '_') java_wrapper.write('// Automatically generated file\n') java_wrapper.write('#include\n') java_wrapper.write('#include\n') @@ -578,7 +579,17 @@ def mk_java(): java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') java_wrapper.write(' delete [] NEW; \n\n') java_wrapper.write('#endif\n\n') - pkg_str = get_component('java').package_name.replace('.', '_') + java_wrapper.write('void Z3JavaErrorHandler(Z3_context c, Z3_error_code e)\n') + java_wrapper.write('{\n') + java_wrapper.write(' // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n') + java_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n') + java_wrapper.write(' // wrappers below.\n') + java_wrapper.write('}\n\n') + java_wrapper.write('JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, long a0)\n' % pkg_str) + java_wrapper.write('{\n') + java_wrapper.write(' Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);\n') + java_wrapper.write('}\n\n') + java_wrapper.write('') for name, result, params in _dotnet_decls: java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) i = 0; diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 1d2f800ba..f375ab525 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -38,12 +38,11 @@ public class Context extends IDisposable InitContext(); } - private Context(long ctx, long refCount, Native.errorHandler errh) + private Context(long ctx, long refCount) { super(); this.m_ctx = ctx; this.m_refCount = refCount; - this.m_n_err_handler = errh; } /** @@ -2908,21 +2907,6 @@ public class Context extends IDisposable Native.toggleWarningMessages((enabled) ? true : false); } - // /// - // /// A delegate which is executed when an error is raised. - // /// - // /// - // /// Note that it is possible for memory leaks to occur if error handlers - // /// throw exceptions. - // /// - // public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, - // String errorString); - - // /// - // /// The OnError event. - // /// - // public event ErrorHandler OnError = null; - /** * Update a mutable configuration parameter. The list of all * configuration parameters can be obtained using the Z3 executable: @@ -2950,26 +2934,16 @@ public class Context extends IDisposable } long m_ctx = 0; - Native.errorHandler m_n_err_handler = null; long nCtx() { return m_ctx; } - // void NativeErrorHandler(long ctx, Z3_error_code errorCode) - // { - // // Do-nothing error handler. The wrappers in Z3.Native will throw - // exceptions upon errors. - // } - void InitContext() throws Z3Exception { setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); - // m_n_err_handler = new Native.errorHandler(NativeErrorHandler); // - // keep reference so it doesn't get collected. - // if (m_n_err_handler != null) Native.setErrorHandler(m_ctx, - // m_n_err_handler); + Native.setInternalErrorHandler(nCtx()); } void CheckContextMatch(Z3Object other) throws Z3Exception @@ -3087,7 +3061,6 @@ public class Context extends IDisposable if (m_refCount == 0) { - m_n_err_handler = null; try { Native.delContext(m_ctx); @@ -3099,7 +3072,7 @@ public class Context extends IDisposable } else /* re-queue the finalizer */ /* BUG: DRQ's need to be taken over too! */ - new Context(m_ctx, m_refCount, m_n_err_handler); + new Context(m_ctx, m_refCount); } /** From 9b2236361c98feaee24b2e4a3c10506dcd1b5d8b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 30 Nov 2012 19:50:57 +0000 Subject: [PATCH 2/5] Java API: bugfix Signed-off-by: Christoph M. Wintersteiger --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index abd347a74..f89764299 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -585,7 +585,7 @@ def mk_java(): java_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n') java_wrapper.write(' // wrappers below.\n') java_wrapper.write('}\n\n') - java_wrapper.write('JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, long a0)\n' % pkg_str) + java_wrapper.write('JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0)\n' % pkg_str) java_wrapper.write('{\n') java_wrapper.write(' Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);\n') java_wrapper.write('}\n\n') From 692593baaa391ab747a08f3781224c22d26aa575 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 30 Nov 2012 22:31:07 +0000 Subject: [PATCH 3/5] Java API: 32-bit issues and bugfixes. Signed-off-by: Christoph M. Wintersteiger --- examples/java/JavaExample.java | 50 +++++++++++++++++++--------- scripts/update_api.py | 60 ++++++++++++++++++++++------------ src/api/java/AST.java | 39 +++++++++++++--------- src/api/java/Context.java | 2 +- src/api/java/EnumSort.java | 9 ++--- src/api/java/Quantifier.java | 15 +++++---- src/api/java/Sort.java | 13 +++++--- src/api/java/Z3Object.java | 2 +- 8 files changed, 119 insertions(+), 71 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 5d56a474b..d06f72217 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -907,11 +907,10 @@ class JavaExample // Error handling test. try { - IntExpr i = ctx.MkInt("0.5"); + IntExpr i = ctx.MkInt("1/2"); throw new TestFailedException(); // unreachable } catch (Z3Exception e) - { - System.out.println("GOT: " + e.getMessage()); + { } } @@ -1001,19 +1000,38 @@ class JavaExample } AST a = ctx.MkInt(42); - Expr ae = (a.getClass() == Expr.class) ? ((Expr) a) : null; - if (ae == null) + + try + { + Expr.class.cast(a); + } catch (ClassCastException e) + { throw new TestFailedException(); - ArithExpr aae = (a.getClass() == ArithExpr.class) ? ((ArithExpr) a) - : null; - if (aae == null) + } + + try + { + ArithExpr.class.cast(a); + } catch (ClassCastException e) + { throw new TestFailedException(); - IntExpr aie = (a.getClass() == IntExpr.class) ? ((IntExpr) a) : null; - if (aie == null) + } + + try + { + IntExpr.class.cast(a); + } catch (ClassCastException e) + { throw new TestFailedException(); - IntNum ain = (a.getClass() == IntNum.class) ? ((IntNum) a) : null; - if (ain == null) + } + + try + { + IntNum.class.cast(a); + } catch (ClassCastException e) + { throw new TestFailedException(); + } Expr[][] earr = new Expr[2][]; earr[0] = new Expr[2]; @@ -1585,7 +1603,7 @@ class JavaExample Symbol name = ctx.MkSymbol("fruit"); - EnumSort fruit = ctx.MkEnumSort(ctx.MkSymbol("fruit"), + EnumSort fruit = ctx.MkEnumSort(name, new Symbol[] { ctx.MkSymbol("apple"), ctx.MkSymbol("banana"), ctx.MkSymbol("orange") }); @@ -1974,7 +1992,7 @@ class JavaExample { int num_Exprs = to_minimize.length; int[] upper = new int[num_Exprs]; - int[] lower = new int[num_Exprs]; + int[] lower = new int[num_Exprs]; for (int i = 0; i < upper.length; ++i) { upper[i] = Integer.MAX_VALUE; @@ -2207,12 +2225,12 @@ class JavaExample { System.out.println("Z3 Managed Exception: " + ex.getMessage()); System.out.println("Stack trace: "); - ex.printStackTrace(System.out); + ex.printStackTrace(System.out); } catch (TestFailedException ex) { System.out.println("TEST CASE FAILED: " + ex.getMessage()); System.out.println("Stack trace: "); - ex.printStackTrace(System.out); + ex.printStackTrace(System.out); } catch (Exception ex) { System.out.println("Unknown Exception: " + ex.getMessage()); diff --git a/scripts/update_api.py b/scripts/update_api.py index f89764299..d7dbb7bcf 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -474,11 +474,6 @@ def java_array_element_type(p): return 'jint' else: return 'jlong' -def java_set_array_region(p): - if param_type(p) == INT or param_type(p) == UINT: - return 'SetIntArrayRegion' - else: - return 'SetLongArrayRegion' def mk_java(): if not is_java_enabled(): @@ -563,21 +558,43 @@ def mk_java(): java_wrapper.write('#endif\n\n') java_wrapper.write('#if defined(_M_X64) || defined(_AMD64_)\n\n') java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') - java_wrapper.write(' T * NEW = (T*) jenv->GetLongArrayElements(OLD, NULL); \n') + java_wrapper.write(' T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n') java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') - java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT); \n\n') + java_wrapper.write(' if (OLD != 0) jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT); \n\n') + java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n') + java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW); \n') + java_wrapper.write('#define SETLONGAREGION(OLD,Z,SZ,NEW) \\\n') + java_wrapper.write(' jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW) \n\n') java_wrapper.write('#else\n\n') java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') java_wrapper.write(' T * NEW = 0; { \\\n') - java_wrapper.write(' jlong * temp = jenv->GetLongArrayElements(OLD, NULL); \\\n') - java_wrapper.write(' unsigned int size = jenv->GetArrayLength(OLD); \\\n') - java_wrapper.write(' NEW = (T*) (new int[size]); \\\n') - java_wrapper.write(' for (unsigned i=0; i < size; i++) \\\n') - java_wrapper.write(' NEW[i] = reinterpret_cast(temp[i]); \\\n') - java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \\\n') - java_wrapper.write(' } \n\n') - java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') + java_wrapper.write(' jlong * temp = (OLD == 0) ? 0 : jenv->GetLongArrayElements(OLD, NULL); \\\n') + java_wrapper.write(' unsigned int size = (OLD == 0) ? 0 :jenv->GetArrayLength(OLD); \\\n') + java_wrapper.write(' if (OLD != 0) { \\\n') + java_wrapper.write(' NEW = (T*) (new int[size]); \\\n') + java_wrapper.write(' for (unsigned i=0; i < size; i++) \\\n') + java_wrapper.write(' NEW[i] = reinterpret_cast(temp[i]); \\\n') + java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \\\n') + java_wrapper.write(' } \\\n') + java_wrapper.write(' } \n\n') + java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') java_wrapper.write(' delete [] NEW; \n\n') + java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n') + java_wrapper.write(' { \\\n') + java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n') + java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)temp); \\\n') + java_wrapper.write(' for (int i = 0; i < (SZ); i++) \\\n') + java_wrapper.write(' NEW[i] = reinterpret_cast(temp[i]); \\\n') + java_wrapper.write(' delete [] temp; \\\n') + java_wrapper.write(' }\n\n') + java_wrapper.write('#define SETLONGAREGION(OLD,Z,SZ,NEW) \\\n') + java_wrapper.write(' { \\\n') + java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n') + java_wrapper.write(' for (int i = 0; i < (SZ); i++) \\\n') + java_wrapper.write(' temp[i] = reinterpret_cast(NEW[i]); \\\n') + java_wrapper.write(' jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,temp); \\\n') + java_wrapper.write(' delete [] temp; \\\n') + java_wrapper.write(' }\n\n') java_wrapper.write('#endif\n\n') java_wrapper.write('void Z3JavaErrorHandler(Z3_context c, Z3_error_code e)\n') java_wrapper.write('{\n') @@ -615,6 +632,10 @@ def mk_java(): type2str(param_type(param)), param_array_capacity_pos(param), type2str(param_type(param)))) + if param_type(param) == INT or param_type(param) == UINT: + java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) + else: + java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i)) elif k == IN and param_type(param) == STRING: java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i)) i = i + 1 @@ -646,11 +667,10 @@ def mk_java(): for param in params: k = param_kind(param) if k == OUT_ARRAY: - java_wrapper.write(' jenv->%s(a%s, 0, (jsize)a%s, (%s *) _a%s);\n' % (java_set_array_region(param), - i, - param_array_capacity_pos(param), - java_array_element_type(param), - i)) + if param_type(param) == INT or param_type(param) == UINT: + java_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) + else: + java_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i)) java_wrapper.write(' free(_a%s);\n' % i) elif k == IN_ARRAY or k == OUT_ARRAY: if param_type(param) == INT or param_type(param) == UINT: diff --git a/src/api/java/AST.java b/src/api/java/AST.java index fbefbf5e2..418c43e9f 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -37,10 +37,15 @@ public class AST extends Z3Object **/ public boolean equals(Object o) { - AST casted = (AST) o; - if (casted == null) - return false; - return this == casted; + AST casted = null; + + try { + casted = AST.class.cast(o); + } catch (ClassCastException e) { + return false; + } + + return this.NativeObject() == casted.NativeObject(); } /** @@ -53,18 +58,20 @@ public class AST extends Z3Object { if (other == null) return 1; - AST oAST = (AST) other; - if (oAST == null) - return 1; - else - { - if (Id() < oAST.Id()) - return -1; - else if (Id() > oAST.Id()) - return +1; - else - return 0; - } + + AST oAST = null; + try { + AST.class.cast(other); + } catch (ClassCastException e) { + return 1; + } + + if (Id() < oAST.Id()) + return -1; + else if (Id() > oAST.Id()) + return +1; + else + return 0; } /** diff --git a/src/api/java/Context.java b/src/api/java/Context.java index f375ab525..d6076b5ee 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -524,7 +524,7 @@ public class Context extends IDisposable public Expr MkConst(FuncDecl f) throws Z3Exception { - return MkApp(f, (Expr) null); + return MkApp(f, (Expr[]) null); } /** diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index f02301a5d..10f0f9764 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -16,7 +16,6 @@ public class EnumSort extends Sort **/ public FuncDecl[] ConstDecls() { - return _constdecls; } @@ -25,7 +24,6 @@ public class EnumSort extends Sort **/ public Expr[] Consts() { - return _consts; } @@ -34,7 +32,6 @@ public class EnumSort extends Sort **/ public FuncDecl[] TesterDecls() { - return _testerdecls; } @@ -53,12 +50,12 @@ public class EnumSort extends Sort n_constdecls, n_testers)); _constdecls = new FuncDecl[n]; for (int i = 0; i < n; i++) - _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]); + _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]); _testerdecls = new FuncDecl[n]; for (int i = 0; i < n; i++) - _testerdecls[i] = new FuncDecl(ctx, n_testers[i]); + _testerdecls[i] = new FuncDecl(ctx, n_testers[i]); _consts = new Expr[n]; for (int i = 0; i < n; i++) - _consts[i] = ctx.MkApp(_constdecls[i], (Expr)null); + _consts[i] = ctx.MkApp(_constdecls[i], (Expr[])null); } }; diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 82e5a958b..6ee7e4412 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -159,13 +159,14 @@ public class Quantifier extends BoolExpr .NativeObject())); } else { - setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), (isForall) ? true - : false, weight, AST.GetNativeObject(quantifierID), AST - .GetNativeObject(skolemID), AST.ArrayLength(patterns), AST - .ArrayToNative(patterns), AST.ArrayLength(noPatterns), AST - .ArrayToNative(noPatterns), AST.ArrayLength(sorts), AST - .ArrayToNative(sorts), Symbol.ArrayToNative(names), body - .NativeObject())); + setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), + (isForall) ? true : false, weight, AST.GetNativeObject(quantifierID), + AST.GetNativeObject(skolemID), + AST.ArrayLength(patterns), AST.ArrayToNative(patterns), + AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), + AST.ArrayLength(sorts), AST.ArrayToNative(sorts), + Symbol.ArrayToNative(names), + body.NativeObject())); } } diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 526329146..fcf6b117a 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -39,10 +39,15 @@ public class Sort extends AST **/ public boolean equals(Object o) { - Sort casted = (Sort) o; - if (casted == null) - return false; - return this == casted; + Sort casted = null; + + try { + casted = Sort.class.cast(o); + } catch (ClassCastException e) { + return false; + } + + return this.NativeObject() == casted.NativeObject(); } /** diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index 877fead79..8aeb03ddf 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -104,7 +104,7 @@ public class Z3Object extends IDisposable return null; long[] an = new long[a.length]; for (int i = 0; i < a.length; i++) - an[i] = a[i].NativeObject(); + an[i] = (a[i] == null) ? 0 : a[i].NativeObject(); return an; } From 2d1a6bf270df9611453abfdc0822f40e3da1b25e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Nov 2012 15:58:06 -0800 Subject: [PATCH 4/5] fix regression for simplifying tails with quantifiers, add some more handling for quantified tails Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 5 +- src/muz_qe/dl_context.cpp | 2 +- src/muz_qe/dl_mk_interp_tail_simplifier.cpp | 2 +- src/muz_qe/dl_util.h | 5 + src/muz_qe/expr_safe_replace.cpp | 102 +++ src/muz_qe/expr_safe_replace.h | 43 + src/muz_qe/pdr_quantifiers.cpp | 433 +++++----- src/muz_qe/pdr_quantifiers.h | 32 +- src/muz_qe/qe_lite.cpp | 889 ++++++++++---------- src/muz_qe/qe_lite.h | 2 +- 10 files changed, 888 insertions(+), 627 deletions(-) create mode 100644 src/muz_qe/expr_safe_replace.cpp create mode 100644 src/muz_qe/expr_safe_replace.h diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 3c98dca33..67f07e414 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2637,12 +2637,13 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro ptr_buffer args; args.append(num_proofs, (expr**) proofs); expr * fact; - expr const * f1 = get_fact(proofs[0]); - expr const * f2 = get_fact(proofs[1]); + expr * f1 = get_fact(proofs[0]); + expr * f2 = get_fact(proofs[1]); if (num_proofs == 2 && is_complement(f1, f2)) { fact = mk_false(); } else { + CTRACE("mk_unit_resolution_bug", !is_or(f1), tout << mk_pp(f1, *this) << " " << mk_pp(f2, *this) << "\n";); SASSERT(is_or(f1)); ptr_buffer new_lits; app const * cls = to_app(f1); diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 3818b1955..48242a7ed 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -1769,7 +1769,7 @@ namespace datalog { if (use_fixedpoint_extensions) { for (unsigned i = 0; i < num_queries; ++i) { out << "(query "; - PP(queries[i]); + PP(queries[i]); out << ")\n"; } } diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp index aa11d1b36..9861c48ca 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp @@ -463,7 +463,7 @@ namespace datalog { if (r->has_quantifiers()) { res = r; - return false; + return true; } start: diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index f314b691d..12ed004ef 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -191,6 +191,11 @@ namespace datalog { scoped_coarse_proof(ast_manager& m): scoped_proof_mode(m, PGM_COARSE) {} }; + class scoped_fine_proof : public scoped_proof_mode { + public: + scoped_fine_proof(ast_manager& m): scoped_proof_mode(m, PGM_FINE) {} + }; + class scoped_no_proof : public scoped_proof_mode { public: scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {} diff --git a/src/muz_qe/expr_safe_replace.cpp b/src/muz_qe/expr_safe_replace.cpp new file mode 100644 index 000000000..b3b4d5138 --- /dev/null +++ b/src/muz_qe/expr_safe_replace.cpp @@ -0,0 +1,102 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + expr_safe_replace.cpp + +Abstract: + + Version of expr_replace/expr_substitution that is safe for quantifiers. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-30 + +Revision History: + + +--*/ + +#include "expr_safe_replace.h" +#include "rewriter.h" + + +void expr_safe_replace::insert(expr* src, expr* dst) { + m_src.push_back(src); + m_dst.push_back(dst); + m_subst.insert(src, dst); +} + +void expr_safe_replace::operator()(expr* e, expr_ref& res) { + obj_map cache; + ptr_vector todo, args; + expr_ref_vector refs(m); + todo.push_back(e); + expr* a, *b, *d; + todo.push_back(e); + + while (!todo.empty()) { + a = todo.back(); + if (cache.contains(a)) { + todo.pop_back(); + } + else if (m_subst.find(a, b)) { + cache.insert(a, b); + todo.pop_back(); + } + else if (is_var(a)) { + cache.insert(a, a); + todo.pop_back(); + } + else if (is_app(a)) { + app* c = to_app(a); + unsigned n = c->get_num_args(); + args.reset(); + for (unsigned i = 0; i < n; ++i) { + if (cache.find(c->get_arg(i), d)) { + args.push_back(d); + } + else { + todo.push_back(c->get_arg(i)); + } + } + if (args.size() == n) { + b = m.mk_app(c->get_decl(), args.size(), args.c_ptr()); + refs.push_back(b); + cache.insert(a, b); + todo.pop_back(); + } + } + else { + SASSERT(is_quantifier(a)); + quantifier* q = to_quantifier(a); + expr_safe_replace replace(m); + var_shifter shift(m); + expr_ref new_body(m), src(m), dst(m), tmp(m); + expr_ref_vector pats(m), nopats(m); + unsigned num_decls = q->get_num_decls(); + for (unsigned i = 0; i < m_src.size(); ++i) { + shift(m_src[i].get(), num_decls, src); + shift(m_dst[i].get(), num_decls, dst); + replace.insert(src, dst); + } + unsigned np = q->get_num_patterns(); + for (unsigned i = 0; i < np; ++i) { + replace(q->get_pattern(i), tmp); + pats.push_back(tmp); + } + np = q->get_num_no_patterns(); + for (unsigned i = 0; i < np; ++i) { + replace(q->get_no_pattern(i), tmp); + nopats.push_back(tmp); + } + replace(q->get_expr(), new_body); + b = m.update_quantifier(q, pats.size(), pats.c_ptr(), nopats.size(), nopats.c_ptr(), new_body); + refs.push_back(b); + cache.insert(a, b); + todo.pop_back(); + } + } + res = cache.find(e); +} diff --git a/src/muz_qe/expr_safe_replace.h b/src/muz_qe/expr_safe_replace.h new file mode 100644 index 000000000..6af819596 --- /dev/null +++ b/src/muz_qe/expr_safe_replace.h @@ -0,0 +1,43 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + expr_safe_replace.h + +Abstract: + + Version of expr_replace/expr_substitution that is safe for quantifiers. + + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-30 + +Revision History: + + +--*/ + +#ifndef __EXPR_SAFE_REPLACE_H__ +#define __EXPR_SAFE_REPLACE_H__ + +#include "ast.h" + +class expr_safe_replace { + ast_manager& m; + expr_ref_vector m_src; + expr_ref_vector m_dst; + obj_map m_subst; + +public: + expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m) {} + + void insert(expr* src, expr* dst); + + void operator()(expr_ref& e) { (*this)(e.get(), e); } + + void operator()(expr* src, expr_ref& e); +}; + +#endif /* __EXPR_SAFE_REPLACE_H__ */ diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp index b681b0121..7922b76c9 100644 --- a/src/muz_qe/pdr_quantifiers.cpp +++ b/src/muz_qe/pdr_quantifiers.cpp @@ -27,6 +27,9 @@ Revision History: #include "ast_smt_pp.h" #include "expr_abstract.h" #include "dl_mk_extract_quantifiers.h" +#include "qe_lite.h" +#include "well_sorted.h" +#include "expr_safe_replace.h" namespace pdr { @@ -49,6 +52,12 @@ namespace pdr { } } + quantifier_model_checker::~quantifier_model_checker() { + obj_map::iterator it = m_reachable.begin(), end = m_reachable.end(); + for (; it != end; ++it) { + m.dec_ref(it->m_value); + } + } void quantifier_model_checker::generalize_binding(expr_ref_vector const& binding, vector& bindings) { expr_ref_vector new_binding(m); @@ -193,13 +202,12 @@ namespace pdr { bool quantifier_model_checker::find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level) { bool found_instance = false; - TRACE("pdr", tout << mk_pp(m_A,m) << "\n";); - datalog::scoped_coarse_proof _scp(m); + datalog::scoped_fine_proof _scp(m); expr_ref_vector fmls(m); front_end_params fparams; - fparams.m_proof_mode = PGM_COARSE; + fparams.m_proof_mode = PGM_FINE; fparams.m_mbqi = true; fmls.push_back(m_A.get()); @@ -209,15 +217,20 @@ namespace pdr { for (unsigned i = 0; i < fmls.size(); ++i) { tout << mk_pp(fmls[i].get(), m) << "\n"; }); + smt::kernel solver(m, fparams); for (unsigned i = 0; i < fmls.size(); ++i) { solver.assert_expr(fmls[i].get()); } lbool result = solver.check(); + + TRACE("pdr", tout << result << "\n";); + if (result != l_false) { - TRACE("pdr", tout << result << "\n";); - return found_instance; + return false; } + m_rules_model_check = false; + map qid_map; quantifier* q; for (unsigned i = 0; i < qs.size(); ++i) { @@ -234,8 +247,7 @@ namespace pdr { for (unsigned i = 0; i < collector.size(); ++i) { symbol qid = quants[i]->get_qid(); if (!qid_map.find(qid, q)) { - TRACE("pdr", tout << "Could not find quantifier " - << mk_pp(quants[i], m) << "\n";); + TRACE("pdr", tout << "Could not find quantifier " << mk_pp(quants[i], m) << "\n";); continue; } expr_ref_vector const& binding = collector.bindings()[i]; @@ -256,8 +268,43 @@ namespace pdr { return found_instance; } + /** - Given node: + For under-approximations: + + m_reachable: set of reachable states, per predicate + + rules: P(x) :- B[x,y] & Fa z . Q(y,z) + Q(y,z) :- C[y,z,u] & Fa w . R(u,w) + + qis: Fa z . Q(y,z) + + M: model satisfying P(x) & B[x,y] + + B'[x,y]: body with reachable states substituted for predicates. + + Q'[y,z]: reachable states substituted for Q. + + S'[x]: Ex y . B'[x,y] & Fa z . Q'[y, z] + + Method: + + 1. M |= Fa z . Q'[y, z] => done + + Weaker variant: + Check B[x,y] & Fa z . Q'[y, z] for consistency. + + 2. Otherwise, extract instantiations. + + 3. Update reachable (for next round): + + Q'[y,z] := Q'[y,z] \/ C'[y,z,u] & Fa w . R'(u,w) + + */ + + + /** + For over-approximations: - pt - predicate transformer for rule: P(x) :- Body1(x,y) || Body2(x,z) & (Fa u . Q(u,x,z)). @@ -267,22 +314,201 @@ namespace pdr { - A := node.state(x) && Body2(x,y) + - Bs := array of Bs of the form: . Fa u . Q(u, P_x, P_y) - instantiate quantifier to P variables. . B := inv(Q_0,Q_1,Q_2) . B := inv(u, P_x, P_y) := B[u/Q_0, P_x/Q_1, P_y/Q_2] . B := Fa u . inv(u, P_x, P_y) - */ + void quantifier_model_checker::update_reachable(func_decl* f, expr* e) { + expr* e_old; + m.inc_ref(e); + if (m_reachable.find(f, e_old)) { + m.dec_ref(e_old); + } + m_reachable.insert(f, e); + } + + + expr_ref quantifier_model_checker::get_reachable(func_decl* p) { + expr* e = 0; + if (!m_reachable.find(p, e)) { + e = m_ctx.get_pred_transformer(p).initial_state(); + update_reachable(p, e); + } + return expr_ref(e, m); + } + + void quantifier_model_checker::add_over_approximations(quantifier_ref_vector& qis, model_node& n) { + add_approximations(qis, n, true); + } + + void quantifier_model_checker::add_under_approximations(quantifier_ref_vector& qis, model_node& n) { + add_approximations(qis, n, false); + } + + void quantifier_model_checker::add_approximations(quantifier_ref_vector& qis, model_node& n, bool is_over) { + pred_transformer& pt = n.pt(); + manager& pm = pt.get_pdr_manager(); + unsigned level = n.level(); + expr_ref_vector Bs(m); + expr_ref B(m), v(m); + quantifier_ref q(m); + datalog::scoped_no_proof _no_proof(m); + scoped_ptr rep = mk_default_expr_replacer(m); + for (unsigned j = 0; j < qis.size(); ++j) { + q = qis[j].get(); + app_ref_vector& inst = pt.get_inst(m_current_rule); + TRACE("pdr", + tout << "q:\n" << mk_pp(q, m) << "\n"; + tout << "level: " << level << "\n"; + model_smt2_pp(tout, m, n.get_model(), 0); + m_current_rule->display(m_ctx.get_context(), tout << "rule:\n"); + ); + + var_subst vs(m, false); + vs(q, inst.size(), (expr*const*)inst.c_ptr(), B); + q = to_quantifier(B); + TRACE("pdr", tout << "q instantiated:\n" << mk_pp(q, m) << "\n";); + + app* a = to_app(q->get_expr()); + func_decl* f = a->get_decl(); + pred_transformer& pt2 = m_ctx.get_pred_transformer(f); + if (is_over) { + B = pt2.get_formulas(level - 1, false); + } + else { + B = get_reachable(f); + SASSERT(is_well_sorted(m, B)); + } + TRACE("pdr", tout << "B:\n" << mk_pp(B, m) << "\n";); + + expr_safe_replace sub(m); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + v = m.mk_const(pm.o2n(pt2.sig(i),0)); + sub.insert(v, a->get_arg(i)); + } + sub(B); + TRACE("pdr", tout << "B substituted:\n" << mk_pp(B, m) << "\n";); + datalog::flatten_and(B, Bs); + for (unsigned i = 0; i < Bs.size(); ++i) { + m_Bs.push_back(m.update_quantifier(q, Bs[i].get())); + } + } + } + + /** + \brief compute strongest post-conditions for each predicate transformer. + (or at least something sufficient to change the set of current counter-examples) + */ + void quantifier_model_checker::weaken_under_approximation() { + + datalog::rule_set::decl2rules::iterator it = m_rules.begin_grouped_rules(), end = m_rules.end_grouped_rules(); + + for (; it != end; ++it) { + func_decl* p = it->m_key; + datalog::rule_vector& rules = *it->m_value; + expr_ref_vector bodies(m); + for (unsigned i = 0; i < rules.size(); ++i) { + bodies.push_back(strongest_post_condition(*rules[i])); + } + update_reachable(p, m.mk_or(bodies.size(), bodies.c_ptr())); + } + } + + expr_ref quantifier_model_checker::strongest_post_condition(datalog::rule& r) { + pred_transformer& pt = m_ctx.get_pred_transformer(r.get_decl()); + manager& pm = pt.get_pdr_manager(); + quantifier_ref_vector* qis = 0; + m_quantifiers.find(&r, qis); + expr_ref_vector body(m), inst(m); + expr_ref fml(m), v(m); + app* a; + func_decl* p; + svector names; + unsigned ut_size = r.get_uninterpreted_tail_size(); + unsigned t_size = r.get_tail_size(); + var_subst vs(m, false); + sort_ref_vector vars(m); + r.get_vars(vars); + if (qis) { + quantifier_ref_vector const& qi = *qis; + for (unsigned i = 0; i < qi.size(); ++i) { + fml = qi[i]->get_expr(); + a = to_app(fml); + p = a->get_decl(); + expr* p_reach = get_reachable(p); + pred_transformer& pt2 = m_ctx.get_pred_transformer(p); + expr_safe_replace sub(m); + for (unsigned j = 0; j < a->get_num_args(); ++j) { + v = m.mk_const(pm.o2n(pt2.sig(j),0)); + sub.insert(v, a->get_arg(j)); + } + sub(p_reach, fml); + body.push_back(m.update_quantifier(qi[i], fml)); + } + } + a = r.get_head(); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + v = m.mk_var(vars.size()+i, m.get_sort(a->get_arg(i))); + body.push_back(m.mk_eq(v, a->get_arg(i))); + } + for (unsigned i = 0; i < ut_size; ++i) { + a = r.get_tail(i); + p = a->get_decl(); + pred_transformer& pt2 = m_ctx.get_pred_transformer(p); + expr* p_reach = get_reachable(p); + expr_safe_replace sub(m); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + v = m.mk_const(pm.o2n(pt2.sig(i),0)); + sub.insert(v, a->get_arg(i)); + } + sub(p_reach, fml); + body.push_back(fml); + } + for (unsigned i = ut_size; i < t_size; ++i) { + body.push_back(r.get_tail(i)); + } + fml = m.mk_and(body.size(), body.c_ptr()); + vars.reverse(); + for (unsigned i = 0; i < vars.size(); ++i) { + names.push_back(symbol(i)); + } + if (!vars.empty()) { + fml = m.mk_exists(vars.size(), vars.c_ptr(), names.c_ptr(), fml); + SASSERT(is_well_sorted(m, fml)); + } + + for (unsigned i = 0; i < r.get_head()->get_num_args(); ++i) { + inst.push_back(m.mk_const(pm.o2n(pt.sig(i),0))); + } + vs(fml, inst.size(), inst.c_ptr(), fml); + SASSERT(is_well_sorted(m, fml)); + if (!vars.empty()) { + fml = to_quantifier(fml)->get_expr(); + uint_set empty_index_set; + qe_lite qe(m); + qe(empty_index_set, false, fml); + fml = m.mk_exists(vars.size(), vars.c_ptr(), names.c_ptr(), fml); + SASSERT(is_well_sorted(m, fml)); + m_ctx.get_context().get_rewriter()(fml); + } + SASSERT(is_well_sorted(m, fml)); + + IF_VERBOSE(0, verbose_stream() << "instantiate to\n:" << mk_pp(fml, m) << "\n";); + return fml; + } + void quantifier_model_checker::model_check_node(model_node& node) { TRACE("pdr", node.display(tout, 0);); pred_transformer& pt = node.pt(); manager& pm = pt.get_pdr_manager(); - expr_ref A(m), B(m), C(m), v(m); - expr_ref_vector As(m), Bs(m); + expr_ref A(m), C(m); + expr_ref_vector As(m); m_Bs.reset(); // // nodes from leaves that are repeated @@ -307,8 +533,6 @@ namespace pdr { if (level == 0) { return; } - unsigned previous_level = level - 1; - As.push_back(pt.get_propagation_formula(m_ctx.get_pred_transformers(), level)); As.push_back(node.state()); @@ -316,48 +540,8 @@ namespace pdr { m_A = pm.mk_and(As); // Add quantifiers: - - { - datalog::scoped_no_proof _no_proof(m); - quantifier_ref q(m); - scoped_ptr rep = mk_default_expr_replacer(m); - for (unsigned j = 0; j < qis->size(); ++j) { - q = (*qis)[j].get(); - app_ref_vector& inst = pt.get_inst(m_current_rule); - TRACE("pdr", - tout << "q:\n" << mk_pp(q, m) << "\n"; - tout << "level: " << level << "\n"; - model_smt2_pp(tout, m, node.get_model(), 0); - m_current_rule->display(m_ctx.get_context(), tout << "rule:\n"); - - ); - - var_subst vs(m, false); - vs(q, inst.size(), (expr*const*)inst.c_ptr(), B); - q = to_quantifier(B); - TRACE("pdr", tout << "q instantiated:\n" << mk_pp(q, m) << "\n";); - - app* a = to_app(q->get_expr()); - func_decl* f = a->get_decl(); - pred_transformer& pt2 = m_ctx.get_pred_transformer(f); - B = pt2.get_formulas(previous_level, false); - TRACE("pdr", tout << "B:\n" << mk_pp(B, m) << "\n";); - - - expr_substitution sub(m); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - v = m.mk_const(pm.o2n(pt2.sig(i),0)); - sub.insert(v, a->get_arg(i)); - } - rep->set_substitution(&sub); - (*rep)(B); - TRACE("pdr", tout << "B substituted:\n" << mk_pp(B, m) << "\n";); - datalog::flatten_and(B, Bs); - for (unsigned i = 0; i < Bs.size(); ++i) { - m_Bs.push_back(m.update_quantifier(q, Bs[i].get())); - } - } - } + // add_over_approximations(*qis, node); + add_under_approximations(*qis, node); TRACE("pdr", tout << "A:\n" << mk_pp(m_A, m) << "\n"; @@ -384,13 +568,17 @@ namespace pdr { bool quantifier_model_checker::model_check(model_node& root) { m_instantiations.reset(); m_instantiated_rules.reset(); + m_rules_model_check = true; ptr_vector nodes; get_nodes(root, nodes); for (unsigned i = nodes.size(); i > 0; ) { --i; model_check_node(*nodes[i]); } - return m_instantiations.empty(); + if (!m_rules_model_check) { + weaken_under_approximation(); + } + return m_rules_model_check; } void quantifier_model_checker::refine() { @@ -446,136 +634,3 @@ namespace pdr { } }; - -#if 0 - // - // Build: - // - // A & forall x . B1 & forall y . B2 & ... - // = - // not exists x y . (!A or !B1 or !B2 or ...) - // - // Find an instance that satisfies formula. - // (or find all instances?) - // - bool quantifier_model_checker::find_instantiations_qe_based(quantifier_ref_vector const& qs, unsigned level) { - expr_ref_vector fmls(m), conjs(m), fresh_vars(m); - app_ref_vector all_vars(m); - expr_ref C(m); - qe::def_vector defs(m); - front_end_params fparams; - qe::expr_quant_elim qe(m, fparams); - for (unsigned i = 0; i < m_Bs.size(); ++i) { - quantifier* q = qs[i]; - unsigned num_decls = q->get_num_decls(); - unsigned offset = all_vars.size(); - for (unsigned j = 0; j < num_decls; ++j) { - all_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j))); - } - var_subst varsubst(m, false); - varsubst(m_Bs[i].get(), num_decls, (expr**)(all_vars.c_ptr() + offset), C); - fmls.push_back(C); - } - conjs.push_back(m_A); - conjs.push_back(m.mk_not(m.mk_and(fmls.size(), fmls.c_ptr()))); - // add previous instances. - expr* r = m.mk_and(m_Bs.size(), m_Bs.c_ptr()); - m_trail.push_back(r); - expr* inst; - if (!m_bound.find(m_current_rule, r, inst)) { - TRACE("pdr", tout << "did not find: " << mk_pp(r, m) << "\n";); - m_trail.push_back(r);Newton Sanches - inst = m.mk_true(); - m_bound.insert(m_current_rule, r, inst); - } - else { - TRACE("pdr", tout << "blocking: " << mk_pp(inst, m) << "\n";); - conjs.push_back(inst); - } - C = m.mk_and(conjs.size(), conjs.c_ptr()); - lbool result = qe.first_elim(all_vars.size(), all_vars.c_ptr(), C, defs); - TRACE("pdr", tout << mk_pp(C.get(), m) << "\n" << result << "\n";); - if (result != l_true) { - return false; - } - inst = m.mk_and(inst, m.mk_not(C)); - m_trail.push_back(inst); - m_bound.insert(m_current_rule, r, inst); - TRACE("pdr", - tout << "Instantiating\n"; - for (unsigned i = 0; i < defs.size(); ++i) { - tout << defs.var(i)->get_name() << " " << mk_pp(defs.def(i), m) << "\n"; - } - ); - expr_substitution sub(m); - for (unsigned i = 0; i < defs.size(); ++i) { - sub.insert(m.mk_const(defs.var(i)), defs.def(i)); - } - scoped_ptr rep = mk_default_expr_replacer(m); - rep->set_substitution(&sub); - for (unsigned i = 0; i < all_vars.size(); ++i) { - expr_ref tmp(all_vars[i].get(), m); - (*rep)(tmp); - all_vars[i] = to_app(tmp); - } - unsigned offset = 0; - for (unsigned i = 0; i < m_Bs.size(); ++i) { - quantifier* q = qs[i]; - unsigned num_decls = q->get_num_decls(); - expr_ref_vector new_binding(m); - for (unsigned j = 0; j < num_decls; ++j) { - new_binding.push_back(all_vars[offset+j].get()); - } - offset += num_decls; - add_binding(q, new_binding); - } - return true; - } - - bool quantifier_model_checker::find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level) { - bool found_instance = false; - expr_ref C(m); - front_end_params fparams; - smt::kernel solver(m, fparams); - solver.assert_expr(m_A); - for (unsigned i = 0; i < m_Bs.size(); ++i) { - expr_ref_vector fresh_vars(m); - quantifier* q = qs[i]; - for (unsigned j = 0; j < q->get_num_decls(); ++j) { - fresh_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j))); - } - var_subst varsubst(m, false); - varsubst(m_Bs[i].get(), fresh_vars.size(), fresh_vars.c_ptr(), C); - TRACE("pdr", tout << "updated propagation formula: " << mk_pp(C,m) << "\n";); - - solver.push(); - // TBD: what to do with the different tags when unfolding the same predicate twice? - solver.assert_expr(m.mk_not(C)); - lbool result = solver.check(); - if (result == l_true) { - found_instance = true; - model_ref mr; - solver.get_model(mr); - TRACE("pdr", model_smt2_pp(tout, m, *mr, 0);); - - expr_ref_vector insts(m); - for (unsigned j = 0; j < fresh_vars.size(); ++j) { - expr* interp = mr->get_const_interp(to_app(fresh_vars[j].get())->get_decl()); - if (interp) { - insts.push_back(interp); - } - else { - insts.push_back(fresh_vars[j].get()); - } - TRACE("pdr", tout << mk_pp(insts.back(), m) << "\n";); - } - add_binding(q, insts); - } - solver.pop(1); - } - return found_instance; - } - - -#endif - diff --git a/src/muz_qe/pdr_quantifiers.h b/src/muz_qe/pdr_quantifiers.h index bae323cf8..2a7dcaf2c 100644 --- a/src/muz_qe/pdr_quantifiers.h +++ b/src/muz_qe/pdr_quantifiers.h @@ -33,24 +33,27 @@ namespace pdr { class model_node; class pred_transformer; class context; - - + class quantifier_model_checker { context& m_ctx; ast_manager& m; obj_map& m_quantifiers; datalog::rule_set& m_rules; - expr_ref_vector m_trail; + + obj_map m_reachable; // set of reachable states expr_ref m_A; expr_ref_vector m_Bs; pred_transformer* m_current_pt; datalog::rule const* m_current_rule; model_node* m_current_node; + bool m_rules_model_check; app_ref_vector m_instantiations; ptr_vector m_instantiated_rules; void model_check_node(model_node& node); + void weaken_under_approximation(); + bool find_instantiations(quantifier_ref_vector const& qs, unsigned level); bool find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level); @@ -79,6 +82,18 @@ namespace pdr { bool model_check(model_node& root); + void add_over_approximations(quantifier_ref_vector& qis, model_node& n); + + void add_under_approximations(quantifier_ref_vector& qis, model_node& n); + + void add_approximations(quantifier_ref_vector& qis, model_node& n, bool is_over); + + expr_ref get_reachable(func_decl* f); + + void update_reachable(func_decl* f, expr* e); + + expr_ref strongest_post_condition(datalog::rule& r); + public: quantifier_model_checker( context& ctx, @@ -89,9 +104,14 @@ namespace pdr { m(m), m_quantifiers(quantifiers), m_rules(rules), - m_trail(m), m_A(m), m_Bs(m), - m_current_pt(0), m_current_rule(0), - m_current_node(0), m_instantiations(m) {} + m_A(m), + m_Bs(m), + m_current_pt(0), + m_current_rule(0), + m_current_node(0), + m_instantiations(m) {} + + ~quantifier_model_checker(); bool check(); }; diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index 6baa7ad80..43008a1d6 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -74,462 +74,489 @@ public: }; -class der2 { - ast_manager & m; - is_variable_proc* m_is_variable; - var_subst m_subst; - expr_ref_buffer m_new_exprs; - - ptr_vector m_map; - int_vector m_pos2var; - ptr_vector m_inx2var; - unsigned_vector m_order; - expr_ref_vector m_subst_map; - expr_ref_buffer m_new_args; - th_rewriter m_rewriter; - - void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsigned_vector & order) { - order.reset(); +namespace eq { + class der { + ast_manager & m; + is_variable_proc* m_is_variable; + var_subst m_subst; + expr_ref_buffer m_new_exprs; - // eliminate self loops, and definitions containing quantifiers. - bool found = false; - for (unsigned i = 0; i < definitions.size(); i++) { - var * v = vars[i]; - expr * t = definitions[i]; - if (t == 0 || has_quantifiers(t) || occurs(v, t)) - definitions[i] = 0; - else - found = true; // found at least one candidate - } + ptr_vector m_map; + int_vector m_pos2var; + ptr_vector m_inx2var; + unsigned_vector m_order; + expr_ref_vector m_subst_map; + expr_ref_buffer m_new_args; + th_rewriter m_rewriter; - if (!found) - return; - - typedef std::pair frame; - svector todo; - - expr_fast_mark1 visiting; - expr_fast_mark2 done; - - unsigned vidx, num; - - for (unsigned i = 0; i < definitions.size(); i++) { - if (definitions[i] == 0) - continue; - var * v = vars[i]; - SASSERT(v->get_idx() == i); - SASSERT(todo.empty()); - todo.push_back(frame(v, 0)); - while (!todo.empty()) { - start: - frame & fr = todo.back(); - expr * t = fr.first; - if (t->get_ref_count() > 1 && done.is_marked(t)) { - todo.pop_back(); + void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsigned_vector & order) { + order.reset(); + + // eliminate self loops, and definitions containing quantifiers. + bool found = false; + for (unsigned i = 0; i < definitions.size(); i++) { + var * v = vars[i]; + expr * t = definitions[i]; + if (t == 0 || has_quantifiers(t) || occurs(v, t)) + definitions[i] = 0; + else + found = true; // found at least one candidate + } + + if (!found) + return; + + typedef std::pair frame; + svector todo; + + expr_fast_mark1 visiting; + expr_fast_mark2 done; + + unsigned vidx, num; + + for (unsigned i = 0; i < definitions.size(); i++) { + if (definitions[i] == 0) continue; - } - switch (t->get_kind()) { - case AST_VAR: - vidx = to_var(t)->get_idx(); - if (fr.second == 0) { - CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";); - // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula. - if (definitions.get(vidx, 0) != 0) { - if (visiting.is_marked(t)) { - // cycle detected: remove t - visiting.reset_mark(t); - definitions[vidx] = 0; - } - else { - visiting.mark(t); - fr.second = 1; - todo.push_back(frame(definitions[vidx], 0)); - goto start; - } - } + var * v = vars[i]; + SASSERT(v->get_idx() == i); + SASSERT(todo.empty()); + todo.push_back(frame(v, 0)); + while (!todo.empty()) { + start: + frame & fr = todo.back(); + expr * t = fr.first; + if (t->get_ref_count() > 1 && done.is_marked(t)) { + todo.pop_back(); + continue; } - else { - SASSERT(fr.second == 1); - if (definitions.get(vidx, 0) != 0) { - visiting.reset_mark(t); - order.push_back(vidx); + switch (t->get_kind()) { + case AST_VAR: + vidx = to_var(t)->get_idx(); + if (fr.second == 0) { + CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";); + // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula. + if (definitions.get(vidx, 0) != 0) { + if (visiting.is_marked(t)) { + // cycle detected: remove t + visiting.reset_mark(t); + definitions[vidx] = 0; + } + else { + visiting.mark(t); + fr.second = 1; + todo.push_back(frame(definitions[vidx], 0)); + goto start; + } + } } else { - // var was removed from the list of candidate vars to elim cycle - // do nothing + SASSERT(fr.second == 1); + if (definitions.get(vidx, 0) != 0) { + visiting.reset_mark(t); + order.push_back(vidx); + } + else { + // var was removed from the list of candidate vars to elim cycle + // do nothing + } } + if (t->get_ref_count() > 1) + done.mark(t); + todo.pop_back(); + break; + case AST_QUANTIFIER: + UNREACHABLE(); + todo.pop_back(); + break; + case AST_APP: + num = to_app(t)->get_num_args(); + while (fr.second < num) { + expr * arg = to_app(t)->get_arg(fr.second); + fr.second++; + if (arg->get_ref_count() > 1 && done.is_marked(arg)) + continue; + todo.push_back(frame(arg, 0)); + goto start; + } + if (t->get_ref_count() > 1) + done.mark(t); + todo.pop_back(); + break; + default: + UNREACHABLE(); + todo.pop_back(); + break; } - if (t->get_ref_count() > 1) - done.mark(t); - todo.pop_back(); - break; - case AST_QUANTIFIER: - UNREACHABLE(); - todo.pop_back(); - break; - case AST_APP: - num = to_app(t)->get_num_args(); - while (fr.second < num) { - expr * arg = to_app(t)->get_arg(fr.second); - fr.second++; - if (arg->get_ref_count() > 1 && done.is_marked(arg)) - continue; - todo.push_back(frame(arg, 0)); - goto start; - } - if (t->get_ref_count() > 1) - done.mark(t); - todo.pop_back(); - break; - default: - UNREACHABLE(); - todo.pop_back(); - break; } } } - } - - bool is_variable(expr * e) const { - return (*m_is_variable)(e); - } - - bool is_neg_var(ast_manager & m, expr * e) { - expr* e1; - return m.is_not(e, e1) && is_variable(e1); - } - - - /** - \brief Return true if e can be viewed as a variable disequality. - Store the variable id in v and the definition in t. - For example: - - if e is (not (= (VAR 1) T)), then v assigned to 1, and t to T. - if e is (iff (VAR 2) T), then v is assigned to 2, and t to (not T). - (not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))), - and can be viewed as a disequality. - */ - bool is_var_diseq(expr * e, var * & v, expr_ref & t) { - expr* e1; - if (m.is_not(e, e1)) { - return is_var_eq(e, v, t); - } - else if (is_var_eq(e, v, t) && m.is_bool(v)) { - bool_rewriter(m).mk_not(t, t); - m_new_exprs.push_back(t); - return true; - } - else { - return false; - } - } - - - - /** - \brief Return true if e can be viewed as a variable equality. - */ - - bool is_var_eq(expr * e, var * & v, expr_ref & t) { - expr* lhs, *rhs; - // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases - if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) { - // (iff (not VAR) t) (iff t (not VAR)) cases - if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) { - if (!is_neg_var(m, lhs)) { - std::swap(lhs, rhs); - } - if (!is_neg_var(m, lhs)) { - return false; - } - v = to_var(lhs); - t = m.mk_not(rhs); + bool is_variable(expr * e) const { + return (*m_is_variable)(e); + } + + bool is_neg_var(ast_manager & m, expr * e) { + expr* e1; + return m.is_not(e, e1) && is_variable(e1); + } + + + /** + \brief Return true if e can be viewed as a variable disequality. + Store the variable id in v and the definition in t. + For example: + + if e is (not (= (VAR 1) T)), then v assigned to 1, and t to T. + if e is (iff (VAR 2) T), then v is assigned to 2, and t to (not T). + (not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))), + and can be viewed as a disequality. + */ + bool is_var_diseq(expr * e, var * & v, expr_ref & t) { + expr* e1; + if (m.is_not(e, e1)) { + return is_var_eq(e, v, t); + } + else if (is_var_eq(e, v, t) && m.is_bool(v)) { + bool_rewriter(m).mk_not(t, t); m_new_exprs.push_back(t); + return true; + } + else { + return false; + } + } + + + + /** + \brief Return true if e can be viewed as a variable equality. + */ + + bool is_var_eq(expr * e, var * & v, expr_ref & t) { + expr* lhs, *rhs; + + // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases + if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) { + // (iff (not VAR) t) (iff t (not VAR)) cases + if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) { + if (!is_neg_var(m, lhs)) { + std::swap(lhs, rhs); + } + if (!is_neg_var(m, lhs)) { + return false; + } + v = to_var(lhs); + t = m.mk_not(rhs); + m_new_exprs.push_back(t); + TRACE("der", tout << mk_pp(e, m) << "\n";); + return true; + } + if (!is_variable(lhs)) + std::swap(lhs, rhs); + if (!is_variable(lhs)) + return false; + v = to_var(lhs); + t = rhs; TRACE("der", tout << mk_pp(e, m) << "\n";); return true; } - if (!is_variable(lhs)) - std::swap(lhs, rhs); - if (!is_variable(lhs)) + + // (ite cond (= VAR t) (= VAR t2)) case + expr* cond, *e2, *e3; + if (m.is_ite(e, cond, e2, e3)) { + if (is_var_eq(e2, v, t)) { + expr_ref t2(m); + var* v2; + if (is_var_eq(e3, v2, t2) && v2 == v) { + t = m.mk_ite(cond, t, t2); + m_new_exprs.push_back(t); + return true; + } + } return false; - v = to_var(lhs); - t = rhs; - TRACE("der", tout << mk_pp(e, m) << "\n";); - return true; + } + + // VAR = true case + if (is_variable(e)) { + t = m.mk_true(); + v = to_var(e); + TRACE("der", tout << mk_pp(e, m) << "\n";); + return true; + } + + // VAR = false case + if (is_neg_var(m, e)) { + t = m.mk_false(); + v = to_var(to_app(e)->get_arg(0)); + TRACE("der", tout << mk_pp(e, m) << "\n";); + return true; + } + + return false; } - // (ite cond (= VAR t) (= VAR t2)) case - expr* cond, *e2, *e3; - if (m.is_ite(e, cond, e2, e3)) { - if (is_var_eq(e2, v, t)) { - expr_ref t2(m); - var* v2; - if (is_var_eq(e3, v2, t2) && v2 == v) { - t = m.mk_ite(cond, t, t2); - m_new_exprs.push_back(t); + + bool is_var_def(bool check_eq, expr* e, var*& v, expr_ref& t) { + if (check_eq) { + return is_var_eq(e, v, t); + } + else { + return is_var_diseq(e, v, t); + } + } + + void get_elimination_order() { + m_order.reset(); + + TRACE("top_sort", + tout << "DEFINITIONS: " << std::endl; + for(unsigned i = 0; i < m_map.size(); i++) + if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m) << std::endl; + ); + + der_sort_vars(m_inx2var, m_map, m_order); + + TRACE("der", + tout << "Elimination m_order:" << std::endl; + for(unsigned i=0; iget_expr(); + if ((q->is_forall() && m.is_or(e)) || + (q->is_exists() && m.is_and(e))) { + num_args = to_app(e)->get_num_args(); + args = to_app(e)->get_args(); + } + } + + void apply_substitution(quantifier * q, expr_ref & r) { + + expr * e = q->get_expr(); + unsigned num_args = 1; + expr* const* args = &e; + flatten_args(q, num_args, args); + bool_rewriter rw(m); + + // get a new expression + m_new_args.reset(); + for(unsigned i = 0; i < num_args; i++) { + int x = m_pos2var[i]; + if (x == -1 || m_map[x] == 0) { + m_new_args.push_back(args[i]); + } + } + + expr_ref t(m); + if (q->is_forall()) { + rw.mk_or(m_new_args.size(), m_new_args.c_ptr(), t); + } + else { + rw.mk_and(m_new_args.size(), m_new_args.c_ptr(), t); + } + expr_ref new_e(m); + m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e); + + // don't forget to update the quantifier patterns + expr_ref_buffer new_patterns(m); + expr_ref_buffer new_no_patterns(m); + for (unsigned j = 0; j < q->get_num_patterns(); j++) { + expr_ref new_pat(m); + m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_pat); + new_patterns.push_back(new_pat); + } + + for (unsigned j = 0; j < q->get_num_no_patterns(); j++) { + expr_ref new_nopat(m); + m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_nopat); + new_no_patterns.push_back(new_nopat); + } + + r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), + new_no_patterns.size(), new_no_patterns.c_ptr(), new_e); + } + + void reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr) { + expr * e = q->get_expr(); + is_variable_test is_v(q->get_num_decls()); + set_is_variable_proc(is_v); + unsigned num_args = 1; + expr* const* args = &e; + flatten_args(q, num_args, args); + + unsigned def_count = 0; + unsigned largest_vinx = 0; + + find_definitions(num_args, args, q->is_exists(), def_count, largest_vinx); + + if (def_count > 0) { + get_elimination_order(); + SASSERT(m_order.size() <= def_count); // some might be missing because of cycles + + if (!m_order.empty()) { + create_substitution(largest_vinx + 1); + apply_substitution(q, r); + } + else { + r = q; + } + } + else { + TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";); + r = q; + } + + if (m.proofs_enabled()) { + pr = r == q ? 0 : m.mk_der(q, r); + } + } + + void elim_unused_vars(expr_ref& r, proof_ref &pr) { + if (is_quantifier(r)) { + quantifier * q = to_quantifier(r); + ::elim_unused_vars(m, q, r); + if (m.proofs_enabled()) { + proof * p1 = m.mk_elim_unused_vars(q, r); + pr = m.mk_transitivity(pr, p1); + } + } + } + + void find_definitions(unsigned num_args, expr* const* args, bool is_exists, unsigned& def_count, unsigned& largest_vinx) { + var * v = 0; + expr_ref t(m); + def_count = 0; + largest_vinx = 0; + m_map.reset(); + m_pos2var.reset(); + m_inx2var.reset(); + m_pos2var.reserve(num_args, -1); + + // Find all definitions + for (unsigned i = 0; i < num_args; i++) { + if (is_var_def(is_exists, args[i], v, t)) { + unsigned idx = v->get_idx(); + if(m_map.get(idx, 0) == 0) { + m_map.reserve(idx + 1, 0); + m_inx2var.reserve(idx + 1, 0); + m_map[idx] = t; + m_inx2var[idx] = v; + m_pos2var[i] = idx; + def_count++; + largest_vinx = std::max(idx, largest_vinx); + } + } + } + } + + bool reduce_var_set(expr_ref_vector& conjs) { + unsigned def_count = 0; + unsigned largest_vinx = 0; + + find_definitions(conjs.size(), conjs.c_ptr(), true, def_count, largest_vinx); + + if (def_count > 0) { + get_elimination_order(); + SASSERT(m_order.size() <= def_count); // some might be missing because of cycles + + if (!m_order.empty()) { + expr_ref r(m), new_r(m); + r = m.mk_and(conjs.size(), conjs.c_ptr()); + create_substitution(largest_vinx + 1); + m_subst(r, m_subst_map.size(), m_subst_map.c_ptr(), new_r); + m_rewriter(new_r); + conjs.reset(); + datalog::flatten_and(new_r, conjs); return true; } } return false; } - - // VAR = true case - if (is_variable(e)) { - t = m.mk_true(); - v = to_var(e); - TRACE("der", tout << mk_pp(e, m) << "\n";); - return true; - } - - // VAR = false case - if (is_neg_var(m, e)) { - t = m.mk_false(); - v = to_var(to_app(e)->get_arg(0)); - TRACE("der", tout << mk_pp(e, m) << "\n";); - return true; - } - - return false; - } - - bool is_var_def(bool check_eq, expr* e, var*& v, expr_ref& t) { - if (check_eq) { - return is_var_eq(e, v, t); - } - else { - return is_var_diseq(e, v, t); - } - } - - void get_elimination_order() { - m_order.reset(); - - TRACE("top_sort", - tout << "DEFINITIONS: " << std::endl; - for(unsigned i = 0; i < m_map.size(); i++) - if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m) << std::endl; - ); + public: + der(ast_manager & m): m(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m) {} - der_sort_vars(m_inx2var, m_map, m_order); + void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} - TRACE("der", - tout << "Elimination m_order:" << std::endl; - for(unsigned i=0; iget_expr(); - if ((q->is_forall() && m.is_or(e)) || - (q->is_exists() && m.is_and(e))) { - num_args = to_app(e)->get_num_args(); - args = to_app(e)->get_args(); - } - } - - void apply_substitution(quantifier * q, expr_ref & r) { - - expr * e = q->get_expr(); - unsigned num_args = 1; - expr* const* args = &e; - flatten_args(q, num_args, args); - bool_rewriter rw(m); - - // get a new expression - m_new_args.reset(); - for(unsigned i = 0; i < num_args; i++) { - int x = m_pos2var[i]; - if (x == -1 || m_map[x] == 0) { - m_new_args.push_back(args[i]); + void operator()(quantifier * q, expr_ref & r, proof_ref & pr) { + TRACE("der", tout << mk_pp(q, m) << "\n";); + pr = 0; + r = q; + reduce_quantifier(q, r, pr); + if (r != q) { + elim_unused_vars(r, pr); } } - expr_ref t(m); - if (q->is_forall()) { - rw.mk_or(m_new_args.size(), m_new_args.c_ptr(), t); - } - else { - rw.mk_and(m_new_args.size(), m_new_args.c_ptr(), t); - } - expr_ref new_e(m); - m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e); - - // don't forget to update the quantifier patterns - expr_ref_buffer new_patterns(m); - expr_ref_buffer new_no_patterns(m); - for (unsigned j = 0; j < q->get_num_patterns(); j++) { - expr_ref new_pat(m); - m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_pat); - new_patterns.push_back(new_pat); - } - - for (unsigned j = 0; j < q->get_num_no_patterns(); j++) { - expr_ref new_nopat(m); - m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_nopat); - new_no_patterns.push_back(new_nopat); - } - - r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), - new_no_patterns.size(), new_no_patterns.c_ptr(), new_e); - } - - void reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr) { - expr * e = q->get_expr(); - is_variable_test is_v(q->get_num_decls()); - set_is_variable_proc(is_v); - unsigned num_args = 1; - expr* const* args = &e; - flatten_args(q, num_args, args); - - unsigned def_count = 0; - unsigned largest_vinx = 0; - - find_definitions(num_args, args, q->is_exists(), def_count, largest_vinx); - - if (def_count > 0) { - get_elimination_order(); - SASSERT(m_order.size() <= def_count); // some might be missing because of cycles - - if (!m_order.empty()) { - create_substitution(largest_vinx + 1); - apply_substitution(q, r); - } - else { - r = q; - } - } - else { - TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";); + void reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr) { r = q; - } - - if (m.proofs_enabled()) { - pr = r == q ? 0 : m.mk_der(q, r); - } - } - - void elim_unused_vars(expr_ref& r, proof_ref &pr) { - if (is_quantifier(r)) { - quantifier * q = to_quantifier(r); - ::elim_unused_vars(m, q, r); - if (m.proofs_enabled()) { - proof * p1 = m.mk_elim_unused_vars(q, r); - pr = m.mk_transitivity(pr, p1); - } - } - } - - void find_definitions(unsigned num_args, expr* const* args, bool is_exists, unsigned& def_count, unsigned& largest_vinx) { - var * v = 0; - expr_ref t(m); - def_count = 0; - largest_vinx = 0; - m_map.reset(); - m_pos2var.reset(); - m_inx2var.reset(); - m_pos2var.reserve(num_args, -1); - - // Find all definitions - for (unsigned i = 0; i < num_args; i++) { - if (is_var_def(is_exists, args[i], v, t)) { - unsigned idx = v->get_idx(); - if(m_map.get(idx, 0) == 0) { - m_map.reserve(idx + 1, 0); - m_inx2var.reserve(idx + 1, 0); - m_map[idx] = t; - m_inx2var[idx] = v; - m_pos2var[i] = idx; - def_count++; - largest_vinx = std::max(idx, largest_vinx); + // Keep applying reduce_quantifier1 until r doesn't change anymore + do { + proof_ref curr_pr(m); + q = to_quantifier(r); + reduce_quantifier1(q, r, curr_pr); + if (m.proofs_enabled()) { + pr = m.mk_transitivity(pr, curr_pr); } - } - } - } - - bool reduce_var_set(expr_ref_vector& conjs) { - unsigned def_count = 0; - unsigned largest_vinx = 0; - - find_definitions(conjs.size(), conjs.c_ptr(), true, def_count, largest_vinx); - - if (def_count > 0) { - get_elimination_order(); - SASSERT(m_order.size() <= def_count); // some might be missing because of cycles + } while (q != r && is_quantifier(r)); - if (!m_order.empty()) { - expr_ref r(m), new_r(m); - r = m.mk_and(conjs.size(), conjs.c_ptr()); - create_substitution(largest_vinx + 1); - m_subst(r, m_subst_map.size(), m_subst_map.c_ptr(), new_r); - m_rewriter(new_r); - conjs.reset(); - datalog::flatten_and(new_r, conjs); - return true; - } + m_new_exprs.reset(); } - return false; - } - - -public: - der2(ast_manager & m): m(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m) {} - - void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} - - void operator()(quantifier * q, expr_ref & r, proof_ref & pr) { - TRACE("der", tout << mk_pp(q, m) << "\n";); - pr = 0; - r = q; - reduce_quantifier(q, r, pr); - if (r != q) { - elim_unused_vars(r, pr); - } - } - - void reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr) { - r = q; - // Keep applying reduce_quantifier1 until r doesn't change anymore - do { - proof_ref curr_pr(m); - q = to_quantifier(r); - reduce_quantifier1(q, r, curr_pr); - if (m.proofs_enabled()) { - pr = m.mk_transitivity(pr, curr_pr); - } - } while (q != r && is_quantifier(r)); - m_new_exprs.reset(); - } + void operator()(expr_ref_vector& r) { + while (reduce_var_set(r)) ; + m_new_exprs.reset(); + } + + ast_manager& get_manager() const { return m; } + }; +}; // namespace eq - void operator()(expr_ref_vector& r) { - while (reduce_var_set(r)) ; - m_new_exprs.reset(); - } +// ------------------------------------------------------------ +// basic destructive equality (and disequality) resolution for arrays. + +namespace ar { + class der { + ast_manager& m; + is_variable_proc* m_is_variable; + + bool is_variable(expr * e) const { + return (*m_is_variable)(e); + } + + public: + + der(ast_manager& m): m(m), m_is_variable(0) {} + + void operator()(expr_ref_vector& fmls) { + IF_VERBOSE(1, verbose_stream() << "Todo: eliminate arrays\n";); + } + + void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} + + }; +}; // namespace ar - ast_manager& get_manager() const { return m; } -}; // ------------------------------------------------------------ // fm_tactic adapted to eliminate designated de-Brujin indices. @@ -1808,7 +1835,6 @@ namespace fm { void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} - void operator()(expr_ref_vector& fmls) { init(fmls); init_use_list(fmls); @@ -1873,12 +1899,13 @@ namespace fm { class qe_lite::impl { ast_manager& m; - der2 m_der; params_ref m_params; + eq::der m_der; fm::fm m_fm; + ar::der m_array_der; public: - impl(ast_manager& m): m(m), m_der(m), m_fm(m, m_params) {} + impl(ast_manager& m): m(m), m_der(m), m_fm(m, m_params), m_array_der(m) {} void operator()(app_ref_vector& vars, expr_ref& fml) { if (vars.empty()) { @@ -1928,10 +1955,16 @@ public: } void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) { - expr_ref_vector conjs(m); - conjs.push_back(fml); - (*this)(index_set, index_of_bound, conjs); - bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), fml); + expr_ref_vector disjs(m); + datalog::flatten_or(fml, disjs); + for (unsigned i = 0; i < disjs.size(); ++i) { + expr_ref_vector conjs(m); + conjs.push_back(disjs[i].get()); + (*this)(index_set, index_of_bound, conjs); + bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), fml); + disjs[i] = fml; + } + bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), fml); } @@ -1941,9 +1974,11 @@ public: TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";); IF_VERBOSE(3, for (unsigned i = 0; i < fmls.size(); ++i) verbose_stream() << mk_pp(fmls[i].get(), m) << "\n";); m_der.set_is_variable_proc(is_var); - m_der(fmls); m_fm.set_is_variable_proc(is_var); + m_array_der.set_is_variable_proc(is_var); + m_der(fmls); m_fm(fmls); + m_array_der(fmls); TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";); } diff --git a/src/muz_qe/qe_lite.h b/src/muz_qe/qe_lite.h index 3a23c7188..3ffbf8fad 100644 --- a/src/muz_qe/qe_lite.h +++ b/src/muz_qe/qe_lite.h @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2010 Microsoft Corporation +Copyright (c) 2012 Microsoft Corporation Module Name: From f78e595b566cbb9d6f5d55311a046268dd97c98c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 1 Dec 2012 15:51:33 +0000 Subject: [PATCH 5/5] Added QF_FPABV logic, default tactic, and the asIEEEBV conversion function. Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 30 +++++++++++-- src/ast/float_decl_plugin.h | 9 +++- src/ast/rewriter/float_rewriter.cpp | 5 +++ src/ast/rewriter/float_rewriter.h | 2 + src/cmd_context/cmd_context.cpp | 6 ++- src/tactic/fpa/fpa2bv_converter.cpp | 45 +++++++++++++++++-- src/tactic/fpa/fpa2bv_converter.h | 1 + src/tactic/fpa/fpa2bv_rewriter.h | 1 + src/tactic/fpa/qffpa_tactic.h | 1 + src/tactic/portfolio/smt_strategic_solver.cpp | 1 + 10 files changed, 90 insertions(+), 11 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 7cf8f32bd..dbe7d5232 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -348,13 +348,13 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, // When the bv_decl_plugin is installed, then we know how to convert 3 bit-vectors into a float! sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); symbol name("asFloat"); - return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } else { // .. Otherwise we only know how to convert rationals/reals. if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) m_manager->raise_exception("expecting two integer parameters to asFloat"); - if (arity != 2 && arity != 3) + if (arity != 2 && arity != 3) m_manager->raise_exception("invalid number of arguments to asFloat operator"); if (!is_rm_sort(domain[0]) || domain[1] != m_real_sort) m_manager->raise_exception("sort mismatch"); @@ -373,6 +373,23 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, } } +func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (!m_bv_plugin) + m_manager->raise_exception("asIEEEBV unsupported; use a logic with BV support"); + if (arity != 1) + m_manager->raise_exception("invalid number of arguments to asIEEEBV"); + if (!is_float_sort(domain[0])) + m_manager->raise_exception("sort mismatch"); + + // When the bv_decl_plugin is installed, then we know how to convert a float to an IEEE bit-vector. + unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int(); + parameter ps[] = { parameter(float_sz) }; + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps); + symbol name("asIEEEBV"); + return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); +} + func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { switch (k) { @@ -420,6 +437,8 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_rm_unary_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_FUSED_MA: return mk_fused_ma(k, num_parameters, parameters, arity, domain, range); + case OP_TO_IEEE_BV: + return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; @@ -462,7 +481,10 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("min", OP_FLOAT_MIN)); op_names.push_back(builtin_name("max", OP_FLOAT_MAX)); - op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT)); + op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT)); + + if (m_bv_plugin) + op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV)); } void float_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 416275306..c4503349b 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -67,6 +67,7 @@ enum float_op_kind { OP_FLOAT_IS_SIGN_MINUS, OP_TO_FLOAT, + OP_TO_IEEE_BV, LAST_FLOAT_OP }; @@ -118,6 +119,8 @@ class float_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_to_float(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); @@ -159,7 +162,7 @@ class float_util { ast_manager & m_manager; float_decl_plugin * m_plugin; family_id m_fid; - arith_util m_a_util; + arith_util m_a_util; public: float_util(ast_manager & m); ~float_util(); @@ -209,7 +212,7 @@ public: bool is_to_float(expr * n) { return is_app_of(n, m_fid, OP_TO_FLOAT); } - app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_TO_FLOAT, arg1, arg2); } + app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_TO_FLOAT, arg1, arg2); } app * mk_add(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_ADD, arg1, arg2, arg3); } app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); } app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); } @@ -238,6 +241,8 @@ public: app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); } bool is_uminus(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_UMINUS); } + + app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_TO_IEEE_BV, arg1); } }; #endif diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index ad0709423..9678af216 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -59,6 +59,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_NZERO: SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break; case OP_FLOAT_IS_PZERO: SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break; case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break; + case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; } return st; } @@ -439,3 +440,7 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result return BR_FAILED; } + +br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) { + return BR_FAILED; +} \ No newline at end of file diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index e4258895d..7c86a5bc3 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -67,6 +67,8 @@ public: br_status mk_is_nzero(expr * arg1, expr_ref & result); br_status mk_is_pzero(expr * arg1, expr_ref & result); br_status mk_is_sign_minus(expr * arg1, expr_ref & result); + + br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); }; #endif diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index afcac48ac..9ec11d085 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -460,6 +460,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "LIA" || s == "LRA" || s == "QF_FPA" || + s == "QF_FPABV" || s == "HORN"; } @@ -478,6 +479,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const { s == "QF_ABV" || s == "QF_AUFBV" || s == "QF_BVRE" || + s == "QF_FPABV" || s == "HORN"; } @@ -502,7 +504,7 @@ bool cmd_context::logic_has_seq() const { } bool cmd_context::logic_has_floats() const { - return !has_logic() || m_logic == "QF_FPA"; + return !has_logic() || m_logic == "QF_FPA" || m_logic == "QF_FPABV"; } bool cmd_context::logic_has_array_core(symbol const & s) const { @@ -599,7 +601,7 @@ bool cmd_context::supported_logic(symbol const & s) const { logic_has_arith_core(s) || logic_has_bv_core(s) || logic_has_array_core(s) || logic_has_seq_core(s) || logic_has_horn(s) || - s == "QF_FPA"; + s == "QF_FPA" || s == "QF_FPABV"; } void cmd_context::set_logic(symbol const & s) { diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 77ff50e9b..21d5a2d23 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1399,6 +1399,13 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a } } +void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + expr * sgn, * s, * e; + split(args[0], sgn, s, e); + result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, s), e); +} + void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(to_app(e)->get_num_args() == 3); @@ -2035,7 +2042,8 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { tout << bv_mdl->get_constant(i)->get_name() << " --> " << mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl; ); - + + obj_hashtable seen; for (obj_map::iterator it = m_const2bv.begin(); it != m_const2bv.end(); @@ -2053,6 +2061,10 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { expr * sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl()); expr * exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl()); + seen.insert(to_app(a->get_arg(0))->get_decl()); + seen.insert(to_app(a->get_arg(1))->get_decl()); + seen.insert(to_app(a->get_arg(2))->get_decl()); + if (!sgn && !sig && !exp) continue; @@ -2080,7 +2092,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z); float_mdl->register_decl(var, fu.mk_value(fp_val)); - + mpzm.del(sig_z); } @@ -2104,9 +2116,36 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break; case BV_RM_TO_ZERO: default: float_mdl->register_decl(var, fu.mk_round_toward_zero()); - } + } + seen.insert(var); } } fu.fm().del(fp_val); + + // Keep all the non-float constants. + unsigned sz = bv_mdl->get_num_constants(); + for (unsigned i = 0; i < sz; i++) + { + func_decl * c = bv_mdl->get_constant(i); + if (seen.contains(c)) + continue; + float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); + } + + // And keep everything else + sz = bv_mdl->get_num_functions(); + for (unsigned i = 0; i < sz; i++) + { + func_decl * c = bv_mdl->get_function(i); + float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); + } + + sz = bv_mdl->get_num_uninterpreted_sorts(); + for (unsigned i = 0; i < sz; i++) + { + sort * s = bv_mdl->get_uninterpreted_sort(i); + ptr_vector u = bv_mdl->get_universe(s); + float_mdl->register_usort(s, u.size(), u.c_ptr()); + } } diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 291120e92..1ee374941 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -100,6 +100,7 @@ public: void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); fpa2bv_model_converter * mk_model_converter(); diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index 62c6f1a2d..91682c6e1 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -129,6 +129,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE; + case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); diff --git a/src/tactic/fpa/qffpa_tactic.h b/src/tactic/fpa/qffpa_tactic.h index 660565463..8ca2183c1 100644 --- a/src/tactic/fpa/qffpa_tactic.h +++ b/src/tactic/fpa/qffpa_tactic.h @@ -27,6 +27,7 @@ class tactic; tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref()); /* ADD_TACTIC("qffpa", "(try to) solve goal using the tactic for QF_FPA.", "mk_qffpa_tactic(m, p)") + ADD_TACTIC("qffpabv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffpa_tactic(m, p)") */ #endif diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 4cf530b1e..7a274a830 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -79,6 +79,7 @@ static void init(strategic_solver * s) { s->set_tactic_for(symbol("UFBV"), alloc(ufbv_fct)); s->set_tactic_for(symbol("BV"), alloc(ufbv_fct)); s->set_tactic_for(symbol("QF_FPA"), alloc(qffpa_fct)); + s->set_tactic_for(symbol("QF_FPABV"), alloc(qffpa_fct)); s->set_tactic_for(symbol("HORN"), alloc(horn_fct)); }