diff --git a/.gitattributes b/.gitattributes
index b86ed5df79b..8df0f39d948 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -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
diff --git a/.gitignore b/.gitignore
index 2b3149d04d8..75a87c37b18 100644
--- a/.gitignore
+++ b/.gitignore
@@ -56,6 +56,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
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 301282870a0..ce1014ebeec 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -43,17 +43,18 @@ def init_project_def():
# Simplifier module will be deleted in the future.
# It has been replaced with rewriter module.
add_lib('simplifier', ['rewriter'], 'ast/simplifier')
+ add_lib('fpa', ['ast', 'util', 'simplifier'], 'ast/fpa')
add_lib('macros', ['simplifier'], 'ast/macros')
add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern')
add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster')
add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params')
add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model')
add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
- 'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util'])
+ 'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa'])
add_lib('user_plugin', ['smt'], 'smt/user_plugin')
add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
add_lib('fuzzing', ['ast'], 'test/fuzzing')
- add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
+ add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
add_lib('smt_tactic', ['smt'], 'smt/tactic')
add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
add_lib('qe', ['smt','sat'], 'qe')
@@ -69,7 +70,7 @@ def init_project_def():
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf'], 'muz/fp')
add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics')
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
- add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
+ add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
add_lib('smtparser', ['portfolio'], 'parsers/smt')
add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic'], 'opt')
API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h']
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 88349261434..89cabe87e05 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -54,6 +54,7 @@ def getenv(name, default):
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 @@ def check_eol():
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")
@@ -1181,6 +1187,8 @@ def mk_makefile(self, out):
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)
diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py
index a52c8af4306..3a95fb730f0 100644
--- a/scripts/mk_win_dist.py
+++ b/scripts/mk_win_dist.py
@@ -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:
diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp
index 07d4fda18bb..0109d6e6b2b 100644
--- a/src/api/api_bv.cpp
+++ b/src/api/api_bv.cpp
@@ -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 {
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 847115951d7..fcbba1ff6c7 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -302,11 +302,11 @@ public ListSort MkListSort(string name, Sort elemSort)
}
///
- /// Create a new finite domain sort.
- /// The name used to identify the sort
- /// The size of the sort
- /// The result is a sort
+ /// Create a new finite domain sort.
+ /// The result is a sort
///
+ /// The name used to identify the sort
+ /// The size of the sort
public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
{
Contract.Requires(name != null);
@@ -317,13 +317,13 @@ public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
}
///
- /// Create a new finite domain sort.
- /// The name used to identify the sort
- /// The size of the sort
- /// The result is a sort
- /// Elements of the sort are created using ,
- /// and the elements range from 0 to size-1.
+ /// Create a new finite domain sort.
+ /// The result is a sort
+ /// Elements of the sort are created using ,
+ /// and the elements range from 0 to size-1.
///
+ /// The name used to identify the sort
+ /// The size of the sort
public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
{
Contract.Ensures(Contract.Result() != null);
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index 49b46edebab..c8fdfb51f4b 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -99,7 +99,7 @@ public void Update(Expr[] args)
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,57 @@ public bool IsBool
///
/// Indicates whether the term is the constant true.
///
- 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; } }
///
/// Indicates whether the term is the constant false.
///
- 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; } }
///
/// Indicates whether the term is an equality predicate.
///
- 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; } }
///
/// Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).
///
- 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; } }
///
/// Indicates whether the term is a ternary if-then-else term
///
- 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; } }
///
/// Indicates whether the term is an n-ary conjunction
///
- 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; } }
///
/// Indicates whether the term is an n-ary disjunction
///
- 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; } }
///
/// Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)
///
- 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; } }
///
/// Indicates whether the term is an exclusive or
///
- 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; } }
///
/// Indicates whether the term is a negation
///
- 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; } }
///
/// Indicates whether the term is an implication
///
- 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
@@ -347,82 +347,82 @@ public bool IsReal
///
/// Indicates whether the term is an arithmetic numeral.
///
- 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; } }
///
/// Indicates whether the term is a less-than-or-equal
///
- 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; } }
///
/// Indicates whether the term is a greater-than-or-equal
///
- 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; } }
///
/// Indicates whether the term is a less-than
///
- 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; } }
///
/// Indicates whether the term is a greater-than
///
- 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; } }
///
/// Indicates whether the term is addition (binary)
///
- 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; } }
///
/// Indicates whether the term is subtraction (binary)
///
- 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; } }
///
/// Indicates whether the term is a unary minus
///
- 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; } }
///
/// Indicates whether the term is multiplication (binary)
///
- 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; } }
///
/// Indicates whether the term is division (binary)
///
- 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; } }
///
/// Indicates whether the term is integer division (binary)
///
- 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; } }
///
/// Indicates whether the term is remainder (binary)
///
- 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; } }
///
/// Indicates whether the term is modulus (binary)
///
- 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; } }
///
/// Indicates whether the term is a coercion of integer to real (unary)
///
- 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; } }
///
/// Indicates whether the term is a coercion of real to integer (unary)
///
- 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; } }
///
/// Indicates whether the term is a check that tests whether a real is integral (unary)
///
- 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
@@ -444,64 +444,64 @@ public bool IsArray
///
/// It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j).
/// Array store takes at least 3 arguments.
- 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; } }
///
/// Indicates whether the term is an array select.
///
- 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; } }
///
/// Indicates whether the term is a constant array.
///
/// For example, select(const(v),i) = v holds for every v and i. The function is unary.
- 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; } }
///
/// Indicates whether the term is a default array.
///
/// For example default(const(v)) = v. The function is unary.
- 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; } }
///
/// Indicates whether the term is an array map.
///
/// It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.
- 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; } }
///
/// Indicates whether the term is an as-array term.
///
/// An as-array term is n array value that behaves as the function graph of the
/// function passed as parameter.
- 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
///
/// Indicates whether the term is set union
///
- 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; } }
///
/// Indicates whether the term is set intersection
///
- 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; } }
///
/// Indicates whether the term is set difference
///
- 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; } }
///
/// Indicates whether the term is set complement
///
- 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; } }
///
/// Indicates whether the term is set subset
///
- 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
@@ -516,266 +516,266 @@ public bool IsBV
///
/// Indicates whether the term is a bit-vector numeral
///
- 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; } }
///
/// Indicates whether the term is a one-bit bit-vector with value one
///
- 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; } }
///
/// Indicates whether the term is a one-bit bit-vector with value zero
///
- 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; } }
///
/// Indicates whether the term is a bit-vector unary minus
///
- 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; } }
///
/// Indicates whether the term is a bit-vector addition (binary)
///
- 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; } }
///
/// Indicates whether the term is a bit-vector subtraction (binary)
///
- 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; } }
///
/// Indicates whether the term is a bit-vector multiplication (binary)
///
- 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; } }
///
/// Indicates whether the term is a bit-vector signed division (binary)
///
- 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; } }
///
/// Indicates whether the term is a bit-vector unsigned division (binary)
///
- 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; } }
///
/// Indicates whether the term is a bit-vector signed remainder (binary)
///
- 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; } }
///
/// Indicates whether the term is a bit-vector unsigned remainder (binary)
///
- 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; } }
///
/// Indicates whether the term is a bit-vector signed modulus
///
- 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; } }
///
/// Indicates whether the term is a bit-vector signed division by zero
///
- 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; } }
///
/// Indicates whether the term is a bit-vector unsigned division by zero
///
- 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; } }
///
/// Indicates whether the term is a bit-vector signed remainder by zero
///
- 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; } }
///
/// Indicates whether the term is a bit-vector unsigned remainder by zero
///
- 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; } }
///
/// Indicates whether the term is a bit-vector signed modulus by zero
///
- 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; } }
///
/// Indicates whether the term is an unsigned bit-vector less-than-or-equal
///
- 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; } }
///
/// Indicates whether the term is a signed bit-vector less-than-or-equal
///
- 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; } }
///
/// Indicates whether the term is an unsigned bit-vector greater-than-or-equal
///
- 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; } }
///
/// Indicates whether the term is a signed bit-vector greater-than-or-equal
///
- 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; } }
///
/// Indicates whether the term is an unsigned bit-vector less-than
///
- 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; } }
///
/// Indicates whether the term is a signed bit-vector less-than
///
- 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; } }
///
/// Indicates whether the term is an unsigned bit-vector greater-than
///
- 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; } }
///
/// Indicates whether the term is a signed bit-vector greater-than
///
- 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; } }
///
/// Indicates whether the term is a bit-wise AND
///
- 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; } }
///
/// Indicates whether the term is a bit-wise OR
///
- 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; } }
///
/// Indicates whether the term is a bit-wise NOT
///
- 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; } }
///
/// Indicates whether the term is a bit-wise XOR
///
- 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; } }
///
/// Indicates whether the term is a bit-wise NAND
///
- 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; } }
///
/// Indicates whether the term is a bit-wise NOR
///
- 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; } }
///
/// Indicates whether the term is a bit-wise XNOR
///
- 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; } }
///
/// Indicates whether the term is a bit-vector concatenation (binary)
///
- 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; } }
///
/// Indicates whether the term is a bit-vector sign extension
///
- 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; } }
///
/// Indicates whether the term is a bit-vector zero extension
///
- 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; } }
///
/// Indicates whether the term is a bit-vector extraction
///
- 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; } }
///
/// Indicates whether the term is a bit-vector repetition
///
- 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; } }
///
/// Indicates whether the term is a bit-vector reduce OR
///
- 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; } }
///
/// Indicates whether the term is a bit-vector reduce AND
///
- 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; } }
///
/// Indicates whether the term is a bit-vector comparison
///
- 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; } }
///
/// Indicates whether the term is a bit-vector shift left
///
- 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; } }
///
/// Indicates whether the term is a bit-vector logical shift right
///
- 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; } }
///
/// Indicates whether the term is a bit-vector arithmetic shift left
///
- 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; } }
///
/// Indicates whether the term is a bit-vector rotate left
///
- 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; } }
///
/// Indicates whether the term is a bit-vector rotate right
///
- 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; } }
///
/// Indicates whether the term is a bit-vector rotate left (extended)
///
/// Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.
- 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; } }
///
/// Indicates whether the term is a bit-vector rotate right (extended)
///
/// Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.
- 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; } }
///
/// Indicates whether the term is a coercion from integer to bit-vector
///
/// This function is not supported by the decision procedures. Only the most
/// rudimentary simplification rules are applied to this function.
- 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; } }
///
/// Indicates whether the term is a coercion from bit-vector to integer
///
/// This function is not supported by the decision procedures. Only the most
/// rudimentary simplification rules are applied to this function.
- 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; } }
///
/// Indicates whether the term is a bit-vector carry
///
/// Compute the carry bit in a full-adder. The meaning is given by the
/// equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))
- 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; } }
///
/// Indicates whether the term is a bit-vector ternary XOR
///
/// The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
- 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
@@ -784,13 +784,13 @@ public bool IsBV
/// Indicates whether the term is a label (used by the Boogie Verification condition generator).
///
/// The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula.
- 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; } }
///
/// Indicates whether the term is a label literal (used by the Boogie Verification condition generator).
///
/// A label literal has a set of string parameters. It takes no arguments.
- 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
@@ -799,22 +799,22 @@ public bool IsBV
///
/// This binary predicate is used in proof terms.
/// It captures equisatisfiability and equivalence modulo renamings.
- 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; } }
///
/// Indicates whether the term is a Proof for the expression 'true'.
///
- 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; } }
///
/// Indicates whether the term is a proof for a fact asserted by the user.
///
- 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; } }
///
/// Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
///
- 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; } }
///
/// Indicates whether the term is proof via modus ponens
@@ -825,7 +825,7 @@ public bool IsBV
/// T2: (implies p q)
/// [mp T1 T2]: q
/// The second antecedents may also be a proof for (iff p q).
- 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; } }
///
/// Indicates whether the term is a proof for (R t t), where R is a reflexive relation.
@@ -834,7 +834,7 @@ public bool IsBV
/// The only reflexive relations that are used are
/// equivalence modulo namings, equality and equivalence.
/// That is, R is either '~', '=' or 'iff'.
- 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; } }
///
/// Indicates whether the term is proof by symmetricity of a relation
@@ -845,7 +845,7 @@ public bool IsBV
/// [symmetry T1]: (R s t)
/// T1 is the antecedent of this proof object.
///
- 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; } }
///
/// Indicates whether the term is a proof by transitivity of a relation
@@ -857,7 +857,7 @@ public bool IsBV
/// T2: (R s u)
/// [trans T1 T2]: (R t u)
///
- 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; } }
///
/// Indicates whether the term is a proof by condensed transitivity of a relation
@@ -878,7 +878,7 @@ public bool IsBV
/// if there is a path from s to t, if we view every
/// antecedent (R a b) as an edge between a and b.
///
- 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; } }
///
@@ -892,7 +892,7 @@ public bool IsBV
/// Remark: if t_i == s_i, then the antecedent Ti is suppressed.
/// That is, reflexivity proofs are supressed to save space.
///
- 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; } }
///
/// Indicates whether the term is a quant-intro proof
@@ -902,7 +902,7 @@ public bool IsBV
/// T1: (~ p q)
/// [quant-intro T1]: (~ (forall (x) p) (forall (x) q))
///
- 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; } }
///
/// Indicates whether the term is a distributivity proof object.
@@ -920,7 +920,7 @@ public bool IsBV
/// Remark. This rule is used by the CNF conversion pass and
/// instantiated by f = or, and g = and.
///
- 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; } }
///
/// Indicates whether the term is a proof by elimination of AND
@@ -930,7 +930,7 @@ public bool IsBV
/// T1: (and l_1 ... l_n)
/// [and-elim T1]: l_i
///
- 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; } }
///
/// Indicates whether the term is a proof by eliminiation of not-or
@@ -940,7 +940,7 @@ public bool IsBV
/// T1: (not (or l_1 ... l_n))
/// [not-or-elim T1]: (not l_i)
///
- 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; } }
///
/// Indicates whether the term is a proof by rewriting
@@ -959,7 +959,7 @@ public bool IsBV
/// (= (+ x 1 2) (+ 3 x))
/// (iff (or x false) x)
///
- 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; } }
///
/// Indicates whether the term is a proof by rewriting
@@ -975,7 +975,7 @@ public bool IsBV
/// - When converting bit-vectors to Booleans (BIT2BOOL=true)
/// - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
///
- 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; } }
///
/// Indicates whether the term is a proof for pulling quantifiers out.
@@ -983,7 +983,7 @@ public bool IsBV
///
/// A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
///
- 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; } }
///
/// Indicates whether the term is a proof for pulling quantifiers out.
@@ -993,7 +993,7 @@ public bool IsBV
/// This proof object is only used if the parameter PROOF_MODE is 1.
/// This proof object has no antecedents
///
- 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; } }
///
/// Indicates whether the term is a proof for pushing quantifiers in.
@@ -1006,7 +1006,7 @@ public bool IsBV
/// (forall (x_1 ... x_m) p_n[x_1 ... x_m])))
/// This proof object has no antecedents
///
- 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; } }
///
/// Indicates whether the term is a proof for elimination of unused variables.
@@ -1018,7 +1018,7 @@ public bool IsBV
/// It is used to justify the elimination of unused variables.
/// This proof object has no antecedents.
///
- 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; } }
///
/// Indicates whether the term is a proof for destructive equality resolution
@@ -1032,7 +1032,7 @@ public bool IsBV
///
/// Several variables can be eliminated simultaneously.
///
- 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; } }
///
/// Indicates whether the term is a proof for quantifier instantiation
@@ -1040,13 +1040,13 @@ public bool IsBV
///
/// A proof of (or (not (forall (x) (P x))) (P a))
///
- 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; } }
///
/// Indicates whether the term is a hypthesis marker.
///
/// Mark a hypothesis in a natural deduction style proof.
- 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; } }
///
/// Indicates whether the term is a proof by lemma
@@ -1059,7 +1059,7 @@ public bool IsBV
/// It converts the proof in a proof for (or (not l_1) ... (not l_n)),
/// when T1 contains the hypotheses: l_1, ..., l_n.
///
- 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; } }
///
/// Indicates whether the term is a proof by unit resolution
@@ -1071,7 +1071,7 @@ public bool IsBV
/// T(n+1): (not l_n)
/// [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
///
- 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; } }
///
/// Indicates whether the term is a proof by iff-true
@@ -1080,7 +1080,7 @@ public bool IsBV
/// T1: p
/// [iff-true T1]: (iff p true)
///
- 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; } }
///
/// Indicates whether the term is a proof by iff-false
@@ -1089,7 +1089,7 @@ public bool IsBV
/// T1: (not p)
/// [iff-false T1]: (iff p false)
///
- 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; } }
///
/// Indicates whether the term is a proof by commutativity
@@ -1102,7 +1102,7 @@ public bool IsBV
/// This proof object has no antecedents.
/// Remark: if f is bool, then = is iff.
///
- 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; } }
///
/// Indicates whether the term is a proof for Tseitin-like axioms
@@ -1138,7 +1138,7 @@ public bool IsBV
/// unfolding the Boolean connectives in the axioms a small
/// bounded number of steps (=3).
///
- 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; } }
///
/// Indicates whether the term is a proof for introduction of a name
@@ -1161,7 +1161,7 @@ public bool IsBV
/// Otherwise:
/// [def-intro]: (= n e)
///
- 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; } }
///
/// Indicates whether the term is a proof for application of a definition
@@ -1171,7 +1171,7 @@ public bool IsBV
/// F is 'equivalent' to n, given that T1 is a proof that
/// n is a name for F.
///
- 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; } }
///
/// Indicates whether the term is a proof iff-oeq
@@ -1180,7 +1180,7 @@ public bool IsBV
/// T1: (iff p q)
/// [iff~ T1]: (~ p q)
///
- 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; } }
///
/// Indicates whether the term is a proof for a positive NNF step
@@ -1208,7 +1208,7 @@ public bool IsBV
/// NNF_NEG furthermore handles the case where negation is pushed
/// over Boolean connectives 'and' and 'or'.
///
- 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; } }
///
/// Indicates whether the term is a proof for a negative NNF step
@@ -1233,7 +1233,7 @@ public bool IsBV
/// [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
/// (and (or r_1 r_2) (or r_1' r_2')))
///
- 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; } }
///
/// Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
@@ -1245,7 +1245,7 @@ public bool IsBV
///
/// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
///
- 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; } }
///
/// Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
@@ -1255,7 +1255,7 @@ public bool IsBV
/// 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.
///
- 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; } }
///
/// Indicates whether the term is a proof for a Skolemization step
@@ -1268,7 +1268,7 @@ public bool IsBV
///
/// This proof object has no antecedents.
///
- 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; } }
///
/// Indicates whether the term is a proof by modus ponens for equi-satisfiability.
@@ -1279,7 +1279,7 @@ public bool IsBV
/// T2: (~ p q)
/// [mp~ T1 T2]: q
///
- 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; } }
///
/// Indicates whether the term is a proof for theory lemma
@@ -1298,7 +1298,7 @@ public bool IsBV
/// (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1)))
/// - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
///
- 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
@@ -1323,40 +1323,40 @@ public bool IsRelation
/// The function takes n+1 arguments, where the first argument is the relation and the remaining n elements
/// correspond to the n columns of the relation.
///
- 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; } }
///
/// Indicates whether the term is an empty relation
///
- 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; } }
///
/// Indicates whether the term is a test for the emptiness of a relation
///
- 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; } }
///
/// Indicates whether the term is a relational join
///
- 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; } }
///
/// Indicates whether the term is the union or convex hull of two relations.
///
/// The function takes two arguments.
- 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; } }
///
/// Indicates whether the term is the widening of two relations
///
/// The function takes two arguments.
- 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; } }
///
/// Indicates whether the term is a projection of columns (provided as numbers in the parameters).
///
/// The function takes one argument.
- 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; } }
///
/// Indicates whether the term is a relation filter
@@ -1368,7 +1368,7 @@ public bool IsRelation
/// corresponding to the columns of the relation.
/// So the first column in the relation has index 0.
///
- 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; } }
///
/// Indicates whether the term is an intersection of a relation with the negation of another.
@@ -1384,7 +1384,7 @@ public bool IsRelation
/// 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.
///
- 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; } }
///
/// Indicates whether the term is the renaming of a column in a relation
@@ -1393,12 +1393,12 @@ public bool IsRelation
/// The function takes one argument.
/// The parameters contain the renaming as a cycle.
///
- 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; } }
///
/// Indicates whether the term is the complement of a relation
///
- 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; } }
///
/// Indicates whether the term is a relational select
@@ -1408,7 +1408,7 @@ public bool IsRelation
/// The function takes n+1 arguments, where the first argument is a relation,
/// and the remaining n arguments correspond to a record.
///
- 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; } }
///
/// Indicates whether the term is a relational clone (copy)
@@ -1420,7 +1420,7 @@ public bool IsRelation
/// for terms of kind
/// to perform destructive updates to the first argument.
///
- 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
@@ -1439,7 +1439,7 @@ public bool IsFiniteDomain
///
/// Indicates whether the term is a less than predicate over a finite domain.
///
- 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
diff --git a/src/api/dotnet/Global.cs b/src/api/dotnet/Global.cs
index 707264c828a..787c9b78890 100644
--- a/src/api/dotnet/Global.cs
+++ b/src/api/dotnet/Global.cs
@@ -43,7 +43,7 @@ public static class Global
/// 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 ..
+ /// 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.
diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj
index 9eb9eb660da..0a062054dc5 100644
--- a/src/api/dotnet/Microsoft.Z3.csproj
+++ b/src/api/dotnet/Microsoft.Z3.csproj
@@ -24,8 +24,7 @@
prompt
4
true
-
-
+ ..\Debug\Microsoft.Z3.XML
False
False
True
@@ -140,6 +139,7 @@
Full
%28none%29
0
+ ..\x64\Debug\Microsoft.Z3.XML
..\x64\external_64\
@@ -193,7 +193,7 @@
..\x64\external\
true
- ..\external\Microsoft.Z3.xml
+ ..\x64\external\Microsoft.Z3.XML
true
pdbonly
x64
@@ -220,7 +220,7 @@
..\Release_delaysign\
true
- ..\Release_delaysign\Microsoft.Z3.xml
+ ..\Release_delaysign\Microsoft.Z3.XML
true
pdbonly
AnyCPU
@@ -238,7 +238,7 @@
bin\x64\Release_delaysign\
true
- ..\x64\external_64\Microsoft.Z3.xml
+ bin\x64\Release_delaysign\Microsoft.Z3.XML
true
pdbonly
x64
@@ -266,11 +266,12 @@
MinimumRecommendedRules.ruleset
;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ bin\x86\Debug\Microsoft.Z3.XML
bin\x86\Release\
true
- ..\external\Microsoft.Z3.xml
+ bin\x86\Release\Microsoft.Z3.xml
true
pdbonly
x86
@@ -285,7 +286,7 @@
bin\x86\external\
true
- ..\external\Microsoft.Z3.xml
+ bin\x86\external\Microsoft.Z3.XML
true
pdbonly
x86
@@ -303,7 +304,7 @@
bin\x86\Release_delaysign\
DELAYSIGN
true
- ..\Release_delaysign\Microsoft.Z3.xml
+ bin\x86\Release_delaysign\Microsoft.Z3.XML
true
pdbonly
x86
@@ -399,4 +400,4 @@
-->
-
+
\ No newline at end of file
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 555a2466fac..9de515e8629 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -132,7 +132,8 @@ public void Add(params BoolExpr[] constraints)
///
/// This API is an alternative to 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 and the Boolean literals
+ /// of the Boolean variables provided using
+ /// and the Boolean literals
/// provided using with assumptions.
///
public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
@@ -156,7 +157,8 @@ public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
///
/// This API is an alternative to 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 and the Boolean literals
+ /// of the Boolean variables provided using
+ /// and the Boolean literals
/// provided using with assumptions.
///
public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 7793a16e5e7..f7edc6a2b14 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -94,7 +94,7 @@ public Expr[] getArgs() throws Z3Exception
public void update(Expr[] args) throws Z3Exception
{
getContext().checkContextMatch(args);
- if (args.length != getNumArgs())
+ if (isApp() && args.length != getNumArgs())
throw new Z3Exception("Number of arguments does not match");
setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(),
(int) args.length, Expr.arrayToNative(args)));
@@ -245,7 +245,7 @@ public boolean isBool() throws Z3Exception
**/
public boolean isTrue() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE;
}
/**
@@ -253,7 +253,7 @@ public boolean isTrue() throws Z3Exception
**/
public boolean isFalse() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE;
}
/**
@@ -261,7 +261,7 @@ public boolean isFalse() throws Z3Exception
**/
public boolean isEq() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ;
}
/**
@@ -270,7 +270,7 @@ public boolean isEq() throws Z3Exception
**/
public boolean isDistinct() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT;
}
/**
@@ -278,7 +278,7 @@ public boolean isDistinct() throws Z3Exception
**/
public boolean isITE() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE;
}
/**
@@ -286,7 +286,7 @@ public boolean isITE() throws Z3Exception
**/
public boolean isAnd() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND;
}
/**
@@ -294,7 +294,7 @@ public boolean isAnd() throws Z3Exception
**/
public boolean isOr() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR;
}
/**
@@ -303,7 +303,7 @@ public boolean isOr() throws Z3Exception
**/
public boolean isIff() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF;
}
/**
@@ -311,7 +311,7 @@ public boolean isIff() throws Z3Exception
**/
public boolean isXor() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR;
}
/**
@@ -319,7 +319,7 @@ public boolean isXor() throws Z3Exception
**/
public boolean isNot() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT;
}
/**
@@ -327,7 +327,7 @@ public boolean isNot() throws Z3Exception
**/
public boolean isImplies() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES;
}
/**
@@ -356,7 +356,7 @@ public boolean isReal() throws Z3Exception
**/
public boolean isArithmeticNumeral() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM;
}
/**
@@ -364,7 +364,7 @@ public boolean isArithmeticNumeral() throws Z3Exception
**/
public boolean isLE() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE;
}
/**
@@ -372,7 +372,7 @@ public boolean isLE() throws Z3Exception
**/
public boolean isGE() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE;
}
/**
@@ -380,7 +380,7 @@ public boolean isGE() throws Z3Exception
**/
public boolean isLT() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT;
}
/**
@@ -388,7 +388,7 @@ public boolean isLT() throws Z3Exception
**/
public boolean isGT() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT;
}
/**
@@ -396,7 +396,7 @@ public boolean isGT() throws Z3Exception
**/
public boolean isAdd() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD;
}
/**
@@ -404,7 +404,7 @@ public boolean isAdd() throws Z3Exception
**/
public boolean isSub() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB;
}
/**
@@ -412,7 +412,7 @@ public boolean isSub() throws Z3Exception
**/
public boolean isUMinus() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS;
}
/**
@@ -420,7 +420,7 @@ public boolean isUMinus() throws Z3Exception
**/
public boolean isMul() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL;
}
/**
@@ -428,7 +428,7 @@ public boolean isMul() throws Z3Exception
**/
public boolean isDiv() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV;
}
/**
@@ -436,7 +436,7 @@ public boolean isDiv() throws Z3Exception
**/
public boolean isIDiv() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV;
}
/**
@@ -444,7 +444,7 @@ public boolean isIDiv() throws Z3Exception
**/
public boolean isRemainder() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM;
}
/**
@@ -452,7 +452,7 @@ public boolean isRemainder() throws Z3Exception
**/
public boolean isModulus() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD;
}
/**
@@ -460,7 +460,7 @@ public boolean isModulus() throws Z3Exception
**/
public boolean isIntToReal() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL;
}
/**
@@ -468,7 +468,7 @@ public boolean isIntToReal() throws Z3Exception
**/
public boolean isRealToInt() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT;
}
/**
@@ -477,7 +477,7 @@ public boolean isRealToInt() throws Z3Exception
**/
public boolean isRealIsInt() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT;
}
/**
@@ -497,7 +497,7 @@ public boolean isArray() throws Z3Exception
**/
public boolean isStore() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE;
}
/**
@@ -505,7 +505,7 @@ public boolean isStore() throws Z3Exception
**/
public boolean isSelect() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT;
}
/**
@@ -515,7 +515,7 @@ public boolean isSelect() throws Z3Exception
**/
public boolean isConstantArray() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY;
}
/**
@@ -524,7 +524,7 @@ public boolean isConstantArray() throws Z3Exception
**/
public boolean isDefaultArray() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT;
}
/**
@@ -533,7 +533,7 @@ public boolean isDefaultArray() throws Z3Exception
**/
public boolean isArrayMap() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP;
}
/**
@@ -543,7 +543,7 @@ public boolean isArrayMap() throws Z3Exception
**/
public boolean isAsArray() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY;
}
/**
@@ -551,7 +551,7 @@ public boolean isAsArray() throws Z3Exception
**/
public boolean isSetUnion() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION;
}
/**
@@ -559,7 +559,7 @@ public boolean isSetUnion() throws Z3Exception
**/
public boolean isSetIntersect() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT;
}
/**
@@ -567,7 +567,7 @@ public boolean isSetIntersect() throws Z3Exception
**/
public boolean isSetDifference() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE;
}
/**
@@ -575,7 +575,7 @@ public boolean isSetDifference() throws Z3Exception
**/
public boolean isSetComplement() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT;
}
/**
@@ -583,7 +583,7 @@ public boolean isSetComplement() throws Z3Exception
**/
public boolean isSetSubset() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET;
}
/**
@@ -601,7 +601,7 @@ public boolean isBV() throws Z3Exception
**/
public boolean isBVNumeral() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM;
}
/**
@@ -609,7 +609,7 @@ public boolean isBVNumeral() throws Z3Exception
**/
public boolean isBVBitOne() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1;
}
/**
@@ -617,7 +617,7 @@ public boolean isBVBitOne() throws Z3Exception
**/
public boolean isBVBitZero() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0;
}
/**
@@ -625,7 +625,7 @@ public boolean isBVBitZero() throws Z3Exception
**/
public boolean isBVUMinus() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG;
}
/**
@@ -633,7 +633,7 @@ public boolean isBVUMinus() throws Z3Exception
**/
public boolean isBVAdd() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD;
}
/**
@@ -641,7 +641,7 @@ public boolean isBVAdd() throws Z3Exception
**/
public boolean isBVSub() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB;
}
/**
@@ -649,7 +649,7 @@ public boolean isBVSub() throws Z3Exception
**/
public boolean isBVMul() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL;
}
/**
@@ -657,7 +657,7 @@ public boolean isBVMul() throws Z3Exception
**/
public boolean isBVSDiv() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV;
}
/**
@@ -665,7 +665,7 @@ public boolean isBVSDiv() throws Z3Exception
**/
public boolean isBVUDiv() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV;
}
/**
@@ -673,7 +673,7 @@ public boolean isBVUDiv() throws Z3Exception
**/
public boolean isBVSRem() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM;
}
/**
@@ -681,7 +681,7 @@ public boolean isBVSRem() throws Z3Exception
**/
public boolean isBVURem() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM;
}
/**
@@ -689,7 +689,7 @@ public boolean isBVURem() throws Z3Exception
**/
public boolean isBVSMod() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD;
}
/**
@@ -697,7 +697,7 @@ public boolean isBVSMod() throws Z3Exception
**/
boolean IsBVSDiv0() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV0;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV0;
}
/**
@@ -705,7 +705,7 @@ boolean IsBVSDiv0() throws Z3Exception
**/
boolean IsBVUDiv0() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV0;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV0;
}
/**
@@ -713,7 +713,7 @@ boolean IsBVUDiv0() throws Z3Exception
**/
boolean IsBVSRem0() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM0;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM0;
}
/**
@@ -721,7 +721,7 @@ boolean IsBVSRem0() throws Z3Exception
**/
boolean IsBVURem0() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM0;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM0;
}
/**
@@ -729,7 +729,7 @@ boolean IsBVURem0() throws Z3Exception
**/
boolean IsBVSMod0() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD0;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD0;
}
/**
@@ -737,7 +737,7 @@ boolean IsBVSMod0() throws Z3Exception
**/
public boolean isBVULE() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ;
}
/**
@@ -745,7 +745,7 @@ public boolean isBVULE() throws Z3Exception
**/
public boolean isBVSLE() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ;
}
/**
@@ -754,7 +754,7 @@ public boolean isBVSLE() throws Z3Exception
**/
public boolean isBVUGE() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ;
}
/**
@@ -762,7 +762,7 @@ public boolean isBVUGE() throws Z3Exception
**/
public boolean isBVSGE() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ;
}
/**
@@ -770,7 +770,7 @@ public boolean isBVSGE() throws Z3Exception
**/
public boolean isBVULT() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT;
}
/**
@@ -778,7 +778,7 @@ public boolean isBVULT() throws Z3Exception
**/
public boolean isBVSLT() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT;
}
/**
@@ -786,7 +786,7 @@ public boolean isBVSLT() throws Z3Exception
**/
public boolean isBVUGT() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT;
}
/**
@@ -794,7 +794,7 @@ public boolean isBVUGT() throws Z3Exception
**/
public boolean isBVSGT() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT;
}
/**
@@ -802,7 +802,7 @@ public boolean isBVSGT() throws Z3Exception
**/
public boolean isBVAND() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND;
}
/**
@@ -810,7 +810,7 @@ public boolean isBVAND() throws Z3Exception
**/
public boolean isBVOR() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
}
/**
@@ -818,7 +818,7 @@ public boolean isBVOR() throws Z3Exception
**/
public boolean isBVNOT() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT;
}
/**
@@ -826,7 +826,7 @@ public boolean isBVNOT() throws Z3Exception
**/
public boolean isBVXOR() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR;
}
/**
@@ -834,7 +834,7 @@ public boolean isBVXOR() throws Z3Exception
**/
public boolean isBVNAND() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND;
}
/**
@@ -842,7 +842,7 @@ public boolean isBVNAND() throws Z3Exception
**/
public boolean isBVNOR() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR;
}
/**
@@ -850,7 +850,7 @@ public boolean isBVNOR() throws Z3Exception
**/
public boolean isBVXNOR() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR;
}
/**
@@ -858,7 +858,7 @@ public boolean isBVXNOR() throws Z3Exception
**/
public boolean isBVConcat() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT;
}
/**
@@ -866,7 +866,7 @@ public boolean isBVConcat() throws Z3Exception
**/
public boolean isBVSignExtension() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT;
}
/**
@@ -874,7 +874,7 @@ public boolean isBVSignExtension() throws Z3Exception
**/
public boolean isBVZeroExtension() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT;
}
/**
@@ -882,7 +882,7 @@ public boolean isBVZeroExtension() throws Z3Exception
**/
public boolean isBVExtract() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT;
}
/**
@@ -890,7 +890,7 @@ public boolean isBVExtract() throws Z3Exception
**/
public boolean isBVRepeat() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT;
}
/**
@@ -898,7 +898,7 @@ public boolean isBVRepeat() throws Z3Exception
**/
public boolean isBVReduceOR() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR;
}
/**
@@ -906,7 +906,7 @@ public boolean isBVReduceOR() throws Z3Exception
**/
public boolean isBVReduceAND() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND;
}
/**
@@ -914,7 +914,7 @@ public boolean isBVReduceAND() throws Z3Exception
**/
public boolean isBVComp() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP;
}
/**
@@ -922,7 +922,7 @@ public boolean isBVComp() throws Z3Exception
**/
public boolean isBVShiftLeft() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL;
}
/**
@@ -930,7 +930,7 @@ public boolean isBVShiftLeft() throws Z3Exception
**/
public boolean isBVShiftRightLogical() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR;
}
/**
@@ -938,7 +938,7 @@ public boolean isBVShiftRightLogical() throws Z3Exception
**/
public boolean isBVShiftRightArithmetic() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR;
}
/**
@@ -946,7 +946,7 @@ public boolean isBVShiftRightArithmetic() throws Z3Exception
**/
public boolean isBVRotateLeft() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT;
}
/**
@@ -954,7 +954,7 @@ public boolean isBVRotateLeft() throws Z3Exception
**/
public boolean isBVRotateRight() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT;
}
/**
@@ -964,7 +964,7 @@ public boolean isBVRotateRight() throws Z3Exception
**/
public boolean isBVRotateLeftExtended() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT;
}
/**
@@ -974,7 +974,7 @@ public boolean isBVRotateLeftExtended() throws Z3Exception
**/
public boolean isBVRotateRightExtended() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT;
}
/**
@@ -985,7 +985,7 @@ public boolean isBVRotateRightExtended() throws Z3Exception
**/
public boolean isIntToBV() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV;
}
/**
@@ -996,7 +996,7 @@ public boolean isIntToBV() throws Z3Exception
**/
public boolean isBVToInt() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT;
}
/**
@@ -1006,7 +1006,7 @@ public boolean isBVToInt() throws Z3Exception
**/
public boolean isBVCarry() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY;
}
/**
@@ -1016,7 +1016,7 @@ public boolean isBVCarry() throws Z3Exception
**/
public boolean isBVXOR3() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3;
}
/**
@@ -1026,7 +1026,7 @@ public boolean isBVXOR3() throws Z3Exception
**/
public boolean isLabel() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL;
}
/**
@@ -1036,7 +1036,7 @@ public boolean isLabel() throws Z3Exception
**/
public boolean isLabelLit() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
}
/**
@@ -1046,7 +1046,7 @@ public boolean isLabelLit() throws Z3Exception
**/
public boolean isOEQ() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
}
/**
@@ -1054,7 +1054,7 @@ public boolean isOEQ() throws Z3Exception
**/
public boolean isProofTrue() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE;
}
/**
@@ -1062,7 +1062,7 @@ public boolean isProofTrue() throws Z3Exception
**/
public boolean isProofAsserted() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED;
}
/**
@@ -1071,7 +1071,7 @@ public boolean isProofAsserted() throws Z3Exception
**/
public boolean isProofGoal() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL;
}
/**
@@ -1082,7 +1082,7 @@ public boolean isProofGoal() throws Z3Exception
**/
public boolean isProofModusPonens() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS;
}
/**
@@ -1094,7 +1094,7 @@ public boolean isProofModusPonens() throws Z3Exception
**/
public boolean isProofReflexivity() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY;
}
/**
@@ -1105,7 +1105,7 @@ public boolean isProofReflexivity() throws Z3Exception
**/
public boolean isProofSymmetry() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY;
}
/**
@@ -1116,7 +1116,7 @@ public boolean isProofSymmetry() throws Z3Exception
**/
public boolean isProofTransitivity() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY;
}
/**
@@ -1134,7 +1134,7 @@ public boolean isProofTransitivity() throws Z3Exception
**/
public boolean isProofTransitivityStar() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR;
}
/**
@@ -1146,7 +1146,7 @@ public boolean isProofTransitivityStar() throws Z3Exception
**/
public boolean isProofMonotonicity() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY;
}
/**
@@ -1156,7 +1156,7 @@ public boolean isProofMonotonicity() throws Z3Exception
**/
public boolean isProofQuantIntro() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO;
}
/**
@@ -1172,7 +1172,7 @@ public boolean isProofQuantIntro() throws Z3Exception
**/
public boolean isProofDistributivity() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY;
}
/**
@@ -1182,7 +1182,7 @@ public boolean isProofDistributivity() throws Z3Exception
**/
public boolean isProofAndElimination() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM;
}
/**
@@ -1192,7 +1192,7 @@ public boolean isProofAndElimination() throws Z3Exception
**/
public boolean isProofOrElimination() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM;
}
/**
@@ -1209,7 +1209,7 @@ public boolean isProofOrElimination() throws Z3Exception
**/
public boolean isProofRewrite() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE;
}
/**
@@ -1225,7 +1225,7 @@ public boolean isProofRewrite() throws Z3Exception
**/
public boolean isProofRewriteStar() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR;
}
/**
@@ -1235,7 +1235,7 @@ public boolean isProofRewriteStar() throws Z3Exception
**/
public boolean isProofPullQuant() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
}
/**
@@ -1246,7 +1246,7 @@ public boolean isProofPullQuant() throws Z3Exception
**/
public boolean isProofPullQuantStar() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR;
}
/**
@@ -1258,7 +1258,7 @@ public boolean isProofPullQuantStar() throws Z3Exception
**/
public boolean isProofPushQuant() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT;
}
/**
@@ -1271,7 +1271,7 @@ public boolean isProofPushQuant() throws Z3Exception
**/
public boolean isProofElimUnusedVars() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS;
}
/**
@@ -1285,7 +1285,7 @@ public boolean isProofElimUnusedVars() throws Z3Exception
**/
public boolean isProofDER() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER;
}
/**
@@ -1294,7 +1294,7 @@ public boolean isProofDER() throws Z3Exception
**/
public boolean isProofQuantInst() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST;
}
/**
@@ -1303,7 +1303,7 @@ public boolean isProofQuantInst() throws Z3Exception
**/
public boolean isProofHypothesis() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS;
}
/**
@@ -1316,7 +1316,7 @@ public boolean isProofHypothesis() throws Z3Exception
**/
public boolean isProofLemma() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA;
}
/**
@@ -1326,7 +1326,7 @@ public boolean isProofLemma() throws Z3Exception
**/
public boolean isProofUnitResolution() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION;
}
/**
@@ -1335,7 +1335,7 @@ public boolean isProofUnitResolution() throws Z3Exception
**/
public boolean isProofIFFTrue() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE;
}
/**
@@ -1344,7 +1344,7 @@ public boolean isProofIFFTrue() throws Z3Exception
**/
public boolean isProofIFFFalse() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE;
}
/**
@@ -1358,7 +1358,7 @@ public boolean isProofIFFFalse() throws Z3Exception
**/
public boolean isProofCommutativity() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY;
}
/**
@@ -1381,7 +1381,7 @@ public boolean isProofCommutativity() throws Z3Exception
**/
public boolean isProofDefAxiom() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM;
}
/**
@@ -1402,7 +1402,7 @@ public boolean isProofDefAxiom() throws Z3Exception
**/
public boolean isProofDefIntro() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO;
}
/**
@@ -1412,7 +1412,7 @@ public boolean isProofDefIntro() throws Z3Exception
**/
public boolean isProofApplyDef() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF;
}
/**
@@ -1421,7 +1421,7 @@ public boolean isProofApplyDef() throws Z3Exception
**/
public boolean isProofIFFOEQ() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ;
}
/**
@@ -1446,7 +1446,7 @@ public boolean isProofIFFOEQ() throws Z3Exception
**/
public boolean isProofNNFPos() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS;
}
/**
@@ -1462,7 +1462,7 @@ public boolean isProofNNFPos() throws Z3Exception
**/
public boolean isProofNNFNeg() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
}
/**
@@ -1477,7 +1477,7 @@ public boolean isProofNNFNeg() throws Z3Exception
**/
public boolean isProofNNFStar() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR;
}
/**
@@ -1489,7 +1489,7 @@ public boolean isProofNNFStar() throws Z3Exception
**/
public boolean isProofCNFStar() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR;
}
/**
@@ -1503,7 +1503,7 @@ public boolean isProofCNFStar() throws Z3Exception
**/
public boolean isProofSkolemize() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE;
}
/**
@@ -1513,7 +1513,7 @@ public boolean isProofSkolemize() throws Z3Exception
**/
public boolean isProofModusPonensOEQ() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ;
}
/**
@@ -1532,7 +1532,7 @@ public boolean isProofModusPonensOEQ() throws Z3Exception
**/
public boolean isProofTheoryLemma() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA;
}
/**
@@ -1554,7 +1554,7 @@ public boolean isRelation() throws Z3Exception
**/
public boolean isRelationStore() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE;
}
/**
@@ -1562,7 +1562,7 @@ public boolean isRelationStore() throws Z3Exception
**/
public boolean isEmptyRelation() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY;
}
/**
@@ -1570,7 +1570,7 @@ public boolean isEmptyRelation() throws Z3Exception
**/
public boolean isIsEmptyRelation() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY;
}
/**
@@ -1578,7 +1578,7 @@ public boolean isIsEmptyRelation() throws Z3Exception
**/
public boolean isRelationalJoin() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN;
}
/**
@@ -1587,7 +1587,7 @@ public boolean isRelationalJoin() throws Z3Exception
**/
public boolean isRelationUnion() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION;
}
/**
@@ -1596,7 +1596,7 @@ public boolean isRelationUnion() throws Z3Exception
**/
public boolean isRelationWiden() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN;
}
/**
@@ -1606,7 +1606,7 @@ public boolean isRelationWiden() throws Z3Exception
**/
public boolean isRelationProject() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT;
}
/**
@@ -1618,7 +1618,7 @@ public boolean isRelationProject() throws Z3Exception
**/
public boolean isRelationFilter() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER;
}
/**
@@ -1635,7 +1635,7 @@ public boolean isRelationFilter() throws Z3Exception
**/
public boolean isRelationNegationFilter() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER;
}
/**
@@ -1645,7 +1645,7 @@ public boolean isRelationNegationFilter() throws Z3Exception
**/
public boolean isRelationRename() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME;
}
/**
@@ -1653,7 +1653,7 @@ public boolean isRelationRename() throws Z3Exception
**/
public boolean isRelationComplement() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT;
}
/**
@@ -1664,7 +1664,7 @@ public boolean isRelationComplement() throws Z3Exception
**/
public boolean isRelationSelect() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT;
}
/**
@@ -1676,7 +1676,7 @@ public boolean isRelationSelect() throws Z3Exception
**/
public boolean isRelationClone() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE;
}
/**
@@ -1695,7 +1695,7 @@ public boolean isFiniteDomain() throws Z3Exception
**/
public boolean isFiniteDomainLT() throws Z3Exception
{
- return getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT;
+ return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT;
}
/**
diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
similarity index 92%
rename from src/tactic/fpa/fpa2bv_converter.cpp
rename to src/ast/fpa/fpa2bv_converter.cpp
index 2d1d6705f7a..20925a0f98d 100644
--- a/src/tactic/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -872,8 +872,19 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(extra_bits-2, 0, quotient));
res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(extra_bits+sbits+1, extra_bits-1, quotient), sticky);
- SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4));
+ 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.
@@ -2743,215 +2754,3 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
}
-
-void fpa2bv_model_converter::display(std::ostream & out) {
- out << "(fpa2bv-model-converter";
- for (obj_map::iterator it = m_const2bv.begin();
- it != m_const2bv.end();
- it++) {
- const symbol & n = it->m_key->get_name();
- out << "\n (" << n << " ";
- unsigned indent = n.size() + 4;
- out << mk_ismt2_pp(it->m_value, m, indent) << ")";
- }
- for (obj_map::iterator it = m_rm_const2bv.begin();
- it != m_rm_const2bv.end();
- it++) {
- const symbol & n = it->m_key->get_name();
- out << "\n (" << n << " ";
- unsigned indent = n.size() + 4;
- out << mk_ismt2_pp(it->m_value, m, indent) << ")";
- }
- for (obj_map::iterator it = m_uf2bvuf.begin();
- it != m_uf2bvuf.end();
- it++) {
- const symbol & n = it->m_key->get_name();
- out << "\n (" << n << " ";
- unsigned indent = n.size() + 4;
- out << mk_ismt2_pp(it->m_value, m, indent) << ")";
- }
- for (obj_map::iterator it = m_uf23bvuf.begin();
- it != m_uf23bvuf.end();
- it++) {
- const symbol & n = it->m_key->get_name();
- out << "\n (" << n << " ";
- unsigned indent = n.size() + 4;
- out << mk_ismt2_pp(it->m_value.f_sgn, m, indent) << " ; " <<
- mk_ismt2_pp(it->m_value.f_sig, m, indent) << " ; " <<
- mk_ismt2_pp(it->m_value.f_exp, m, indent) << " ; " <<
- ")";
- }
- out << ")" << std::endl;
-}
-
-model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
- fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to());
- for (obj_map::iterator it = m_const2bv.begin();
- it != m_const2bv.end();
- it++)
- {
- func_decl * k = translator(it->m_key);
- expr * v = translator(it->m_value);
- res->m_const2bv.insert(k, v);
- translator.to().inc_ref(k);
- translator.to().inc_ref(v);
- }
- for (obj_map::iterator it = m_rm_const2bv.begin();
- it != m_rm_const2bv.end();
- it++)
- {
- func_decl * k = translator(it->m_key);
- expr * v = translator(it->m_value);
- res->m_rm_const2bv.insert(k, v);
- translator.to().inc_ref(k);
- translator.to().inc_ref(v);
- }
- return res;
-}
-
-void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
- float_util fu(m);
- bv_util bu(m);
- mpf fp_val;
- unsynch_mpz_manager & mpzm = fu.fm().mpz_manager();
- unsynch_mpq_manager & mpqm = fu.fm().mpq_manager();
-
- TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
- for (unsigned i = 0 ; i < bv_mdl->get_num_constants(); i++)
- tout << bv_mdl->get_constant(i)->get_name() << " --> " <<
- mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl;
- );
-
- obj_hashtable seen;
-
- for (obj_map::iterator it = m_const2bv.begin();
- it != m_const2bv.end();
- it++)
- {
- func_decl * var = it->m_key;
- app * a = to_app(it->m_value);
- SASSERT(fu.is_float(var->get_range()));
- SASSERT(var->get_range()->get_num_parameters() == 2);
-
- unsigned ebits = fu.get_ebits(var->get_range());
- unsigned sbits = fu.get_sbits(var->get_range());
-
- expr_ref sgn(m), sig(m), exp(m);
- sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl());
- sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
- exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
-
- seen.insert(to_app(a->get_arg(0))->get_decl());
- seen.insert(to_app(a->get_arg(1))->get_decl());
- seen.insert(to_app(a->get_arg(2))->get_decl());
-
- if (!sgn && !sig && !exp)
- continue;
-
- unsigned sgn_sz = bu.get_bv_size(m.get_sort(a->get_arg(0)));
- unsigned sig_sz = bu.get_bv_size(m.get_sort(a->get_arg(1))) - 1;
- unsigned exp_sz = bu.get_bv_size(m.get_sort(a->get_arg(2)));
-
- rational sgn_q(0), sig_q(0), exp_q(0);
-
- if (sgn) bu.is_numeral(sgn, sgn_q, sgn_sz);
- if (sig) bu.is_numeral(sig, sig_q, sig_sz);
- if (exp) bu.is_numeral(exp, exp_q, exp_sz);
-
- // un-bias exponent
- rational exp_unbiased_q;
- exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(ebits-1);
-
- mpz sig_z; mpf_exp_t exp_z;
- mpzm.set(sig_z, sig_q.to_mpq().numerator());
- exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
-
- TRACE("fpa2bv_mc", tout << var->get_name() << " == [" << sgn_q.to_string() << " " <<
- mpzm.to_string(sig_z) << " " << exp_z << "(" << exp_q.to_string() << ")]" << std::endl; );
-
- fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z);
-
- float_mdl->register_decl(var, fu.mk_value(fp_val));
-
- mpzm.del(sig_z);
- }
-
- for (obj_map::iterator it = m_rm_const2bv.begin();
- it != m_rm_const2bv.end();
- it++)
- {
- func_decl * var = it->m_key;
- app * a = to_app(it->m_value);
- SASSERT(fu.is_rm(var->get_range()));
- rational val(0);
- unsigned sz = 0;
- if (a && bu.is_numeral(a, val, sz)) {
- TRACE("fpa2bv_mc", tout << var->get_name() << " == " << val.to_string() << std::endl; );
- SASSERT(val.is_uint64());
- switch (val.get_uint64())
- {
- case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break;
- case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break;
- case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break;
- case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break;
- case BV_RM_TO_ZERO:
- default: float_mdl->register_decl(var, fu.mk_round_toward_zero());
- }
- seen.insert(var);
- }
- }
-
- for (obj_map::iterator it = m_uf2bvuf.begin();
- it != m_uf2bvuf.end();
- it++)
- seen.insert(it->m_value);
-
- for (obj_map::iterator it = m_uf23bvuf.begin();
- it != m_uf23bvuf.end();
- it++)
- {
- seen.insert(it->m_value.f_sgn);
- seen.insert(it->m_value.f_sig);
- seen.insert(it->m_value.f_exp);
- }
-
- fu.fm().del(fp_val);
-
- // Keep all the non-float constants.
- unsigned sz = bv_mdl->get_num_constants();
- for (unsigned i = 0; i < sz; i++)
- {
- func_decl * c = bv_mdl->get_constant(i);
- if (!seen.contains(c))
- float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
- }
-
- // And keep everything else
- sz = bv_mdl->get_num_functions();
- for (unsigned i = 0; i < sz; i++)
- {
- func_decl * f = bv_mdl->get_function(i);
- if (!seen.contains(f))
- {
- TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl; );
- func_interp * val = bv_mdl->get_func_interp(f);
- float_mdl->register_decl(f, val);
- }
- }
-
- sz = bv_mdl->get_num_uninterpreted_sorts();
- for (unsigned i = 0; i < sz; i++)
- {
- sort * s = bv_mdl->get_uninterpreted_sort(i);
- ptr_vector u = bv_mdl->get_universe(s);
- float_mdl->register_usort(s, u.size(), u.c_ptr());
- }
-}
-
-model_converter * mk_fpa2bv_model_converter(ast_manager & m,
- obj_map const & const2bv,
- obj_map const & rm_const2bv,
- obj_map const & uf2bvuf,
- obj_map const & uf23bvuf) {
- return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf);
-}
diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
similarity index 72%
rename from src/tactic/fpa/fpa2bv_converter.h
rename to src/ast/fpa/fpa2bv_converter.h
index 79c8039ef83..2ccdac6a9aa 100644
--- a/src/tactic/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -24,13 +24,10 @@ Module Name:
#include"ref_util.h"
#include"float_decl_plugin.h"
#include"bv_decl_plugin.h"
-#include"model_converter.h"
#include"basic_simplifier_plugin.h"
typedef enum { BV_RM_TIES_TO_AWAY=0, BV_RM_TIES_TO_EVEN=1, BV_RM_TO_NEGATIVE=2, BV_RM_TO_POSITIVE=3, BV_RM_TO_ZERO=4 } BV_RM_VAL;
-class fpa2bv_model_converter;
-
struct func_decl_triple {
func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; }
func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp)
@@ -173,86 +170,4 @@ class fpa2bv_converter {
expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp);
};
-
-class fpa2bv_model_converter : public model_converter {
- ast_manager & m;
- obj_map m_const2bv;
- obj_map m_rm_const2bv;
- obj_map m_uf2bvuf;
- obj_map m_uf23bvuf;
-
-public:
- fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv,
- obj_map const & rm_const2bv,
- obj_map const & uf2bvuf,
- obj_map const & uf23bvuf) :
- m(m) {
- // Just create a copy?
- for (obj_map::iterator it = const2bv.begin();
- it != const2bv.end();
- it++)
- {
- m_const2bv.insert(it->m_key, it->m_value);
- m.inc_ref(it->m_key);
- m.inc_ref(it->m_value);
- }
- for (obj_map::iterator it = rm_const2bv.begin();
- it != rm_const2bv.end();
- it++)
- {
- m_rm_const2bv.insert(it->m_key, it->m_value);
- m.inc_ref(it->m_key);
- m.inc_ref(it->m_value);
- }
- for (obj_map::iterator it = uf2bvuf.begin();
- it != uf2bvuf.end();
- it++)
- {
- m_uf2bvuf.insert(it->m_key, it->m_value);
- m.inc_ref(it->m_key);
- m.inc_ref(it->m_value);
- }
- for (obj_map::iterator it = uf23bvuf.begin();
- it != uf23bvuf.end();
- it++)
- {
- m_uf23bvuf.insert(it->m_key, it->m_value);
- m.inc_ref(it->m_key);
- }
- }
-
- virtual ~fpa2bv_model_converter() {
- dec_ref_map_key_values(m, m_const2bv);
- dec_ref_map_key_values(m, m_rm_const2bv);
- }
-
- virtual void operator()(model_ref & md, unsigned goal_idx) {
- SASSERT(goal_idx == 0);
- model * new_model = alloc(model, m);
- obj_hashtable bits;
- convert(md.get(), new_model);
- md = new_model;
- }
-
- virtual void operator()(model_ref & md) {
- operator()(md, 0);
- }
-
- void display(std::ostream & out);
-
- virtual model_converter * translate(ast_translation & translator);
-
-protected:
- fpa2bv_model_converter(ast_manager & m) : m(m) { }
-
- void convert(model * bv_mdl, model * float_mdl);
-};
-
-
-model_converter * mk_fpa2bv_model_converter(ast_manager & m,
- obj_map const & const2bv,
- obj_map const & rm_const2bv,
- obj_map const & uf2bvuf,
- obj_map const & uf23bvuf);
-
#endif
diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
similarity index 100%
rename from src/tactic/fpa/fpa2bv_rewriter.h
rename to src/ast/fpa/fpa2bv_rewriter.h
diff --git a/src/duality/duality.h b/src/duality/duality.h
old mode 100755
new mode 100644
index aa147d93e5e..fc70ffa70a2
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -1,1317 +1,1321 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
- duality.h
-
-Abstract:
-
- main header for duality
-
-Author:
-
- Ken McMillan (kenmcmil)
-
-Revision History:
-
-
---*/
-
-#pragma once
-
-#include "duality_wrapper.h"
-#include
-#include