mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 02:45:51 +00:00
Typo Fixes (#6803)
This commit is contained in:
THE Spellchecker
GitHub
parent
28a0c2d18f
commit
dc0887db5a
43 changed files with 1811 additions and 1811 deletions
|
|
@ -81,7 +81,7 @@ if (EXISTS "${GIT_DIR}")
|
|||
# This mimics the behaviour of the old build system.
|
||||
set(Z3_FULL_VERSION_STR "${Z3_FULL_VERSION_STR} ${Z3_GIT_DESCRIPTION}")
|
||||
else()
|
||||
message(STATUS "Not including git descrption in version")
|
||||
message(STATUS "Not including git description in version")
|
||||
endif()
|
||||
else()
|
||||
message(WARNING "Failed to add git dependency.")
|
||||
|
|
@ -462,7 +462,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${PROJECT_BINARY_DIR}")
|
|||
# generate files used for Z3's build. Changes to these files will trigger
|
||||
# a rebuild of all the generated files.
|
||||
################################################################################
|
||||
# Note: ``update_api.py`` is deliberately not here because it not used
|
||||
# Note: ``update_api.py`` is deliberately not here because it is not used
|
||||
# to generate every generated file. The targets that need it list it explicitly.
|
||||
set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES
|
||||
"${PROJECT_SOURCE_DIR}/scripts/mk_genfile_common.py"
|
||||
|
|
|
|||
|
|
@ -125,7 +125,7 @@ Note that this is `libz3` not `z3` (`libz3` refers to the library target from `s
|
|||
|
||||
[Ninja](https://ninja-build.org/) is a simple build system that is built for speed.
|
||||
It can be significantly faster than "UNIX Makefile"s because it is not a recursive
|
||||
build system and thus doesn't create a new process everytime it traverses into a directory.
|
||||
build system and thus doesn't create a new process every time it traverses into a directory.
|
||||
Ninja is particularly appropriate if you want fast incremental building.
|
||||
|
||||
Basic usage is as follows:
|
||||
|
|
@ -236,7 +236,7 @@ more interactive and allow you to change various options. In both these
|
|||
tools the basic steps to follow are:
|
||||
|
||||
1. Configure.
|
||||
2. Change any options you wish. Everytime you change a set of options
|
||||
2. Change any options you wish. Every time you change a set of options
|
||||
You should configure again. This may cause new options to appear
|
||||
3. Generate.
|
||||
|
||||
|
|
@ -348,7 +348,7 @@ These notes are help developers and packagers of Z3.
|
|||
### Install/Uninstall
|
||||
|
||||
Install and uninstall targets are supported. Use ``CMAKE_INSTALL_PREFIX`` to
|
||||
set the install prefix. If you also need need to control which directories are
|
||||
set the install prefix. If you also need to control which directories are
|
||||
used for install set the documented ``CMAKE_INSTALL_*`` options.
|
||||
|
||||
To install run
|
||||
|
|
|
|||
|
|
@ -62,7 +62,7 @@ Version 4.12.0
|
|||
Clauses that are deduced by theories are marked by default
|
||||
by 'smt', and when more detailed information
|
||||
is available with proof hints or proof objects.
|
||||
Instantations are considered useful to track so they
|
||||
Instantiations are considered useful to track so they
|
||||
are logged using terms of the form
|
||||
|
||||
(inst (not (forall (x) body)) body[t/x] (bind t)), where
|
||||
|
|
@ -88,7 +88,7 @@ Version 4.12.0
|
|||
checker cannot check. It is mainly a limitation
|
||||
of the arithmetic solver not pulling relevant information.
|
||||
Ensuring a tight coupling with proof hints and the validator
|
||||
capabilites is open ended future work and good material for theses.
|
||||
capabilities is open ended future work and good material for theses.
|
||||
- bit-vector inferences - are treated as trusted
|
||||
(there is no validation, it always blindly succeeds)
|
||||
- arrays, datatypes - there is no custom validation for
|
||||
|
|
@ -158,13 +158,13 @@ Version 4.11.2
|
|||
with SMT format that is extensible. The resulting format is a mild extension of SMTLIB with
|
||||
three extra commands assume, learn, del. They track input clauses, generated clauses and deleted clauses.
|
||||
They are optionally augmented by proof hints. Two proof hints are used in the current version: "rup" and "farkas".
|
||||
"rup" is used whent the generated clause can be justified by reverse unit propagation. "farkas" is used when
|
||||
"rup" is used when the generated clause can be justified by reverse unit propagation. "farkas" is used when
|
||||
the clause can be justified by a combination of Farkas cutting planes. There is a built-in proof checker for the
|
||||
format. Quantifier instantiations are also tracked as proof hints.
|
||||
Other proof hints are to be added as the feature set is tested and developed. The fallback, buit-in,
|
||||
Other proof hints are to be added as the feature set is tested and developed. The fallback, built-in,
|
||||
self-checker uses z3 to check that the generated clause is a consequence. Note that this is generally
|
||||
insufficient as generated clauses are in principle required to only be satisfiability preserving.
|
||||
Proof checking and tranformation operations is overall open ended.
|
||||
Proof checking and transformation operations is overall open ended.
|
||||
The log for the first commit introducing this change contains further information on the format.
|
||||
- fix to re-entrancy bug in user propagator (thanks to Clemens Eisenhofer).
|
||||
- handle _toExpr for quantified formulas in JS bindings
|
||||
|
|
@ -638,7 +638,7 @@ xor88, parno, gario, Bauna, GManNickG, hanwentao, dinu09, fhowar, Cici, chinissa
|
|||
(assert F)
|
||||
(check-sat a)
|
||||
(check-sat)
|
||||
If 'F' is unstatisfiable independently of the assumption 'a', and
|
||||
If 'F' is unsatisfiable independently of the assumption 'a', and
|
||||
the inconsistency can be detected by just performing propagation,
|
||||
Then, version <= 4.3.1 may return
|
||||
unsat
|
||||
|
|
|
|||
|
|
@ -952,7 +952,7 @@ def mk_hpp_from_pyg(pyg_file, output_dir):
|
|||
'UINT_MAX' : UINT_MAX,
|
||||
'max_memory_param' : max_memory_param,
|
||||
'max_steps_param' : max_steps_param,
|
||||
# Note that once this function is enterred that function
|
||||
# Note that once this function is entered that function
|
||||
# executes with respect to the globals of this module and
|
||||
# not the globals defined here
|
||||
'def_module_params' : def_module_params,
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ A tactic for performing Ackermann reduction for bit-vector formulas
|
|||
### Long Description
|
||||
|
||||
The Ackermann reduction replaces uninterpreted functions $f(t_1), f(t_2)$
|
||||
by fresh variables $f_1, f_2$ and addes axioms $t_1 \simeq t_2 \implies f_1 \simeq f_2$.
|
||||
by fresh variables $f_1, f_2$ and adds axioms $t_1 \simeq t_2 \implies f_1 \simeq f_2$.
|
||||
The reduction has the effect of eliminating uninterpreted functions. When the reduction
|
||||
produces a pure bit-vector benchmark, it allows Z3 to use a specialized SAT solver.
|
||||
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ Revision History:
|
|||
|
||||
/** \brief
|
||||
Information about how a formula is being converted into
|
||||
a formula without uninterpreted function symbols via ackermannization.
|
||||
a formula without uninterpreted function symbols via ackermannization.
|
||||
|
||||
The intended use is that new terms are added via set_abstr.
|
||||
Once all terms are abstracted, call seal.
|
||||
|
|
|
|||
|
|
@ -231,7 +231,7 @@ namespace api {
|
|||
void handle_exception(z3_exception & ex);
|
||||
char const * get_exception_msg() const { return m_exception_msg.c_str(); }
|
||||
|
||||
// Interrupt the current interruptable object
|
||||
// Interrupt the current interruptible object
|
||||
void interrupt();
|
||||
|
||||
void invoke_error_handler(Z3_error_code c);
|
||||
|
|
|
|||
|
|
@ -742,7 +742,7 @@ extern "C" {
|
|||
fpa_util & fu = ctx->fpautil();
|
||||
if (!ctx->bvutil().is_bv(to_expr(bv)) ||
|
||||
!fu.is_float(to_sort(s))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG, "bv sort the flaot sort expected");
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG, "bv sort the float sort expected");
|
||||
return nullptr;
|
||||
}
|
||||
expr * a = fu.mk_to_fp(to_sort(s), to_expr(bv));
|
||||
|
|
|
|||
|
|
@ -320,7 +320,7 @@ namespace z3 {
|
|||
/**
|
||||
\brief Create a recursive datatype over a single sort.
|
||||
\c name is the name of the recursive datatype
|
||||
\c n - the numer of constructors of the datatype
|
||||
\c n - the number of constructors of the datatype
|
||||
\c cs - the \c n constructors used to define the datatype
|
||||
|
||||
References to the datatype can be created using \ref datatype_sort.
|
||||
|
|
|
|||
|
|
@ -3770,7 +3770,7 @@ namespace Microsoft.Z3
|
|||
}
|
||||
|
||||
/// <summary>
|
||||
/// Create a simplifie that applies <paramref name="t1"/> and
|
||||
/// Create a simplifier that applies <paramref name="t1"/> and
|
||||
/// then <paramref name="t2"/>.
|
||||
/// </summary>
|
||||
public Simplifier AndThen(Simplifier t1, Simplifier t2, params Simplifier[] ts)
|
||||
|
|
|
|||
|
|
@ -97,7 +97,7 @@ namespace Microsoft.Z3
|
|||
}
|
||||
|
||||
/// <summary>
|
||||
/// The Symbols's hash code.
|
||||
/// The Symbol's hash code.
|
||||
/// </summary>
|
||||
/// <returns>A hash code</returns>
|
||||
public override int GetHashCode()
|
||||
|
|
|
|||
|
|
@ -58,7 +58,7 @@ namespace Microsoft.Z3
|
|||
public delegate void CreatedEh(Expr term);
|
||||
|
||||
/// <summary>
|
||||
/// Delegate type for callback into solver's branching. The values can be overriden by calling <see cref="NextSplit" />.
|
||||
/// Delegate type for callback into solver's branching. The values can be overridden by calling <see cref="NextSplit" />.
|
||||
/// </summary>
|
||||
/// <param name="term">A bit-vector or Boolean used for branching</param>
|
||||
/// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
|
||||
|
|
|
|||
|
|
@ -2309,7 +2309,7 @@ public class Context implements AutoCloseable {
|
|||
|
||||
/**
|
||||
* Create the empty regular expression.
|
||||
* Coresponds to re.none
|
||||
* Corresponds to re.none
|
||||
*/
|
||||
public final <R extends Sort> ReExpr<R> mkEmptyRe(ReSort<R> s)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ import java.util.Map;
|
|||
*
|
||||
* <p><b>Mechanics: </b>once an object is created, a metadata is stored for it in
|
||||
* {@code referenceMap}, and a {@link PhantomReference} is created with a
|
||||
* reference to {@code referenceQueue}.
|
||||
* reference to {@code referenceQueue}.
|
||||
* Once the object becomes strongly unreachable, the phantom reference gets
|
||||
* added by JVM to the {@code referenceQueue}.
|
||||
* After each object creation, we iterate through the available objects in
|
||||
|
|
|
|||
|
|
@ -166,7 +166,7 @@ public class Quantifier extends BoolExpr
|
|||
* @param sorts Sorts of bound variables.
|
||||
* @param names Names of bound variables
|
||||
* @param body Body of quantifier
|
||||
* @param weight Weight used to indicate priority for qunatifier instantiation
|
||||
* @param weight Weight used to indicate priority for quantifier instantiation
|
||||
* @param patterns Nullable patterns
|
||||
* @param noPatterns Nullable noPatterns
|
||||
* @param quantifierID Nullable quantifierID
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ Then run `npm i` to install dependencies, `npm run build:ts` to build the TypeSc
|
|||
|
||||
### Build on your own
|
||||
|
||||
Consult the file [build-wasm.ts](https://github.com/Z3Prover/z3/blob/master/src/api/js/scripts/build-wasm.ts) for configurations used for building wasm.
|
||||
Consult the file [build-wasm.ts](https://github.com/Z3Prover/z3/blob/master/src/api/js/scripts/build-wasm.ts) for configurations used for building wasm.
|
||||
|
||||
## Tests
|
||||
|
||||
|
|
|
|||
|
|
@ -350,7 +350,7 @@ for (let fn of functions) {
|
|||
param.sizeIndex = defParams[idx].sizeIndex;
|
||||
if (!param.isArray && param.isPtr) {
|
||||
// not clear why some things are written as `int * x` and others `int x[]`
|
||||
// but we can jsut cast
|
||||
// but we can just cast
|
||||
param.isArray = true;
|
||||
param.isPtr = false;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -223,7 +223,7 @@ correctly found by gcc.
|
|||
|
||||
I specifically left the cygwin part of the code intact as I have no
|
||||
idea what the original author meant by this, neither do I use or
|
||||
tested this patch in the cygwin or mingw environemt. I think that this
|
||||
tested this patch in the cygwin or mingw environment. I think that this
|
||||
code is rather outdated and shouldn't really work. E.g., in the
|
||||
--staticlib mode adding z3linkdep (which is libz3-static.a) as an
|
||||
argument to `ocamlmklib` will yield the following broken archive
|
||||
|
|
|
|||
|
|
@ -292,7 +292,7 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
|
|||
distos = RELEASE_METADATA[2]
|
||||
if distos in ('debian', 'ubuntu'):
|
||||
raise Exception(
|
||||
"Linux binary distributions must be built on centos to conform to PEP 513 or alpine if targetting musl"
|
||||
"Linux binary distributions must be built on centos to conform to PEP 513 or alpine if targeting musl"
|
||||
)
|
||||
elif distos == 'glibc':
|
||||
if arch == 'x64':
|
||||
|
|
|
|||
|
|
@ -5385,7 +5385,7 @@ def EnumSort(name, values, ctx=None):
|
|||
"""
|
||||
if z3_debug():
|
||||
_z3_assert(isinstance(name, str), "Name must be a string")
|
||||
_z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
|
||||
_z3_assert(all([isinstance(v, str) for v in values]), "Enumeration sort values must be strings")
|
||||
_z3_assert(len(values) > 0, "At least one value expected")
|
||||
ctx = _get_ctx(ctx)
|
||||
num = len(values)
|
||||
|
|
|
|||
|
|
@ -275,7 +275,7 @@ def prove(claim, assume=None, verbose=0):
|
|||
|
||||
def get_models(f, k):
|
||||
"""
|
||||
Returns the first k models satisfiying f.
|
||||
Returns the first k models satisfying f.
|
||||
If f is not satisfiable, returns False.
|
||||
If f cannot be solved, returns None
|
||||
If f is satisfiable, returns the first k models
|
||||
|
|
@ -485,7 +485,7 @@ def model_str(m, as_str=True):
|
|||
x = 10, y = 3
|
||||
|
||||
EXAMPLES:
|
||||
see doctest exampels from function prove()
|
||||
see doctest examples from function prove()
|
||||
|
||||
"""
|
||||
if z3_debug():
|
||||
|
|
|
|||
|
|
@ -2172,7 +2172,7 @@ extern "C" {
|
|||
\brief Query constructor for declared functions.
|
||||
|
||||
\param c logical context.
|
||||
\param constr constructor container. The container must have been passed in to a #Z3_mk_datatype call.
|
||||
\param constr constructor container. The container must have been passed into a #Z3_mk_datatype call.
|
||||
\param num_fields number of accessor fields in the constructor.
|
||||
\param constructor constructor function declaration, allocated by user.
|
||||
\param tester constructor test function declaration, allocated by user.
|
||||
|
|
@ -2317,7 +2317,7 @@ extern "C" {
|
|||
\param args constants that are used as arguments to the recursive function in the definition.
|
||||
\param body body of the recursive function
|
||||
|
||||
After declaring a recursive function or a collection of mutually recursive functions, use
|
||||
After declaring a recursive function or a collection of mutually recursive functions, use
|
||||
this function to provide the definition for the recursive function.
|
||||
|
||||
\sa Z3_mk_rec_func_decl
|
||||
|
|
@ -3614,7 +3614,7 @@ extern "C" {
|
|||
|
||||
/**
|
||||
\brief Retrieve the string constant stored in \c s.
|
||||
Characters outside the basic printiable ASCII range are escaped.
|
||||
Characters outside the basic printable ASCII range are escaped.
|
||||
|
||||
\pre Z3_is_string(c, s)
|
||||
|
||||
|
|
@ -4897,7 +4897,7 @@ extern "C" {
|
|||
/**
|
||||
\brief Return a hash code for the given AST.
|
||||
The hash code is structural but two different AST objects can map to the same hash.
|
||||
The result of \c Z3_get_ast_id returns an indentifier that is unique over the
|
||||
The result of \c Z3_get_ast_id returns an identifier that is unique over the
|
||||
set of live AST objects.
|
||||
|
||||
def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST)))
|
||||
|
|
@ -5346,7 +5346,7 @@ extern "C" {
|
|||
Z3_ast const to[]);
|
||||
|
||||
/**
|
||||
\brief Substitute funcions in \c from with new expressions in \c to.
|
||||
\brief Substitute functions in \c from with new expressions in \c to.
|
||||
|
||||
The expressions in \c to can have free variables. The free variable in \c to at index 0
|
||||
refers to the first argument of \c from, the free variable at index 1 corresponds to the second argument.
|
||||
|
|
@ -7026,13 +7026,13 @@ extern "C" {
|
|||
Z3_on_clause_eh on_clause_eh);
|
||||
|
||||
/**
|
||||
\brief register a user-properator with the solver.
|
||||
\brief register a user-propagator with the solver.
|
||||
|
||||
\param c - context.
|
||||
\param s - solver object.
|
||||
\param user_context - a context used to maintain state for callbacks.
|
||||
\param push_eh - a callback invoked when scopes are pushed
|
||||
\param pop_eh - a callback invoked when scopes are poped
|
||||
\param pop_eh - a callback invoked when scopes are popped
|
||||
\param fresh_eh - a solver may spawn new solvers internally. This callback is used to produce a fresh user_context to be associated with fresh solvers.
|
||||
|
||||
def_API('Z3_solver_propagate_init', VOID, (_in(CONTEXT), _in(SOLVER), _in(VOID_PTR), _fnptr(Z3_push_eh), _fnptr(Z3_pop_eh), _fnptr(Z3_fresh_eh)))
|
||||
|
|
|
|||
|
|
@ -651,7 +651,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
|
|||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
if (args[i]->get_sort() != r->get_domain(i)) {
|
||||
std::ostringstream buffer;
|
||||
buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " has sort " << mk_pp(args[i]->get_sort(), m) << " it does does not match declaration " << mk_pp(r, m);
|
||||
buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " has sort " << mk_pp(args[i]->get_sort(), m) << " it does not match declaration " << mk_pp(r, m);
|
||||
m.raise_exception(buffer.str());
|
||||
return nullptr;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -96,7 +96,7 @@ enum bv_op_kind {
|
|||
OP_BUMUL_OVFL, // unsigned multiplication overflow predicate (negation of OP_BUMUL_NO_OVFL)
|
||||
OP_BSMUL_OVFL, // signed multiplication over/underflow predicate
|
||||
|
||||
OP_BSDIV_OVFL, // signed division overflow perdicate
|
||||
OP_BSDIV_OVFL, // signed division overflow predicate
|
||||
|
||||
OP_BNEG_OVFL, // negation overflow predicate
|
||||
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ Module Name:
|
|||
|
||||
Abstract:
|
||||
|
||||
char_plugin for unicode suppport
|
||||
char_plugin for unicode support
|
||||
|
||||
Author:
|
||||
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ Module Name:
|
|||
|
||||
Abstract:
|
||||
|
||||
char_plugin for unicode suppport
|
||||
char_plugin for unicode support
|
||||
|
||||
Author:
|
||||
|
||||
|
|
|
|||
|
|
@ -78,7 +78,7 @@ public:
|
|||
*
|
||||
* x = t -> fresh
|
||||
* x := if(fresh, t, diff(t))
|
||||
* where diff is a diagnonalization function available in domains of size > 1.
|
||||
* where diff is a diagonalization function available in domains of size > 1.
|
||||
*
|
||||
*/
|
||||
|
||||
|
|
@ -807,7 +807,7 @@ bool iexpr_inverter::uncnstr(unsigned num, expr * const * args) const {
|
|||
|
||||
/**
|
||||
\brief Create a fresh variable for abstracting (f args[0] ... args[num-1])
|
||||
Return true if it a new variable was created, and false if the variable already existed for this
|
||||
Return true if a new variable was created, and false if the variable already existed for this
|
||||
application. Store the variable in v
|
||||
*/
|
||||
void iexpr_inverter::mk_fresh_uncnstr_var_for(sort * s, expr_ref & v) {
|
||||
|
|
|
|||
|
|
@ -275,7 +275,7 @@ namespace datatype {
|
|||
}
|
||||
parameter const & name = parameters[0];
|
||||
if (!name.is_symbol()) {
|
||||
TRACE("datatype", tout << "expected symol parameter at position " << 0 << " got: " << name << "\n";);
|
||||
TRACE("datatype", tout << "expected symbol parameter at position " << 0 << " got: " << name << "\n";);
|
||||
throw invalid_datatype();
|
||||
}
|
||||
for (unsigned i = 1; i < num_parameters; ++i) {
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@ namespace datatype {
|
|||
class accessor {
|
||||
symbol m_name;
|
||||
sort_ref m_range;
|
||||
unsigned m_index; // reference to recursive data-type may only get resolved after all mutually recursive data-types are procssed.
|
||||
unsigned m_index; // reference to recursive data-type may only get resolved after all mutually recursive data-types are processed.
|
||||
constructor* m_constructor{ nullptr };
|
||||
public:
|
||||
accessor(ast_manager& m, symbol const& n, sort* range):
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ Notes:
|
|||
- data structures form the (legacy) SMT solver.
|
||||
- it still uses eager path compression.
|
||||
|
||||
NB. The worklist is in reality inheritied from the legacy SMT solver.
|
||||
NB. The worklist is in reality inherited from the legacy SMT solver.
|
||||
It is claimed to have the same effect as delayed congruence table reconstruction from egg.
|
||||
Similar to the legacy solver, parents are partially deduplicated.
|
||||
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ Author:
|
|||
Notes:
|
||||
|
||||
- congruence closure justifications are given a timestamp so it is easy to sort them.
|
||||
See the longer descriptoin in euf_proof_checker.cpp
|
||||
See the longer description in euf_proof_checker.cpp
|
||||
|
||||
--*/
|
||||
|
||||
|
|
|
|||
|
|
@ -65,7 +65,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, bool deps_valid, expr_de
|
|||
// functions introduced within macros are Skolem functions
|
||||
// To avoid unsound expansion of these as macros (because they
|
||||
// appear in model conversions and are therefore not fully
|
||||
// replacable) we prevent these from being treated as macro functions.
|
||||
// replaceable) we prevent these from being treated as macro functions.
|
||||
if (m_macro_manager.contains(f) || f->is_skolem())
|
||||
return false;
|
||||
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ Revision History:
|
|||
where T[X] does not contain f.
|
||||
|
||||
This class is responsible for storing macros and expanding them.
|
||||
It has support for backtracking and tagging declarations in an expression as forbidded for being macros.
|
||||
It has support for backtracking and tagging declarations in an expression as forbidden for being macros.
|
||||
*/
|
||||
class macro_manager {
|
||||
ast_manager & m;
|
||||
|
|
|
|||
|
|
@ -207,7 +207,7 @@ void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var
|
|||
// the instantiation rules for store(a, i, v) are:
|
||||
// store(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] }
|
||||
// The first pattern is not included.
|
||||
// TBD use a model-based scheme for exracting instantiations instead of
|
||||
// TBD use a model-based scheme for extracting instantiations instead of
|
||||
// using multi-patterns.
|
||||
//
|
||||
|
||||
|
|
|
|||
|
|
@ -260,7 +260,7 @@ class reduce_hypotheses {
|
|||
{ cls.push_back(cls_fact->get_arg(i)); }
|
||||
} else { cls.push_back(cls_fact); }
|
||||
|
||||
// construct new resovent
|
||||
// construct new resolvent
|
||||
ptr_buffer<expr> new_fact_cls;
|
||||
bool found;
|
||||
// XXX quadratic
|
||||
|
|
@ -604,7 +604,7 @@ public:
|
|||
// -- otherwise, the fact has not changed. nothing to simplify
|
||||
SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
|
||||
parents.push_back(tmp);
|
||||
// remember that we have this derivation while we have not poped the trail
|
||||
// remember that we have this derivation while we have not popped the trail
|
||||
// but only if the proof is closed (i.e., a real unit)
|
||||
if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
|
||||
m_units.insert(m.get_fact(tmp), tmp);
|
||||
|
|
|
|||
|
|
@ -1121,7 +1121,7 @@ bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) {
|
|||
if (m_util.is_numeral(arg, num_r)) num_e = arg;
|
||||
}
|
||||
for (expr* arg : args2) {
|
||||
// dont remove divisor on (div (* -1 x) (* -1 y)) because rewriting would diverge.
|
||||
// don't remove divisor on (div (* -1 x) (* -1 y)) because rewriting would diverge.
|
||||
if (mark.is_marked(arg) && (!m_util.is_numeral(arg, num_r) || !num_r.is_minus_one())) {
|
||||
result = remove_divisor(arg, num, den);
|
||||
return true;
|
||||
|
|
@ -1619,7 +1619,7 @@ br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) {
|
|||
}
|
||||
|
||||
|
||||
// Return true if t is of the form c*Pi where c is a numeral.
|
||||
// Return true if t is of the form c*Pi where c is a numeral.
|
||||
// Store c into k
|
||||
bool arith_rewriter::is_pi_multiple(expr * t, rational & k) {
|
||||
if (m_util.is_pi(t)) {
|
||||
|
|
@ -1630,7 +1630,7 @@ bool arith_rewriter::is_pi_multiple(expr * t, rational & k) {
|
|||
return m_util.is_mul(t, a, b) && m_util.is_pi(b) && m_util.is_numeral(a, k);
|
||||
}
|
||||
|
||||
// Return true if t is of the form (+ s c*Pi) where c is a numeral.
|
||||
// Return true if t is of the form (+ s c*Pi) where c is a numeral.
|
||||
// Store c into k, and c*Pi into m.
|
||||
bool arith_rewriter::is_pi_offset(expr * t, rational & k, expr * & m) {
|
||||
if (m_util.is_add(t)) {
|
||||
|
|
@ -1943,7 +1943,7 @@ br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) {
|
|||
br_status arith_rewriter::mk_asin_core(expr * arg, expr_ref & result) {
|
||||
// Remark: we assume that ForAll x : asin(-x) == asin(x).
|
||||
// Mathematica uses this as an axiom. Although asin is an underspecified function for x < -1 or x > 1.
|
||||
// Actually, in Mathematica, asin(x) is a total function that returns a complex number fo x < -1 or x > 1.
|
||||
// Actually, in Mathematica, asin(x) is a total function that returns a complex number for x < -1 or x > 1.
|
||||
rational k;
|
||||
if (is_numeral(arg, k)) {
|
||||
if (k.is_zero()) {
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -94,7 +94,7 @@ namespace sat {
|
|||
// from clause x, y, z
|
||||
// then ~x, ~y -> z
|
||||
// look for ~y, z -> ~x - contains ternary(y, ~z, ~x)
|
||||
// look for ~x, y -> u - u is used in a ternary claues (~y, x)
|
||||
// look for ~x, y -> u - u is used in a ternary clause (~y, x)
|
||||
// look for y, u -> ~x - contains ternary(~u, ~x, ~y)
|
||||
// then ~x = if ~y then z else u
|
||||
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ Marijn's version:
|
|||
if inconsistent():
|
||||
learn C (subsumes C or p)
|
||||
else:
|
||||
candidates' := C union ~(consequencs of propagate(~C))
|
||||
candidates' := C union ~(consequences of propagate(~C))
|
||||
candidates := candidates' intersect candidates
|
||||
pop(1)
|
||||
for q in candidates:
|
||||
|
|
@ -77,7 +77,7 @@ Marijn's version:
|
|||
if inconsistent():
|
||||
learn C (subsumes C or p)
|
||||
else:
|
||||
candidates := candicates union C union ~(consequencs of propagate(~C))
|
||||
candidates := candidates union C union ~(consequences of propagate(~C))
|
||||
pop(1)
|
||||
for q in candidates:
|
||||
push(1)
|
||||
|
|
|
|||
|
|
@ -3462,7 +3462,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
// can't eliminat FUIP
|
||||
// can't eliminate FUIP
|
||||
SASSERT(is_marked_lit(m_lemma[0]));
|
||||
|
||||
unsigned j = 0;
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ class sat_smt_solver : public solver {
|
|||
ast_manager& m;
|
||||
trail_stack& m_trail;
|
||||
expr_ref_vector m_refs;
|
||||
obj_map<expr, expr*> m_dep2orig; // map original dependency to uninterpeted literal
|
||||
obj_map<expr, expr*> m_dep2orig; // map original dependency to uninterpreted literal
|
||||
|
||||
u_map<expr*> m_lit2dep; // map from literal assumption to original expression
|
||||
obj_map<expr, sat::literal> m_dep2lit; // map uninterpreted literal to sat literal
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ struct check_logic::imp {
|
|||
datatype_util m_dt_util;
|
||||
pb_util m_pb_util;
|
||||
bool m_uf; // true if the logic supports uninterpreted functions
|
||||
bool m_dt; // true if the lgoic supports dattypes
|
||||
bool m_dt; // true if the logic supports dattypes
|
||||
bool m_arrays; // true if the logic supports arbitrary arrays
|
||||
bool m_bv_arrays; // true if the logic supports only bv arrays
|
||||
bool m_reals; // true if the logic supports reals
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ void check_sat_result::set_reason_unknown(event_handler& eh) {
|
|||
switch (eh.caller_id()) {
|
||||
case UNSET_EH_CALLER:
|
||||
if (reason_unknown() == "")
|
||||
set_reason_unknown("unclassifed exception");
|
||||
set_reason_unknown("unclassified exception");
|
||||
break;
|
||||
case CTRL_C_EH_CALLER:
|
||||
set_reason_unknown("interrupted from keyboard");
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue