mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 02:45:51 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
db63c9299c
22 changed files with 161 additions and 115 deletions
|
|
@ -409,6 +409,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.
|
||||
################################################################################
|
||||
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 +448,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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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 {
|
||||
|
|
|
|||
|
|
@ -2515,7 +2515,7 @@ namespace Microsoft.Z3
|
|||
|
||||
|
||||
/// <summary>
|
||||
/// Concatentate sequences.
|
||||
/// Concatenate sequences.
|
||||
/// </summary>
|
||||
public SeqExpr MkConcat(params SeqExpr[] t)
|
||||
{
|
||||
|
|
@ -3597,7 +3597,7 @@ namespace Microsoft.Z3
|
|||
}
|
||||
|
||||
/// <summary>
|
||||
/// 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').
|
||||
/// </summary>
|
||||
public Tactic FailIfNotDecided()
|
||||
|
|
@ -4656,7 +4656,7 @@ namespace Microsoft.Z3
|
|||
/// Conversion of a floating-point term into a bit-vector.
|
||||
/// </summary>
|
||||
/// <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.
|
||||
/// </remarks>
|
||||
|
|
@ -4677,7 +4677,7 @@ namespace Microsoft.Z3
|
|||
/// Conversion of a floating-point term into a real-numbered term.
|
||||
/// </summary>
|
||||
/// <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.
|
||||
/// </remarks>
|
||||
|
|
@ -4696,7 +4696,7 @@ namespace Microsoft.Z3
|
|||
/// <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.
|
||||
/// </remarks>
|
||||
/// <param name="t">FloatingPoint term.</param>
|
||||
|
|
|
|||
|
|
@ -1978,7 +1978,7 @@ public class Context implements AutoCloseable {
|
|||
}
|
||||
|
||||
/**
|
||||
* Concatentate sequences.
|
||||
* Concatenate sequences.
|
||||
*/
|
||||
public SeqExpr mkConcat(SeqExpr... t)
|
||||
{
|
||||
|
|
@ -2781,7 +2781,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()
|
||||
|
|
@ -3769,7 +3769,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
|
||||
|
|
@ -3786,7 +3786,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
|
||||
|
|
@ -3802,7 +3802,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
|
||||
**/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)))
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -922,7 +922,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 +938,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 +953,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 +963,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 +974,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 +986,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 +997,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 +1010,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 +1022,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 +1035,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 +1046,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 +1186,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 +1205,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 +1227,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 +1253,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));
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -358,7 +358,7 @@ void rewriter_tpl<Config>::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());
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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"),
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
@ -8731,8 +8763,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;
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ Module Name:
|
|||
|
||||
Abstract:
|
||||
|
||||
Tactic expection object.
|
||||
Tactic exception object.
|
||||
|
||||
Author:
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue