mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

merged

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-01 16:36:24 -08:00
commit 32791204e7
28 changed files with 1114 additions and 742 deletions
Download patch file Download diff file Expand all files Collapse all files

50
examples/java/JavaExample.java
View file

@ -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());

77
scripts/update_api.py
View file

@ -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():
@ -494,12 +489,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 +548,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<jni.h>\n')
java_wrapper.write('#include<stdlib.h>\n')
@ -562,23 +558,55 @@ 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<T>(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<T>(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<T>(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<jlong>(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')
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, 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')
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;
@ -604,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
@ -635,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:

39
src/api/java/AST.java
View file

@ -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;
}
/**

35
src/api/java/Context.java
View file

@ -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;
}
/**
@ -525,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);
}
/**
@ -2908,21 +2907,6 @@ public class Context extends IDisposable
Native.toggleWarningMessages((enabled) ? true : false);
}
// /// <summary>
// /// A delegate which is executed when an error is raised.
// /// </summary>
// /// <remarks>
// /// Note that it is possible for memory leaks to occur if error handlers
// /// throw exceptions.
// /// </remarks>
// public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode,
// String errorString);
// /// <summary>
// /// The OnError event.
// /// </summary>
// public event ErrorHandler OnError = null;
/**
* Update a mutable configuration parameter. <remarks> 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);
}
/**

9
src/api/java/EnumSort.java
View file

@ -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);
}
};

15
src/api/java/Quantifier.java
View file

@ -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()));
}
}

13
src/api/java/Sort.java
View file

@ -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();
}
/**

2
src/api/java/Z3Object.java
View file

@ -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;
}

5
src/ast/ast.cpp
View file

@ -2637,12 +2637,13 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
ptr_buffer<expr> 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<expr> new_lits;
app const * cls = to_app(f1);

30
src/ast/float_decl_plugin.cpp
View file

@ -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<builtin_name> & 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<builtin_name> & sort_names, symbol const & logic) {

9
src/ast/float_decl_plugin.h
View file

@ -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

5
src/ast/rewriter/float_rewriter.cpp
View file

@ -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;
}

2
src/ast/rewriter/float_rewriter.h
View file

@ -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

6
src/cmd_context/cmd_context.cpp
View file

@ -469,6 +469,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "LIA" ||
s == "LRA" ||
s == "QF_FPA" ||
s == "QF_FPABV" ||
s == "HORN";
}
@ -487,6 +488,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";
}
@ -511,7 +513,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 {
@ -609,7 +611,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) {

2
src/muz_qe/dl_context.cpp
View file

@ -1768,7 +1768,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";
}
}

2
src/muz_qe/dl_mk_interp_tail_simplifier.cpp
View file

@ -463,7 +463,7 @@ namespace datalog {
if (r->has_quantifiers()) {
res = r;
return false;
return true;
}
start:

5
src/muz_qe/dl_util.h
View file

@ -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) {}

102
src/muz_qe/expr_safe_replace.cpp Normal file
View file

@ -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<expr,expr*> cache;
ptr_vector<expr> 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);
}

43
src/muz_qe/expr_safe_replace.h Normal file
View file

@ -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<expr, expr*> 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__ */

433
src/muz_qe/pdr_quantifiers.cpp
View file

@ -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<func_decl,expr*>::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<expr_ref_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<symbol, quantifier*, symbol_hash_proc, symbol_eq_proc> 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<expr_replacer> 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<symbol> 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<expr_replacer> 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<model_node> 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<expr_replacer> 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

32
src/muz_qe/pdr_quantifiers.h
View file

@ -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<datalog::rule const, quantifier_ref_vector*>& m_quantifiers;
datalog::rule_set& m_rules;
expr_ref_vector m_trail;
obj_map<func_decl, expr*> 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<datalog::rule const> 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();
};

889
src/muz_qe/qe_lite.cpp
View file

@ -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<expr> m_map;
int_vector m_pos2var;
ptr_vector<var> 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<var> & vars, ptr_vector<expr> & 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<expr> m_map;
int_vector m_pos2var;
ptr_vector<var> 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<expr *, unsigned> frame;
svector<frame> 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<var> & vars, ptr_vector<expr> & 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<expr *, unsigned> frame;
svector<frame> 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; i<m_order.size(); i++)
{
if (i != 0) tout << ",";
tout << m_order[i];
}
tout << std::endl;
);
}
void create_substitution(unsigned sz) {
m_subst_map.reset();
m_subst_map.resize(sz, 0);
for (unsigned i = 0; i < m_order.size(); i++) {
expr_ref cur(m_map[m_order[i]], m);
// do all the previous substitutions before inserting
expr_ref r(m);
m_subst(cur, m_subst_map.size(), m_subst_map.c_ptr(), r);
unsigned inx = sz - m_order[i]- 1;
SASSERT(m_subst_map[inx]==0);
m_subst_map[inx] = r;
}
}
void flatten_args(quantifier* q, unsigned& num_args, expr*const*& args) {
expr * e = q->get_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; i<m_order.size(); i++)
{
if (i != 0) tout << ",";
tout << m_order[i];
}
tout << std::endl;
);
}
void create_substitution(unsigned sz) {
m_subst_map.reset();
m_subst_map.resize(sz, 0);
for (unsigned i = 0; i < m_order.size(); i++) {
expr_ref cur(m_map[m_order[i]], m);
// do all the previous substitutions before inserting
expr_ref r(m);
m_subst(cur, m_subst_map.size(), m_subst_map.c_ptr(), r);
unsigned inx = sz - m_order[i]- 1;
SASSERT(m_subst_map[inx]==0);
m_subst_map[inx] = r;
}
}
void flatten_args(quantifier* q, unsigned& num_args, expr*const*& args) {
expr * e = q->get_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";);
}

2
src/muz_qe/qe_lite.h
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2010 Microsoft Corporation
Copyright (c) 2012 Microsoft Corporation
Module Name:

45
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -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<func_decl> seen;
for (obj_map<func_decl, expr*>::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<expr> u = bv_mdl->get_universe(s);
float_mdl->register_usort(s, u.size(), u.c_ptr());
}
}

1
src/tactic/fpa/fpa2bv_converter.h
View file

@ -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();

1
src/tactic/fpa/fpa2bv_rewriter.h
View file

@ -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;);

1
src/tactic/fpa/qffpa_tactic.h
View file

@ -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

1
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -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));
}