mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

fix box

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-15 14:29:39 -07:00
commit ce18421a7a
51 changed files with 1663 additions and 1117 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_ast.cpp
View file

@ -209,7 +209,7 @@ extern "C" {
MK_BINARY(Z3_mk_xor, mk_c(c)->get_basic_fid(), OP_XOR, SKIP);
MK_NARY(Z3_mk_and, mk_c(c)->get_basic_fid(), OP_AND, SKIP);
MK_NARY(Z3_mk_or, mk_c(c)->get_basic_fid(), OP_OR, SKIP);
MK_UNARY(Z3_mk_interp, mk_c(c)->get_basic_fid(), OP_INTERP, SKIP);
MK_UNARY(Z3_mk_interpolant, mk_c(c)->get_basic_fid(), OP_INTERP, SKIP);
Z3_ast mk_ite_core(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) {
expr * result = mk_c(c)->m().mk_ite(to_expr(t1), to_expr(t2), to_expr(t3));

1207
src/api/api_interp.cpp
View file

File diff suppressed because it is too large Load diff

12
src/api/api_solver.cpp
View file

@ -40,6 +40,11 @@ extern "C" {
params_ref p = s->m_params;
mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
param_descrs r;
s->m_solver->collect_param_descrs(r);
context_params::collect_solver_param_descrs(r);
p.validate(r);
s->m_solver->updt_params(p);
}
@ -102,6 +107,7 @@ extern "C" {
if (!initialized)
init_solver(c, s);
to_solver_ref(s)->collect_param_descrs(descrs);
context_params::collect_solver_param_descrs(descrs);
if (!initialized)
to_solver(s)->m_solver = 0;
descrs.display(buffer);
@ -119,6 +125,7 @@ extern "C" {
if (!initialized)
init_solver(c, s);
to_solver_ref(s)->collect_param_descrs(d->m_descrs);
context_params::collect_solver_param_descrs(d->m_descrs);
if (!initialized)
to_solver(s)->m_solver = 0;
Z3_param_descrs r = of_param_descrs(d);
@ -130,11 +137,16 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_set_params(c, s, p);
RESET_ERROR_CODE();
if (to_solver(s)->m_solver) {
bool old_model = to_solver(s)->m_params.get_bool("model", true);
bool new_model = to_param_ref(p).get_bool("model", true);
if (old_model != new_model)
to_solver_ref(s)->set_produce_models(new_model);
param_descrs r;
to_solver_ref(s)->collect_param_descrs(r);
context_params::collect_solver_param_descrs(r);
to_param_ref(p).validate(r);
to_solver_ref(s)->updt_params(to_param_ref(p));
}
to_solver(s)->m_params = to_param_ref(p);

3
src/api/api_tactic.cpp
View file

@ -450,6 +450,9 @@ extern "C" {
Z3_TRY;
LOG_Z3_tactic_apply_ex(c, t, g, p);
RESET_ERROR_CODE();
param_descrs pd;
to_tactic_ref(t)->collect_param_descrs(pd);
to_param_ref(p).validate(pd);
Z3_apply_result r = _tactic_apply(c, t, g, to_param_ref(p));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);

120
src/api/c++/z3++.h
View file

@ -85,6 +85,8 @@ namespace z3 {
friend std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
};
/**
\brief Z3 global configuration object.
*/
@ -269,8 +271,9 @@ namespace z3 {
object(object const & s):m_ctx(s.m_ctx) {}
context & ctx() const { return *m_ctx; }
void check_error() const { m_ctx->check_error(); }
friend void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); }
friend void check_context(object const & a, object const & b);
};
inline void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); }
class symbol : public object {
Z3_symbol m_sym;
@ -282,7 +285,7 @@ namespace z3 {
Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
friend std::ostream & operator<<(std::ostream & out, symbol const & s) {
friend std::ostream & operator<<(std::ostream & out, symbol const & s) {
if (s.kind() == Z3_INT_SYMBOL)
out << "k!" << s.to_int();
else
@ -291,6 +294,7 @@ namespace z3 {
}
};
class params : public object {
Z3_params m_params;
public:
@ -309,7 +313,9 @@ namespace z3 {
void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
friend std::ostream & operator<<(std::ostream & out, params const & p) { out << Z3_params_to_string(p.ctx(), p); return out; }
friend std::ostream & operator<<(std::ostream & out, params const & p) {
out << Z3_params_to_string(p.ctx(), p); return out;
}
};
class ast : public object {
@ -325,14 +331,19 @@ namespace z3 {
ast & operator=(ast const & s) { Z3_inc_ref(s.ctx(), s.m_ast); if (m_ast) Z3_dec_ref(ctx(), m_ast); m_ctx = s.m_ctx; m_ast = s.m_ast; return *this; }
Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
friend std::ostream & operator<<(std::ostream & out, ast const & n) { out << Z3_ast_to_string(n.ctx(), n.m_ast); return out; }
friend std::ostream & operator<<(std::ostream & out, ast const & n) {
out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
}
/**
\brief Return true if the ASTs are structurally identical.
*/
friend bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
friend bool eq(ast const & a, ast const & b);
};
inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
/**
\brief A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
*/
@ -570,6 +581,7 @@ namespace z3 {
return expr(a.ctx(), r);
}
/**
\brief Return an expression representing <tt>a and b</tt>.
@ -585,6 +597,7 @@ namespace z3 {
return expr(a.ctx(), r);
}
/**
\brief Return an expression representing <tt>a and b</tt>.
The C++ Boolean value \c b is automatically converted into a Z3 Boolean constant.
@ -636,21 +649,10 @@ namespace z3 {
a.check_error();
return expr(a.ctx(), r);
}
friend expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
friend expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
friend expr implies(expr const & a, bool b);
friend expr implies(bool a, expr const & b);
/**
\brief Create the if-then-else expression <tt>ite(c, t, e)</tt>
\pre c.is_bool()
*/
friend expr ite(expr const & c, expr const & t, expr const & e) {
check_context(c, t); check_context(c, e);
assert(c.is_bool());
Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
c.check_error();
return expr(c.ctx(), r);
}
friend expr ite(expr const & c, expr const & t, expr const & e);
friend expr distinct(expr_vector const& args);
@ -716,15 +718,9 @@ namespace z3 {
/**
\brief Power operator
*/
friend expr pw(expr const & a, expr const & b) {
assert(a.is_arith() && b.is_arith());
check_context(a, b);
Z3_ast r = Z3_mk_power(a.ctx(), a, b);
a.check_error();
return expr(a.ctx(), r);
}
friend expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
friend expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
friend expr pw(expr const & a, expr const & b);
friend expr pw(expr const & a, int b);
friend expr pw(int a, expr const & b);
friend expr operator/(expr const & a, expr const & b) {
check_context(a, b);
@ -891,6 +887,38 @@ namespace z3 {
expr substitute(expr_vector const& dst);
};
inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
inline expr pw(expr const & a, expr const & b) {
assert(a.is_arith() && b.is_arith());
check_context(a, b);
Z3_ast r = Z3_mk_power(a.ctx(), a, b);
a.check_error();
return expr(a.ctx(), r);
}
inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief Create the if-then-else expression <tt>ite(c, t, e)</tt>
\pre c.is_bool()
*/
inline expr ite(expr const & c, expr const & t, expr const & e) {
check_context(c, t); check_context(c, e);
assert(c.is_bool());
Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
c.check_error();
return expr(c.ctx(), r);
}
/**
\brief Wraps a Z3_ast as an expr object. It also checks for errors.
@ -1404,22 +1432,28 @@ namespace z3 {
t1.check_error();
return tactic(t1.ctx(), r);
}
friend tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
t.check_error();
return tactic(t.ctx(), r);
}
friend tactic with(tactic const & t, params const & p) {
Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
t.check_error();
return tactic(t.ctx(), r);
}
friend tactic try_for(tactic const & t, unsigned ms) {
Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
t.check_error();
return tactic(t.ctx(), r);
}
friend tactic repeat(tactic const & t, unsigned max);
friend tactic with(tactic const & t, params const & p);
friend tactic try_for(tactic const & t, unsigned ms);
};
inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
t.check_error();
return tactic(t.ctx(), r);
}
inline tactic with(tactic const & t, params const & p) {
Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
t.check_error();
return tactic(t.ctx(), r);
}
inline tactic try_for(tactic const & t, unsigned ms) {
Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
t.check_error();
return tactic(t.ctx(), r);
}
class probe : public object {
Z3_probe m_probe;

6
src/api/dotnet/Constructor.cs
View file

@ -50,7 +50,7 @@ namespace Microsoft.Z3
IntPtr constructor = IntPtr.Zero;
IntPtr tester = IntPtr.Zero;
IntPtr[] accessors = new IntPtr[n];
Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors);
return new FuncDecl(Context, constructor);
}
}
@ -66,7 +66,7 @@ namespace Microsoft.Z3
IntPtr constructor = IntPtr.Zero;
IntPtr tester = IntPtr.Zero;
IntPtr[] accessors = new IntPtr[n];
Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors);
return new FuncDecl(Context, tester);
}
}
@ -82,7 +82,7 @@ namespace Microsoft.Z3
IntPtr constructor = IntPtr.Zero;
IntPtr tester = IntPtr.Zero;
IntPtr[] accessors = new IntPtr[n];
Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors);
FuncDecl[] t = new FuncDecl[n];
for (uint i = 0; i < n; i++)
t[i] = new FuncDecl(Context, accessors[i]);

2
src/api/dotnet/Context.cs
View file

@ -424,7 +424,7 @@ namespace Microsoft.Z3
n_constr[i] = cla[i].NativeObject;
}
IntPtr[] n_res = new IntPtr[n];
Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), out n_res, n_constr);
DatatypeSort[] res = new DatatypeSort[n];
for (uint i = 0; i < n; i++)
res[i] = new DatatypeSort(this, n_res[i]);

2
src/api/dotnet/Deprecated.cs
View file

@ -78,7 +78,7 @@ namespace Microsoft.Z3
IntPtr[] native_core = new IntPtr[assumptions.Length];
r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx,
(uint)assumptions.Length, AST.ArrayToNative(assumptions),
ref mdl, ref prf, ref core_size, native_core);
ref mdl, ref prf, ref core_size, out native_core);
for (uint i = 0; i < core_size; i++)
core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));

2
src/api/dotnet/EnumSort.cs
View file

@ -88,7 +88,7 @@ namespace Microsoft.Z3
IntPtr[] n_constdecls = new IntPtr[n];
IntPtr[] n_testers = new IntPtr[n];
NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
Symbol.ArrayToNative(enumNames), out n_constdecls, out n_testers);
}
#endregion
};

10
src/api/dotnet/Expr.cs
View file

@ -323,6 +323,14 @@ namespace Microsoft.Z3
#endregion
#region Interpolation
/// <summary>
/// Indicates whether the term is marked for interpolation.
/// </summary>
/// <remarks></remarks>
public bool IsInterpolant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INTERP; } }
#endregion
#region Arithmetic Terms
/// <summary>
/// Indicates whether the term is of integer sort.
@ -791,7 +799,7 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>A label literal has a set of string parameters. It takes no arguments.</remarks>
public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
#endregion
#endregion
#region Proof Terms
/// <summary>

162
src/api/dotnet/InterpolationContext.cs Normal file
View file

@ -0,0 +1,162 @@
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
using System.Runtime.InteropServices;
namespace Microsoft.Z3
{
/// <summary>
/// The InterpolationContext is suitable for generation of interpolants.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the C/C++ API, which is well documented.</remarks>
[ContractVerification(true)]
class InterpolationContext : Context
{
/// <summary>
/// Constructor.
/// </summary>
public InterpolationContext() : base() { }
/// <summary>
/// Constructor.
/// </summary>
/// <remarks><seealso cref="Context.Context(Dictionary&lt;string, string&gt;)"/></remarks>
public InterpolationContext(Dictionary<string, string> settings) : base(settings) { }
#region Terms
/// <summary>
/// Create an expression that marks a formula position for interpolation.
/// </summary>
public BoolExpr MkInterpolant(BoolExpr a)
{
Contract.Requires(a != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(a);
return new BoolExpr(this, Native.Z3_mk_interpolant(nCtx, a.NativeObject));
}
#endregion
/// <summary>
/// Computes an interpolant.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_get_interpolant in the C/C++ API, which is
/// well documented.</remarks>
Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
{
Contract.Requires(pf != null);
Contract.Requires(pat != null);
Contract.Requires(p != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(pf);
CheckContextMatch(pat);
CheckContextMatch(p);
ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
uint n = seq.Size;
Expr[] res = new Expr[n];
for (uint i = 0; i < n; i++)
res[i] = Expr.Create(this, seq[i].NativeObject);
return res;
}
/// <summary>
/// Computes an interpolant.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_compute_interpolant in the C/C++ API, which is
/// well documented.</remarks>
Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
{
Contract.Requires(pat != null);
Contract.Requires(p != null);
Contract.Ensures(Contract.ValueAtReturn(out interp) != null);
Contract.Ensures(Contract.ValueAtReturn(out model) != null);
CheckContextMatch(pat);
CheckContextMatch(p);
IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
interp = new ASTVector(this, i);
model = new Model(this, m);
return (Z3_lbool)r;
}
/// <summary>
/// Return a string summarizing cumulative time used for interpolation.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_interpolation_profile in the C/C++ API, which is
/// well documented.</remarks>
public string InterpolationProfile()
{
return Native.Z3_interpolation_profile(nCtx);
}
/// <summary>
/// Checks the correctness of an interpolant.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_check_interpolant in the C/C++ API, which is
/// well documented.</remarks>
public int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory)
{
Contract.Requires(cnsts.Length == parents.Length);
Contract.Requires(cnsts.Length == interps.Length + 1);
IntPtr n_err_str;
int r = Native.Z3_check_interpolant(nCtx,
(uint)cnsts.Length,
Expr.ArrayToNative(cnsts),
parents,
Expr.ArrayToNative(interps),
out n_err_str,
(uint)theory.Length,
Expr.ArrayToNative(theory));
error = Marshal.PtrToStringAnsi(n_err_str);
return r;
}
/// <summary>
/// Reads an interpolation problem from a file.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_read_interpolation_problem in the C/C++ API, which is
/// well documented.</remarks>
public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory)
{
uint num = 0, num_theory = 0;
IntPtr[] n_cnsts;
IntPtr[] n_theory;
IntPtr n_err_str;
int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out n_theory);
error = Marshal.PtrToStringAnsi(n_err_str);
cnsts = new Expr[num];
parents = new uint[num];
theory = new Expr[num_theory];
for (int i = 0; i < num; i++)
cnsts[i] = Expr.Create(this, n_cnsts[i]);
for (int i = 0; i < num_theory; i++)
theory[i] = Expr.Create(this, n_theory[i]);
return r;
}
/// <summary>
/// Writes an interpolation problem to a file.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_write_interpolation_problem in the C/C++ API, which is
/// well documented.</remarks>
public void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory)
{
Contract.Requires(cnsts.Length == parents.Length);
Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length, Expr.ArrayToNative(theory));
}
}
}

9
src/api/dotnet/Microsoft.Z3.csproj
View file

@ -19,12 +19,12 @@
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
<OutputPath>..\Debug\</OutputPath>
<OutputPath>..\..\..\..\..\cwinter\bugs\z3bugs\Debug\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\Debug\Microsoft.Z3.XML</DocumentationFile>
<DocumentationFile>C:\cwinter\bugs\z3bugs\Debug\Microsoft.Z3.XML</DocumentationFile>
<CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
@ -254,7 +254,7 @@
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">
<DebugSymbols>true</DebugSymbols>
<OutputPath>bin\x86\Debug\</OutputPath>
<OutputPath>..\..\..\..\..\cwinter\bugs\z3bugs\Debug\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DebugType>full</DebugType>
@ -266,7 +266,7 @@
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<DocumentationFile>bin\x86\Debug\Microsoft.Z3.XML</DocumentationFile>
<DocumentationFile>C:\cwinter\bugs\z3bugs\Debug\Microsoft.Z3.XML</DocumentationFile>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">
<OutputPath>bin\x86\Release\</OutputPath>
@ -352,6 +352,7 @@
<Compile Include="FuncDecl.cs" />
<Compile Include="FuncInterp.cs" />
<Compile Include="Goal.cs" />
<Compile Include="InterpolationContext.cs" />
<Compile Include="IntExpr.cs" />
<Compile Include="IntNum.cs" />
<Compile Include="IntSort.cs" />

10
src/api/dotnet/Params.cs
View file

@ -58,6 +58,16 @@ namespace Microsoft.Z3
Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value);
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, string value)
{
Contract.Requires(value != null);
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value).NativeObject);
}
/// <summary>
/// Adds a parameter setting.
/// </summary>

3
src/api/dotnet/TupleSort.cs
View file

@ -74,9 +74,10 @@ namespace Microsoft.Z3
Contract.Requires(name != null);
IntPtr t = IntPtr.Zero;
IntPtr[] f;
NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
ref t, new IntPtr[numFields]);
ref t, out f);
}
#endregion
};

169
src/api/java/InterpolationContext.java Normal file
View file

@ -0,0 +1,169 @@
/**
*
*/
package com.microsoft.z3;
import java.util.Map;
import java.lang.String;
import com.microsoft.z3.Native.IntPtr;
import com.microsoft.z3.Native.UIntArrayPtr;
import com.microsoft.z3.enumerations.Z3_lbool;
/** <summary>
* The InterpolationContext is suitable for generation of interpolants.
* </summary>
* <remarks>For more information on interpolation please refer
* too the C/C++ API, which is well documented.</remarks>
**/
public class InterpolationContext extends Context
{
/**
* Constructor.
**/
public InterpolationContext() throws Z3Exception
{
m_ctx = Native.mkInterpolationContext(0);
initContext();
}
/**
* Constructor.
*
* <remarks><seealso cref="Context.Context(Dictionary&lt;string, string&gt;)"/></remarks>
**/
public InterpolationContext(Map<String, String> settings) throws Z3Exception
{
long cfg = Native.mkConfig();
for (Map.Entry<String, String> kv : settings.entrySet())
Native.setParamValue(cfg, kv.getKey(), kv.getValue());
m_ctx = Native.mkInterpolationContext(cfg);
Native.delConfig(cfg);
initContext();
}
/**
* Create an expression that marks a formula position for interpolation.
* @throws Z3Exception
**/
public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception
{
checkContextMatch(a);
return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject()));
}
/**
* Computes an interpolant.
* <remarks>For more information on interpolation please refer
* too the function Z3_get_interpolant in the C/C++ API, which is
* well documented.</remarks>
* @throws Z3Exception
**/
Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception
{
checkContextMatch(pf);
checkContextMatch(pat);
checkContextMatch(p);
ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
int n = seq.size();
Expr[] res = new Expr[n];
for (int i = 0; i < n; i++)
res[i] = Expr.create(this, seq.get(i).getNativeObject());
return res;
}
/**
* Computes an interpolant.
* <remarks>For more information on interpolation please refer
* too the function Z3_compute_interpolant in the C/C++ API, which is
* well documented.</remarks>
* @throws Z3Exception
**/
Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception
{
checkContextMatch(pat);
checkContextMatch(p);
Native.LongPtr n_i = new Native.LongPtr();
Native.LongPtr n_m = new Native.LongPtr();
int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m);
interp = new ASTVector(this, n_i.value);
model = new Model(this, n_m.value);
return Z3_lbool.fromInt(r);
}
/// <summary>
/// Return a string summarizing cumulative time used for interpolation.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_interpolation_profile in the C/C++ API, which is
/// well documented.</remarks>
public String InterpolationProfile() throws Z3Exception
{
return Native.interpolationProfile(nCtx());
}
/// <summary>
/// Checks the correctness of an interpolant.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_check_interpolant in the C/C++ API, which is
/// well documented.</remarks>
public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception
{
Native.StringPtr n_err_str = new Native.StringPtr();
int r = Native.checkInterpolant(nCtx(),
cnsts.length,
Expr.arrayToNative(cnsts),
parents,
Expr.arrayToNative(interps),
n_err_str,
theory.length,
Expr.arrayToNative(theory));
error = n_err_str.value;
return r;
}
/// <summary>
/// Reads an interpolation problem from a file.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_read_interpolation_problem in the C/C++ API, which is
/// well documented.</remarks>
public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception
{
Native.IntPtr n_num = new Native.IntPtr();
Native.IntPtr n_num_theory = new Native.IntPtr();
Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
Native.StringPtr n_err_str = new Native.StringPtr();
int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
int num = n_num.value;
int num_theory = n_num_theory.value;
error = n_err_str.value;
cnsts = new Expr[num];
parents = new int[num];
theory = new Expr[num_theory];
for (int i = 0; i < num; i++)
{
cnsts[i] = Expr.create(this, n_cnsts.value[i]);
parents[i] = n_parents.value[i];
}
for (int i = 0; i < num_theory; i++)
theory[i] = Expr.create(this, n_theory.value[i]);
return r;
}
/// <summary>
/// Writes an interpolation problem to a file.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_write_interpolation_problem in the C/C++ API, which is
/// well documented.</remarks>
public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception
{
Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));
}
}

22
src/api/java/Params.java
View file

@ -28,6 +28,17 @@ public class Params extends Z3Object
Native.paramsSetDouble(getContext().nCtx(), getNativeObject(),
name.getNativeObject(), value);
}
/**
* Adds a parameter setting.
**/
public void add(Symbol name, String value) throws Z3Exception
{
Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
name.getNativeObject(),
getContext().mkSymbol(value).getNativeObject());
}
/**
* Adds a parameter setting.
@ -75,6 +86,17 @@ public class Params extends Z3Object
.mkSymbol(name).getNativeObject(), value.getNativeObject());
}
/**
* Adds a parameter setting.
**/
public void add(String name, String value) throws Z3Exception
{
Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
getContext().mkSymbol(name).getNativeObject(),
getContext().mkSymbol(value).getNativeObject());
}
/**
* A string representation of the parameter set.
**/

14
src/api/python/z3.py
View file

@ -7426,19 +7426,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.
@ -7477,10 +7477,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:
@ -7519,7 +7519,7 @@ def binary_interpolant(a,b,p=None,ctx=None):
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):
@ -7548,6 +7548,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)

1
src/api/z3.h
View file

@ -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

336
src/api/z3_api.h
View file

@ -1796,7 +1796,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[]);
@ -2133,17 +2133,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: <tt>ite(t1, t2,
@ -4957,8 +4947,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.
@ -4967,13 +4956,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 <mlx_parse_smtlib.idl>
@ -7931,314 +7919,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

277
src/api/z3_interp.h Normal file
View file

@ -0,0 +1,277 @@
/*++
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
/**
@name Interpolation
*/
/*@{*/
/**
\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)
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)
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
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

1
src/ast/rewriter/th_rewriter.cpp
View file

@ -75,6 +75,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);
}

10
src/cmd_context/context_params.cpp
View file

@ -114,15 +114,19 @@ 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) {

2
src/cmd_context/context_params.h
View file

@ -55,6 +55,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.

2
src/cmd_context/tactic_cmds.cpp
View file

@ -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:

2
src/muz/pdr/pdr_context.h
View file

@ -257,7 +257,7 @@ namespace pdr {
void enqueue_leaf(model_node& n); // add leaf to priority queue.
void update_models();
public:
model_search(bool bfs): m_bfs(bfs), m_root(0) {}
model_search(bool bfs): m_bfs(bfs), m_root(0) {}
~model_search();
void reset();

20
src/opt/opt_solver.cpp
View file

@ -161,17 +161,27 @@ namespace opt {
void opt_solver::maximize_objectives(expr_ref_vector& blockers) {
expr_ref blocker(m);
vector<inf_eps> values;
for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
values.push_back(current_objective_value(i));
}
for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
maximize_objective(i, blocker);
blockers.push_back(blocker);
if (values[i] > m_objective_values[i]) {
std::cout << "local optimization produced a worse result\n";
exit(0);
}
}
}
void opt_solver::maximize_objective(unsigned i, expr_ref& blocker) {
smt::theory_var v = m_objective_vars[i];
m_objective_values[i] = get_optimizer().maximize(v, blocker);
m_context.get_context().update_model();
TRACE("opt", { model_ref mdl; get_model(mdl); model_smt2_pp(tout << "update model: ", m, *mdl, 0); });
TRACE("opt", { model_ref mdl; tout << m_objective_values[i] << "\n";
get_model(mdl); model_smt2_pp(tout << "update model: ", m, *mdl, 0); });
}
void opt_solver::get_unsat_core(ptr_vector<expr> & r) {
@ -232,10 +242,16 @@ namespace opt {
return m_objective_values;
}
inf_eps const& opt_solver::get_objective_value(unsigned i) {
inf_eps const& opt_solver::saved_objective_value(unsigned i) {
return m_objective_values[i];
}
inf_eps opt_solver::current_objective_value(unsigned i) {
smt::theory_var v = m_objective_vars[i];
return get_optimizer().value(v);
}
expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& val) {
smt::theory_opt& opt = get_optimizer();
smt::theory_var v = m_objective_vars[var];

3
src/opt/opt_solver.h
View file

@ -107,9 +107,10 @@ namespace opt {
void reset_objectives();
void maximize_objective(unsigned i, expr_ref& blocker);
void maximize_objectives(expr_ref_vector& blockers);
inf_eps const & saved_objective_value(unsigned obj_index);
inf_eps current_objective_value(unsigned obj_index);
vector<inf_eps> const& get_objective_values();
inf_eps const & get_objective_value(unsigned obj_index);
expr_ref mk_ge(unsigned obj_index, inf_eps const& val);
static opt_solver& to_opt(solver& s);

36
src/opt/optsmt.cpp
View file

@ -46,12 +46,21 @@ namespace opt {
m_cancel = f;
}
void optsmt::set_max(vector<inf_eps>& dst, vector<inf_eps> const& src) {
void optsmt::set_max(vector<inf_eps>& dst, vector<inf_eps> const& src, expr_ref_vector& fmls) {
for (unsigned i = 0; i < src.size(); ++i) {
if (src[i] > dst[i]) {
dst[i] = src[i];
m_lower_fmls[i] = fmls[i].get();
if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already.
m_lower_fmls[i] = m.mk_false();
fmls[i] = m.mk_false();
}
}
else if (src[i] < dst[i] && !m.is_true(m_lower_fmls[i].get())) {
fmls[i] = m_lower_fmls[i].get();
}
}
std::cout << "\n";
}
/*
@ -131,20 +140,17 @@ namespace opt {
disj.reset();
m_s->maximize_objectives(disj);
m_s->get_model(m_model);
set_max(m_lower, m_s->get_objective_values());
for (unsigned i = 0; i < ors.size(); ++i) {
expr_ref tmp(m);
m_model->eval(ors[i].get(), tmp);
if (m.is_true(tmp)) {
m_lower[i] = m_upper[i];
ors[i] = m.mk_false();
}
if (m.is_false(ors[i].get())) {
ors[i] = m.mk_false();
disj[i] = m.mk_false();
}
}
set_max(m_lower, m_s->get_objective_values(), disj);
or = m.mk_or(ors.size(), ors.c_ptr());
bound = m.mk_or(disj.size(), disj.c_ptr());
m_s->assert_expr(or);
}
else if (is_sat == l_undef) {
@ -155,6 +161,7 @@ namespace opt {
}
}
}
bound = m.mk_or(m_lower_fmls.size(), m_lower_fmls.c_ptr());
m_s->assert_expr(bound);
if (m_cancel) {
@ -177,9 +184,9 @@ namespace opt {
void optsmt::update_lower() {
expr_ref_vector disj(m);
m_s->maximize_objectives(disj);
m_s->get_model(m_model);
set_max(m_lower, m_s->get_objective_values());
m_s->maximize_objectives(disj);
set_max(m_lower, m_s->get_objective_values(), disj);
TRACE("opt",
for (unsigned i = 0; i < m_lower.size(); ++i) {
tout << m_lower[i] << " ";
@ -192,11 +199,8 @@ namespace opt {
verbose_stream() << m_lower[i] << " ";
}
verbose_stream() << ")\n";);
for (unsigned i = 0; i < m_lower.size(); ++i) {
if (m_lower[i].is_pos() && !m_lower[i].is_finite()) {
disj[i] = m.mk_false();
}
}
IF_VERBOSE(3, verbose_stream() << disj << "\n";);
IF_VERBOSE(3, model_pp(verbose_stream(), *m_model););
expr_ref constraint(m);
constraint = m.mk_or(disj.size(), disj.c_ptr());
@ -309,7 +313,7 @@ namespace opt {
m_s->maximize_objective(obj_index, block);
m_s->get_model(m_model);
inf_eps obj = m_s->get_objective_value(obj_index);
inf_eps obj = m_s->saved_objective_value(obj_index);
if (obj > m_lower[obj_index]) {
m_lower[obj_index] = obj;
IF_VERBOSE(1,
@ -320,7 +324,7 @@ namespace opt {
);
for (unsigned i = obj_index+1; i < m_vars.size(); ++i) {
m_s->maximize_objective(i, tmp);
m_lower[i] = m_s->get_objective_value(i);
m_lower[i] = m_s->saved_objective_value(i);
}
}
m_s->assert_expr(block);
@ -401,6 +405,7 @@ namespace opt {
m_objs.push_back(to_app(t2));
m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
m_lower_fmls.push_back(m.mk_true());
return m_objs.size()-1;
}
@ -415,6 +420,7 @@ namespace opt {
m_objs.reset();
m_vars.reset();
m_model.reset();
m_lower_fmls.reset();
m_s = 0;
}
}

6
src/opt/optsmt.h
View file

@ -34,11 +34,13 @@ namespace opt {
vector<inf_eps> m_lower;
vector<inf_eps> m_upper;
app_ref_vector m_objs;
expr_ref_vector m_lower_fmls;
svector<smt::theory_var> m_vars;
symbol m_optsmt_engine;
model_ref m_model;
public:
optsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_objs(m) {}
optsmt(ast_manager& m):
m(m), m_s(0), m_cancel(false), m_objs(m), m_lower_fmls(m) {}
void setup(opt_solver& solver);
@ -73,7 +75,7 @@ namespace opt {
lbool farkas_opt();
void set_max(vector<inf_eps>& dst, vector<inf_eps> const& src);
void set_max(vector<inf_eps>& dst, vector<inf_eps> const& src, expr_ref_vector& fmls);
void update_lower();

23
src/qe/qe.cpp
View file

@ -2238,8 +2238,7 @@ namespace qe {
m_params(p),
m_trail(m),
m_qe(0),
m_assumption(m.mk_true()),
m_use_new_qe(true)
m_assumption(m.mk_true())
{
}
@ -2261,12 +2260,6 @@ namespace qe {
}
void expr_quant_elim::updt_params(params_ref const& p) {
bool r = p.get_bool("use_neq_qe", m_use_new_qe);
if (r != m_use_new_qe) {
dealloc(m_qe);
m_qe = 0;
m_use_new_qe = r;
}
init_qe();
m_qe->updt_params(p);
}
@ -2274,7 +2267,6 @@ namespace qe {
void expr_quant_elim::collect_param_descrs(param_descrs& r) {
r.insert("eliminate_variables_as_block", CPK_BOOL,
"(default: true) eliminate variables as a block (true) or one at a time (false)");
// r.insert("use_new_qe", CPK_BOOL, "(default: true) invoke quantifier engine based on abstracted solver");
}
void expr_quant_elim::init_qe() {
@ -2517,6 +2509,10 @@ namespace qe {
add_plugin(mk_arith_plugin(*this, false, m_fparams));
}
void updt_params(params_ref const& p) {
m_fparams.updt_params(p);
}
virtual ~simplify_solver_context() { reset(); }
void solve(expr_ref& fml, app_ref_vector& vars) {
@ -2607,6 +2603,10 @@ namespace qe {
public:
impl(ast_manager& m) : m(m), m_ctx(m) {}
void updt_params(params_ref const& p) {
m_ctx.updt_params(p);
}
bool reduce_quantifier(
quantifier * old_q,
expr * new_body,
@ -2670,6 +2670,10 @@ namespace qe {
return imp->reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr);
}
void simplify_rewriter_cfg::updt_params(params_ref const& p) {
imp->updt_params(p);
}
bool simplify_rewriter_cfg::pre_visit(expr* e) {
if (!is_quantifier(e)) return true;
quantifier * q = to_quantifier(e);
@ -2677,7 +2681,6 @@ namespace qe {
}
void simplify_exists(app_ref_vector& vars, expr_ref& fml) {
smt_params params;
ast_manager& m = fml.get_manager();
simplify_solver_context ctx(m);
ctx.solve(fml, vars);

7
src/qe/qe.h
View file

@ -275,13 +275,12 @@ namespace qe {
class expr_quant_elim {
ast_manager& m;
smt_params const& m_fparams;
smt_params const& m_fparams;
params_ref m_params;
expr_ref_vector m_trail;
obj_map<expr,expr*> m_visited;
quant_elim* m_qe;
expr* m_assumption;
bool m_use_new_qe;
public:
expr_quant_elim(ast_manager& m, smt_params const& fp, params_ref const& p = params_ref());
~expr_quant_elim();
@ -372,6 +371,8 @@ namespace qe {
bool pre_visit(expr* e);
void updt_params(params_ref const& p);
};
class simplify_rewriter_star : public rewriter_tpl<simplify_rewriter_cfg> {
@ -380,6 +381,8 @@ namespace qe {
simplify_rewriter_star(ast_manager& m):
rewriter_tpl<simplify_rewriter_cfg>(m, false, m_cfg),
m_cfg(m) {}
void updt_params(params_ref const& p) { m_cfg.updt_params(p); }
};
};

9
src/qe/qe_sat_tactic.cpp
View file

@ -74,6 +74,7 @@ namespace qe {
is_relevant_default m_is_relevant;
mk_atom_default m_mk_atom;
th_rewriter m_rewriter;
simplify_rewriter_star m_qe_rw;
expr_strong_context_simplifier m_ctx_rewriter;
class solver_context : public i_solver_context {
@ -218,6 +219,7 @@ namespace qe {
m_Ms(m),
m_assignments(m),
m_rewriter(m),
m_qe_rw(m),
m_ctx_rewriter(m_fparams, m) {
m_fparams.m_model = true;
}
@ -256,10 +258,9 @@ namespace qe {
ptr_vector<expr> fmls;
goal->get_formulas(fmls);
m_fml = m.mk_and(fmls.size(), fmls.c_ptr());
TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";);
simplify_rewriter_star rw(m);
TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";);
expr_ref tmp(m);
rw(m_fml, tmp);
m_qe_rw(m_fml, tmp);
m_fml = tmp;
TRACE("qe", tout << "reduced: " << mk_pp(m_fml,m) << "\n";);
skolemize_existential_prefix();
@ -305,6 +306,8 @@ namespace qe {
m_projection_mode_param = p.get_bool("projection_mode", m_projection_mode_param);
m_strong_context_simplify_param = p.get_bool("strong_context_simplify", m_strong_context_simplify_param);
m_ctx_simplify_local_param = p.get_bool("strong_context_simplify_local", m_ctx_simplify_local_param);
m_fparams.updt_params(p);
m_qe_rw.updt_params(p);
}
virtual void collect_param_descrs(param_descrs & r) {

1
src/qe/qe_tactic.cpp
View file

@ -36,6 +36,7 @@ class qe_tactic : public tactic {
}
void updt_params(params_ref const & p) {
m_fparams.updt_params(p);
m_fparams.m_nlquant_elim = p.get_bool("qe_nonlinear", false);
m_qe.updt_params(p);
}

1
src/sat/sat_simplifier.cpp
View file

@ -1426,7 +1426,6 @@ namespace sat {
void simplifier::elim_vars() {
if (!m_elim_vars) return;
elim_var_report rpt(*this);
bool_var_vector vars;
order_vars_for_elim(vars);

3
src/smt/params/smt_params.cpp
View file

@ -19,10 +19,11 @@ Revision History:
#include"smt_params.h"
#include"smt_params_helper.hpp"
#include"model_params.hpp"
#include"gparams.h"
void smt_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
m_auto_config = p.auto_config();
m_auto_config = p.auto_config() && gparams::get_value("auto_config") == "true"; // auto-config is not scoped by smt in gparams.
m_random_seed = p.random_seed();
m_relevancy_lvl = p.relevancy();
m_ematching = p.ematching();

1
src/smt/theory_arith.h
View file

@ -1017,6 +1017,7 @@ namespace smt {
//
// -----------------------------------
virtual inf_eps_rational<inf_rational> maximize(theory_var v, expr_ref& blocker);
virtual inf_eps_rational<inf_rational> value(theory_var v);
virtual theory_var add_objective(app* term);
virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val);
void enable_record_conflict(expr* bound);

23
src/smt/theory_arith_aux.h
View file

@ -1059,7 +1059,6 @@ namespace smt {
theory_var theory_arith<Ext>::add_objective(app* term) {
theory_var v = internalize_term_core(term);
TRACE("opt", tout << mk_pp(term, get_manager()) << " |-> v" << v << "\n";);
TRACE("opt", tout << "data-size: " << m_data.size() << "\n";);
SASSERT(!is_quasi_base(v));
if (!is_linear(get_manager(), term)) {
v = null_theory_var;
@ -1067,6 +1066,11 @@ namespace smt {
return v;
}
template<typename Ext>
inf_eps_rational<inf_rational> theory_arith<Ext>::value(theory_var v) {
return inf_eps_rational<inf_rational>(get_value(v));
}
template<typename Ext>
inf_eps_rational<inf_rational> theory_arith<Ext>::maximize(theory_var v, expr_ref& blocker) {
TRACE("bound_bug", display_var(tout, v); display(tout););
@ -1533,12 +1537,14 @@ namespace smt {
*/
template<typename Ext>
typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min(theory_var v, bool max) {
TRACE("opt", tout << (max ? "maximizing" : "minimizing") << " v" << v << "...\n";);
expr* e = get_enode(v)->get_owner();
SASSERT(valid_row_assignment());
SASSERT(satisfy_bounds());
SASSERT(!is_quasi_base(v));
if ((max && at_upper(v)) || (!max && at_lower(v)))
if ((max && at_upper(v)) || (!max && at_lower(v))) {
TRACE("opt", tout << "At bound: " << mk_pp(e, get_manager()) << "...\n";);
return AT_BOUND; // nothing to be done...
}
m_tmp_row.reset();
if (is_non_base(v)) {
add_tmp_row_entry<false>(m_tmp_row, numeral(1), v);
@ -1554,11 +1560,16 @@ namespace smt {
}
max_min_t r = max_min(m_tmp_row, max);
if (r == OPTIMIZED) {
TRACE("opt", tout << "v" << v << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n";
TRACE("opt", tout << mk_pp(e, get_manager()) << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n";
display_row(tout, m_tmp_row, true); display_row_info(tout, m_tmp_row););
mk_bound_from_row(v, get_value(v), max ? B_UPPER : B_LOWER, m_tmp_row);
mk_bound_from_row(v, get_value(v), max ? B_UPPER : B_LOWER, m_tmp_row);
}
else if (r == UNBOUNDED) {
TRACE("opt", tout << "unbounded: " << mk_pp(e, get_manager()) << "...\n";);
}
else {
TRACE("opt", tout << "not optimized: " << mk_pp(e, get_manager()) << "...\n";);
}
return r;
}

32
src/smt/theory_bv.cpp
View file

@ -53,6 +53,7 @@ namespace smt {
unsigned bv_size = get_bv_size(n);
context & ctx = get_context();
literal_vector & bits = m_bits[v];
bits.reset();
for (unsigned i = 0; i < bv_size; i++) {
app * bit = mk_bit2bool(owner, i);
ctx.internalize(bit, true);
@ -75,12 +76,14 @@ namespace smt {
void theory_bv::mk_bit2bool(app * n) {
context & ctx = get_context();
SASSERT(!ctx.b_internalized(n));
if (!ctx.e_internalized(n->get_arg(0))) {
expr* first_arg = n->get_arg(0);
if (!ctx.e_internalized(first_arg)) {
// This may happen if bit2bool(x) is in a conflict
// clause that is being reinitialized, and x was not reinitialized
// yet.
// So, we internalize x (i.e., n->get_arg(0))
expr * first_arg = n->get_arg(0);
// So, we internalize x (i.e., arg)
ctx.internalize(first_arg, false);
SASSERT(ctx.e_internalized(first_arg));
// In most cases, when x is internalized, its bits are created.
@ -91,10 +94,27 @@ namespace smt {
// This will also force the creation of all bits for x.
enode * first_arg_enode = ctx.get_enode(first_arg);
get_var(first_arg_enode);
SASSERT(ctx.b_internalized(n));
// numerals are not blasted into bit2bool, so we do this directly.
if (!ctx.b_internalized(n)) {
rational val;
unsigned sz;
VERIFY(m_util.is_numeral(first_arg, val, sz));
theory_var v = first_arg_enode->get_th_var(get_id());
app* owner = first_arg_enode->get_owner();
for (unsigned i = 0; i < sz; ++i) {
ctx.internalize(mk_bit2bool(owner, i), true);
}
m_bits[v].reset();
rational bit;
for (unsigned i = 0; i < sz; ++i) {
div(val, rational::power_of_two(i), bit);
mod(bit, rational(2), bit);
m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);
}
}
}
else {
enode * arg = ctx.get_enode(n->get_arg(0));
enode * arg = ctx.get_enode(first_arg);
// The argument was already internalized, but it may not have a theory variable associated with it.
// For example, for ite-terms the method apply_sort_cnstr is not invoked.
// See comment in the then-branch.
@ -1041,6 +1061,7 @@ namespace smt {
void theory_bv::new_diseq_eh(theory_var v1, theory_var v2) {
if (is_bv(v1)) {
SASSERT(m_bits[v1].size() == m_bits[v2].size());
expand_diseq(v1, v2);
}
}
@ -1381,6 +1402,7 @@ namespace smt {
if (v1 != null_theory_var) {
// conflict was detected ... v1 and v2 have complementary bits
SASSERT(m_bits[v1][it->m_idx] == ~(m_bits[v2][it->m_idx]));
SASSERT(m_bits[v1].size() == m_bits[v2].size());
mk_new_diseq_axiom(v1, v2, it->m_idx);
RESET_MERGET_AUX();
return false;

1
src/smt/theory_dense_diff_logic.h
View file

@ -267,6 +267,7 @@ namespace smt {
// -----------------------------------
virtual inf_eps_rational<inf_rational> maximize(theory_var v, expr_ref& blocker);
virtual inf_eps_rational<inf_rational> value(theory_var v);
virtual theory_var add_objective(app* term);
virtual expr_ref mk_gt(theory_var v, inf_rational const& val);
virtual expr* mk_ge(theory_var v, inf_rational const& val) { return 0; }

13
src/smt/theory_dense_diff_logic_def.h
View file

@ -875,6 +875,19 @@ namespace smt {
return true;
}
template<typename Ext>
inf_eps_rational<inf_rational> theory_dense_diff_logic<Ext>::value(theory_var v) {
objective_term const& objective = m_objectives[v];
inf_eps r = inf_eps(m_objective_consts[v]);
for (unsigned i = 0; i < objective.size(); ++i) {
numeral n = m_assignment[v];
rational r1 = n.get_rational().to_rational();
rational r2 = n.get_infinitesimal().to_rational();
r += objective[i].second * inf_eps(rational(0), inf_rational(r1, r2));
}
return r;
}
template<typename Ext>
inf_eps_rational<inf_rational> theory_dense_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker) {
typedef simplex::simplex<simplex::mpq_ext> Simplex;

4
src/smt/theory_diff_logic.h
View file

@ -65,6 +65,7 @@ namespace smt {
typedef typename Ext::numeral numeral;
typedef simplex::simplex<simplex::mpq_ext> Simplex;
typedef inf_eps_rational<inf_rational> inf_eps;
class atom {
bool_var m_bvar;
@ -319,7 +320,8 @@ namespace smt {
//
// -----------------------------------
virtual inf_eps_rational<inf_rational> maximize(theory_var v, expr_ref& blocker);
virtual inf_eps maximize(theory_var v, expr_ref& blocker);
virtual inf_eps value(theory_var v);
virtual theory_var add_objective(app* term);
virtual expr_ref mk_gt(theory_var v, inf_rational const& val);
virtual expr* mk_ge(theory_var v, inf_rational const& val) { return 0; }

33
src/smt/theory_diff_logic_def.h
View file

@ -1078,43 +1078,32 @@ void theory_diff_logic<Ext>::get_implied_bound_antecedents(edge_id bridge_edge,
template<typename Ext>
unsigned theory_diff_logic<Ext>::node2simplex(unsigned v) {
//return v;
return m_objectives.size() + 2*v + 1;
}
template<typename Ext>
unsigned theory_diff_logic<Ext>::edge2simplex(unsigned e) {
//return m_graph.get_num_nodes() + e;
return m_objectives.size() + 2*e;
}
template<typename Ext>
unsigned theory_diff_logic<Ext>::obj2simplex(unsigned e) {
//return m_graph.get_num_nodes() + m_graph.get_num_edges() + e;
return e;
}
template<typename Ext>
unsigned theory_diff_logic<Ext>::num_simplex_vars() {
//return m_graph.get_num_nodes() + m_graph.get_num_edges() + m_objectives.size();
return m_objectives.size() + std::max(2*m_graph.get_num_edges(),2*m_graph.get_num_nodes()+1);
}
template<typename Ext>
bool theory_diff_logic<Ext>::is_simplex_edge(unsigned e) {
#if 0
return
m_graph.get_num_nodes() <= e &&
e < m_graph.get_num_nodes() + m_graph.get_num_edges();
#else
if (e < m_objectives.size()) return false;
e -= m_objectives.size();
return (0 == (e & 0x1));
#endif
}
template<typename Ext>
unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
SASSERT(is_simplex_edge(e));
//return e - m_graph.get_num_nodes();
return (e - m_objectives.size())/2;
}
@ -1184,7 +1173,21 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
}
template<typename Ext>
inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker) {
typename theory_diff_logic<Ext>::inf_eps theory_diff_logic<Ext>::value(theory_var v) {
objective_term const& objective = m_objectives[v];
inf_eps r = inf_eps(m_objective_consts[v]);
for (unsigned i = 0; i < objective.size(); ++i) {
numeral n = m_graph.get_assignment(v);
rational r1 = n.get_rational().to_rational();
rational r2 = n.get_infinitesimal().to_rational();
r += objective[i].second * inf_eps(rational(0), inf_rational(r1, r2));
}
return r;
}
template<typename Ext>
typename theory_diff_logic<Ext>::inf_eps
theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker) {
Simplex& S = m_S;
ast_manager& m = get_manager();
@ -1206,7 +1209,7 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v, ex
lbool is_sat = S.make_feasible();
if (is_sat == l_undef) {
blocker = m.mk_false();
return inf_eps_rational<inf_rational>::infinity();
return inf_eps::infinity();
}
TRACE("opt", S.display(tout); );
SASSERT(is_sat != l_false);
@ -1233,12 +1236,12 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v, ex
}
}
blocker = mk_gt(v, r);
return inf_eps_rational<inf_rational>(rational(0), r);
return inf_eps(rational(0), r);
}
default:
TRACE("opt", tout << "unbounded\n"; );
blocker = m.mk_false();
return inf_eps_rational<inf_rational>::infinity();
return inf_eps::infinity();
}
}

1
src/smt/theory_opt.h
View file

@ -30,6 +30,7 @@ namespace smt {
class theory_opt {
public:
typedef inf_eps_rational<inf_rational> inf_eps;
virtual inf_eps value(theory_var) = 0;
virtual inf_eps maximize(theory_var v, expr_ref& blocker) = 0;
virtual theory_var add_objective(app* term) = 0;
virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return 0; }

57
src/util/params.cpp
View file

@ -97,6 +97,35 @@ struct param_descrs::imp {
return CPK_INVALID;
}
bool split_name(symbol const& name, symbol & prefix, symbol & suffix) const {
if (name.is_numerical()) return false;
char const* str = name.bare_str();
char const* period = strchr(str,'.');
if (!period) return false;
svector<char> prefix_((unsigned)(period-str), str);
prefix_.push_back(0);
prefix = symbol(prefix_.c_ptr());
suffix = symbol(period + 1);
return true;
}
param_kind get_kind_in_module(symbol & name) const {
param_kind k = get_kind(name);
symbol prefix, suffix;
if (k == CPK_INVALID && split_name(name, prefix, suffix)) {
k = get_kind(suffix);
if (k != CPK_INVALID) {
if (symbol(get_module(suffix)) == prefix) {
name = suffix;
}
else {
k = CPK_INVALID;
}
}
}
return k;
}
char const* get_module(symbol const& name) const {
info i;
if (m_info.find(name, i))
@ -230,6 +259,10 @@ void param_descrs::erase(char const * name) {
erase(symbol(name));
}
param_kind param_descrs::get_kind_in_module(symbol & name) const {
return m_imp->get_kind_in_module(name);
}
param_kind param_descrs::get_kind(symbol const & name) const {
return m_imp->get_kind(name);
}
@ -311,35 +344,13 @@ public:
void reset(symbol const & k);
void reset(char const * k);
bool split_name(symbol const& name, symbol & prefix, symbol & suffix) {
if (name.is_numerical()) return false;
char const* str = name.bare_str();
char const* period = strchr(str,'.');
if (!period) return false;
svector<char> prefix_((unsigned)(period-str), str);
prefix_.push_back(0);
prefix = symbol(prefix_.c_ptr());
suffix = symbol(period + 1);
return true;
}
void validate(param_descrs const & p) {
svector<params::entry>::iterator it = m_entries.begin();
svector<params::entry>::iterator end = m_entries.end();
symbol suffix, prefix;
for (; it != end; ++it) {
param_kind expected = p.get_kind(it->first);
if (expected == CPK_INVALID && split_name(it->first, prefix, suffix)) {
expected = p.get_kind(suffix);
if (expected != CPK_INVALID) {
if (symbol(p.get_module(suffix)) == prefix) {
it->first = suffix;
}
else {
expected = CPK_INVALID;
}
}
}
param_kind expected = p.get_kind_in_module(it->first);
if (expected == CPK_INVALID) {
std::stringstream strm;
strm << "unknown parameter '" << it->first.str() << "'\n";

1
src/util/params.h
View file

@ -123,6 +123,7 @@ public:
void erase(symbol const & name);
param_kind get_kind(char const * name) const;
param_kind get_kind(symbol const & name) const;
param_kind get_kind_in_module(symbol & name) const;
char const * get_descr(char const * name) const;
char const * get_descr(symbol const & name) const;
char const * get_default(char const * name) const;

2
src/util/scoped_timer.cpp
View file

@ -129,7 +129,7 @@ struct scoped_timer::imp {
WT_EXECUTEINTIMERTHREAD);
#elif defined(__APPLE__) && defined(__MACH__)
// Mac OS X
m_interval = ms;
m_interval = ms?ms:0xFFFFFFFF;
if (pthread_attr_init(&m_attributes) != 0)
throw default_exception("failed to initialize timer thread attributes");
if (pthread_cond_init(&m_condition_var, NULL) != 0)

21
src/util/stopwatch.h
View file

@ -91,7 +91,7 @@ public:
~stopwatch() {}
void reset() {
m_time = 0ull;
m_time = 0ull;
}
void start() {
@ -102,11 +102,11 @@ public:
}
void stop() {
if (m_running) {
if (m_running) {
mach_timespec_t _stop;
clock_get_time(m_host_clock, &_stop);
m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull;
m_time += (_stop.tv_nsec - m_start.tv_nsec);
m_time += (_stop.tv_nsec - m_start.tv_nsec);
m_running = false;
}
}
@ -121,7 +121,7 @@ public:
}
double get_current_seconds() const {
return get_seconds();
return get_seconds();
}
};
@ -142,22 +142,23 @@ public:
~stopwatch() {}
void reset() {
m_time = 0ull;
m_time = 0ull;
}
void start() {
if (!m_running) {
clock_gettime(CLOCK_THREAD_CPUTIME_ID, &m_start);
clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &m_start);
m_running = true;
}
}
void stop() {
if (m_running) {
if (m_running) {
struct timespec _stop;
clock_gettime(CLOCK_THREAD_CPUTIME_ID, &_stop);
clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &_stop);
m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull;
m_time += (_stop.tv_nsec - m_start.tv_nsec);
if (m_time != 0 || _stop.tv_nsec >= m_start.tv_nsec)
m_time += (_stop.tv_nsec - m_start.tv_nsec);
m_running = false;
}
}
@ -172,7 +173,7 @@ public:
}
double get_current_seconds() const {
return get_seconds();
return get_seconds();
}
};