mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-04-23 14:50:51 +01:00
commit 3e5a702073
59 changed files with 12324 additions and 13030 deletions
Download patch file Download diff file Expand all files Collapse all files

3
.gitattributes vendored
View file

@ -1 +1,4 @@
# Set default behaviour, in case users don't have core.autocrlf set.
* text=auto
src/api/dotnet/Properties/AssemblyInfo.cs text eol=crlf

2
.gitignore vendored
View file

@ -55,6 +55,8 @@ src/api/api_log_macros.cpp
src/api/dll/api_dll.def
src/api/dotnet/Enumerations.cs
src/api/dotnet/Native.cs
src/api/dotnet/Properties/AssemblyInfo.cs
src/api/dotnet/Microsoft.Z3.xml
src/api/python/z3consts.py
src/api/python/z3core.py
src/ast/pattern/database.h

10
scripts/mk_util.py
View file

@ -54,6 +54,7 @@ CPP_COMPONENT='cpp'
IS_WINDOWS=False
IS_LINUX=False
IS_OSX=False
IS_FREEBSD=False
VERBOSE=True
DEBUG_MODE=False
SHOW_CPPS = True
@ -98,6 +99,9 @@ def is_windows():
def is_linux():
return IS_LINUX
def is_freebsd():
return IS_FREEBSD
def is_osx():
return IS_OSX
@ -426,6 +430,8 @@ elif os.name == 'posix':
IS_OSX=True
elif os.uname()[0] == 'Linux':
IS_LINUX=True
elif os.uname()[0] == 'FreeBSD':
IS_FREEBSD=True
def display_help(exit_code):
print("mk_make.py: Z3 Makefile generator\n")
@ -639,7 +645,7 @@ def is_CXX_gpp():
return is_compiler(CXX, 'g++')
def is_clang_in_gpp_form(cc):
version_string = subprocess.check_output([cc, '--version'])
version_string = check_output([cc, '--version'])
return str(version_string).find('clang') != -1
def is_CXX_clangpp():
@ -1181,6 +1187,8 @@ class JavaDLLComponent(Component):
t = t.replace('PLATFORM', 'darwin')
elif IS_LINUX:
t = t.replace('PLATFORM', 'linux')
elif IS_FREEBSD:
t = t.replace('PLATFORM', 'freebsd')
else:
t = t.replace('PLATFORM', 'win32')
out.write(t)

2
scripts/mk_win_dist.py
View file

@ -144,7 +144,7 @@ def mk_z3_core(x64):
cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" amd64')
cmds.append('cd %s' % BUILD_X64_DIR)
else:
cmds.append('"call %VCINSTALLDIR%vcvarsall.bat" x86')
cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" x86')
cmds.append('cd %s' % BUILD_X86_DIR)
cmds.append('nmake')
if exec_cmds(cmds) != 0:

2
src/api/api_bv.cpp
View file

@ -117,6 +117,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_sort int_s = Z3_mk_int_sort(c);
if (is_signed) {
Z3_ast r = Z3_mk_bv2int(c, n, false);
Z3_inc_ref(c, r);
Z3_sort s = Z3_get_sort(c, n);
unsigned sz = Z3_get_bv_sort_size(c, s);
rational max_bound = power(rational(2), sz);
@ -135,6 +136,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_dec_ref(c, pred);
Z3_dec_ref(c, sub);
Z3_dec_ref(c, zero);
Z3_dec_ref(c, r);
RETURN_Z3(res);
}
else {

4
src/api/api_interp.cpp
View file

@ -39,11 +39,8 @@ Revision History:
#include"iz3pp.h"
#include"iz3checker.h"
#ifndef WIN32
using namespace stl_ext;
#endif
#ifndef WIN32
// WARNING: don't make a hash_map with this if the range type
// has a destructor: you'll get an address dependency!!!
namespace stl_ext {
@ -55,7 +52,6 @@ namespace stl_ext {
}
};
}
#endif
typedef interpolation_options_struct *Z3_interpolation_options;

12
src/api/c++/z3++.h
View file

@ -652,6 +652,8 @@ namespace z3 {
return expr(c.ctx(), r);
}
friend expr distinct(expr_vector const& args);
friend expr operator==(expr const & a, expr const & b) {
check_context(a, b);
Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
@ -1066,6 +1068,16 @@ namespace z3 {
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
}
inline expr distinct(expr_vector const& args) {
assert(args.size() > 0);
context& ctx = args[0].ctx();
array<Z3_ast> _args(args);
Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
ctx.check_error();
return expr(ctx, r);
}
class func_entry : public object {
Z3_func_entry m_entry;
void init(Z3_func_entry e) {

12
src/api/dotnet/Context.cs
View file

@ -303,10 +303,10 @@ namespace Microsoft.Z3
/// <summary>
/// Create a new finite domain sort.
/// <param name="name">The name used to identify the sort</param>
/// <param size="size">The size of the sort</param>
/// <returns>The result is a sort</returns>
/// </summary>
/// <param name="name">The name used to identify the sort</param>
/// <param name="size">The size of the sort</param>
public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
{
Contract.Requires(name != null);
@ -318,12 +318,12 @@ namespace Microsoft.Z3
/// <summary>
/// Create a new finite domain sort.
/// <param name="name">The name used to identify the sort</param>
/// <param size="size">The size of the sort</param>
/// <returns>The result is a sort</returns>
/// Elements of the sort are created using <seealso cref="MkNumeral"/>,
/// Elements of the sort are created using <seealso cref="MkNumeral(ulong, Sort)"/>,
/// and the elements range from 0 to <tt>size-1</tt>.
/// </summary>
/// <param name="name">The name used to identify the sort</param>
/// <param name="size">The size of the sort</param>
public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
{
Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
@ -916,6 +916,8 @@ namespace Microsoft.Z3
CheckContextMatch(t);
return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
}
#endregion
#region Arithmetic

291
src/api/dotnet/Expr.cs
View file

@ -99,7 +99,7 @@ namespace Microsoft.Z3
Contract.Requires(Contract.ForAll(args, a => a != null));
Context.CheckContextMatch(args);
if (args.Length != NumArgs)
if (IsApp && args.Length != NumArgs)
throw new Z3Exception("Number of arguments does not match");
NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args));
}
@ -269,57 +269,58 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is the constant true.
/// </summary>
public bool IsTrue { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } }
public bool IsTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } }
/// <summary>
/// Indicates whether the term is the constant false.
/// </summary>
public bool IsFalse { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } }
public bool IsFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } }
/// <summary>
/// Indicates whether the term is an equality predicate.
/// </summary>
public bool IsEq { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } }
public bool IsEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } }
/// <summary>
/// Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).
/// </summary>
public bool IsDistinct { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } }
public bool IsDistinct { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } }
/// <summary>
/// Indicates whether the term is a ternary if-then-else term
/// </summary>
public bool IsITE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } }
public bool IsITE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } }
/// <summary>
/// Indicates whether the term is an n-ary conjunction
/// </summary>
public bool IsAnd { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } }
public bool IsAnd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } }
/// <summary>
/// Indicates whether the term is an n-ary disjunction
/// </summary>
public bool IsOr { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } }
public bool IsOr { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } }
/// <summary>
/// Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)
/// </summary>
public bool IsIff { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } }
public bool IsIff { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } }
/// <summary>
/// Indicates whether the term is an exclusive or
/// </summary>
public bool IsXor { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } }
public bool IsXor { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } }
/// <summary>
/// Indicates whether the term is a negation
/// </summary>
public bool IsNot { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } }
public bool IsNot { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } }
/// <summary>
/// Indicates whether the term is an implication
/// </summary>
public bool IsImplies { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
public bool IsImplies { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
#endregion
#region Arithmetic Terms
@ -346,82 +347,82 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is an arithmetic numeral.
/// </summary>
public bool IsArithmeticNumeral { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } }
public bool IsArithmeticNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } }
/// <summary>
/// Indicates whether the term is a less-than-or-equal
/// </summary>
public bool IsLE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } }
public bool IsLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } }
/// <summary>
/// Indicates whether the term is a greater-than-or-equal
/// </summary>
public bool IsGE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } }
public bool IsGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } }
/// <summary>
/// Indicates whether the term is a less-than
/// </summary>
public bool IsLT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } }
public bool IsLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } }
/// <summary>
/// Indicates whether the term is a greater-than
/// </summary>
public bool IsGT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } }
public bool IsGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } }
/// <summary>
/// Indicates whether the term is addition (binary)
/// </summary>
public bool IsAdd { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } }
public bool IsAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } }
/// <summary>
/// Indicates whether the term is subtraction (binary)
/// </summary>
public bool IsSub { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } }
public bool IsSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } }
/// <summary>
/// Indicates whether the term is a unary minus
/// </summary>
public bool IsUMinus { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } }
public bool IsUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } }
/// <summary>
/// Indicates whether the term is multiplication (binary)
/// </summary>
public bool IsMul { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } }
public bool IsMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } }
/// <summary>
/// Indicates whether the term is division (binary)
/// </summary>
public bool IsDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } }
public bool IsDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } }
/// <summary>
/// Indicates whether the term is integer division (binary)
/// </summary>
public bool IsIDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } }
public bool IsIDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } }
/// <summary>
/// Indicates whether the term is remainder (binary)
/// </summary>
public bool IsRemainder { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } }
public bool IsRemainder { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } }
/// <summary>
/// Indicates whether the term is modulus (binary)
/// </summary>
public bool IsModulus { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } }
public bool IsModulus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } }
/// <summary>
/// Indicates whether the term is a coercion of integer to real (unary)
/// </summary>
public bool IsIntToReal { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } }
public bool IsIntToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } }
/// <summary>
/// Indicates whether the term is a coercion of real to integer (unary)
/// </summary>
public bool IsRealToInt { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } }
public bool IsRealToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } }
/// <summary>
/// Indicates whether the term is a check that tests whether a real is integral (unary)
/// </summary>
public bool IsRealIsInt { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } }
public bool IsRealIsInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } }
#endregion
#region Array Terms
@ -443,64 +444,64 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j).
/// Array store takes at least 3 arguments. </remarks>
public bool IsStore { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }
public bool IsStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }
/// <summary>
/// Indicates whether the term is an array select.
/// </summary>
public bool IsSelect { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } }
public bool IsSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } }
/// <summary>
/// Indicates whether the term is a constant array.
/// </summary>
/// <remarks>For example, select(const(v),i) = v holds for every v and i. The function is unary.</remarks>
public bool IsConstantArray { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } }
public bool IsConstantArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } }
/// <summary>
/// Indicates whether the term is a default array.
/// </summary>
/// <remarks>For example default(const(v)) = v. The function is unary.</remarks>
public bool IsDefaultArray { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } }
public bool IsDefaultArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } }
/// <summary>
/// Indicates whether the term is an array map.
/// </summary>
/// <remarks>It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.</remarks>
public bool IsArrayMap { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } }
public bool IsArrayMap { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } }
/// <summary>
/// Indicates whether the term is an as-array term.
/// </summary>
/// <remarks>An as-array term is n array value that behaves as the function graph of the
/// function passed as parameter.</remarks>
public bool IsAsArray { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }
public bool IsAsArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }
#endregion
#region Set Terms
/// <summary>
/// Indicates whether the term is set union
/// </summary>
public bool IsSetUnion { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } }
public bool IsSetUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } }
/// <summary>
/// Indicates whether the term is set intersection
/// </summary>
public bool IsSetIntersect { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } }
public bool IsSetIntersect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } }
/// <summary>
/// Indicates whether the term is set difference
/// </summary>
public bool IsSetDifference { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } }
public bool IsSetDifference { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } }
/// <summary>
/// Indicates whether the term is set complement
/// </summary>
public bool IsSetComplement { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } }
public bool IsSetComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } }
/// <summary>
/// Indicates whether the term is set subset
/// </summary>
public bool IsSetSubset { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } }
public bool IsSetSubset { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } }
#endregion
#region Bit-vector terms
@ -515,266 +516,266 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is a bit-vector numeral
/// </summary>
public bool IsBVNumeral { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } }
public bool IsBVNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } }
/// <summary>
/// Indicates whether the term is a one-bit bit-vector with value one
/// </summary>
public bool IsBVBitOne { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } }
public bool IsBVBitOne { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } }
/// <summary>
/// Indicates whether the term is a one-bit bit-vector with value zero
/// </summary>
public bool IsBVBitZero { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } }
public bool IsBVBitZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } }
/// <summary>
/// Indicates whether the term is a bit-vector unary minus
/// </summary>
public bool IsBVUMinus { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } }
public bool IsBVUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } }
/// <summary>
/// Indicates whether the term is a bit-vector addition (binary)
/// </summary>
public bool IsBVAdd { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } }
public bool IsBVAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } }
/// <summary>
/// Indicates whether the term is a bit-vector subtraction (binary)
/// </summary>
public bool IsBVSub { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } }
public bool IsBVSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } }
/// <summary>
/// Indicates whether the term is a bit-vector multiplication (binary)
/// </summary>
public bool IsBVMul { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } }
public bool IsBVMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } }
/// <summary>
/// Indicates whether the term is a bit-vector signed division (binary)
/// </summary>
public bool IsBVSDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } }
public bool IsBVSDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } }
/// <summary>
/// Indicates whether the term is a bit-vector unsigned division (binary)
/// </summary>
public bool IsBVUDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } }
public bool IsBVUDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } }
/// <summary>
/// Indicates whether the term is a bit-vector signed remainder (binary)
/// </summary>
public bool IsBVSRem { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } }
public bool IsBVSRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } }
/// <summary>
/// Indicates whether the term is a bit-vector unsigned remainder (binary)
/// </summary>
public bool IsBVURem { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } }
public bool IsBVURem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } }
/// <summary>
/// Indicates whether the term is a bit-vector signed modulus
/// </summary>
public bool IsBVSMod { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } }
public bool IsBVSMod { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } }
/// <summary>
/// Indicates whether the term is a bit-vector signed division by zero
/// </summary>
internal bool IsBVSDiv0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } }
internal bool IsBVSDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } }
/// <summary>
/// Indicates whether the term is a bit-vector unsigned division by zero
/// </summary>
internal bool IsBVUDiv0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } }
internal bool IsBVUDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } }
/// <summary>
/// Indicates whether the term is a bit-vector signed remainder by zero
/// </summary>
internal bool IsBVSRem0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } }
internal bool IsBVSRem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } }
/// <summary>
/// Indicates whether the term is a bit-vector unsigned remainder by zero
/// </summary>
internal bool IsBVURem0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } }
internal bool IsBVURem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } }
/// <summary>
/// Indicates whether the term is a bit-vector signed modulus by zero
/// </summary>
internal bool IsBVSMod0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } }
internal bool IsBVSMod0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } }
/// <summary>
/// Indicates whether the term is an unsigned bit-vector less-than-or-equal
/// </summary>
public bool IsBVULE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } }
public bool IsBVULE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } }
/// <summary>
/// Indicates whether the term is a signed bit-vector less-than-or-equal
/// </summary>
public bool IsBVSLE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } }
public bool IsBVSLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } }
/// <summary>
/// Indicates whether the term is an unsigned bit-vector greater-than-or-equal
/// </summary>
public bool IsBVUGE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } }
public bool IsBVUGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } }
/// <summary>
/// Indicates whether the term is a signed bit-vector greater-than-or-equal
/// </summary>
public bool IsBVSGE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } }
public bool IsBVSGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } }
/// <summary>
/// Indicates whether the term is an unsigned bit-vector less-than
/// </summary>
public bool IsBVULT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } }
public bool IsBVULT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } }
/// <summary>
/// Indicates whether the term is a signed bit-vector less-than
/// </summary>
public bool IsBVSLT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } }
public bool IsBVSLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } }
/// <summary>
/// Indicates whether the term is an unsigned bit-vector greater-than
/// </summary>
public bool IsBVUGT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } }
public bool IsBVUGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } }
/// <summary>
/// Indicates whether the term is a signed bit-vector greater-than
/// </summary>
public bool IsBVSGT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } }
public bool IsBVSGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } }
/// <summary>
/// Indicates whether the term is a bit-wise AND
/// </summary>
public bool IsBVAND { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } }
public bool IsBVAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } }
/// <summary>
/// Indicates whether the term is a bit-wise OR
/// </summary>
public bool IsBVOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } }
public bool IsBVOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } }
/// <summary>
/// Indicates whether the term is a bit-wise NOT
/// </summary>
public bool IsBVNOT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } }
public bool IsBVNOT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } }
/// <summary>
/// Indicates whether the term is a bit-wise XOR
/// </summary>
public bool IsBVXOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } }
public bool IsBVXOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } }
/// <summary>
/// Indicates whether the term is a bit-wise NAND
/// </summary>
public bool IsBVNAND { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } }
public bool IsBVNAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } }
/// <summary>
/// Indicates whether the term is a bit-wise NOR
/// </summary>
public bool IsBVNOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } }
public bool IsBVNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } }
/// <summary>
/// Indicates whether the term is a bit-wise XNOR
/// </summary>
public bool IsBVXNOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } }
public bool IsBVXNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } }
/// <summary>
/// Indicates whether the term is a bit-vector concatenation (binary)
/// </summary>
public bool IsBVConcat { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } }
public bool IsBVConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } }
/// <summary>
/// Indicates whether the term is a bit-vector sign extension
/// </summary>
public bool IsBVSignExtension { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } }
public bool IsBVSignExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } }
/// <summary>
/// Indicates whether the term is a bit-vector zero extension
/// </summary>
public bool IsBVZeroExtension { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } }
public bool IsBVZeroExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } }
/// <summary>
/// Indicates whether the term is a bit-vector extraction
/// </summary>
public bool IsBVExtract { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } }
public bool IsBVExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } }
/// <summary>
/// Indicates whether the term is a bit-vector repetition
/// </summary>
public bool IsBVRepeat { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } }
public bool IsBVRepeat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } }
/// <summary>
/// Indicates whether the term is a bit-vector reduce OR
/// </summary>
public bool IsBVReduceOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } }
public bool IsBVReduceOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } }
/// <summary>
/// Indicates whether the term is a bit-vector reduce AND
/// </summary>
public bool IsBVReduceAND { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } }
public bool IsBVReduceAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } }
/// <summary>
/// Indicates whether the term is a bit-vector comparison
/// </summary>
public bool IsBVComp { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } }
public bool IsBVComp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } }
/// <summary>
/// Indicates whether the term is a bit-vector shift left
/// </summary>
public bool IsBVShiftLeft { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } }
public bool IsBVShiftLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } }
/// <summary>
/// Indicates whether the term is a bit-vector logical shift right
/// </summary>
public bool IsBVShiftRightLogical { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } }
public bool IsBVShiftRightLogical { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } }
/// <summary>
/// Indicates whether the term is a bit-vector arithmetic shift left
/// </summary>
public bool IsBVShiftRightArithmetic { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } }
public bool IsBVShiftRightArithmetic { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } }
/// <summary>
/// Indicates whether the term is a bit-vector rotate left
/// </summary>
public bool IsBVRotateLeft { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } }
public bool IsBVRotateLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } }
/// <summary>
/// Indicates whether the term is a bit-vector rotate right
/// </summary>
public bool IsBVRotateRight { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } }
public bool IsBVRotateRight { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } }
/// <summary>
/// Indicates whether the term is a bit-vector rotate left (extended)
/// </summary>
/// <remarks>Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.</remarks>
public bool IsBVRotateLeftExtended { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } }
public bool IsBVRotateLeftExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } }
/// <summary>
/// Indicates whether the term is a bit-vector rotate right (extended)
/// </summary>
/// <remarks>Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.</remarks>
public bool IsBVRotateRightExtended { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } }
public bool IsBVRotateRightExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } }
/// <summary>
/// Indicates whether the term is a coercion from integer to bit-vector
/// </summary>
/// <remarks>This function is not supported by the decision procedures. Only the most
/// rudimentary simplification rules are applied to this function.</remarks>
public bool IsIntToBV { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }
public bool IsIntToBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }
/// <summary>
/// Indicates whether the term is a coercion from bit-vector to integer
/// </summary>
/// <remarks>This function is not supported by the decision procedures. Only the most
/// rudimentary simplification rules are applied to this function.</remarks>
public bool IsBVToInt { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }
public bool IsBVToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }
/// <summary>
/// Indicates whether the term is a bit-vector carry
/// </summary>
/// <remarks>Compute the carry bit in a full-adder. The meaning is given by the
/// equivalence (carry l1 l2 l3) &lt;=&gt; (or (and l1 l2) (and l1 l3) (and l2 l3)))</remarks>
public bool IsBVCarry { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }
public bool IsBVCarry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }
/// <summary>
/// Indicates whether the term is a bit-vector ternary XOR
/// </summary>
/// <remarks>The meaning is given by the equivalence (xor3 l1 l2 l3) &lt;=&gt; (xor (xor l1 l2) l3)</remarks>
public bool IsBVXOR3 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } }
public bool IsBVXOR3 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } }
#endregion
@ -783,13 +784,13 @@ namespace Microsoft.Z3
/// Indicates whether the term is a label (used by the Boogie Verification condition generator).
/// </summary>
/// <remarks>The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula.</remarks>
public bool IsLabel { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }
public bool IsLabel { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }
/// <summary>
/// Indicates whether the term is a label literal (used by the Boogie Verification condition generator).
/// </summary>
/// <remarks>A label literal has a set of string parameters. It takes no arguments.</remarks>
public bool IsLabelLit { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
#endregion
#region Proof Terms
@ -798,22 +799,22 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>This binary predicate is used in proof terms.
/// It captures equisatisfiability and equivalence modulo renamings.</remarks>
public bool IsOEQ { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } }
public bool IsOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } }
/// <summary>
/// Indicates whether the term is a Proof for the expression 'true'.
/// </summary>
public bool IsProofTrue { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } }
public bool IsProofTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } }
/// <summary>
/// Indicates whether the term is a proof for a fact asserted by the user.
/// </summary>
public bool IsProofAsserted { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } }
public bool IsProofAsserted { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } }
/// <summary>
/// Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
/// </summary>
public bool IsProofGoal { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } }
public bool IsProofGoal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } }
/// <summary>
/// Indicates whether the term is proof via modus ponens
@ -824,7 +825,7 @@ namespace Microsoft.Z3
/// T2: (implies p q)
/// [mp T1 T2]: q
/// The second antecedents may also be a proof for (iff p q).</remarks>
public bool IsProofModusPonens { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } }
public bool IsProofModusPonens { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } }
/// <summary>
/// Indicates whether the term is a proof for (R t t), where R is a reflexive relation.
@ -833,7 +834,7 @@ namespace Microsoft.Z3
/// The only reflexive relations that are used are
/// equivalence modulo namings, equality and equivalence.
/// That is, R is either '~', '=' or 'iff'.</remarks>
public bool IsProofReflexivity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }
public bool IsProofReflexivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }
/// <summary>
/// Indicates whether the term is proof by symmetricity of a relation
@ -844,7 +845,7 @@ namespace Microsoft.Z3
/// [symmetry T1]: (R s t)
/// T1 is the antecedent of this proof object.
/// </remarks>
public bool IsProofSymmetry { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } }
public bool IsProofSymmetry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } }
/// <summary>
/// Indicates whether the term is a proof by transitivity of a relation
@ -856,7 +857,7 @@ namespace Microsoft.Z3
/// T2: (R s u)
/// [trans T1 T2]: (R t u)
/// </remarks>
public bool IsProofTransitivity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } }
public bool IsProofTransitivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } }
/// <summary>
/// Indicates whether the term is a proof by condensed transitivity of a relation
@ -877,7 +878,7 @@ namespace Microsoft.Z3
/// if there is a path from s to t, if we view every
/// antecedent (R a b) as an edge between a and b.
/// </remarks>
public bool IsProofTransitivityStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } }
public bool IsProofTransitivityStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } }
/// <summary>
@ -891,7 +892,7 @@ namespace Microsoft.Z3
/// Remark: if t_i == s_i, then the antecedent Ti is suppressed.
/// That is, reflexivity proofs are supressed to save space.
/// </remarks>
public bool IsProofMonotonicity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
/// <summary>
/// Indicates whether the term is a quant-intro proof
@ -901,7 +902,7 @@ namespace Microsoft.Z3
/// T1: (~ p q)
/// [quant-intro T1]: (~ (forall (x) p) (forall (x) q))
/// </remarks>
public bool IsProofQuantIntro { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }
public bool IsProofQuantIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }
/// <summary>
/// Indicates whether the term is a distributivity proof object.
@ -919,7 +920,7 @@ namespace Microsoft.Z3
/// Remark. This rule is used by the CNF conversion pass and
/// instantiated by f = or, and g = and.
/// </remarks>
public bool IsProofDistributivity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }
public bool IsProofDistributivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }
/// <summary>
/// Indicates whether the term is a proof by elimination of AND
@ -929,7 +930,7 @@ namespace Microsoft.Z3
/// T1: (and l_1 ... l_n)
/// [and-elim T1]: l_i
/// </remarks>
public bool IsProofAndElimination { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
public bool IsProofAndElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
/// <summary>
/// Indicates whether the term is a proof by eliminiation of not-or
@ -939,7 +940,7 @@ namespace Microsoft.Z3
/// T1: (not (or l_1 ... l_n))
/// [not-or-elim T1]: (not l_i)
/// </remarks>
public bool IsProofOrElimination { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }
public bool IsProofOrElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }
/// <summary>
/// Indicates whether the term is a proof by rewriting
@ -958,7 +959,7 @@ namespace Microsoft.Z3
/// (= (+ x 1 2) (+ 3 x))
/// (iff (or x false) x)
/// </remarks>
public bool IsProofRewrite { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }
public bool IsProofRewrite { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }
/// <summary>
/// Indicates whether the term is a proof by rewriting
@ -974,7 +975,7 @@ namespace Microsoft.Z3
/// - When converting bit-vectors to Booleans (BIT2BOOL=true)
/// - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
/// </remarks>
public bool IsProofRewriteStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
/// <summary>
/// Indicates whether the term is a proof for pulling quantifiers out.
@ -982,7 +983,7 @@ namespace Microsoft.Z3
/// <remarks>
/// A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
/// </remarks>
public bool IsProofPullQuant { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
/// <summary>
/// Indicates whether the term is a proof for pulling quantifiers out.
@ -992,7 +993,7 @@ namespace Microsoft.Z3
/// This proof object is only used if the parameter PROOF_MODE is 1.
/// This proof object has no antecedents
/// </remarks>
public bool IsProofPullQuantStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
/// <summary>
/// Indicates whether the term is a proof for pushing quantifiers in.
@ -1005,7 +1006,7 @@ namespace Microsoft.Z3
/// (forall (x_1 ... x_m) p_n[x_1 ... x_m])))
/// This proof object has no antecedents
/// </remarks>
public bool IsProofPushQuant { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }
public bool IsProofPushQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }
/// <summary>
/// Indicates whether the term is a proof for elimination of unused variables.
@ -1017,7 +1018,7 @@ namespace Microsoft.Z3
/// It is used to justify the elimination of unused variables.
/// This proof object has no antecedents.
/// </remarks>
public bool IsProofElimUnusedVars { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } }
public bool IsProofElimUnusedVars { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } }
/// <summary>
/// Indicates whether the term is a proof for destructive equality resolution
@ -1031,7 +1032,7 @@ namespace Microsoft.Z3
///
/// Several variables can be eliminated simultaneously.
/// </remarks>
public bool IsProofDER { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }
public bool IsProofDER { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }
/// <summary>
/// Indicates whether the term is a proof for quantifier instantiation
@ -1039,13 +1040,13 @@ namespace Microsoft.Z3
/// <remarks>
/// A proof of (or (not (forall (x) (P x))) (P a))
/// </remarks>
public bool IsProofQuantInst { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
/// <summary>
/// Indicates whether the term is a hypthesis marker.
/// </summary>
/// <remarks>Mark a hypothesis in a natural deduction style proof.</remarks>
public bool IsProofHypothesis { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
/// <summary>
/// Indicates whether the term is a proof by lemma
@ -1058,7 +1059,7 @@ namespace Microsoft.Z3
/// It converts the proof in a proof for (or (not l_1) ... (not l_n)),
/// when T1 contains the hypotheses: l_1, ..., l_n.
/// </remarks>
public bool IsProofLemma { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } }
public bool IsProofLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } }
/// <summary>
/// Indicates whether the term is a proof by unit resolution
@ -1070,7 +1071,7 @@ namespace Microsoft.Z3
/// T(n+1): (not l_n)
/// [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
/// </remarks>
public bool IsProofUnitResolution { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } }
public bool IsProofUnitResolution { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } }
/// <summary>
/// Indicates whether the term is a proof by iff-true
@ -1079,7 +1080,7 @@ namespace Microsoft.Z3
/// T1: p
/// [iff-true T1]: (iff p true)
/// </remarks>
public bool IsProofIFFTrue { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } }
public bool IsProofIFFTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } }
/// <summary>
/// Indicates whether the term is a proof by iff-false
@ -1088,7 +1089,7 @@ namespace Microsoft.Z3
/// T1: (not p)
/// [iff-false T1]: (iff p false)
/// </remarks>
public bool IsProofIFFFalse { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } }
public bool IsProofIFFFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } }
/// <summary>
/// Indicates whether the term is a proof by commutativity
@ -1101,7 +1102,7 @@ namespace Microsoft.Z3
/// This proof object has no antecedents.
/// Remark: if f is bool, then = is iff.
/// </remarks>
public bool IsProofCommutativity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } }
public bool IsProofCommutativity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } }
/// <summary>
/// Indicates whether the term is a proof for Tseitin-like axioms
@ -1137,7 +1138,7 @@ namespace Microsoft.Z3
/// unfolding the Boolean connectives in the axioms a small
/// bounded number of steps (=3).
/// </remarks>
public bool IsProofDefAxiom { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } }
public bool IsProofDefAxiom { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } }
/// <summary>
/// Indicates whether the term is a proof for introduction of a name
@ -1160,7 +1161,7 @@ namespace Microsoft.Z3
/// Otherwise:
/// [def-intro]: (= n e)
/// </remarks>
public bool IsProofDefIntro { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }
public bool IsProofDefIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }
/// <summary>
/// Indicates whether the term is a proof for application of a definition
@ -1170,7 +1171,7 @@ namespace Microsoft.Z3
/// F is 'equivalent' to n, given that T1 is a proof that
/// n is a name for F.
/// </remarks>
public bool IsProofApplyDef { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } }
public bool IsProofApplyDef { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } }
/// <summary>
/// Indicates whether the term is a proof iff-oeq
@ -1179,7 +1180,7 @@ namespace Microsoft.Z3
/// T1: (iff p q)
/// [iff~ T1]: (~ p q)
/// </remarks>
public bool IsProofIFFOEQ { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } }
public bool IsProofIFFOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } }
/// <summary>
/// Indicates whether the term is a proof for a positive NNF step
@ -1207,7 +1208,7 @@ namespace Microsoft.Z3
/// NNF_NEG furthermore handles the case where negation is pushed
/// over Boolean connectives 'and' and 'or'.
/// </remarks>
public bool IsProofNNFPos { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } }
public bool IsProofNNFPos { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } }
/// <summary>
/// Indicates whether the term is a proof for a negative NNF step
@ -1232,7 +1233,7 @@ namespace Microsoft.Z3
/// [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
/// (and (or r_1 r_2) (or r_1' r_2')))
/// </remarks>
public bool IsProofNNFNeg { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
/// <summary>
/// Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
@ -1244,7 +1245,7 @@ namespace Microsoft.Z3
///
/// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
/// </remarks>
public bool IsProofNNFStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
/// <summary>
/// Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
@ -1254,7 +1255,7 @@ namespace Microsoft.Z3
/// This proof object is only used if the parameter PROOF_MODE is 1.
/// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
/// </remarks>
public bool IsProofCNFStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
/// <summary>
/// Indicates whether the term is a proof for a Skolemization step
@ -1267,7 +1268,7 @@ namespace Microsoft.Z3
///
/// This proof object has no antecedents.
/// </remarks>
public bool IsProofSkolemize { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }
public bool IsProofSkolemize { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }
/// <summary>
/// Indicates whether the term is a proof by modus ponens for equi-satisfiability.
@ -1278,7 +1279,7 @@ namespace Microsoft.Z3
/// T2: (~ p q)
/// [mp~ T1 T2]: q
/// </remarks>
public bool IsProofModusPonensOEQ { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }
public bool IsProofModusPonensOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }
/// <summary>
/// Indicates whether the term is a proof for theory lemma
@ -1297,7 +1298,7 @@ namespace Microsoft.Z3
/// (iff (= t1 t2) (and (&lt;= t1 t2) (&lt;= t2 t1)))
/// - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
/// </remarks>
public bool IsProofTheoryLemma { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } }
public bool IsProofTheoryLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } }
#endregion
#region Relational Terms
@ -1322,40 +1323,40 @@ namespace Microsoft.Z3
/// The function takes <c>n+1</c> arguments, where the first argument is the relation and the remaining <c>n</c> elements
/// correspond to the <c>n</c> columns of the relation.
/// </remarks>
public bool IsRelationStore { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }
public bool IsRelationStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }
/// <summary>
/// Indicates whether the term is an empty relation
/// </summary>
public bool IsEmptyRelation { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } }
public bool IsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } }
/// <summary>
/// Indicates whether the term is a test for the emptiness of a relation
/// </summary>
public bool IsIsEmptyRelation { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } }
public bool IsIsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } }
/// <summary>
/// Indicates whether the term is a relational join
/// </summary>
public bool IsRelationalJoin { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }
public bool IsRelationalJoin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }
/// <summary>
/// Indicates whether the term is the union or convex hull of two relations.
/// </summary>
/// <remarks>The function takes two arguments.</remarks>
public bool IsRelationUnion { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }
public bool IsRelationUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }
/// <summary>
/// Indicates whether the term is the widening of two relations
/// </summary>
/// <remarks>The function takes two arguments.</remarks>
public bool IsRelationWiden { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } }
public bool IsRelationWiden { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } }
/// <summary>
/// Indicates whether the term is a projection of columns (provided as numbers in the parameters).
/// </summary>
/// <remarks>The function takes one argument.</remarks>
public bool IsRelationProject { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } }
public bool IsRelationProject { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } }
/// <summary>
/// Indicates whether the term is a relation filter
@ -1367,7 +1368,7 @@ namespace Microsoft.Z3
/// corresponding to the columns of the relation.
/// So the first column in the relation has index 0.
/// </remarks>
public bool IsRelationFilter { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } }
public bool IsRelationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } }
/// <summary>
/// Indicates whether the term is an intersection of a relation with the negation of another.
@ -1383,7 +1384,7 @@ namespace Microsoft.Z3
/// target are elements in x in pos, such that there is no y in neg that agrees with
/// x on the columns c1, d1, .., cN, dN.
/// </remarks>
public bool IsRelationNegationFilter { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } }
public bool IsRelationNegationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } }
/// <summary>
/// Indicates whether the term is the renaming of a column in a relation
@ -1392,12 +1393,12 @@ namespace Microsoft.Z3
/// The function takes one argument.
/// The parameters contain the renaming as a cycle.
/// </remarks>
public bool IsRelationRename { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } }
public bool IsRelationRename { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } }
/// <summary>
/// Indicates whether the term is the complement of a relation
/// </summary>
public bool IsRelationComplement { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } }
public bool IsRelationComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } }
/// <summary>
/// Indicates whether the term is a relational select
@ -1407,7 +1408,7 @@ namespace Microsoft.Z3
/// The function takes <c>n+1</c> arguments, where the first argument is a relation,
/// and the remaining <c>n</c> arguments correspond to a record.
/// </remarks>
public bool IsRelationSelect { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } }
public bool IsRelationSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } }
/// <summary>
/// Indicates whether the term is a relational clone (copy)
@ -1419,7 +1420,7 @@ namespace Microsoft.Z3
/// for terms of kind <seealso cref="IsRelationUnion"/>
/// to perform destructive updates to the first argument.
/// </remarks>
public bool IsRelationClone { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }
public bool IsRelationClone { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }
#endregion
#region Finite domain terms
@ -1438,7 +1439,7 @@ namespace Microsoft.Z3
/// <summary>
/// Indicates whether the term is a less than predicate over a finite domain.
/// </summary>
public bool IsFiniteDomainLT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }
public bool IsFiniteDomainLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }
#endregion
#endregion

2
src/api/dotnet/Global.cs
View file

@ -43,7 +43,7 @@ namespace Microsoft.Z3
/// The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'.
/// Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION".
/// This function can be used to set parameters for a specific Z3 module.
/// This can be done by using <module-name>.<parameter-name>.
/// This can be done by using [module-name].[parameter-name].
/// For example:
/// Z3_global_param_set('pp.decimal', 'true')
/// will set the parameter "decimal" in the module "pp" to true.

17
src/api/dotnet/Microsoft.Z3.csproj
View file

@ -24,8 +24,7 @@
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>
</DocumentationFile>
<DocumentationFile>..\Debug\Microsoft.Z3.XML</DocumentationFile>
<CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
@ -140,6 +139,7 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
<DocumentationFile>..\x64\Debug\Microsoft.Z3.XML</DocumentationFile>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x64'">
<OutputPath>..\x64\external_64\</OutputPath>
@ -193,7 +193,7 @@
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external|x64'">
<OutputPath>..\x64\external\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>..\x64\external\Microsoft.Z3.XML</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x64</PlatformTarget>
@ -220,7 +220,7 @@
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|AnyCPU'">
<OutputPath>..\Release_delaysign\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\Release_delaysign\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>..\Release_delaysign\Microsoft.Z3.XML</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
@ -238,7 +238,7 @@
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|x64'">
<OutputPath>bin\x64\Release_delaysign\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>bin\x64\Release_delaysign\Microsoft.Z3.XML</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x64</PlatformTarget>
@ -266,11 +266,12 @@
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<DocumentationFile>bin\x86\Debug\Microsoft.Z3.XML</DocumentationFile>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">
<OutputPath>bin\x86\Release\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>bin\x86\Release\Microsoft.Z3.xml</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x86</PlatformTarget>
@ -285,7 +286,7 @@
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external|x86'">
<OutputPath>bin\x86\external\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>bin\x86\external\Microsoft.Z3.XML</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x86</PlatformTarget>
@ -303,7 +304,7 @@
<OutputPath>bin\x86\Release_delaysign\</OutputPath>
<DefineConstants>DELAYSIGN</DefineConstants>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\Release_delaysign\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>bin\x86\Release_delaysign\Microsoft.Z3.XML</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x86</PlatformTarget>

6
src/api/dotnet/Solver.cs
View file

@ -132,7 +132,8 @@ namespace Microsoft.Z3
/// <remarks>
/// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
/// Both APIs can be used in the same solver. The unsat core will contain a combination
/// of the Boolean variables provided using <see cref="AssertAndTrack"/> and the Boolean literals
/// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check"/> with assumptions.
/// </remarks>
public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
@ -156,7 +157,8 @@ namespace Microsoft.Z3
/// <remarks>
/// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
/// Both APIs can be used in the same solver. The unsat core will contain a combination
/// of the Boolean variables provided using <see cref="AssertAndTrack"/> and the Boolean literals
/// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check"/> with assumptions.
/// </remarks>
public void AssertAndTrack(BoolExpr constraint, BoolExpr p)

290
src/api/java/Expr.java
View file

File diff suppressed because it is too large Load diff

2
src/api/python/z3printer.py
View file

@ -386,7 +386,7 @@ def seq3(args, lp='(', rp=')'):
else:
return group(indent(len(lp), compose(to_format(lp), seq(args), to_format(rp))))
class StopPPException:
class StopPPException(Exception):
def __str__(self):
return 'pp-interrupted'

28
src/ast/ast_smt2_pp.cpp
View file

@ -472,6 +472,25 @@ class smt2_printer {
ast_manager & m() const { return m_manager; }
ast_manager & fm() const { return format_ns::fm(m()); }
std::string ensure_quote(symbol const& s) {
std::string str;
if (is_smt2_quoted_symbol(s))
str = mk_smt2_quoted_symbol(s);
else
str = s.str();
return str;
}
symbol ensure_quote_sym(symbol const& s) {
if (is_smt2_quoted_symbol(s)) {
std::string str;
str = mk_smt2_quoted_symbol(s);
return symbol(str.c_str());
}
else
return s;
}
void pp_var(var * v) {
format * f;
if (v->get_idx() < m_var_names.size()) {
@ -501,11 +520,7 @@ class smt2_printer {
}
format * pp_simple_attribute(char const * attr, symbol const & s) {
std::string str;
if (is_smt2_quoted_symbol(s))
str = mk_smt2_quoted_symbol(s);
else
str = s.str();
std::string str = ensure_quote(s);
return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str.c_str()));
}
@ -773,7 +788,7 @@ class smt2_printer {
void register_var_names(quantifier * q) {
unsigned num_decls = q->get_num_decls();
for (unsigned i = 0; i < num_decls; i++) {
symbol name = q->get_decl_name(i);
symbol name = ensure_quote_sym(q->get_decl_name(i));
if (name.is_numerical()) {
unsigned idx = 1;
name = next_name("x", idx);
@ -997,6 +1012,7 @@ public:
unsigned idx = 1;
for (unsigned i = 0; i < num; i++) {
symbol name = next_name(var_prefix, idx);
name = ensure_quote_sym(name);
var_names.push_back(name);
m_var_names_set.insert(name);
m_var_names.push_back(name);

7
src/ast/rewriter/arith_rewriter.cpp
View file

@ -753,12 +753,7 @@ br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & resul
}
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) {
if (is_add(arg1) || is_mul(arg1)) {
ptr_buffer<expr> new_args;
unsigned num_args = to_app(arg1)->get_num_args();
for (unsigned i = 0; i < num_args; i++)
new_args.push_back(m_util.mk_rem(to_app(arg1)->get_arg(i), arg2));
result = m().mk_app(to_app(arg1)->get_decl(), new_args.size(), new_args.c_ptr());
return BR_REWRITE2;
return BR_FAILED;
}
else {
if (v2.is_neg()) {

2
src/cmd_context/check_logic.cpp
View file

@ -310,6 +310,8 @@ struct check_logic::imp {
return false;
non_numeral = arg;
}
if (non_numeral == 0)
return true;
if (is_diff_var(non_numeral))
return true;
if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral))

19
src/cmd_context/pdecl.cpp
View file

@ -515,6 +515,25 @@ bool pdatatype_decl::has_missing_refs(symbol & missing) const {
return false;
}
bool pdatatype_decl::has_duplicate_accessors(symbol & duplicated) const {
hashtable<symbol, symbol_hash_proc, symbol_eq_proc> names;
ptr_vector<pconstructor_decl>::const_iterator it = m_constructors.begin();
ptr_vector<pconstructor_decl>::const_iterator end = m_constructors.end();
for (; it != end; ++it) {
ptr_vector<paccessor_decl> const& acc = (*it)->m_accessors;
for (unsigned i = 0; i < acc.size(); ++i) {
symbol const& name = acc[i]->get_name();
if (names.contains(name)) {
duplicated = name;
return true;
}
names.insert(name);
}
}
return false;
}
bool pdatatype_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
ptr_vector<pconstructor_decl>::iterator it = m_constructors.begin();
ptr_vector<pconstructor_decl>::iterator end = m_constructors.end();

2
src/cmd_context/pdecl.h
View file

@ -169,6 +169,7 @@ public:
class paccessor_decl : public pdecl {
friend class pdecl_manager;
friend class pconstructor_decl;
friend class pdatatype_decl;
symbol m_name;
ptype m_type;
paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r);
@ -222,6 +223,7 @@ public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s);
virtual void display(std::ostream & out) const;
bool has_missing_refs(symbol & missing) const;
bool has_duplicate_accessors(symbol & repeated) const;
};
/**

70
src/duality/duality.h
View file

@ -25,12 +25,12 @@ Revision History:
#include <map>
// make hash_map and hash_set available
#ifndef _WINDOWS
using namespace stl_ext;
#endif
namespace Duality {
class implicant_solver;
/* Generic operations on Z3 formulas */
struct Z3User {
@ -82,6 +82,8 @@ namespace Duality {
Term SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val);
Term CloneQuantAndSimp(const expr &t, const expr &body);
Term RemoveRedundancy(const Term &t);
Term IneqToEq(const Term &t);
@ -102,6 +104,9 @@ namespace Duality {
FuncDecl RenumberPred(const FuncDecl &f, int n);
Term ExtractStores(hash_map<ast, Term> &memo, const Term &t, std::vector<expr> &cnstrs, hash_map<ast,expr> &renaming);
protected:
void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
@ -113,7 +118,11 @@ protected:
expr FinishAndOr(const std::vector<expr> &args, bool is_and);
expr PullCommonFactors(std::vector<expr> &args, bool is_and);
Term IneqToEqRec(hash_map<ast, Term> &memo, const Term &t);
Term CloneQuantAndSimp(const expr &t, const expr &body, bool is_forall);
Term PushQuantifier(const expr &t, const expr &body, bool is_forall);
void CollectJuncts(const Term &f, std::vector<Term> &lits, decl_kind op, bool negate);
Term DeleteBoundRec(hash_map<int,hash_map<ast,Term> > &memo, int level, int num, const Term &t);
Term DeleteBound(int level, int num, const Term &t);
};
@ -197,6 +206,9 @@ protected:
/** Is this a background constant? */
virtual bool is_constant(const func_decl &f) = 0;
/** Get the constants in the background vocabulary */
virtual hash_set<func_decl> &get_constants() = 0;
/** Assert a background axiom. */
virtual void assert_axiom(const expr &axiom) = 0;
@ -290,6 +302,11 @@ protected:
return bckg.find(f) != bckg.end();
}
/** Get the constants in the background vocabulary */
virtual hash_set<func_decl> &get_constants(){
return bckg;
}
~iZ3LogicSolver(){
// delete ictx;
delete islvr;
@ -601,6 +618,8 @@ protected:
void FixCurrentStateFull(Edge *edge, const expr &extra);
void FixCurrentStateFull(Edge *edge, const std::vector<expr> &assumps, const hash_map<ast,expr> &renaming);
/** Declare a constant in the background theory. */
void DeclareConstant(const FuncDecl &f);
@ -731,6 +750,10 @@ protected:
struct bad_format {
};
// thrown on internal error
struct Bad {
};
/** Pop a scope (see Push). Note, you cannot pop axioms. */
void Pop(int num_scopes);
@ -942,10 +965,12 @@ protected:
Term UnderapproxFormula(const Term &f, hash_set<ast> &dont_cares);
void ImplicantFullRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
hash_set<ast> &done, hash_set<ast> &dont_cares);
hash_set<ast> &done, hash_set<ast> &dont_cares, bool extensional = true);
Term UnderapproxFullFormula(const Term &f, hash_set<ast> &dont_cares);
public:
Term UnderapproxFullFormula(const Term &f, bool extensional = true);
protected:
Term ToRuleRec(Edge *e, hash_map<ast,Term> &memo, const Term &t, std::vector<expr> &quants);
hash_map<ast,Term> resolve_ite_memo;
@ -986,6 +1011,8 @@ protected:
void AddEdgeToSolver(Edge *edge);
void AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge);
void AddToProofCore(hash_set<ast> &core);
void GetGroundLitsUnderQuants(hash_set<ast> *memo, const Term &f, std::vector<Term> &res, int under);
@ -1051,13 +1078,40 @@ protected:
public:
struct Counterexample {
class Counterexample {
private:
RPFP *tree;
RPFP::Node *root;
public:
Counterexample(){
tree = 0;
root = 0;
}
Counterexample(RPFP *_tree, RPFP::Node *_root){
tree = _tree;
root = _root;
}
~Counterexample(){
if(tree) delete tree;
}
void swap(Counterexample &other){
std::swap(tree,other.tree);
std::swap(root,other.root);
}
void set(RPFP *_tree, RPFP::Node *_root){
if(tree) delete tree;
tree = _tree;
root = _root;
}
void clear(){
if(tree) delete tree;
tree = 0;
}
RPFP *get_tree() const {return tree;}
RPFP::Node *get_root() const {return root;}
private:
Counterexample &operator=(const Counterexample &);
Counterexample(const Counterexample &);
};
/** Solve the problem. You can optionally give an old
@ -1067,7 +1121,7 @@ protected:
virtual bool Solve() = 0;
virtual Counterexample GetCounterexample() = 0;
virtual Counterexample &GetCounterexample() = 0;
virtual bool SetOption(const std::string &option, const std::string &value) = 0;
@ -1075,7 +1129,7 @@ protected:
is chiefly useful for abstraction refinement, when we want to
solve a series of similar problems. */
virtual void LearnFrom(Counterexample &old_cex) = 0;
virtual void LearnFrom(Solver *old_solver) = 0;
virtual ~Solver(){}

169
src/duality/duality_hash.h
View file

@ -1,169 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3hash.h
Abstract:
Wrapper for stl hash tables
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
// pull in the headers for has_map and hash_set
// these live in non-standard places
#ifndef IZ3_HASH_H
#define IZ3_HASH_H
//#define USE_UNORDERED_MAP
#ifdef USE_UNORDERED_MAP
#define stl_ext std
#define hash_space std
#include <unordered_map>
#include <unordered_set>
#define hash_map unordered_map
#define hash_set unordered_set
#else
#if __GNUC__ >= 3
#undef __DEPRECATED
#define stl_ext __gnu_cxx
#define hash_space stl_ext
#include <ext/hash_map>
#include <ext/hash_set>
#else
#ifdef WIN32
#define stl_ext stdext
#define hash_space std
#include <hash_map>
#include <hash_set>
#else
#define stl_ext std
#define hash_space std
#include <hash_map>
#include <hash_set>
#endif
#endif
#endif
#include <string>
// stupid STL doesn't include hash function for class string
#ifndef WIN32
namespace stl_ext {
template <>
class hash<std::string> {
stl_ext::hash<char *> H;
public:
size_t operator()(const std::string &s) const {
return H(s.c_str());
}
};
}
#endif
namespace hash_space {
template <>
class hash<std::pair<int,int> > {
public:
size_t operator()(const std::pair<int,int> &p) const {
return p.first + p.second;
}
};
}
#ifdef WIN32
template <> inline
size_t stdext::hash_value<std::pair<int,int> >(const std::pair<int,int>& p)
{ // hash _Keyval to size_t value one-to-one
return p.first + p.second;
}
#endif
namespace hash_space {
template <class T>
class hash<std::pair<T *, T *> > {
public:
size_t operator()(const std::pair<T *,T *> &p) const {
return (size_t)p.first + (size_t)p.second;
}
};
}
#if 0
template <class T> inline
size_t stdext::hash_value<std::pair<T *, T *> >(const std::pair<T *, T *>& p)
{ // hash _Keyval to size_t value one-to-one
return (size_t)p.first + (size_t)p.second;
}
#endif
#ifdef WIN32
namespace std {
template <>
class less<std::pair<int,int> > {
public:
bool operator()(const pair<int,int> &x, const pair<int,int> &y) const {
return x.first < y.first || x.first == y.first && x.second < y.second;
}
};
}
namespace std {
template <class T>
class less<std::pair<T *,T *> > {
public:
bool operator()(const pair<T *,T *> &x, const pair<T *,T *> &y) const {
return (size_t)x.first < (size_t)y.first || (size_t)x.first == (size_t)y.first && (size_t)x.second < (size_t)y.second;
}
};
}
#endif
#ifndef WIN32
namespace stl_ext {
template <class T>
class hash<T *> {
public:
size_t operator()(const T *p) const {
return (size_t) p;
}
};
}
#endif
#ifdef WIN32
template <class K, class T>
class hash_map : public stl_ext::hash_map<K,T,stl_ext::hash_compare<K,std::less<K> > > {};
template <class K>
class hash_set : public stl_ext::hash_set<K,stl_ext::hash_compare<K,std::less<K> > > {};
#endif
#endif

2
src/duality/duality_profiling.cpp
View file

@ -25,7 +25,7 @@ Revision History:
#include <string.h>
#include <stdlib.h>
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)

371
src/duality/duality_rpfp.cpp
View file

@ -21,7 +21,7 @@ Revision History:
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -36,10 +36,6 @@ Revision History:
#include "duality.h"
#include "duality_profiling.h"
#ifndef WIN32
// #define Z3OPS
#endif
// TODO: do we need these?
#ifdef Z3OPS
@ -150,8 +146,10 @@ namespace Duality {
}
return 0;
}
if(t.is_quantifier())
return CountOperatorsRec(memo,t.body())+2; // count 2 for a quantifier
if(t.is_quantifier()){
int nbv = t.get_quantifier_num_bound();
return CountOperatorsRec(memo,t.body()) + 2 * nbv; // count 2 for each quantifier
}
return 0;
}
@ -410,6 +408,33 @@ namespace Duality {
return res;
}
Z3User::Term Z3User::ExtractStores(hash_map<ast, Term> &memo, const Term &t, std::vector<expr> &cnstrs, hash_map<ast,expr> &renaming)
{
std::pair<ast,Term> foo(t,expr(ctx));
std::pair<hash_map<ast,Term>::iterator, bool> bar = memo.insert(foo);
Term &res = bar.first->second;
if(!bar.second) return res;
if (t.is_app()) {
func_decl f = t.decl();
std::vector<Term> args;
int nargs = t.num_args();
for(int i = 0; i < nargs; i++)
args.push_back(ExtractStores(memo, t.arg(i),cnstrs,renaming));
res = f(args.size(),&args[0]);
if(f.get_decl_kind() == Store){
func_decl fresh = ctx.fresh_func_decl("@arr", res.get_sort());
expr y = fresh();
expr equ = ctx.make(Equal,y,res);
cnstrs.push_back(equ);
renaming[y] = res;
res = y;
}
}
else res = t;
return res;
}
bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){
if(!(lit.is_quantifier() && IsClosedFormula(lit))){
if(!lit.is_app())
@ -523,6 +548,53 @@ namespace Duality {
return foo;
}
Z3User::Term Z3User::PushQuantifier(const expr &t, const expr &body, bool is_forall){
if(t.get_quantifier_num_bound() == 1){
std::vector<expr> fmlas,free,not_free;
CollectJuncts(body,fmlas, is_forall ? Or : And, false);
for(unsigned i = 0; i < fmlas.size(); i++){
const expr &fmla = fmlas[i];
if(fmla.has_free(0))
free.push_back(fmla);
else
not_free.push_back(fmla);
}
decl_kind op = is_forall ? Or : And;
if(free.empty())
return DeleteBound(0,1,SimplifyAndOr(not_free,op == And));
expr q = clone_quantifier(is_forall ? Forall : Exists,t, SimplifyAndOr(free, op == And));
if(!not_free.empty())
q = ctx.make(op,q,DeleteBound(0,1,SimplifyAndOr(not_free, op == And)));
return q;
}
return clone_quantifier(is_forall ? Forall : Exists,t,body);
}
Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body, bool is_forall){
if(body.is_app()){
if(body.decl().get_decl_kind() == (is_forall ? And : Or)){ // quantifier distributes
int nargs = body.num_args();
std::vector<expr> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = CloneQuantAndSimp(t, body.arg(i), is_forall);
return SimplifyAndOr(args, body.decl().get_decl_kind() == And);
}
else if(body.decl().get_decl_kind() == (is_forall ? Or : And)){ // quantifier distributes
return PushQuantifier(t,body,is_forall); // may distribute partially
}
else if(body.decl().get_decl_kind() == Not){
return ctx.make(Not,CloneQuantAndSimp(t,body.arg(0),!is_forall));
}
}
if(t.get_quantifier_num_bound() == 1 && !body.has_free(0))
return DeleteBound(0,1,body); // drop the quantifier
return clone_quantifier(is_forall ? Forall : Exists,t,body);
}
Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body){
return CloneQuantAndSimp(t,body,t.is_quantifier_forall());
}
Z3User::Term Z3User::SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val){
std::pair<ast,Term> foo(t,expr(ctx));
std::pair<hash_map<ast,Term>::iterator, bool> bar = memo.insert(foo);
@ -615,7 +687,7 @@ namespace Duality {
else if (t.is_quantifier())
{
Term body = RemoveRedundancyRec(memo,smemo,t.body());
res = clone_quantifier(t, body);
res = CloneQuantAndSimp(t, body);
}
else res = t;
return res;
@ -1832,7 +1904,7 @@ namespace Duality {
}
void RPFP::ImplicantFullRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
hash_set<ast> &done, hash_set<ast> &dont_cares){
hash_set<ast> &done, hash_set<ast> &dont_cares, bool extensional){
if(done.find(f) != done.end())
return; /* already processed */
if(f.is_app()){
@ -1840,7 +1912,7 @@ namespace Duality {
decl_kind k = f.decl().get_decl_kind();
if(k == Implies || k == Iff || k == And || k == Or || k == Not){
for(int i = 0; i < nargs; i++)
ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares);
ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares, extensional);
goto done;
}
}
@ -1848,6 +1920,15 @@ namespace Duality {
if(dont_cares.find(f) == dont_cares.end()){
int b = SubtermTruth(memo,f);
if(b != 0 && b != 1) goto done;
if(f.is_app() && f.decl().get_decl_kind() == Equal && f.arg(0).is_array()){
if(b == 1 && !extensional){
expr x = dualModel.eval(f.arg(0)); expr y = dualModel.eval(f.arg(1));
if(!eq(x,y))
b = 0;
}
if(b == 0)
goto done;
}
expr bv = (b==1) ? f : !f;
lits.push_back(bv);
}
@ -1969,12 +2050,16 @@ namespace Duality {
return conjoin(lits);
}
RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set<ast> &dont_cares){
RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, bool extensional){
hash_set<ast> dont_cares;
resolve_ite_memo.clear();
timer_start("UnderapproxFormula");
/* first compute truth values of subterms */
hash_map<ast,int> memo;
hash_set<ast> done;
std::vector<Term> lits;
ImplicantFullRed(memo,f,lits,done,dont_cares);
ImplicantFullRed(memo,f,lits,done,dont_cares, extensional);
timer_stop("UnderapproxFormula");
/* return conjunction of literals */
return conjoin(lits);
}
@ -2411,6 +2496,20 @@ namespace Duality {
}
}
void Z3User::CollectJuncts(const Term &f, std::vector<Term> &lits, decl_kind op, bool negate){
if(f.is_app() && f.decl().get_decl_kind() == Not)
CollectJuncts(f.arg(0), lits, (op == And) ? Or : And, !negate);
else if(f.is_app() && f.decl().get_decl_kind() == op){
int num_args = f.num_args();
for(int i = 0; i < num_args; i++)
CollectJuncts(f.arg(i),lits,op,negate);
}
else {
expr junct = negate ? Negate(f) : f;
lits.push_back(junct);
}
}
struct TermLt {
bool operator()(const expr &x, const expr &y){
unsigned xid = x.get_id();
@ -2519,22 +2618,6 @@ namespace Duality {
ConstrainEdgeLocalized(edge,eu);
}
void RPFP::FixCurrentStateFull(Edge *edge, const expr &extra){
hash_set<ast> dont_cares;
resolve_ite_memo.clear();
timer_start("UnderapproxFormula");
Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual;
for(unsigned i = 0; i < edge->constraints.size(); i++)
dual = dual && edge->constraints[i];
// dual = dual && extra;
Term eu = UnderapproxFullFormula(dual,dont_cares);
timer_stop("UnderapproxFormula");
ConstrainEdgeLocalized(edge,eu);
}
void RPFP::GetGroundLitsUnderQuants(hash_set<ast> *memo, const Term &f, std::vector<Term> &res, int under){
if(memo[under].find(f) != memo[under].end())
return;
@ -2817,7 +2900,91 @@ namespace Duality {
return ctx.make(And,lits);
}
/* This is a wrapper for a solver that is intended to compute
implicants from models. It works around a problem in Z3 with
models in the non-extensional array theory. It does this by
naming all of the store terms in a formula. That is, (store ...)
is replaced by "name" with an added constraint name = (store
...). This allows us to determine from the model whether an array
equality is true or false (it is false if the two sides are
mapped to different function symbols, even if they have the same
contents).
*/
struct implicant_solver {
RPFP *owner;
solver &aux_solver;
std::vector<expr> assumps, namings;
std::vector<int> assump_stack, naming_stack;
hash_map<ast,expr> renaming, renaming_memo;
void add(const expr &e){
expr t = e;
if(!aux_solver.extensional_array_theory()){
unsigned i = namings.size();
t = owner->ExtractStores(renaming_memo,t,namings,renaming);
for(; i < namings.size(); i++)
aux_solver.add(namings[i]);
}
assumps.push_back(t);
aux_solver.add(t);
}
void push() {
assump_stack.push_back(assumps.size());
naming_stack.push_back(namings.size());
aux_solver.push();
}
// When we pop the solver, we have to re-add any namings that were lost
void pop(int n) {
aux_solver.pop(n);
int new_assumps = assump_stack[assump_stack.size()-n];
int new_namings = naming_stack[naming_stack.size()-n];
for(unsigned i = new_namings; i < namings.size(); i++)
aux_solver.add(namings[i]);
assumps.resize(new_assumps);
namings.resize(new_namings);
assump_stack.resize(assump_stack.size()-1);
naming_stack.resize(naming_stack.size()-1);
}
check_result check() {
return aux_solver.check();
}
model get_model() {
return aux_solver.get_model();
}
expr get_implicant() {
owner->dualModel = aux_solver.get_model();
expr dual = owner->ctx.make(And,assumps);
bool ext = aux_solver.extensional_array_theory();
expr eu = owner->UnderapproxFullFormula(dual,ext);
// if we renamed store terms, we have to undo
if(!ext)
eu = owner->SubstRec(renaming,eu);
return eu;
}
implicant_solver(RPFP *_owner, solver &_aux_solver)
: owner(_owner), aux_solver(_aux_solver)
{}
};
// set up edge constraint in aux solver
void RPFP::AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge){
if(!edge->dual.null())
aux_solver.add(edge->dual);
for(unsigned i = 0; i < edge->constraints.size(); i++){
expr tl = edge->constraints[i];
aux_solver.add(tl);
}
}
void RPFP::AddEdgeToSolver(Edge *edge){
if(!edge->dual.null())
aux_solver.add(edge->dual);
@ -2827,57 +2994,132 @@ namespace Duality {
}
}
static int by_case_counter = 0;
void RPFP::InterpolateByCases(Node *root, Node *node){
timer_start("InterpolateByCases");
bool axioms_added = false;
aux_solver.push();
AddEdgeToSolver(node->Outgoing);
hash_set<ast> axioms_needed;
const std::vector<expr> &theory = ls->get_axioms();
for(unsigned i = 0; i < theory.size(); i++)
axioms_needed.insert(theory[i]);
implicant_solver is(this,aux_solver);
is.push();
AddEdgeToSolver(is,node->Outgoing);
node->Annotation.SetEmpty();
hash_set<ast> *core = new hash_set<ast>;
core->insert(node->Outgoing->dual);
while(1){
aux_solver.push();
by_case_counter++;
is.push();
expr annot = !GetAnnotation(node);
aux_solver.add(annot);
if(aux_solver.check() == unsat){
aux_solver.pop(1);
is.add(annot);
if(is.check() == unsat){
is.pop(1);
break;
}
dualModel = aux_solver.get_model();
aux_solver.pop(1);
is.pop(1);
Push();
FixCurrentStateFull(node->Outgoing,annot);
ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node));
ConstrainEdgeLocalized(node->Outgoing,is.get_implicant());
ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this?
check_result foo = Check(root);
if(foo != unsat)
if(foo != unsat){
slvr().print("should_be_unsat.smt2");
throw "should be unsat";
AddToProofCore(*core);
}
std::vector<expr> assumps, axioms_to_add;
slvr().get_proof().get_assumptions(assumps);
for(unsigned i = 0; i < assumps.size(); i++){
(*core).insert(assumps[i]);
if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
axioms_to_add.push_back(assumps[i]);
axioms_needed.erase(assumps[i]);
}
}
// AddToProofCore(*core);
Transformer old_annot = node->Annotation;
SolveSingleNode(root,node);
{
expr itp = GetAnnotation(node);
dualModel = aux_solver.get_model();
dualModel = is.get_model(); // TODO: what does this mean?
std::vector<expr> case_lits;
itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
SetAnnotation(node,itp);
node->Annotation.Formula = node->Annotation.Formula.simplify();
}
for(unsigned i = 0; i < axioms_to_add.size(); i++)
is.add(axioms_to_add[i]);
#define TEST_BAD
#ifdef TEST_BAD
{
static int bad_count = 0, num_bads = 1;
if(bad_count >= num_bads){
bad_count = 0;
num_bads = num_bads * 2;
Pop(1);
is.pop(1);
delete core;
timer_stop("InterpolateByCases");
throw Bad();
}
bad_count++;
}
#endif
if(node->Annotation.IsEmpty()){
if(!axioms_added){
// add the axioms in the off chance they are useful
const std::vector<expr> &theory = ls->get_axioms();
for(unsigned i = 0; i < theory.size(); i++)
aux_solver.add(theory[i]);
is.add(theory[i]);
axioms_added = true;
}
else {
#ifdef KILL_ON_BAD_INTERPOLANT
std::cout << "bad in InterpolateByCase -- core:\n";
#if 0
std::vector<expr> assumps;
slvr().get_proof().get_assumptions(assumps);
for(unsigned i = 0; i < assumps.size(); i++)
assumps[i].show();
#endif
std::cout << "checking for inconsistency\n";
std::cout << "model:\n";
is.get_model().show();
expr impl = is.get_implicant();
std::vector<expr> conjuncts;
CollectConjuncts(impl,conjuncts,true);
std::cout << "impl:\n";
for(unsigned i = 0; i < conjuncts.size(); i++)
conjuncts[i].show();
std::cout << "annot:\n";
annot.show();
is.add(annot);
for(unsigned i = 0; i < conjuncts.size(); i++)
is.add(conjuncts[i]);
if(is.check() == unsat){
std::cout << "inconsistent!\n";
std::vector<expr> is_assumps;
is.aux_solver.get_proof().get_assumptions(is_assumps);
std::cout << "core:\n";
for(unsigned i = 0; i < is_assumps.size(); i++)
is_assumps[i].show();
}
else {
std::cout << "consistent!\n";
is.aux_solver.print("should_be_inconsistent.smt2");
}
std::cout << "by_case_counter = " << by_case_counter << "\n";
throw "ack!";
#endif
Pop(1);
is.pop(1);
delete core;
timer_stop("InterpolateByCases");
throw Bad();
}
}
Pop(1);
@ -2886,7 +3128,8 @@ namespace Duality {
if(proof_core)
delete proof_core; // shouldn't happen
proof_core = core;
aux_solver.pop(1);
is.pop(1);
timer_stop("InterpolateByCases");
}
void RPFP::Generalize(Node *root, Node *node){
@ -3187,7 +3430,7 @@ namespace Duality {
func_decl f = t.decl();
std::vector<Term> args;
int nargs = t.num_args();
if(nargs == 0)
if(nargs == 0 && f.get_decl_kind() == Uninterpreted)
ls->declare_constant(f); // keep track of background constants
for(int i = 0; i < nargs; i++)
args.push_back(SubstBoundRec(memo, subst, level, t.arg(i)));
@ -3217,6 +3460,46 @@ namespace Duality {
return SubstBoundRec(memo, subst, 0, t);
}
// Eliminate the deBruijn indices from level to level+num-1
Z3User::Term Z3User::DeleteBoundRec(hash_map<int,hash_map<ast,Term> > &memo, int level, int num, const Term &t)
{
std::pair<ast,Term> foo(t,expr(ctx));
std::pair<hash_map<ast,Term>::iterator, bool> bar = memo[level].insert(foo);
Term &res = bar.first->second;
if(!bar.second) return res;
if (t.is_app())
{
func_decl f = t.decl();
std::vector<Term> args;
int nargs = t.num_args();
for(int i = 0; i < nargs; i++)
args.push_back(DeleteBoundRec(memo, level, num, t.arg(i)));
res = f(args.size(),&args[0]);
}
else if (t.is_quantifier()){
int bound = t.get_quantifier_num_bound();
std::vector<expr> pats;
t.get_patterns(pats);
for(unsigned i = 0; i < pats.size(); i++)
pats[i] = DeleteBoundRec(memo, level + bound, num, pats[i]);
res = clone_quantifier(t, DeleteBoundRec(memo, level + bound, num, t.body()), pats);
}
else if (t.is_var()) {
int idx = t.get_index_value();
if(idx >= level){
res = ctx.make_var(idx-num,t.get_sort());
}
else res = t;
}
else res = t;
return res;
}
Z3User::Term Z3User::DeleteBound(int level, int num, const Term &t){
hash_map<int,hash_map<ast,Term> > memo;
return DeleteBoundRec(memo, level, num, t);
}
int Z3User::MaxIndex(hash_map<ast,int> &memo, const Term &t)
{
std::pair<ast,int> foo(t,-1);

525
src/duality/duality_solver.cpp
View file

@ -19,7 +19,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -54,6 +54,7 @@ Revision History:
// #define KEEP_EXPANSIONS
// #define USE_CACHING_RPFP
// #define PROPAGATE_BEFORE_CHECK
#define NEW_STRATIFIED_INLINING
#define USE_RPFP_CLONE
#define USE_NEW_GEN_CANDS
@ -82,7 +83,7 @@ namespace Duality {
rpfp = _rpfp;
}
virtual void Extend(RPFP::Node *node){}
virtual void Update(RPFP::Node *node, const RPFP::Transformer &update){}
virtual void Update(RPFP::Node *node, const RPFP::Transformer &update, bool eager){}
virtual void Bound(RPFP::Node *node){}
virtual void Expand(RPFP::Edge *edge){}
virtual void AddCover(RPFP::Node *covered, std::vector<RPFP::Node *> &covering){}
@ -94,6 +95,7 @@ namespace Duality {
virtual void UpdateUnderapprox(RPFP::Node *node, const RPFP::Transformer &update){}
virtual void Reject(RPFP::Edge *edge, const std::vector<RPFP::Node *> &Children){}
virtual void Message(const std::string &msg){}
virtual void Depth(int){}
virtual ~Reporter(){}
};
@ -124,6 +126,7 @@ namespace Duality {
rpfp = _rpfp;
reporter = 0;
heuristic = 0;
unwinding = 0;
FullExpand = false;
NoConj = false;
FeasibleEdges = true;
@ -131,6 +134,7 @@ namespace Duality {
Report = false;
StratifiedInlining = false;
RecursionBound = -1;
BatchExpand = false;
{
scoped_no_proof no_proofs_please(ctx.m());
#ifdef USE_RPFP_CLONE
@ -151,6 +155,7 @@ namespace Duality {
#ifdef USE_NEW_GEN_CANDS
delete gen_cands_rpfp;
#endif
if(unwinding) delete unwinding;
}
#ifdef USE_RPFP_CLONE
@ -249,6 +254,19 @@ namespace Duality {
virtual void Done() {}
};
/** The Proposer class proposes conjectures eagerly. These can come
from any source, including predicate abstraction, templates, or
previous solver runs. The proposed conjectures are checked
with low effort when the unwinding is expanded.
*/
class Proposer {
public:
/** Given a node in the unwinding, propose some conjectures */
virtual std::vector<RPFP::Transformer> &Propose(Node *node) = 0;
virtual ~Proposer(){};
};
class Covering; // see below
@ -278,6 +296,7 @@ namespace Duality {
hash_map<Node *, Node *> underapprox_map; // maps underapprox nodes to the nodes they approximate
int last_decisions;
hash_set<Node *> overapproxes;
std::vector<Proposer *> proposers;
#ifdef BOUNDED
struct Counter {
@ -292,24 +311,22 @@ namespace Duality {
virtual bool Solve(){
reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp);
#ifndef LOCALIZE_CONJECTURES
heuristic = !cex.tree ? new Heuristic(rpfp) : new ReplayHeuristic(rpfp,cex);
heuristic = !cex.get_tree() ? new Heuristic(rpfp) : new ReplayHeuristic(rpfp,cex);
#else
heuristic = !cex.tree ? (Heuristic *)(new LocalHeuristic(rpfp))
heuristic = !cex.get_tree() ? (Heuristic *)(new LocalHeuristic(rpfp))
: (Heuristic *)(new ReplayHeuristic(rpfp,cex));
#endif
cex.tree = 0; // heuristic now owns it
cex.clear(); // in case we didn't use it for heuristic
if(unwinding) delete unwinding;
unwinding = new RPFP(rpfp->ls);
unwinding->HornClauses = rpfp->HornClauses;
indset = new Covering(this);
last_decisions = 0;
CreateEdgesByChildMap();
CreateLeaves();
#ifndef TOP_DOWN
if(!StratifiedInlining){
if(FeasibleEdges)NullaryCandidates();
else InstantiateAllEdges();
}
CreateInitialUnwinding();
#else
CreateLeaves();
for(unsigned i = 0; i < leaves.size(); i++)
if(!SatisfyUpperBound(leaves[i]))
return false;
@ -321,11 +338,29 @@ namespace Duality {
// print_profile(std::cout);
delete indset;
delete heuristic;
delete unwinding;
// delete unwinding; // keep the unwinding for future mining of predicates
delete reporter;
for(unsigned i = 0; i < proposers.size(); i++)
delete proposers[i];
return res;
}
void CreateInitialUnwinding(){
if(!StratifiedInlining){
CreateLeaves();
if(FeasibleEdges)NullaryCandidates();
else InstantiateAllEdges();
}
else {
#ifdef NEW_STRATIFIED_INLINING
#else
CreateLeaves();
#endif
}
}
void Cancel(){
// TODO
}
@ -346,15 +381,19 @@ namespace Duality {
}
#endif
virtual void LearnFrom(Counterexample &old_cex){
cex = old_cex;
virtual void LearnFrom(Solver *other_solver){
// get the counterexample as a guide
cex.swap(other_solver->GetCounterexample());
// propose conjectures based on old unwinding
Duality *old_duality = dynamic_cast<Duality *>(other_solver);
if(old_duality)
proposers.push_back(new HistoryProposer(old_duality,this));
}
/** Return the counterexample */
virtual Counterexample GetCounterexample(){
Counterexample res = cex;
cex.tree = 0; // Cex now belongs to caller
return res;
/** Return a reference to the counterexample */
virtual Counterexample &GetCounterexample(){
return cex;
}
// options
@ -365,6 +404,7 @@ namespace Duality {
bool Report; // spew on stdout
bool StratifiedInlining; // Do stratified inlining as preprocessing step
int RecursionBound; // Recursion bound for bounded verification
bool BatchExpand;
bool SetBoolOption(bool &opt, const std::string &value){
if(value == "0") {
@ -403,6 +443,9 @@ namespace Duality {
if(option == "stratified_inlining"){
return SetBoolOption(StratifiedInlining,value);
}
if(option == "batch_expand"){
return SetBoolOption(BatchExpand,value);
}
if(option == "recursion_bound"){
return SetIntOption(RecursionBound,value);
}
@ -514,7 +557,11 @@ namespace Duality {
c.Children.resize(edge->Children.size());
for(unsigned j = 0; j < c.Children.size(); j++)
c.Children[j] = leaf_map[edge->Children[j]];
Extend(c);
Node *new_node;
Extend(c,new_node);
#ifdef EARLY_EXPAND
TryExpandNode(new_node);
#endif
}
for(Unexpanded::iterator it = unexpanded.begin(), en = unexpanded.end(); it != en; ++it)
indset->Add(*it);
@ -766,16 +813,14 @@ namespace Duality {
}
/* For stratified inlining, we need a topological sort of the
nodes. */
hash_map<Node *, int> TopoSort;
int TopoSortCounter;
std::vector<Edge *> SortedEdges;
void DoTopoSortRec(Node *node){
if(TopoSort.find(node) != TopoSort.end())
return;
TopoSort[node] = TopoSortCounter++; // just to break cycles
TopoSort[node] = INT_MAX; // just to break cycles
Edge *edge = node->Outgoing; // note, this is just *one* outgoing edge
if(edge){
std::vector<Node *> &chs = edge->Children;
@ -783,23 +828,82 @@ namespace Duality {
DoTopoSortRec(chs[i]);
}
TopoSort[node] = TopoSortCounter++;
SortedEdges.push_back(edge);
}
void DoTopoSort(){
TopoSort.clear();
SortedEdges.clear();
TopoSortCounter = 0;
for(unsigned i = 0; i < nodes.size(); i++)
DoTopoSortRec(nodes[i]);
}
int StratifiedLeafCount;
#ifdef NEW_STRATIFIED_INLINING
/** Stratified inlining builds an initial layered unwinding before
switching to the LAWI strategy. Currently the number of layers
is one. Only nodes that are the targets of back edges are
consider to be leaves. This assumes we have already computed a
topological sort.
*/
bool DoStratifiedInlining(){
DoTopoSort();
int depth = 1; // TODO: make this an option
std::vector<hash_map<Node *,Node *> > unfolding_levels(depth+1);
for(int level = 1; level <= depth; level++)
for(unsigned i = 0; i < SortedEdges.size(); i++){
Edge *edge = SortedEdges[i];
Node *parent = edge->Parent;
std::vector<Node *> &chs = edge->Children;
std::vector<Node *> my_chs(chs.size());
for(unsigned j = 0; j < chs.size(); j++){
Node *child = chs[j];
int ch_level = TopoSort[child] >= TopoSort[parent] ? level-1 : level;
if(unfolding_levels[ch_level].find(child) == unfolding_levels[ch_level].end()){
if(ch_level == 0)
unfolding_levels[0][child] = CreateLeaf(child);
else
throw InternalError("in levelized unwinding");
}
my_chs[j] = unfolding_levels[ch_level][child];
}
Candidate cand; cand.edge = edge; cand.Children = my_chs;
Node *new_node;
bool ok = Extend(cand,new_node);
MarkExpanded(new_node); // we don't expand here -- just mark it done
if(!ok) return false; // got a counterexample
unfolding_levels[level][parent] = new_node;
}
return true;
}
Node *CreateLeaf(Node *node){
RPFP::Node *nchild = CreateNodeInstance(node);
MakeLeaf(nchild, /* do_not_expand = */ true);
nchild->Annotation.SetEmpty();
return nchild;
}
void MarkExpanded(Node *node){
if(unexpanded.find(node) != unexpanded.end()){
unexpanded.erase(node);
insts_of_node[node->map].push_back(node);
}
}
#else
/** In stratified inlining, we build the unwinding from the bottom
down, trying to satisfy the node bounds. We do this as a pre-pass,
limiting the expansion. If we get a counterexample, we are done,
else we continue as usual expanding the unwinding upward.
*/
int StratifiedLeafCount;
bool DoStratifiedInlining(){
timer_start("StratifiedInlining");
DoTopoSort();
@ -821,6 +925,8 @@ namespace Duality {
return true;
}
#endif
/** Here, we do the downward expansion for stratified inlining */
hash_map<Node *, Node *> LeafMap, StratifiedLeafMap;
@ -907,9 +1013,14 @@ namespace Duality {
}
Candidate cand = candidates.front();
candidates.pop_front();
if(CandidateFeasible(cand))
if(!Extend(cand))
if(CandidateFeasible(cand)){
Node *new_node;
if(!Extend(cand,new_node))
return false;
#ifdef EARLY_EXPAND
TryExpandNode(new_node);
#endif
}
}
}
@ -929,9 +1040,9 @@ namespace Duality {
Node *CreateUnderapproxNode(Node *node){
// cex.tree->ComputeUnderapprox(cex.root,0);
// cex.get_tree()->ComputeUnderapprox(cex.get_root(),0);
RPFP::Node *under_node = CreateNodeInstance(node->map /* ,StratifiedLeafCount-- */);
under_node->Annotation.IntersectWith(cex.root->Underapprox);
under_node->Annotation.IntersectWith(cex.get_root()->Underapprox);
AddThing(under_node->Annotation.Formula);
Edge *e = unwinding->CreateLowerBoundEdge(under_node);
under_node->Annotation.SetFull(); // allow this node to cover others
@ -967,9 +1078,8 @@ namespace Duality {
ExpandNodeFromCoverFail(node);
}
#endif
if(_cex) *_cex = cex;
else delete cex.tree; // delete the cex if not required
cex.tree = 0;
if(_cex) (*_cex).swap(cex); // return the cex if asked
cex.clear(); // throw away the useless cex
node->Bound = save; // put back original bound
timer_stop("ProveConjecture");
return false;
@ -1349,17 +1459,21 @@ namespace Duality {
}
}
bool UpdateNodeToNode(Node *node, Node *top){
if(!node->Annotation.SubsetEq(top->Annotation)){
reporter->Update(node,top->Annotation);
indset->Update(node,top->Annotation);
bool Update(Node *node, const RPFP::Transformer &fact, bool eager=false){
if(!node->Annotation.SubsetEq(fact)){
reporter->Update(node,fact,eager);
indset->Update(node,fact);
updated_nodes.insert(node->map);
node->Annotation.IntersectWith(top->Annotation);
node->Annotation.IntersectWith(fact);
return true;
}
return false;
}
bool UpdateNodeToNode(Node *node, Node *top){
return Update(node,top->Annotation);
}
/** Update the unwinding solution, using an interpolant for the
derivation tree. */
void UpdateWithInterpolant(Node *node, RPFP *tree, Node *top){
@ -1400,8 +1514,7 @@ namespace Duality {
// std::cout << "decisions: " << (end_decs - start_decs) << std::endl;
last_decisions = end_decs - start_decs;
if(res){
cex.tree = dt.tree;
cex.root = dt.top;
cex.set(dt.tree,dt.top); // note tree is now owned by cex
if(UseUnderapprox){
UpdateWithCounterexample(node,dt.tree,dt.top);
}
@ -1414,6 +1527,64 @@ namespace Duality {
return !res;
}
/* For a given nod in the unwinding, get conjectures from the
proposers and check them locally. Update the node with any true
conjectures.
*/
void DoEagerDeduction(Node *node){
for(unsigned i = 0; i < proposers.size(); i++){
const std::vector<RPFP::Transformer> &conjectures = proposers[i]->Propose(node);
for(unsigned j = 0; j < conjectures.size(); j++){
const RPFP::Transformer &conjecture = conjectures[j];
RPFP::Transformer bound(conjecture);
std::vector<expr> conj_vec;
unwinding->CollectConjuncts(bound.Formula,conj_vec);
for(unsigned k = 0; k < conj_vec.size(); k++){
bound.Formula = conj_vec[k];
if(CheckEdgeCaching(node->Outgoing,bound) == unsat)
Update(node,bound, /* eager = */ true);
//else
//std::cout << "conjecture failed\n";
}
}
}
}
check_result CheckEdge(RPFP *checker, Edge *edge){
Node *root = edge->Parent;
checker->Push();
checker->AssertNode(root);
checker->AssertEdge(edge,1,true);
check_result res = checker->Check(root);
checker->Pop(1);
return res;
}
check_result CheckEdgeCaching(Edge *unwinding_edge, const RPFP::Transformer &bound){
// use a dedicated solver for this edge
// TODO: can this mess be hidden somehow?
RPFP_caching *checker = gen_cands_rpfp; // TODO: a good choice?
Edge *edge = unwinding_edge->map; // get the edge in the original RPFP
RPFP_caching::scoped_solver_for_edge ssfe(checker,edge,true /* models */, true /*axioms*/);
Edge *checker_edge = checker->GetEdgeClone(edge);
// copy the annotations and bound to the clone
Node *root = checker_edge->Parent;
root->Bound = bound;
for(unsigned j = 0; j < checker_edge->Children.size(); j++){
Node *oc = unwinding_edge->Children[j];
Node *nc = checker_edge->Children[j];
nc->Annotation = oc->Annotation;
}
return CheckEdge(checker,checker_edge);
}
/* If the counterexample derivation is partial due to
use of underapproximations, complete it. */
@ -1421,10 +1592,7 @@ namespace Duality {
DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand);
bool res = dt.Derive(unwinding,node,UseUnderapprox,true); // build full tree
if(!res) throw "Duality internal error in BuildFullCex";
if(cex.tree)
delete cex.tree;
cex.tree = dt.tree;
cex.root = dt.top;
cex.set(dt.tree,dt.top);
}
void UpdateBackEdges(Node *node){
@ -1447,25 +1615,23 @@ namespace Duality {
}
/** Extend the unwinding, keeping it solved. */
bool Extend(Candidate &cand){
bool Extend(Candidate &cand, Node *&node){
timer_start("Extend");
Node *node = CreateNodeInstance(cand.edge->Parent);
node = CreateNodeInstance(cand.edge->Parent);
CreateEdgeInstance(cand.edge,node,cand.Children);
UpdateBackEdges(node);
reporter->Extend(node);
bool res = SatisfyUpperBound(node);
DoEagerDeduction(node); // first be eager...
bool res = SatisfyUpperBound(node); // then be lazy
if(res) indset->CloseDescendants(node);
else {
#ifdef UNDERAPPROX_NODES
ExpandUnderapproxNodes(cex.tree, cex.root);
ExpandUnderapproxNodes(cex.get_tree(), cex.get_root());
#endif
if(UseUnderapprox) BuildFullCex(node);
timer_stop("Extend");
return res;
}
#ifdef EARLY_EXPAND
TryExpandNode(node);
#endif
timer_stop("Extend");
return res;
}
@ -1563,6 +1729,8 @@ namespace Duality {
class DerivationTree {
public:
virtual ~DerivationTree(){}
DerivationTree(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand)
: slvr(rpfp->slvr()),
ctx(rpfp->ctx)
@ -1912,10 +2080,28 @@ namespace Duality {
stack.push_back(stack_entry());
}
struct DoRestart {};
virtual bool Build(){
while (true) {
try {
return BuildMain();
}
catch (const DoRestart &) {
// clear the statck and try again
updated_nodes.clear();
while(stack.size() > 1)
PopLevel();
reporter->Message("restarted");
}
}
}
bool BuildMain(){
stack.back().level = tree->slvr().get_scope_level();
bool was_sat = true;
int update_failures = 0;
while (true)
{
@ -1924,6 +2110,7 @@ namespace Duality {
unsigned slvr_level = tree->slvr().get_scope_level();
if(slvr_level != stack.back().level)
throw "stacks out of sync!";
reporter->Depth(stack.size());
// res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop
check_result foo = tree->Check(top);
@ -1942,11 +2129,17 @@ namespace Duality {
#ifdef NO_GENERALIZE
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
#else
try {
if(expansions.size() == 1 && NodeTooComplicated(node))
SimplifyNode(node);
else
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
Generalize(node);
}
catch(const RPFP::Bad &){
// bad interpolants can get us here
throw DoRestart();
}
#endif
if(RecordUpdate(node))
update_count++;
@ -1954,36 +2147,20 @@ namespace Duality {
heuristic->Update(node->map); // make it less likely to expand this node in future
}
if(update_count == 0){
if(was_sat)
if(was_sat){
update_failures++;
if(update_failures > 10)
throw Incompleteness();
}
reporter->Message("backtracked without learning");
}
else update_failures = 0;
}
tree->ComputeProofCore(); // need to compute the proof core before popping solver
bool propagated = false;
while(1) {
std::vector<Node *> &expansions = stack.back().expansions;
bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop
tree->Pop(1);
hash_set<Node *> leaves_to_remove;
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
// if(node != top)
// tree->ConstrainParent(node->Incoming[0],node);
std::vector<Node *> &cs = node->Outgoing->Children;
for(unsigned i = 0; i < cs.size(); i++){
leaves_to_remove.insert(cs[i]);
UnmapNode(cs[i]);
if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
throw "help!";
}
}
RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
RemoveExpansion(node);
}
stack.pop_back();
PopLevel();
if(stack.size() == 1)break;
if(prev_level_used){
Node *node = stack.back().expansions[0];
@ -2022,11 +2199,17 @@ namespace Duality {
if(tree->slvr().check() == unsat)
throw "help!";
#endif
stack.push_back(stack_entry());
stack.back().level = tree->slvr().get_scope_level();
if(ExpandSomeNodes(false,1)){
continue;
int expand_max = 1;
if(0&&duality->BatchExpand){
int thing = stack.size() * 0.1;
expand_max = std::max(1,thing);
if(expand_max > 1)
std::cout << "foo!\n";
}
if(ExpandSomeNodes(false,expand_max))
continue;
tree->Pop(1);
while(stack.size() > 1){
tree->Pop(1);
stack.pop_back();
@ -2036,6 +2219,30 @@ namespace Duality {
}
}
void PopLevel(){
std::vector<Node *> &expansions = stack.back().expansions;
tree->Pop(1);
hash_set<Node *> leaves_to_remove;
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
// if(node != top)
// tree->ConstrainParent(node->Incoming[0],node);
std::vector<Node *> &cs = node->Outgoing->Children;
for(unsigned i = 0; i < cs.size(); i++){
leaves_to_remove.insert(cs[i]);
UnmapNode(cs[i]);
if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
throw "help!";
}
}
RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
RemoveExpansion(node);
}
stack.pop_back();
}
bool NodeTooComplicated(Node *node){
int ops = tree->CountOperators(node->Annotation.Formula);
if(ops > 10) return true;
@ -2047,7 +2254,13 @@ namespace Duality {
// have to destroy the old proof to get a new interpolant
timer_start("SimplifyNode");
tree->PopPush();
try {
tree->InterpolateByCases(top,node);
}
catch(const RPFP::Bad&){
timer_stop("SimplifyNode");
throw RPFP::Bad();
}
timer_stop("SimplifyNode");
}
@ -2085,6 +2298,8 @@ namespace Duality {
std::list<Node *> updated_nodes;
virtual void ExpandNode(RPFP::Node *p){
stack.push_back(stack_entry());
stack.back().level = tree->slvr().get_scope_level();
stack.back().expansions.push_back(p);
DerivationTree::ExpandNode(p);
std::vector<Node *> &new_nodes = p->Outgoing->Children;
@ -2442,7 +2657,7 @@ namespace Duality {
}
bool ContainsCex(Node *node, Counterexample &cex){
expr val = cex.tree->Eval(cex.root->Outgoing,node->Annotation.Formula);
expr val = cex.get_tree()->Eval(cex.get_root()->Outgoing,node->Annotation.Formula);
return eq(val,parent->ctx.bool_val(true));
}
@ -2461,15 +2676,15 @@ namespace Duality {
Node *other = insts[i];
if(CouldCover(node,other)){
reporter()->Forcing(node,other);
if(cex.tree && !ContainsCex(other,cex))
if(cex.get_tree() && !ContainsCex(other,cex))
continue;
if(cex.tree) {delete cex.tree; cex.tree = 0;}
cex.clear();
if(parent->ProveConjecture(node,other->Annotation,other,&cex))
if(CloseDescendants(node))
return true;
}
}
if(cex.tree) {delete cex.tree; cex.tree = 0;}
cex.clear();
return false;
}
#else
@ -2568,13 +2783,12 @@ namespace Duality {
Counterexample old_cex;
public:
ReplayHeuristic(RPFP *_rpfp, Counterexample &_old_cex)
: Heuristic(_rpfp), old_cex(_old_cex)
: Heuristic(_rpfp)
{
old_cex.swap(_old_cex); // take ownership from caller
}
~ReplayHeuristic(){
if(old_cex.tree)
delete old_cex.tree;
}
// Maps nodes of derivation tree into old cex
@ -2582,9 +2796,7 @@ namespace Duality {
void Done() {
cex_map.clear();
if(old_cex.tree)
delete old_cex.tree;
old_cex.tree = 0; // only replay once!
old_cex.clear();
}
void ShowNodeAndChildren(Node *n){
@ -2606,7 +2818,7 @@ namespace Duality {
}
virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority, bool best_only){
if(!high_priority || !old_cex.tree){
if(!high_priority || !old_cex.get_tree()){
Heuristic::ChooseExpand(choices,best,false);
return;
}
@ -2615,7 +2827,7 @@ namespace Duality {
for(std::set<Node *>::iterator it = choices.begin(), en = choices.end(); it != en; ++it){
Node *node = (*it);
if(cex_map.empty())
cex_map[node] = old_cex.root; // match the root nodes
cex_map[node] = old_cex.get_root(); // match the root nodes
if(cex_map.find(node) == cex_map.end()){ // try to match an unmatched node
Node *parent = node->Incoming[0]->Parent; // assumes we are a tree!
if(cex_map.find(parent) == cex_map.end())
@ -2641,7 +2853,7 @@ namespace Duality {
Node *old_node = cex_map[node];
if(!old_node)
unmatched.insert(node);
else if(old_cex.tree->Empty(old_node))
else if(old_cex.get_tree()->Empty(old_node))
unmatched.insert(node);
else
matched.insert(node);
@ -2715,7 +2927,120 @@ namespace Duality {
}
};
/** This proposer class generates conjectures based on the
unwinding generated by a previous solver. The assumption is
that the provious solver was working on a different
abstraction of the same system. The trick is to adapt the
annotations in the old unwinding to the new predicates. We
start by generating a map from predicates and parameters in
the old problem to the new.
HACK: mapping is done by cheesy name comparison.
*/
class HistoryProposer : public Proposer
{
Duality *old_solver;
Duality *new_solver;
hash_map<Node *, std::vector<RPFP::Transformer> > conjectures;
public:
/** Construct a history solver. */
HistoryProposer(Duality *_old_solver, Duality *_new_solver)
: old_solver(_old_solver), new_solver(_new_solver) {
// tricky: names in the axioms may have changed -- map them
hash_set<func_decl> &old_constants = old_solver->unwinding->ls->get_constants();
hash_set<func_decl> &new_constants = new_solver->rpfp->ls->get_constants();
hash_map<std::string,func_decl> cmap;
for(hash_set<func_decl>::iterator it = new_constants.begin(), en = new_constants.end(); it != en; ++it)
cmap[GetKey(*it)] = *it;
hash_map<func_decl,func_decl> bckg_map;
for(hash_set<func_decl>::iterator it = old_constants.begin(), en = old_constants.end(); it != en; ++it){
func_decl f = new_solver->ctx.translate(*it); // move to new context
if(cmap.find(GetKey(f)) != cmap.end())
bckg_map[f] = cmap[GetKey(f)];
// else
// std::cout << "constant not matched\n";
}
RPFP *old_unwinding = old_solver->unwinding;
hash_map<std::string, std::vector<Node *> > pred_match;
// index all the predicates in the old unwinding
for(unsigned i = 0; i < old_unwinding->nodes.size(); i++){
Node *node = old_unwinding->nodes[i];
std::string key = GetKey(node);
pred_match[key].push_back(node);
}
// match with predicates in the new RPFP
RPFP *rpfp = new_solver->rpfp;
for(unsigned i = 0; i < rpfp->nodes.size(); i++){
Node *node = rpfp->nodes[i];
std::string key = GetKey(node);
std::vector<Node *> &matches = pred_match[key];
for(unsigned j = 0; j < matches.size(); j++)
MatchNodes(node,matches[j],bckg_map);
}
}
virtual std::vector<RPFP::Transformer> &Propose(Node *node){
return conjectures[node->map];
}
virtual ~HistoryProposer(){
};
private:
void MatchNodes(Node *new_node, Node *old_node, hash_map<func_decl,func_decl> &bckg_map){
if(old_node->Annotation.IsFull())
return; // don't conjecture true!
hash_map<std::string, expr> var_match;
std::vector<expr> &new_params = new_node->Annotation.IndParams;
// Index the new parameters by their keys
for(unsigned i = 0; i < new_params.size(); i++)
var_match[GetKey(new_params[i])] = new_params[i];
RPFP::Transformer &old = old_node->Annotation;
std::vector<expr> from_params = old.IndParams;
for(unsigned j = 0; j < from_params.size(); j++)
from_params[j] = new_solver->ctx.translate(from_params[j]); // get in new context
std::vector<expr> to_params = from_params;
for(unsigned j = 0; j < to_params.size(); j++){
std::string key = GetKey(to_params[j]);
if(var_match.find(key) == var_match.end()){
// std::cout << "unmatched parameter!\n";
return;
}
to_params[j] = var_match[key];
}
expr fmla = new_solver->ctx.translate(old.Formula); // get in new context
fmla = new_solver->rpfp->SubstParams(old.IndParams,to_params,fmla); // substitute parameters
hash_map<ast,expr> memo;
fmla = new_solver->rpfp->SubstRec(memo,bckg_map,fmla); // substitute background constants
RPFP::Transformer new_annot = new_node->Annotation;
new_annot.Formula = fmla;
conjectures[new_node].push_back(new_annot);
}
// We match names by removing suffixes beginning with double at sign
std::string GetKey(Node *node){
return GetKey(node->Name);
}
std::string GetKey(const expr &var){
return GetKey(var.decl());
}
std::string GetKey(const func_decl &f){
std::string name = f.name().str();
int idx = name.find("@@");
if(idx >= 0)
name.erase(idx);
return name;
}
};
};
@ -2723,8 +3048,9 @@ namespace Duality {
std::ostream &s;
public:
StreamReporter(RPFP *_rpfp, std::ostream &_s)
: Reporter(_rpfp), s(_s) {event = 0;}
: Reporter(_rpfp), s(_s) {event = 0; depth = -1;}
int event;
int depth;
void ev(){
s << "[" << event++ << "]" ;
}
@ -2735,23 +3061,30 @@ namespace Duality {
s << " " << rps[i]->number;
s << std::endl;
}
virtual void Update(RPFP::Node *node, const RPFP::Transformer &update){
virtual void Update(RPFP::Node *node, const RPFP::Transformer &update, bool eager){
ev(); s << "update " << node->number << " " << node->Name.name() << ": ";
rpfp->Summarize(update.Formula);
std::cout << std::endl;
if(depth > 0) s << " (depth=" << depth << ")";
if(eager) s << " (eager)";
s << std::endl;
}
virtual void Bound(RPFP::Node *node){
ev(); s << "check " << node->number << std::endl;
}
virtual void Expand(RPFP::Edge *edge){
RPFP::Node *node = edge->Parent;
ev(); s << "expand " << node->map->number << " " << node->Name.name() << std::endl;
ev(); s << "expand " << node->map->number << " " << node->Name.name();
if(depth > 0) s << " (depth=" << depth << ")";
s << std::endl;
}
virtual void Depth(int d){
depth = d;
}
virtual void AddCover(RPFP::Node *covered, std::vector<RPFP::Node *> &covering){
ev(); s << "cover " << covered->Name.name() << ": " << covered->number << " by ";
for(unsigned i = 0; i < covering.size(); i++)
std::cout << covering[i]->number << " ";
std::cout << std::endl;
s << covering[i]->number << " ";
s << std::endl;
}
virtual void RemoveCover(RPFP::Node *covered, RPFP::Node *covering){
ev(); s << "uncover " << covered->Name.name() << ": " << covered->number << " by " << covering->number << std::endl;
@ -2762,7 +3095,7 @@ namespace Duality {
virtual void Conjecture(RPFP::Node *node, const RPFP::Transformer &t){
ev(); s << "conjecture " << node->number << " " << node->Name.name() << ": ";
rpfp->Summarize(t.Formula);
std::cout << std::endl;
s << std::endl;
}
virtual void Dominates(RPFP::Node *node, RPFP::Node *other){
ev(); s << "dominates " << node->Name.name() << ": " << node->number << " > " << other->number << std::endl;

34
src/duality/duality_wrapper.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -37,16 +37,18 @@ Revision History:
namespace Duality {
solver::solver(Duality::context& c, bool extensional, bool models) : object(c), the_model(c) {
solver::solver(Duality::context& c, bool _extensional, bool models) : object(c), the_model(c) {
params_ref p;
p.set_bool("proof", true); // this is currently useless
if(models)
p.set_bool("model", true);
p.set_bool("unsat_core", true);
p.set_bool("mbqi",true);
bool mbqi = c.get_config().get().get_bool("mbqi",true);
p.set_bool("mbqi",mbqi); // just to test
p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants
p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants
if(true || extensional)
extensional = mbqi && (true || _extensional);
if(extensional)
p.set_bool("array.extensional",true);
scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
@ -339,6 +341,12 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
return simplify(p);
}
expr context::make_var(int idx, const sort &s){
::sort * a = to_sort(s.raw());
return cook(m().mk_var(idx,a));
}
expr expr::qe_lite() const {
::qe_lite qe(m());
expr_ref result(to_expr(raw()),m());
@ -372,6 +380,12 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, &_patterns[0], to_expr(b.raw())));
}
expr clone_quantifier(decl_kind dk, const expr &q, const expr &b){
quantifier *thing = to_quantifier(q.raw());
bool is_forall = dk == Forall;
return q.ctx().cook(q.m().update_quantifier(thing, is_forall, to_expr(b.raw())));
}
void expr::get_patterns(std::vector<expr> &pats) const {
quantifier *thing = to_quantifier(raw());
unsigned num_patterns = thing->get_num_patterns();
@ -656,6 +670,18 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
pp.display_smt2(std::cout, m_solver->get_assertion(n-1));
}
void solver::print(const char *filename) {
std::ofstream f(filename);
unsigned n = m_solver->get_num_assertions();
if(!n)
return;
ast_smt_pp pp(m());
for (unsigned i = 0; i < n-1; ++i)
pp.add_assumption(m_solver->get_assertion(i));
pp.display_smt2(f, m_solver->get_assertion(n-1));
}
void solver::show_assertion_ids() {
#if 0
unsigned n = m_solver->get_num_assertions();

51
src/duality/duality_wrapper.h
View file

@ -182,6 +182,7 @@ namespace Duality {
void set(char const * param, char const * value) { m_config.set(param,value); }
void set(char const * param, bool value) { m_config.set(param,value); }
void set(char const * param, int value) { m_config.set(param,value); }
config &get_config() {return m_config;}
symbol str_symbol(char const * s);
symbol int_symbol(int n);
@ -237,12 +238,15 @@ namespace Duality {
expr make_quant(decl_kind op, const std::vector<expr> &bvs, const expr &body);
expr make_quant(decl_kind op, const std::vector<sort> &_sorts, const std::vector<symbol> &_names, const expr &body);
expr make_var(int idx, const sort &s);
decl_kind get_decl_kind(const func_decl &t);
sort_kind get_sort_kind(const sort &s);
expr translate(const expr &e);
func_decl translate(const func_decl &);
void print_expr(std::ostream &s, const ast &e);
fixedpoint mk_fixedpoint();
@ -462,6 +466,16 @@ namespace Duality {
bool is_label (bool &pos,std::vector<symbol> &names) const ;
bool is_ground() const {return to_app(raw())->is_ground();}
bool has_quantifiers() const {return to_app(raw())->has_quantifiers();}
bool has_free(int idx) const {
used_vars proc;
proc.process(to_expr(raw()));
return proc.contains(idx);
}
unsigned get_max_var_idx_plus_1() const {
used_vars proc;
proc.process(to_expr(raw()));
return proc.get_max_found_var_idx_plus_1();
}
// operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());}
@ -569,6 +583,8 @@ namespace Duality {
friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);
friend expr clone_quantifier(decl_kind, const expr &, const expr &);
friend std::ostream & operator<<(std::ostream & out, expr const & m){
m.ctx().print_expr(out,m);
return out;
@ -818,6 +834,7 @@ namespace Duality {
model the_model;
bool canceled;
proof_gen_mode m_mode;
bool extensional;
public:
solver(context & c, bool extensional = false, bool models = true);
solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;}
@ -921,6 +938,7 @@ namespace Duality {
unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();}
void show();
void print(const char *filename);
void show_assertion_ids();
proof get_proof(){
@ -928,6 +946,7 @@ namespace Duality {
return proof(ctx(),m_solver->get_proof());
}
bool extensional_array_theory() {return extensional;}
};
#if 0
@ -1370,6 +1389,20 @@ namespace Duality {
return to_expr(a.raw());
}
inline expr context::translate(const expr &e) {
::expr *f = to_expr(e.raw());
if(&e.ctx().m() != &m()) // same ast manager -> no translation
throw "ast manager mismatch";
return cook(f);
}
inline func_decl context::translate(const func_decl &e) {
::func_decl *f = to_func_decl(e.raw());
if(&e.ctx().m() != &m()) // same ast manager -> no translation
throw "ast manager mismatch";
return func_decl(*this,f);
}
typedef double clock_t;
clock_t current_time();
inline void output_time(std::ostream &os, clock_t time){os << time;}
@ -1401,14 +1434,6 @@ namespace hash_space {
};
}
// to make Duality::ast hashable in windows
#ifdef _WINDOWS
template <> inline
size_t stdext::hash_value<Duality::ast >(const Duality::ast& s)
{
return s.raw()->get_id();
}
#endif
// to make Duality::ast usable in ordered collections
namespace std {
@ -1445,14 +1470,6 @@ namespace hash_space {
};
}
// to make Duality::func_decl hashable in windows
#ifdef _WINDOWS
template <> inline
size_t stdext::hash_value<Duality::func_decl >(const Duality::func_decl& s)
{
return s.raw()->get_id();
}
#endif
// to make Duality::func_decl usable in ordered collections
namespace std {

2
src/interp/foci2.h
View file

@ -23,7 +23,7 @@ Revision History:
#include <vector>
#include <string>
#ifdef WIN32
#ifdef _WINDOWS
#define FOCI2_EXPORT __declspec(dllexport)
#else
#define FOCI2_EXPORT __attribute__ ((visibility ("default")))

4
src/interp/iz3base.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -34,9 +34,7 @@ Revision History:
#include "../smt/smt_solver.h"
#ifndef WIN32
using namespace stl_ext;
#endif
iz3base::range &iz3base::ast_range(ast t){

4
src/interp/iz3checker.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -36,9 +36,7 @@ Revision History:
#include <iterator>
#ifndef WIN32
using namespace stl_ext;
#endif
struct iz3checker : iz3base {

2
src/interp/iz3foci.cpp
View file

@ -25,9 +25,7 @@ Revision History:
#include "foci2.h"
#include "iz3foci.h"
#ifndef WIN32
using namespace stl_ext;
#endif
class iz3foci_impl : public iz3secondary {

549
src/interp/iz3hash.h Executable file → Normal file
View file

@ -7,7 +7,16 @@ Module Name:
Abstract:
Wrapper for stl hash tables
Simple implementation of bucket-list hash tables conforming to SGI
hash_map and hash_set interfaces. Just enough members are
implemented to support iz3 and duality.
iz3 and duality need this package because they assume that insert
preserves iterators and references to elements, which is not true
of the hashtable packages in util.
This package lives in namespace hash_space. Specializations of
class "hash" should be made in this namespace.
Author:
@ -17,66 +26,36 @@ Revision History:
--*/
// pull in the headers for has_map and hash_set
// these live in non-standard places
#ifndef IZ3_HASH_H
#define IZ3_HASH_H
//#define USE_UNORDERED_MAP
#ifdef USE_UNORDERED_MAP
#define stl_ext std
#define hash_space std
#include <unordered_map>
#include <unordered_set>
#define hash_map unordered_map
#define hash_set unordered_set
#else
#if __GNUC__ >= 3
#undef __DEPRECATED
#define stl_ext __gnu_cxx
#define hash_space stl_ext
#include <ext/hash_map>
#include <ext/hash_set>
#else
#ifdef _WINDOWS
#define stl_ext stdext
#define hash_space std
#include <hash_map>
#include <hash_set>
#else
#define stl_ext std
#define hash_space std
#include <hash_map>
#include <hash_set>
#endif
#endif
#endif
#include <string>
#include <vector>
#include <iterator>
#include "hash.h"
// stupid STL doesn't include hash function for class string
#ifndef _WINDOWS
namespace stl_ext {
template <>
class hash<std::string> {
stl_ext::hash<const char *> H;
public:
size_t operator()(const std::string &s) const {
return H(s.c_str());
}
};
}
#endif
#define stl_ext hash_space
namespace hash_space {
template <typename T> class hash {};
template <>
class hash<int> {
public:
size_t operator()(const int &s) const {
return s;
}
};
template <>
class hash<std::string> {
public:
size_t operator()(const std::string &s) const {
return string_hash(s.c_str(), s.size(), 0);
}
};
template <>
class hash<std::pair<int,int> > {
public:
@ -84,17 +63,7 @@ namespace hash_space {
return p.first + p.second;
}
};
}
#ifdef _WINDOWS
template <> inline
size_t stdext::hash_value<std::pair<int,int> >(const std::pair<int,int>& p)
{ // hash _Keyval to size_t value one-to-one
return p.first + p.second;
}
#endif
namespace hash_space {
template <class T>
class hash<std::pair<T *, T *> > {
public:
@ -102,70 +71,404 @@ namespace hash_space {
return (size_t)p.first + (size_t)p.second;
}
};
enum { num_primes = 29 };
static const unsigned long primes[num_primes] =
{
7ul,
53ul,
97ul,
193ul,
389ul,
769ul,
1543ul,
3079ul,
6151ul,
12289ul,
24593ul,
49157ul,
98317ul,
196613ul,
393241ul,
786433ul,
1572869ul,
3145739ul,
6291469ul,
12582917ul,
25165843ul,
50331653ul,
100663319ul,
201326611ul,
402653189ul,
805306457ul,
1610612741ul,
3221225473ul,
4294967291ul
};
inline unsigned long next_prime(unsigned long n) {
const unsigned long* to = primes + (int)num_primes;
for(const unsigned long* p = primes; p < to; p++)
if(*p >= n) return *p;
return primes[num_primes-1];
}
#if 0
template <class T> inline
size_t stdext::hash_value<std::pair<T *, T *> >(const std::pair<T *, T *>& p)
{ // hash _Keyval to size_t value one-to-one
return (size_t)p.first + (size_t)p.second;
}
#endif
#ifdef _WINDOWS
namespace std {
template <>
class less<std::pair<int,int> > {
template<class Value, class Key, class HashFun, class GetKey, class KeyEqFun>
class hashtable
{
public:
bool operator()(const pair<int,int> &x, const pair<int,int> &y) const {
return x.first < y.first || x.first == y.first && x.second < y.second;
typedef Value &reference;
typedef const Value &const_reference;
struct Entry
{
Entry* next;
Value val;
Entry(const Value &_val) : val(_val) {next = 0;}
};
struct iterator
{
Entry* ent;
hashtable* tab;
typedef std::forward_iterator_tag iterator_category;
typedef Value value_type;
typedef std::ptrdiff_t difference_type;
typedef size_t size_type;
typedef Value& reference;
typedef Value* pointer;
iterator(Entry* _ent, hashtable* _tab) : ent(_ent), tab(_tab) { }
iterator() { }
Value &operator*() const { return ent->val; }
Value *operator->() const { return &(operator*()); }
iterator &operator++() {
Entry *old = ent;
ent = ent->next;
if (!ent) {
size_t bucket = tab->get_bucket(old->val);
while (!ent && ++bucket < tab->buckets.size())
ent = tab->buckets[bucket];
}
return *this;
}
iterator operator++(int) {
iterator tmp = *this;
operator++();
return tmp;
}
bool operator==(const iterator& it) const {
return ent == it.ent;
}
bool operator!=(const iterator& it) const {
return ent != it.ent;
}
};
struct const_iterator
{
const Entry* ent;
const hashtable* tab;
typedef std::forward_iterator_tag iterator_category;
typedef Value value_type;
typedef std::ptrdiff_t difference_type;
typedef size_t size_type;
typedef const Value& reference;
typedef const Value* pointer;
const_iterator(const Entry* _ent, const hashtable* _tab) : ent(_ent), tab(_tab) { }
const_iterator() { }
const Value &operator*() const { return ent->val; }
const Value *operator->() const { return &(operator*()); }
const_iterator &operator++() {
Entry *old = ent;
ent = ent->next;
if (!ent) {
size_t bucket = tab->get_bucket(old->val);
while (!ent && ++bucket < tab->buckets.size())
ent = tab->buckets[bucket];
}
return *this;
}
const_iterator operator++(int) {
const_iterator tmp = *this;
operator++();
return tmp;
}
bool operator==(const const_iterator& it) const {
return ent == it.ent;
}
bool operator!=(const const_iterator& it) const {
return ent != it.ent;
}
};
private:
typedef std::vector<Entry*> Table;
Table buckets;
size_t entries;
HashFun hash_fun ;
GetKey get_key;
KeyEqFun key_eq_fun;
public:
hashtable(size_t init_size) : buckets(init_size,(Entry *)0) {
entries = 0;
}
hashtable(const hashtable& other) {
dup(other);
}
hashtable& operator= (const hashtable& other) {
if (&other != this)
dup(other);
return *this;
}
~hashtable() {
clear();
}
size_t size() const {
return entries;
}
bool empty() const {
return size() == 0;
}
void swap(hashtable& other) {
buckets.swap(other.buckets);
std::swap(entries, other.entries);
}
iterator begin() {
for (size_t i = 0; i < buckets.size(); ++i)
if (buckets[i])
return iterator(buckets[i], this);
return end();
}
iterator end() {
return iterator(0, this);
}
const_iterator begin() const {
for (size_t i = 0; i < buckets.size(); ++i)
if (buckets[i])
return const_iterator(buckets[i], this);
return end();
}
const_iterator end() const {
return const_iterator(0, this);
}
size_t get_bucket(const Value& val, size_t n) const {
return hash_fun(get_key(val)) % n;
}
size_t get_key_bucket(const Key& key) const {
return hash_fun(key) % buckets.size();
}
size_t get_bucket(const Value& val) const {
return get_bucket(val,buckets.size());
}
Entry *lookup(const Value& val, bool ins = false)
{
resize(entries + 1);
size_t n = get_bucket(val);
Entry* from = buckets[n];
for (Entry* ent = from; ent; ent = ent->next)
if (key_eq_fun(get_key(ent->val), get_key(val)))
return ent;
if(!ins) return 0;
Entry* tmp = new Entry(val);
tmp->next = from;
buckets[n] = tmp;
++entries;
return tmp;
}
Entry *lookup_key(const Key& key) const
{
size_t n = get_key_bucket(key);
Entry* from = buckets[n];
for (Entry* ent = from; ent; ent = ent->next)
if (key_eq_fun(get_key(ent->val), key))
return ent;
return 0;
}
const_iterator find(const Key& key) const {
return const_iterator(lookup_key(key),this);
}
iterator find(const Key& key) {
return iterator(lookup_key(key),this);
}
std::pair<iterator,bool> insert(const Value& val){
size_t old_entries = entries;
Entry *ent = lookup(val,true);
return std::pair<iterator,bool>(iterator(ent,this),entries > old_entries);
}
iterator insert(const iterator &it, const Value& val){
Entry *ent = lookup(val,true);
return iterator(ent,this);
}
size_t erase(const Key& key)
{
Entry** p = &(buckets[get_key_bucket(key)]);
size_t count = 0;
while(*p){
Entry *q = *p;
if (key_eq_fun(get_key(q->val), key)) {
++count;
*p = q->next;
delete q;
}
else
p = &(q->next);
}
entries -= count;
return count;
}
void resize(size_t new_size) {
const size_t old_n = buckets.size();
if (new_size <= old_n) return;
const size_t n = next_prime(new_size);
if (n <= old_n) return;
Table tmp(n, (Entry*)(0));
for (size_t i = 0; i < old_n; ++i) {
Entry* ent = buckets[i];
while (ent) {
size_t new_bucket = get_bucket(ent->val, n);
buckets[i] = ent->next;
ent->next = tmp[new_bucket];
tmp[new_bucket] = ent;
ent = buckets[i];
}
}
buckets.swap(tmp);
}
void clear()
{
for (size_t i = 0; i < buckets.size(); ++i) {
for (Entry* ent = buckets[i]; ent != 0;) {
Entry* next = ent->next;
delete ent;
ent = next;
}
buckets[i] = 0;
}
entries = 0;
}
void dup(const hashtable& other)
{
buckets.resize(other.buckets.size());
for (size_t i = 0; i < other.buckets.size(); ++i) {
Entry** to = &buckets[i];
for (Entry* from = other.buckets[i]; from; from = from->next)
to = &((*to = new Entry(from->val))->next);
}
entries = other.entries;
}
};
template <typename T>
class equal {
public:
bool operator()(const T& x, const T &y) const {
return x == y;
}
};
template <typename T>
class identity {
public:
const T &operator()(const T &x) const {
return x;
}
};
template <typename T, typename U>
class proj1 {
public:
const T &operator()(const std::pair<T,U> &x) const {
return x.first;
}
};
template <typename Element, class HashFun = hash<Element>,
class EqFun = equal<Element> >
class hash_set
: public hashtable<Element,Element,HashFun,identity<Element>,EqFun> {
public:
typedef Element value_type;
hash_set()
: hashtable<Element,Element,HashFun,identity<Element>,EqFun>(7) {}
};
template <typename Key, typename Value, class HashFun = hash<Key>,
class EqFun = equal<Key> >
class hash_map
: public hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun> {
public:
hash_map()
: hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun>(7) {}
Value &operator[](const Key& key) {
std::pair<Key,Value> kvp(key,Value());
return
hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun>::
lookup(kvp,true)->val.second;
}
};
}
namespace std {
template <class T>
class less<std::pair<T *,T *> > {
public:
bool operator()(const pair<T *,T *> &x, const pair<T *,T *> &y) const {
return (size_t)x.first < (size_t)y.first || (size_t)x.first == (size_t)y.first && (size_t)x.second < (size_t)y.second;
}
};
}
#endif
#ifndef _WINDOWS
#if 0
namespace stl_ext {
template <class T>
class hash<T *> {
public:
size_t operator()(const T *p) const {
return (size_t) p;
}
};
}
#endif
#endif
#ifdef _WINDOWS
template <class K, class T>
class hash_map : public stl_ext::hash_map<K,T,stl_ext::hash_compare<K,std::less<K> > > {};
template <class K>
class hash_set : public stl_ext::hash_set<K,stl_ext::hash_compare<K,std::less<K> > > {};
#endif
#endif

6
src/interp/iz3interp.cpp
View file

@ -19,7 +19,7 @@ Revision History:
/* Copyright 2011 Microsoft Research. */
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -43,9 +43,7 @@ Revision History:
#ifndef WIN32
using namespace stl_ext;
#endif
@ -64,7 +62,7 @@ struct frame_reducer : public iz3mgr {
: iz3mgr(other) {}
void get_proof_assumptions_rec(z3pf proof, hash_set<ast> &memo, std::vector<bool> &used_frames){
if(memo.count(proof))return;
if(memo.find(proof) != memo.end())return;
memo.insert(proof);
pfrule dk = pr(proof);
if(dk == PR_ASSERTED){

4
src/interp/iz3mgr.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -38,9 +38,7 @@ Revision History:
#include "params.h"
#ifndef WIN32
using namespace stl_ext;
#endif
std::ostream &operator <<(std::ostream &s, const iz3mgr::ast &a){

8
src/interp/iz3mgr.h
View file

@ -126,14 +126,6 @@ namespace hash_space {
};
}
// to make ast_r hashable in windows
#ifdef _WINDOWS
template <> inline
size_t stdext::hash_value<ast_r >(const ast_r& s)
{
return s.raw()->get_id();
}
#endif
// to make ast_r usable in ordered collections
namespace std {

4
src/interp/iz3pp.cpp
View file

@ -36,11 +36,8 @@ Revision History:
#include"expr_abstract.h"
#ifndef WIN32
using namespace stl_ext;
#endif
#ifndef WIN32
// We promise not to use this for hash_map with range destructor
namespace stl_ext {
template <>
@ -51,7 +48,6 @@ namespace stl_ext {
}
};
}
#endif
// TBD: algebraic data-types declarations will not be printed.

2
src/interp/iz3profiling.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)

2
src/interp/iz3proof.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)

198
src/interp/iz3proof_itp.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -26,9 +26,7 @@ Revision History:
#include "iz3proof_itp.h"
#ifndef WIN32
using namespace stl_ext;
#endif
// #define INVARIANT_CHECKING
@ -369,12 +367,18 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
default:
{
opr o = op(itp2);
if(o == Uninterpreted){
symb s = sym(itp2);
if(s == sforall || s == sexists)
res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1)));
else
res = itp2;
}
else {
res = itp2;
}
}
}
}
return res;
@ -405,12 +409,18 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
default:
{
opr o = op(itp1);
if(o == Uninterpreted){
symb s = sym(itp1);
if(s == sforall || s == sexists)
res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2));
else
res = itp1;
}
else {
res = itp1;
}
}
}
}
return res;
@ -464,6 +474,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo);
ast &res = bar.first->second;
if(bar.second){
if(op(e) == Uninterpreted){
symb g = sym(e);
if(g == rotate_sum){
if(var == get_placeholder(arg(e,0))){
@ -477,6 +488,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
res = e;
return res;
}
}
int nargs = num_args(e);
std::vector<ast> args(nargs);
for(int i = 0; i < nargs; i++)
@ -538,8 +550,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
else if(g == symm) res = simplify_symm(args);
else if(g == modpon) res = simplify_modpon(args);
else if(g == sum) res = simplify_sum(args);
#if 0
else if(g == exmid) res = simplify_exmid(args);
else if(g == cong) res = simplify_cong(args);
#if 0
else if(g == modpon) res = simplify_modpon(args);
else if(g == leq2eq) res = simplify_leq2eq(args);
else if(g == eq2leq) res = simplify_eq2leq(args);
@ -680,7 +693,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast dummy1, dummy2;
sum_cond_ineq(in1,coeff2,in2,dummy1,dummy2);
n1 = merge_normal_chains(n1,n2, Aproves, Bproves);
ineq = make_normal(in1,n1);
ineq = is_true(n1) ? in1 : make_normal(in1,n1);
}
bool is_ineq(const ast &ineq){
@ -729,29 +742,31 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast x = arg(equality,0);
ast y = arg(equality,1);
ast Aproves1 = mk_true(), Bproves1 = mk_true();
ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),Aproves1,Bproves1));
ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),Aproves1,Bproves1));
ast pf1 = destruct_cond_ineq(arg(pf,1), Aproves1, Bproves1);
ast pf2 = destruct_cond_ineq(arg(pf,2), Aproves1, Bproves1);
ast xleqy = round_ineq(ineq_from_chain(pf1,Aproves1,Bproves1));
ast yleqx = round_ineq(ineq_from_chain(pf2,Aproves1,Bproves1));
ast ineq1 = make(Leq,make_int("0"),make_int("0"));
sum_cond_ineq(ineq1,make_int("-1"),xleqy,Aproves1,Bproves1);
sum_cond_ineq(ineq1,make_int("-1"),yleqx,Aproves1,Bproves1);
Bproves1 = my_and(Bproves1,z3_simplify(ineq1));
ast Acond = my_implies(Aproves1,my_and(Bproves1,z3_simplify(ineq1)));
ast Aproves2 = mk_true(), Bproves2 = mk_true();
ast ineq2 = make(Leq,make_int("0"),make_int("0"));
sum_cond_ineq(ineq2,make_int("1"),xleqy,Aproves2,Bproves2);
sum_cond_ineq(ineq2,make_int("1"),yleqx,Aproves2,Bproves2);
Bproves2 = z3_simplify(ineq2);
if(!is_true(Aproves1) || !is_true(Aproves2))
throw "help!";
ast Bcond = my_implies(Bproves1,my_and(Aproves1,z3_simplify(ineq2)));
// if(!is_true(Aproves1) || !is_true(Bproves1))
// std::cout << "foo!\n";;
if(get_term_type(x) == LitA){
ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy)));
ast rewrite1 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,x,iter));
ast rewrite2 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,iter,y));
ast rewrite1 = make_rewrite(LitA,top_pos,Acond,make(Equal,x,iter));
ast rewrite2 = make_rewrite(LitB,top_pos,Bcond,make(Equal,iter,y));
return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
}
if(get_term_type(y) == LitA){
ast iter = z3_simplify(make(Plus,y,get_ineq_rhs(yleqx)));
ast rewrite2 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,iter,y));
ast rewrite1 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,x,iter));
ast rewrite2 = make_rewrite(LitA,top_pos,Acond,make(Equal,iter,y));
ast rewrite1 = make_rewrite(LitB,top_pos,Bcond,make(Equal,x,iter));
return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
}
throw cannot_simplify();
@ -760,6 +775,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
ast round_ineq(const ast &ineq){
if(sym(ineq) == normal)
return make_normal(round_ineq(arg(ineq,0)),arg(ineq,1));
if(!is_ineq(ineq))
throw cannot_simplify();
ast res = simplify_ineq(ineq);
@ -790,12 +807,17 @@ class iz3proof_itp_impl : public iz3proof_itp {
return simplify_sum(args);
}
ast simplify_rotate_eq2leq(const ast &pl, const ast &neg_equality, const ast &pf){
if(pl == arg(pf,1)){
ast cond = mk_true();
ast equa = sep_cond(arg(pf,0),cond);
if(is_equivrel_chain(equa)){
ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove
if(!rewrites_from_to(equa,lhs,rhs)){
lhs = arg(arg(neg_equality,0),0); // the equality proved is ambiguous, sadly
rhs = arg(arg(neg_equality,0),1);
}
LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs);
if(lhst != LitMixed && rhst != LitMixed)
return unmixed_eq2ineq(lhs, rhs, op(arg(neg_equality,0)), equa, cond);
@ -920,6 +942,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
return chain;
}
struct subterm_normals_failed {};
void get_subterm_normals(const ast &ineq1, const ast &ineq2, const ast &chain, ast &normals,
const ast &pos, hash_set<ast> &memo, ast &Aproves, ast &Bproves){
opr o1 = op(ineq1);
@ -933,7 +957,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
get_subterm_normals(arg(ineq1,i), arg(ineq2,i), chain, normals, new_pos, memo, Aproves, Bproves);
}
}
else if(get_term_type(ineq2) == LitMixed && memo.find(ineq2) == memo.end()){
else if(get_term_type(ineq2) == LitMixed){
if(memo.find(ineq2) == memo.end()){
memo.insert(ineq2);
ast sub_chain = extract_rewrites(chain,pos);
if(is_true(sub_chain))
@ -942,6 +967,68 @@ class iz3proof_itp_impl : public iz3proof_itp {
normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
}
}
else if(!(ineq1 == ineq2))
throw subterm_normals_failed();
}
ast rewrites_to_normals(const ast &ineq1, const ast &chain, ast &normals, ast &Aproves, ast &Bproves, ast &Aineqs){
if(is_true(chain))
return ineq1;
ast last = chain_last(chain);
ast rest = chain_rest(chain);
ast new_ineq1 = rewrites_to_normals(ineq1, rest, normals, Aproves, Bproves, Aineqs);
ast p1 = rewrite_pos(last);
ast term1;
ast coeff = arith_rewrite_coeff(new_ineq1,p1,term1);
ast res = subst_in_pos(new_ineq1,rewrite_pos(last),rewrite_rhs(last));
ast rpos;
pos_diff(p1,rewrite_pos(last),rpos);
ast term2 = subst_in_pos(term1,rpos,rewrite_rhs(last));
if(get_term_type(term1) != LitMixed && get_term_type(term2) != LitMixed){
if(is_rewrite_side(LitA,last))
linear_comb(Aineqs,coeff,make(Leq,make_int(rational(0)),make(Sub,term2,term1)));
}
else {
ast pf = extract_rewrites(make(concat,mk_true(),rest),p1);
ast new_normal = fix_normal(term1,term2,pf);
normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
}
return res;
}
ast arith_rewrite_coeff(const ast &ineq, ast &p1, ast &term){
ast coeff = make_int(rational(1));
if(p1 == top_pos){
term = ineq;
return coeff;
}
int argpos = pos_arg(p1);
opr o = op(ineq);
switch(o){
case Leq:
case Lt:
coeff = argpos ? make_int(rational(1)) : make_int(rational(-1));
break;
case Geq:
case Gt:
coeff = argpos ? make_int(rational(-1)) : make_int(rational(1));
break;
case Not:
case Plus:
break;
case Times:
coeff = arg(ineq,0);
break;
default:
p1 = top_pos;
term = ineq;
return coeff;
}
p1 = arg(p1,1);
ast res = arith_rewrite_coeff(arg(ineq,argpos),p1,term);
p1 = pos_add(argpos,p1);
return coeff == make_int(rational(1)) ? res : make(Times,coeff,res);
}
ast rewrite_chain_to_normal_ineq(const ast &chain, ast &Aproves, ast &Bproves){
ast tail, pref = get_head_chain(chain,tail,false); // pref is x=y, tail is x=y -> x'=y'
@ -950,20 +1037,25 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast ineq2 = apply_rewrite_chain(ineq1,tail);
ast nc = mk_true();
hash_set<ast> memo;
ast itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
ast Aproves_save = Aproves, Bproves_save = Bproves; try {
get_subterm_normals(ineq1,ineq2,tail,nc,top_pos,memo, Aproves, Bproves);
ast itp;
}
catch (const subterm_normals_failed &){ Aproves = Aproves_save; Bproves = Bproves_save; nc = mk_true();
rewrites_to_normals(ineq1, tail, nc, Aproves, Bproves, itp);
}
if(is_rewrite_side(LitA,head)){
itp = make(Leq,make_int("0"),make_int("0"));
linear_comb(itp,make_int("1"),ineq1); // make sure it is normal form
//itp = ineq1;
ast mc = z3_simplify(chain_side_proves(LitB,pref));
Bproves = my_and(Bproves,mc);
}
else {
itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
ast mc = z3_simplify(chain_side_proves(LitA,pref));
Aproves = my_and(Aproves,mc);
}
if(is_true(nc))
return itp;
return make_normal(itp,nc);
}
@ -1010,6 +1102,31 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
ast simplify_exmid(const std::vector<ast> &args){
if(is_equivrel(args[0])){
ast Aproves = mk_true(), Bproves = mk_true();
ast chain = destruct_cond_ineq(args[1],Aproves,Bproves);
ast Q2 = destruct_cond_ineq(args[2],Aproves,Bproves);
ast interp = contra_chain(Q2,chain);
return my_and(Aproves,my_implies(Bproves,interp));
}
throw "bad exmid";
}
ast simplify_cong(const std::vector<ast> &args){
ast Aproves = mk_true(), Bproves = mk_true();
ast chain = destruct_cond_ineq(args[0],Aproves,Bproves);
rational pos;
if(is_numeral(args[1],pos)){
int ipos = pos.get_unsigned();
chain = chain_pos_add(ipos,chain);
ast Q2 = destruct_cond_ineq(args[2],Aproves,Bproves);
ast interp = contra_chain(Q2,chain);
return my_and(Aproves,my_implies(Bproves,interp));
}
throw "bad cong";
}
bool is_equivrel(const ast &p){
opr o = op(p);
return o == Equal || o == Iff;
@ -1294,6 +1411,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
if(pos == top_pos && op(equality) == Iff && !is_true(arg(equality,0)))
throw "bad rewrite";
#endif
if(!is_equivrel(equality))
throw "bad rewrite";
return make(t == LitA ? rewrite_A : rewrite_B, pos, cond, equality);
}
@ -1556,9 +1675,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
return head;
}
// split a rewrite chain into head and tail at last non-mixed term
bool has_mixed_summands(const ast &e){
if(op(e) == Plus){
int nargs = num_args(e);
for(int i = 0; i < nargs; i++)
if(has_mixed_summands(arg(e,i)))
return true;
return false;
}
return get_term_type(e) == LitMixed;
}
// split a rewrite chain into head and tail at last sum with no mixed sumands
ast get_right_movers(const ast &chain, const ast &rhs, ast &tail, ast &mid){
if(is_true(chain) || get_term_type(rhs) != LitMixed){
if(is_true(chain) || !has_mixed_summands(rhs)){
mid = rhs;
tail = mk_true();
return chain;
@ -1571,11 +1701,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res;
}
// split a rewrite chain into head and tail at first non-mixed term
// split a rewrite chain into head and tail at first sum with no mixed sumands
ast get_left_movers(const ast &chain, const ast &lhs, ast &tail, ast &mid){
if(is_true(chain)){
mid = lhs;
if(get_term_type(lhs) != LitMixed){
if(!has_mixed_summands(lhs)){
tail = mk_true();
return chain;
}
@ -1675,10 +1805,21 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
bool rewrites_from_to(const ast &chain, const ast &lhs, const ast &rhs){
if(is_true(chain))
return lhs == rhs;
ast last = chain_last(chain);
ast rest = chain_rest(chain);
ast mid = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last));
return rewrites_from_to(rest,lhs,mid);
}
struct bad_ineq_inference {};
ast chain_ineqs(opr comp_op, LitType t, const ast &chain, const ast &lhs, const ast &rhs){
if(is_true(chain)){
if(lhs != rhs)
throw "bad ineq inference";
throw bad_ineq_inference();
return make(Leq,make_int(rational(0)),make_int(rational(0)));
}
ast last = chain_last(chain);
@ -1689,7 +1830,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast diff;
if(comp_op == Leq) diff = make(Sub,rhs,mid);
else diff = make(Sub,mid,rhs);
ast foo = z3_simplify(make(Leq,make_int("0"),diff));
ast foo = make(Leq,make_int("0"),z3_simplify(diff));
if(is_true(cond))
cond = foo;
else {
@ -2541,11 +2682,18 @@ class iz3proof_itp_impl : public iz3proof_itp {
pf = make_refl(e); // proof that e = e
prover::range erng = pv->ast_scope(e);
#if 0
if(!(erng.lo > erng.hi) && pv->ranges_intersect(pv->ast_scope(e),rng)){
return e; // this term occurs in range, so it's O.K.
}
#endif
hash_map<ast,ast>::iterator it = localization_map.find(e);
if(it != localization_map.end() && is_bool_type(get_type(e))
&& !pv->ranges_intersect(pv->ast_scope(it->second),rng))
it = localization_map.end(); // prevent quantifiers over booleans
if(it != localization_map.end()){
pf = localization_pf_map[e];
e = it->second;

33
src/interp/iz3translate.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -39,9 +39,7 @@ Revision History:
#include <set>
//using std::vector;
#ifndef WIN32
using namespace stl_ext;
#endif
@ -1592,6 +1590,27 @@ public:
return res;
}
/* This idiom takes ~P and Q=P, yielding ~Q. It uses a "rewrite"
(Q=false) = ~Q. We eliminate the rewrite by using symmetry,
congruence and modus ponens. */
if(dk == PR_MODUS_PONENS && pr(prem(proof,1)) == PR_REWRITE && pr(prem(proof,0)) == PR_TRANSITIVITY && pr(prem(prem(proof,0),1)) == PR_IFF_FALSE){
if(op(con) == Not && arg(con,0) == arg(conc(prem(proof,0)),0)){
Iproof::node ante1 = translate_main(prem(prem(proof,0),0),false);
Iproof::node ante2 = translate_main(prem(prem(prem(proof,0),1),0),false);
ast ante1_con = conc(prem(prem(proof,0),0));
ast eq0 = arg(ante1_con,0);
ast eq1 = arg(ante1_con,1);
ast symm_con = make(Iff,eq1,eq0);
Iproof::node ante1s = iproof->make_symmetry(symm_con,ante1_con,ante1);
ast cong_con = make(Iff,make(Not,eq1),make(Not,eq0));
Iproof::node ante1sc = iproof->make_congruence(symm_con,cong_con,ante1s);
res = iproof->make_mp(cong_con,ante2,ante1sc);
return res;
}
}
// translate all the premises
std::vector<Iproof::node> args(nprems);
for(unsigned i = 0; i < nprems; i++)
@ -1751,6 +1770,13 @@ public:
res = args[0];
break;
}
case PR_IFF_FALSE: { // turns ~p into p <-> false, noop for us
if(is_local(con))
res = args[0];
else
throw unsupported();
break;
}
case PR_COMMUTATIVITY: {
ast comm_equiv = make(op(con),arg(con,0),arg(con,0));
ast pf = iproof->make_reflexivity(comm_equiv);
@ -1758,6 +1784,7 @@ public:
break;
}
default:
pfgoto(proof);
assert(0 && "translate_main: unsupported proof rule");
throw unsupported();
}

67
src/interp/iz3translate_direct.cpp
View file

@ -20,7 +20,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -42,11 +42,7 @@ Revision History:
#include <set>
//using std::vector;
#ifndef WIN32
using namespace stl_ext;
#endif
#ifndef WIN32
/* This can introduce an address dependency if the range type of hash_map has
a destructor. Since the code in this file is not used and only here for
@ -62,9 +58,6 @@ namespace stl_ext {
};
}
#endif
static int lemma_count = 0;
#if 0
static int nll_lemma_count = 0;
@ -96,38 +89,12 @@ namespace hash_space {
};
}
#ifdef WIN32
template <> inline
size_t stdext::hash_value<Z3_resolvent >(const Z3_resolvent& p)
{
std::hash<Z3_resolvent> h;
return h(p);
}
namespace std {
template <>
class less<Z3_resolvent > {
public:
bool operator()(const Z3_resolvent &x, const Z3_resolvent &y) const {
size_t ixproof = (size_t) x.proof.raw();
size_t iyproof = (size_t) y.proof.raw();
if(ixproof < iyproof) return true;
if(ixproof > iyproof) return false;
return x.pivot < y.pivot;
}
};
}
#else
bool operator==(const Z3_resolvent &x, const Z3_resolvent &y) {
return x.proof == y.proof && x.pivot == y.pivot;
}
#endif
typedef std::vector<Z3_resolvent *> ResolventAppSet;
@ -151,36 +118,6 @@ namespace hash_space {
};
}
#ifdef WIN32
template <> inline
size_t stdext::hash_value<non_local_lits >(const non_local_lits& p)
{
std::hash<non_local_lits> h;
return h(p);
}
namespace std {
template <>
class less<non_local_lits > {
public:
bool operator()(const non_local_lits &x, const non_local_lits &y) const {
ResolventAppSet::const_iterator itx = x.proofs.begin();
ResolventAppSet::const_iterator ity = y.proofs.begin();
while(true){
if(ity == y.proofs.end()) return false;
if(itx == x.proofs.end()) return true;
size_t xi = (size_t) *itx;
size_t yi = (size_t) *ity;
if(xi < yi) return true;
if(xi > yi) return false;
++itx; ++ity;
}
}
};
}
#else
bool operator==(const non_local_lits &x, const non_local_lits &y) {
ResolventAppSet::const_iterator itx = x.proofs.begin();
@ -194,8 +131,6 @@ bool operator==(const non_local_lits &x, const non_local_lits &y) {
}
#endif
/* This translator goes directly from Z3 proofs to interpolatable
proofs without an intermediate representation as an iz3proof. */

2
src/muz/base/fixedpoint_params.pyg
View file

@ -74,6 +74,8 @@ def_module_params('fixedpoint',
('stratified_inlining', BOOL, False, 'DUALITY: Use stratified inlining'),
('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'),
('profile', BOOL, False, 'DUALITY: profile run time'),
('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'),
('batch_expand', BOOL, False, 'DUALITY: use batch expansion'),
('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
))

4
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -1465,6 +1465,10 @@ namespace datalog {
if (m_rules.get_num_rules() == 0) {
return l_false;
}
if (m_rules.get_predicate_rules(m_query_pred).empty()) {
return l_false;
}
if (is_linear()) {
if (m_ctx.get_engine() == QBMC_ENGINE) {

70
src/muz/duality/duality_dl_interface.cpp
View file

@ -64,20 +64,22 @@ namespace Duality {
std::vector<expr> clauses;
std::vector<std::vector<RPFP::label_struct> > clause_labels;
hash_map<RPFP::Edge *,int> map; // edges to clauses
Solver *old_rs;
Solver::Counterexample cex;
duality_data(ast_manager &_m) : ctx(_m,config(params_ref())) {
ls = 0;
rpfp = 0;
status = StatusNull;
old_rs = 0;
}
~duality_data(){
if(old_rs)
dealloc(old_rs);
if(rpfp)
dealloc(rpfp);
if(ls)
dealloc(ls);
if(cex.tree)
delete cex.tree;
}
};
@ -132,15 +134,18 @@ lbool dl_interface::query(::expr * query) {
m_ctx.ensure_opened();
// if there is old data, get the cex and dispose (later)
Solver::Counterexample old_cex;
duality_data *old_data = _d;
if(old_data)
old_cex = old_data->cex;
Solver *old_rs = 0;
if(old_data){
old_rs = old_data->old_rs;
old_rs->GetCounterexample().swap(old_data->cex);
}
scoped_proof generate_proofs_please(m_ctx.get_manager());
// make a new problem and solver
_d = alloc(duality_data,m_ctx.get_manager());
_d->ctx.set("mbqi",m_ctx.get_params().mbqi());
_d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx);
_d->rpfp = alloc(RPFP,_d->ls);
@ -195,7 +200,8 @@ lbool dl_interface::query(::expr * query) {
Solver *rs = Solver::Create("duality", _d->rpfp);
rs->LearnFrom(old_cex); // new solver gets hints from old cex
if(old_rs)
rs->LearnFrom(old_rs); // new solver gets hints from old solver
// set its options
IF_VERBOSE(1, rs->SetOption("report","1"););
@ -204,6 +210,7 @@ lbool dl_interface::query(::expr * query) {
rs->SetOption("feasible_edges",m_ctx.get_params().feasible_edges() ? "1" : "0");
rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0");
rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0");
unsigned rb = m_ctx.get_params().recursion_bound();
if(rb != UINT_MAX){
std::ostringstream os; os << rb;
@ -229,15 +236,14 @@ lbool dl_interface::query(::expr * query) {
// save the result and counterexample if there is one
_d->status = ans ? StatusModel : StatusRefutation;
_d->cex = rs->GetCounterexample();
_d->cex.swap(rs->GetCounterexample()); // take ownership of cex
_d->old_rs = rs; // save this for later hints
if(old_data){
old_data->cex.tree = 0; // we own it now
dealloc(old_data);
dealloc(old_data); // this deallocates the old solver if there is one
}
dealloc(rs);
// dealloc(rs); this is now owned by data
// true means the RPFP problem is SAT, so the query is UNSAT
return ans ? l_false : l_true;
@ -265,18 +271,16 @@ void dl_interface::reset_statistics() {
static hash_set<func_decl> *local_func_decls;
static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexample &cex) {
static void print_proof(dl_interface *d, std::ostream& out, RPFP *tree, RPFP::Node *root) {
context &ctx = d->dd()->ctx;
RPFP::Node &node = *cex.root;
RPFP::Node &node = *root;
RPFP::Edge &edge = *node.Outgoing;
// first, prove the children (that are actually used)
for(unsigned i = 0; i < edge.Children.size(); i++){
if(!cex.tree->Empty(edge.Children[i])){
Solver::Counterexample foo = cex;
foo.root = edge.Children[i];
print_proof(d,out,foo);
if(!tree->Empty(edge.Children[i])){
print_proof(d,out,tree,edge.Children[i]);
}
}
@ -285,7 +289,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
out << "(step s!" << node.number;
out << " (" << node.Name.name();
for(unsigned i = 0; i < edge.F.IndParams.size(); i++)
out << " " << cex.tree->Eval(&edge,edge.F.IndParams[i]);
out << " " << tree->Eval(&edge,edge.F.IndParams[i]);
out << ")\n";
// print the rule number
@ -307,8 +311,8 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
sort the_sort = t.get_quantifier_bound_sort(j);
symbol name = t.get_quantifier_bound_name(j);
expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
out << " (= " << skolem << " " << cex.tree->Eval(&edge,skolem) << ")\n";
expr local_skolem = cex.tree->Localize(&edge,skolem);
out << " (= " << skolem << " " << tree->Eval(&edge,skolem) << ")\n";
expr local_skolem = tree->Localize(&edge,skolem);
(*local_func_decls).insert(local_skolem.decl());
}
}
@ -316,7 +320,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
out << " (labels";
std::vector<symbol> labels;
cex.tree->GetLabels(&edge,labels);
tree->GetLabels(&edge,labels);
for(unsigned j = 0; j < labels.size(); j++){
out << " " << labels[j];
}
@ -328,7 +332,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
out << " (ref ";
for(unsigned i = 0; i < edge.Children.size(); i++){
if(!cex.tree->Empty(edge.Children[i]))
if(!tree->Empty(edge.Children[i]))
out << " s!" << edge.Children[i]->number;
else
out << " true";
@ -353,11 +357,11 @@ void dl_interface::display_certificate_non_const(std::ostream& out) {
// negation of the query is the last clause -- prove it
hash_set<func_decl> locals;
local_func_decls = &locals;
print_proof(this,out,_d->cex);
print_proof(this,out,_d->cex.get_tree(),_d->cex.get_root());
out << ")\n";
out << "(model \n\"";
::model mod(m_ctx.get_manager());
model orig_model = _d->cex.tree->dualModel;
model orig_model = _d->cex.get_tree()->dualModel;
for(unsigned i = 0; i < orig_model.num_consts(); i++){
func_decl cnst = orig_model.get_const_decl(i);
if(locals.find(cnst) == locals.end()){
@ -428,10 +432,10 @@ model_ref dl_interface::get_model() {
return md;
}
static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) {
static proof_ref extract_proof(dl_interface *d, RPFP *tree, RPFP::Node *root) {
context &ctx = d->dd()->ctx;
ast_manager &mgr = ctx.m();
RPFP::Node &node = *cex.root;
RPFP::Node &node = *root;
RPFP::Edge &edge = *node.Outgoing;
RPFP::Edge *orig_edge = edge.map;
@ -453,21 +457,19 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) {
sort the_sort = t.get_quantifier_bound_sort(j);
symbol name = t.get_quantifier_bound_name(j);
expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
expr val = cex.tree->Eval(&edge,skolem);
expr val = tree->Eval(&edge,skolem);
expr_ref thing(ctx.uncook(val),mgr);
substs[0].push_back(thing);
expr local_skolem = cex.tree->Localize(&edge,skolem);
expr local_skolem = tree->Localize(&edge,skolem);
(*local_func_decls).insert(local_skolem.decl());
}
}
svector<std::pair<unsigned, unsigned> > pos;
for(unsigned i = 0; i < edge.Children.size(); i++){
if(!cex.tree->Empty(edge.Children[i])){
if(!tree->Empty(edge.Children[i])){
pos.push_back(std::pair<unsigned,unsigned>(i+1,0));
Solver::Counterexample foo = cex;
foo.root = edge.Children[i];
proof_ref prem = extract_proof(d,foo);
proof_ref prem = extract_proof(d,tree,edge.Children[i]);
prems.push_back(prem);
substs.push_back(expr_ref_vector(mgr));
}
@ -476,7 +478,7 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) {
func_decl f = node.Name;
std::vector<expr> args;
for(unsigned i = 0; i < edge.F.IndParams.size(); i++)
args.push_back(cex.tree->Eval(&edge,edge.F.IndParams[i]));
args.push_back(tree->Eval(&edge,edge.F.IndParams[i]));
expr conc = f(args);
@ -493,7 +495,7 @@ proof_ref dl_interface::get_proof() {
if(_d->status == StatusRefutation){
hash_set<func_decl> locals;
local_func_decls = &locals;
return extract_proof(this,_d->cex);
return extract_proof(this,_d->cex.get_tree(),_d->cex.get_root());
}
else
return proof_ref(m_ctx.get_manager());

8
src/parsers/smt2/smt2parser.cpp
View file

@ -850,6 +850,13 @@ namespace smt2 {
for (unsigned i = 0; i < sz; i++) {
pdatatype_decl * d = new_dt_decls[i];
SASSERT(d != 0);
symbol duplicated;
if (d->has_duplicate_accessors(duplicated)) {
std::string err_msg = "invalid datatype declaration, repeated accessor identifier '";
err_msg += duplicated.str();
err_msg += "'";
throw parser_exception(err_msg, line, pos);
}
m_ctx.insert(d);
if (d->get_num_params() == 0) {
// if datatype is not parametric... then force instantiation to register accessor, recognizers and constructors...
@ -2070,6 +2077,7 @@ namespace smt2 {
void parse_option_value() {
switch (curr()) {
case scanner::BV_TOKEN:
case scanner::INT_TOKEN:
case scanner::FLOAT_TOKEN:
m_curr_cmd->set_next_arg(m_ctx, m_scanner.get_number());

2
src/shell/main.cpp
View file

@ -87,7 +87,7 @@ void display_usage() {
std::cout << "\nResources:\n";
// timeout and memout are now available on Linux and OSX too.
std::cout << " -T:timeout set the timeout (in seconds).\n";
std::cout << " -t:timeout set the soft timeout (in seconds). It only kills the current query.\n";
std::cout << " -t:timeout set the soft timeout (in milli seconds). It only kills the current query.\n";
std::cout << " -memory:Megabytes set a limit for virtual memory consumption.\n";
//
std::cout << "\nOutput:\n";

3
src/smt/params/theory_arith_params.h
View file

@ -27,8 +27,7 @@ enum arith_solver_id {
AS_DIFF_LOGIC,
AS_ARITH,
AS_DENSE_DIFF_LOGIC,
AS_UTVPI,
AS_HORN
AS_UTVPI
};
enum bound_prop_mode {

2
src/smt/smt_quantifier.cpp
View file

@ -441,7 +441,7 @@ namespace smt {
virtual bool mbqi_enabled(quantifier *q) const {
if(!m_fparams->m_mbqi_id) return true;
const symbol &s = q->get_qid();
unsigned len = strlen(m_fparams->m_mbqi_id);
size_t len = strlen(m_fparams->m_mbqi_id);
if(s == symbol::null || s.is_numerical())
return len == 0;
return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0;

7
src/smt/smt_setup.cpp
View file

@ -22,7 +22,6 @@ Revision History:
#include"theory_arith.h"
#include"theory_dense_diff_logic.h"
#include"theory_diff_logic.h"
#include"theory_horn_ineq.h"
#include"theory_utvpi.h"
#include"theory_array.h"
#include"theory_array_full.h"
@ -725,12 +724,6 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_dense_mi, m_manager, m_params));
}
break;
case AS_HORN:
if (m_params.m_arith_int_only)
m_context.register_plugin(alloc(smt::theory_ihi, m_manager));
else
m_context.register_plugin(alloc(smt::theory_rhi, m_manager));
break;
case AS_UTVPI:
if (m_params.m_arith_int_only)
m_context.register_plugin(alloc(smt::theory_iutvpi, m_manager));

107
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -139,22 +139,32 @@ protected:
SASSERT(g.is_well_sorted());
}
struct expr_pos {
unsigned m_parent;
unsigned m_self;
unsigned m_idx;
expr* m_expr;
expr_pos(unsigned p, unsigned s, unsigned i, expr* e):
m_parent(p), m_self(s), m_idx(i), m_expr(e)
{}
expr_pos():
m_parent(0), m_self(0), m_idx(0), m_expr(0)
{}
};
void reduce(expr_ref& result){
SASSERT(m.is_bool(result));
ptr_vector<expr> todo;
ptr_vector<expr> names;
svector<bool> is_checked;
svector<unsigned> parent_ids, self_ids;
svector<expr_pos> todo;
expr_ref_vector fresh_vars(m), trail(m);
expr_ref res(m), tmp(m);
obj_map<expr,std::pair<unsigned, expr*> > cache;
unsigned id = 1;
obj_map<expr, expr_pos> cache;
unsigned id = 1, child_id = 0;
expr_ref n2(m), fml(m);
unsigned path_id = 0, self_pos = 0;
unsigned parent_pos = 0, self_pos = 0, self_idx = 0;
app * a;
unsigned sz;
std::pair<unsigned,expr*> path_r;
ptr_vector<expr> found;
expr_pos path_r;
expr_ref_vector args(m);
expr_ref n = mk_fresh(id, m.mk_bool_sort());
trail.push_back(n);
@ -163,26 +173,25 @@ protected:
tmp = m.mk_not(m.mk_iff(fml, n));
m_solver.assert_expr(tmp);
todo.push_back(fml);
todo.push_back(expr_pos(0,0,0,fml));
names.push_back(n);
is_checked.push_back(false);
parent_ids.push_back(0);
self_ids.push_back(0);
m_solver.push();
while (!todo.empty() && !m_cancel) {
expr_ref res(m);
args.reset();
expr* e = todo.back();
unsigned pos = parent_ids.back();
expr* e = todo.back().m_expr;
self_pos = todo.back().m_self;
parent_pos = todo.back().m_parent;
self_idx = todo.back().m_idx;
n = names.back();
bool checked = is_checked.back();
if (cache.contains(e)) {
goto done;
}
if (m.is_bool(e) && !checked && simplify_bool(n, res)) {
TRACE("ctx_solver_simplify_tactic", tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);
if (m.is_bool(e) && simplify_bool(n, res)) {
TRACE("ctx_solver_simplify_tactic",
tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);
goto done;
}
if (!is_app(e)) {
@ -191,49 +200,31 @@ protected:
}
a = to_app(e);
if (!is_checked.back()) {
self_ids.back() = ++path_id;
is_checked.back() = true;
}
self_pos = self_ids.back();
sz = a->get_num_args();
n2 = 0;
found.reset(); // arguments already simplified.
for (unsigned i = 0; i < sz; ++i) {
expr* arg = a->get_arg(i);
if (cache.find(arg, path_r) && !found.contains(arg)) {
if (cache.find(arg, path_r)) {
//
// This is a single traversal version of the context
// simplifier. It simplifies only the first occurrence of
// a sub-term with respect to the context.
//
found.push_back(arg);
if (path_r.first == self_pos) {
TRACE("ctx_solver_simplify_tactic", tout << "cached " << mk_pp(arg, m) << " |-> " << mk_pp(path_r.second, m) << "\n";);
args.push_back(path_r.second);
}
else if (m.is_bool(arg)) {
res = local_simplify(a, n, id, i);
TRACE("ctx_solver_simplify_tactic",
tout << "Already cached: " << path_r.first << " " << mk_pp(arg, m) << " |-> " << mk_pp(res, m) << "\n";);
args.push_back(res);
if (path_r.m_parent == self_pos && path_r.m_idx == i) {
args.push_back(path_r.m_expr);
}
else {
args.push_back(arg);
}
}
else if (!n2 && !found.contains(arg)) {
else if (!n2) {
n2 = mk_fresh(id, m.get_sort(arg));
trail.push_back(n2);
todo.push_back(arg);
parent_ids.push_back(self_pos);
self_ids.push_back(0);
todo.push_back(expr_pos(self_pos, child_id++, i, arg));
names.push_back(n2);
args.push_back(n2);
is_checked.push_back(false);
}
else {
args.push_back(arg);
@ -251,22 +242,16 @@ protected:
done:
if (res) {
cache.insert(e, std::make_pair(pos, res));
cache.insert(e, expr_pos(parent_pos, self_pos, self_idx, res));
}
TRACE("ctx_solver_simplify_tactic",
tout << mk_pp(e, m) << " checked: " << checked << " cached: " << mk_pp(res?res.get():e, m) << "\n";);
todo.pop_back();
parent_ids.pop_back();
self_ids.pop_back();
names.pop_back();
is_checked.pop_back();
m_solver.pop(1);
}
if (!m_cancel) {
VERIFY(cache.find(fml, path_r));
result = path_r.second;
result = path_r.m_expr;
}
}
@ -307,32 +292,6 @@ protected:
return expr_ref(m.mk_app(fn, m_arith.mk_numeral(rational(id++), true)), m);
}
expr_ref local_simplify(app* a, expr* n, unsigned& id, unsigned index) {
SASSERT(index < a->get_num_args());
SASSERT(m.is_bool(a->get_arg(index)));
expr_ref n2(m), result(m), tmp(m);
n2 = mk_fresh(id, m.get_sort(a->get_arg(index)));
ptr_buffer<expr> args;
for (unsigned i = 0; i < a->get_num_args(); ++i) {
if (i == index) {
args.push_back(n2);
}
else {
args.push_back(a->get_arg(i));
}
}
m_mk_app(a->get_decl(), args.size(), args.c_ptr(), result);
m_solver.push();
tmp = m.mk_eq(result, n);
m_solver.assert_expr(tmp);
if (!simplify_bool(n2, result)) {
result = a->get_arg(index);
}
m_solver.pop(1);
return result;
}
};
tactic * mk_ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p) {

236
src/smt/theory_horn_ineq.cpp
View file

@ -1,236 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
theory_horn_ineq.h
Author:
Nikolaj Bjorner (nbjorner) 2013-04-18
Revision History:
The implementaton is derived from theory_diff_logic.
--*/
#include "theory_horn_ineq.h"
#include "theory_horn_ineq_def.h"
namespace smt {
template class theory_horn_ineq<ihi_ext>;
template class theory_horn_ineq<rhi_ext>;
// similar to test_diff_logic:
horn_ineq_tester::horn_ineq_tester(ast_manager& m): m(m), a(m) {}
bool horn_ineq_tester::operator()(expr* e) {
m_todo.reset();
m_pols.reset();
pos_mark.reset();
neg_mark.reset();
m_todo.push_back(e);
m_pols.push_back(l_true);
while (!m_todo.empty()) {
expr* e = m_todo.back();
lbool p = m_pols.back();
m_todo.pop_back();
m_pols.pop_back();
switch (p) {
case l_true:
if (pos_mark.is_marked(e)) {
continue;
}
pos_mark.mark(e, true);
break;
case l_false:
if (neg_mark.is_marked(e)) {
continue;
}
neg_mark.mark(e, true);
break;
case l_undef:
if (pos_mark.is_marked(e) && neg_mark.is_marked(e)) {
continue;
}
pos_mark.mark(e, true);
neg_mark.mark(e, true);
break;
}
if (!test_expr(p, e)) {
return false;
}
}
return true;
}
vector<std::pair<expr*,rational> > const& horn_ineq_tester::get_linearization() const {
return m_terms;
}
bool horn_ineq_tester::test_expr(lbool p, expr* e) {
expr* e1, *e2, *e3;
if (is_var(e)) {
return true;
}
if (!is_app(e)) {
return false;
}
app* ap = to_app(e);
if (m.is_and(ap) || m.is_or(ap)) {
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
m_todo.push_back(ap->get_arg(i));
m_pols.push_back(p);
}
}
else if (m.is_not(e, e1)) {
m_todo.push_back(e);
m_pols.push_back(~p);
}
else if (m.is_ite(e, e1, e2, e3)) {
m_todo.push_back(e1);
m_pols.push_back(l_undef);
m_todo.push_back(e2);
m_pols.push_back(p);
m_todo.push_back(e3);
m_pols.push_back(p);
}
else if (m.is_iff(e, e1, e2)) {
m_todo.push_back(e1);
m_pols.push_back(l_undef);
m_todo.push_back(e2);
m_pols.push_back(l_undef);
m_todo.push_back(e2);
}
else if (m.is_implies(e, e1, e2)) {
m_todo.push_back(e1);
m_pols.push_back(~p);
m_todo.push_back(e2);
m_pols.push_back(p);
}
else if (m.is_eq(e, e1, e2)) {
return linearize(e1, e2) == diff;
}
else if (m.is_true(e) || m.is_false(e)) {
// no-op
}
else if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1) ||
a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) {
if (p == l_false) {
std::swap(e2, e1);
}
classify_t cl = linearize(e1, e2);
switch(p) {
case l_undef:
return cl == diff;
case l_true:
case l_false:
return cl == horn || cl == diff;
}
}
else if (!is_uninterp_const(e)) {
return false;
}
return true;
}
bool horn_ineq_tester::operator()(unsigned num_fmls, expr* const* fmls) {
for (unsigned i = 0; i < num_fmls; ++i) {
if (!(*this)(fmls[i])) {
return false;
}
}
return true;
}
horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e) {
m_terms.reset();
m_terms.push_back(std::make_pair(e, rational(1)));
return linearize();
}
horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e1, expr* e2) {
m_terms.reset();
m_terms.push_back(std::make_pair(e1, rational(1)));
m_terms.push_back(std::make_pair(e2, rational(-1)));
return linearize();
}
horn_ineq_tester::classify_t horn_ineq_tester::linearize() {
m_weight.reset();
m_coeff_map.reset();
while (!m_terms.empty()) {
expr* e1, *e2;
rational num;
rational mul = m_terms.back().second;
expr* e = m_terms.back().first;
m_terms.pop_back();
if (a.is_add(e)) {
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
m_terms.push_back(std::make_pair(to_app(e)->get_arg(i), mul));
}
}
else if (a.is_mul(e, e1, e2) && a.is_numeral(e1, num)) {
m_terms.push_back(std::make_pair(e2, mul*num));
}
else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) {
m_terms.push_back(std::make_pair(e2, mul*num));
}
else if (a.is_sub(e, e1, e2)) {
m_terms.push_back(std::make_pair(e1, mul));
m_terms.push_back(std::make_pair(e2, -mul));
}
else if (a.is_uminus(e, e1)) {
m_terms.push_back(std::make_pair(e1, -mul));
}
else if (a.is_numeral(e, num)) {
m_weight += num*mul;
}
else if (a.is_to_real(e, e1)) {
m_terms.push_back(std::make_pair(e1, mul));
}
else if (!is_uninterp_const(e)) {
return non_horn;
}
else {
m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul;
}
}
unsigned num_negative = 0;
unsigned num_positive = 0;
bool is_unit_pos = true, is_unit_neg = true;
obj_map<expr, rational>::iterator it = m_coeff_map.begin();
obj_map<expr, rational>::iterator end = m_coeff_map.end();
for (; it != end; ++it) {
rational r = it->m_value;
if (r.is_zero()) {
continue;
}
m_terms.push_back(std::make_pair(it->m_key, r));
if (r.is_pos()) {
is_unit_pos = is_unit_pos && r.is_one();
num_positive++;
}
else {
is_unit_neg = is_unit_neg && r.is_minus_one();
num_negative++;
}
}
if (num_negative <= 1 && is_unit_pos && is_unit_neg && num_positive <= 1) {
return diff;
}
if (num_positive <= 1 && is_unit_pos) {
return horn;
}
if (num_negative <= 1 && is_unit_neg) {
return co_horn;
}
return non_horn;
}
}

328
src/smt/theory_horn_ineq.h
View file

@ -1,328 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
theory_horn_ineq.h
Abstract:
A*x <= weight + D*x, coefficients to A and D are non-negative,
D is a diagonal matrix.
Coefficients to weight may have both signs.
Label variables by weight.
Select inequality that is not satisfied.
Set delta(LHS) := 0
Set delta(RHS(x)) := weight(x) - b
Propagate weight increment through inequalities.
Author:
Nikolaj Bjorner (nbjorner) 2013-04-18
Revision History:
The implementaton is derived from theory_diff_logic.
--*/
#ifndef _THEORY_HORN_INEQ_H_
#define _THEORY_HORN_INEQ_H_
#include"rational.h"
#include"inf_rational.h"
#include"inf_int_rational.h"
#include"inf_eps_rational.h"
#include"smt_theory.h"
#include"arith_decl_plugin.h"
#include"smt_justification.h"
#include"map.h"
#include"smt_params.h"
#include"arith_eq_adapter.h"
#include"smt_model_generator.h"
#include"numeral_factory.h"
#include"smt_clause.h"
namespace smt {
class horn_ineq_tester {
ast_manager& m;
arith_util a;
ptr_vector<expr> m_todo;
svector<lbool> m_pols;
ast_mark pos_mark, neg_mark;
obj_map<expr, rational> m_coeff_map;
rational m_weight;
vector<std::pair<expr*, rational> > m_terms;
public:
enum classify_t {
co_horn,
horn,
diff,
non_horn
};
horn_ineq_tester(ast_manager& m);
// test if formula is in the Horn inequality fragment:
bool operator()(expr* fml);
bool operator()(unsigned num_fmls, expr* const* fmls);
// linearize inequality/equality
classify_t linearize(expr* e);
classify_t linearize(expr* e1, expr* e2);
// retrieve linearization
vector<std::pair<expr*,rational> > const& get_linearization() const;
rational const& get_weight() const { return m_weight; }
private:
bool test_expr(lbool p, expr* e);
classify_t linearize();
};
template<typename Ext>
class theory_horn_ineq : public theory, private Ext {
typedef typename Ext::numeral numeral;
typedef typename Ext::inf_numeral inf_numeral;
typedef literal explanation;
typedef theory_var th_var;
typedef svector<th_var> th_var_vector;
typedef unsigned clause_id;
typedef vector<std::pair<th_var, rational> > coeffs;
class clause;
class graph;
class assignment_trail;
class parent_trail;
class atom {
protected:
bool_var m_bvar;
bool m_true;
int m_pos;
int m_neg;
public:
atom(bool_var bv, int pos, int neg) :
m_bvar(bv), m_true(false),
m_pos(pos), m_neg(neg) {}
~atom() {}
bool_var get_bool_var() const { return m_bvar; }
bool is_true() const { return m_true; }
void assign_eh(bool is_true) { m_true = is_true; }
int get_asserted_edge() const { return this->m_true?m_pos:m_neg; }
int get_pos() const { return m_pos; }
int get_neg() const { return m_neg; }
std::ostream& display(theory_horn_ineq const& th, std::ostream& out) const;
};
typedef svector<atom> atoms;
struct scope {
unsigned m_atoms_lim;
unsigned m_asserted_atoms_lim;
unsigned m_asserted_qhead_old;
};
struct stats {
unsigned m_num_conflicts;
unsigned m_num_assertions;
unsigned m_num_core2th_eqs;
unsigned m_num_core2th_diseqs;
void reset() {
memset(this, 0, sizeof(*this));
}
stats() {
reset();
}
};
stats m_stats;
smt_params m_params;
arith_util a;
arith_eq_adapter m_arith_eq_adapter;
th_var m_zero_int; // cache the variable representing the zero variable.
th_var m_zero_real; // cache the variable representing the zero variable.
graph* m_graph;
atoms m_atoms;
unsigned_vector m_asserted_atoms; // set of asserted atoms
unsigned m_asserted_qhead;
u_map<unsigned> m_bool_var2atom;
svector<scope> m_scopes;
double m_agility;
bool m_lia;
bool m_lra;
bool m_non_horn_ineq_exprs;
horn_ineq_tester m_test;
arith_factory * m_factory;
rational m_delta;
rational m_lambda;
// Set a conflict due to a negative cycle.
void set_neg_cycle_conflict();
// Create a new theory variable.
virtual th_var mk_var(enode* n);
virtual th_var mk_var(expr* n);
void compute_delta();
void found_non_horn_ineq_expr(expr * n);
bool is_interpreted(app* n) const {
return n->get_family_id() == get_family_id();
}
public:
theory_horn_ineq(ast_manager& m);
virtual ~theory_horn_ineq();
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_horn_ineq, get_manager()); }
virtual char const * get_name() const { return "horn-inequality-logic"; }
/**
\brief See comment in theory::mk_eq_atom
*/
virtual app * mk_eq_atom(expr * lhs, expr * rhs) { return a.mk_eq(lhs, rhs); }
virtual void init(context * ctx);
virtual bool internalize_atom(app * atom, bool gate_ctx);
virtual bool internalize_term(app * term);
virtual void internalize_eq_eh(app * atom, bool_var v);
virtual void assign_eh(bool_var v, bool is_true);
virtual void new_eq_eh(th_var v1, th_var v2) {
m_arith_eq_adapter.new_eq_eh(v1, v2);
}
virtual bool use_diseqs() const { return true; }
virtual void new_diseq_eh(th_var v1, th_var v2) {
m_arith_eq_adapter.new_diseq_eh(v1, v2);
}
virtual void push_scope_eh();
virtual void pop_scope_eh(unsigned num_scopes);
virtual void restart_eh() {
m_arith_eq_adapter.restart_eh();
}
virtual void relevant_eh(app* e) {}
virtual void init_search_eh() {
m_arith_eq_adapter.init_search_eh();
}
virtual final_check_status final_check_eh();
virtual bool is_shared(th_var v) const {
return false;
}
virtual bool can_propagate() {
SASSERT(m_asserted_qhead <= m_asserted_atoms.size());
return m_asserted_qhead != m_asserted_atoms.size();
}
virtual void propagate();
virtual justification * why_is_diseq(th_var v1, th_var v2) {
UNREACHABLE();
return 0;
}
virtual void reset_eh();
virtual void init_model(model_generator & m);
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
virtual bool validate_eq_in_model(th_var v1, th_var v2, bool is_true) const {
return true;
}
virtual void display(std::ostream & out) const;
virtual void collect_statistics(::statistics & st) const;
private:
virtual void new_eq_eh(th_var v1, th_var v2, justification& j) {
m_stats.m_num_core2th_eqs++;
new_eq_or_diseq(true, v1, v2, j);
}
virtual void new_diseq_eh(th_var v1, th_var v2, justification& j) {
m_stats.m_num_core2th_diseqs++;
new_eq_or_diseq(false, v1, v2, j);
}
void negate(coeffs& coeffs, rational& weight);
numeral mk_weight(bool is_real, bool is_strict, rational const& w) const;
void mk_coeffs(vector<std::pair<expr*,rational> >const& terms, coeffs& coeffs, rational& w);
void del_atoms(unsigned old_size);
void propagate_core();
bool propagate_atom(atom const& a);
th_var mk_term(app* n);
th_var mk_num(app* n, rational const& r);
bool is_consistent() const;
th_var expand(bool pos, th_var v, rational & k);
void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
th_var get_zero(sort* s) const { return a.is_int(s)?m_zero_int:m_zero_real; }
th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); }
void inc_conflicts();
};
struct rhi_ext {
typedef inf_rational inf_numeral;
typedef inf_eps_rational<inf_rational> numeral;
numeral m_epsilon;
numeral m_minus_infty;
rhi_ext() : m_epsilon(inf_rational(rational(), true)), m_minus_infty(rational(-1),inf_rational()) {}
};
struct ihi_ext {
typedef rational inf_numeral;
typedef inf_eps_rational<rational> numeral;
numeral m_epsilon;
numeral m_minus_infty;
ihi_ext() : m_epsilon(rational(1)), m_minus_infty(rational(-1),rational(0)) {}
};
typedef theory_horn_ineq<rhi_ext> theory_rhi;
typedef theory_horn_ineq<ihi_ext> theory_ihi;
};
#endif /* _THEORY_HORN_INEQ_H_ */

1166
src/smt/theory_horn_ineq_def.h
View file

File diff suppressed because it is too large Load diff

58
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -25,6 +25,7 @@ Notes:
#include"bv_decl_plugin.h"
#include"expr_replacer.h"
#include"extension_model_converter.h"
#include"filter_model_converter.h"
#include"ast_smt2_pp.h"
class bv_size_reduction_tactic : public tactic {
@ -60,6 +61,7 @@ struct bv_size_reduction_tactic::imp {
obj_map<app, numeral> m_unsigned_lowers;
obj_map<app, numeral> m_unsigned_uppers;
ref<bv_size_reduction_mc> m_mc;
ref<filter_model_converter> m_fmc;
scoped_ptr<expr_replacer> m_replacer;
bool m_produce_models;
volatile bool m_cancel;
@ -123,19 +125,39 @@ struct bv_size_reduction_tactic::imp {
}
if (m_util.is_bv_sle(f, lhs, rhs)) {
bv_sz = m_util.get_bv_size(lhs);
if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
// v <= k
if (negated) update_signed_lower(to_app(lhs), val+numeral(1));
val = m_util.norm(val, bv_sz, true);
if (negated) {
val += numeral(1);
if (m_util.norm(val, bv_sz, true) != val) {
// bound is infeasible.
}
else {
update_signed_lower(to_app(lhs), val);
}
}
else update_signed_upper(to_app(lhs), val);
}
else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) {
TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
// k <= v
if (negated) update_signed_upper(to_app(rhs), val-numeral(1));
val = m_util.norm(val, bv_sz, true);
if (negated) {
val -= numeral(1);
if (m_util.norm(val, bv_sz, true) != val) {
// bound is infeasible.
}
else {
update_signed_upper(to_app(lhs), val);
}
}
else update_signed_lower(to_app(rhs), val);
}
}
#if 0
else if (m_util.is_bv_ule(f, lhs, rhs)) {
if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
@ -196,6 +218,7 @@ struct bv_size_reduction_tactic::imp {
numeral u = m_util.norm(entry->get_data().m_value, bv_sz, true);
TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
expr * new_def = 0;
app * new_const = 0;
if (l > u) {
g.assert_expr(m.mk_false());
return;
@ -208,15 +231,19 @@ struct bv_size_reduction_tactic::imp {
if (l.is_neg()) {
unsigned i_nb = (u - l).get_num_bits();
unsigned v_nb = m_util.get_bv_size(v);
if (i_nb < v_nb)
new_def = m_util.mk_sign_extend(v_nb - i_nb, m.mk_fresh_const(0, m_util.mk_sort(i_nb)));
if (i_nb < v_nb) {
new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
}
}
else {
// 0 <= l <= v <= u
unsigned u_nb = u.get_num_bits();
unsigned v_nb = m_util.get_bv_size(v);
if (u_nb < v_nb)
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb)));
if (u_nb < v_nb) {
new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
}
}
}
@ -226,6 +253,10 @@ struct bv_size_reduction_tactic::imp {
if (!m_mc)
m_mc = alloc(bv_size_reduction_mc, m);
m_mc->insert(v->get_decl(), new_def);
if (!m_fmc && new_const)
m_fmc = alloc(filter_model_converter, m);
if (new_const)
m_fmc->insert(new_const->get_decl());
}
num_reduced++;
}
@ -264,6 +295,7 @@ struct bv_size_reduction_tactic::imp {
TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
expr * new_def = 0;
app * new_const = 0;
if (l > u) {
g.assert_expr(m.mk_false());
return;
@ -275,8 +307,10 @@ struct bv_size_reduction_tactic::imp {
// 0 <= l <= v <= u
unsigned u_nb = u.get_num_bits();
unsigned v_nb = m_util.get_bv_size(v);
if (u_nb < v_nb)
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb)));
if (u_nb < v_nb) {
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
}
}
if (new_def) {
@ -285,6 +319,10 @@ struct bv_size_reduction_tactic::imp {
if (!m_mc)
m_mc = alloc(bv_size_reduction_mc, m);
m_mc->insert(v->get_decl(), new_def);
if (!m_fmc && new_const)
m_fmc = alloc(filter_model_converter, m);
if (new_const)
m_fmc->insert(new_const->get_decl());
}
num_reduced++;
TRACE("bv_size_reduction", tout << "New definition = " << mk_ismt2_pp(new_def, m) << "\n";);
@ -309,7 +347,11 @@ struct bv_size_reduction_tactic::imp {
g.update(i, new_f);
}
mc = m_mc.get();
if (m_fmc) {
mc = concat(m_fmc.get(), mc.get());
}
m_mc = 0;
m_fmc = 0;
}
report_tactic_progress(":bv-reduced", num_reduced);
TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout););

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

@ -874,6 +874,17 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4));
expr_ref res_sig_lz(m);
mk_leading_zeros(res_sig, sbits + 4, res_sig_lz);
dbg_decouple("fpa2bv_div_res_sig_lz", res_sig_lz);
expr_ref res_sig_shift_amount(m);
res_sig_shift_amount = m_bv_util.mk_bv_sub(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4));
dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount);
expr_ref shift_cond(m);
shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4));
m_simp.mk_ite(shift_cond, res_sig, m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount), res_sig);
m_simp.mk_ite(shift_cond, res_exp, m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits+1, 0, res_sig_shift_amount)), res_exp);
round(f->get_range(), rm, res_sgn, res_sig, res_exp, v8);
// And finally, we tie them together.

38
src/util/rational.h
View file

@ -331,22 +331,13 @@ public:
return target;
}
friend inline rational gcd(rational const & r1, rational const & r2) {
rational result;
m().gcd(r1.m_val, r2.m_val, result.m_val);
return result;
}
friend inline rational gcd(rational const & r1, rational const & r2);
//
// extended Euclid:
// r1*a + r2*b = gcd
//
friend inline rational gcd(rational const & r1, rational const & r2, rational & a, rational & b) {
rational result;
m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val);
return result;
}
friend inline rational gcd(rational const & r1, rational const & r2, rational & a, rational & b);
friend inline rational lcm(rational const & r1, rational const & r2) {
rational result;
@ -378,11 +369,7 @@ public:
return result;
}
friend inline rational abs(rational const & r) {
rational result(r);
m().abs(result.m_val);
return result;
}
friend inline rational abs(rational const & r);
rational to_rational() const { return *this; }
@ -446,5 +433,24 @@ inline rational power(rational const & r, unsigned p) {
return r.expt(p);
}
inline rational abs(rational const & r) {
rational result(r);
rational::m().abs(result.m_val);
return result;
}
inline rational gcd(rational const & r1, rational const & r2) {
rational result;
rational::m().gcd(r1.m_val, r2.m_val, result.m_val);
return result;
}
inline rational gcd(rational const & r1, rational const & r2, rational & a, rational & b) {
rational result;
rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val);
return result;
}
#endif /* _RATIONAL_H_ */