", line)
- tgt.write(line);
- elif (not in_class and (s.startswith("{") or s.startswith("}"))) or s.startswith("[") or s.startswith("#"):
- # tgt.write("// Skipping: " + s)
- pass
- elif line == "}\n":
- pass
- else:
- # indent = line.find(s)
- # tgt.write("// LINE: " + line)
- if line.find(": base") != -1:
- line = re.sub(": base\((?P[^\{]*)\)", "{ super(\g
);", line)
- line = line[4:]
- obraces = line.count("{")
- cbraces = line.count("}")
- mbraces = obraces - cbraces
- # tgt.write("// obraces = " + str(obraces) + "\n")
- if obraces == 1:
- skip_brace = 1
- else:
- for i in range(0, mbraces):
- line = line.replace("\n", "}\n")
- if (s.find("public") != -1 or s.find("protected") != -1 or s.find("internal") != -1) and s.find("(") != -1:
- line = re.sub(" = [\w.]+(?P[,;\)])", "\g", line)
- a = type_replace(line)
- a = enum_replace(a)
- a = re.sub("(?P[\(, ])params ", "\g", a)
- a = a.replace("base.", "super.")
- a = re.sub("Contract.\w+\([\s\S]*\);", "", a)
- a = rename_native(a)
- a = re.sub("~\w+\(\)", "protected void finalize()", a)
-
- if missing_foreach_brace == 1:
- # a = a.replace("\n", " // checked " + str(foreach_opened_brace) + "\n")
- if foreach_opened_brace == 0 and a.find("{") != -1:
- foreach_opened_brace = 1
- elif foreach_opened_brace == 0 and a.find("}") == -1:
- a = a.replace("\n", "}}\n")
- foreach_opened_brace = 0
- missing_foreach_brace = 0
- elif foreach_opened_brace == 1 and a.find("}") != -1:
- a = a.replace("\n", "}}\n")
- foreach_opened_brace = 0
- missing_foreach_brace = 0
-
-# if a.find("foreach") != -1:
-# missing_foreach_brace = 1
-# a = re.sub("foreach\s*\((?P[\w <>,]+)\s+(?P\w+)\s+in\s+(?P\w+)\)",
- # "{ Iterator fe_i = \g.iterator(); while (fe_i.hasNext()) { \g \g = (long)fe_i.next(); ",
-# a)
- a = re.sub("foreach\s*\((?P[\w <>,]+)\s+(?P\w+)\s+in\s+(?P\w+)\)",
- "for (\g \g: \g)",
- a)
- if a.find("long o: m_queue") != -1:
- a = a.replace("long", "Long")
- a = a.replace("readonly ", "")
- a = a.replace("const ", "final ")
- a = a.replace("String ToString", "String toString")
- a = a.replace(".ToString", ".toString")
- a = a.replace("internal ", "")
- a = a.replace("new static", "static")
- a = a.replace("new public", "public")
- a = a.replace("override ", "")
- a = a.replace("virtual ", "")
- a = a.replace("o as AST", "(AST) o")
- a = a.replace("o as Sort", "(Sort) o")
- a = a.replace("other as AST", "(AST) other")
- a = a.replace("o as FuncDecl", "(FuncDecl) o")
- a = a.replace("IntPtr obj", "long obj")
- a = a.replace("IntPtr o", "long o")
- a = a.replace("new long()", "0")
- a = a.replace("long.Zero", "0")
- a = a.replace("object o", "Object o")
- a = a.replace("object other", "Object other")
- a = a.replace("IntPtr res = IntPtr.Zero;", "Native.IntPtr res = new Native.IntPtr();")
- a = a.replace("out res", "res")
- a = a.replace("GC.ReRegisterForFinalize(m_ctx);", "")
- a = a.replace("GC.SuppressFinalize(this);", "")
- a = a.replace(".Length", ".length")
- a = a.replace("m_queue.Count", "m_queue.size()")
- a = a.replace("m_queue.Add", "m_queue.add")
- a = a.replace("m_queue.Clear", "m_queue.clear")
- a = a.replace("for (long ", "for (int ")
- a = a.replace("ReferenceEquals(Context, ctx)", "Context() == ctx")
- a = a.replace("BigInteger.Parse", "new BigInteger")
- if had_ulong_res == 0 and a.find("ulong res = 0") != -1:
- a = a.replace("ulong res = 0;", "LongPtr res = new LongPtr();")
- elif had_ulong_res == 1:
- a = a.replace("ref res)", "res)")
- if a.find("return res;") != -1:
- a = a.replace("return res;", "return res.value;")
- had_ulong_res = 0
- a = a.replace("lock (", "synchronized (")
- if in_static_class:
- a = a.replace("static", "")
- a = re.sub("ref (?P\w+)", "\g", a)
- subst_getters(a, getters)
- a = re.sub("NativeObject = (?P.*);", "setNativeObject(\g);", a)
- a = replace_generals(a)
- tgt.write(a)
- tgt.close()
-
-mk_java_bindings()
diff --git a/src/api/ml/z3_theory_stubs.c b/src/api/ml/z3_theory_stubs.c
index d17a1790d..a48b94553 100644
--- a/src/api/ml/z3_theory_stubs.c
+++ b/src/api/ml/z3_theory_stubs.c
@@ -1,5 +1,5 @@
/*++
-Copyright (c) 2010 Microsoft Corporation
+Copyright (c) Microsoft Corporation
Module Name:
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 50d29a790..bb0212820 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -38,7 +38,7 @@ Z3 exceptions:
... n = x + y
... except Z3Exception as ex:
... print("failed: %s" % ex)
-failed: 'sort mismatch'
+failed: sort mismatch
"""
from z3core import *
from z3types import *
@@ -297,6 +297,11 @@ class AstRef(Z3PPObject):
"""Return a pointer to the corresponding C Z3_ast object."""
return self.ast
+ def get_id(self):
+ """Return unique identifier for object. It can be used for hash-tables and maps."""
+ return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
+
def ctx_ref(self):
"""Return a reference to the C context where this AST node is stored."""
return self.ctx.ref()
@@ -447,6 +452,10 @@ class SortRef(AstRef):
def as_ast(self):
return Z3_sort_to_ast(self.ctx_ref(), self.ast)
+ def get_id(self):
+ return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
+
def kind(self):
"""Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
@@ -585,6 +594,9 @@ class FuncDeclRef(AstRef):
def as_ast(self):
return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
+ def get_id(self):
+ return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
def as_func_decl(self):
return self.ast
@@ -730,6 +742,9 @@ class ExprRef(AstRef):
def as_ast(self):
return self.ast
+ def get_id(self):
+ return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
def sort(self):
"""Return the sort of expression `self`.
@@ -1383,7 +1398,7 @@ def BoolVector(prefix, sz, ctx=None):
return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
def FreshBool(prefix='b', ctx=None):
- """Return a fresh Bolean constant in the given context using the given prefix.
+ """Return a fresh Boolean constant in the given context using the given prefix.
If `ctx=None`, then the global context is used.
@@ -1524,6 +1539,9 @@ class PatternRef(ExprRef):
def as_ast(self):
return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
+ def get_id(self):
+ return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
def is_pattern(a):
"""Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
@@ -1586,6 +1604,9 @@ class QuantifierRef(BoolRef):
def as_ast(self):
return self.ast
+ def get_id(self):
+ return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
def sort(self):
"""Return the Boolean sort."""
return BoolSort(self.ctx)
@@ -3792,6 +3813,18 @@ def RepeatBitVec(n, a):
_z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
+def BVRedAnd(a):
+ """Return the reduction-and expression of `a`."""
+ if __debug__:
+ _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
+ return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
+
+def BVRedOr(a):
+ """Return the reduction-or expression of `a`."""
+ if __debug__:
+ _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
+ return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
+
#########################################
#
# Arrays
@@ -4448,7 +4481,7 @@ def args2params(arguments, keywords, ctx=None):
A ':' is added to the keywords, and '_' is replaced with '-'
>>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
- (params model 1 relevancy 2 elim_and 1)
+ (params model true relevancy 2 elim_and true)
"""
if __debug__:
_z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
@@ -6011,6 +6044,24 @@ class Solver(Z3PPObject):
"""
return Z3_solver_to_string(self.ctx.ref(), self.solver)
+ def to_smt2(self):
+ """return SMTLIB2 formatted benchmark for solver's assertions"""
+ es = self.assertions()
+ sz = len(es)
+ sz1 = sz
+ if sz1 > 0:
+ sz1 -= 1
+ v = (Ast * sz1)()
+ for i in range(sz1):
+ v[i] = es[i].as_ast()
+ if sz > 0:
+ e = es[sz1].as_ast()
+ else:
+ e = BoolVal(True, self.ctx).as_ast()
+ return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
+
+
+
def SolverFor(logic, ctx=None):
"""Create a solver customized for the given logic.
@@ -6127,7 +6178,7 @@ class Fixedpoint(Z3PPObject):
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
else:
body = _get_args(body)
- f = self.abstract(Implies(And(body),head))
+ f = self.abstract(Implies(And(body, self.ctx),head))
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def rule(self, head, body = None, name = None):
@@ -6155,7 +6206,7 @@ class Fixedpoint(Z3PPObject):
if sz == 1:
query = query[0]
else:
- query = And(query)
+ query = And(query, self.ctx)
query = self.abstract(query, False)
r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
return CheckSatResult(r)
@@ -6174,7 +6225,7 @@ class Fixedpoint(Z3PPObject):
name = ""
name = to_symbol(name, self.ctx)
body = _get_args(body)
- f = self.abstract(Implies(And(body),head))
+ f = self.abstract(Implies(And(body, self.ctx),head))
Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def get_answer(self):
@@ -6960,7 +7011,7 @@ def substitute(t, *m):
if isinstance(m, tuple):
m1 = _get_args(m)
if isinstance(m1, list):
- m = _get_args(m1)
+ m = m1
if __debug__:
_z3_assert(is_expr(t), "Z3 expression expected")
_z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
@@ -7253,19 +7304,19 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
dsz, dnames, ddecls = _dict2darray(decls, ctx)
return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
-def Interp(a,ctx=None):
+def Interpolant(a,ctx=None):
"""Create an interpolation operator.
The argument is an interpolation pattern (see tree_interpolant).
>>> x = Int('x')
- >>> print Interp(x>0)
+ >>> print Interpolant(x>0)
interp(x > 0)
"""
ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
s = BoolSort(ctx)
a = s.cast(a)
- return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx)
+ return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)
def tree_interpolant(pat,p=None,ctx=None):
"""Compute interpolant for a tree of formulas.
@@ -7304,10 +7355,10 @@ def tree_interpolant(pat,p=None,ctx=None):
>>> x = Int('x')
>>> y = Int('y')
- >>> print tree_interpolant(And(Interp(x < 0), Interp(y > 2), x == y))
+ >>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
[Not(x >= 0), Not(y <= 2)]
- >>> g = And(Interp(x<0),x<2)
+ >>> g = And(Interpolant(x<0),x<2)
>>> try:
... print tree_interpolant(g).sexpr()
... except ModelRef as m:
@@ -7342,11 +7393,11 @@ def binary_interpolant(a,b,p=None,ctx=None):
If parameters p are supplied, these are used in creating the
solver that determines satisfiability.
- >>> x = Int('x')
- >>> print binary_interpolant(x<0,x>2)
- x <= 2
+ x = Int('x')
+ print binary_interpolant(x<0,x>2)
+ Not(x >= 0)
"""
- f = And(Interp(a),b)
+ f = And(Interpolant(a),b)
return tree_interpolant(f,p,ctx)[0]
def sequence_interpolant(v,p=None,ctx=None):
@@ -7375,6 +7426,6 @@ def sequence_interpolant(v,p=None,ctx=None):
"""
f = v[0]
for i in range(1,len(v)):
- f = And(Interp(f),v[i])
+ f = And(Interpolant(f),v[i])
return tree_interpolant(f,p,ctx)
diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py
index 593312d68..5d59368ff 100644
--- a/src/api/python/z3types.py
+++ b/src/api/python/z3types.py
@@ -4,7 +4,7 @@ class Z3Exception(Exception):
def __init__(self, value):
self.value = value
def __str__(self):
- return repr(self.value)
+ return str(self.value)
class ContextObj(ctypes.c_void_p):
def __init__(self, context): self._as_parameter_ = context
diff --git a/src/api/z3.h b/src/api/z3.h
index db8becafd..2ebc20977 100644
--- a/src/api/z3.h
+++ b/src/api/z3.h
@@ -27,6 +27,7 @@ Notes:
#include"z3_algebraic.h"
#include"z3_polynomial.h"
#include"z3_rcf.h"
+#include"z3_interp.h"
#undef __in
#undef __out
diff --git a/src/api/z3_algebraic.h b/src/api/z3_algebraic.h
index eef791170..8b6d97aa8 100644
--- a/src/api/z3_algebraic.h
+++ b/src/api/z3_algebraic.h
@@ -23,7 +23,19 @@ Notes:
#ifdef __cplusplus
extern "C" {
-#endif // __cplusplus
+#endif // __cplusplus
+
+ /**
+ \defgroup capi C API
+
+ */
+
+ /*@{*/
+
+ /**
+ @name Algebraic Numbers API
+ */
+ /*@{*/
/**
\brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic
@@ -218,6 +230,8 @@ extern "C" {
*/
int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
+ /*@}*/
+ /*@}*/
#ifdef __cplusplus
};
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 4ffdfa9c2..71a6dde2b 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -771,7 +771,6 @@ typedef enum
The premises of the rules is a sequence of clauses.
The first clause argument is the main clause of the rule.
- One literal from the second, third, .. clause is resolved
with a literal from the first (main) clause.
Premises of the rules are of the form
@@ -1143,8 +1142,8 @@ typedef enum {
- Z3_FILE_ACCESS_ERRROR: A file could not be accessed.
- Z3_INVALID_USAGE: API call is invalid in the current state.
- Z3_INTERNAL_FATAL: An error internal to Z3 occurred.
- - Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized\mlonly.\endmlonly\conly with #Z3_inc_ref.
- - Z3_EXCEPTION: Internal Z3 exception. Additional details can be retrieved using \mlonly #Z3_get_error_msg. \endmlonly \conly #Z3_get_error_msg_ex.
+ - Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized \mlonly.\endmlonly \conly with #Z3_inc_ref.
+ - Z3_EXCEPTION: Internal Z3 exception. Additional details can be retrieved using #Z3_get_error_msg.
*/
typedef enum
{
@@ -1287,8 +1286,6 @@ extern "C" {
\sa Z3_global_param_set
- The caller must invoke #Z3_global_param_del_value to delete the value returned at \c param_value.
-
\remark This function cannot be invoked simultaneously from different threads without synchronization.
The result string stored in param_value is stored in shared location.
@@ -1462,15 +1459,6 @@ extern "C" {
*/
void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value);
- /**
- \brief Return the value of a context parameter.
-
- \sa Z3_global_param_get
-
- def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING)))
- */
- Z3_bool_opt Z3_API Z3_get_param_value(__in Z3_context c, __in Z3_string param_id, __out_opt Z3_string_ptr param_value);
-
#ifdef CorML4
/**
\brief Interrupt the execution of a Z3 procedure.
@@ -1779,7 +1767,7 @@ extern "C" {
Z3_sort Z3_API Z3_mk_tuple_sort(__in Z3_context c,
__in Z3_symbol mk_tuple_name,
__in unsigned num_fields,
- __in_ecount(num_fields) Z3_symbol const field_names[],
+ __in_ecount(num_fields) Z3_symbol const field_names[],
__in_ecount(num_fields) Z3_sort const field_sorts[],
__out Z3_func_decl * mk_tuple_decl,
__out_ecount(num_fields) Z3_func_decl proj_decl[]);
@@ -2116,17 +2104,7 @@ END_MLAPI_EXCLUDE
def_API('Z3_mk_not', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_not(__in Z3_context c, __in Z3_ast a);
-
- /**
- \brief \mlh mk_interp c a \endmlh
- Create an AST node marking a formula position for interpolation.
- The node \c a must have Boolean sort.
-
- def_API('Z3_mk_interp', AST, (_in(CONTEXT), _in(AST)))
- */
- Z3_ast Z3_API Z3_mk_interp(__in Z3_context c, __in Z3_ast a);
-
/**
\brief \mlh mk_ite c t1 t2 t2 \endmlh
Create an AST node representing an if-then-else: ite(t1, t2,
@@ -4010,6 +3988,12 @@ END_MLAPI_EXCLUDE
/**
\brief Return a unique identifier for \c t.
+ The identifier is unique up to structural equality. Thus, two ast nodes
+ created by the same context and having the same children and same function symbols
+ have the same identifiers. Ast nodes created in the same context, but having
+ different children or different functions have different identifiers.
+ Variables and quantifiers are also assigned different identifiers according to
+ their structure.
\mlonly \remark Implicitly used by [Pervasives.compare] for values of type [ast], [app], [sort], [func_decl], and [pattern]. \endmlonly
def_API('Z3_get_ast_id', UINT, (_in(CONTEXT), _in(AST)))
@@ -4018,6 +4002,8 @@ END_MLAPI_EXCLUDE
/**
\brief Return a hash code for the given AST.
+ The hash code is structural. You can use Z3_get_ast_id interchangably with
+ this function.
\mlonly \remark Implicitly used by [Hashtbl.hash] for values of type [ast], [app], [sort], [func_decl], and [pattern]. \endmlonly
def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST)))
@@ -4917,8 +4903,7 @@ END_MLAPI_EXCLUDE
__in_ecount(num_sorts) Z3_sort const sorts[],
__in unsigned num_decls,
__in_ecount(num_decls) Z3_symbol const decl_names[],
- __in_ecount(num_decls) Z3_func_decl const decls[]
- );
+ __in_ecount(num_decls) Z3_func_decl const decls[]);
/**
\brief Similar to #Z3_parse_smtlib2_string, but reads the benchmark from a file.
@@ -4927,13 +4912,12 @@ END_MLAPI_EXCLUDE
*/
Z3_ast Z3_API Z3_parse_smtlib2_file(__in Z3_context c,
__in Z3_string file_name,
- __in unsigned num_sorts,
- __in_ecount(num_sorts) Z3_symbol const sort_names[],
- __in_ecount(num_sorts) Z3_sort const sorts[],
- __in unsigned num_decls,
- __in_ecount(num_decls) Z3_symbol const decl_names[],
- __in_ecount(num_decls) Z3_func_decl const decls[]
- );
+ __in unsigned num_sorts,
+ __in_ecount(num_sorts) Z3_symbol const sort_names[],
+ __in_ecount(num_sorts) Z3_sort const sorts[],
+ __in unsigned num_decls,
+ __in_ecount(num_decls) Z3_symbol const decl_names[],
+ __in_ecount(num_decls) Z3_func_decl const decls[]);
#ifdef ML4only
#include
@@ -6620,6 +6604,13 @@ END_MLAPI_EXCLUDE
/**
\brief Create a new (incremental) solver.
+ The function #Z3_solver_get_model retrieves a model if the
+ assertions is satisfiable (i.e., the result is \c
+ Z3_L_TRUE) and model construction is enabled.
+ The function #Z3_solver_get_model can also be used even
+ if the result is \c Z3_L_UNDEF, but the returned model
+ is not guaranteed to satisfy quantified assertions.
+
def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),))
*/
Z3_solver Z3_API Z3_mk_simple_solver(__in Z3_context c);
@@ -6757,8 +6748,11 @@ END_MLAPI_EXCLUDE
\brief Check whether the assertions in a given solver are consistent or not.
The function #Z3_solver_get_model retrieves a model if the
- assertions are not unsatisfiable (i.e., the result is not \c
- Z3_L_FALSE) and model construction is enabled.
+ assertions is satisfiable (i.e., the result is \c
+ Z3_L_TRUE) and model construction is enabled.
+ Note that if the call returns Z3_L_UNDEF, Z3 does not
+ ensure that calls to #Z3_solver_get_model succeed and any models
+ produced in this case are not guaranteed to satisfy the assertions.
The function #Z3_solver_get_proof retrieves a proof if proof
generation was enabled when the context was created, and the
@@ -7069,7 +7063,7 @@ END_MLAPI_EXCLUDE
\mlonly then a valid model is returned. Otherwise, it is unsafe to use the returned model.\endmlonly
\conly The caller is responsible for deleting the model using the function #Z3_del_model.
- \conly \remark In constrast with the rest of the Z3 API, the reference counter of the
+ \conly \remark In contrast with the rest of the Z3 API, the reference counter of the
\conly model is incremented. This is to guarantee backward compatibility. In previous
\conly versions, models did not support reference counting.
@@ -7182,6 +7176,11 @@ END_MLAPI_EXCLUDE
\brief Delete a model object.
\sa Z3_check_and_get_model
+
+ \conly \remark The Z3_check_and_get_model automatically increments a reference count on the model.
+ \conly The expected usage is that models created by that method are deleted using Z3_del_model.
+ \conly This is for backwards compatibility and in contrast to the rest of the API where
+ \conly callers are responsible for managing reference counts.
\deprecated Subsumed by Z3_solver API
@@ -7685,314 +7684,6 @@ END_MLAPI_EXCLUDE
Z3_ast Z3_API Z3_get_context_assignment(__in Z3_context c);
/*@}*/
-
- /**
- @name Interpolation
- */
- /*@{*/
-
- /** \brief This function generates a Z3 context suitable for generation of
- interpolants. Formulas can be generated as abstract syntx trees in
- this context using the Z3 C API.
-
- Interpolants are also generated as AST's in this context.
-
- If cfg is non-null, it will be used as the base configuration
- for the Z3 context. This makes it possible to set Z3 options
- to be used during interpolation. This feature should be used
- with some caution however, as it may be that certain Z3 options
- are incompatible with interpolation.
-
- def_API('Z3_mk_interpolation_context', CONTEXT, (_in(CONFIG),))
-
- */
-
- Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
-
- /** Compute an interpolant from a refutation. This takes a proof of
- "false" from a set of formulas C, and an interpolation
- pattern. The pattern pat is a formula combining the formulas in C
- using logical conjunction and the "interp" operator (see
- #Z3_mk_interp). This interp operator is logically the identity
- operator. It marks the sub-formulas of the pattern for which interpolants should
- be computed. The interpolant is a map sigma from marked subformulas to
- formulas, such that, for each marked subformula phi of pat (where phi sigma
- is phi with sigma(psi) substituted for each subformula psi of phi such that
- psi in dom(sigma)):
-
- 1) phi sigma implies sigma(phi), and
-
- 2) sigma(phi) is in the common uninterpreted vocabulary between
- the formulas of C occurring in phi and those not occurring in
- phi
-
- and moreover pat sigma implies false. In the simplest case
- an interpolant for the pattern "(and (interp A) B)" maps A
- to an interpolant for A /\ B.
-
- The return value is a vector of formulas representing sigma. The
- vector contains sigma(phi) for each marked subformula of pat, in
- pre-order traversal. This means that subformulas of phi occur before phi
- in the vector. Also, subformulas that occur multiply in pat will
- occur multiply in the result vector.
-
- In particular, calling Z3_get_interpolant on a pattern of the
- form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will
- result in a sequence interpolant for A_1, A_2,... A_N.
-
- Neglecting interp markers, the pattern must be a conjunction of
- formulas in C, the set of premises of the proof. Otherwise an
- error is flagged.
-
- Any premises of the proof not present in the pattern are
- treated as "background theory". Predicate and function symbols
- occurring in the background theory are treated as interpreted and
- thus always allowed in the interpolant.
-
- 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
- supported, and the premises must be expressed using only
- theories and operators for which interpolation is supported.
-
- Currently, the only SMT solver that is supported is the legacy
- SMT solver. Such a solver is available as the default solver in
- #Z3_context objects produced by #Z3_mk_interpolation_context.
- Currently, the theories supported are equality with
- uninterpreted functions, linear integer arithmetic, and the
- theory of arrays (in SMT-LIB terms, this is AUFLIA).
- Quantifiers are allowed. Use of any other operators (including
- "labels") may result in failure to compute an interpolant from a
- proof.
-
- Parameters:
-
- \param c logical context.
- \param pf a refutation from premises (assertions) C
- \param pat an interpolation pattern over C
- \param p parameters
-
- def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS)))
- */
-
- Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p);
-
- /* Compute an interpolant for an unsatisfiable conjunction of formulas.
-
- This takes as an argument an interpolation pattern as in
- #Z3_get_interpolant. This is a conjunction, some subformulas of
- which are marked with the "interp" operator (see #Z3_mk_interp).
-
- The conjunction is first checked for unsatisfiability. The result
- of this check is returned in the out parameter "status". If the result
- is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
- and returned as a vector of formulas. Otherwise the return value is
- an empty formula.
-
- See #Z3_get_interpolant for a discussion of supported theories.
-
- The advantage of this function over #Z3_get_interpolant is that
- it is not necessary to create a suitable SMT solver and generate
- a proof. The disadvantage is that it is not possible to use the
- solver incrementally.
-
- Parameters:
-
- \param c logical context.
- \param pat an interpolation pattern
- \param p parameters for solver creation
- \param status returns the status of the sat check
- \param model returns model if satisfiable
-
- Return value: status of SAT check
-
- def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
- */
-
- Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp, __out Z3_model *model);
-
-
-/** Constant reprepresenting a root of a formula tree for tree interpolation */
-#define IZ3_ROOT SHRT_MAX
-
-/** This function uses Z3 to determine satisfiability of a set of
- constraints. If UNSAT, an interpolant is returned, based on the
- refutation generated by Z3. If SAT, a model is returned.
-
- If "parents" is non-null, computes a tree interpolant. The tree is
- defined by the array "parents". This array maps each formula in
- the tree to its parent, where formulas are indicated by their
- integer index in "cnsts". The parent of formula n must have index
- greater than n. The last formula is the root of the tree. Its
- parent entry should be the constant IZ3_ROOT.
-
- If "parents" is null, computes a sequence interpolant.
-
- \param ctx The Z3 context. Must be generated by iz3_mk_context
- \param num The number of constraints in the sequence
- \param cnsts Array of constraints (AST's in context ctx)
- \param parents The parents vector defining the tree structure
- \param options Interpolation options (may be NULL)
- \param interps Array to return interpolants (size at least num-1, may be NULL)
- \param model Returns a Z3 model if constraints SAT (may be NULL)
- \param labels Returns relevant labels if SAT (may be NULL)
- \param incremental
-
- VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3
- context ctx. The model and interpolants returned are also
- in this context.
-
- The return code is as in Z3_check_assumptions, that is,
-
- Z3_L_FALSE = constraints UNSAT (interpolants returned)
- Z3_L_TRUE = constraints SAT (model returned)
- Z3_L_UNDEF = Z3 produced no result, or interpolation not possible
-
- Currently, this function supports integer and boolean variables,
- as well as arrays over these types, with linear arithmetic,
- uninterpreted functions and quantifiers over integers (that is
- AUFLIA). Interpolants are produced in AUFLIA. However, some
- uses of array operations may cause quantifiers to appear in the
- interpolants even when there are no quantifiers in the input formulas.
- Although quantifiers may appear in the input formulas, Z3 may give up in
- this case, returning Z3_L_UNDEF.
-
- If "incremental" is true, cnsts must contain exactly the set of
- formulas that are currently asserted in the context. If false,
- there must be no formulas currently asserted in the context.
- Setting "incremental" to true makes it posisble to incrementally
- add and remove constraints from the context until the context
- becomes UNSAT, at which point an interpolant is computed. Caution
- must be used, however. Before popping the context, if you wish to
- keep the interolant formulas, you *must* preserve them by using
- Z3_persist_ast. Also, if you want to simplify the interpolant
- formulas using Z3_simplify, you must first pop all of the
- assertions in the context (or use a different context). Otherwise,
- the formulas will be simplified *relative* to these constraints,
- which is almost certainly not what you want.
-
-
- Current limitations on tree interpolants. In a tree interpolation
- problem, each constant (0-ary function symbol) must occur only
- along one path from root to leaf. Function symbols (of arity > 0)
- are considered to have global scope (i.e., may appear in any
- interpolant formula).
-
-
- */
-
-
- Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,
- __in int num,
- __in_ecount(num) Z3_ast *cnsts,
- __in_ecount(num) unsigned *parents,
- __in Z3_params options,
- __out_ecount(num-1) Z3_ast *interps,
- __out Z3_model *model,
- __out Z3_literals *labels,
- __in int incremental,
- __in int num_theory,
- __in_ecount(num_theory) Z3_ast *theory);
-
- /** Return a string summarizing cumulative time used for
- interpolation. This string is purely for entertainment purposes
- and has no semantics.
-
- \param ctx The context (currently ignored)
-
- def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),))
- */
-
- Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx);
-
- /**
- \brief Read an interpolation problem from file.
-
- \param ctx The Z3 context. This resets the error handler of ctx.
- \param filename The file name to read.
- \param num Returns length of sequence.
- \param cnsts Returns sequence of formulas (do not free)
- \param parents Returns the parents vector (or NULL for sequence)
- \param error Returns an error message in case of failure (do not free the string)
-
- Returns true on success.
-
- File formats: Currently two formats are supported, based on
- SMT-LIB2. For sequence interpolants, the sequence of constraints is
- represented by the sequence of "assert" commands in the file.
-
- For tree interpolants, one symbol of type bool is associated to
- each vertex of the tree. For each vertex v there is an "assert"
- of the form:
-
- (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
- 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
- valuation of the vertices that makes all the implications true
- where each value is represented using the common symbols between
- the formulas in the subtree and the remainder of the formulas.
-
- */
-
-
- int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx,
- __out int *num,
- __out_ecount(*num) Z3_ast **cnsts,
- __out_ecount(*num) int **parents,
- __in const char *filename,
- __out const char **error,
- __out int *num_theory,
- __out_ecount(*num_theory) Z3_ast **theory);
-
-
-
- /** Check the correctness of an interpolant. The Z3 context must
- have no constraints asserted when this call is made. That means
- that after interpolating, you must first fully pop the Z3
- context before calling this. See Z3_interpolate for meaning of parameters.
-
- \param ctx The Z3 context. Must be generated by Z3_mk_interpolation_context
- \param num The number of constraints in the sequence
- \param cnsts Array of constraints (AST's in context ctx)
- \param parents The parents vector (or NULL for sequence)
- \param interps The interpolant to check
- \param error Returns an error message if interpolant incorrect (do not free the string)
-
- Return value is Z3_L_TRUE if interpolant is verified, Z3_L_FALSE if
- incorrect, and Z3_L_UNDEF if unknown.
-
- */
-
- int Z3_API Z3_check_interpolant(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, Z3_ast *interps, const char **error,
- int num_theory, Z3_ast *theory);
-
- /** Write an interpolation problem to file suitable for reading with
- Z3_read_interpolation_problem. The output file is a sequence
- of SMT-LIB2 format commands, suitable for reading with command-line Z3
- or other interpolating solvers.
-
- \param ctx The Z3 context. Must be generated by z3_mk_interpolation_context
- \param num The number of constraints in the sequence
- \param cnsts Array of constraints
- \param parents The parents vector (or NULL for sequence)
- \param filename The file name to write
-
- */
-
- void Z3_API Z3_write_interpolation_problem(Z3_context ctx,
- int num,
- Z3_ast *cnsts,
- int *parents,
- const char *filename,
- int num_theory,
- Z3_ast *theory);
-
-
-
#endif
diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h
new file mode 100644
index 000000000..6ae26c0ed
--- /dev/null
+++ b/src/api/z3_interp.h
@@ -0,0 +1,293 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+ z3_interp.h
+
+Abstract:
+
+ API for interpolation
+
+Author:
+
+ Kenneth McMillan (kenmcmil)
+
+Notes:
+
+--*/
+#ifndef _Z3_INTERPOLATION_H_
+#define _Z3_INTERPOLATION_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif // __cplusplus
+
+ /**
+ \defgroup capi C API
+
+ */
+
+ /*@{*/
+
+ /**
+ @name Interpolation API
+ */
+ /*@{*/
+
+ /**
+ \brief \mlh mk_interp c a \endmlh
+ Create an AST node marking a formula position for interpolation.
+
+ The node \c a must have Boolean sort.
+
+ def_API('Z3_mk_interpolant', AST, (_in(CONTEXT), _in(AST)))
+ */
+ Z3_ast Z3_API Z3_mk_interpolant(__in Z3_context c, __in Z3_ast a);
+
+
+ /** \brief This function generates a Z3 context suitable for generation of
+ interpolants. Formulas can be generated as abstract syntax trees in
+ this context using the Z3 C API.
+
+ Interpolants are also generated as AST's in this context.
+
+ If cfg is non-null, it will be used as the base configuration
+ for the Z3 context. This makes it possible to set Z3 options
+ to be used during interpolation. This feature should be used
+ with some caution however, as it may be that certain Z3 options
+ are incompatible with interpolation.
+
+ def_API('Z3_mk_interpolation_context', CONTEXT, (_in(CONFIG),))
+
+ */
+
+ Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
+
+ /** Compute an interpolant from a refutation. This takes a proof of
+ "false" from a set of formulas C, and an interpolation
+ pattern. The pattern pat is a formula combining the formulas in C
+ using logical conjunction and the "interp" operator (see
+ #Z3_mk_interpolant). This interp operator is logically the identity
+ operator. It marks the sub-formulas of the pattern for which interpolants should
+ be computed. The interpolant is a map sigma from marked subformulas to
+ formulas, such that, for each marked subformula phi of pat (where phi sigma
+ is phi with sigma(psi) substituted for each subformula psi of phi such that
+ psi in dom(sigma)):
+
+ 1) phi sigma implies sigma(phi), and
+
+ 2) sigma(phi) is in the common uninterpreted vocabulary between
+ the formulas of C occurring in phi and those not occurring in
+ phi
+
+ and moreover pat sigma implies false. In the simplest case
+ an interpolant for the pattern "(and (interp A) B)" maps A
+ to an interpolant for A /\ B.
+
+ The return value is a vector of formulas representing sigma. The
+ vector contains sigma(phi) for each marked subformula of pat, in
+ pre-order traversal. This means that subformulas of phi occur before phi
+ in the vector. Also, subformulas that occur multiply in pat will
+ occur multiply in the result vector.
+
+ In particular, calling Z3_get_interpolant on a pattern of the
+ form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will
+ result in a sequence interpolant for A_1, A_2,... A_N.
+
+ Neglecting interp markers, the pattern must be a conjunction of
+ formulas in C, the set of premises of the proof. Otherwise an
+ error is flagged.
+
+ Any premises of the proof not present in the pattern are
+ treated as "background theory". Predicate and function symbols
+ occurring in the background theory are treated as interpreted and
+ thus always allowed in the interpolant.
+
+ 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
+ supported, and the premises must be expressed using only
+ theories and operators for which interpolation is supported.
+
+ Currently, the only SMT solver that is supported is the legacy
+ SMT solver. Such a solver is available as the default solver in
+ #Z3_context objects produced by #Z3_mk_interpolation_context.
+ Currently, the theories supported are equality with
+ uninterpreted functions, linear integer arithmetic, and the
+ theory of arrays (in SMT-LIB terms, this is AUFLIA).
+ Quantifiers are allowed. Use of any other operators (including
+ "labels") may result in failure to compute an interpolant from a
+ proof.
+
+ Parameters:
+
+ \param c logical context.
+ \param pf a refutation from premises (assertions) C
+ \param pat an interpolation pattern over C
+ \param p parameters
+
+ def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS)))
+ */
+
+ Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p);
+
+ /* Compute an interpolant for an unsatisfiable conjunction of formulas.
+
+ This takes as an argument an interpolation pattern as in
+ #Z3_get_interpolant. This is a conjunction, some subformulas of
+ which are marked with the "interp" operator (see #Z3_mk_interpolant).
+
+ The conjunction is first checked for unsatisfiability. The result
+ of this check is returned in the out parameter "status". If the result
+ is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
+ and returned as a vector of formulas. Otherwise the return value is
+ an empty formula.
+
+ See #Z3_get_interpolant for a discussion of supported theories.
+
+ The advantage of this function over #Z3_get_interpolant is that
+ it is not necessary to create a suitable SMT solver and generate
+ a proof. The disadvantage is that it is not possible to use the
+ solver incrementally.
+
+ Parameters:
+
+ \param c logical context.
+ \param pat an interpolation pattern
+ \param p parameters for solver creation
+ \param status returns the status of the sat check
+ \param model returns model if satisfiable
+
+ Return value: status of SAT check
+
+ def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
+ */
+
+ Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c,
+ __in Z3_ast pat,
+ __in Z3_params p,
+ __out Z3_ast_vector *interp,
+ __out Z3_model *model);
+
+ /** Return a string summarizing cumulative time used for
+ interpolation. This string is purely for entertainment purposes
+ and has no semantics.
+
+ \param ctx The context (currently ignored)
+
+
+ def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),))
+ */
+
+ Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx);
+
+ /**
+ \brief Read an interpolation problem from file.
+
+ \param ctx The Z3 context. This resets the error handler of ctx.
+ \param filename The file name to read.
+ \param num Returns length of sequence.
+ \param cnsts Returns sequence of formulas (do not free)
+ \param parents Returns the parents vector (or NULL for sequence)
+ \param error Returns an error message in case of failure (do not free the string)
+ \param num_theory Number of theory terms
+ \param theory Theory terms
+
+ Returns true on success.
+
+ File formats: Currently two formats are supported, based on
+ SMT-LIB2. For sequence interpolants, the sequence of constraints is
+ represented by the sequence of "assert" commands in the file.
+
+ For tree interpolants, one symbol of type bool is associated to
+ each vertex of the tree. For each vertex v there is an "assert"
+ of the form:
+
+ (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
+ 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
+ valuation of the vertices that makes all the implications true
+ where each value is represented using the common symbols between
+ the formulas in the subtree and the remainder of the formulas.
+
+ def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out_managed_array(1, AST), _out_managed_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out_managed_array(6, AST)))
+
+ */
+
+ int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx,
+ __out unsigned *num,
+ __out Z3_ast *cnsts[],
+ __out unsigned *parents[],
+ __in Z3_string filename,
+ __out_opt Z3_string_ptr error,
+ __out unsigned *num_theory,
+ __out Z3_ast *theory[]);
+
+
+
+ /** Check the correctness of an interpolant. The Z3 context must
+ have no constraints asserted when this call is made. That means
+ that after interpolating, you must first fully pop the Z3
+ context before calling this. See Z3_interpolate for meaning of parameters.
+
+ \param ctx The Z3 context. Must be generated by Z3_mk_interpolation_context
+ \param num The number of constraints in the sequence
+ \param cnsts Array of constraints (AST's in context ctx)
+ \param parents The parents vector (or NULL for sequence)
+ \param interps The interpolant to check
+ \param error Returns an error message if interpolant incorrect (do not free the string)
+ \param num_theory Number of theory terms
+ \param theory Theory terms
+
+ Return value is Z3_L_TRUE if interpolant is verified, Z3_L_FALSE if
+ incorrect, and Z3_L_UNDEF if unknown.
+
+ def_API('Z3_check_interpolant', INT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in_array(1, AST), _out(STRING), _in(UINT), _in_array(6, AST)))
+ */
+
+ int Z3_API Z3_check_interpolant(__in Z3_context ctx,
+ __in unsigned num,
+ __in_ecount(num) Z3_ast cnsts[],
+ __in_ecount(num) unsigned parents[],
+ __in_ecount(num - 1) Z3_ast *interps,
+ __out_opt Z3_string_ptr error,
+ __in unsigned num_theory,
+ __in_ecount(num_theory) Z3_ast theory[]);
+
+ /** Write an interpolation problem to file suitable for reading with
+ Z3_read_interpolation_problem. The output file is a sequence
+ of SMT-LIB2 format commands, suitable for reading with command-line Z3
+ or other interpolating solvers.
+
+ \param ctx The Z3 context. Must be generated by z3_mk_interpolation_context
+ \param num The number of constraints in the sequence
+ \param cnsts Array of constraints
+ \param parents The parents vector (or NULL for sequence)
+ \param filename The file name to write
+ \param num_theory Number of theory terms
+ \param theory Theory terms
+
+ def_API('Z3_write_interpolation_problem', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(STRING), _in(UINT), _in_array(5, AST)))
+ */
+
+ void Z3_API Z3_write_interpolation_problem(__in Z3_context ctx,
+ __in unsigned num,
+ __in_ecount(num) Z3_ast cnsts[],
+ __in_ecount(num) unsigned parents[],
+ __in Z3_string filename,
+ __in unsigned num_theory,
+ __in_ecount(num_theory) Z3_ast theory[]);
+
+ /*@}*/
+ /*@}*/
+
+#ifdef __cplusplus
+};
+#endif // __cplusplus
+
+#endif
diff --git a/src/api/z3_polynomial.h b/src/api/z3_polynomial.h
index 614e654f9..f55a63dd4 100644
--- a/src/api/z3_polynomial.h
+++ b/src/api/z3_polynomial.h
@@ -24,6 +24,19 @@ Notes:
extern "C" {
#endif // __cplusplus
+ /**
+ \defgroup capi C API
+
+ */
+
+ /*@{*/
+
+
+ /**
+ @name Polynomials API
+ */
+ /*@{*/
+
/**
\brief Return the nonzero subresultants of \c p and \c q with respect to the "variable" \c x.
@@ -38,6 +51,9 @@ extern "C" {
Z3_ast_vector Z3_API Z3_polynomial_subresultants(__in Z3_context c, __in Z3_ast p, __in Z3_ast q, __in Z3_ast x);
+ /*@}*/
+ /*@}*/
+
#ifdef __cplusplus
};
#endif // __cplusplus
diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h
index e2b4b7e05..04fe40253 100644
--- a/src/api/z3_rcf.h
+++ b/src/api/z3_rcf.h
@@ -25,6 +25,18 @@ Notes:
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
+
+ /**
+ \defgroup capi C API
+
+ */
+
+ /*@{*/
+
+ /**
+ @name Real Closed Fields API
+ */
+ /*@{*/
/**
\brief Delete a RCF numeral created using the RCF API.
@@ -192,6 +204,9 @@ extern "C" {
*/
void Z3_API Z3_rcf_get_numerator_denominator(__in Z3_context c, __in Z3_rcf_num a, __out Z3_rcf_num * n, __out Z3_rcf_num * d);
+ /*@}*/
+ /*@}*/
+
#ifdef __cplusplus
};
#endif // __cplusplus
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 68f7596ee..09965be85 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1013,6 +1013,17 @@ func_decl * basic_decl_plugin::mk_ite_decl(sort * s) {
return m_ite_decls[id];
}
+sort* basic_decl_plugin::join(sort* s1, sort* s2) {
+ if (s1 == s2) return s1;
+ if (s1->get_family_id() == m_manager->m_arith_family_id &&
+ s2->get_family_id() == m_manager->m_arith_family_id) {
+ if (s1->get_decl_kind() == REAL_SORT) {
+ return s1;
+ }
+ }
+ return s2;
+}
+
func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
switch (static_cast(k)) {
@@ -1025,10 +1036,10 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;
- case OP_ITE: return arity == 3 ? mk_ite_decl(domain[1]) : 0;
+ case OP_ITE: return arity == 3 ? mk_ite_decl(join(domain[1], domain[2])) : 0;
// eq and oeq must have at least two arguments, they can have more since they are chainable
- case OP_EQ: return arity >= 2 ? mk_eq_decl_core("=", OP_EQ, domain[0], m_eq_decls) : 0;
- case OP_OEQ: return arity >= 2 ? mk_eq_decl_core("~", OP_OEQ, domain[0], m_oeq_decls) : 0;
+ case OP_EQ: return arity >= 2 ? mk_eq_decl_core("=", OP_EQ, join(domain[0],domain[1]), m_eq_decls) : 0;
+ case OP_OEQ: return arity >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(domain[0],domain[1]), m_oeq_decls) : 0;
case OP_DISTINCT: {
func_decl_info info(m_family_id, OP_DISTINCT);
info.set_pairwise();
@@ -1061,10 +1072,12 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;
- case OP_ITE: return num_args == 3 ? mk_ite_decl(m_manager->get_sort(args[1])): 0;
+ case OP_ITE: return num_args == 3 ? mk_ite_decl(join(m_manager->get_sort(args[1]), m_manager->get_sort(args[2]))): 0;
// eq and oeq must have at least two arguments, they can have more since they are chainable
- case OP_EQ: return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, m_manager->get_sort(args[0]), m_eq_decls) : 0;
- case OP_OEQ: return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, m_manager->get_sort(args[0]), m_oeq_decls) : 0;
+ case OP_EQ: return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, join(m_manager->get_sort(args[0]),
+ m_manager->get_sort(args[1])), m_eq_decls) : 0;
+ case OP_OEQ: return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(m_manager->get_sort(args[0]),
+ m_manager->get_sort(args[1])), m_oeq_decls) : 0;
case OP_DISTINCT:
return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
default:
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 68f08e1ac..93f456965 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1100,6 +1100,7 @@ protected:
virtual void set_manager(ast_manager * m, family_id id);
func_decl * mk_eq_decl_core(char const * name, decl_kind k, sort * s, ptr_vector & cache);
func_decl * mk_ite_decl(sort * s);
+ sort* join(sort* s1, sort* s2);
public:
basic_decl_plugin();
@@ -1378,7 +1379,7 @@ enum proof_gen_mode {
// -----------------------------------
class ast_manager {
-protected:
+ friend class basic_decl_plugin;
protected:
struct config {
typedef ast_manager value_manager;
diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp
index df26422c8..f51101d79 100644
--- a/src/ast/float_decl_plugin.cpp
+++ b/src/ast/float_decl_plugin.cpp
@@ -40,11 +40,10 @@ void float_decl_plugin::set_manager(ast_manager * m, family_id id) {
SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before float_decl_plugin.
m_manager->inc_ref(m_int_sort);
- if (m_manager->has_plugin(symbol("bv"))) {
- // bv plugin is optional, so m_bv_plugin may be 0
+ // BV is not optional anymore.
+ SASSERT(m_manager->has_plugin(symbol("bv")));
m_bv_fid = m_manager->mk_family_id("bv");
m_bv_plugin = static_cast(m_manager->get_plugin(m_bv_fid));
- }
}
float_decl_plugin::~float_decl_plugin() {
@@ -103,6 +102,18 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) {
m_fm.mk_nan(ebits, sbits, val);
return true;
}
+ else if (is_app_of(n, m_family_id, OP_FLOAT_PLUS_ZERO)) {
+ unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int();
+ unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int();
+ m_fm.mk_pzero(ebits, sbits, val);
+ return true;
+ }
+ else if (is_app_of(n, m_family_id, OP_FLOAT_MINUS_ZERO)) {
+ unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int();
+ unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int();
+ m_fm.mk_nzero(ebits, sbits, val);
+ return true;
+ }
return false;
}
@@ -156,7 +167,7 @@ sort * float_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) {
parameter ps[2] = { p1, p2 };
sort_size sz;
sz = sort_size::mk_very_big(); // TODO: refine
- return m_manager->mk_sort(symbol("FP"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps));
+ return m_manager->mk_sort(symbol("FloatingPoint"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps));
}
sort * float_decl_plugin::mk_rm_sort() {
@@ -176,6 +187,14 @@ sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
return mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
case ROUNDING_MODE_SORT:
return mk_rm_sort();
+ case FLOAT16_SORT:
+ return mk_float_sort(5, 11);
+ case FLOAT32_SORT:
+ return mk_float_sort(8, 24);
+ case FLOAT64_SORT:
+ return mk_float_sort(11, 53);
+ case FLOAT128_SORT:
+ return mk_float_sort(15, 133);
default:
m_manager->raise_exception("unknown floating point theory sort");
return 0;
@@ -229,17 +248,18 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par
unsigned ebits = s->get_parameter(0).get_int();
unsigned sbits = s->get_parameter(1).get_int();
scoped_mpf val(m_fm);
- if (k == OP_FLOAT_NAN) {
- m_fm.mk_nan(ebits, sbits, val);
+
+ switch (k)
+ {
+ case OP_FLOAT_NAN: m_fm.mk_nan(ebits, sbits, val);
SASSERT(m_fm.is_nan(val));
+ break;
+ case OP_FLOAT_MINUS_INF: m_fm.mk_ninf(ebits, sbits, val); break;
+ case OP_FLOAT_PLUS_INF: m_fm.mk_pinf(ebits, sbits, val); break;
+ case OP_FLOAT_MINUS_ZERO: m_fm.mk_nzero(ebits, sbits, val); break;
+ case OP_FLOAT_PLUS_ZERO: m_fm.mk_pzero(ebits, sbits, val); break;
}
- else if (k == OP_FLOAT_MINUS_INF) {
- m_fm.mk_ninf(ebits, sbits, val);
- }
- else {
- SASSERT(k == OP_FLOAT_PLUS_INF);
- m_fm.mk_pinf(ebits, sbits, val);
- }
+
return mk_value_decl(val);
}
@@ -248,14 +268,14 @@ func_decl * float_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_paramet
if (arity != 2)
m_manager->raise_exception("invalid number of arguments to floating point relation");
if (domain[0] != domain[1] || !is_float_sort(domain[0]))
- m_manager->raise_exception("sort mismatch");
+ m_manager->raise_exception("sort mismatch, expected equal FloatingPoint sorts as arguments");
symbol name;
switch (k) {
- case OP_FLOAT_EQ: name = "=="; break;
- case OP_FLOAT_LT: name = "<"; break;
- case OP_FLOAT_GT: name = ">"; break;
- case OP_FLOAT_LE: name = "<="; break;
- case OP_FLOAT_GE: name = ">="; break;
+ case OP_FLOAT_EQ: name = "fp.eq"; break;
+ case OP_FLOAT_LT: name = "fp.lt"; break;
+ case OP_FLOAT_GT: name = "fp.gt"; break;
+ case OP_FLOAT_LE: name = "fp.lte"; break;
+ case OP_FLOAT_GE: name = "fp.gte"; break;
default:
UNREACHABLE();
break;
@@ -270,17 +290,18 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param
if (arity != 1)
m_manager->raise_exception("invalid number of arguments to floating point relation");
if (!is_float_sort(domain[0]))
- m_manager->raise_exception("sort mismatch");
+ m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort");
symbol name;
switch (k) {
- case OP_FLOAT_IS_ZERO: name = "isZero"; break;
- case OP_FLOAT_IS_NZERO: name = "isNZero"; break;
- case OP_FLOAT_IS_PZERO: name = "isPZero"; break;
- case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus"; break;
- case OP_FLOAT_IS_NAN: name = "isNaN"; break;
- case OP_FLOAT_IS_INF: name = "isInfinite"; break;
- case OP_FLOAT_IS_NORMAL: name = "isNormal"; break;
- case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal"; break;
+ case OP_FLOAT_IS_ZERO: name = "fp.isZero"; break;
+ case OP_FLOAT_IS_NZERO: name = "fp.isNZero"; break;
+ case OP_FLOAT_IS_PZERO: name = "fp.isPZero"; break;
+ case OP_FLOAT_IS_NEGATIVE: name = "fp.isNegative"; break;
+ case OP_FLOAT_IS_POSITIVE: name = "fp.isPositive"; break;
+ case OP_FLOAT_IS_NAN: name = "fp.isNaN"; break;
+ case OP_FLOAT_IS_INF: name = "fp.isInfinite"; break;
+ case OP_FLOAT_IS_NORMAL: name = "fp.isNormal"; break;
+ case OP_FLOAT_IS_SUBNORMAL: name = "fp.isSubnormal"; break;
default:
UNREACHABLE();
break;
@@ -293,11 +314,11 @@ func_decl * float_decl_plugin::mk_unary_decl(decl_kind k, unsigned num_parameter
if (arity != 1)
m_manager->raise_exception("invalid number of arguments to floating point operator");
if (!is_float_sort(domain[0]))
- m_manager->raise_exception("sort mismatch");
+ m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort");
symbol name;
switch (k) {
- case OP_FLOAT_ABS: name = "abs"; break;
- case OP_FLOAT_UMINUS: name = "-"; break;
+ case OP_FLOAT_ABS: name = "fp.abs"; break;
+ case OP_FLOAT_NEG: name = "fp.neg"; break;
default:
UNREACHABLE();
break;
@@ -310,12 +331,12 @@ func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_paramete
if (arity != 2)
m_manager->raise_exception("invalid number of arguments to floating point operator");
if (domain[0] != domain[1] || !is_float_sort(domain[0]))
- m_manager->raise_exception("sort mismatch");
+ m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts");
symbol name;
switch (k) {
- case OP_FLOAT_REM: name = "remainder"; break;
- case OP_FLOAT_MIN: name = "min"; break;
- case OP_FLOAT_MAX: name = "max"; break;
+ case OP_FLOAT_REM: name = "fp.rem"; break;
+ case OP_FLOAT_MIN: name = "fp.min"; break;
+ case OP_FLOAT_MAX: name = "fp.max"; break;
default:
UNREACHABLE();
break;
@@ -327,14 +348,16 @@ func_decl * float_decl_plugin::mk_rm_binary_decl(decl_kind k, unsigned num_param
unsigned arity, sort * const * domain, sort * range) {
if (arity != 3)
m_manager->raise_exception("invalid number of arguments to floating point operator");
- if (!is_rm_sort(domain[0]) || domain[1] != domain[2] || !is_float_sort(domain[1]))
- m_manager->raise_exception("sort mismatch");
+ if (!is_rm_sort(domain[0]))
+ m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort");
+ if (domain[1] != domain[2] || !is_float_sort(domain[1]))
+ m_manager->raise_exception("sort mismatch, expected arguments 1 and 2 of equal FloatingPoint sorts");
symbol name;
switch (k) {
- case OP_FLOAT_ADD: name = "+"; break;
- case OP_FLOAT_SUB: name = "-"; break;
- case OP_FLOAT_MUL: name = "*"; break;
- case OP_FLOAT_DIV: name = "/"; break;
+ case OP_FLOAT_ADD: name = "fp.add"; break;
+ case OP_FLOAT_SUB: name = "fp.sub"; break;
+ case OP_FLOAT_MUL: name = "fp.mul"; break;
+ case OP_FLOAT_DIV: name = "fp.div"; break;
default:
UNREACHABLE();
break;
@@ -346,12 +369,14 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame
unsigned arity, sort * const * domain, sort * range) {
if (arity != 2)
m_manager->raise_exception("invalid number of arguments to floating point operator");
- if (!is_rm_sort(domain[0]) || !is_float_sort(domain[1]))
- m_manager->raise_exception("sort mismatch");
+ if (!is_rm_sort(domain[0]))
+ m_manager->raise_exception("sort mismatch, expected RoundingMode as first argument");
+ if (!is_float_sort(domain[1]))
+ m_manager->raise_exception("sort mismatch, expected FloatingPoint as second argument");
symbol name;
switch (k) {
- case OP_FLOAT_SQRT: name = "squareRoot"; break;
- case OP_FLOAT_ROUND_TO_INTEGRAL: name = "roundToIntegral"; break;
+ case OP_FLOAT_SQRT: name = "fp.sqrt"; break;
+ case OP_FLOAT_ROUND_TO_INTEGRAL: name = "fp.roundToIntegral"; break;
default:
UNREACHABLE();
break;
@@ -359,13 +384,15 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame
return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k));
}
-func_decl * float_decl_plugin::mk_fused_ma(decl_kind k, unsigned num_parameters, parameter const * parameters,
+func_decl * float_decl_plugin::mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 4)
m_manager->raise_exception("invalid number of arguments to fused_ma operator");
- if (!is_rm_sort(domain[0]) || domain[1] != domain[2] || domain[1] != domain[3] || !is_float_sort(domain[1]))
- m_manager->raise_exception("sort mismatch");
- symbol name("fusedMA");
+ if (!is_rm_sort(domain[0]))
+ m_manager->raise_exception("sort mismatch, expected RoundingMode as first argument");
+ if (domain[1] != domain[2] || domain[1] != domain[3] || !is_float_sort(domain[1]))
+ m_manager->raise_exception("sort mismatch, expected arguments 1,2,3 of equal FloatingPoint sort");
+ symbol name("fp.fma");
return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k));
}
@@ -375,12 +402,13 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
is_sort_of(domain[0], m_bv_fid, BV_SORT) &&
is_sort_of(domain[1], m_bv_fid, BV_SORT) &&
is_sort_of(domain[2], m_bv_fid, BV_SORT)) {
- // When the bv_decl_plugin is installed, then we know how to convert 3 bit-vectors into a float!
+ // 3 BVs -> 1 FP
sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1);
- symbol name("asFloat");
+ symbol name("fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) {
+ // 1 BV -> 1 FP
if (num_parameters != 2)
m_manager->raise_exception("invalid number of parameters to to_fp");
if (!parameters[0].is_int() || !parameters[1].is_int())
@@ -389,37 +417,67 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
int sbits = parameters[1].get_int();
sort * fp = mk_float_sort(ebits, sbits);
- symbol name("asFloat");
+ symbol name("to_fp");
+ return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
+ }
+ else if (m_bv_plugin && arity == 2 &&
+ is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
+ is_sort_of(domain[1], m_bv_fid, BV_SORT)) {
+ // Rounding + 1 BV -> 1 FP
+ if (num_parameters != 2)
+ m_manager->raise_exception("invalid number of parameters to to_fp");
+ if (!parameters[0].is_int() || !parameters[1].is_int())
+ m_manager->raise_exception("invalid parameter type to to_fp");
+ int ebits = parameters[0].get_int();
+ int sbits = parameters[1].get_int();
+
+ sort * fp = mk_float_sort(ebits, sbits);
+ symbol name("to_fp");
+ return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
+ }
+ else if (arity == 2 &&
+ is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
+ is_sort_of(domain[1], m_family_id, FLOAT_SORT)) {
+ // Rounding + 1 FP -> 1 FP
+ if (num_parameters != 2)
+ m_manager->raise_exception("invalid number of parameters to to_fp");
+ if (!parameters[0].is_int() || !parameters[1].is_int())
+ m_manager->raise_exception("invalid parameter type to to_fp");
+ int ebits = parameters[0].get_int();
+ int sbits = parameters[1].get_int();
+ if (!is_rm_sort(domain[0]))
+ m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort");
+ if (!is_sort_of(domain[1], m_family_id, FLOAT_SORT))
+ m_manager->raise_exception("sort mismatch, expected second argument of FloatingPoint sort");
+
+ sort * fp = mk_float_sort(ebits, sbits);
+ symbol name("to_fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else {
- // .. Otherwise we only know how to convert rationals/reals.
+ // 1 Real -> 1 FP
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
- m_manager->raise_exception("expecting two integer parameters to asFloat");
+ m_manager->raise_exception("expecting two integer parameters to to_fp");
if (arity != 2 && arity != 3)
- m_manager->raise_exception("invalid number of arguments to asFloat operator");
+ m_manager->raise_exception("invalid number of arguments to to_fp operator");
if (arity == 3 && domain[2] != m_int_sort)
- m_manager->raise_exception("sort mismatch");
- if (!is_rm_sort(domain[0]) ||
- !(domain[1] == m_real_sort || is_sort_of(domain[1], m_family_id, FLOAT_SORT)))
- m_manager->raise_exception("sort mismatch");
+ m_manager->raise_exception("sort mismatch, expected second argument of Int sort");
+ if (domain[1] != m_real_sort)
+ m_manager->raise_exception("sort mismatch, expected second argument of Real sort");
sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
- symbol name("asFloat");
+ symbol name("to_fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
}
-func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+func_decl * float_decl_plugin::mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
- if (!m_bv_plugin)
- m_manager->raise_exception("asIEEEBV unsupported; use a logic with BV support");
if (arity != 1)
m_manager->raise_exception("invalid number of arguments to asIEEEBV");
if (!is_float_sort(domain[0]))
- m_manager->raise_exception("sort mismatch");
-
- // When the bv_decl_plugin is installed, then we know how to convert a float to an IEEE bit-vector.
+ m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort");
+
unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int();
parameter ps[] = { parameter(float_sz) };
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
@@ -429,41 +487,34 @@ func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameter
func_decl * float_decl_plugin::mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
- if (!m_bv_plugin)
- m_manager->raise_exception("fp unsupported; use a logic with BV support");
if (arity != 3)
m_manager->raise_exception("invalid number of arguments to fp");
if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) ||
!is_sort_of(domain[1], m_bv_fid, BV_SORT) ||
!is_sort_of(domain[2], m_bv_fid, BV_SORT))
- m_manager->raise_exception("sort mismtach");
+ m_manager->raise_exception("sort mismatch");
sort * fp = mk_float_sort(domain[1]->get_parameter(0).get_int(), domain[2]->get_parameter(0).get_int() + 1);
symbol name("fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
}
-func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
+func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (!m_bv_plugin)
m_manager->raise_exception("to_fp_unsigned unsupported; use a logic with BV support");
if (arity != 2)
m_manager->raise_exception("invalid number of arguments to to_fp_unsigned");
if (is_rm_sort(domain[0]))
- m_manager->raise_exception("sort mismtach");
+ m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort");
if (!is_sort_of(domain[1], m_bv_fid, BV_SORT))
- m_manager->raise_exception("sort mismtach");
+ m_manager->raise_exception("sort mismatch, expected second argument of BV sort");
sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
- symbol name("to_fp_unsigned");
+ symbol name("fp.t_ubv");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
}
-func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
- unsigned arity, sort * const * domain, sort * range) {
- NOT_IMPLEMENTED_YET();
-}
-
func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
NOT_IMPLEMENTED_YET();
@@ -498,14 +549,15 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_FLOAT_IS_ZERO:
case OP_FLOAT_IS_NZERO:
case OP_FLOAT_IS_PZERO:
- case OP_FLOAT_IS_SIGN_MINUS:
+ case OP_FLOAT_IS_NEGATIVE:
+ case OP_FLOAT_IS_POSITIVE:
case OP_FLOAT_IS_NAN:
case OP_FLOAT_IS_INF:
case OP_FLOAT_IS_NORMAL:
case OP_FLOAT_IS_SUBNORMAL:
return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_ABS:
- case OP_FLOAT_UMINUS:
+ case OP_FLOAT_NEG:
return mk_unary_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_REM:
case OP_FLOAT_MIN:
@@ -517,20 +569,18 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_SUB:
if (arity == 1)
- return mk_unary_decl(OP_FLOAT_UMINUS, num_parameters, parameters, arity, domain, range);
+ return mk_unary_decl(OP_FLOAT_NEG, num_parameters, parameters, arity, domain, range);
else
return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_SQRT:
case OP_FLOAT_ROUND_TO_INTEGRAL:
return mk_rm_unary_decl(k, num_parameters, parameters, arity, domain, range);
- case OP_FLOAT_FUSED_MA:
- return mk_fused_ma(k, num_parameters, parameters, arity, domain, range);
- case OP_TO_IEEE_BV:
- return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
+ case OP_FLOAT_FMA:
+ return mk_fma(k, num_parameters, parameters, arity, domain, range);
+ case OP_FLOAT_TO_IEEE_BV:
+ return mk_float_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_FP:
return mk_from3bv(k, num_parameters, parameters, arity, domain, range);
- case OP_FLOAT_TO_FP_UNSIGNED:
- return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_TO_UBV:
return mk_to_ubv(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_TO_SBV:
@@ -544,8 +594,11 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
}
void float_decl_plugin::get_op_names(svector & op_names, symbol const & logic) {
- op_names.push_back(builtin_name("plusInfinity", OP_FLOAT_PLUS_INF));
- op_names.push_back(builtin_name("minusInfinity", OP_FLOAT_MINUS_INF));
+ // These are the operators from the final draft of the SMT FloatingPoint standard
+ op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF));
+ op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF));
+ op_names.push_back(builtin_name("+zero", OP_FLOAT_PLUS_ZERO));
+ op_names.push_back(builtin_name("-zero", OP_FLOAT_MINUS_ZERO));
op_names.push_back(builtin_name("NaN", OP_FLOAT_NAN));
op_names.push_back(builtin_name("roundNearestTiesToEven", OP_RM_NEAREST_TIES_TO_EVEN));
@@ -554,45 +607,6 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co
op_names.push_back(builtin_name("roundTowardNegative", OP_RM_TOWARD_NEGATIVE));
op_names.push_back(builtin_name("roundTowardZero", OP_RM_TOWARD_ZERO));
- op_names.push_back(builtin_name("+", OP_FLOAT_ADD));
- op_names.push_back(builtin_name("-", OP_FLOAT_SUB));
- op_names.push_back(builtin_name("/", OP_FLOAT_DIV));
- op_names.push_back(builtin_name("*", OP_FLOAT_MUL));
-
- op_names.push_back(builtin_name("abs", OP_FLOAT_ABS));
- op_names.push_back(builtin_name("remainder", OP_FLOAT_REM));
- op_names.push_back(builtin_name("fusedMA", OP_FLOAT_FUSED_MA));
- op_names.push_back(builtin_name("squareRoot", OP_FLOAT_SQRT));
- op_names.push_back(builtin_name("roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL));
-
- op_names.push_back(builtin_name("==", OP_FLOAT_EQ));
-
- op_names.push_back(builtin_name("<", OP_FLOAT_LT));
- op_names.push_back(builtin_name(">", OP_FLOAT_GT));
- op_names.push_back(builtin_name("<=", OP_FLOAT_LE));
- op_names.push_back(builtin_name(">=", OP_FLOAT_GE));
-
- op_names.push_back(builtin_name("isNaN", OP_FLOAT_IS_NAN));
- op_names.push_back(builtin_name("isInfinite", OP_FLOAT_IS_INF));
- op_names.push_back(builtin_name("isZero", OP_FLOAT_IS_ZERO));
- op_names.push_back(builtin_name("isNZero", OP_FLOAT_IS_NZERO));
- op_names.push_back(builtin_name("isPZero", OP_FLOAT_IS_PZERO));
- op_names.push_back(builtin_name("isNormal", OP_FLOAT_IS_NORMAL));
- op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL));
- op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS));
-
- op_names.push_back(builtin_name("min", OP_FLOAT_MIN));
- op_names.push_back(builtin_name("max", OP_FLOAT_MAX));
-
- op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT));
-
- if (m_bv_plugin)
- op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV));
-
- // These are the operators from the final draft of the SMT FloatingPoints standard
- op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF));
- op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF));
-
op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN));
op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY));
op_names.push_back(builtin_name("RTP", OP_RM_TOWARD_POSITIVE));
@@ -600,44 +614,47 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co
op_names.push_back(builtin_name("RTZ", OP_RM_TOWARD_ZERO));
op_names.push_back(builtin_name("fp.abs", OP_FLOAT_ABS));
- op_names.push_back(builtin_name("fp.neg", OP_FLOAT_UMINUS));
+ op_names.push_back(builtin_name("fp.neg", OP_FLOAT_NEG));
op_names.push_back(builtin_name("fp.add", OP_FLOAT_ADD));
op_names.push_back(builtin_name("fp.sub", OP_FLOAT_SUB));
op_names.push_back(builtin_name("fp.mul", OP_FLOAT_MUL));
op_names.push_back(builtin_name("fp.div", OP_FLOAT_DIV));
- op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FUSED_MA));
+ op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FMA));
op_names.push_back(builtin_name("fp.sqrt", OP_FLOAT_SQRT));
op_names.push_back(builtin_name("fp.rem", OP_FLOAT_REM));
- op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ));
+ op_names.push_back(builtin_name("fp.roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL));
+ op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN));
+ op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX));
op_names.push_back(builtin_name("fp.leq", OP_FLOAT_LE));
op_names.push_back(builtin_name("fp.lt", OP_FLOAT_LT));
op_names.push_back(builtin_name("fp.geq", OP_FLOAT_GE));
op_names.push_back(builtin_name("fp.gt", OP_FLOAT_GT));
+ op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ));
+
op_names.push_back(builtin_name("fp.isNormal", OP_FLOAT_IS_NORMAL));
op_names.push_back(builtin_name("fp.isSubnormal", OP_FLOAT_IS_SUBNORMAL));
op_names.push_back(builtin_name("fp.isZero", OP_FLOAT_IS_ZERO));
op_names.push_back(builtin_name("fp.isInfinite", OP_FLOAT_IS_INF));
op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN));
- op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN));
- op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX));
- op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT));
+ op_names.push_back(builtin_name("fp.isNegative", OP_FLOAT_IS_NEGATIVE));
+ op_names.push_back(builtin_name("fp.isPositive", OP_FLOAT_IS_POSITIVE));
- if (m_bv_plugin) {
- op_names.push_back(builtin_name("fp", OP_FLOAT_FP));
- op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED));
- op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV));
- op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV));
- }
+ op_names.push_back(builtin_name("fp", OP_FLOAT_FP));
+ op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV));
+ op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV));
- // op_names.push_back(builtin_name("fp.toReal", ?));
+ op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT));
}
void float_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) {
- sort_names.push_back(builtin_name("FP", FLOAT_SORT));
+ sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT));
sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT));
- // In the SMT FPA final draft, FP is called FloatingPoint
- sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT));
+ // The final theory supports three common FloatingPoint sorts
+ sort_names.push_back(builtin_name("Float16", FLOAT16_SORT));
+ sort_names.push_back(builtin_name("Float32", FLOAT32_SORT));
+ sort_names.push_back(builtin_name("Float64", FLOAT64_SORT));
+ sort_names.push_back(builtin_name("Float128", FLOAT128_SORT));
}
expr * float_decl_plugin::get_some_value(sort * s) {
@@ -661,6 +678,8 @@ bool float_decl_plugin::is_value(app * e) const {
case OP_FLOAT_VALUE:
case OP_FLOAT_PLUS_INF:
case OP_FLOAT_MINUS_INF:
+ case OP_FLOAT_PLUS_ZERO:
+ case OP_FLOAT_MINUS_ZERO:
case OP_FLOAT_NAN:
return true;
case OP_TO_FLOAT:
diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h
index 58c37080d..c7ec04932 100644
--- a/src/ast/float_decl_plugin.h
+++ b/src/ast/float_decl_plugin.h
@@ -27,7 +27,11 @@ Revision History:
enum float_sort_kind {
FLOAT_SORT,
- ROUNDING_MODE_SORT
+ ROUNDING_MODE_SORT,
+ FLOAT16_SORT,
+ FLOAT32_SORT,
+ FLOAT64_SORT,
+ FLOAT128_SORT
};
enum float_op_kind {
@@ -37,22 +41,23 @@ enum float_op_kind {
OP_RM_TOWARD_NEGATIVE,
OP_RM_TOWARD_ZERO,
-
OP_FLOAT_VALUE,
OP_FLOAT_PLUS_INF,
OP_FLOAT_MINUS_INF,
OP_FLOAT_NAN,
+ OP_FLOAT_PLUS_ZERO,
+ OP_FLOAT_MINUS_ZERO,
OP_FLOAT_ADD,
OP_FLOAT_SUB,
- OP_FLOAT_UMINUS,
+ OP_FLOAT_NEG,
OP_FLOAT_MUL,
OP_FLOAT_DIV,
OP_FLOAT_REM,
OP_FLOAT_ABS,
OP_FLOAT_MIN,
OP_FLOAT_MAX,
- OP_FLOAT_FUSED_MA, // x*y + z
+ OP_FLOAT_FMA, // x*y + z
OP_FLOAT_SQRT,
OP_FLOAT_ROUND_TO_INTEGRAL,
@@ -68,13 +73,14 @@ enum float_op_kind {
OP_FLOAT_IS_SUBNORMAL,
OP_FLOAT_IS_PZERO,
OP_FLOAT_IS_NZERO,
- OP_FLOAT_IS_SIGN_MINUS,
+ OP_FLOAT_IS_NEGATIVE,
+ OP_FLOAT_IS_POSITIVE,
OP_TO_FLOAT,
- OP_TO_IEEE_BV,
+ OP_FLOAT_TO_IEEE_BV,
OP_FLOAT_FP,
- OP_FLOAT_TO_FP_UNSIGNED,
+ OP_FLOAT_TO_FP,
OP_FLOAT_TO_UBV,
OP_FLOAT_TO_SBV,
OP_FLOAT_TO_REAL,
@@ -125,16 +131,14 @@ class float_decl_plugin : public decl_plugin {
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_rm_unary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
- func_decl * mk_fused_ma(decl_kind k, unsigned num_parameters, parameter const * parameters,
- unsigned arity, sort * const * domain, sort * range);
+ func_decl * mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters,
+ unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_float(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
- func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
- unsigned arity, sort * const * domain, sort * range);
+ func_decl * mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+ unsigned arity, sort * const * domain, sort * range);
func_decl * mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
- func_decl * mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
- unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
@@ -195,6 +199,7 @@ public:
family_id get_fid() const { return m_fid; }
family_id get_family_id() const { return m_fid; }
arith_util & au() { return m_a_util; }
+ float_decl_plugin & plugin() { return *m_plugin; }
sort * mk_float_sort(unsigned ebits, unsigned sbits);
sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); }
@@ -242,16 +247,16 @@ public:
app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); }
app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); }
app * mk_div(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_DIV, arg1, arg2, arg3); }
- app * mk_uminus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_UMINUS, arg1); }
+ app * mk_neg(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_NEG, arg1); }
app * mk_rem(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_REM, arg1, arg2); }
app * mk_max(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MAX, arg1, arg2); }
app * mk_min(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MIN, arg1, arg2); }
app * mk_abs(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1); }
app * mk_sqrt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_SQRT, arg1, arg2); }
app * mk_round(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); }
- app * mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) {
+ app * mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) {
expr * args[4] = { arg1, arg2, arg3, arg4 };
- return m().mk_app(m_fid, OP_FLOAT_FUSED_MA, 4, args);
+ return m().mk_app(m_fid, OP_FLOAT_FMA, 4, args);
}
app * mk_float_eq(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_EQ, arg1, arg2); }
@@ -267,11 +272,13 @@ public:
app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SUBNORMAL, arg1); }
app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NZERO, arg1); }
app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_PZERO, arg1); }
- app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); }
+ app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); }
+ app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_POSITIVE, arg1); }
+ app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); }
- bool is_uminus(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_UMINUS); }
+ bool is_neg(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_NEG); }
- app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_TO_IEEE_BV, arg1); }
+ app * mk_float_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_TO_IEEE_BV, arg1); }
};
#endif
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index d6f362902..c23de3bfa 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -136,12 +136,13 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
unsigned sbits = m_util.get_sbits(srt);
expr_ref sgn(m), s(m), e(m);
- sort_ref s_sgn(m), s_sig(m), s_exp(m);
- s_sgn = m_bv_util.mk_sort(1);
- s_sig = m_bv_util.mk_sort(sbits-1);
- s_exp = m_bv_util.mk_sort(ebits);
#ifdef Z3DEBUG
+ sort_ref s_sgn(m), s_sig(m), s_exp(m);
+ s_sgn = m_bv_util.mk_sort(1);
+ s_sig = m_bv_util.mk_sort(sbits - 1);
+ s_exp = m_bv_util.mk_sort(ebits);
+
std::string p("fpa2bv");
std::string name = f->get_name().str();
@@ -149,9 +150,17 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
s = m.mk_fresh_const((p + "_sig_" + name).c_str(), s_sig);
e = m.mk_fresh_const((p + "_exp_" + name).c_str(), s_exp);
#else
- sgn = m.mk_fresh_const(0, s_sgn);
- s = m.mk_fresh_const(0, s_sig);
- e = m.mk_fresh_const(0, s_exp);
+ expr_ref bv(m);
+ unsigned bv_sz = 1 + ebits + (sbits - 1);
+ bv = m.mk_fresh_const(0, m_bv_util.mk_sort(bv_sz));
+
+ sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv);
+ e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv);
+ s = m_bv_util.mk_extract(sbits - 2, 0, bv);
+
+ SASSERT(m_bv_util.get_bv_size(sgn) == 1);
+ SASSERT(m_bv_util.get_bv_size(s) == sbits-1);
+ SASSERT(m_bv_util.get_bv_size(e) == ebits);
#endif
mk_triple(sgn, s, e, result);
@@ -595,12 +604,12 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3);
expr_ref t(m);
- mk_uminus(f, 1, &args[2], t);
+ mk_neg(f, 1, &args[2], t);
expr * nargs[3] = { args[0], args[1], t };
mk_add(f, 3, nargs, result);
}
-void fpa2bv_converter::mk_uminus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
expr * sgn, * s, * e;
split(args[0], sgn, s, e);
@@ -906,7 +915,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
TRACE("fpa2bv_div", tout << "DIV = " << mk_ismt2_pp(result, m) << std::endl; );
}
-void fpa2bv_converter::mk_remainder(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
// Remainder is always exact, so there is no rounding mode.
@@ -1114,7 +1123,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
mk_triple(r_sgn, r_sig, r_exp, result);
}
-void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 4);
// fusedma means (x * y) + z
@@ -1835,9 +1844,18 @@ void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const
mk_is_denormal(args[0], result);
}
-void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+void fpa2bv_converter::mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
mk_is_neg(args[0], result);
+ TRACE("fpa2bv_is_negative", tout << "result = " << mk_ismt2_pp(result, m) << std::endl;);
+}
+
+void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+ SASSERT(num == 1);
+ expr_ref t1(m), t2(m);
+ mk_is_nan(args[0], t1);
+ mk_is_pos(args[0], t2);
+ result = m.mk_and(m.mk_not(t1), t2);
}
void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@@ -2123,7 +2141,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
expr * sgn, * s, * e;
- split(args[0], sgn, s, e);
+ split(args[0], sgn, s, e);
result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
}
@@ -2132,19 +2150,55 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e
mk_triple(args[0], args[2], args[1], result);
}
-void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
- NOT_IMPLEMENTED_YET();
-}
-
void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+ SASSERT(num == 2);
+ SASSERT(f->get_num_parameters() == 1);
+ SASSERT(f->get_parameter(0).is_int());
+
+ //unsigned ebits = m_util.get_ebits(f->get_range());
+ //unsigned sbits = m_util.get_sbits(f->get_range());
+ //int width = f->get_parameter(0).get_int();
+
+ //expr * rm = args[0];
+ //expr * x = args[1];
+
+ //expr * sgn, *s, *e;
+ //split(x, sgn, s, e);
+
NOT_IMPLEMENTED_YET();
}
void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+ SASSERT(num == 2);
+ SASSERT(f->get_num_parameters() == 1);
+ SASSERT(f->get_parameter(0).is_int());
+
+ //unsigned ebits = m_util.get_ebits(f->get_range());
+ //unsigned sbits = m_util.get_sbits(f->get_range());
+ //int width = f->get_parameter(0).get_int();
+
+ //expr * rm = args[0];
+ //expr * x = args[1];
+
+ //expr * sgn, *s, *e;
+ //split(x, sgn, s, e);
+
NOT_IMPLEMENTED_YET();
}
void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+ SASSERT(num == 1);
+
+ //unsigned ebits = m_util.get_ebits(f->get_range());
+ //unsigned sbits = m_util.get_sbits(f->get_range());
+ //int width = f->get_parameter(0).get_int();
+
+ //expr * rm = args[0];
+ //expr * x = args[1];
+
+ //expr * sgn, *s, *e;
+ //split(x, sgn, s, e);
+
NOT_IMPLEMENTED_YET();
}
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index dcb508ffd..eb539d8ae 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -94,14 +94,14 @@ public:
void mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
- void mk_uminus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+ void mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
- void mk_remainder(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+ void mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
- void mk_fusedma(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+ void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
@@ -114,7 +114,8 @@ public:
void mk_is_zero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
- void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+ void mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+ void mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index 225aad668..7a245b71a 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -65,8 +65,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("fpa2bv");
- if (memory::get_allocation_size() > m_max_memory)
- throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
return num_steps > m_max_steps;
}
@@ -117,17 +115,19 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE;
case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE;
case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE;
+ case OP_FLOAT_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
+ case OP_FLOAT_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE;
case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE;
case OP_FLOAT_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
case OP_FLOAT_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
- case OP_FLOAT_UMINUS: m_conv.mk_uminus(f, num, args, result); return BR_DONE;
+ case OP_FLOAT_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE;
case OP_FLOAT_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
case OP_FLOAT_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
- case OP_FLOAT_REM: m_conv.mk_remainder(f, num, args, result); return BR_DONE;
+ case OP_FLOAT_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE;
case OP_FLOAT_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FLOAT_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
case OP_FLOAT_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
- case OP_FLOAT_FUSED_MA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE;
+ case OP_FLOAT_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE;
case OP_FLOAT_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
case OP_FLOAT_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
case OP_FLOAT_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
@@ -142,18 +142,18 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
- case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
+ case OP_FLOAT_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE;
+ case OP_FLOAT_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE;
case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
- case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
+ case OP_FLOAT_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
- case OP_FLOAT_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
- throw tactic_exception("NYI");
+ NOT_IMPLEMENTED_YET();
}
}
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index b41aa2238..b579d698e 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -911,18 +911,34 @@ void bit_blaster_tpl::mk_shl(unsigned sz, expr * const * a_bits, expr * con
out_bits.push_back(a_bits[i]);
}
else {
- expr_ref_vector eqs(m());
- mk_eqs(sz, b_bits, eqs);
- for (unsigned i = 0; i < sz; i++) {
+ out_bits.append(sz, a_bits);
+
+ unsigned i = 0;
+ expr_ref_vector new_out_bits(m());
+ for (; i < sz; ++i) {
checkpoint();
- expr_ref out(m());
- mk_ite(eqs.get(i), a_bits[0], m().mk_false(), out);
- for (unsigned j = 1; j <= i; j++) {
+ unsigned shift_i = 1 << i;
+ if (shift_i >= sz) break;
+ for (unsigned j = 0; j < sz; ++j) {
expr_ref new_out(m());
- mk_ite(eqs.get(i - j), a_bits[j], out, new_out);
- out = new_out;
+ expr* a_j = m().mk_false();
+ if (shift_i <= j) a_j = out_bits[j-shift_i].get();
+ mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out);
+ new_out_bits.push_back(new_out);
}
- out_bits.push_back(out);
+ out_bits.reset();
+ out_bits.append(new_out_bits);
+ new_out_bits.reset();
+ }
+ expr_ref is_large(m());
+ is_large = m().mk_false();
+ for (; i < sz; ++i) {
+ mk_or(is_large, b_bits[i], is_large);
+ }
+ for (unsigned j = 0; j < sz; ++j) {
+ expr_ref new_out(m());
+ mk_ite(is_large, m().mk_false(), out_bits[j].get(), new_out);
+ out_bits[j] = new_out;
}
}
}
@@ -939,19 +955,32 @@ void bit_blaster_tpl::mk_lshr(unsigned sz, expr * const * a_bits, expr * co
out_bits.push_back(m().mk_false());
}
else {
- expr_ref_vector eqs(m());
- mk_eqs(sz, b_bits, eqs);
- out_bits.resize(sz);
- for (unsigned i = 0; i < sz; i++) {
+ out_bits.append(sz, a_bits);
+ unsigned i = 0;
+ for (; i < sz; ++i) {
checkpoint();
- expr_ref out(m());
- mk_ite(eqs.get(i), a_bits[sz-1], m().mk_false(), out);
- for (unsigned j = 1; j <= i; j++) {
+ expr_ref_vector new_out_bits(m());
+ unsigned shift_i = 1 << i;
+ if (shift_i >= sz) break;
+ for (unsigned j = 0; j < sz; ++j) {
expr_ref new_out(m());
- mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out);
- out = new_out;
+ expr* a_j = m().mk_false();
+ if (shift_i + j < sz) a_j = out_bits[j+shift_i].get();
+ mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out);
+ new_out_bits.push_back(new_out);
}
- out_bits.set(sz - i - 1, out);
+ out_bits.reset();
+ out_bits.append(new_out_bits);
+ }
+ expr_ref is_large(m());
+ is_large = m().mk_false();
+ for (; i < sz; ++i) {
+ mk_or(is_large, b_bits[i], is_large);
+ }
+ for (unsigned j = 0; j < sz; ++j) {
+ expr_ref new_out(m());
+ mk_ite(is_large, m().mk_false(), out_bits[j].get(), new_out);
+ out_bits[j] = new_out;
}
}
}
@@ -968,20 +997,32 @@ void bit_blaster_tpl::mk_ashr(unsigned sz, expr * const * a_bits, expr * co
out_bits.push_back(a_bits[sz-1]);
}
else {
- expr_ref_vector eqs(m());
- mk_eqs(sz, b_bits, eqs);
- out_bits.resize(sz);
- for (unsigned i = 0; i < sz; i++) {
+ out_bits.append(sz, a_bits);
+ unsigned i = 0;
+ for (; i < sz; ++i) {
checkpoint();
- expr_ref out(m());
- out = a_bits[sz-1];
- for (unsigned j = 1; j <= i; j++) {
+ expr_ref_vector new_out_bits(m());
+ unsigned shift_i = 1 << i;
+ if (shift_i >= sz) break;
+ for (unsigned j = 0; j < sz; ++j) {
expr_ref new_out(m());
- mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out);
- out = new_out;
+ expr* a_j = a_bits[sz-1];
+ if (shift_i + j < sz) a_j = out_bits[j+shift_i].get();
+ mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out);
+ new_out_bits.push_back(new_out);
}
- TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
- out_bits.set(sz - i - 1, out);
+ out_bits.reset();
+ out_bits.append(new_out_bits);
+ }
+ expr_ref is_large(m());
+ is_large = m().mk_false();
+ for (; i < sz; ++i) {
+ mk_or(is_large, b_bits[i], is_large);
+ }
+ for (unsigned j = 0; j < sz; ++j) {
+ expr_ref new_out(m());
+ mk_ite(is_large, a_bits[sz-1], out_bits[j].get(), new_out);
+ out_bits[j] = new_out;
}
}
}
diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp
index a4212d579..7dc34dd11 100644
--- a/src/ast/rewriter/float_rewriter.cpp
+++ b/src/ast/rewriter/float_rewriter.cpp
@@ -36,17 +36,17 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
br_status st = BR_FAILED;
SASSERT(f->get_family_id() == get_fid());
switch (f->get_decl_kind()) {
- case OP_TO_FLOAT: st = mk_to_float(f, num_args, args, result); break;
+ case OP_TO_FLOAT: st = mk_to_fp(f, num_args, args, result); break;
case OP_FLOAT_ADD: SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break;
case OP_FLOAT_SUB: SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break;
- case OP_FLOAT_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break;
+ case OP_FLOAT_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break;
case OP_FLOAT_MUL: SASSERT(num_args == 3); st = mk_mul(args[0], args[1], args[2], result); break;
case OP_FLOAT_DIV: SASSERT(num_args == 3); st = mk_div(args[0], args[1], args[2], result); break;
case OP_FLOAT_REM: SASSERT(num_args == 2); st = mk_rem(args[0], args[1], result); break;
case OP_FLOAT_ABS: SASSERT(num_args == 1); st = mk_abs(args[0], result); break;
case OP_FLOAT_MIN: SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break;
case OP_FLOAT_MAX: SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break;
- case OP_FLOAT_FUSED_MA: SASSERT(num_args == 4); st = mk_fused_ma(args[0], args[1], args[2], args[3], result); break;
+ case OP_FLOAT_FMA: SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break;
case OP_FLOAT_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break;
case OP_FLOAT_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round(args[0], args[1], result); break;
@@ -62,10 +62,10 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
case OP_FLOAT_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break;
case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;
case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
- case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break;
- case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
+ case OP_FLOAT_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break;
+ case OP_FLOAT_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break;
+ case OP_FLOAT_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
case OP_FLOAT_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break;
- case OP_FLOAT_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(args[0], args[1], result); break;
case OP_FLOAT_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break;
case OP_FLOAT_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break;
case OP_FLOAT_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
@@ -73,7 +73,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
return st;
}
-br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(f->get_num_parameters() == 2);
SASSERT(f->get_parameter(0).is_int());
SASSERT(f->get_parameter(1).is_int());
@@ -154,7 +154,7 @@ br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref
br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
// a - b = a + (-b)
- result = m_util.mk_add(arg1, arg2, m_util.mk_uminus(arg3));
+ result = m_util.mk_add(arg1, arg2, m_util.mk_neg(arg3));
return BR_REWRITE2;
}
@@ -188,7 +188,7 @@ br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref
return BR_FAILED;
}
-br_status float_rewriter::mk_uminus(expr * arg1, expr_ref & result) {
+br_status float_rewriter::mk_neg(expr * arg1, expr_ref & result) {
if (m_util.is_nan(arg1)) {
// -nan --> nan
result = arg1;
@@ -204,7 +204,7 @@ br_status float_rewriter::mk_uminus(expr * arg1, expr_ref & result) {
result = m_util.mk_plus_inf(m().get_sort(arg1));
return BR_DONE;
}
- if (m_util.is_uminus(arg1)) {
+ if (m_util.is_neg(arg1)) {
// - - a --> a
result = to_app(arg1)->get_arg(0);
return BR_DONE;
@@ -239,7 +239,7 @@ br_status float_rewriter::mk_abs(expr * arg1, expr_ref & result) {
return BR_DONE;
}
result = m().mk_ite(m_util.mk_is_sign_minus(arg1),
- m_util.mk_uminus(arg1),
+ m_util.mk_neg(arg1),
arg1);
return BR_REWRITE2;
}
@@ -284,7 +284,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
return BR_REWRITE_FULL;
}
-br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
+br_status float_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm());
@@ -480,7 +480,7 @@ br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) {
return BR_FAILED;
}
-br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) {
+br_status float_rewriter::mk_is_negative(expr * arg1, expr_ref & result) {
scoped_mpf v(m_util.fm());
if (m_util.is_value(arg1, v)) {
result = (m_util.fm().is_neg(v)) ? m().mk_true() : m().mk_false();
@@ -490,6 +490,17 @@ br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) {
return BR_FAILED;
}
+br_status float_rewriter::mk_is_positive(expr * arg1, expr_ref & result) {
+ scoped_mpf v(m_util.fm());
+ if (m_util.is_value(arg1, v)) {
+ result = (m_util.fm().is_neg(v) || m_util.fm().is_nan(v)) ? m().mk_false() : m().mk_true();
+ return BR_DONE;
+ }
+
+ return BR_FAILED;
+}
+
+
// This the SMT =
br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_util.fm()), v2(m_util.fm());
@@ -532,10 +543,6 @@ br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref
return BR_FAILED;
}
-br_status float_rewriter::mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result) {
- return BR_FAILED;
-}
-
br_status float_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) {
return BR_FAILED;
}
diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h
index 0f44d227c..4d8cec856 100644
--- a/src/ast/rewriter/float_rewriter.h
+++ b/src/ast/rewriter/float_rewriter.h
@@ -45,17 +45,16 @@ public:
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result);
- br_status mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
- br_status mk_uminus(expr * arg1, expr_ref & result);
+ br_status mk_neg(expr * arg1, expr_ref & result);
br_status mk_rem(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_abs(expr * arg1, expr_ref & result);
br_status mk_min(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_max(expr * arg1, expr * arg2, expr_ref & result);
- br_status mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result);
+ br_status mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result);
br_status mk_sqrt(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_round(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_float_eq(expr * arg1, expr * arg2, expr_ref & result);
@@ -70,10 +69,12 @@ public:
br_status mk_is_inf(expr * arg1, expr_ref & result);
br_status mk_is_normal(expr * arg1, expr_ref & result);
br_status mk_is_subnormal(expr * arg1, expr_ref & result);
- br_status mk_is_sign_minus(expr * arg1, expr_ref & result);
+ br_status mk_is_negative(expr * arg1, expr_ref & result);
+ br_status mk_is_positive(expr * arg1, expr_ref & result);
br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);
+ br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result);
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 5d19c53e3..0e2c8e781 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -73,6 +73,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_a_rw.updt_params(p);
m_bv_rw.updt_params(p);
m_ar_rw.updt_params(p);
+ m_f_rw.updt_params(p);
updt_local_params(p);
}
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 836ade9ce..a80c5bc6c 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -241,7 +241,6 @@ protected:
symbol m_produce_models;
symbol m_produce_assignments;
symbol m_produce_interpolants;
- symbol m_check_interpolants;
symbol m_regular_output_channel;
symbol m_diagnostic_output_channel;
symbol m_random_seed;
@@ -256,7 +255,6 @@ protected:
s == m_print_success || s == m_print_warning || s == m_expand_definitions ||
s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores ||
s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants ||
- s == m_check_interpolants ||
s == m_regular_output_channel || s == m_diagnostic_output_channel ||
s == m_random_seed || s == m_verbosity || s == m_global_decls;
}
@@ -275,7 +273,6 @@ public:
m_produce_models(":produce-models"),
m_produce_assignments(":produce-assignments"),
m_produce_interpolants(":produce-interpolants"),
- m_check_interpolants(":check-interpolants"),
m_regular_output_channel(":regular-output-channel"),
m_diagnostic_output_channel(":diagnostic-output-channel"),
m_random_seed(":random-seed"),
@@ -347,9 +344,6 @@ class set_option_cmd : public set_get_option_cmd {
check_not_initialized(ctx, m_produce_interpolants);
ctx.set_produce_interpolants(to_bool(value));
}
- else if (m_option == m_check_interpolants) {
- ctx.set_check_interpolants(to_bool(value));
- }
else if (m_option == m_produce_unsat_cores) {
check_not_initialized(ctx, m_produce_unsat_cores);
ctx.set_produce_unsat_cores(to_bool(value));
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index ce2838aba..ee5437bd6 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -314,8 +314,9 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_numeral_as_real(false),
m_ignore_check(false),
m_exit_on_error(false),
- m_manager(m),
+ m_manager(m),
m_own_manager(m == 0),
+ m_manager_initialized(false),
m_pmanager(0),
m_sexpr_manager(0),
m_regular("stdout", std::cout),
@@ -326,8 +327,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
install_core_tactic_cmds(*this);
install_interpolant_cmds(*this);
SASSERT(m != 0 || !has_manager());
- if (m)
- init_external_manager();
if (m_main_ctx) {
set_verbose_stream(diagnostic_stream());
}
@@ -397,10 +396,6 @@ void cmd_context::set_produce_interpolants(bool f) {
// set_solver_factory(mk_smt_solver_factory());
}
-void cmd_context::set_check_interpolants(bool f) {
- m_params.m_check_interpolants = f;
-}
-
bool cmd_context::produce_models() const {
return m_params.m_model;
}
@@ -414,10 +409,6 @@ bool cmd_context::produce_interpolants() const {
return m_params.m_proof;
}
-bool cmd_context::check_interpolants() const {
- return m_params.m_check_interpolants;
-}
-
bool cmd_context::produce_unsat_cores() const {
return m_params.m_unsat_core;
}
@@ -479,6 +470,16 @@ void cmd_context::register_plugin(symbol const & name, decl_plugin * p, bool ins
}
}
+void cmd_context::load_plugin(symbol const & name, bool install, svector& fids) {
+ family_id id = m_manager->get_family_id(name);
+ decl_plugin* p = m_manager->get_plugin(id);
+ if (install && p && fids.contains(id)) {
+ register_builtin_sorts(p);
+ register_builtin_ops(p);
+ }
+ fids.erase(id);
+}
+
bool cmd_context::logic_has_arith_core(symbol const & s) const {
return
s == "QF_LRA" ||
@@ -595,17 +596,26 @@ void cmd_context::init_manager_core(bool new_manager) {
register_builtin_sorts(basic);
register_builtin_ops(basic);
// the manager was created by the command context.
- register_plugin(symbol("arith"), alloc(arith_decl_plugin), logic_has_arith());
- register_plugin(symbol("bv"), alloc(bv_decl_plugin), logic_has_bv());
- register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array());
+ register_plugin(symbol("arith"), alloc(arith_decl_plugin), logic_has_arith());
+ register_plugin(symbol("bv"), alloc(bv_decl_plugin), logic_has_bv());
+ register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array());
register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype());
register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq());
register_plugin(symbol("float"), alloc(float_decl_plugin), logic_has_floats());
}
else {
- // the manager was created by an external module, we must register all plugins available in the manager.
+ // the manager was created by an external module
+ // we register all plugins available in the manager.
+ // unless the logic specifies otherwise.
svector fids;
m_manager->get_range(fids);
+ load_plugin(symbol("arith"), logic_has_arith(), fids);
+ load_plugin(symbol("bv"), logic_has_bv(), fids);
+ load_plugin(symbol("array"), logic_has_array(), fids);
+ load_plugin(symbol("datatype"), logic_has_datatype(), fids);
+ load_plugin(symbol("seq"), logic_has_seq(), fids);
+ load_plugin(symbol("float"), logic_has_floats(), fids);
+
svector::iterator it = fids.begin();
svector::iterator end = fids.end();
for (; it != end; ++it) {
@@ -628,12 +638,22 @@ void cmd_context::init_manager_core(bool new_manager) {
}
void cmd_context::init_manager() {
- SASSERT(m_manager == 0);
- SASSERT(m_pmanager == 0);
- m_check_sat_result = 0;
- m_manager = m_params.mk_ast_manager();
- m_pmanager = alloc(pdecl_manager, *m_manager);
- init_manager_core(true);
+ if (m_manager_initialized) {
+ // no-op
+ }
+ else if (m_manager) {
+ m_manager_initialized = true;
+ SASSERT(!m_own_manager);
+ init_external_manager();
+ }
+ else {
+ m_manager_initialized = true;
+ SASSERT(m_pmanager == 0);
+ m_check_sat_result = 0;
+ m_manager = m_params.mk_ast_manager();
+ m_pmanager = alloc(pdecl_manager, *m_manager);
+ init_manager_core(true);
+ }
}
void cmd_context::init_external_manager() {
@@ -1173,12 +1193,15 @@ void cmd_context::reset(bool finalize) {
if (m_own_manager) {
dealloc(m_manager);
m_manager = 0;
+ m_manager_initialized = false;
}
else {
// doesn't own manager... so it cannot be deleted
// reinit cmd_context if this is not a finalization step
if (!finalize)
init_external_manager();
+ else
+ m_manager_initialized = false;
}
}
if (m_sexpr_manager) {
@@ -1219,8 +1242,7 @@ void cmd_context::assert_expr(symbol const & name, expr * t) {
void cmd_context::push() {
m_check_sat_result = 0;
- if (!has_manager())
- init_manager();
+ init_manager();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
s.m_func_decls_stack_lim = m_func_decls_stack.size();
@@ -1340,8 +1362,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
return;
IF_VERBOSE(100, verbose_stream() << "(started \"check-sat\")" << std::endl;);
TRACE("before_check_sat", dump_assertions(tout););
- if (!has_manager())
- init_manager();
+ init_manager();
if (m_solver) {
m_check_sat_result = m_solver.get(); // solver itself stores the result.
m_solver->set_progress_callback(this);
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index e34975183..1c8dba21a 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -149,6 +149,7 @@ protected:
ast_manager * m_manager;
bool m_own_manager;
+ bool m_manager_initialized;
pdecl_manager * m_pmanager;
sexpr_manager * m_sexpr_manager;
check_logic m_check_logic;
@@ -213,6 +214,7 @@ protected:
void register_builtin_sorts(decl_plugin * p);
void register_builtin_ops(decl_plugin * p);
void register_plugin(symbol const & name, decl_plugin * p, bool install_names);
+ void load_plugin(symbol const & name, bool install_names, svector& fids);
void init_manager_core(bool new_manager);
void init_manager();
void init_external_manager();
@@ -279,7 +281,6 @@ public:
bool produce_models() const;
bool produce_proofs() const;
bool produce_interpolants() const;
- bool check_interpolants() const;
bool produce_unsat_cores() const;
bool well_sorted_check_enabled() const;
bool validate_model_enabled() const;
@@ -287,7 +288,6 @@ public:
void set_produce_unsat_cores(bool flag);
void set_produce_proofs(bool flag);
void set_produce_interpolants(bool flag);
- void set_check_interpolants(bool flag);
bool produce_assignments() const { return m_produce_assignments; }
void set_produce_assignments(bool flag) { m_produce_assignments = flag; }
void set_status(status st) { m_status = st; }
@@ -295,7 +295,7 @@ public:
std::string reason_unknown() const;
bool has_manager() const { return m_manager != 0; }
- ast_manager & m() const { if (!m_manager) const_cast(this)->init_manager(); return *m_manager; }
+ ast_manager & m() const { const_cast(this)->init_manager(); return *m_manager; }
virtual ast_manager & get_ast_manager() { return m(); }
pdecl_manager & pm() const { if (!m_pmanager) const_cast(this)->init_manager(); return *m_pmanager; }
sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp
index 0ec44e0cf..f87c8d264 100644
--- a/src/cmd_context/context_params.cpp
+++ b/src/cmd_context/context_params.cpp
@@ -61,9 +61,6 @@ void context_params::set(char const * param, char const * value) {
else if (p == "proof") {
set_bool(m_proof, param, value);
}
- else if (p == "check_interpolants") {
- set_bool(m_check_interpolants, param, value);
- }
else if (p == "model") {
set_bool(m_model, param, value);
}
@@ -86,7 +83,13 @@ void context_params::set(char const * param, char const * value) {
set_bool(m_smtlib2_compliant, param, value);
}
else {
- throw default_exception("unknown parameter '%s'", p.c_str());
+ param_descrs d;
+ collect_param_descrs(d);
+ std::stringstream strm;
+ strm << "unknown parameter '" << p << "'\n";
+ strm << "Legal parameters are:\n";
+ d.display(strm, 2, false, false);
+ throw default_exception(strm.str());
}
}
@@ -99,7 +102,6 @@ void context_params::updt_params(params_ref const & p) {
m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true));
m_auto_config = p.get_bool("auto_config", true);
m_proof = p.get_bool("proof", false);
- m_check_interpolants = p.get_bool("check_interpolants", false);
m_model = p.get_bool("model", true);
m_model_validate = p.get_bool("model_validate", false);
m_trace = p.get_bool("trace", false);
@@ -114,15 +116,18 @@ void context_params::collect_param_descrs(param_descrs & d) {
d.insert("well_sorted_check", CPK_BOOL, "type checker", "true");
d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
- d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
- d.insert("check_interpolants", CPK_BOOL, "check correctness of interpolants", "false");
- d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false");
d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
- d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");
d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false");
+ collect_solver_param_descrs(d);
+}
+
+void context_params::collect_solver_param_descrs(param_descrs & d) {
+ d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
+ d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
+ d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
}
params_ref context_params::merge_default_params(params_ref const & p) {
diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h
index 7271bb84f..506e559db 100644
--- a/src/cmd_context/context_params.h
+++ b/src/cmd_context/context_params.h
@@ -30,7 +30,6 @@ public:
bool m_auto_config;
bool m_proof;
bool m_interpolants;
- bool m_check_interpolants;
bool m_debug_ref_count;
bool m_trace;
std::string m_trace_file_name;
@@ -55,6 +54,8 @@ public:
*/
void get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled);
+ static void collect_solver_param_descrs(param_descrs & d);
+
/**
\brief Include in p parameters derived from this context_params.
These are parameters that are meaningful for tactics and solvers.
diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp
index cb83b52f6..42646a99d 100644
--- a/src/cmd_context/interpolant_cmds.cpp
+++ b/src/cmd_context/interpolant_cmds.cpp
@@ -65,7 +65,7 @@ static void show_interpolant_and_maybe_check(cmd_context & ctx,
s.cleanup();
// verify, for the paranoid...
- if(check || ctx.check_interpolants()){
+ if(check || interp_params(m_params).check()){
std::ostringstream err;
ast_manager &_m = ctx.m();
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 27014bca9..75d56928e 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -500,7 +500,7 @@ static tactic * mk_using_params(cmd_context & ctx, sexpr * n) {
symbol param_name = symbol(norm_param_name(c->get_symbol()).c_str());
c = n->get_child(i);
i++;
- switch (descrs.get_kind(param_name)) {
+ switch (descrs.get_kind_in_module(param_name)) {
case CPK_INVALID:
throw cmd_exception("invalid using-params combinator, unknown parameter ", param_name, c->get_line(), c->get_pos());
case CPK_BOOL:
diff --git a/src/duality/duality.h b/src/duality/duality.h
index c1c9797f3..04527450c 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -104,6 +104,8 @@ namespace Duality {
FuncDecl RenumberPred(const FuncDecl &f, int n);
+ FuncDecl NumberPred(const FuncDecl &f, int n);
+
Term ExtractStores(hash_map &memo, const Term &t, std::vector &cnstrs, hash_map &renaming);
@@ -488,9 +490,10 @@ protected:
std::vector Incoming;
Term dual;
Node *map;
+ unsigned recursion_bound;
Node(const FuncDecl &_Name, const Transformer &_Annotation, const Transformer &_Bound, const Transformer &_Underapprox, const Term &_dual, RPFP *_owner, int _number)
- : Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0;}
+ : Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0; recursion_bound = UINT_MAX;}
};
/** Create a node in the graph. The input is a term R(v_1...v_n)
@@ -775,6 +778,10 @@ protected:
struct Bad {
};
+ // thrown on more serious internal error
+ struct ReallyBad {
+ };
+
/** Pop a scope (see Push). Note, you cannot pop axioms. */
void Pop(int num_scopes);
@@ -829,7 +836,7 @@ protected:
#ifdef _WINDOWS
__declspec(dllexport)
#endif
- void FromClauses(const std::vector &clauses);
+ void FromClauses(const std::vector &clauses, const std::vector *bounds = 0);
void FromFixpointContext(fixedpoint fp, std::vector &queries);
@@ -902,6 +909,10 @@ protected:
int CumulativeDecisions();
+ void GreedyReduceNodes(std::vector &nodes);
+
+ check_result CheckWithConstrainedNodes(std::vector &posnodes,std::vector &negnodes);
+
solver &slvr(){
return *ls->slvr;
}
diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp
index d5dac0811..5bcda972a 100755
--- a/src/duality/duality_profiling.cpp
+++ b/src/duality/duality_profiling.cpp
@@ -125,8 +125,18 @@ namespace Duality {
void timer_stop(const char *name){
if(current->name != name || !current->parent){
+#if 0
std::cerr << "imbalanced timer_start and timer_stop";
exit(1);
+#endif
+ // in case we lost a timer stop due to an exception
+ while(current->name != name && current->parent)
+ current = current->parent;
+ if(current->parent){
+ current->time += (current_time() - current->start_time);
+ current = current->parent;
+ }
+ return;
}
current->time += (current_time() - current->start_time);
current = current->parent;
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index ef37dd8a2..cdc8fb3b2 100755
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -2643,6 +2643,10 @@ namespace Duality {
GetGroundLitsUnderQuants(memo,f.body(),res,1);
return;
}
+ if(f.is_var()){
+ // std::cout << "foo!\n";
+ return;
+ }
if(under && f.is_ground())
res.push_back(f);
}
@@ -2816,6 +2820,62 @@ namespace Duality {
}
}
+ void foobar(){
+ }
+
+ void RPFP::GreedyReduceNodes(std::vector &nodes){
+ std::vector lits;
+ for(unsigned i = 0; i < nodes.size(); i++){
+ Term b; std::vector v;
+ RedVars(nodes[i], b, v);
+ lits.push_back(!b);
+ expr bv = dualModel.eval(b);
+ if(eq(bv,ctx.bool_val(true))){
+ check_result res = slvr_check(lits.size(),&lits[0]);
+ if(res == unsat)
+ lits.pop_back();
+ else
+ foobar();
+ }
+ }
+ }
+
+ check_result RPFP::CheckWithConstrainedNodes(std::vector &posnodes,std::vector &negnodes){
+ timer_start("Check");
+ std::vector lits;
+ for(unsigned i = 0; i < posnodes.size(); i++){
+ Term b; std::vector v;
+ RedVars(posnodes[i], b, v);
+ lits.push_back(b);
+ }
+ for(unsigned i = 0; i < negnodes.size(); i++){
+ Term b; std::vector v;
+ RedVars(negnodes[i], b, v);
+ lits.push_back(!b);
+ }
+ check_result res = slvr_check(lits.size(),&lits[0]);
+ if(res == unsat && posnodes.size()){
+ lits.resize(posnodes.size());
+ res = slvr_check(lits.size(),&lits[0]);
+ }
+ dualModel = slvr().get_model();
+#if 0
+ if(!dualModel.null()){
+ std::cout << "posnodes called:\n";
+ for(unsigned i = 0; i < posnodes.size(); i++)
+ if(!Empty(posnodes[i]))
+ std::cout << posnodes[i]->Name.name() << "\n";
+ std::cout << "negnodes called:\n";
+ for(unsigned i = 0; i < negnodes.size(); i++)
+ if(!Empty(negnodes[i]))
+ std::cout << negnodes[i]->Name.name() << "\n";
+ }
+#endif
+ timer_stop("Check");
+ return res;
+ }
+
+
void RPFP_caching::FilterCore(std::vector &core, std::vector &full_core){
hash_set core_set;
std::copy(full_core.begin(),full_core.end(),std::inserter(core_set,core_set.begin()));
@@ -3009,10 +3069,14 @@ namespace Duality {
node->Annotation.SetEmpty();
hash_set *core = new hash_set;
core->insert(node->Outgoing->dual);
+ expr prev_annot = ctx.bool_val(false);
+ expr prev_impl = ctx.bool_val(false);
+ int repeated_case_count = 0;
while(1){
by_case_counter++;
is.push();
expr annot = !GetAnnotation(node);
+ Transformer old_annot = node->Annotation;
is.add(annot);
if(is.check() == unsat){
is.pop(1);
@@ -3020,56 +3084,70 @@ namespace Duality {
}
is.pop(1);
Push();
- ConstrainEdgeLocalized(node->Outgoing,is.get_implicant());
+ expr the_impl = is.get_implicant();
+ if(eq(the_impl,prev_impl)){
+ // std::cout << "got old implicant\n";
+ repeated_case_count++;
+ }
+ prev_impl = the_impl;
+ ConstrainEdgeLocalized(node->Outgoing,the_impl);
ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this?
- check_result foo = Check(root);
- if(foo != unsat){
- slvr().print("should_be_unsat.smt2");
- throw "should be unsat";
- }
- std::vector assumps, axioms_to_add;
- slvr().get_proof().get_assumptions(assumps);
- for(unsigned i = 0; i < assumps.size(); i++){
- (*core).insert(assumps[i]);
- if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
- axioms_to_add.push_back(assumps[i]);
- axioms_needed.erase(assumps[i]);
- }
- }
- // AddToProofCore(*core);
- Transformer old_annot = node->Annotation;
- SolveSingleNode(root,node);
-
- {
- expr itp = GetAnnotation(node);
- dualModel = is.get_model(); // TODO: what does this mean?
- std::vector case_lits;
- itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
- SetAnnotation(node,itp);
- node->Annotation.Formula = node->Annotation.Formula.simplify();
- }
-
- for(unsigned i = 0; i < axioms_to_add.size(); i++)
- is.add(axioms_to_add[i]);
-#define TEST_BAD
-#ifdef TEST_BAD
{
- static int bad_count = 0, num_bads = 1;
- if(bad_count >= num_bads){
- bad_count = 0;
- num_bads = num_bads * 2;
+ check_result foo = Check(root);
+ if(foo != unsat){
Pop(1);
is.pop(1);
delete core;
timer_stop("InterpolateByCases");
- throw Bad();
+ throw ReallyBad();
+ // slvr().print("should_be_unsat.smt2");
+ // throw "should be unsat";
}
- bad_count++;
- }
-#endif
+ std::vector assumps, axioms_to_add;
+ slvr().get_proof().get_assumptions(assumps);
+ for(unsigned i = 0; i < assumps.size(); i++){
+ (*core).insert(assumps[i]);
+ if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
+ axioms_to_add.push_back(assumps[i]);
+ axioms_needed.erase(assumps[i]);
+ }
+ }
+ // AddToProofCore(*core);
+ SolveSingleNode(root,node);
- if(node->Annotation.IsEmpty()){
+ {
+ expr itp = GetAnnotation(node);
+ dualModel = is.get_model(); // TODO: what does this mean?
+ std::vector case_lits;
+ itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
+ SetAnnotation(node,itp);
+ node->Annotation.Formula = node->Annotation.Formula.simplify();
+ }
+
+ for(unsigned i = 0; i < axioms_to_add.size(); i++)
+ is.add(axioms_to_add[i]);
+
+#define TEST_BAD
+#ifdef TEST_BAD
+ {
+ static int bad_count = 0, num_bads = 1;
+ if(bad_count >= num_bads){
+ bad_count = 0;
+ num_bads = num_bads * 2;
+ Pop(1);
+ is.pop(1);
+ delete core;
+ timer_stop("InterpolateByCases");
+ throw Bad();
+ }
+ bad_count++;
+ }
+#endif
+ }
+
+ if(node->Annotation.IsEmpty() || eq(node->Annotation.Formula,prev_annot) || (repeated_case_count > 0 && !axioms_added) || (repeated_case_count >= 10)){
+ looks_bad:
if(!axioms_added){
// add the axioms in the off chance they are useful
const std::vector &theory = ls->get_axioms();
@@ -3078,6 +3156,7 @@ namespace Duality {
axioms_added = true;
}
else {
+ //#define KILL_ON_BAD_INTERPOLANT
#ifdef KILL_ON_BAD_INTERPOLANT
std::cout << "bad in InterpolateByCase -- core:\n";
#if 0
@@ -3119,10 +3198,11 @@ namespace Duality {
is.pop(1);
delete core;
timer_stop("InterpolateByCases");
- throw Bad();
+ throw ReallyBad();
}
}
Pop(1);
+ prev_annot = node->Annotation.Formula;
node->Annotation.UnionWith(old_annot);
}
if(proof_core)
@@ -3333,6 +3413,17 @@ namespace Duality {
return ctx.function(name.c_str(), arity, &domain[0], f.range());
}
+ Z3User::FuncDecl Z3User::NumberPred(const FuncDecl &f, int n)
+ {
+ std::string name = f.name().str();
+ name = name + "_" + string_of_int(n);
+ int arity = f.arity();
+ std::vector domain;
+ for(int i = 0; i < arity; i++)
+ domain.push_back(f.domain(i));
+ return ctx.function(name.c_str(), arity, &domain[0], f.range());
+ }
+
// Scan the clause body for occurrences of the predicate unknowns
RPFP::Term RPFP::ScanBody(hash_map &memo,
@@ -3570,7 +3661,7 @@ namespace Duality {
#define USE_QE_LITE
- void RPFP::FromClauses(const std::vector &unskolemized_clauses){
+ void RPFP::FromClauses(const std::vector &unskolemized_clauses, const std::vector *bounds){
hash_map pmap;
func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort());
@@ -3663,6 +3754,7 @@ namespace Duality {
pmap[R] = node;
if (is_query)
node->Bound = CreateRelation(std::vector(), ctx.bool_val(false));
+ node->recursion_bound = bounds ? 0 : UINT_MAX;
}
}
@@ -3728,6 +3820,8 @@ namespace Duality {
Transformer T = CreateTransformer(Relparams,Indparams,body);
Edge *edge = CreateEdge(Parent,T,Children);
edge->labeled = labeled;; // remember for label extraction
+ if(bounds)
+ Parent->recursion_bound = std::max(Parent->recursion_bound,(*bounds)[i]);
// edges.push_back(edge);
}
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index 681582415..b40ab9370 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -33,6 +33,7 @@ Revision History:
#include