diff --git a/CMakeLists.txt b/CMakeLists.txt
index 69a0ca123..c11c272be 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -34,7 +34,7 @@ endif()
################################################################################
set(Z3_VERSION_MAJOR 4)
set(Z3_VERSION_MINOR 6)
-set(Z3_VERSION_PATCH 1)
+set(Z3_VERSION_PATCH 2)
set(Z3_VERSION_TWEAK 0)
set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
@@ -240,6 +240,9 @@ elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD")
message(STATUS "Platform: FreeBSD")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
+elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "NetBSD")
+ message(STATUS "Platform: NetBSD")
+ list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_")
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD")
message(STATUS "Platform: OpenBSD")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")
@@ -409,6 +412,20 @@ list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT})
################################################################################
include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake)
+################################################################################
+# If using Ninja, force color output for Clang (and gcc, disabled to check build).
+################################################################################
+if (UNIX AND CMAKE_GENERATOR STREQUAL "Ninja")
+ if (CMAKE_CXX_COMPILER_ID STREQUAL "Clang")
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics")
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fcolor-diagnostics")
+ endif()
+# if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU")
+# set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color")
+# set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fdiagnostics-color")
+# endif()
+endif()
+
################################################################################
# Option to control what type of library we build
################################################################################
@@ -434,7 +451,7 @@ else()
endif()
################################################################################
-# Postion independent code
+# Position independent code
################################################################################
# This is required because code built in the components will end up in a shared
# library. If not building a shared library ``-fPIC`` isn't needed and would add
diff --git a/configure b/configure
index 29408d3e7..807fba392 100755
--- a/configure
+++ b/configure
@@ -14,4 +14,4 @@ if ! $PYTHON -c "print('testing')" > /dev/null ; then
exit 1
fi
-$PYTHON scripts/mk_make.py $*
+$PYTHON scripts/mk_make.py "$@"
diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index b2736df4c..772440b42 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -1609,7 +1609,6 @@ public:
display_inference(out, "rewrite", "thm", p);
break;
case Z3_OP_PR_PULL_QUANT:
- case Z3_OP_PR_PULL_QUANT_STAR:
display_inference(out, "pull_quant", "thm", p);
break;
case Z3_OP_PR_PUSH_QUANT:
@@ -1669,12 +1668,6 @@ public:
case Z3_OP_PR_NNF_NEG:
display_inference(out, "nnf_neg", "sab", p);
break;
- case Z3_OP_PR_NNF_STAR:
- display_inference(out, "nnf", "sab", p);
- break;
- case Z3_OP_PR_CNF_STAR:
- display_inference(out, "cnf", "sab", p);
- break;
case Z3_OP_PR_SKOLEMIZE:
display_inference(out, "skolemize", "sab", p);
break;
@@ -1706,10 +1699,6 @@ public:
return display_hyp_inference(out, "modus_ponens", "thm", conclusion, hyp, hyp2);
}
case Z3_OP_PR_NNF_POS:
- case Z3_OP_PR_NNF_STAR:
- return display_hyp_inference(out, "nnf", "sab", conclusion, hyp);
- case Z3_OP_PR_CNF_STAR:
- return display_hyp_inference(out, "cnf", "sab", conclusion, hyp);
case Z3_OP_PR_SKOLEMIZE:
return display_hyp_inference(out, "skolemize", "sab", conclusion, hyp);
case Z3_OP_PR_TRANSITIVITY:
diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py
index d0502c19d..39d4e9439 100755
--- a/scripts/mk_consts_files.py
+++ b/scripts/mk_consts_files.py
@@ -72,7 +72,7 @@ def main(args):
if count == 0:
logging.info('No files generated. You need to specific an output directory'
- ' for the relevant langauge bindings')
+ ' for the relevant language bindings')
# TODO: Add support for other bindings
return 0
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 8f75e97ed..2f7402760 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -9,7 +9,7 @@ from mk_util import *
# Z3 Project definition
def init_project_def():
- set_version(4, 6, 1, 0)
+ set_version(4, 6, 2, 0)
add_lib('util', [])
add_lib('lp', ['util'], 'util/lp')
add_lib('polynomial', ['util'], 'math/polynomial')
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 03256125c..99de61703 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -69,6 +69,7 @@ IS_WINDOWS=False
IS_LINUX=False
IS_OSX=False
IS_FREEBSD=False
+IS_NETBSD=False
IS_OPENBSD=False
IS_CYGWIN=False
IS_CYGWIN_MINGW=False
@@ -141,6 +142,9 @@ def is_linux():
def is_freebsd():
return IS_FREEBSD
+def is_netbsd():
+ return IS_NETBSD
+
def is_openbsd():
return IS_OPENBSD
@@ -604,6 +608,8 @@ elif os.name == 'posix':
IS_LINUX=True
elif os.uname()[0] == 'FreeBSD':
IS_FREEBSD=True
+ elif os.uname()[0] == 'NetBSD':
+ IS_NETBSD=True
elif os.uname()[0] == 'OpenBSD':
IS_OPENBSD=True
elif os.uname()[0][:6] == 'CYGWIN':
@@ -889,8 +895,13 @@ def is_CXX_gpp():
return is_compiler(CXX, 'g++')
def is_clang_in_gpp_form(cc):
- version_string = check_output([cc, '--version']).encode('utf-8').decode('utf-8')
- return version_string.find('clang') != -1
+ str = check_output([cc, '--version'])
+ try:
+ version_string = str.encode('utf-8')
+ except:
+ version_string = str
+ clang = 'clang'.encode('utf-8')
+ return version_string.find(clang) != -1
def is_CXX_clangpp():
if is_compiler(CXX, 'g++'):
@@ -1240,7 +1251,7 @@ def get_so_ext():
sysname = os.uname()[0]
if sysname == 'Darwin':
return 'dylib'
- elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD':
+ elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'NetBSD' or sysname == 'OpenBSD':
return 'so'
elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
return 'dll'
@@ -1790,6 +1801,8 @@ class JavaDLLComponent(Component):
t = t.replace('PLATFORM', 'linux')
elif IS_FREEBSD:
t = t.replace('PLATFORM', 'freebsd')
+ elif IS_NETBSD:
+ t = t.replace('PLATFORM', 'netbsd')
elif IS_OPENBSD:
t = t.replace('PLATFORM', 'openbsd')
elif IS_CYGWIN:
@@ -2499,6 +2512,13 @@ def mk_config():
LDFLAGS = '%s -lrt' % LDFLAGS
SLIBFLAGS = '-shared'
SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
+ elif sysname == 'NetBSD':
+ CXXFLAGS = '%s -D_NETBSD_' % CXXFLAGS
+ OS_DEFINES = '-D_NETBSD_'
+ SO_EXT = '.so'
+ LDFLAGS = '%s -lrt' % LDFLAGS
+ SLIBFLAGS = '-shared'
+ SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
elif sysname == 'OpenBSD':
CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS
OS_DEFINES = '-D_OPENBSD_'
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 3f5a0fcf1..1f4a86903 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -919,7 +919,6 @@ extern "C" {
case PR_REWRITE: return Z3_OP_PR_REWRITE;
case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR;
case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT;
- case PR_PULL_QUANT_STAR: return Z3_OP_PR_PULL_QUANT_STAR;
case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT;
case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS;
case PR_DER: return Z3_OP_PR_DER;
@@ -936,9 +935,7 @@ extern "C" {
case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;
case PR_NNF_POS: return Z3_OP_PR_NNF_POS;
case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG;
- case PR_NNF_STAR: return Z3_OP_PR_NNF_STAR;
case PR_SKOLEMIZE: return Z3_OP_PR_SKOLEMIZE;
- case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR;
case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ;
case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA;
case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE;
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 49f6cfbf3..42467cb22 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -989,7 +989,7 @@ namespace z3 {
/**
\brief sequence and regular expression operations.
- + is overloaeded as sequence concatenation and regular expression union.
+ + is overloaded as sequence concatenation and regular expression union.
concat is overloaded to handle sequences and regular expressions
*/
expr extract(expr const& offset, expr const& length) const {
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index cbd6a1bac..b3b24a6d1 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2515,7 +2515,7 @@ namespace Microsoft.Z3
///
- /// Concatentate sequences.
+ /// Concatenate sequences.
///
public SeqExpr MkConcat(params SeqExpr[] t)
{
@@ -3597,7 +3597,7 @@ namespace Microsoft.Z3
}
///
- /// Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
+ /// Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty)
/// or trivially unsatisfiable (i.e., contains `false').
///
public Tactic FailIfNotDecided()
@@ -4656,7 +4656,7 @@ namespace Microsoft.Z3
/// Conversion of a floating-point term into a bit-vector.
///
///
- /// Produces a term that represents the conversion of the floating-poiunt term t into a
+ /// Produces a term that represents the conversion of the floating-point term t into a
/// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary,
/// the result will be rounded according to rounding mode rm.
///
@@ -4677,7 +4677,7 @@ namespace Microsoft.Z3
/// Conversion of a floating-point term into a real-numbered term.
///
///
- /// Produces a term that represents the conversion of the floating-poiunt term t into a
+ /// Produces a term that represents the conversion of the floating-point term t into a
/// real number. Note that this type of conversion will often result in non-linear
/// constraints over real terms.
///
@@ -4696,7 +4696,7 @@ namespace Microsoft.Z3
///
/// The size of the resulting bit-vector is automatically determined. Note that
/// IEEE 754-2008 allows multiple different representations of NaN. This conversion
- /// knows only one NaN and it will always produce the same bit-vector represenatation of
+ /// knows only one NaN and it will always produce the same bit-vector representation of
/// that NaN.
///
/// FloatingPoint term.
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index 0726f9d53..9310d1e7d 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -932,7 +932,7 @@ namespace Microsoft.Z3
/// Indicates whether the term is a proof by condensed transitivity of a relation
///
///
- /// Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
+ /// Condensed transitivity proof.
/// It combines several symmetry and transitivity proofs.
/// Example:
/// T1: (R a b)
@@ -1035,14 +1035,11 @@ namespace Microsoft.Z3
///
///
/// A proof for rewriting an expression t into an expression s.
- /// This proof object is used if the parameter PROOF_MODE is 1.
/// This proof object can have n antecedents.
/// The antecedents are proofs for equalities used as substitution rules.
- /// The object is also used in a few cases if the parameter PROOF_MODE is 2.
- /// The cases are:
+ /// The object is used in a few cases:
/// - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
/// - When converting bit-vectors to Booleans (BIT2BOOL=true)
- /// - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
///
public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
@@ -1054,15 +1051,6 @@ namespace Microsoft.Z3
///
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.
- ///
- ///
- /// A proof for (iff P Q) where Q is in prenex normal form.
- /// This proof object is only used if the parameter PROOF_MODE is 1.
- /// This proof object has no antecedents
- ///
- 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.
@@ -1304,28 +1292,6 @@ namespace Microsoft.Z3
///
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.
- ///
- ///
- /// A proof for (~ P Q) where Q is in negation normal form.
- ///
- /// 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 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.
- ///
- ///
- /// A proof for (~ P Q) where Q is in conjunctive normal form.
- /// 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 IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
-
///
/// Indicates whether the term is a proof for a Skolemization step
///
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 8720fd975..c45dce933 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -1978,7 +1978,7 @@ public class Context implements AutoCloseable {
}
/**
- * Concatentate sequences.
+ * Concatenate sequences.
*/
public SeqExpr mkConcat(SeqExpr... t)
{
@@ -2782,7 +2782,7 @@ public class Context implements AutoCloseable {
}
/**
- * Create a tactic that fails if the goal is not triviall satisfiable (i.e.,
+ * Create a tactic that fails if the goal is not trivially satisfiable (i.e.,
* empty) or trivially unsatisfiable (i.e., contains `false').
**/
public Tactic failIfNotDecided()
@@ -3770,7 +3770,7 @@ public class Context implements AutoCloseable {
* @param sz Size of the resulting bit-vector.
* @param signed Indicates whether the result is a signed or unsigned bit-vector.
* Remarks:
- * Produces a term that represents the conversion of the floating-poiunt term t into a
+ * Produces a term that represents the conversion of the floating-point term t into a
* bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary,
* the result will be rounded according to rounding mode rm.
* @throws Z3Exception
@@ -3787,7 +3787,7 @@ public class Context implements AutoCloseable {
* Conversion of a floating-point term into a real-numbered term.
* @param t FloatingPoint term
* Remarks:
- * Produces a term that represents the conversion of the floating-poiunt term t into a
+ * Produces a term that represents the conversion of the floating-point term t into a
* real number. Note that this type of conversion will often result in non-linear
* constraints over real terms.
* @throws Z3Exception
@@ -3803,7 +3803,7 @@ public class Context implements AutoCloseable {
* Remarks:
* The size of the resulting bit-vector is automatically determined. Note that
* IEEE 754-2008 allows multiple different representations of NaN. This conversion
- * knows only one NaN and it will always produce the same bit-vector represenatation of
+ * knows only one NaN and it will always produce the same bit-vector representation of
* that NaN.
* @throws Z3Exception
**/
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 7b20b7993..db5c33e79 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -1398,8 +1398,7 @@ public class Expr extends AST
/**
* Indicates whether the term is a proof by condensed transitivity of a
* relation
- * Remarks: Condensed transitivity proof. This proof object is
- * only used if the parameter PROOF_MODE is 1. It combines several symmetry
+ * Remarks: Condensed transitivity proof. It combines several symmetry
* and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d)
* [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.
*
@@ -1506,14 +1505,11 @@ public class Expr extends AST
/**
* Indicates whether the term is a proof by rewriting
* Remarks: A proof for
- * rewriting an expression t into an expression s. This proof object is used
- * if the parameter PROOF_MODE is 1. This proof object can have n
+ * rewriting an expression t into an expression s. This proof object can have n
* antecedents. The antecedents are proofs for equalities used as
- * substitution rules. The object is also used in a few cases if the
- * parameter PROOF_MODE is 2. The cases are: - When applying contextual
+ * substitution rules. The object is used in a few cases . The cases are: - When applying contextual
* simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to
- * Booleans (BIT2BOOL=true) - When pulling ite expression up
- * (PULL_CHEAP_ITE_TREES=true)
+ * Booleans (BIT2BOOL=true)
* @throws Z3Exception on error
* @return a boolean
**/
@@ -1534,17 +1530,6 @@ public class Expr extends AST
return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
}
- /**
- * Indicates whether the term is a proof for pulling quantifiers out.
- *
- * Remarks: A proof for (iff P Q) where Q is in prenex normal form. This * proof object is only used if the parameter PROOF_MODE is 1. This proof * object has no antecedents
- * @throws Z3Exception on error
- * @return a boolean
- **/
- public boolean isProofPullQuantStar()
- {
- return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR;
- }
/**
* Indicates whether the term is a proof for pushing quantifiers in.
@@ -1804,38 +1789,6 @@ public class Expr extends AST
return isApp() && getFuncDecl().getDeclKind() == 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.
- * Remarks: A proof for (~ P Q) where Q is in negation normal
- * form.
- *
- * 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.
- * @throws Z3Exception on error
- * @return a boolean
- **/
- public boolean isProofNNFStar()
- {
- return isApp() && getFuncDecl().getDeclKind() == 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.
- * Remarks: A proof for (~ P Q) where Q is in
- * conjunctive normal form. 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.
- * @throws Z3Exception on error
- * @return a boolean
- **/
- public boolean isProofCNFStar()
- {
- return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR;
- }
/**
* Indicates whether the term is a proof for a Skolemization step
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 120b0ddfd..5766c79f9 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1402,7 +1402,6 @@ struct
let is_rewrite (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE)
let is_rewrite_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE_STAR)
let is_pull_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT)
- let is_pull_quant_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT_STAR)
let is_push_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PUSH_QUANT)
let is_elim_unused_vars (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_ELIM_UNUSED_VARS)
let is_der (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_DER)
@@ -1419,8 +1418,6 @@ struct
let is_iff_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_IFF_OEQ)
let is_nnf_pos (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_POS)
let is_nnf_neg (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_NEG)
- let is_nnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_STAR)
- let is_cnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_CNF_STAR)
let is_skolemize (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_SKOLEMIZE)
let is_modus_ponens_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_MODUS_PONENS_OEQ)
let is_theory_lemma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_TH_LEMMA)
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 1cfb10179..e68d7280d 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -2428,7 +2428,7 @@ def is_rational_value(a):
return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
def is_algebraic_value(a):
- """Return `True` if `a` is an algerbraic value of sort Real.
+ """Return `True` if `a` is an algebraic value of sort Real.
>>> is_algebraic_value(RealVal("3/5"))
False
@@ -4437,7 +4437,7 @@ class Datatype:
"""Declare constructor named `name` with the given accessors `args`.
Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared.
- In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
+ In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
declares the constructor named `cons` that builds a new List using an integer and a List.
It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create
@@ -4457,7 +4457,7 @@ class Datatype:
return "Datatype(%s, %s)" % (self.name, self.constructors)
def create(self):
- """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`.
+ """Create a Z3 datatype based on the constructors declared using the method `declare()`.
The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
@@ -8874,7 +8874,7 @@ class FPNumRef(FPRef):
def isSubnormal(self):
return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
- """Indicates whether the numeral is postitive."""
+ """Indicates whether the numeral is positive."""
def isPositive(self):
return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
@@ -9670,7 +9670,7 @@ def fpToIEEEBV(x, ctx=None):
The size of the resulting bit-vector is automatically determined.
Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
- knows only one NaN and it will always produce the same bit-vector represenatation of
+ knows only one NaN and it will always produce the same bit-vector representation of
that NaN.
>>> x = FP('x', FPSort(8, 24))
@@ -9845,7 +9845,7 @@ def Empty(s):
raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
def Full(s):
- """Create the regular expression that accepts the universal langauge
+ """Create the regular expression that accepts the universal language
>>> e = Full(ReSort(SeqSort(IntSort())))
>>> print(e)
re.all
diff --git a/src/api/z3.h b/src/api/z3.h
index 99929f33b..b29f1d6ba 100644
--- a/src/api/z3.h
+++ b/src/api/z3.h
@@ -21,7 +21,8 @@ Notes:
#ifndef Z3_H_
#define Z3_H_
-#include
+#include
+#include
#include "z3_macros.h"
#include "z3_api.h"
#include "z3_ast_containers.h"
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 500533e91..88d6aa1cf 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -459,7 +459,7 @@ typedef enum
[trans T1 T2]: (R t u)
}
- - Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
+ - Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof.
It combines several symmetry and transitivity proofs.
Example:
@@ -539,21 +539,14 @@ typedef enum
}
- Z3_OP_PR_REWRITE_STAR: A proof for rewriting an expression t into an expression s.
- This proof object is used if the parameter PROOF_MODE is 1.
This proof object can have n antecedents.
The antecedents are proofs for equalities used as substitution rules.
- The object is also used in a few cases if the parameter PROOF_MODE is 2.
- The cases are:
+ The proof rule is used in a few cases. The cases are:
- When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
- When converting bit-vectors to Booleans (BIT2BOOL=true)
- - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
- Z3_OP_PR_PULL_QUANT: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
- - Z3_OP_PR_PULL_QUANT_STAR: A proof for (iff P Q) where Q is in prenex normal form.
- This proof object is only used if the parameter PROOF_MODE is 1.
- This proof object has no antecedents.
-
- Z3_OP_PR_PUSH_QUANT: A proof for:
\nicebox{
@@ -726,15 +719,6 @@ typedef enum
[nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
(and (or r_1 r_2) (or r_1' r_2')))
}
- - Z3_OP_PR_NNF_STAR: A proof for (~ P Q) where Q is in negation normal form.
-
- 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.
-
- - Z3_OP_PR_CNF_STAR: A proof for (~ P Q) where Q is in conjunctive normal form.
- 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.
- Z3_OP_PR_SKOLEMIZE: Proof for:
@@ -1142,7 +1126,6 @@ typedef enum {
Z3_OP_PR_REWRITE,
Z3_OP_PR_REWRITE_STAR,
Z3_OP_PR_PULL_QUANT,
- Z3_OP_PR_PULL_QUANT_STAR,
Z3_OP_PR_PUSH_QUANT,
Z3_OP_PR_ELIM_UNUSED_VARS,
Z3_OP_PR_DER,
@@ -1159,8 +1142,6 @@ typedef enum {
Z3_OP_PR_IFF_OEQ,
Z3_OP_PR_NNF_POS,
Z3_OP_PR_NNF_NEG,
- Z3_OP_PR_NNF_STAR,
- Z3_OP_PR_CNF_STAR,
Z3_OP_PR_SKOLEMIZE,
Z3_OP_PR_MODUS_PONENS_OEQ,
Z3_OP_PR_TH_LEMMA,
@@ -1477,7 +1458,6 @@ extern "C" {
/*@{*/
/**
- \deprecated
\brief Create a configuration object for the Z3 context object.
Configurations are created in order to assign parameters prior to creating
@@ -1510,7 +1490,6 @@ extern "C" {
Z3_config Z3_API Z3_mk_config(void);
/**
- \deprecated
\brief Delete the given configuration object.
\sa Z3_mk_config
@@ -1520,7 +1499,6 @@ extern "C" {
void Z3_API Z3_del_config(Z3_config c);
/**
- \deprecated
\brief Set a configuration parameter.
The following parameters can be set for
@@ -1537,7 +1515,6 @@ extern "C" {
/*@{*/
/**
- \deprecated
\brief Create a context using the given configuration.
After a context is created, the configuration cannot be changed,
@@ -1617,7 +1594,6 @@ extern "C" {
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a);
/**
- \deprecated
\brief Set a value of a context parameter.
\sa Z3_global_param_set
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index 358a3c619..7d237c6e7 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -756,7 +756,7 @@ extern "C" {
/**
\brief Conversion of a floating-point term into an unsigned bit-vector.
- Produces a term that represents the conversion of the floating-poiunt term t into a
+ Produces a term that represents the conversion of the floating-point term t into a
bit-vector term of size sz in unsigned 2's complement format. If necessary, the result
will be rounded according to rounding mode rm.
@@ -772,7 +772,7 @@ extern "C" {
/**
\brief Conversion of a floating-point term into a signed bit-vector.
- Produces a term that represents the conversion of the floating-poiunt term t into a
+ Produces a term that represents the conversion of the floating-point term t into a
bit-vector term of size sz in signed 2's complement format. If necessary, the result
will be rounded according to rounding mode rm.
@@ -788,7 +788,7 @@ extern "C" {
/**
\brief Conversion of a floating-point term into a real-numbered term.
- Produces a term that represents the conversion of the floating-poiunt term t into a
+ Produces a term that represents the conversion of the floating-point term t into a
real number. Note that this type of conversion will often result in non-linear
constraints over real terms.
@@ -1011,7 +1011,7 @@ extern "C" {
determined.
Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
- knows only one NaN and it will always produce the same bit-vector represenatation of
+ knows only one NaN and it will always produce the same bit-vector representation of
that NaN.
def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))
diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h
index bcee0e22d..2441d4339 100644
--- a/src/api/z3_interp.h
+++ b/src/api/z3_interp.h
@@ -98,7 +98,7 @@ extern "C" {
Interpolant may not necessarily be computable from all
proofs. To be sure an interpolant can be computed, the proof
- must be generated by an SMT solver for which interpoaltion is
+ must be generated by an SMT solver for which interpolation is
supported, and the premises must be expressed using only
theories and operators for which interpolation is supported.
@@ -199,7 +199,7 @@ extern "C" {
(implies (and c1 ... cn f) v)
where c1 .. cn are the children of v (which must precede v in the file)
- and f is the formula assiciated to node v. The last formula in the
+ and f is the formula associated to node v. The last formula in the
file is the root vertex, and is represented by the predicate "false".
A solution to a tree interpolation problem can be thought of as a
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index c27651fca..7e143e1a3 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -663,7 +663,6 @@ basic_decl_plugin::basic_decl_plugin():
m_not_or_elim_decl(nullptr),
m_rewrite_decl(nullptr),
m_pull_quant_decl(nullptr),
- m_pull_quant_star_decl(nullptr),
m_push_quant_decl(nullptr),
m_elim_unused_vars_decl(nullptr),
m_der_decl(nullptr),
@@ -827,7 +826,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
case PR_REWRITE: return mk_proof_decl("rewrite", k, 0, m_rewrite_decl);
case PR_REWRITE_STAR: return mk_proof_decl("rewrite*", k, num_parents, m_rewrite_star_decls);
case PR_PULL_QUANT: return mk_proof_decl("pull-quant", k, 0, m_pull_quant_decl);
- case PR_PULL_QUANT_STAR: return mk_proof_decl("pull-quant*", k, 0, m_pull_quant_star_decl);
case PR_PUSH_QUANT: return mk_proof_decl("push-quant", k, 0, m_push_quant_decl);
case PR_ELIM_UNUSED_VARS: return mk_proof_decl("elim-unused", k, 0, m_elim_unused_vars_decl);
case PR_DER: return mk_proof_decl("der", k, 0, m_der_decl);
@@ -844,8 +842,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
case PR_IFF_OEQ: return mk_proof_decl("iff~", k, 1, m_iff_oeq_decl);
case PR_NNF_POS: return mk_proof_decl("nnf-pos", k, num_parents, m_nnf_pos_decls);
case PR_NNF_NEG: return mk_proof_decl("nnf-neg", k, num_parents, m_nnf_neg_decls);
- case PR_NNF_STAR: return mk_proof_decl("nnf*", k, num_parents, m_nnf_star_decls);
- case PR_CNF_STAR: return mk_proof_decl("cnf*", k, num_parents, m_cnf_star_decls);
case PR_SKOLEMIZE: return mk_proof_decl("sk", k, 0, m_skolemize_decl);
case PR_MODUS_PONENS_OEQ: return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl);
case PR_TH_LEMMA: return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls);
@@ -949,7 +945,6 @@ void basic_decl_plugin::finalize() {
DEC_REF(m_not_or_elim_decl);
DEC_REF(m_rewrite_decl);
DEC_REF(m_pull_quant_decl);
- DEC_REF(m_pull_quant_star_decl);
DEC_REF(m_push_quant_decl);
DEC_REF(m_elim_unused_vars_decl);
DEC_REF(m_der_decl);
@@ -975,8 +970,6 @@ void basic_decl_plugin::finalize() {
DEC_ARRAY_REF(m_apply_def_decls);
DEC_ARRAY_REF(m_nnf_pos_decls);
DEC_ARRAY_REF(m_nnf_neg_decls);
- DEC_ARRAY_REF(m_nnf_star_decls);
- DEC_ARRAY_REF(m_cnf_star_decls);
DEC_ARRAY_REF(m_th_lemma_decls);
DEC_REF(m_hyper_res_decl0);
@@ -1536,34 +1529,35 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
// assigned in the order that they are created, this can result in differing
// family ids. To avoid this, we first assign all family ids and only then inherit plugins.
for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
- symbol fid_name = from.get_family_name(fid);
- if (!m_family_manager.has_family(fid)) {
- family_id new_fid = mk_family_id(fid_name);
- (void)new_fid;
- TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
- }
+ symbol fid_name = from.get_family_name(fid);
+ if (!m_family_manager.has_family(fid)) {
+ family_id new_fid = mk_family_id(fid_name);
+ (void)new_fid;
+ TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
+ }
}
for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
- SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
- SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
- symbol fid_name = from.get_family_name(fid);
- TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
- << ", target has_family: " << m_family_manager.has_family(fid) << "\n";
- if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
- TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
- SASSERT(fid == get_family_id(fid_name));
- if (from.has_plugin(fid) && !has_plugin(fid)) {
- decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();
- register_plugin(fid, new_p);
- SASSERT(new_p->get_family_id() == fid);
- SASSERT(has_plugin(fid));
- }
- if (from.has_plugin(fid)) {
- get_plugin(fid)->inherit(from.get_plugin(fid), trans);
- }
- SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
- SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
- SASSERT(!from.has_plugin(fid) || has_plugin(fid));
+ SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
+ SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
+ symbol fid_name = from.get_family_name(fid);
+ (void)fid_name;
+ TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
+ << ", target has_family: " << m_family_manager.has_family(fid) << "\n";
+ if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
+ TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
+ SASSERT(fid == get_family_id(fid_name));
+ if (from.has_plugin(fid) && !has_plugin(fid)) {
+ decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();
+ register_plugin(fid, new_p);
+ SASSERT(new_p->get_family_id() == fid);
+ SASSERT(has_plugin(fid));
+ }
+ if (from.has_plugin(fid)) {
+ get_plugin(fid)->inherit(from.get_plugin(fid), trans);
+ }
+ SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
+ SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
+ SASSERT(!from.has_plugin(fid) || has_plugin(fid));
}
}
@@ -2843,12 +2837,6 @@ proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
}
-proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
- if (proofs_disabled())
- return nullptr;
- return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
-}
-
proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
if (proofs_disabled())
return nullptr;
@@ -3093,15 +3081,6 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
return mk_app(m_basic_family_id, PR_NNF_NEG, args.size(), args.c_ptr());
}
-proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
- if (proofs_disabled())
- return nullptr;
- ptr_buffer args;
- args.append(num_proofs, (expr**) proofs);
- args.push_back(mk_oeq(s, t));
- return mk_app(m_basic_family_id, PR_NNF_STAR, args.size(), args.c_ptr());
-}
-
proof * ast_manager::mk_skolemization(expr * q, expr * e) {
if (proofs_disabled())
return nullptr;
@@ -3110,15 +3089,6 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) {
return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e));
}
-proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
- if (proofs_disabled())
- return nullptr;
- ptr_buffer args;
- args.append(num_proofs, (expr**) proofs);
- args.push_back(mk_oeq(s, t));
- return mk_app(m_basic_family_id, PR_CNF_STAR, args.size(), args.c_ptr());
-}
-
proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
if (proofs_disabled())
return nullptr;
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 55fea1b69..68e02d791 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1042,11 +1042,11 @@ enum basic_op_kind {
PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
- PR_PULL_QUANT_STAR, PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
+ PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM,
- PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR,
+ PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_SKOLEMIZE,
PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR
};
@@ -1080,7 +1080,6 @@ protected:
func_decl * m_not_or_elim_decl;
func_decl * m_rewrite_decl;
func_decl * m_pull_quant_decl;
- func_decl * m_pull_quant_star_decl;
func_decl * m_push_quant_decl;
func_decl * m_elim_unused_vars_decl;
func_decl * m_der_decl;
@@ -1106,8 +1105,6 @@ protected:
ptr_vector m_apply_def_decls;
ptr_vector m_nnf_pos_decls;
ptr_vector m_nnf_neg_decls;
- ptr_vector m_nnf_star_decls;
- ptr_vector m_cnf_star_decls;
ptr_vector m_th_lemma_decls;
func_decl * m_hyper_res_decl0;
@@ -2182,7 +2179,6 @@ public:
proof * mk_oeq_rewrite(expr * s, expr * t);
proof * mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_pull_quant(expr * e, quantifier * q);
- proof * mk_pull_quant_star(expr * e, quantifier * q);
proof * mk_push_quant(quantifier * q, expr * e);
proof * mk_elim_unused_vars(quantifier * q, expr * r);
proof * mk_der(quantifier * q, expr * r);
@@ -2201,9 +2197,8 @@ public:
proof * mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
- proof * mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_skolemization(expr * q, expr * e);
- proof * mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
+
proof * mk_and_elim(proof * p, unsigned i);
proof * mk_not_or_elim(proof * p, unsigned i);
diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp
index 37785e072..23c9ebe51 100644
--- a/src/ast/ast_pp_util.cpp
+++ b/src/ast/ast_pp_util.cpp
@@ -46,13 +46,18 @@ void ast_pp_util::display_decls(std::ostream& out) {
n = coll.get_num_decls();
for (unsigned i = 0; i < n; ++i) {
func_decl* f = coll.get_func_decls()[i];
- if (f->get_family_id() == null_family_id) {
+ if (f->get_family_id() == null_family_id && !m_removed.contains(f)) {
ast_smt2_pp(out, f, env);
out << "\n";
}
}
}
+void ast_pp_util::remove_decl(func_decl* f) {
+ m_removed.insert(f);
+}
+
+
void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) {
if (neat) {
smt2_pp_environment_dbg env(m);
diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h
index 964a862a2..1b2686511 100644
--- a/src/ast/ast_pp_util.h
+++ b/src/ast/ast_pp_util.h
@@ -20,9 +20,11 @@ Revision History:
#define AST_PP_UTIL_H_
#include "ast/decl_collector.h"
+#include "util/obj_hashtable.h"
class ast_pp_util {
ast_manager& m;
+ obj_hashtable m_removed;
public:
decl_collector coll;
@@ -35,6 +37,8 @@ class ast_pp_util {
void collect(expr_ref_vector const& es);
+ void remove_decl(func_decl* f);
+
void display_decls(std::ostream& out);
void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true);
diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp
index 9ba52a402..0e16abd11 100644
--- a/src/ast/proofs/proof_checker.cpp
+++ b/src/ast/proofs/proof_checker.cpp
@@ -440,16 +440,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m););
return false;
}
- case PR_PULL_QUANT_STAR: {
- if (match_proof(p) &&
- match_fact(p, fact) &&
- match_iff(fact.get(), t1, t2)) {
- // TBD: check the enchilada.
- return true;
- }
- IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m););
- return false;
- }
case PR_PUSH_QUANT: {
if (match_proof(p) &&
match_fact(p, fact) &&
@@ -730,10 +720,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
// TBD:
return true;
}
- case PR_NNF_STAR: {
- // TBD:
- return true;
- }
case PR_SKOLEMIZE: {
// (exists ?x (p ?x y)) -> (p (sk y) y)
// (not (forall ?x (p ?x y))) -> (not (p (sk y) y))
@@ -755,19 +741,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
UNREACHABLE();
return false;
}
- case PR_CNF_STAR: {
- for (unsigned i = 0; i < proofs.size(); ++i) {
- if (match_op(proofs[i].get(), PR_DEF_INTRO, terms)) {
- // ok
- }
- else {
- UNREACHABLE();
- return false;
- }
- }
- // coarse grain CNF conversion.
- return true;
- }
case PR_MODUS_PONENS_OEQ: {
if (match_fact(p, fact) &&
match_proof(p, p0, p1) &&
@@ -922,7 +895,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
}
}
-bool proof_checker::match_fact(proof* p, expr_ref& fact) {
+bool proof_checker::match_fact(proof const* p, expr_ref& fact) const {
if (m.is_proof(p) &&
m.has_fact(p)) {
fact = m.get_fact(p);
@@ -938,13 +911,13 @@ void proof_checker::add_premise(proof* p) {
}
}
-bool proof_checker::match_proof(proof* p) {
+bool proof_checker::match_proof(proof const* p) const {
return
m.is_proof(p) &&
m.get_num_parents(p) == 0;
}
-bool proof_checker::match_proof(proof* p, proof_ref& p0) {
+bool proof_checker::match_proof(proof const* p, proof_ref& p0) const {
if (m.is_proof(p) &&
m.get_num_parents(p) == 1) {
p0 = m.get_parent(p, 0);
@@ -953,7 +926,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0) {
return false;
}
-bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
+bool proof_checker::match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const {
if (m.is_proof(p) &&
m.get_num_parents(p) == 2) {
p0 = m.get_parent(p, 0);
@@ -963,7 +936,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
return false;
}
-bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
+bool proof_checker::match_proof(proof const* p, proof_ref_vector& parents) const {
if (m.is_proof(p)) {
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
parents.push_back(m.get_parent(p, i));
@@ -974,7 +947,7 @@ bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
}
-bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const {
if (e->get_kind() == AST_APP &&
to_app(e)->get_num_args() == 2) {
d = to_app(e)->get_decl();
@@ -986,7 +959,7 @@ bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_r
}
-bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms) {
+bool proof_checker::match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const {
if (e->get_kind() == AST_APP) {
d = to_app(e)->get_decl();
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
@@ -997,9 +970,9 @@ bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms)
return false;
}
-bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) {
+bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) const {
if (is_quantifier(e)) {
- quantifier* q = to_quantifier(e);
+ quantifier const* q = to_quantifier(e);
is_univ = q->is_forall();
body = q->get_expr();
for (unsigned i = 0; i < q->get_num_decls(); ++i) {
@@ -1010,7 +983,7 @@ bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& so
return false;
}
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const {
if (e->get_kind() == AST_APP &&
to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k &&
@@ -1022,7 +995,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
return false;
}
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const {
if (e->get_kind() == AST_APP &&
to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k) {
@@ -1035,7 +1008,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
}
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t) const {
if (e->get_kind() == AST_APP &&
to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k &&
@@ -1046,39 +1019,39 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
return false;
}
-bool proof_checker::match_not(expr* e, expr_ref& t) {
+bool proof_checker::match_not(expr const* e, expr_ref& t) const {
return match_op(e, OP_NOT, t);
}
-bool proof_checker::match_or(expr* e, expr_ref_vector& terms) {
+bool proof_checker::match_or(expr const* e, expr_ref_vector& terms) const {
return match_op(e, OP_OR, terms);
}
-bool proof_checker::match_and(expr* e, expr_ref_vector& terms) {
+bool proof_checker::match_and(expr const* e, expr_ref_vector& terms) const {
return match_op(e, OP_AND, terms);
}
-bool proof_checker::match_iff(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_IFF, t1, t2);
}
-bool proof_checker::match_equiv(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_equiv(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_oeq(e, t1, t2) || match_eq(e, t1, t2);
}
-bool proof_checker::match_implies(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_IMPLIES, t1, t2);
}
-bool proof_checker::match_eq(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_EQ, t1, t2) || match_iff(e, t1, t2);
}
-bool proof_checker::match_oeq(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_OEQ, t1, t2);
}
-bool proof_checker::match_negated(expr* a, expr* b) {
+bool proof_checker::match_negated(expr const* a, expr* b) const {
expr_ref t(m);
return
(match_not(a, t) && t.get() == b) ||
@@ -1186,14 +1159,14 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
}
-bool proof_checker::match_nil(expr* e) const {
+bool proof_checker::match_nil(expr const* e) const {
return
is_app(e) &&
to_app(e)->get_family_id() == m_hyp_fid &&
to_app(e)->get_decl_kind() == OP_NIL;
}
-bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
+bool proof_checker::match_cons(expr const* e, expr_ref& a, expr_ref& b) const {
if (is_app(e) &&
to_app(e)->get_family_id() == m_hyp_fid &&
to_app(e)->get_decl_kind() == OP_CONS) {
@@ -1205,7 +1178,7 @@ bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
}
-bool proof_checker::match_atom(expr* e, expr_ref& a) const {
+bool proof_checker::match_atom(expr const* e, expr_ref& a) const {
if (is_app(e) &&
to_app(e)->get_family_id() == m_hyp_fid &&
to_app(e)->get_decl_kind() == OP_ATOM) {
@@ -1227,7 +1200,7 @@ expr* proof_checker::mk_nil() {
return m_nil.get();
}
-bool proof_checker::is_hypothesis(proof* p) const {
+bool proof_checker::is_hypothesis(proof const* p) const {
return
m.is_proof(p) &&
p->get_decl_kind() == PR_HYPOTHESIS;
@@ -1253,7 +1226,7 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
}
}
-void proof_checker::dump_proof(proof * pr) {
+void proof_checker::dump_proof(proof const* pr) {
if (!m_dump_lemmas)
return;
SASSERT(m.has_fact(pr));
diff --git a/src/ast/proofs/proof_checker.h b/src/ast/proofs/proof_checker.h
index ccb815c61..ac0e31dbd 100644
--- a/src/ast/proofs/proof_checker.h
+++ b/src/ast/proofs/proof_checker.h
@@ -77,39 +77,39 @@ private:
bool check1_spc(proof* p, expr_ref_vector& side_conditions);
bool check_arith_proof(proof* p);
bool check_arith_literal(bool is_pos, app* lit, rational const& coeff, expr_ref& sum, bool& is_strict);
- bool match_fact(proof* p, expr_ref& fact);
+ bool match_fact(proof const* p, expr_ref& fact) const;
void add_premise(proof* p);
- bool match_proof(proof* p);
- bool match_proof(proof* p, proof_ref& p0);
- bool match_proof(proof* p, proof_ref& p0, proof_ref& p1);
- bool match_proof(proof* p, proof_ref_vector& parents);
- bool match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2);
- bool match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2);
- bool match_op(expr* e, decl_kind k, expr_ref& t);
- bool match_op(expr* e, decl_kind k, expr_ref_vector& terms);
- bool match_iff(expr* e, expr_ref& t1, expr_ref& t2);
- bool match_implies(expr* e, expr_ref& t1, expr_ref& t2);
- bool match_eq(expr* e, expr_ref& t1, expr_ref& t2);
- bool match_oeq(expr* e, expr_ref& t1, expr_ref& t2);
- bool match_not(expr* e, expr_ref& t);
- bool match_or(expr* e, expr_ref_vector& terms);
- bool match_and(expr* e, expr_ref_vector& terms);
- bool match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms);
- bool match_quantifier(expr*, bool& is_univ, sort_ref_vector&, expr_ref& body);
- bool match_negated(expr* a, expr* b);
- bool match_equiv(expr* a, expr_ref& t1, expr_ref& t2);
+ bool match_proof(proof const* p) const;
+ bool match_proof(proof const* p, proof_ref& p0) const;
+ bool match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const;
+ bool match_proof(proof const* p, proof_ref_vector& parents) const;
+ bool match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const;
+ bool match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const;
+ bool match_op(expr const* e, decl_kind k, expr_ref& t) const;
+ bool match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const;
+ bool match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const;
+ bool match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const;
+ bool match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const;
+ bool match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const;
+ bool match_not(expr const* e, expr_ref& t) const;
+ bool match_or(expr const* e, expr_ref_vector& terms) const;
+ bool match_and(expr const* e, expr_ref_vector& terms) const;
+ bool match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const;
+ bool match_quantifier(expr const*, bool& is_univ, sort_ref_vector&, expr_ref& body) const;
+ bool match_negated(expr const* a, expr* b) const;
+ bool match_equiv(expr const* a, expr_ref& t1, expr_ref& t2) const;
void get_ors(expr* e, expr_ref_vector& ors);
void get_hypotheses(proof* p, expr_ref_vector& ante);
- bool match_nil(expr* e) const;
- bool match_cons(expr* e, expr_ref& a, expr_ref& b) const;
- bool match_atom(expr* e, expr_ref& a) const;
+ bool match_nil(expr const* e) const;
+ bool match_cons(expr const* e, expr_ref& a, expr_ref& b) const;
+ bool match_atom(expr const* e, expr_ref& a) const;
expr* mk_nil();
expr* mk_cons(expr* a, expr* b);
expr* mk_atom(expr* e);
- bool is_hypothesis(proof* p) const;
+ bool is_hypothesis(proof const* p) const;
expr* mk_hyp(unsigned num_hyps, expr * const * hyps);
- void dump_proof(proof * pr);
+ void dump_proof(proof const* pr);
void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent);
void set_false(expr_ref& e, unsigned idx, expr_ref& lit);
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 658fb2e05..878f4ef4c 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -358,7 +358,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) {
if (ProofGen) {
NOT_IMPLEMENTED_YET();
// We do not support the use of bindings in proof generation mode.
- // Thus we have to apply the subsitution here, and
+ // Thus we have to apply the substitution here, and
// beta_reducer subst(m());
// subst.set_bindings(new_num_args, new_args);
// expr_ref r2(m());
diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp
index cfea511ad..511342819 100644
--- a/src/interp/iz3checker.cpp
+++ b/src/interp/iz3checker.cpp
@@ -43,7 +43,7 @@ struct iz3checker : iz3base {
/* HACK: for tree interpolants, we assume that uninterpreted functions
are global. This is because in the current state of the tree interpolation
code, symbols that appear in sibling sub-trees have to be global, and
- we have no way to eliminate such function symbols. When tree interpoaltion is
+ we have no way to eliminate such function symbols. When tree interpolation is
fixed, we can tree function symbols the same as constant symbols. */
bool is_tree;
diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp
index f7cc16de2..cc2442981 100644
--- a/src/math/polynomial/upolynomial.cpp
+++ b/src/math/polynomial/upolynomial.cpp
@@ -781,17 +781,15 @@ namespace upolynomial {
set(q.size(), q.c_ptr(), C);
m().set(bound, p);
}
+ else if (q.size() < C.size() || m().m().is_even(p) || m().m().is_even(bound)) {
+ // discard accumulated image, it was affected by unlucky primes
+ TRACE("mgcd", tout << "discarding image\n";);
+ set(q.size(), q.c_ptr(), C);
+ m().set(bound, p);
+ }
else {
- if (q.size() < C.size()) {
- // discard accumulated image, it was affected by unlucky primes
- TRACE("mgcd", tout << "discarding image\n";);
- set(q.size(), q.c_ptr(), C);
- m().set(bound, p);
- }
- else {
- CRA_combine_images(q, p, C, bound);
- TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";);
- }
+ CRA_combine_images(q, p, C, bound);
+ TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";);
}
numeral_vector & candidate = q;
get_primitive(C, candidate);
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 47d7cc357..521cf0dc9 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -1106,6 +1106,16 @@ namespace datalog {
names.push_back(m_rule_names[i]);
}
}
+
+ static std::ostream& display_symbol(std::ostream& out, symbol const& nm) {
+ if (is_smt2_quoted_symbol(nm)) {
+ out << mk_smt2_quoted_symbol(nm);
+ }
+ else {
+ out << nm;
+ }
+ return out;
+ }
void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) {
ast_manager& m = get_manager();
@@ -1148,13 +1158,13 @@ namespace datalog {
if (!use_fixedpoint_extensions) {
out << "(set-logic HORN)\n";
}
+ for (func_decl * f : rels)
+ visitor.remove_decl(f);
visitor.display_decls(out);
- func_decl_set::iterator it = rels.begin(), end = rels.end();
- for (; it != end; ++it) {
- func_decl* f = *it;
+
+ for (func_decl * f : rels)
display_rel_decl(out, f);
- }
if (use_fixedpoint_extensions && do_declare_vars) {
declare_vars(rules, fresh_names, out);
@@ -1185,13 +1195,7 @@ namespace datalog {
nm = symbol(s.str().c_str());
}
fresh_names.add(nm);
- if (is_smt2_quoted_symbol(nm)) {
- out << mk_smt2_quoted_symbol(nm);
- }
- else {
- out << nm;
- }
- out << ")";
+ display_symbol(out, nm) << ")";
}
out << ")\n";
}
@@ -1219,7 +1223,8 @@ namespace datalog {
PP(qfn);
out << ")\n";
}
- out << "(query " << fn->get_name() << ")\n";
+ out << "(query ";
+ display_symbol(out, fn->get_name()) << ")\n";
}
}
else {
@@ -1238,7 +1243,8 @@ namespace datalog {
void context::display_rel_decl(std::ostream& out, func_decl* f) {
smt2_pp_environment_dbg env(m);
- out << "(declare-rel " << f->get_name() << " (";
+ out << "(declare-rel ";
+ display_symbol(out, f->get_name()) << " (";
for (unsigned i = 0; i < f->get_arity(); ++i) {
ast_smt2_pp(out, f->get_domain(i), env);
if (i + 1 < f->get_arity()) {
diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index 0c2f03460..753a45e06 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -33,7 +33,7 @@ def_module_params('fixedpoint',
"updated relation was modified or not"),
('datalog.compile_with_widening', BOOL, False,
"widening will be used to compile recursive rules"),
- ('datalog.default_table_checked', BOOL, False, "if true, the detault " +
+ ('datalog.default_table_checked', BOOL, False, "if true, the default " +
'table will be default_table inside a wrapper that checks that its results ' +
'are the same as of default_table_checker table'),
('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"),
@@ -59,7 +59,7 @@ def_module_params('fixedpoint',
('duality.full_expand', BOOL, False, 'Fully expand derivation trees'),
('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'),
('duality.feasible_edges', BOOL, True,
- 'Don\'t expand definitley infeasible edges'),
+ 'Don\'t expand definitely infeasible edges'),
('duality.use_underapprox', BOOL, False, 'Use underapproximations'),
('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'),
('duality.recursion_bound', UINT, UINT_MAX,
@@ -130,7 +130,7 @@ def_module_params('fixedpoint',
('xform.magic', BOOL, False,
"perform symbolic magic set transformation"),
('xform.scale', BOOL, False,
- "add scaling variable to linear real arithemtic clauses"),
+ "add scaling variable to linear real arithmetic clauses"),
('xform.inline_linear', BOOL, True, "try linear inlining method"),
('xform.inline_eager', BOOL, True, "try eager inlining of rules"),
('xform.inline_linear_branch', BOOL, False,
@@ -176,7 +176,7 @@ def_module_params('fixedpoint',
('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),
('spacer.reach_as_init', BOOL, True, "Extend initial rules with computed reachability facts"),
('spacer.blast_term_ite', BOOL, True, "Expand non-Boolean ite-terms"),
- ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministicly"),
+ ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministically"),
('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"),
('bmc.linear_unrolling_depth', UINT, UINT_MAX, "Maximal level to explore"),
('spacer.split_farkas_literals', BOOL, False, "Split Farkas literals"),
diff --git a/src/muz/transforms/dl_mk_array_instantiation.h b/src/muz/transforms/dl_mk_array_instantiation.h
index cd5715a4f..b2e80ab84 100644
--- a/src/muz/transforms/dl_mk_array_instantiation.h
+++ b/src/muz/transforms/dl_mk_array_instantiation.h
@@ -26,7 +26,7 @@ Implementation:
1) Dealing with multiple quantifiers -> The options fixedpoint.xform.instantiate_arrays.nb_quantifier gives the number of quantifiers per array.
- 2) Inforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
+ 2) Enforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
P(a) into P(i, a[i]). This enforces the solver to limit the space search at the cost of imprecise results. This option
corresponds to fixedpoint.xform.instantiate_arrays.enforce
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.h b/src/muz/transforms/dl_mk_interp_tail_simplifier.h
index 713827588..0d4c65d11 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.h
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.h
@@ -53,7 +53,7 @@ namespace datalog {
*/
void reset(rule * r);
- /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
+ /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
bool unify(expr * e1, expr * e2);
void get_result(rule_ref & res);
diff --git a/src/muz/transforms/dl_mk_rule_inliner.h b/src/muz/transforms/dl_mk_rule_inliner.h
index 27b6dd418..9146343fa 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.h
+++ b/src/muz/transforms/dl_mk_rule_inliner.h
@@ -45,7 +45,7 @@ namespace datalog {
: m(ctx.get_manager()), m_rm(ctx.get_rule_manager()), m_context(ctx),
m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false), m_normalize(true) {}
- /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
+ /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
bool unify_rules(rule const& tgt, unsigned tgt_idx, rule const& src);
/**
diff --git a/src/muz/transforms/dl_mk_scale.h b/src/muz/transforms/dl_mk_scale.h
index c171a1d06..94090ec93 100644
--- a/src/muz/transforms/dl_mk_scale.h
+++ b/src/muz/transforms/dl_mk_scale.h
@@ -7,7 +7,7 @@ Module Name:
Abstract:
- Add scale factor to linear (Real) arithemetic Horn clauses.
+ Add scale factor to linear (Real) arithmetic Horn clauses.
The transformation replaces occurrences of isolated constants by
a scale multiplied to each constant.
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index fe62efbf4..46388fcf4 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -469,7 +469,8 @@ namespace smt {
if (negated) l_conseq.neg();
TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";
- tout << s_ante << "\n" << s_conseq << "\n";);
+ tout << s_ante << "\n" << s_conseq << "\n";
+ tout << l_ante << "\n" << l_conseq << "\n";);
// literal lits[2] = {l_ante, l_conseq};
mk_clause(l_ante, l_conseq, 0, nullptr);
@@ -589,13 +590,13 @@ namespace smt {
}
//
- // create the term: s := to_real(to_int(x)) - x
+ // create the term: s := x - to_real(to_int(x))
// add the bounds 0 <= s < 1
//
template
void theory_arith::mk_to_int_axiom(app * n) {
SASSERT(m_util.is_to_int(n));
- ast_manager & m = get_manager();
+ ast_manager & m = get_manager();
expr* x = n->get_arg(0);
// to_int (to_real x) = x
@@ -603,11 +604,15 @@ namespace smt {
mk_axiom(m.mk_false(), m.mk_eq(to_app(x)->get_arg(0), n));
return;
}
- expr* to_r = m_util.mk_to_real(n);
- expr_ref lo(m_util.mk_le(to_r, x), m);
- expr_ref hi(m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false))), m);
- mk_axiom(m.mk_false(), lo);
- mk_axiom(m.mk_false(), hi);
+ expr_ref to_r(m_util.mk_to_real(n), m);
+ expr_ref diff(m_util.mk_add(x, m_util.mk_mul(m_util.mk_real(-1), to_r)), m);
+
+ expr_ref lo(m_util.mk_ge(diff, m_util.mk_real(0)), m);
+ expr_ref hi(m_util.mk_ge(diff, m_util.mk_real(1)), m);
+ hi = m.mk_not(hi);
+
+ mk_axiom(m.mk_false(), lo, false);
+ mk_axiom(m.mk_false(), hi, false);
}
template
@@ -1202,7 +1207,7 @@ namespace smt {
template
bool theory_arith::internalize_atom(app * n, bool gate_ctx) {
- TRACE("arith_internalize", tout << "internalising atom:\n" << mk_pp(n, this->get_manager()) << "\n";);
+ TRACE("arith_internalize", tout << "internalizing atom:\n" << mk_pp(n, this->get_manager()) << "\n";);
context & ctx = get_context();
SASSERT(m_util.is_le(n) || m_util.is_ge(n) || m_util.is_is_int(n));
SASSERT(!ctx.b_internalized(n));
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 8567c6b30..0016b8f36 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -641,7 +641,6 @@ namespace smt {
}
app * theory_str::mk_indexof(expr * haystack, expr * needle) {
- // TODO check meaning of the third argument here
app * indexof = u.str.mk_index(haystack, needle, mk_int(0));
m_trail.push_back(indexof);
// immediately force internalization so that axiom setup does not fail
@@ -844,14 +843,7 @@ namespace smt {
instantiate_axiom_Contains(e);
} else if (u.str.is_index(a)) {
instantiate_axiom_Indexof(e);
- /* TODO NEXT: Indexof2/Lastindexof rewrite?
- } else if (is_Indexof2(e)) {
- instantiate_axiom_Indexof2(e);
- } else if (is_LastIndexof(e)) {
- instantiate_axiom_LastIndexof(e);
- */
} else if (u.str.is_extract(a)) {
- // TODO check semantics of substr vs. extract
instantiate_axiom_Substr(e);
} else if (u.str.is_replace(a)) {
instantiate_axiom_Replace(e);
@@ -1232,27 +1224,37 @@ namespace smt {
context & ctx = get_context();
ast_manager & m = get_manager();
- app * expr = e->get_owner();
- if (axiomatized_terms.contains(expr)) {
- TRACE("str", tout << "already set up Indexof axiom for " << mk_pp(expr, m) << std::endl;);
+ app * ex = e->get_owner();
+ if (axiomatized_terms.contains(ex)) {
+ TRACE("str", tout << "already set up str.indexof axiom for " << mk_pp(ex, m) << std::endl;);
return;
}
- axiomatized_terms.insert(expr);
+ SASSERT(ex->get_num_args() == 3);
+ // if the third argument is exactly the integer 0, we can use this "simple" indexof;
+ // otherwise, we call the "extended" version
+ expr * startingPosition = ex->get_arg(2);
+ rational startingInteger;
+ if (!m_autil.is_numeral(startingPosition, startingInteger) || !startingInteger.is_zero()) {
+ // "extended" indexof term with prefix
+ instantiate_axiom_Indexof_extended(e);
+ return;
+ }
+ axiomatized_terms.insert(ex);
- TRACE("str", tout << "instantiate Indexof axiom for " << mk_pp(expr, m) << std::endl;);
+ TRACE("str", tout << "instantiate str.indexof axiom for " << mk_pp(ex, m) << std::endl;);
expr_ref x1(mk_str_var("x1"), m);
expr_ref x2(mk_str_var("x2"), m);
expr_ref indexAst(mk_int_var("index"), m);
- expr_ref condAst(mk_contains(expr->get_arg(0), expr->get_arg(1)), m);
+ expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m);
SASSERT(condAst);
// -----------------------
// true branch
expr_ref_vector thenItems(m);
// args[0] = x1 . args[1] . x2
- thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x1, mk_concat(expr->get_arg(1), x2))));
+ thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x1, mk_concat(ex->get_arg(1), x2))));
// indexAst = |x1|
thenItems.push_back(ctx.mk_eq_atom(indexAst, mk_strlen(x1)));
// args[0] = x3 . x4
@@ -1260,11 +1262,11 @@ namespace smt {
// /\ ! contains(x3, args[1])
expr_ref x3(mk_str_var("x3"), m);
expr_ref x4(mk_str_var("x4"), m);
- expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(expr->get_arg(1)), mk_int(-1)), m);
+ expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(ex->get_arg(1)), mk_int(-1)), m);
SASSERT(tmpLen);
- thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
+ thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x3, x4)));
thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
- thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
+ thenItems.push_back(mk_not(m, mk_contains(x3, ex->get_arg(1))));
expr_ref thenBranch(m.mk_and(thenItems.size(), thenItems.c_ptr()), m);
SASSERT(thenBranch);
@@ -1276,26 +1278,42 @@ namespace smt {
expr_ref breakdownAssert(m.mk_ite(condAst, thenBranch, elseBranch), m);
SASSERT(breakdownAssert);
- expr_ref reduceToIndex(ctx.mk_eq_atom(expr, indexAst), m);
+ expr_ref reduceToIndex(ctx.mk_eq_atom(ex, indexAst), m);
SASSERT(reduceToIndex);
expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToIndex), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
+
+ {
+ // heuristic: integrate with str.contains information
+ // (but don't introduce it if it isn't already in the instance)
+ expr_ref haystack(ex->get_arg(0), m), needle(ex->get_arg(1), m), startIdx(ex->get_arg(2), m);
+ expr_ref zeroAst(mk_int(0), m);
+ // (H contains N) <==> (H indexof N, i) >= 0
+ expr_ref premise(u.str.mk_contains(haystack, needle), m);
+ ctx.internalize(premise, false);
+ expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m);
+ expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
+ SASSERT(containsAxiom);
+ // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
+ m_delayed_axiom_setup_terms.push_back(containsAxiom);
+ }
}
- void theory_str::instantiate_axiom_Indexof2(enode * e) {
+ void theory_str::instantiate_axiom_Indexof_extended(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
- TRACE("str", tout << "already set up Indexof2 axiom for " << mk_pp(expr, m) << std::endl;);
+ TRACE("str", tout << "already set up extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;);
return;
}
+ SASSERT(expr->get_num_args() == 3);
axiomatized_terms.insert(expr);
- TRACE("str", tout << "instantiate Indexof2 axiom for " << mk_pp(expr, m) << std::endl;);
+ TRACE("str", tout << "instantiate extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;);
// -------------------------------------------------------------------------------
// if (arg[2] >= length(arg[0])) // ite2
@@ -1327,7 +1345,7 @@ namespace smt {
ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1))));
ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen));
ite2ElseItems.push_back(ite3);
- expr_ref ite2Else(m.mk_and(ite2ElseItems.size(), ite2ElseItems.c_ptr()), m);
+ expr_ref ite2Else(mk_and(ite2ElseItems), m);
SASSERT(ite2Else);
expr_ref ite2(m.mk_ite(
@@ -1350,6 +1368,20 @@ namespace smt {
expr_ref reduceTerm(ctx.mk_eq_atom(expr, resAst), m);
SASSERT(reduceTerm);
assert_axiom(reduceTerm);
+
+ {
+ // heuristic: integrate with str.contains information
+ // (but don't introduce it if it isn't already in the instance)
+ expr_ref haystack(expr->get_arg(0), m), needle(expr->get_arg(1), m), startIdx(expr->get_arg(2), m);
+ // (H contains N) <==> (H indexof N, i) >= 0
+ expr_ref premise(u.str.mk_contains(haystack, needle), m);
+ ctx.internalize(premise, false);
+ expr_ref conclusion(m_autil.mk_ge(expr, zeroAst), m);
+ expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
+ SASSERT(containsAxiom);
+ // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
+ m_delayed_axiom_setup_terms.push_back(containsAxiom);
+ }
}
void theory_str::instantiate_axiom_LastIndexof(enode * e) {
@@ -5521,7 +5553,8 @@ namespace smt {
return node;
}
- void theory_str::get_grounded_concats(expr* node, std::map & varAliasMap,
+ void theory_str::get_grounded_concats(unsigned depth,
+ expr* node, std::map & varAliasMap,
std::map & concatAliasMap, std::map & varConstMap,
std::map & concatConstMap, std::map > & varEqConcatMap,
std::map, std::set > > & groundedMap) {
@@ -5536,6 +5569,9 @@ namespace smt {
if (groundedMap.find(node) != groundedMap.end()) {
return;
}
+ IF_VERBOSE(100, verbose_stream() << "concats " << depth << "\n";
+ if (depth > 100) verbose_stream() << mk_pp(node, get_manager()) << "\n";
+ );
// haven't computed grounded concats for "node" (de-aliased)
// ---------------------------------------------------------
@@ -5565,8 +5601,8 @@ namespace smt {
expr * arg1 = to_app(node)->get_arg(1);
expr * arg0DeAlias = dealias_node(arg0, varAliasMap, concatAliasMap);
expr * arg1DeAlias = dealias_node(arg1, varAliasMap, concatAliasMap);
- get_grounded_concats(arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
- get_grounded_concats(arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+ get_grounded_concats(depth + 1, arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+ get_grounded_concats(depth + 1, arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
std::map, std::set >::iterator arg0_grdItor = groundedMap[arg0DeAlias].begin();
std::map, std::set >::iterator arg1_grdItor;
@@ -5616,7 +5652,7 @@ namespace smt {
else if (varEqConcatMap.find(node) != varEqConcatMap.end()) {
expr * eqConcat = varEqConcatMap[node].begin()->first;
expr * deAliasedEqConcat = dealias_node(eqConcat, varAliasMap, concatAliasMap);
- get_grounded_concats(deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+ get_grounded_concats(depth + 1, deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
std::map, std::set >::iterator grdItor = groundedMap[deAliasedEqConcat].begin();
for (; grdItor != groundedMap[deAliasedEqConcat].end(); grdItor++) {
@@ -5825,8 +5861,8 @@ namespace smt {
expr* strDeAlias = dealias_node(str, varAliasMap, concatAliasMap);
expr* subStrDeAlias = dealias_node(subStr, varAliasMap, concatAliasMap);
- get_grounded_concats(strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
- get_grounded_concats(subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+ get_grounded_concats(0, strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+ get_grounded_concats(0, subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
// debugging
print_grounded_concat(strDeAlias, groundedMap);
@@ -8731,8 +8767,8 @@ namespace smt {
context & ctx = get_context();
ast_manager & m = get_manager();
- expr_ref_vector assignments(m);
- ctx.get_assignments(assignments);
+ //expr_ref_vector assignments(m);
+ //ctx.get_assignments(assignments);
if (opt_VerifyFinalCheckProgress) {
finalCheckProgressIndicator = false;
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 3b71a2282..64ede71b5 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -447,7 +447,7 @@ protected:
void instantiate_axiom_suffixof(enode * e);
void instantiate_axiom_Contains(enode * e);
void instantiate_axiom_Indexof(enode * e);
- void instantiate_axiom_Indexof2(enode * e);
+ void instantiate_axiom_Indexof_extended(enode * e);
void instantiate_axiom_LastIndexof(enode * e);
void instantiate_axiom_Substr(enode * e);
void instantiate_axiom_Replace(enode * e);
@@ -495,10 +495,11 @@ protected:
std::map & concatAliasMap, std::map & varConstMap,
std::map & concatConstMap, std::map > & varEqConcatMap);
expr * dealias_node(expr * node, std::map & varAliasMap, std::map & concatAliasMap);
- void get_grounded_concats(expr* node, std::map & varAliasMap,
- std::map & concatAliasMap, std::map & varConstMap,
- std::map & concatConstMap, std::map > & varEqConcatMap,
- std::map, std::set > > & groundedMap);
+ void get_grounded_concats(unsigned depth,
+ expr* node, std::map & varAliasMap,
+ std::map & concatAliasMap, std::map & varConstMap,
+ std::map & concatConstMap, std::map > & varEqConcatMap,
+ std::map, std::set > > & groundedMap);
void print_grounded_concat(expr * node, std::map, std::set > > & groundedMap);
void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
std::map, std::set > > & groundedMap);
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index 40c68f72a..6afac32b8 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -267,7 +267,7 @@ struct aig_manager::imp {
}
if (b == r) {
if (sign1) {
- // subsitution
+ // substitution
// not (a and b) and r --> (not a) and r IF b == r
l = a;
l.invert();
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 6ad9c0812..93a0b2e88 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -582,7 +582,7 @@ struct ctx_simplify_tactic::imp {
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
expr * t = g.form(i);
process(t, r);
- proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(t, r, 0, nullptr)); // TODO :-)
+ proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(t, r));
g.update(i, r, new_pr, g.dep(i));
}
}
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index e8d3150af..47f96a7d9 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -382,7 +382,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
change |= r != g.form(i);
proof* new_pr = nullptr;
if (g.proofs_enabled()) {
- new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr));
+ new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
}
g.update(i, r, new_pr, g.dep(i));
}
@@ -402,7 +402,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
proof* new_pr = nullptr;
if (g.proofs_enabled()) {
- new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr));
+ new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
}
g.update(i, r, new_pr, g.dep(i));
}
diff --git a/src/tactic/tactic_exception.h b/src/tactic/tactic_exception.h
index 177524726..bdf2636a9 100644
--- a/src/tactic/tactic_exception.h
+++ b/src/tactic/tactic_exception.h
@@ -7,7 +7,7 @@ Module Name:
Abstract:
- Tactic expection object.
+ Tactic exception object.
Author:
diff --git a/src/tactic/tactical.h b/src/tactic/tactical.h
index 169566f39..9ec2f901f 100644
--- a/src/tactic/tactical.h
+++ b/src/tactic/tactical.h
@@ -47,7 +47,7 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5
tactic * repeat(tactic * t, unsigned max = UINT_MAX);
/**
- \brief Fails if \c t produeces more than \c threshold subgoals.
+ \brief Fails if \c t produces more than \c threshold subgoals.
Otherwise, it behaves like \c t.
*/
tactic * fail_if_branching(tactic * t, unsigned threshold = 1);
diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp
index 12fca706d..f376e2c1d 100644
--- a/src/test/quant_elim.cpp
+++ b/src/test/quant_elim.cpp
@@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/reg_decl_plugins.h"
+#if 0
static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char const* option) {
// enable_trace("bit2int");
@@ -48,6 +49,7 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons
//exit(-1);
}
}
+#endif
static void test_formula(lbool expected_outcome, char const* fml) {
ast_manager m;
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index 1ecca8ffe..a2a0cc269 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -33,8 +33,8 @@ Revision History:
#include
#include
#include
-#elif defined(_LINUX_) || defined(_FREEBSD_)
-// Linux
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NetBSD_)
+// Linux & FreeBSD & NetBSD
#include
#include
#include
@@ -66,8 +66,8 @@ struct scoped_timer::imp {
pthread_mutex_t m_mutex;
pthread_cond_t m_condition_var;
struct timespec m_end_time;
-#elif defined(_LINUX_) || defined(_FREEBSD_)
- // Linux & FreeBSD
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
+ // Linux & FreeBSD & NetBSD
pthread_t m_thread_id;
pthread_mutex_t m_mutex;
pthread_cond_t m_cond;
@@ -104,7 +104,7 @@ struct scoped_timer::imp {
return st;
}
-#elif defined(_LINUX_) || defined(_FREEBSD_)
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
static void* thread_func(void *arg) {
scoped_timer::imp *st = static_cast(arg);
@@ -175,8 +175,8 @@ struct scoped_timer::imp {
if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
throw default_exception("failed to start timer thread");
-#elif defined(_LINUX_) || defined(_FREEBSD_)
- // Linux & FreeBSD
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
+ // Linux & FreeBSD & NetBSD
m_ms = ms;
m_initialized = false;
m_signal_sent = false;
@@ -216,8 +216,8 @@ struct scoped_timer::imp {
throw default_exception("failed to destroy pthread condition variable");
if (pthread_attr_destroy(&m_attributes) != 0)
throw default_exception("failed to destroy pthread attributes object");
-#elif defined(_LINUX_) || defined(_FREEBSD_)
- // Linux & FreeBSD
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
+ // Linux & FreeBSD & NetBSD
bool init = false;
// spin until timer thread has been created
diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h
index 9ba707af0..83e03a2f7 100644
--- a/src/util/stopwatch.h
+++ b/src/util/stopwatch.h
@@ -134,6 +134,11 @@ public:
#include
+#ifndef CLOCK_PROCESS_CPUTIME_ID
+/* BSD */
+# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC
+#endif
+
class stopwatch {
unsigned long long m_time; // elapsed time in ns
bool m_running;